Make ExtTheory independent of Theory (#5010)

This makes it so that ExtTheory uses a generic callback instead of relying on Theory.

The primary purpose of this commit is to eliminate the connection of TheoryBV and ExtTheory. This commit moves all things related to ExtTheory in BV into CoreSolver.

It also refactors the use of ExtTheory in strings and arithmetic.

1 files changed, 17 insertions, 0 deletions

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index b028da38a..6fcd5785d 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -700,6 +700,23 @@ std::vector<Node> ExtfSolver::getActive(Kind k) const
   return d_extt.getActive(k);
 }
 
+bool StringsExtfCallback::getCurrentSubstitution(
+    int effort,
+    const std::vector<Node>& vars,
+    std::vector<Node>& subs,
+    std::map<Node, std::vector<Node> >& exp)
+{
+  Trace("strings-subs") << "getCurrentSubstitution, effort = " << effort
+                        << std::endl;
+  for (const Node& v : vars)
+  {
+    Trace("strings-subs") << "  get subs for " << v << "..." << std::endl;
+    Node s = d_esolver->getCurrentSubstitutionFor(effort, v, exp[v]);
+    subs.push_back(s);
+  }
+  return true;
+}
+
 }  // namespace strings
 }  // namespace theory
 }  // namespace CVC4