(new theory) Update TheoryBV to new standard for collectModelValues (#5025)

This makes collectModelValues the main model interface in BV instead of collectModelInfo. BV is no longer responsible for asserting its equality engine or computing relevant/asserted terms.

This involved updating the interface on many subsolvers of BvSolverLazy. This includes moving the responsibility of addSharedTerm (regarding trigger terms) from the subsolvers to TheoryBV, this eventually will be automatically handled in Theory once all theories are migrated to the new standard.

This ensures that TheoryBV is updated to the new standard (check was already migrated on c9e23f6).

diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 3e32b4cc352276cd5eaae5bbb203885f05f7d7d3..1813784d74fa912aed1cde0ea9ea912d8e87671f 100644 (file)
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -530,12 +530,9 @@ Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
   return utils::mkConst(bits.size(), value);
 }
 
-bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
+bool TLazyBitblaster::collectModelValues(TheoryModel* m,
+                                         const std::set<Node>& termSet)
 {
-  std::set<Node> termSet;
-  const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
-  d_bv->computeAssertedTerms(termSet, irrKinds, true);
-
   for (std::set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) {
     TNode var = *it;
     // not actually a leaf of the bit-vector theory
@@ -549,9 +546,9 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
     Node const_value = getModelFromSatSolver(var, true);
     Assert(const_value.isNull() || const_value.isConst());
     if(const_value != Node()) {
-      Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
-                               << var << " "
-                               << const_value << "))\n";
+      Debug("bitvector-model")
+          << "TLazyBitblaster::collectModelValues (assert (= " << var << " "
+          << const_value << "))\n";
       if (!m->assertEquality(var, const_value, true))
       {
         return false;

diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index e53f1697dd3574f4c94af3a8a0c0b40fdcf3ecd6..66cd6cc23e881a6cb038805d6bfa6b23e42fd9be 100644 (file)
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -72,10 +72,10 @@ class TLazyBitblaster : public TBitblaster<Node>
    * Adds a constant value for each bit-blasted variable in the model.
    *
    * @param m the model
-   * @param fullModel whether to create a "full model," i.e., add
-   * constants to equivalence classes that don't already have them
+   * @param termSet the set of relevant terms
    */
-  bool collectModelInfo(TheoryModel* m, bool fullModel);
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet);
 
   typedef TNodeSet::const_iterator vars_iterator;
   vars_iterator beginVars() { return d_variables.begin(); }

diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index f8e30247f6f4a2a2e8162216547b407e918a6cbe..10fc8c4b776434118a61ef14d885ee70ef7c2482 100644 (file)
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -140,9 +140,10 @@ void BVQuickCheck::popToZero() {
   }
 }
 
-bool BVQuickCheck::collectModelInfo(theory::TheoryModel* model, bool fullModel)
+bool BVQuickCheck::collectModelValues(theory::TheoryModel* model,
+                                      const std::set<Node>& termSet)
 {
-  return d_bitblaster->collectModelInfo(model, fullModel);
+  return d_bitblaster->collectModelValues(model, termSet);
 }
 
 BVQuickCheck::~BVQuickCheck() {

diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index c1d9e333e539d1078da3413bb17f880105c3de95..95e1eb600a19b55e496f55ca84f10f95350b4a1d 100644 (file)
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -98,7 +98,8 @@ class BVQuickCheck
    * @return
    */
   uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
-  bool collectModelInfo(theory::TheoryModel* model, bool fullModel);
+  bool collectModelValues(theory::TheoryModel* model,
+                          const std::set<Node>& termSet);
 
   typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator
       vars_iterator;

diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
index fef95ceef1d98399f9c32781515f7d5558f45b64..f8d6467aab1ede755dd362c74f36dc8dbea6c0bb 100644 (file)
--- a/src/theory/bv/bv_solver.h
+++ b/src/theory/bv/bv_solver.h
@@ -77,13 +77,11 @@ class BVSolver
     Unimplemented() << "BVSolver propagated a node but doesn't implement the "
                        "BVSolver::explain() interface!";
     return TrustNode::null();
-  };
+  }
 
-  /**
-   * This is temporary only and will be deprecated soon in favor of
-   * Theory::collectModelValues.
-   */
-  virtual bool collectModelInfo(TheoryModel* m) = 0;
+  /** 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;
 
@@ -96,7 +94,7 @@ class BVSolver
 
   virtual void presolve(){};
 
-  virtual void notifySharedTerm(TNode t) = 0;
+  virtual void notifySharedTerm(TNode t) {}
 
   virtual EqualityStatus getEqualityStatus(TNode a, TNode b)
   {

diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index ad673b402f859f9b016e1e064a32b1fd6e9805b1..c0f34c132fac2810668c21aae43fa6905b75245a 100644 (file)
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -368,7 +368,8 @@ bool BVSolverLazy::needsCheckLastEffort()
   return false;
 }
 
-bool BVSolverLazy::collectModelInfo(TheoryModel* m)
+bool BVSolverLazy::collectModelValues(TheoryModel* m,
+                                      const std::set<Node>& termSet)
 {
   Assert(!inConflict());
   if (options::bitblastMode() == options::BitblastMode::EAGER)
@@ -382,7 +383,7 @@ bool BVSolverLazy::collectModelInfo(TheoryModel* m)
   {
     if (d_subtheories[i]->isComplete())
     {
-      return d_subtheories[i]->collectModelInfo(m, true);
+      return d_subtheories[i]->collectModelValues(m, termSet);
     }
   }
   return true;
@@ -719,13 +720,6 @@ void BVSolverLazy::notifySharedTerm(TNode t)
   Debug("bitvector::sharing")
       << indent() << "BVSolverLazy::notifySharedTerm(" << t << ")" << std::endl;
   d_sharedTermsSet.insert(t);
-  if (options::bitvectorEqualitySolver())
-  {
-    for (unsigned i = 0; i < d_subtheories.size(); ++i)
-    {
-      d_subtheories[i]->addSharedTerm(t);
-    }
-  }
 }
 
 EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b)

diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index 81f40340ee3d61c4d7c6239a19e9f308f3ee412a..e7033275fd84c4c429dbc68d683daa4d3cb84ad5 100644 (file)
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -87,7 +87,8 @@ class BVSolverLazy : public BVSolver
 
   TrustNode explain(TNode n) override;
 
-  bool collectModelInfo(TheoryModel* m) override;
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
 
   std::string identify() const override { return std::string("BVSolverLazy"); }
 
@@ -208,13 +209,6 @@ class BVSolverLazy : public BVSolver
 
   void checkForLemma(TNode node);
 
-  void computeAssertedTerms(std::set<Node>& termSet,
-                            const std::set<Kind>& irrKinds,
-                            bool includeShared) const
-  {
-    return d_bv.computeAssertedTerms(termSet, irrKinds, includeShared);
-  }
-
   size_t numAssertions() { return d_bv.numAssertions(); }
 
   theory::Assertion get() { return d_bv.get(); }

diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 1244ae8285e7ab7fd291d9503dd81f9391fce032..37474bfec62c4be931911a02e20ebe4df9f40c88 100644 (file)
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -74,11 +74,11 @@ class SubtheorySolver {
   virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
   virtual void preRegister(TNode node) {}
   virtual void propagate(Theory::Effort e) {}
-  virtual bool collectModelInfo(TheoryModel* m, bool fullModel) = 0;
+  virtual bool collectModelValues(TheoryModel* m,
+                                  const std::set<Node>& termSet) = 0;
   virtual Node getModelValue(TNode var) = 0;
   virtual bool isComplete() = 0;
   virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0;
-  virtual void addSharedTerm(TNode node) {}
   bool done() { return d_assertionQueue.size() == d_assertionIndex; }
   TNode get() {
     Assert(!done());

diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 49043b4459c40fbba383e42b2873daf2f36b501f..e900566f9716878969834d59e2deeff0fe7a537c 100644 (file)
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -472,7 +472,8 @@ bool AlgebraicSolver::quickCheck(std::vector<Node>& facts) {
   return false;
 }
 
-void AlgebraicSolver::setConflict(TNode conflict) {
+void AlgebraicSolver::setConflict(TNode conflict)
+{
   Node final_conflict = conflict;
   if (options::bitvectorQuickXplain() &&
       conflict.getKind() == kind::AND &&
@@ -711,13 +712,11 @@ EqualityStatus AlgebraicSolver::getEqualityStatus(TNode a, TNode b) {
   return EQUALITY_UNKNOWN;
 }
 
-bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
+bool AlgebraicSolver::collectModelValues(TheoryModel* model,
+                                         const std::set<Node>& termSet)
 {
-  Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n";
+  Debug("bitvector-model") << "AlgebraicSolver::collectModelValues\n";
   AlwaysAssert(!d_quickSolver->inConflict());
-  set<Node> termSet;
-  const std::set<Kind>& irrKinds = model->getIrrelevantKinds();
-  d_bv->computeAssertedTerms(termSet, irrKinds, true);
 
   // collect relevant terms that the bv theory abstracts to variables
   // (variables and parametric terms such as select apply_uf)
@@ -748,7 +747,7 @@ bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
   for (NodeSet::const_iterator it = leaf_vars.begin(); it != leaf_vars.end(); ++it) {
     TNode var = *it;
     Node value = d_quickSolver->getVarValue(var, true);
-    Assert(!value.isNull() || !fullModel);
+    Assert(!value.isNull());
 
     // may be a shared term that did not appear in the current assertions
     // AJR: need to check whether already in map for cases where collectModelInfo is called multiple times in the same context

diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index a5d7b2db3c5a499a8eaee7025236631921efcceb..92cfac71ef16974a21117d64c36dd737ba182760 100644 (file)
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -236,7 +236,8 @@ class AlgebraicSolver : public SubtheorySolver
     Unreachable() << "AlgebraicSolver does not propagate.\n";
   }
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
-  bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
   Node getModelValue(TNode node) override;
   bool isComplete() override;
   void assertFact(TNode fact) override;

diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 93ac87abefa2e9b909fba09bdad987eb582d7c26..47ab5cec5d1dfc7c21156e922017dcb52c71954c 100644 (file)
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -248,9 +248,10 @@ EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
   return d_bitblaster->getEqualityStatus(a, b);
 }
 
-bool BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
+bool BitblastSolver::collectModelValues(TheoryModel* m,
+                                        const std::set<Node>& termSet)
 {
-  return d_bitblaster->collectModelInfo(m, fullModel);
+  return d_bitblaster->collectModelValues(m, termSet);
 }
 
 Node BitblastSolver::getModelValue(TNode node)
@@ -263,9 +264,8 @@ Node BitblastSolver::getModelValue(TNode node)
   return val;
 }
 
-
-
-void BitblastSolver::setConflict(TNode conflict) {
+void BitblastSolver::setConflict(TNode conflict)
+{
   Node final_conflict = conflict;
   if (options::bitvectorQuickXplain() &&
       conflict.getKind() == kind::AND) {

diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 0832b67729468b383aeaebc0a056bc4a2a859ffc..0f43b4f30bf9c2c45ef0ff064014d6faead99881 100644 (file)
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -72,7 +72,8 @@ class BitblastSolver : public SubtheorySolver
   bool check(Theory::Effort e) override;
   void explain(TNode literal, std::vector<TNode>& assumptions) override;
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
-  bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
   Node getModelValue(TNode node) override;
   bool isComplete() override { return true; }
   void bitblastQueue();

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 5bb6a45e41bbb0abe3e810c1616ebd713eb820e6..162c2d31d4f6c08d49fe360b977129e67ca6f167 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -347,7 +347,10 @@ void CoreSolver::buildModel()
 
 bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
   // Notify the equality engine
-  if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_CORE)) {
+  if (!d_bv->inConflict()
+      && (!d_bv->wasPropagatedBySubtheory(fact)
+          || d_bv->getPropagatingSubtheory(fact) != SUB_CORE))
+  {
     Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
     // Debug("bv-slicer-eq") << "                     reason=" << reason << endl;
     bool negated = fact.getKind() == kind::NOT;
@@ -370,7 +373,8 @@ bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
   }
 
   // checking for a conflict
-  if (d_bv->inConflict()) {
+  if (d_bv->inConflict())
+  {
     return false;
   }
   return true;
@@ -412,29 +416,23 @@ bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) {
   return utils::isEqualityTerm(term, seen); 
 }
 
-bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel)
+bool CoreSolver::collectModelValues(TheoryModel* m,
+                                    const std::set<Node>& termSet)
 {
   if (Debug.isOn("bitvector-model")) {
     context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin();
     for (; it!= d_assertionQueue.end(); ++it) {
-      Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert "
-                               << *it << ")\n";
+      Debug("bitvector-model")
+          << "CoreSolver::collectModelValues (assert " << *it << ")\n";
     }
   }
-  set<Node> termSet;
-  const std::set<Kind>& irrKinds = m->getIrrelevantKinds();
-  d_bv->computeAssertedTerms(termSet, irrKinds, true);
-  if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
-  {
-    return false;
-  }
   if (isComplete()) {
-    Debug("bitvector-model") << "CoreSolver::collectModelInfo complete.";
+    Debug("bitvector-model") << "CoreSolver::collectModelValues complete.";
     for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) {
       Node a = it->first;
       Node b = it->second;
-      Debug("bitvector-model") << "CoreSolver::collectModelInfo modelValues "
-                               << a << " => " << b <<")\n";
+      Debug("bitvector-model") << "CoreSolver::collectModelValues modelValues "
+                               << a << " => " << b << ")\n";
       if (!m->assertEquality(a, b, true))
       {
         return false;
@@ -462,11 +460,6 @@ Node CoreSolver::getModelValue(TNode var) {
   return result;
 }
 
-void CoreSolver::addSharedTerm(TNode t)
-{
-  d_equalityEngine->addTriggerTerm(t, THEORY_BV);
-}
-
 EqualityStatus CoreSolver::getEqualityStatus(TNode a, TNode b)
 {
   if (d_equalityEngine->areEqual(a, b))

diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 876daeabee7d3a2564e2935a88bb97ebabcc752a..7bc5337c48ab5c76adeed8a69b0caa9c28990200 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -110,8 +110,6 @@ class CoreSolver : public SubtheorySolver {
   ModelValue d_modelValues;
   void buildModel();
   bool assertFactToEqualityEngine(TNode fact, TNode reason);
-  bool decomposeFact(TNode fact);
-  Node getBaseDecomposition(TNode a);
   bool isCompleteForTerm(TNode term, TNodeBoolMap& seen);
   Statistics d_statistics;
 
@@ -154,9 +152,9 @@ class CoreSolver : public SubtheorySolver {
   void preRegister(TNode node) override;
   bool check(Theory::Effort e) override;
   void explain(TNode literal, std::vector<TNode>& assumptions) override;
-  bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
   Node getModelValue(TNode var) override;
-  void addSharedTerm(TNode t) override;
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   bool hasTerm(TNode node) const;
   void addTermToEqualityEngine(TNode node);

diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index ffc354d8d11692db9951b95d910cddf1ea509658..80a603ef01bcc7f2388962a7b9e7094edb95c5b9 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -189,9 +189,10 @@ void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
 }
 
 void InequalitySolver::propagate(Theory::Effort e) { Assert(false); }
-bool InequalitySolver::collectModelInfo(TheoryModel* m, bool fullModel)
+bool InequalitySolver::collectModelValues(TheoryModel* m,
+                                          const std::set<Node>& termSet)
 {
-  Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n";
+  Debug("bitvector-model") << "InequalitySolver::collectModelValues \n";
   std::vector<Node> model;
   d_inequalityGraph.getAllValuesInModel(model);
   for (unsigned i = 0; i < model.size(); ++i) {

diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 05c9c3d60c7f792ae205f1b7af19829cfb7967e9..ba0275fa680923e596c49ae3a1684d84c93fa5ae 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -79,7 +79,8 @@ class InequalitySolver : public SubtheorySolver
   void propagate(Theory::Effort e) override;
   void explain(TNode literal, std::vector<TNode>& assumptions) override;
   bool isComplete() override { return d_isComplete; }
-  bool collectModelInfo(TheoryModel* m, bool fullModel) override;
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
   Node getModelValue(TNode var) override;
   EqualityStatus getEqualityStatus(TNode a, TNode b) override;
   void assertFact(TNode fact) override;

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 6f25d0843ad075715a180e3d3c483ff5cc139759..fb7395a28f29ce485b207a6322186ec6fa534644 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -164,9 +164,9 @@ bool TheoryBV::needsCheckLastEffort()
   return d_internal->needsCheckLastEffort();
 }
 
-bool TheoryBV::collectModelInfo(TheoryModel* m)
+bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 {
-  return d_internal->collectModelInfo(m);
+  return d_internal->collectModelValues(m, termSet);
 }
 
 void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }
@@ -183,7 +183,15 @@ void TheoryBV::presolve() { d_internal->presolve(); }
 
 TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); }
 
-void TheoryBV::notifySharedTerm(TNode t) { d_internal->notifySharedTerm(t); };
+void TheoryBV::notifySharedTerm(TNode t)
+{
+  d_internal->notifySharedTerm(t);
+  // temporary, will be built into Theory::addSharedTerm
+  if (d_equalityEngine != nullptr)
+  {
+    d_equalityEngine->addTriggerTerm(t, THEORY_BV);
+  }
+}
 
 void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned)
 {

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index d33ea1337133133f3294a53a26de65b5499ac806..cff16bec04229ad434f67e9ff95cab3bae9a84d4 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -71,7 +71,9 @@ class TheoryBV : public Theory
 
   TrustNode explain(TNode n) override;
 
-  bool collectModelInfo(TheoryModel* m) override;
+  /** Collect model values in m based on the relevant terms given by termSet */
+  bool collectModelValues(TheoryModel* m,
+                          const std::set<Node>& termSet) override;
 
   std::string identify() const override { return std::string("TheoryBV"); }