projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a6c122d) | patch
Add BV solver bitblast. (#5851)
authorMathias Preiner <mathias.preiner@gmail.com>
Wed, 3 Feb 2021 20:38:09 +0000 (12:38 -0800)
committerGitHub <noreply@github.com>
Wed, 3 Feb 2021 20:38:09 +0000 (12:38 -0800)
commitac998a45ae64c589aeb79c5fd72234468e40451c
treeade5266bbc0a5279ea76b4eb5c9d8a77e3ab967dtree
parenta6c122da21b3d5b9c37d9ec670dec766eaff7001commit | diff
Add BV solver bitblast. (#5851)

This PR adds a new bit-blasting BV solver, which can be enabled via --bv-solver=bitblast. The new bit-blast solver can be used instead of the lazy BV solver and currently supports CaDiCaL and CryptoMiniSat as SAT back end.
16 files changed:
src/CMakeLists.txt diff | blob | history
src/options/bv_options.toml diff | blob | history
src/options/options_handler.cpp diff | blob | history
src/prop/cadical.cpp diff | blob | history
src/prop/cadical.h diff | blob | history
src/prop/cryptominisat.cpp diff | blob | history
src/prop/cryptominisat.h diff | blob | history
src/prop/sat_solver.h diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/bv/bitblast/bitblast_strategies_template.h diff | blob | history
src/theory/bv/bitblast/simple_bitblaster.cpp diff | blob | history
src/theory/bv/bitblast/simple_bitblaster.h diff | blob | history
src/theory/bv/bv_solver_bitblast.cpp [new file with mode: 0644] blob
src/theory/bv/bv_solver_bitblast.h [new file with mode: 0644] blob
src/theory/bv/theory_bv.cpp diff | blob | history
src/theory/bv/theory_bv.h diff | blob | history