From 13fe59109928f6ca173691a94b705ad3225aeb85 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 2 Aug 2021 14:33:34 -0700 Subject: [PATCH] bv: Enable equality engine for bitblast-internal. (#6961) --- src/theory/bv/bv_solver_bitblast_internal.cpp | 8 +++++++- src/theory/bv/bv_solver_bitblast_internal.h | 2 ++ src/theory/theory.cpp | 6 ------ 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) -- 2.30.2