From 204d3a6799f5f6d96b321cb1e2092b11233db6d8 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 12 May 2020 14:46:40 -0500 Subject: Reg exp unfold, more eq proof --- src/theory/strings/proof_checker.cpp | 4 +- src/theory/strings/regexp_operation.cpp | 80 ++++++++++++++++++--------------- src/theory/strings/regexp_operation.h | 10 ++--- src/theory/uf/eq_proof.cpp | 31 ++++++++++--- 4 files changed, 75 insertions(+), 50 deletions(-) diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp index 226db01f6..191e0e16c 100644 --- a/src/theory/strings/proof_checker.cpp +++ b/src/theory/strings/proof_checker.cpp @@ -444,11 +444,11 @@ Node StringProofRuleChecker::checkInternal(PfRule id, SkolemCache sc; if (id == PfRule::RE_UNFOLD_POS) { - conc = RegExpOpr::reduceRegExpPos(atom[0], atom[1], &sc); + conc = RegExpOpr::reduceRegExpPos(children[0], &sc); } else { - conc = RegExpOpr::reduceRegExpNeg(atom[0], atom[1], &sc); + conc = RegExpOpr::reduceRegExpNeg(children[0], &sc); } return ProofSkolemCache::getWitnessForm(conc); } diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index fbd10b7a3..60be02bb2 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -845,51 +845,48 @@ Node RegExpOpr::simplify(Node t, bool polarity) Node str = t[0]; Node re = t[1]; Node conc; - std::pair p(str, re); - std::map, Node>::const_iterator itr; if(polarity) { - itr = d_simpl_cache.find(p); - if (itr != d_simpl_cache.end()) + conc = reduceRegExpPos(t, d_sc); + // we also immediately unfold the last disjunct for re.* + if (re.getKind() == REGEXP_STAR) { - conc = itr->second; - } - else - { - conc = reduceRegExpPos(str, re, d_sc); - // we also immediately unfold the last disjunct for re.* - if (re.getKind() == REGEXP_STAR) - { - Assert(conc.getKind() == OR && conc.getNumChildren() == 3); - std::vector newChildren; - newChildren.push_back(conc[0]); - newChildren.push_back(conc[1]); - Node starExpUnf = simplify(conc[2], true); - newChildren.push_back(starExpUnf); - conc = NodeManager::currentNM()->mkNode(OR, newChildren); - } - d_simpl_cache[p] = conc; + Assert(conc.getKind() == OR && conc.getNumChildren() == 3); + std::vector newChildren; + newChildren.push_back(conc[0]); + newChildren.push_back(conc[1]); + Node starExpUnf = simplify(conc[2], true); + newChildren.push_back(starExpUnf); + conc = NodeManager::currentNM()->mkNode(OR, newChildren); } } else { - itr = d_simpl_neg_cache.find(p); - if (itr != d_simpl_neg_cache.end()) - { - conc = itr->second; - } - else - { - conc = reduceRegExpNeg(str, re, d_sc); - d_simpl_neg_cache[p] = conc; - } + Node tnot = t.notNode(); + conc = reduceRegExpNeg(tnot, d_sc); } Trace("strings-regexp-simpl") << "RegExpOpr::simplify: returns " << conc << std::endl; return conc; } -Node RegExpOpr::reduceRegExpNeg(Node s, Node r, SkolemCache* sc) +/** + * Associating formulas with their "unfolded form". + */ +struct ReUnfoldAttributeId +{ +}; +typedef expr::Attribute ReUnfoldAttribute; + +Node RegExpOpr::reduceRegExpNeg(Node mem, SkolemCache* sc) { + Assert (mem.getKind()==NOT && mem[0].getKind()==STRING_IN_REGEXP); + ReUnfoldAttribute rua; + if (mem.hasAttribute(rua)) + { + return mem.getAttribute(rua); + } + Node s = mem[0][0]; + Node r = mem[0][1]; NodeManager* nm = NodeManager::currentNM(); Kind k = r.getKind(); Node zero = nm->mkConst(Rational(0)); @@ -986,11 +983,24 @@ Node RegExpOpr::reduceRegExpNeg(Node s, Node r, SkolemCache* sc) conc = nm->mkNode(FORALL, b1v, conc); conc = nm->mkNode(AND, sne, conc); } + else + { + Assert(!utils::isRegExpKind(k)); + } + mem.setAttribute(rua,conc); return conc; } -Node RegExpOpr::reduceRegExpPos(Node s, Node r, SkolemCache* sc) -{ +Node RegExpOpr::reduceRegExpPos(Node mem, SkolemCache* sc) +{ + Assert ( mem.getKind()==STRING_IN_REGEXP); + ReUnfoldAttribute rua; + if (mem.hasAttribute(rua)) + { + return mem.getAttribute(rua); + } + Node s = mem[0]; + Node r = mem[1]; NodeManager* nm = NodeManager::currentNM(); Kind k = r.getKind(); Node conc; @@ -1000,7 +1010,6 @@ Node RegExpOpr::reduceRegExpPos(Node s, Node r, SkolemCache* sc) std::vector cc; // Look up skolems for each of the components. If sc has optimizations // enabled, this will return arguments of str.to_re. - Node mem = nm->mkNode(STRING_IN_REGEXP, s, r); for (unsigned i = 0, nchild = r.getNumChildren(); i < nchild; ++i) { Node index = nm->mkConst(Rational(i)); @@ -1037,6 +1046,7 @@ Node RegExpOpr::reduceRegExpPos(Node s, Node r, SkolemCache* sc) { Assert(!utils::isRegExpKind(k)); } + mem.setAttribute(rua,conc); return conc; } diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index e69657a2c..fec87b350 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -73,8 +73,6 @@ class RegExpOpr { Node d_sigma; Node d_sigma_star; - std::map d_simpl_cache; - std::map d_simpl_neg_cache; std::map > d_delta_cache; std::map d_dv_cache; std::map > d_deriv_cache; @@ -128,13 +126,13 @@ class RegExpOpr { */ Node simplify(Node t, bool polarity); /** - * Return the unfolded form of (str.in_re s r). + * Return the unfolded form of mem of the form (str.in_re s r). */ - static Node reduceRegExpPos(Node s, Node r, SkolemCache* sc); + static Node reduceRegExpPos(Node mem, SkolemCache* sc); /** - * Return the unfolded form of (not (str.in_re s r)). + * Return the unfolded form of mem of the form (not (str.in_re s r)). */ - static Node reduceRegExpNeg(Node s, Node r, SkolemCache* sc); + static Node reduceRegExpNeg(Node mem, SkolemCache* sc); /** * This method returns 1 if the empty string is in r, 2 if the empty string * is not in r, or 0 if it is unknown whether the empty string is in r. diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index f5004e90e..053aa0e9e 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -116,7 +116,8 @@ bool EqProof::foldTransitivityChildren(Node conclusion, unsigned termPos = 2, offending = size; for (unsigned i = 0; i < size; ++i) { - Assert(premises[i].getKind() == kind::EQUAL); + Trace("ajr-temp") << "Premise trans : "<< premises[i] << std::endl; + AlwaysAssert(premises[i].getKind() == kind::EQUAL); for (unsigned j = 0; j < 2; ++j) { if (premises[i][j].getKind() == kind::CONST_BOOLEAN @@ -471,7 +472,8 @@ Node EqProof::addToProof( // refl if (d_id == MERGED_THROUGH_REFLEXIVITY) { - Assert(d_node.getKind() == kind::EQUAL); + Trace("ajr-temp") << "Refl node: " << d_node << std::endl; + AlwaysAssert(d_node.getKind() == kind::EQUAL); std::vector children; std::vector args{d_node[0]}; if (!p->addStep(d_node, PfRule::REFL, children, args)) @@ -496,6 +498,10 @@ Node EqProof::addToProof( // // (= t1 c1) (= t2 c2) // -------------------- MACRO_SR_PRED_INTRO + // (= (= t1 t2) false) + + // The additional step is commented out below: + // -------------------- FALSE_ELIM // (not (= t1 t2)) // // First process the children proofs @@ -522,7 +528,8 @@ Node EqProof::addToProof( // look in children for (unsigned j = 0; j < premises.size(); ++j) { - Assert(premises[j].getKind() == kind::EQUAL); + Trace("ajr-temp") << "Premise : "<< premises[j] << std::endl; + AlwaysAssert(premises[j].getKind() == kind::EQUAL); if (premises[j][0] == term) { Assert(premises[j][1].isConst()); @@ -539,14 +546,24 @@ Node EqProof::addToProof( Trace("eqproof-conv") << "EqProof::addToProof: adding " << PfRule::MACRO_SR_PRED_INTRO << " step from " << children << "\n"; - Node conclusion = d_node[0].notNode(); - if (!p->addStep(conclusion, PfRule::MACRO_SR_PRED_INTRO, children, {conclusion})) + if (!p->addStep(d_node, PfRule::MACRO_SR_PRED_INTRO, children, {d_node})) { Assert(false) << "EqProof::addToProof: couldn't add " << PfRule::MACRO_SR_PRED_INTRO << " rule\n"; } - visited[d_node] = conclusion; - return conclusion; + /* + Node conclusion = d_node[0].notNode(); + Trace("eqproof-conv") << "EqProof::addToProof: adding " + << PfRule::FALSE_ELIM << " step from " << d_node + << "\n"; + if (!p->addStep(conclusion, PfRule::FALSE_ELIM, {d_node}, {})) + { + Assert(false) << "EqProof::addToProof: couldn't add " + << PfRule::FALSE_ELIM << " rule\n"; + } + */ + visited[d_node] = d_node; + return d_node; } if (d_id == MERGED_THROUGH_TRANS) { -- cgit v1.2.3