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/theory/quantifiers/equality_query.cpp | |
| 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/theory/quantifiers/equality_query.cpp')
0 files changed, 0 insertions, 0 deletions