diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-25 18:26:41 -0500 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-09-25 16:26:41 -0700 |
| commit | 923abd7000a2ab6e3c0776c59d159bdc3a4d9a52 (patch) | |
| tree | 8f5a1e11428ce181abc5b722997847c4faecc29f /src | |
| parent | 91565cda11ad42082a11055514e12ddeee459460 (diff) | |
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.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 18 |
1 files changed, 13 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, |