From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Thu, 25 Feb 2021 23:46:17 +0000 (+0100)
Subject: Move (optional) rewrite from TrustSubstitutionMap to SubstitutionMap. (#5992)
X-Git-Tag: cvc5-1.0.0~2208
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1c7ed68156cb3cf19ef036cbbfff18bcc4e45c36;p=cvc5.git

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 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
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b08777a51..1a43b0335 100644
--- 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
index 000000000..f3abedcdf
--- /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)