diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-08-02 14:33:34 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-02 21:33:34 +0000 |
| commit | 13fe59109928f6ca173691a94b705ad3225aeb85 (patch) | |
| tree | 6d6b5f86ecb73e9c055512754ac4b65658202861 | |
| parent | fda46132b3f5c945a2b5e75bfa6bd5c84525fee6 (diff) | |
bv: Enable equality engine for bitblast-internal. (#6961)
| -rw-r--r-- | src/theory/bv/bv_solver_bitblast_internal.cpp | 8 | ||||
| -rw-r--r-- | src/theory/bv/bv_solver_bitblast_internal.h | 2 | ||||
| -rw-r--r-- | src/theory/theory.cpp | 6 | ||||
| -rw-r--r-- | test/regress/regress2/bug349.smtv1.smt2 | 1 |
4 files changed, 10 insertions, 7 deletions
diff --git a/src/theory/bv/bv_solver_bitblast_internal.cpp b/src/theory/bv/bv_solver_bitblast_internal.cpp index ef4f3559b..1b606a0e9 100644 --- a/src/theory/bv/bv_solver_bitblast_internal.cpp +++ b/src/theory/bv/bv_solver_bitblast_internal.cpp @@ -138,7 +138,13 @@ bool BVSolverBitblastInternal::preNotifyFact( } } - return true; + return false; // Return false to enable equality engine reasoning in Theory. +} + +TrustNode BVSolverBitblastInternal::explain(TNode n) +{ + Debug("bv-bitblast-internal") << "explain called on " << n << std::endl; + return d_im.explainLit(n); } bool BVSolverBitblastInternal::collectModelValues(TheoryModel* m, diff --git a/src/theory/bv/bv_solver_bitblast_internal.h b/src/theory/bv/bv_solver_bitblast_internal.h index 1ec3ec1fe..2fc7173d1 100644 --- a/src/theory/bv/bv_solver_bitblast_internal.h +++ b/src/theory/bv/bv_solver_bitblast_internal.h @@ -52,6 +52,8 @@ class BVSolverBitblastInternal : public BVSolver bool isPrereg, bool isInternal) override; + TrustNode explain(TNode n) override; + std::string identify() const override { return "BVSolverBitblastInternal"; }; bool collectModelValues(TheoryModel* m, diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 07920ecc6..96bc85336 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -23,7 +23,6 @@ #include "base/check.h" #include "expr/node_algorithm.h" #include "options/arith_options.h" -#include "options/bv_options.h" #include "options/smt_options.h" #include "options/theory_options.h" #include "smt/smt_statistics_registry.h" @@ -620,11 +619,6 @@ bool Theory::usesCentralEqualityEngine(TheoryId id) // conditional on whether we are using the equality solver return options::arithEqSolver(); } - if (id == THEORY_BV) - { - // the internal bitblast BV solver doesnt use an equality engine - return options::bvSolver() != options::BVSolver::BITBLAST_INTERNAL; - } return id == THEORY_UF || id == THEORY_DATATYPES || id == THEORY_BAGS || id == THEORY_FP || id == THEORY_SETS || id == THEORY_STRINGS || id == THEORY_SEP || id == THEORY_ARRAYS; diff --git a/test/regress/regress2/bug349.smtv1.smt2 b/test/regress/regress2/bug349.smtv1.smt2 index f1807fd8f..ffbd7f331 100644 --- a/test/regress/regress2/bug349.smtv1.smt2 +++ b/test/regress/regress2/bug349.smtv1.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --bv-solver=bitblast (set-option :incremental false) (set-info :status unsat) (set-logic QF_AUFBV) |