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.

diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 6db70156575f63ef92e170aec34523521ba0e650..8cff66d721303d72b10fef290032a0df16849841 100644 (file)
--- 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 4c610ccfc79450f38f41539b9805d423d5fdae91..e45972e9454599305c8ee6545d321cb43cfefefc 100644 (file)
--- 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 66dcd81a095be42aa9f32297b4557067feaf8216..2f1b3ce69799f9c1ce9776c1cc9ec29b472d3816 100644 (file)
--- 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 4f174e69ef08702d6ce8e3ee97dec28f09185ce5..2a270fe208152f2326e4750d0c9dac4e6b4a8955 100644 (file)
--- 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

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b08777a51a7b07f77d3a4572ef1ee0e849cad205..1a43b0335f19d8f1af1f3888560be33dc14be0c3 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -746,6 +746,7 @@ set(regress_0_tests
   regress0/precedence/xor-or.cvc
   regress0/preprocess/circuit-prop.smt2
   regress0/preprocess/issue5729-rewritten-assertions.smt2
+  regress0/preprocess/issue5943-non-clausal-simp.smt2
   regress0/preprocess/preprocess_00.cvc
   regress0/preprocess/preprocess_01.cvc
   regress0/preprocess/preprocess_02.cvc

diff --git a/test/regress/regress0/preprocess/issue5943-non-clausal-simp.smt2 b/test/regress/regress0/preprocess/issue5943-non-clausal-simp.smt2
new file mode 100644 (file)
index 0000000..f3abedc
--- /dev/null
+++ b/test/regress/regress0/preprocess/issue5943-non-clausal-simp.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: unsat
+(set-logic QF_SLIA)
+(declare-fun s () String)
+(assert (and (and (= (str.len (str.at s 3)) 4) (not (not (= (ite (not (= (ite (not (= (str.at (str.at s 3) 
+(ite (not (not (= (ite (<= (str.len (str.at s 1)) 3) 1 0) 0))) 1 0)) (str.at s 5))) 1 0) 0)) 1 0) 0)))) (not (not (= (str.len s) 3)))))
+(check-sat)