From 22c36b3bceb5d1a73dc0f0355c0a01703db51acc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 29 Apr 2020 13:02:02 -0500 Subject: Avoid circular dependencies for justifying reductions in strings extf eval (#4415) An incorrect answer of "sat" could be found after 8 seconds on the given benchmark (with --strings-fmf) due to a circular justification for why an extended function was reduced. In particular, we ran checkExtfInference on the same term twice and then marked it as reduced since we had already seen it. This makes the code more conservative. Notice I'm making the code doubly conservative in case there is any chance for duplication again (e.g. if ExtTheory provides duplicate terms). --- src/theory/strings/extf_solver.cpp | 14 +++++++++++--- test/regress/CMakeLists.txt | 1 + test/regress/regress3/strings/unsat-circ-reduce.smt2 | 13 +++++++++++++ 3 files changed, 25 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress3/strings/unsat-circ-reduce.smt2 diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 55985406e..dd4144313 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -235,6 +235,8 @@ void ExtfSolver::checkExtfEval(int effort) NodeManager* nm = NodeManager::currentNM(); bool has_nreduce = false; std::vector terms = d_extt.getActive(); + // the set of terms we have done extf inferences for + std::unordered_set inferProcessed; for (const Node& n : terms) { // Setup information about n, including if it is equal to a constant. @@ -415,16 +417,22 @@ void ExtfSolver::checkExtfEval(int effort) effort == 0 ? Inference::EXTF_D : Inference::EXTF_D_N; d_im.sendInternalInference(einfo.d_exp, nrcAssert, infer); } - to_reduce = nrc; + // We must use the original n here to avoid circular justifications for + // why extended functions are reduced below. In particular, to_reduce + // should never be a duplicate of another term considered in the block + // of code for checkExtfInference below. + to_reduce = n; } } else { to_reduce = n; } - // if not reduced - if (!to_reduce.isNull()) + // if not reduced and not processed + if (!to_reduce.isNull() + && inferProcessed.find(to_reduce) == inferProcessed.end()) { + inferProcessed.insert(to_reduce); Assert(effort < 3); if (effort == 1) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 656bb5880..38b741ced 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2114,6 +2114,7 @@ set(regress_3_tests regress3/sixfuncs.sy regress3/strings-any-term.sy regress3/strings/extf_d_perf.smt2 + regress3/strings/unsat-circ-reduce.smt2 ) #-----------------------------------------------------------------------------# diff --git a/test/regress/regress3/strings/unsat-circ-reduce.smt2 b/test/regress/regress3/strings/unsat-circ-reduce.smt2 new file mode 100644 index 000000000..b584c0fb1 --- /dev/null +++ b/test/regress/regress3/strings/unsat-circ-reduce.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --strings-exp --no-re-elim +; EXPECT: unsat +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-fun x () String) +(assert (not (= +(let ((_let_0 (re.* re.allchar ))) +(str.in_re x (re.++ re.allchar _let_0 (str.to_re "AC") _let_0 (str.to_re "CA") _let_0))) +(let ((_let_0 (+ 0 1))) (let ((_let_1 (str.indexof x "AC" _let_0))) (and (not (= _let_1 (- 1))) (not (= (str.indexof x "CA" (+ _let_1 (str.len "AC"))) (- 1)))))) +))) +(assert (<= (str.len x) 8)) +; adding --strings-fmf to command line above incorrectly said "sat" for this at ad0b69e6 +(check-sat) -- cgit v1.2.3