diff options
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 18 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue3272.smt2 | 23 |
3 files changed, 37 insertions, 5 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 0f9a78516..fafff1412 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2380,6 +2380,9 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc, inelig.push_back(eqc[start]); } Node a = eqc[start]; + Trace("strings-ff-debug") + << "Check flat form for a = " << a << ", whose flat form is " + << d_flat_form[a] << ")" << std::endl; Node b; do { @@ -2398,6 +2401,9 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc, unsigned bsize = d_flat_form[b].size(); if (count < bsize) { + Trace("strings-ff-debug") + << "Found endpoint (in a) with non-empty b = " << b + << ", whose flat form is " << d_flat_form[b] << std::endl; // endpoint std::vector<Node> conc_c; for (unsigned j = count; j < bsize; j++) @@ -2412,7 +2418,6 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc, // swap, will enforce is empty past current a = eqc[i]; b = eqc[start]; - count--; break; } inelig.push_back(eqc[i]); @@ -2434,6 +2439,9 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc, if (count == d_flat_form[b].size()) { inelig.push_back(b); + Trace("strings-ff-debug") + << "Found endpoint in b = " << b << ", whose flat form is " + << d_flat_form[b] << std::endl; // endpoint std::vector<Node> conc_c; for (unsigned j = count; j < asize; j++) @@ -2445,7 +2453,6 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc, conc = utils::mkAnd(conc_c); inf_type = 2; Assert(count > 0); - count--; break; } else @@ -2558,10 +2565,11 @@ void TheoryStrings::checkFlatForm(std::vector<Node>& eqc, } } } - // notice that F_EndpointEmp is not typically applied, since + // Notice that F_EndpointEmp is not typically applied, since // strict prefix equality ( a.b = a ) where a,b non-empty - // is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a) - // when len(b)!=0. + // is conflicting by arithmetic len(a.b)=len(a)+len(b)!=len(a) + // when len(b)!=0. Although if we do not infer this conflict eagerly, + // it may be applied (see #3272). d_im.sendInference( exp, conc, diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index bcae83b0a..a1be9ad62 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1571,6 +1571,7 @@ set(regress_1_tests regress1/strings/issue2982.smt2 regress1/strings/issue3090.smt2 regress1/strings/issue3217.smt2 + regress1/strings/issue3272.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue3272.smt2 b/test/regress/regress1/strings/issue3272.smt2 new file mode 100644 index 000000000..47759ef1e --- /dev/null +++ b/test/regress/regress1/strings/issue3272.smt2 @@ -0,0 +1,23 @@ +(set-logic ALL_SUPPORTED) +(set-option :strings-exp true) +(set-info :status sat) +(declare-fun a () String) +(declare-fun b () String) +(declare-fun c () String) +(assert + (and + (and + (and + (not (= (ite (= (str.at (str.substr c 1 (- (str.len (str.substr c 0 (- (str.len c) 1))) 1)) (- (str.len (str.substr (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1))) 1)) "\t") 1 0) 0)) + + (= (ite (= (str.at (str.substr (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1)) 0) "\n") 1 0) 0) + ) + + (= (ite (= (str.at (str.substr (str.substr c 1 (- (str.len c) 1)) 0 (- (str.len (str.substr (str.replace a b "") 1 (- (str.len (str.replace a b "")) 1))) 1)) 0) " ") 1 0) 0) + (not (= (ite (= (str.at (str.substr (str.replace a b "") 1 (- (str.len c) 1)) (- (str.len (str.substr c 1 (- (str.len c) 1))) 1)) "\v") 1 0) 0)) + ) + (= (ite (= (str.at (str.substr c 1 (- (str.len (str.replace a b "")) 1)) 0) " ") 1 0) 0) + ) +) +; may trigger F_EndpointEmp inference +(check-sat) |