diff options
Diffstat (limited to 'src/theory/strings/infer_proof_cons.cpp')
-rw-r--r-- | src/theory/strings/infer_proof_cons.cpp | 140 |
1 files changed, 131 insertions, 9 deletions
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index d214babae..b8c0a851c 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -84,7 +84,7 @@ void InferProofCons::convert(InferenceId infer, { Trace("strings-ipc-debug") << "InferProofCons::convert: " << infer << (isRev ? " :rev " : " ") << conc << std::endl; - for (const Node& ec : exp) + for (const Node& ec : ps.d_children) { Trace("strings-ipc-debug") << " e: " << ec << std::endl; } @@ -103,9 +103,17 @@ void InferProofCons::convert(InferenceId infer, case InferenceId::STRINGS_NORMAL_FORM: case InferenceId::STRINGS_CODE_PROXY: { - ps.d_args.push_back(conc); - // will attempt this rule - ps.d_rule = PfRule::MACRO_SR_PRED_INTRO; + std::vector<Node> pcs = ps.d_children; + Node pconc = conc; + // purify core substitution proves conc from pconc if necessary, + // we apply MACRO_SR_PRED_INTRO to prove pconc + if (purifyCoreSubstitution(pconc, pcs, psb, false)) + { + if (psb.applyPredIntro(pconc, pcs)) + { + useBuffer = true; + } + } } break; // ========================== substitution + rewriting @@ -232,14 +240,23 @@ void InferProofCons::convert(InferenceId infer, break; } // apply MACRO_SR_PRED_ELIM using equalities up to the main eq + // we purify the core substitution + std::vector<Node> pcsr(ps.d_children.begin(), + ps.d_children.begin() + mainEqIndex); + Node pmainEq = mainEq; + // we transform mainEq to pmainEq and then use this as the first + // argument to MACRO_SR_PRED_ELIM. + if (!purifyCoreSubstitution(pmainEq, pcsr, psb, true)) + { + break; + } std::vector<Node> childrenSRew; - childrenSRew.push_back(mainEq); - childrenSRew.insert(childrenSRew.end(), - ps.d_children.begin(), - ps.d_children.begin() + mainEqIndex); + childrenSRew.push_back(pmainEq); + childrenSRew.insert(childrenSRew.end(), pcsr.begin(), pcsr.end()); + // now, conclude the proper equality Node mainEqSRew = psb.tryStep(PfRule::MACRO_SR_PRED_ELIM, childrenSRew, {}); - if (CDProof::isSame(mainEqSRew, mainEq)) + if (CDProof::isSame(mainEqSRew, pmainEq)) { Trace("strings-ipc-core") << "...undo step" << std::endl; // the rule added above was not necessary @@ -1048,6 +1065,111 @@ std::string InferProofCons::identify() const return "strings::InferProofCons"; } +bool InferProofCons::purifyCoreSubstitution(Node& tgt, + std::vector<Node>& children, + TheoryProofStepBuffer& psb, + bool concludeTgtNew) const +{ + // collect the terms to purify, which are the LHS of the substitution + std::unordered_set<Node> termsToPurify; + for (const Node& nc : children) + { + Assert(nc.getKind() == EQUAL && nc[0].getType().isStringLike()); + termsToPurify.insert(nc[0]); + } + // now, purify each of the children of the substitution + for (size_t i = 0, nchild = children.size(); i < nchild; i++) + { + Node pnc = purifyCorePredicate(children[i], true, psb, termsToPurify); + if (pnc.isNull()) + { + return false; + } + if (children[i] != pnc) + { + Trace("strings-ipc-pure-subs") + << "Converted: " << children[i] << " to " << pnc << std::endl; + children[i] = pnc; + } + // we now should have a substitution with only atomic terms + Assert(children[i][0].getNumChildren() == 0); + } + // now, purify the target predicate + tgt = purifyCorePredicate(tgt, concludeTgtNew, psb, termsToPurify); + return !tgt.isNull(); +} + +Node InferProofCons::purifyCorePredicate( + Node lit, + bool concludeNew, + TheoryProofStepBuffer& psb, + std::unordered_set<Node>& termsToPurify) const +{ + bool pol = lit.getKind() != NOT; + Node atom = pol ? lit : lit[0]; + if (atom.getKind() != EQUAL || !atom[0].getType().isStringLike()) + { + // we only purify string (dis)equalities + return lit; + } + // purify both sides of the equality + std::vector<Node> pcs; + bool childChanged = false; + for (const Node& lc : atom) + { + Node plc = purifyCoreTerm(lc, termsToPurify); + childChanged = childChanged || plc != lc; + pcs.push_back(plc); + } + if (!childChanged) + { + return lit; + } + NodeManager* nm = NodeManager::currentNM(); + Node newLit = nm->mkNode(EQUAL, pcs); + if (!pol) + { + newLit = newLit.notNode(); + } + Assert(lit != newLit); + // prove by transformation, should always succeed + if (!psb.applyPredTransform( + concludeNew ? lit : newLit, concludeNew ? newLit : lit, {})) + { + // failed, return null + return Node::null(); + } + return newLit; +} + +Node InferProofCons::purifyCoreTerm( + Node n, std::unordered_set<Node>& termsToPurify) const +{ + Assert(n.getType().isStringLike()); + if (n.getNumChildren() == 0) + { + return n; + } + NodeManager* nm = NodeManager::currentNM(); + if (n.getKind() == STRING_CONCAT) + { + std::vector<Node> pcs; + for (const Node& nc : n) + { + pcs.push_back(purifyCoreTerm(nc, termsToPurify)); + } + return nm->mkNode(STRING_CONCAT, pcs); + } + if (termsToPurify.find(n) == termsToPurify.end()) + { + // did not need to purify + return n; + } + SkolemManager* sm = nm->getSkolemManager(); + Node k = sm->mkPurifySkolem(n, "k"); + return k; +} + } // namespace strings } // namespace theory } // namespace cvc5 |