diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-25 21:41:27 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-25 21:41:27 -0600 |
commit | c725b56d1a5a1f896ee76178c718093859aedccb (patch) | |
tree | 4fb103688e664cf6b800d40003320bf5f03c9df6 /src | |
parent | 1c7ed68156cb3cf19ef036cbbfff18bcc4e45c36 (diff) |
(proof-new) Fix regular expression unfolding under substitution (#5958)
This case was previously unhandled and exercised by a recently added regression.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/infer_proof_cons.cpp | 40 |
1 files changed, 34 insertions, 6 deletions
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index c3e1ce294..3bbfc1c98 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -533,16 +533,34 @@ void InferProofCons::convert(InferenceId infer, case InferenceId::STRINGS_RE_UNFOLD_POS: case InferenceId::STRINGS_RE_UNFOLD_NEG: { - if (infer == InferenceId::STRINGS_RE_UNFOLD_POS) + Assert (!ps.d_children.empty()); + size_t nchild = ps.d_children.size(); + Node mem = ps.d_children[nchild-1]; + if (nchild>1) + { + // if more than one, apply MACRO_SR_PRED_ELIM + std::vector<Node> tcs; + tcs.insert(tcs.end(), + ps.d_children.begin(), + ps.d_children.begin() + (nchild-1)); + mem = psb.applyPredElim(mem, tcs); + useBuffer = true; + } + PfRule r = PfRule::UNKNOWN; + if (mem.isNull()) + { + // failed to eliminate above + Assert(false) << "Failed to apply MACRO_SR_PRED_ELIM for RE unfold"; + useBuffer = false; + } + else if (infer == InferenceId::STRINGS_RE_UNFOLD_POS) { - ps.d_rule = PfRule::RE_UNFOLD_POS; + r = PfRule::RE_UNFOLD_POS; } else { - ps.d_rule = PfRule::RE_UNFOLD_NEG; + r = PfRule::RE_UNFOLD_NEG; // it may be an optimized form of concat simplification - Assert(ps.d_children.size() == 1); - Node mem = ps.d_children[0]; Assert(mem.getKind() == NOT && mem[0].getKind() == STRING_IN_REGEXP); if (mem[0][1].getKind() == REGEXP_CONCAT) { @@ -552,10 +570,20 @@ void InferProofCons::convert(InferenceId infer, // version if (!reLen.isNull()) { - ps.d_rule = PfRule::RE_UNFOLD_NEG_CONCAT_FIXED; + r = PfRule::RE_UNFOLD_NEG_CONCAT_FIXED; } } } + if (useBuffer) + { + mem = psb.tryStep(r, {mem}, {}); + // should match the conclusion + useBuffer = (mem==conc); + } + else + { + ps.d_rule = r; + } } break; // ========================== Reduction |