diff options
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 58 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 7 |
2 files changed, 46 insertions, 19 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index f0e68890a..bf3a170df 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -172,23 +172,35 @@ void RegExpSolver::check() if (!addedLemma) { NodeManager* nm = NodeManager::currentNM(); - for (unsigned i = 0; i < d_regexp_memberships.size(); i++) + // representatives of strings that are the LHS of positive memberships that + // we unfolded + std::unordered_set<Node, NodeHashFunction> repUnfold; + // check positive (e=0), then negative (e=1) memberships + for (unsigned e = 0; e < 2; e++) { - // check regular expression membership - Node assertion = d_regexp_memberships[i]; - Trace("regexp-debug") - << "Check : " << assertion << " " - << (d_regexp_ucached.find(assertion) == d_regexp_ucached.end()) << " " - << (d_regexp_ccached.find(assertion) == d_regexp_ccached.end()) - << std::endl; - if (d_regexp_ucached.find(assertion) == d_regexp_ucached.end() - && d_regexp_ccached.find(assertion) == d_regexp_ccached.end()) + for (const Node& assertion : d_regexp_memberships) { + // check regular expression membership + Trace("regexp-debug") + << "Check : " << assertion << " " + << (d_regexp_ucached.find(assertion) == d_regexp_ucached.end()) + << " " + << (d_regexp_ccached.find(assertion) == d_regexp_ccached.end()) + << std::endl; + if (d_regexp_ucached.find(assertion) != d_regexp_ucached.end() + || d_regexp_ccached.find(assertion) != d_regexp_ccached.end()) + { + continue; + } Trace("strings-regexp") << "We have regular expression assertion : " << assertion << std::endl; Node atom = assertion.getKind() == NOT ? assertion[0] : assertion; bool polarity = assertion.getKind() != NOT; + if (polarity != (e == 0)) + { + continue; + } bool flag = true; Node x = atom[0]; Node r = atom[1]; @@ -228,7 +240,16 @@ void RegExpSolver::check() break; } } - + if (e == 1 && repUnfold.find(x) != repUnfold.end()) + { + // do not unfold negative memberships of strings that have new + // positive unfoldings. For example: + // x in ("A")* ^ NOT x in ("B")* + // We unfold x = "A" ++ x' only. The intution here is that positive + // unfoldings lead to stronger constraints (equalities are stronger + // than disequalities), and are easier to check. + continue; + } if (polarity) { flag = checkPDerivative(x, r, atom, addedLemma, rnfexp); @@ -269,11 +290,18 @@ void RegExpSolver::check() { processed.push_back(assertion); } + if (e == 0) + { + // Remember that we have unfolded a membership for x + // notice that we only do this here, after we have definitely + // added a lemma. + repUnfold.insert(x); + } + } + if (d_parent.inConflict()) + { + break; } - } - if (d_parent.inConflict()) - { - break; } } } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index cea3c3515..7b6bbdc99 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -4023,10 +4023,9 @@ void TheoryStrings::registerTerm( Node n, int effort ) { else if (n.getKind() == STRING_STRIDOF) { Node len = mkLength(n[0]); - Node lem = nm->mkNode( - AND, - nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))), - nm->mkNode(LT, n, len)); + Node lem = nm->mkNode(AND, + nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))), + nm->mkNode(LT, n, len)); d_out->lemma(lem); } } |