projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 69b463e) | patch
Optimizer for BitVectors (#6213)
authorYancheng Ou <ou2@ualberta.ca>
Mon, 5 Apr 2021 13:21:40 +0000 (06:21 -0700)
committerGitHub <noreply@github.com>
Mon, 5 Apr 2021 13:21:40 +0000 (08:21 -0500)
commit3f1ab5672ca746a4a6573e1ebf9f74d72978d1cf
tree86518c88e615cbf7cc0cc3d37cc9866d1bfbb6c4tree
parent69b463e1b1150715b2f4179786ddab8ba0c43b37commit | diff
Optimizer for BitVectors (#6213)

Adds support for BitVector optimization, which is done via offline binary search. Units tests included.
Also mildly refactors the optimizer architecture.
12 files changed:
src/CMakeLists.txt diff | blob | history
src/omt/bitvector_optimizer.cpp [new file with mode: 0644] blob
src/omt/bitvector_optimizer.h [new file with mode: 0644] blob
src/omt/integer_optimizer.cpp [new file with mode: 0644] blob
src/omt/integer_optimizer.h [new file with mode: 0644] blob
src/omt/omt_optimizer.cpp [new file with mode: 0644] blob
src/omt/omt_optimizer.h [new file with mode: 0644] blob
src/smt/optimization_solver.cpp diff | blob | history
src/smt/optimization_solver.h diff | blob | history
test/unit/theory/CMakeLists.txt diff | blob | history
test/unit/theory/theory_bv_opt_white.cpp [new file with mode: 0644] blob
test/unit/theory/theory_int_opt_white.cpp diff | blob | history