diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/proof_rule.h | 15 | ||||
-rw-r--r-- | src/smt/proof_post_processor.cpp | 48 | ||||
-rw-r--r-- | src/theory/builtin/proof_checker.cpp | 20 | ||||
-rw-r--r-- | src/theory/builtin/proof_checker.h | 6 | ||||
-rw-r--r-- | src/theory/rewriter.cpp | 51 | ||||
-rw-r--r-- | src/theory/rewriter.h | 3 |
6 files changed, 111 insertions, 32 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index e24d5c522..2b5565318 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -201,16 +201,17 @@ enum class PfRule : uint32_t THEORY_LEMMA, // ======== Theory Rewrite // Children: none - // Arguments: (F, tid, preRewrite?) + // Arguments: (F, tid, rid) // ---------------------------------------- // Conclusion: F // where F is an equality of the form (= t t') where t' is obtained by - // applying the theory rewriter with identifier tid in either its prewrite - // (when preRewrite is true) or postrewrite method. Notice that the checker - // for this rule does not replay the rewrite to ensure correctness, since - // theory rewriter methods are not static. For example, the quantifiers - // rewriter involves constructing new bound variables that are not guaranteed - // to be consistent on each call. + // applying the kind of rewriting given by the method identifier rid, which + // is one of: + // { RW_REWRITE_THEORY_PRE, RW_REWRITE_THEORY_POST, RW_REWRITE_EQ_EXT } + // Notice that the checker for this rule does not replay the rewrite to ensure + // correctness, since theory rewriter methods are not static. For example, + // the quantifiers rewriter involves constructing new bound variables that are + // not guaranteed to be consistent on each call. THEORY_REWRITE, // The rules in this section have the signature of a "trusted rule": // diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index a7723d265..40e61964c 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -21,6 +21,7 @@ #include "smt/smt_statistics_registry.h" #include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" +#include "theory/theory.h" using namespace CVC4::kind; using namespace CVC4::theory; @@ -543,14 +544,11 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, Node eq = args[0].eqNode(ret); if (idr == MethodId::RW_REWRITE || idr == MethodId::RW_REWRITE_EQ_EXT) { - // automatically expand THEORY_REWRITE as well here if set - bool elimTR = - (d_elimRules.find(PfRule::THEORY_REWRITE) != d_elimRules.end()); // rewrites from theory::Rewriter bool isExtEq = (idr == MethodId::RW_REWRITE_EQ_EXT); // use rewrite with proof interface Rewriter* rr = d_smte->getRewriter(); - TrustNode trn = rr->rewriteWithProof(args[0], elimTR, isExtEq); + TrustNode trn = rr->rewriteWithProof(args[0], isExtEq); std::shared_ptr<ProofNode> pfn = trn.toProofNode(); if (pfn == nullptr) { @@ -559,10 +557,17 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // did not have a proof of rewriting, probably isExtEq is true if (isExtEq) { - // don't update - return Node::null(); + // update to THEORY_REWRITE with idr + Assert(args.size() >= 1); + TheoryId theoryId = Theory::theoryOf(args[0].getType()); + Node tid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId); + cdp->addStep(eq, PfRule::THEORY_REWRITE, {}, {eq, tid, args[1]}); + } + else + { + // this should never be applied + cdp->addStep(eq, PfRule::TRUST_REWRITE, {}, {eq}); } - cdp->addStep(eq, PfRule::TRUST_REWRITE, {}, {eq}); } else { @@ -590,6 +595,24 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, } return eq; } + else if (id == PfRule::THEORY_REWRITE) + { + Assert(!args.empty()); + Node eq = args[0]; + Assert(eq.getKind() == EQUAL); + // try to replay theory rewrite + // first, check that maybe its just an evaluation step + ProofChecker* pc = d_pnm->getChecker(); + Node ceval = + pc->checkDebug(PfRule::EVALUATE, {}, {eq[0]}, eq, "smt-proof-pp-debug"); + if (!ceval.isNull() && ceval == eq) + { + cdp->addStep(eq, PfRule::EVALUATE, {}, {eq[0]}); + return eq; + } + // otherwise no update + Trace("final-pf-hole") << "hole: " << id << " : " << eq << std::endl; + } // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS? @@ -712,14 +735,6 @@ bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn, bool& continueUpdate) { PfRule r = pn->getRule(); - if (Trace.isOn("final-pf-hole")) - { - if (r == PfRule::THEORY_REWRITE) - { - Trace("final-pf-hole") << "hole: " << r << " : " << pn->getResult() - << std::endl; - } - } // if not doing eager pedantic checking, fail if below threshold if (!options::proofNewPedanticEager()) { @@ -758,7 +773,8 @@ ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm, ProofGenerator* pppg) : d_pnm(pnm), d_cb(pnm, smte, pppg), - d_updater(d_pnm, d_cb), + // the update merges subproofs + d_updater(d_pnm, d_cb, true), d_finalCb(pnm), d_finalizer(d_pnm, d_finalCb) { diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 73d39f417..4e2e78bae 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -34,6 +34,8 @@ const char* toString(MethodId id) case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT"; case MethodId::RW_EVALUATE: return "RW_EVALUATE"; case MethodId::RW_IDENTITY: return "RW_IDENTITY"; + case MethodId::RW_REWRITE_THEORY_PRE: return "RW_REWRITE_THEORY_PRE"; + case MethodId::RW_REWRITE_THEORY_POST: return "RW_REWRITE_THEORY_POST"; case MethodId::SB_DEFAULT: return "SB_DEFAULT"; case MethodId::SB_LITERAL: return "SB_LITERAL"; case MethodId::SB_FORMULA: return "SB_FORMULA"; @@ -76,7 +78,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3); pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1); pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1); - pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1); + pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 3); } Node BuiltinProofRuleChecker::applySubstitutionRewrite( @@ -282,6 +284,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, exp.push_back(children[i]); } Node res = applySubstitution(args[0], exp, ids); + if (res.isNull()) + { + return Node::null(); + } return args[0].eqNode(res); } else if (id == PfRule::REWRITE) @@ -294,6 +300,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, return Node::null(); } Node res = applyRewrite(args[0], idr); + if (res.isNull()) + { + return Node::null(); + } return args[0].eqNode(res); } else if (id == PfRule::EVALUATE) @@ -301,6 +311,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, Assert(children.empty()); Assert(args.size() == 1); Node res = applyRewrite(args[0], MethodId::RW_EVALUATE); + if (res.isNull()) + { + return Node::null(); + } return args[0].eqNode(res); } else if (id == PfRule::MACRO_SR_EQ_INTRO) @@ -312,6 +326,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, return Node::null(); } Node res = applySubstitutionRewrite(args[0], children, ids, idr); + if (res.isNull()) + { + return Node::null(); + } return args[0].eqNode(res); } else if (id == PfRule::MACRO_SR_PRED_INTRO) diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 66b04de45..fc26beaa1 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -50,6 +50,12 @@ enum class MethodId : uint32_t RW_EVALUATE, // identity RW_IDENTITY, + // theory preRewrite, note this is only intended to be used as an argument + // to THEORY_REWRITE in the final proof. It is not implemented in + // applyRewrite below, see documentation in proof_rule.h for THEORY_REWRITE. + RW_REWRITE_THEORY_PRE, + // same as above, for theory postRewrite + RW_REWRITE_THEORY_POST, //---------------------------- Substitutions // (= x y) is interpreted as x -> y, using Node::substitute SB_DEFAULT, diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 9e5708d4d..7ebacee92 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -31,6 +31,13 @@ using namespace std; namespace CVC4 { namespace theory { +/** Attribute true for nodes that have been rewritten with proofs enabled */ +struct RewriteWithProofsAttributeId +{ +}; +typedef expr::Attribute<RewriteWithProofsAttributeId, bool> + RewriteWithProofsAttribute; + // Note that this function is a simplified version of Theory::theoryOf for // (type-based) theoryOfMode. We expand and simplify it here for the sake of // efficiency. @@ -100,7 +107,6 @@ Node Rewriter::rewrite(TNode node) { } TrustNode Rewriter::rewriteWithProof(TNode node, - bool elimTheoryRewrite, bool isExtEq) { // must set the proof checker before calling this @@ -121,6 +127,7 @@ void Rewriter::setProofNodeManager(ProofNodeManager* pnm) // if not already initialized with proof support if (d_tpg == nullptr) { + Trace("rewriter") << "Rewriter::setProofNodeManager" << std::endl; // the rewriter is staticly determinstic, thus use static cache policy // for the term conversion proof generator d_tpg.reset(new TConvProofGenerator(pnm, @@ -182,6 +189,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node, TConvProofGenerator* tcpg) { + RewriteWithProofsAttribute rpfa; #ifdef CVC4_ASSERTIONS bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean()); @@ -195,7 +203,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, // Check if it's been cached already Node cached = getPostRewriteCache(theoryId, node); - if (!cached.isNull() && (tcpg == nullptr || tcpg->hasRewriteStep(node))) + if (!cached.isNull() && (tcpg == nullptr || node.getAttribute(rpfa))) { return cached; } @@ -232,7 +240,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, cached = getPreRewriteCache(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node); if (cached.isNull() - || (tcpg != nullptr && !tcpg->hasRewriteStep(rewriteStackTop.d_node))) + || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa))) { // Rewrite until fix-point is reached for(;;) { @@ -271,7 +279,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, rewriteStackTop.d_node); // If not, go through the children if (cached.isNull() - || (tcpg != nullptr && !tcpg->hasRewriteStep(rewriteStackTop.d_node))) + || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa))) { // The child we need to rewrite unsigned child = rewriteStackTop.d_nextChild++; @@ -355,6 +363,37 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, } // We're done with the post rewrite, so we add to the cache + if (tcpg != nullptr) + { + // if proofs are enabled, mark that we've rewritten with proofs + rewriteStackTop.d_original.setAttribute(rpfa, true); + if (!cached.isNull()) + { + // We may have gotten a different node, due to non-determinism in + // theory rewriters (e.g. quantifiers rewriter which introduces + // fresh BOUND_VARIABLE). This can happen if we wrote once without + // proofs and then rewrote again with proofs. + if (rewriteStackTop.d_node != cached) + { + Trace("rewriter-proof") << "WARNING: Rewritten forms with and " + "without proofs were not equivalent" + << std::endl; + Trace("rewriter-proof") + << " original: " << rewriteStackTop.d_original << std::endl; + Trace("rewriter-proof") + << "with proofs: " << rewriteStackTop.d_node << std::endl; + Trace("rewriter-proof") << " w/o proofs: " << cached << std::endl; + Node eq = rewriteStackTop.d_node.eqNode(cached); + tcpg->addRewriteStep(rewriteStackTop.d_node, + cached, + PfRule::TRUST_REWRITE, + {}, + {eq}); + // don't overwrite the cache, should be the same + rewriteStackTop.d_node = cached; + } + } + } setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(), rewriteStackTop.d_original, rewriteStackTop.d_node); @@ -443,11 +482,13 @@ RewriteResponse Rewriter::processTrustRewriteResponse( Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId); // add small step trusted rewrite NodeManager* nm = NodeManager::currentNM(); + Node rid = mkMethodId(isPre ? MethodId::RW_REWRITE_THEORY_PRE + : MethodId::RW_REWRITE_THEORY_POST); tcpg->addRewriteStep(proven[0], proven[1], PfRule::THEORY_REWRITE, {}, - {proven, tidn, nm->mkConst(isPre)}); + {proven, tidn, rid}); } else { diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index f38f3b174..e36426a81 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -83,15 +83,12 @@ class Rewriter { * to setProofNodeManager prior to this call. * * @param node The node to rewrite. - * @param elimTheoryRewrite Whether we also want fine-grained proofs for - * THEORY_REWRITE steps. * @param isExtEq Whether node is an equality which we are applying * rewriteEqualityExt on. * @return The trust node of kind TrustNodeKind::REWRITE that contains the * rewritten form of node. */ TrustNode rewriteWithProof(TNode node, - bool elimTheoryRewrite = false, bool isExtEq = false); /** Set proof node manager */ |