From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 7 Jan 2022 19:30:36 +0000 (-0600)
Subject: Fix eager string preprocessing in incremental mode (#7895)
X-Git-Tag: cvc5-1.0.0~584
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=35f4cd5a28d0a499f7ffdfcb88d6df0032b1c14a;p=cvc5.git

Fix eager string preprocessing in incremental mode (#7895)

Fixes #5780.

Issue was caused by reintroducing skolems during preprocessing that were already solved for.
---

diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 89e40a0aa..2924b2dc3 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -147,8 +147,12 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   {
     // Simplify the literal we learned wrt previous substitutions
     Node learnedLiteral = learned_literals[i].getNode();
+    Trace("non-clausal-simplify")
+        << "Process learnedLiteral : " << learnedLiteral;
     Assert(rewrite(learnedLiteral) == learnedLiteral);
-    Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral);
+    Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral)
+        << learnedLiteral << " after subs is "
+        << top_level_substs.apply(learnedLiteral);
     // process the learned literal with substitutions and const propagations
     learnedLiteral = processLearnedLit(
         learnedLiteral, newSubstitutions.get(), constantPropagations.get());
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 329f42609..90fd5847d 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -229,6 +229,9 @@ bool ProcessAssertions::apply(Assertions& as)
   if (!options().strings.stringLazyPreproc)
   {
     applyPass("strings-eager-pp", as);
+    // needed since strings eager preprocessing may reintroduce skolems that
+    // were already solved for in incremental mode
+    applyPass("apply-substs", as);
   }
   if (options().smt.sortInference || options().uf.ufssFairnessMonotone)
   {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4d9d88c6b..4f79758c4 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2329,6 +2329,7 @@ set(regress_1_tests
   regress1/strings/issue5610-2-infer-proxy.smt2
   regress1/strings/issue5611-deq-norm-emp.smt2
   regress1/strings/issue5692-infer-proxy.smt2
+  regress1/strings/issue5780-repeat-skolem.smt2
   regress1/strings/issue5940-skc-len-conc.smt2
   regress1/strings/issue5940-2-skc-len-conc.smt2
   regress1/strings/issue6057-replace-re.smt2
diff --git a/test/regress/regress1/strings/issue5780-repeat-skolem.smt2 b/test/regress/regress1/strings/issue5780-repeat-skolem.smt2
new file mode 100644
index 000000000..08308d424
--- /dev/null
+++ b/test/regress/regress1/strings/issue5780-repeat-skolem.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+(set-logic ALL)
+(set-option :strings-lazy-pp false)
+(set-info :status sat)
+(declare-fun s () String)
+(declare-fun t () String)
+(declare-fun r () String)
+(declare-fun u () String)
+(assert (= u (str.replace_re (str.++ t s) re.none r)))
+(push)
+(assert (= t (str.replace_re (str.++ t s) re.none r)))
+(push)
+(check-sat)