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/theory_strings.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/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 0f59e73dc..cbe6000bf 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -86,11 +86,6 @@ class TheoryStrings : public Theory { std::string identify() const override; /** Explain */ TrustNode explain(TNode literal) override; - /** Get current substitution */ - bool getCurrentSubstitution(int effort, - std::vector<Node>& vars, - std::vector<Node>& subs, - std::map<Node, std::vector<Node> >& exp) override; /** presolve */ void presolve() override; /** shutdown */ @@ -262,6 +257,8 @@ class TheoryStrings : public Theory { SolverState d_state; /** The term registry for this theory */ TermRegistry d_termReg; + /** The extended theory callback */ + StringsExtfCallback d_extTheoryCb; /** Extended theory, responsible for context-dependent simplification. */ ExtTheory d_extTheory; /** The (custom) output channel of the theory of strings */ |