ACL2 experiments on arithmetic circuits
The code here is pure experiment. Don't expect it to be maintained.
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.
Here. It says some conditions about constraints imply add32p.
- 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). - Run
saved_acl2 - Paste the contents of
package.lspin this directory into the ACL2 console. - Paste the contents of
add32.lispin this directory into the ACL2 console.