The implementation of quantifier elimination for bit vector arithmetic based on elimination of quantifiers for Presburger arithmetic expanded by function (in progress).
Download and build boolector according to the instructions given here: https://github.com/Boolector/boolector.
Use make, to build the project.
./main tests/<test_file> <out_file>
If you want check the result use python check.py tests/<test_file> <out_file>
The folder tests contains five subfolders:
- benchmarks contains tests used for conducting the experiments reported in the report;
- simp_lin contains tests with a trivial occurrence of the bound variable;
- simp_exp contains those tests in which the bound variable occurs trivially in an exponential term;
- simp_mix contains tests with conjunctions of formulas of said two types;
- lin contains tests with a linear (non-trivial) occurrence of the bound variable;
- exp contains those tests in which the bound variable occurs non trivially in an exponential term.
The implementation is currently working for formulas like (instead of there can be
, instead of ≤ there can be < or =)
, where
— free variables,
— terms in the signature of Presburger arithmetic expanded by
.
.
To run all tests and check the output use bash all_tests.sh [-check] or bash all_tests.sh [-check] <folder> if you want to run tests from the specific folder from tests/.
More details about the project can be found in pres/course.pdf and pres/slides.pdf.