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).

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 49385294c4df2d4e125c59d21229e2ab0abd8679..57b2803d980e3cb0b2b78701f8e26f05eb89622a 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -82,7 +82,7 @@ void NonlinearExtension::preRegisterTerm(TNode n)
 {
   // register terms with extended theory, to find extended terms that can be
   // eliminated by context-depedendent simplification.
-  d_extTheory.registerTermRec(n);
+  d_extTheory.registerTerm(n);
 }
 
 void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out)

diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp
index 7a6d5c9abcc68bef679a8216f4991cfb8dfc4905..7b4936a536c047f70ae390ac1342018d48ad83c7 100644 (file)
--- a/src/theory/ext_theory.cpp
+++ b/src/theory/ext_theory.cpp
@@ -438,28 +438,6 @@ void ExtTheory::registerTerm(Node n)
   }
 }
 
-void ExtTheory::registerTermRec(Node n)
-{
-  std::unordered_set<TNode, TNodeHashFunction> visited;
-  std::vector<TNode> visit;
-  TNode cur;
-  visit.push_back(n);
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    if (visited.find(cur) == visited.end())
-    {
-      visited.insert(cur);
-      registerTerm(cur);
-      for (const Node& cc : cur)
-      {
-        visit.push_back(cc);
-      }
-    }
-  } while (!visit.empty());
-}
-
 // mark reduced
 void ExtTheory::markReduced(Node n, bool satDep)
 {

diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h
index 1577c8b6fa9cf6cbb391641db4ad5148e7af34a3..efe235432d956d3c43b0bc92a29a5c913e3d5da3 100644 (file)
--- a/src/theory/ext_theory.h
+++ b/src/theory/ext_theory.h
@@ -144,8 +144,6 @@ class ExtTheory
    * that is, if addFunctionKind( n.getKind() ) was called.
    */
   void registerTerm(Node n);
-  /** register all subterms of n with this class */
-  void registerTermRec(Node n);
   /** set n as reduced/inactive
    *
    * If satDep = false, then n remains inactive in the duration of this

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 352da5ac8e58f953a4c4505c587de1e35ad810c3..8db53c53ed5a2f97dd3e18efa39d62b4f4722741 100644 (file)
--- 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 df0a7ccb5d980e908414e187e110f03e811ff7d4..7d7ecdbe4528a15579d5852cf4e05f968e5cc81c 100644 (file)
--- 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 eec59685af85f288e3ca65aa6dc0e770a8f612c8..f25f9e29c943bf83f65d57d4d3bc82d6e6834651 100644 (file)
--- 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 ebded2aec9bbbf30cbb7fb9e8f5f89cf09c672ef..c150fb3df0930fbccdc939f5e1961ab6ee9c562b 100644 (file)
--- 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 */