diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-02 11:43:53 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-02 16:43:53 +0000 |
commit | c6c40d12c38fb30d0c4f503353532b93f03e745a (patch) | |
tree | 366ad9f9af8144e4259a39bbce7379d7bd2ce944 /src/theory | |
parent | ed1e21df4c7364e9d78f1a5c0605c45640d9ccca (diff) |
Fix case where RE unfolding generates a trivially true lemma (#6267)
An RE unfolding lemma may rewrite to true for tautological RE memberships that our rewriter does not rewrite the membership to true.
An example is (str.in_re x (re.* (re.union (str.to_re "A") (str.to_re x))).
This PR ensures we are robust to these cases.
This fixes benchmarks 3-5 from #6203. Benchmark 3 is added here, 4-5 time out.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/regexp_solver.cpp | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 7737a90f7..0db536d1b 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -284,16 +284,21 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) } InferenceId inf = polarity ? InferenceId::STRINGS_RE_UNFOLD_POS : InferenceId::STRINGS_RE_UNFOLD_NEG; - d_im.sendInference(iexp, noExplain, conc, inf); - addedLemma = true; - processed.push_back(assertion); - if (e == 0) + // in very rare cases, we may find out that the unfolding lemma + // for a membership is equivalent to true, in spite of the RE + // not being rewritten to true. + if (d_im.sendInference(iexp, noExplain, conc, inf)) { - // 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); + addedLemma = true; + 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); + } } + processed.push_back(assertion); } else { |