(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, 2 insertions, 8 deletions

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(); }