diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-02-03 12:38:09 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-03 12:38:09 -0800 |
| commit | ac998a45ae64c589aeb79c5fd72234468e40451c (patch) | |
| tree | ade5266bbc0a5279ea76b4eb5c9d8a77e3ab967d /src/CMakeLists.txt | |
| parent | a6c122da21b3d5b9c37d9ec670dec766eaff7001 (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.
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0929b6625..c5673a396 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -525,6 +525,8 @@ libcvc4_add_sources( theory/bv/bv_quick_check.cpp theory/bv/bv_quick_check.h theory/bv/bv_solver.h + theory/bv/bv_solver_bitblast.cpp + theory/bv/bv_solver_bitblast.h theory/bv/bv_solver_lazy.cpp theory/bv/bv_solver_lazy.h theory/bv/bv_solver_simple.cpp |