diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-09-22 15:40:48 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-22 17:40:48 -0500 |
| commit | 30e6dc83aed15ef002087e55cf228f0735c63f40 (patch) | |
| tree | 76547d252a34cc2b56015957e2d5f9740b1002b2 /src/smt | |
| parent | e4a29a6033ecc7ba5ec266f37e8f151f09ead020 (diff) | |
Add simple BV solver (#5065)
This PR adds a simple BV solver that sends bit-blasting lemmas to the internal MiniSat.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/set_defaults.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 2dc0d52ac..32e716ab2 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -124,6 +124,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } + /* BVSolver::SIMPLE does not natively support int2bv and nat2bv, they need to + * to be eliminated eagerly. */ + if (options::bvSolver() == options::BVSolver::SIMPLE) + { + options::bvLazyReduceExtf.set(false); + options::bvLazyRewriteExtf.set(false); + } + if (options::solveIntAsBV() > 0) { // not compatible with incremental |