diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -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, |