diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-23 18:15:28 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-23 16:15:28 -0700 |
commit | 64cef995a521ac7211b9e3ed95c85deb186ff352 (patch) | |
tree | 927d14ff521127f37192afcfe8b737f15d54e061 /src/theory/strings/regexp_solver.cpp | |
parent | 0d4d9bf3f31687d9cf48b0c45ab420b06ff099f7 (diff) |
Fixes for SyGuS + regular expressions (#3313)
This commit fixes numerous issues involving the combination of SyGuS and regular expressions.
Combining SyGuS and regular expressions may involve constructing regular expressions that are neither variables nor builtin regular expression operators. The code was not robust for this case, either throwing spurious assertion failures or having incorrect behavior.
Diffstat (limited to 'src/theory/strings/regexp_solver.cpp')
-rw-r--r-- | src/theory/strings/regexp_solver.cpp | 50 |
1 files changed, 29 insertions, 21 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 0e44c9461..11471c09f 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -227,29 +227,37 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) << std::endl; // if so, do simple unrolling std::vector<Node> nvec; - if (nvec.empty()) + Trace("strings-regexp") << "Simplify on " << atom << std::endl; + d_regexp_opr.simplify(atom, nvec, polarity); + Trace("strings-regexp") << "...finished" << std::endl; + // if simplifying successfully generated a lemma + if (!nvec.empty()) { - d_regexp_opr.simplify(atom, nvec, polarity); - } - std::vector<Node> exp_n; - exp_n.push_back(assertion); - Node conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(AND, nvec); - d_im.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold"); - addedLemma = true; - if (changed) - { - cprocessed.push_back(assertion); + std::vector<Node> exp_n; + exp_n.push_back(assertion); + Node conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(AND, nvec); + d_im.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold"); + addedLemma = true; + if (changed) + { + cprocessed.push_back(assertion); + } + else + { + 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(rep); + } } else { - 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(rep); + // otherwise we are incomplete + d_parent.getOutputChannel().setIncomplete(); } } if (d_state.isInConflict()) @@ -387,7 +395,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems) Assert(m.getKind() == NOT && m[0].getKind() == STRING_IN_REGEXP); continue; } - RegExpConstType rct = d_regexp_opr.getRegExpConstType(m); + RegExpConstType rct = d_regexp_opr.getRegExpConstType(m[1]); if (rct == RE_C_VARIABLE || (options::stringRegExpInterMode() == RE_INTER_CONSTANT && rct != RE_C_CONRETE_CONSTANT)) @@ -629,7 +637,7 @@ Node RegExpSolver::getNormalSymRegExp(Node r, std::vector<Node>& nf_exp) { Trace("strings-error") << "Unsupported term: " << r << " in normalization SymRegExp." << std::endl; - Assert(false); + Assert(!RegExpOpr::isRegExpKind(r.getKind())); } } return ret; |