Fix model issues with --bitblast=eager. (#6753)

For model construction we only compute model values for relevant terms. The set of relevant terms is computed in https://github.com/cvc5/cvc5/blob/master/src/theory/model_manager_distributed.cpp#L58, which skips equalities by default because equalities are usually handled by the equality engine.
When --bitblast=eager is enabled all assertions are wrapped into BITVECTOR_EAGER_ATOM nodes and passed to the BV solver, which results in equalities below BITVECTOR_EAGER_ATOM nodes not being handled by the equality engine but by the BV solver directly. These equalities, however, are skipped when computing the relevant terms and therefore the BV solver is not asked to compute model values for variables below these equalities.

If --bitblast=eager is enabled the BV solver now additionally adds the variables encountered during bit-blasting to the relevant terms via computeRelevantTerms.

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>

diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp
index a38dfdfe51e7b9967b685fc46b5a3624b93265cc..357a54b1a8b724a1c394cea0d2a5148dca1f2e89 100644 (file)
--- a/src/theory/bv/bitblast/simple_bitblaster.cpp
+++ b/src/theory/bv/bitblast/simple_bitblaster.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/theory_model.h"
 #include "theory/theory_state.h"
+#include "options/bv_options.h"
 
 namespace cvc5 {
 namespace theory {
@@ -129,6 +130,15 @@ Node BBSimple::getModelFromSatSolver(TNode a, bool fullModel)
   return utils::mkConst(bits.size(), value);
 }
 
+void BBSimple::computeRelevantTerms(std::set<Node>& termSet)
+{
+  Assert(options::bitblastMode() == options::BitblastMode::EAGER);
+  for (const auto& var : d_variables)
+  {
+    termSet.insert(var);
+  }
+}
+
 bool BBSimple::collectModelValues(TheoryModel* m,
                                   const std::set<Node>& relevantTerms)
 {

diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h
index ebbb2891f94125fd32d3c0111288d92b6850f068..ec08991455ee9947a757a7d8085683f08f9bf74a 100644 (file)
--- a/src/theory/bv/bitblast/simple_bitblaster.h
+++ b/src/theory/bv/bitblast/simple_bitblaster.h
@@ -53,6 +53,8 @@ class BBSimple : public TBitblaster<Node>
   /** Create 'bits' for variable 'var'. */
   void makeVariable(TNode var, Bits& bits) override;
 
+  /** Add d_variables to termSet. */
+  void computeRelevantTerms(std::set<Node>& termSet);
   /** Collect model values for all relevant terms given in 'relevantTerms'. */
   bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
 

diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
index 8ff4318c084295207c4c23adbc2f4ac4846fe05b..6ccc6c7c17890801e967c6630a37220d49d52866 100644 (file)
--- a/src/theory/bv/bv_solver.h
+++ b/src/theory/bv/bv_solver.h
@@ -32,7 +32,7 @@ class BVSolver
   BVSolver(TheoryState& state, TheoryInferenceManager& inferMgr)
       : d_state(state), d_im(inferMgr){};
 
-  virtual ~BVSolver(){};
+  virtual ~BVSolver() {}
 
   /**
    * Returns true if we need an equality engine. If so, we initialize the
@@ -71,7 +71,7 @@ class BVSolver
 
   virtual bool needsCheckLastEffort() { return false; }
 
-  virtual void propagate(Theory::Effort e){};
+  virtual void propagate(Theory::Effort e) {}
 
   virtual TrustNode explain(TNode n)
   {
@@ -80,17 +80,20 @@ class BVSolver
     return TrustNode::null();
   }
 
+  /** Additionally collect terms relevant for collecting model values. */
+  virtual void computeRelevantTerms(std::set<Node>& termSet) {}
+
   /** Collect model values in m based on the relevant terms given by termSet */
   virtual bool collectModelValues(TheoryModel* m,
                                   const std::set<Node>& termSet) = 0;
 
   virtual std::string identify() const = 0;
 
-  virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); };
+  virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); }
 
-  virtual void ppStaticLearn(TNode in, NodeBuilder& learned){};
+  virtual void ppStaticLearn(TNode in, NodeBuilder& learned) {}
 
-  virtual void presolve(){};
+  virtual void presolve() {}
 
   virtual void notifySharedTerm(TNode t) {}
 

diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 414e57e19c177a9d18c509cc6802dd4aee8f5d4a..3ae4a7f0ae87ece14f773461b7760644d338bd37 100644 (file)
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -238,6 +238,21 @@ TrustNode BVSolverBitblast::explain(TNode n)
   return d_im.explainLit(n);
 }
 
+void BVSolverBitblast::computeRelevantTerms(std::set<Node>& termSet)
+{
+  /* BITVECTOR_EAGER_ATOM wraps input assertions that may also contain
+   * equalities. As a result, these equalities are not handled by the equality
+   * engine and terms below these equalities do not appear in `termSet`.
+   * We need to make sure that we compute model values for all relevant terms
+   * in BitblastMode::EAGER and therefore add all variables from the
+   * bit-blaster to `termSet`.
+   */
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
+    d_bitblaster->computeRelevantTerms(termSet);
+  }
+}
+
 bool BVSolverBitblast::collectModelValues(TheoryModel* m,
                                           const std::set<Node>& termSet)
 {

diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index 31d9443c897ecaf0dd714f08355c5eedbac770d3..c5134c6fceef3b9bb5f3ea21cfb67b965b8ed2d1 100644 (file)
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -64,6 +64,8 @@ class BVSolverBitblast : public BVSolver
 
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
 
+  void computeRelevantTerms(std::set<Node>& termSet) override;
+
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;
 

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 22b05b02659b4dd443a845ae3f6f61318baaa96d..3d7f11f6d2cbcbe5a91782c7f595e3eef55a1eba 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -175,6 +175,11 @@ bool TheoryBV::needsCheckLastEffort()
   return d_internal->needsCheckLastEffort();
 }
 
+void TheoryBV::computeRelevantTerms(std::set<Node>& termSet)
+{
+  return d_internal->computeRelevantTerms(termSet);
+}
+
 bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 {
   return d_internal->collectModelValues(m, termSet);

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 4b3a1f3b2d576d3437aacfa9f629db119a28be3e..e884f621ca13373c4c3b7601387a908a5442e085 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -83,6 +83,8 @@ class TheoryBV : public Theory
 
   TrustNode explain(TNode n) override;
 
+  void computeRelevantTerms(std::set<Node>& termSet) override;
+
   /** Collect model values in m based on the relevant terms given by termSet */
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& termSet) override;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 9ad4f7e8a81651e8eaf8d6eb0c134ad449730577..444e4c7f6e5725b61911973c970579f30186a9b1 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -670,6 +670,7 @@ set(regress_0_tests
   regress0/issue5743.smt2
   regress0/issue5947.smt2
   regress0/issue6605-2-abd-triv.smt2
+  regress0/issue6741.smt2
   regress0/ite_arith.smt2
   regress0/ite_real_int_type.smtv1.smt2
   regress0/ite_real_valid.smtv1.smt2

diff --git a/test/regress/regress0/issue6741.smt2 b/test/regress/regress0/issue6741.smt2
new file mode 100644 (file)
index 0000000..0fbf4ed
--- /dev/null
+++ b/test/regress/regress0/issue6741.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --bv-solver=bitblast --bitblast=eager --check-models
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-fun x () (_ BitVec 1))
+(declare-fun y () (_ BitVec 1))
+(assert (= y (ite (= x (_ bv1 1)) (_ bv1 1) (_ bv0 1))))
+(assert (= y (_ bv1 1)))
+(check-sat)