(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).

18 files changed, 74 insertions, 85 deletions

diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index 3e32b4cc3..1813784d7 100644
--- 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 e53f1697d..66cd6cc23 100644
--- 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 f8e30247f..10fc8c4b7 100644
--- 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 c1d9e333e..95e1eb600 100644
--- 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 fef95ceef..f8d6467aa 100644
--- 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 ad673b402..c0f34c132 100644
--- 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 81f40340e..e7033275f 100644
--- 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 1244ae828..37474bfec 100644
--- 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 49043b445..e900566f9 100644
--- 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 a5d7b2db3..92cfac71e 100644
--- 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 93ac87abe..47ab5cec5 100644
--- 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 0832b6772..0f43b4f30 100644
--- 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 5bb6a45e4..162c2d31d 100644
--- 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 876daeabe..7bc5337c4 100644
--- 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 ffc354d8d..80a603ef0 100644
--- 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 05c9c3d60..ba0275fa6 100644
--- 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 6f25d0843..fb7395a28 100644
--- 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 d33ea1337..cff16bec0 100644
--- 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"); }