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.h | |
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.h')
-rw-r--r-- | src/theory/strings/extf_solver.h | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index 4ba38bfc6..5b11b6faf 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -214,6 +214,23 @@ class ExtfSolver NodeSet d_reduced; }; +/** An extended theory callback */ +class StringsExtfCallback : public ExtTheoryCallback +{ + public: + StringsExtfCallback() : d_esolver(nullptr) {} + /** + * Get current substitution based on the underlying extended function + * solver. + */ + bool getCurrentSubstitution(int effort, + const std::vector<Node>& vars, + std::vector<Node>& subs, + std::map<Node, std::vector<Node> >& exp) override; + /** The extended function solver */ + ExtfSolver* d_esolver; +}; + } // namespace strings } // namespace theory } // namespace CVC4 |