Fix term registration and non-theory-preprocessed terms in substitutions (#6080)

This fixes two issues for preprocessing:
(1) The term preregistration visitor was calling preRegister on terms multiple times in a SAT context, which the linear arithmetic solver is sensitive to.
(2) It was possible for non-preprocessed terms to appear in assertions if they were on the RHS of substitutions learned by non-clausal simplification, and substituted into assertions post-theory-preprocessing.

To fix (1), the SharedTermsVisitor is update to track which theories has preregistered each term, as is done in the PreRegisterVisitor. To fix (2), we no longer apply-subst after theory preprocessing.

These two fixes are required to fix #6071.

Note: we should performance test this on SMT-LIB.

1 files changed, 27 insertions, 10 deletions

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 3a3003ba9..253f21d98 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -113,8 +113,9 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
   TheoryIdSet visitedTheories = d_visited[current];
 
   // call the preregistration on current, parent or type theories and update
-  // visitedTheories.
-  preRegister(d_engine, visitedTheories, current, parent);
+  // visitedTheories. The set of preregistering theories coincides with
+  // visitedTheories here.
+  preRegister(d_engine, visitedTheories, current, parent, visitedTheories);
 
   Debug("register::internal")
       << "PreRegisterVisitor::visit(" << current << "," << parent
@@ -129,17 +130,20 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
 void PreRegisterVisitor::preRegister(TheoryEngine* te,
                                      TheoryIdSet& visitedTheories,
                                      TNode current,
-                                     TNode parent)
+                                     TNode parent,
+                                     TheoryIdSet preregTheories)
 {
   // Preregister with the current theory, if necessary
   TheoryId currentTheoryId = Theory::theoryOf(current);
-  preRegisterWithTheory(te, visitedTheories, currentTheoryId, current, parent);
+  preRegisterWithTheory(
+      te, visitedTheories, currentTheoryId, current, parent, preregTheories);
 
   if (current != parent)
   {
     // preregister with parent theory, if necessary
     TheoryId parentTheoryId = Theory::theoryOf(parent);
-    preRegisterWithTheory(te, visitedTheories, parentTheoryId, current, parent);
+    preRegisterWithTheory(
+        te, visitedTheories, parentTheoryId, current, parent, preregTheories);
 
     // Note that if enclosed by different theories it's shared, for example,
     // in read(a, f(a)), f(a) should be shared with integers.
@@ -148,7 +152,8 @@ void PreRegisterVisitor::preRegister(TheoryEngine* te,
     {
       // preregister with the type's theory, if necessary
       TheoryId typeTheoryId = Theory::theoryOf(type);
-      preRegisterWithTheory(te, visitedTheories, typeTheoryId, current, parent);
+      preRegisterWithTheory(
+          te, visitedTheories, typeTheoryId, current, parent, preregTheories);
     }
   }
 }
@@ -156,11 +161,18 @@ void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te,
                                                TheoryIdSet& visitedTheories,
                                                TheoryId id,
                                                TNode current,
-                                               TNode parent)
+                                               TNode parent,
+                                               TheoryIdSet preregTheories)
 {
   if (TheoryIdSetUtil::setContains(id, visitedTheories))
   {
-    // already registered
+    // already visited
+    return;
+  }
+  visitedTheories = TheoryIdSetUtil::setInsert(id, visitedTheories);
+  if (TheoryIdSetUtil::setContains(id, preregTheories))
+  {
+    // already pregregistered
     return;
   }
   if (Configuration::isAssertionBuild())
@@ -192,7 +204,6 @@ void PreRegisterVisitor::preRegisterWithTheory(TheoryEngine* te,
     }
   }
   // call the theory's preRegisterTerm method
-  visitedTheories = TheoryIdSetUtil::setInsert(id, visitedTheories);
   Theory* th = te->theoryOf(id);
   th->preRegisterTerm(current);
 }
@@ -242,13 +253,19 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) {
     Debug("register::internal") << toString() << std::endl;
   }
   TheoryIdSet visitedTheories = d_visited[current];
+  TheoryIdSet preregTheories = d_preregistered[current];
 
   // preregister the term with the current, parent or type theories, as needed
-  PreRegisterVisitor::preRegister(d_engine, visitedTheories, current, parent);
+  PreRegisterVisitor::preRegister(
+      d_engine, visitedTheories, current, parent, preregTheories);
 
   // Record the new theories that we visited
   d_visited[current] = visitedTheories;
 
+  // add visited theories to those who have preregistered
+  d_preregistered[current] =
+      TheoryIdSetUtil::setUnion(preregTheories, visitedTheories);
+
   // If there is more than two theories and a new one has been added notify the shared terms database
   TheoryId currentTheoryId = Theory::theoryOf(current);
   if (TheoryIdSetUtil::setDifference(