diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-16 12:10:58 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-16 12:10:58 -0500 |
| commit | f7559c879d1ebc7d4d9b9f72b0858bdf42c9ed8c (patch) | |
| tree | f4ceec82dfec21737b4cc1c555706bd8426fc9e9 /src/theory/strings/extf_solver.cpp | |
| parent | 051106d0033c8108008acba65ad02a77b5ddd19c (diff) | |
Make ExtTheory a utility and not a member of Theory (#4753)
Previously, we assumed that ExtTheory, the module for doing context-dependent simplification, was one-to-one with Theory. This design is not necessary. This makes this class a utility, which can be used as needed. This makes e.g. the initialization of TheoryStrings much easier, since the ExtTheory object can be created first.
Diffstat (limited to 'src/theory/strings/extf_solver.cpp')
| -rw-r--r-- | src/theory/strings/extf_solver.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 9b1b0e6dd..eff0b3d74 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -74,6 +74,8 @@ ExtfSolver::ExtfSolver(context::Context* c, ExtfSolver::~ExtfSolver() {} +void ExtfSolver::addSharedTerm(TNode n) { d_extt.registerTermRec(n); } + bool ExtfSolver::doReduction(int effort, Node n) { Assert(d_extfInfoTmp.find(n) != d_extfInfoTmp.end()); |