diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-02 20:18:48 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-02 18:18:48 -0700 |
commit | 8b4444dad1647c89b313deedd22129252078fe1b (patch) | |
tree | 23dbe0b73868eb5d2bc45d640eba755fa9b50fd5 /src/theory/strings/extf_solver.cpp | |
parent | 5f3d21a7402538af837eaf943b5252b1db90080b (diff) |
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.
Diffstat (limited to 'src/theory/strings/extf_solver.cpp')
-rw-r--r-- | src/theory/strings/extf_solver.cpp | 17 |
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 |