acl2-experiment

ACL2 experiments on arithmetic circuits

Experimental

The code here is pure experiment. Don't expect it to be maintained.

Is this cutting-edge?

No. This is just an experiment using an existing library in an elementary way. For more advanced usage of the library see the paper by the original authors of the library.

Where is the theorem?

Here. It says some conditions about constraints imply add32p.

How to reproduce

1. Install acl2. The code was developed using the ACL2 commit ID 17138a64970a2ec5159c36d0dcedbba3cb0e3583. Build books using make regression (or later by need when you get stuck).
2. Run saved_acl2
3. Paste the contents of package.lsp in this directory into the ACL2 console.
4. Paste the contents of add32.lisp in this directory into the ACL2 console.