From 923abd7000a2ab6e3c0776c59d159bdc3a4d9a52 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 Sep 2019 18:26:41 -0500 Subject: [PATCH] Fix off by one error in strings flat form explanation (#3273) Fixes #3272. This was caused by not explaining the last equal component in a flat form inference. For example, if `x=y`, we may infer `z=""` from `u++x++z=u++y` since the 1st and 2nd components of these strings are equal. However, we would not add the explanation of `x=y` due to an off-by-one error. Notice that this code is very rarely used (the code for F_EndpointEmp is not covered by our regressions). This is since length elaboration should catch conflicting cases like above, where `len(u++x++z)!=len(u++y)` if `x=y` and `z!=""` and thus `u++x++z != u++y`. #3272 happened to catch a rare case where it is applied. This is likely due to theory combination not propagating an equality prior to running a full effort call to strings check, which is unexpected but not impossible. --- src/theory/strings/theory_strings.cpp | 18 ++++++++++----- test/regress/CMakeLists.txt | 1 + test/regress/regress1/strings/issue3272.smt2 | 23 ++++++++++++++++++++ 3 files changed, 37 insertions(+), 5 deletions(-) create mode 100644 test/regress/regress1/strings/issue3272.smt2 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& 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& 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 conc_c; for (unsigned j = count; j < bsize; j++) @@ -2412,7 +2418,6 @@ void TheoryStrings::checkFlatForm(std::vector& 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& 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 conc_c; for (unsigned j = count; j < asize; j++) @@ -2445,7 +2453,6 @@ void TheoryStrings::checkFlatForm(std::vector& eqc, conc = utils::mkAnd(conc_c); inf_type = 2; Assert(count > 0); - count--; break; } else @@ -2558,10 +2565,11 @@ void TheoryStrings::checkFlatForm(std::vector& 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) -- 2.30.2