diff options
| -rw-r--r-- | src/smt/check_models.cpp | 1 | ||||
| -rw-r--r-- | src/theory/strings/extf_solver.cpp | 18 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress2/strings/issue5381.smt2 | 30 |
4 files changed, 44 insertions, 6 deletions
diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index a55f53f96..612084de2 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -174,6 +174,7 @@ void CheckModels::checkModel(Model* m, Notice() << "SmtEngine::checkModel(): checking assertion " << assertion << std::endl; Node n = assertion; + Notice() << "SmtEngine::checkModel(): -- rewritten form is " << Rewriter::rewrite(n) << std::endl; Node nr = Rewriter::rewrite(substitutions.apply(n)); if (nr.isConst() && nr.getConst<bool>()) { diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 53cd92ac2..531b281a7 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -81,11 +81,13 @@ bool ExtfSolver::doReduction(int effort, Node n) if (!d_extfInfoTmp[n].d_modelActive) { // n is not active in the model, no need to reduce + Trace("strings-extf-debug") << "...skip due to model active" << std::endl; return false; } if (d_reduced.find(n)!=d_reduced.end()) { // already sent a reduction lemma + Trace("strings-extf-debug") << "...skip due to reduced" << std::endl; return false; } // determine the effort level to process the extf at @@ -157,6 +159,8 @@ bool ExtfSolver::doReduction(int effort, Node n) } if (effort != r_effort) { + + Trace("strings-extf-debug") << "...skip due to effort" << std::endl; // not the right effort level to reduce return false; } @@ -202,6 +206,8 @@ bool ExtfSolver::doReduction(int effort, Node n) Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl; Trace("strings-red-lemma") << "...from " << n << std::endl; + Trace("strings-red-lemma") + << "Reduction_" << effort << " rewritten : " << Rewriter::rewrite(nnlem) << std::endl; d_im.sendInference(d_emptyVec, nnlem, Inference::REDUCTION, false, true); Trace("strings-extf-debug") << " resolve extf : " << n << " based on reduction." << std::endl; @@ -625,13 +631,13 @@ void ExtfSolver::checkExtfInference(Node n, } else { - // If we already know that s (does not) contain t, then n is redundant. - // For example, if str.contains( x, y ), str.contains( z, y ), and x=z - // are asserted in the current context, then str.contains( z, y ) is - // satisfied by all models of str.contains( x, y ) ^ x=z and thus can - // be ignored. + // If we already know that s (does not) contain t, then n may be + // redundant. However, we do not mark n as reduced here, since strings + // reductions may require dependencies between extended functions. + // Marking reduced here could lead to incorrect models if an + // extended function is marked reduced based on an assignment to + // something that depends on n. Trace("strings-extf-debug") << " redundant." << std::endl; - d_extt.markReduced(n); } } return; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 58a43895e..9a0565d8e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2174,6 +2174,7 @@ set(regress_2_tests regress2/strings/cmu-prereg-fmf.smt2 regress2/strings/cmu-repl-len-nterm.smt2 regress2/strings/issue3203.smt2 + regress2/strings/issue5381.smt2 regress2/strings/issue918.smt2 regress2/strings/non_termination_regular_expression6.smt2 regress2/strings/range-perf.smt2 diff --git a/test/regress/regress2/strings/issue5381.smt2 b/test/regress/regress2/strings/issue5381.smt2 new file mode 100644 index 000000000..6efd22a6e --- /dev/null +++ b/test/regress/regress2/strings/issue5381.smt2 @@ -0,0 +1,30 @@ +; COMMAND-LINE: --strings-fmf --strings-exp +; EXPECT: sat +(set-logic QF_SLIA) +(set-info :status sat) +; required for solving the benchmark, although the original benchmark only has an error when this is disabled +(set-option :strings-fmf true) +(declare-fun a () String) +(assert (not (= (ite (str.contains (str.++ (str.replace (str.substr + (str.substr (str.substr a 1 (- (str.len a) 1)) 0 (- (str.len + (str.substr a 1 (- (str.len a) 1))) 0)) 0 (- (+ (str.indexof (str.++ + (str.replace (str.substr (str.substr a 1 (- (str.len a) 1)) 0 1) "A" + "") "") "D" 0) 1) 0)) "" "") (str.substr (str.substr (str.substr a 1 + (- (str.len a) 1)) 1 (str.len (str.substr a 1 (- (str.len a) 1)))) 0 + (str.len (str.substr (str.substr a 1 (- (str.len a) 1)) 0 (str.len + (str.substr a 1 (- (str.len a) 1))))))) "F") 1 0) 0))) +(assert (= (ite (str.contains (str.substr (str.substr (str.substr a 1 + (- (str.len a) 1)) (+ (str.indexof (str.substr a 1 (- (str.len a) + 1)) "A" 0) 1) (str.len (str.substr a 1 (- (str.len a) 1)))) 0 (- + (str.len (str.substr (str.substr a 1 (- (str.len a) 1)) 0 (str.len + (str.substr a 1 (- (str.len a) 1))))) (+ (str.indexof (str.substr + (str.substr a 1 (- (str.len a) 1)) 1 (str.len (str.substr a 1 (- + (str.len a) 1)))) "D" 0) 1))) "D") 1 0) 0)) +(assert (not (= (ite (str.contains (str.substr (str.substr a 1 (- + (str.len a) 1)) 0 (str.len (str.substr a 1 (- (str.len a) 1)))) "D") + 1 0) 0))) +(assert (<= (+ (str.indexof (str.substr (str.substr a 1 (- (str.len a) + 1)) (+ (str.indexof (str.substr a 1 (- (str.len a) 1)) "A" 0) 1) (- + (str.len (str.substr a 1 (- (str.len a) 1))) 0)) "D" 0) 1) 0)) +(check-sat) +(exit) |