bv: Enable equality engine for bitblast-internal. (#6961)

diff --git a/src/theory/bv/bv_solver_bitblast_internal.cpp b/src/theory/bv/bv_solver_bitblast_internal.cpp
index ef4f3559be18c53501879478cf4c73a788a35583..1b606a0e9343791eb6fa79113ad6c28dab2783c6 100644 (file)
--- 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 1ec3ec1fec8eaef12b23f7ba47bd3402b1670beb..2fc7173d13aa0affa4535275213a229f48a11930 100644 (file)
--- 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 07920ecc6a329cb24defd50ec8d2274afed55076..96bc85336ad29b990a9b7c5da026130fda8deefa 100644 (file)
--- 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 f1807fd8f0e6c103cbbb5c1dcaa3e67b2b6ed492..ffbd7f331568cf4840c0e76bf448f0a7984b2630 100644 (file)
--- 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)