diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-30 09:41:37 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-30 09:41:37 -0600 |
commit | ac6150d7992b5dd1cace8d8d6e0d308e4a741c12 (patch) | |
tree | e8379438a90fdb24539578c04688f66d41ba7905 /src/theory/strings/regexp_elim.cpp | |
parent | 865d1ee48de8e4a21d1e97c707be46c34918367d (diff) |
(proof-new) Proofs for regular expression elimination (#5361)
Adds support for proofs for regular expression elimination in TheoryStrings::ppRewrite via a coarse-grained rule RE_ELIM.
This rule is updated by this PR to distinguish whether we apply aggressive elimination. Aggressive elimination is not currently supported, since it is non-deterministic due to generating fresh BOUND_VARIABLE.
Diffstat (limited to 'src/theory/strings/regexp_elim.cpp')
-rw-r--r-- | src/theory/strings/regexp_elim.cpp | 57 |
1 files changed, 45 insertions, 12 deletions
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 1d0db0e4d..aaa9ffc48 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -20,30 +20,58 @@ #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" -using namespace CVC4; using namespace CVC4::kind; -using namespace CVC4::theory; -using namespace CVC4::theory::strings; -RegExpElimination::RegExpElimination() +namespace CVC4 { +namespace theory { +namespace strings { + +RegExpElimination::RegExpElimination(bool isAgg, + ProofNodeManager* pnm, + context::Context* c) + : d_isAggressive(isAgg), + d_pnm(pnm), + d_epg(pnm == nullptr + ? nullptr + : new EagerProofGenerator(pnm, c, "RegExpElimination::epg")) { } -Node RegExpElimination::eliminate(Node atom) +Node RegExpElimination::eliminate(Node atom, bool isAgg) { Assert(atom.getKind() == STRING_IN_REGEXP); if (atom[1].getKind() == REGEXP_CONCAT) { - return eliminateConcat(atom); + return eliminateConcat(atom, isAgg); } else if (atom[1].getKind() == REGEXP_STAR) { - return eliminateStar(atom); + return eliminateStar(atom, isAgg); } return Node::null(); } -Node RegExpElimination::eliminateConcat(Node atom) +TrustNode RegExpElimination::eliminateTrusted(Node atom) +{ + Node eatom = eliminate(atom, d_isAggressive); + if (!eatom.isNull()) + { + // Currently aggressive doesnt work due to fresh bound variables + if (isProofEnabled() && !d_isAggressive) + { + Node eq = atom.eqNode(eatom); + Node aggn = NodeManager::currentNM()->mkConst(d_isAggressive); + std::shared_ptr<ProofNode> pn = + d_pnm->mkNode(PfRule::RE_ELIM, {}, {atom, aggn}, eq); + d_epg->setProofFor(eq, pn); + return TrustNode::mkTrustRewrite(atom, eatom, d_epg.get()); + } + return TrustNode::mkTrustRewrite(atom, eatom, nullptr); + } + return TrustNode::null(); +} + +Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) { NodeManager* nm = NodeManager::currentNM(); Node x = atom[0]; @@ -217,7 +245,7 @@ Node RegExpElimination::eliminateConcat(Node atom) // otherwise, we can use indexof to represent some next occurrence if (gap_exact[i + 1] && i + 1 != size) { - if (!options::regExpElimAgg()) + if (!isAgg) { canProcess = false; break; @@ -330,7 +358,7 @@ Node RegExpElimination::eliminateConcat(Node atom) } } - if (!options::regExpElimAgg()) + if (!isAgg) { return Node::null(); } @@ -455,9 +483,9 @@ Node RegExpElimination::eliminateConcat(Node atom) return Node::null(); } -Node RegExpElimination::eliminateStar(Node atom) +Node RegExpElimination::eliminateStar(Node atom, bool isAgg) { - if (!options::regExpElimAgg()) + if (!isAgg) { return Node::null(); } @@ -580,3 +608,8 @@ Node RegExpElimination::returnElim(Node atom, Node atomElim, const char* id) << "." << std::endl; return atomElim; } +bool RegExpElimination::isProofEnabled() const { return d_pnm != nullptr; } + +} // namespace strings +} // namespace theory +} // namespace CVC4 |