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

1 files changed, 5 insertions, 7 deletions

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)
   {