diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-08 09:17:31 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-08 09:17:31 -0600 |
commit | 0745ca0490e04c4a5b10a50bd91193e41c45c415 (patch) | |
tree | dabb1ea42753ad2ed74a70d77ce64a03839a29ff /src/theory/strings | |
parent | 9e6ca7166cc2c3444429ee691f7b0c32281eddf1 (diff) |
Avoid spurious traversal of terms during preregistration (#5860)
This simplifies a few places in the code which unecessarily traverse terms during preregistration (which already traverses terms).
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/extf_solver.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/extf_solver.h | 6 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 19 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 2 |
4 files changed, 4 insertions, 25 deletions
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 352da5ac8..8db53c53e 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -73,8 +73,6 @@ ExtfSolver::ExtfSolver(SolverState& s, 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()); diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h index df0a7ccb5..7d7ecdbe4 100644 --- a/src/theory/strings/extf_solver.h +++ b/src/theory/strings/extf_solver.h @@ -92,12 +92,6 @@ class ExtfSolver ExtTheory& et, SequencesStatistics& statistics); ~ExtfSolver(); - - /** - * Called when a shared term is added to theory of strings, this registers - * n with the extended theory utility for context-depdendent simplification. - */ - void addSharedTerm(TNode n); /** check extended functions evaluation * * This applies "context-dependent simplification" for all active extended diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index eec59685a..f25f9e29c 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -164,17 +164,6 @@ bool TheoryStrings::areCareDisequal( TNode x, TNode y ) { return false; } -void TheoryStrings::notifySharedTerm(TNode t) -{ - Debug("strings") << "TheoryStrings::notifySharedTerm(): " << t << " " - << t.getType().isBoolean() << endl; - if (options::stringExp()) - { - d_esolver.addSharedTerm(t); - } - Debug("strings") << "TheoryStrings::notifySharedTerm() finished" << std::endl; -} - bool TheoryStrings::propagateLit(TNode literal) { Debug("strings-propagate") @@ -566,6 +555,10 @@ void TheoryStrings::preRegisterTerm(TNode n) Trace("strings-preregister") << "TheoryStrings::preRegisterTerm: " << n << std::endl; d_termReg.preRegisterTerm(n); + // Register the term with the extended theory. Notice we do not recurse on + // this term here since preRegisterTerm is already called recursively on all + // subterms in preregistered literals. + d_extTheory.registerTerm(n); } TrustNode TheoryStrings::expandDefinition(Node node) @@ -634,10 +627,6 @@ void TheoryStrings::notifyFact(TNode atom, return; } Trace("strings-pending-debug") << " Now collect terms" << std::endl; - // Collect extended function terms in the atom. Notice that we must register - // all extended functions occurring in assertions and shared terms. We - // make a similar call to registerTermRec in TheoryStrings::addSharedTerm. - d_extTheory.registerTermRec(atom); Trace("strings-pending-debug") << " Finished collect terms" << std::endl; } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index ebded2aec..c150fb3df 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -91,8 +91,6 @@ class TheoryStrings : public Theory { void presolve() override; /** shutdown */ void shutdown() override {} - /** add shared term */ - void notifySharedTerm(TNode n) override; /** preregister term */ void preRegisterTerm(TNode n) override; /** Expand definition */ |