From 35f4cd5a28d0a499f7ffdfcb88d6df0032b1c14a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 7 Jan 2022 13:30:36 -0600 Subject: [PATCH] Fix eager string preprocessing in incremental mode (#7895) Fixes #5780. Issue was caused by reintroducing skolems during preprocessing that were already solved for. --- src/preprocessing/passes/non_clausal_simp.cpp | 6 +++++- src/smt/process_assertions.cpp | 3 +++ test/regress/CMakeLists.txt | 1 + .../regress1/strings/issue5780-repeat-skolem.smt2 | 14 ++++++++++++++ 4 files changed, 23 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress1/strings/issue5780-repeat-skolem.smt2 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) -- 2.30.2