Move (optional) rewrite from TrustSubstitutionMap to SubstitutionMap. (#5992)

This PR adds optional rewriting to the SubstitutionMap class. Before, only the new TrustSubstitutionMap added optional rewriting, leading to unexpected inconsistencies between the two. In particular, cases exist where the substitution and the rewriting cancel each other (see #5943).
This PR moves the optional rewriting from TrustSubstitutionMap into SubstitutionMap. While the former enables it by default, it is disabled by default for the latter and thus does not change current behavior.
We now use this new option in an assertion in the non-clausal simplification.
Fixes #5943.

4 files changed, 11 insertions, 12 deletions

diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 6db701565..8cff66d72 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -232,7 +232,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
             c = learnedLiteral[1];
           }
           Assert(!t.isConst());
-          Assert(cps.apply(t) == t);
+          Assert(cps.apply(t, true) == t);
           Assert(top_level_substs.apply(t) == t);
           Assert(nss.apply(t) == t);
           // also add to learned literal
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 4c610ccfc..e45972e94 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -184,7 +184,7 @@ void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateC
   }
 }
 
-Node SubstitutionMap::apply(TNode t) {
+Node SubstitutionMap::apply(TNode t, bool doRewrite) {
 
   Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << endl;
 
@@ -199,6 +199,11 @@ Node SubstitutionMap::apply(TNode t) {
   Node result = internalSubstitute(t, d_substitutionCache);
   Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << endl;
 
+  if (doRewrite)
+  {
+    result = Rewriter::rewrite(result);
+  }
+
   return result;
 }
 
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 66dcd81a0..2f1b3ce69 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -133,13 +133,13 @@ public:
   /**
    * Apply the substitutions to the node.
    */
-  Node apply(TNode t);
+  Node apply(TNode t, bool doRewrite = false);
 
   /**
    * Apply the substitutions to the node.
    */
-  Node apply(TNode t) const {
-    return const_cast<SubstitutionMap*>(this)->apply(t);
+  Node apply(TNode t, bool doRewrite = false) const {
+    return const_cast<SubstitutionMap*>(this)->apply(t, doRewrite);
   }
 
   iterator begin() {
diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index 4f174e69e..2a270fe20 100644
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -138,14 +138,8 @@ TrustNode TrustSubstitutionMap::apply(Node n, bool doRewrite)
 {
   Trace("trust-subs") << "TrustSubstitutionMap::addSubstitution: apply " << n
                       << std::endl;
-  Node ns = d_subs.apply(n);
+  Node ns = d_subs.apply(n, doRewrite);
   Trace("trust-subs") << "...subs " << ns << std::endl;
-  // rewrite if indicated
-  if (doRewrite)
-  {
-    ns = Rewriter::rewrite(ns);
-    Trace("trust-subs") << "...rewrite " << ns << std::endl;
-  }
   if (n == ns)
   {
     // no change