From f9a4549c3dab3cd91f0d9973b24b7891048ed1d9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Sep 2020 14:32:24 -0500 Subject: [PATCH] (proof-new) Updates to builtin proof checker (#4962) This includes support for some trusted rules (whose use is to come). It also modifies THEORY_REWRITE so that it is a "trusted" rule, that is, it is not re-checked. The reason for this is that TheoryRewriter is not deterministic. An example of non-determinism in TheoryRewriter are rules that introduce bound variables (e.g. quantifiers rewriter) since these bound variables are fresh each time it is invoked. Non-deterministic theory rewriters cannot be rechecked, which was leading to failures on proof-new at proof check time. The other way to fix this would be to cache TheoryRewriter responses, but then the checker would only be verifying that the caching was being done properly. This is not worthwhile. --- src/expr/proof_rule.cpp | 4 +- src/expr/proof_rule.h | 39 ++++++++++++---- src/theory/builtin/proof_checker.cpp | 68 +++++++++++++++++++++------- src/theory/builtin/proof_checker.h | 40 ++++++++-------- src/theory/rewriter.cpp | 20 +++++--- src/theory/rewriter.h | 9 ++-- 6 files changed, 124 insertions(+), 56 deletions(-) diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index bd58fc787..1d46b183f 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -27,13 +27,15 @@ const char* toString(PfRule id) case PfRule::SCOPE: return "SCOPE"; case PfRule::SUBS: return "SUBS"; case PfRule::REWRITE: return "REWRITE"; + case PfRule::EVALUATE: return "EVALUATE"; case PfRule::MACRO_SR_EQ_INTRO: return "MACRO_SR_EQ_INTRO"; case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO"; case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM"; case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM"; - case PfRule::THEORY_REWRITE: return "THEORY_REWRITE"; case PfRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM"; //================================================= Trusted rules + case PfRule::THEORY_LEMMA: return "THEORY_LEMMA"; + case PfRule::THEORY_REWRITE: return "THEORY_REWRITE"; case PfRule::PREPROCESS: return "PREPROCESS"; case PfRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA"; case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index b6b9f1ea8..825503d5d 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -91,6 +91,14 @@ enum class PfRule : uint32_t // where idr is a MethodId identifier, which determines the kind of rewriter // to apply, e.g. Rewriter::rewrite. REWRITE, + // ======== Evaluate + // Children: none + // Arguments: (t) + // ---------------------------------------- + // Conclusion: (= t Evaluator::evaluate(t)) + // Note this is equivalent to: + // (REWRITE t MethodId::RW_EVALUATE) + EVALUATE, // ======== Substitution + Rewriting equality introduction // // In this rule, we provide a term t and conclude that it is equal to its @@ -163,15 +171,6 @@ enum class PfRule : uint32_t // Notice that we apply rewriting on the witness form of F and G, similar to // MACRO_SR_PRED_INTRO. MACRO_SR_PRED_TRANSFORM, - // ======== Theory Rewrite - // Children: none - // Arguments: (t, preRewrite?) - // ---------------------------------------- - // Conclusion: (= t t') - // where - // t' is the result of applying either a pre-rewrite or a post-rewrite step - // to t (depending on the second argument). - THEORY_REWRITE, //================================================= Processing rules // ======== Remove Term Formulas Axiom @@ -182,6 +181,28 @@ enum class PfRule : uint32_t REMOVE_TERM_FORMULA_AXIOM, //================================================= Trusted rules + // ======== Theory lemma + // Children: none + // Arguments: (F, tid) + // --------------------------------------------------------------- + // Conclusion: F + // where F is a (T-valid) theory lemma generated by theory with TheoryId tid. + // This is a "coarse-grained" rule that is used as a placeholder if a theory + // did not provide a proof for a lemma or conflict. + THEORY_LEMMA, + // ======== Theory Rewrite + // Children: none + // Arguments: (F, tid, preRewrite?) + // ---------------------------------------- + // 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. + THEORY_REWRITE, // The rules in this section have the signature of a "trusted rule": // // Children: none diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 7521d116e..cf27b516e 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -16,6 +16,7 @@ #include "expr/skolem_manager.h" #include "smt/term_formula_removal.h" +#include "theory/evaluator.h" #include "theory/rewriter.h" #include "theory/theory.h" @@ -29,6 +30,9 @@ const char* toString(MethodId id) switch (id) { case MethodId::RW_REWRITE: return "RW_REWRITE"; + case MethodId::RW_EXT_REWRITE: return "RW_EXT_REWRITE"; + 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::SB_DEFAULT: return "SB_DEFAULT"; case MethodId::SB_LITERAL: return "SB_LITERAL"; @@ -56,6 +60,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::SCOPE, this); pc->registerChecker(PfRule::SUBS, this); pc->registerChecker(PfRule::REWRITE, this); + pc->registerChecker(PfRule::EVALUATE, this); pc->registerChecker(PfRule::MACRO_SR_EQ_INTRO, this); pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this); pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this); @@ -63,6 +68,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::THEORY_REWRITE, this); pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this); // trusted rules + pc->registerTrustedChecker(PfRule::THEORY_LEMMA, this, 1); pc->registerTrustedChecker(PfRule::PREPROCESS, this, 2); pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 2); pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 2); @@ -70,16 +76,6 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 2); } -Node BuiltinProofRuleChecker::applyTheoryRewrite(Node n, bool preRewrite) -{ - TheoryId tid = Theory::theoryOf(n); - Rewriter* rewriter = Rewriter::getInstance(); - Node nkr = preRewrite ? rewriter->preRewrite(tid, n).d_node - : rewriter->postRewrite(tid, n).d_node; - return nkr; -} - - Node BuiltinProofRuleChecker::applySubstitutionRewrite( Node n, const std::vector& exp, MethodId ids, MethodId idr) { @@ -95,7 +91,20 @@ Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr) { return Rewriter::rewrite(n); } - else if (idr == MethodId::RW_IDENTITY) + if (idr == MethodId::RW_EXT_REWRITE) + { + return d_ext_rewriter.extendedRewrite(n); + } + if (idr == MethodId::RW_REWRITE_EQ_EXT) + { + return Rewriter::rewriteEqualityExt(n); + } + if (idr == MethodId::RW_EVALUATE) + { + Evaluator eval; + return eval.eval(n, {}, {}, false); + } + if (idr == MethodId::RW_IDENTITY) { // does nothing return n; @@ -228,7 +237,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, { exp.push_back(children[i]); } - Node res = applySubstitution(args[0], exp); + Node res = applySubstitution(args[0], exp, ids); return args[0].eqNode(res); } else if (id == PfRule::REWRITE) @@ -243,6 +252,13 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, Node res = applyRewrite(args[0], idr); return args[0].eqNode(res); } + else if (id == PfRule::EVALUATE) + { + Assert(children.empty()); + Assert(args.size() == 1); + Node res = applyRewrite(args[0], MethodId::RW_EVALUATE); + return args[0].eqNode(res); + } else if (id == PfRule::MACRO_SR_EQ_INTRO) { Assert(1 <= args.size() && args.size() <= 3); @@ -334,13 +350,14 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, Assert(args.size() == 1); return RemoveTermFormulas::getAxiomFor(args[0]); } - else if (id == PfRule::PREPROCESS || id == PfRule::PREPROCESS_LEMMA - || id == PfRule::THEORY_PREPROCESS - || id == PfRule::THEORY_PREPROCESS_LEMMA - || id == PfRule::WITNESS_AXIOM) + else if (id == PfRule::PREPROCESS || id == PfRule::THEORY_PREPROCESS + || id == PfRule::WITNESS_AXIOM || id == PfRule::THEORY_LEMMA + || id == PfRule::PREPROCESS_LEMMA || id == PfRule::THEORY_REWRITE) { + // "trusted" rules Assert(children.empty()); - Assert(args.size() == 1); + Assert(!args.empty()); + Assert(args[0].getType().isBoolean()); return args[0]; } // no rule @@ -390,6 +407,23 @@ void BuiltinProofRuleChecker::addMethodIds(std::vector& args, } } +bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid) +{ + uint32_t i; + if (!getUInt32(n, i)) + { + return false; + } + tid = static_cast(i); + return true; +} + +Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid) +{ + return NodeManager::currentNM()->mkConst( + Rational(static_cast(tid))); +} + } // namespace builtin } // namespace theory } // namespace CVC4 diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 7e46587b7..3251b4e9e 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -20,11 +20,12 @@ #include "expr/node.h" #include "expr/proof_checker.h" #include "expr/proof_node.h" +#include "theory/quantifiers/extended_rewrite.h" namespace CVC4 { namespace theory { -/** +/** * Identifiers for rewriters and substitutions, which we abstractly * classify as "methods". Methods have a unique identifier in the internal * proof calculus implemented by the checker below. @@ -41,6 +42,12 @@ enum class MethodId : uint32_t //---------------------------- Rewriters // Rewriter::rewrite(n) RW_REWRITE, + // d_ext_rew.extendedRewrite(n); + RW_EXT_REWRITE, + // Rewriter::rewriteExtEquality(n) + RW_REWRITE_EQ_EXT, + // Evaluator::evaluate(n) + RW_EVALUATE, // identity RW_IDENTITY, //---------------------------- Substitutions @@ -75,21 +82,10 @@ class BuiltinProofRuleChecker : public ProofRuleChecker * specifying a call to Rewriter::rewrite. * @return The rewritten form of n. */ - static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE); - /** - * Apply small-step rewrite on n in skolem form (either pre- or - * post-rewrite). This encapsulates the exact behavior of a THEORY_REWRITE - * step in a proof. - * - * @param n The node to rewrite - * @param preRewrite If true, performs a pre-rewrite or a post-rewrite - * otherwise - * @return The rewritten form of n - */ - static Node applyTheoryRewrite(Node n, bool preRewrite); + Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE); /** * Get substitution. Updates vars/subs to the substitution specified by - * exp (e.g. as an equality) for the substitution method ids. + * exp for the substitution method ids. */ static bool getSubstitution(Node exp, TNode& var, @@ -123,10 +119,10 @@ class BuiltinProofRuleChecker : public ProofRuleChecker * @param idr The method identifier of the rewriter. * @return The substituted, rewritten form of n. */ - static Node applySubstitutionRewrite(Node n, - const std::vector& exp, - MethodId ids = MethodId::SB_DEFAULT, - MethodId idr = MethodId::RW_REWRITE); + Node applySubstitutionRewrite(Node n, + const std::vector& exp, + MethodId ids = MethodId::SB_DEFAULT, + MethodId idr = MethodId::RW_REWRITE); /** get a method identifier from a node, return false if we fail */ static bool getMethodId(TNode n, MethodId& i); /** @@ -144,6 +140,11 @@ class BuiltinProofRuleChecker : public ProofRuleChecker */ static void addMethodIds(std::vector& args, MethodId ids, MethodId idr); + /** get a TheoryId from a node, return false if we fail */ + static bool getTheoryId(TNode n, TheoryId& tid); + /** Make a TheoryId into a node */ + static Node mkTheoryIdNode(TheoryId tid); + /** Register all rules owned by this rule checker into pc. */ void registerTo(ProofChecker* pc) override; protected: @@ -151,6 +152,9 @@ class BuiltinProofRuleChecker : public ProofRuleChecker Node checkInternal(PfRule id, const std::vector& children, const std::vector& args) override; + + /** extended rewriter object */ + quantifiers::ExtendedRewriter d_ext_rewriter; }; } // namespace builtin diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index f2e13d1e0..9238525dc 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -21,6 +21,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "theory/builtin/proof_checker.h" #include "theory/rewriter_tables.h" #include "theory/theory.h" #include "util/resource_manager.h" @@ -115,13 +116,18 @@ TrustNode Rewriter::rewriteWithProof(TNode node, return TrustNode::mkTrustRewrite(node, ret, d_tpg.get()); } -void Rewriter::setProofChecker(ProofChecker* pc) +void Rewriter::setProofNodeManager(ProofNodeManager* pnm) { // if not already initialized with proof support if (d_tpg == nullptr) { - d_pnm.reset(new ProofNodeManager(pc)); - d_tpg.reset(new TConvProofGenerator(d_pnm.get())); + // the rewriter is staticly determinstic, thus use static cache policy + // for the term conversion proof generator + d_tpg.reset(new TConvProofGenerator(pnm, + nullptr, + TConvPolicy::FIXPOINT, + TConvCachePolicy::STATIC, + "Rewriter::TConvProofGenerator")); } } @@ -391,7 +397,7 @@ RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId, d_theoryRewriters[theoryId]->preRewriteWithProof(n); // process the trust rewrite response: store the proof step into // tcpg if necessary and then convert to rewrite response. - return processTrustRewriteResponse(tresponse, true, tcpg); + return processTrustRewriteResponse(theoryId, tresponse, true, tcpg); } return d_theoryRewriters[theoryId]->preRewrite(n); } @@ -412,7 +418,7 @@ RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId, // same as above, for post-rewrite TrustRewriteResponse tresponse = d_theoryRewriters[theoryId]->postRewriteWithProof(n); - return processTrustRewriteResponse(tresponse, false, tcpg); + return processTrustRewriteResponse(theoryId, tresponse, false, tcpg); } return d_theoryRewriters[theoryId]->postRewrite(n); } @@ -420,6 +426,7 @@ RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId, } RewriteResponse Rewriter::processTrustRewriteResponse( + theory::TheoryId theoryId, const TrustRewriteResponse& tresponse, bool isPre, TConvProofGenerator* tcpg) @@ -433,13 +440,14 @@ RewriteResponse Rewriter::processTrustRewriteResponse( ProofGenerator* pg = trn.getGenerator(); if (pg == nullptr) { + Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId); // add small step trusted rewrite NodeManager* nm = NodeManager::currentNM(); tcpg->addRewriteStep(proven[0], proven[1], PfRule::THEORY_REWRITE, {}, - {proven[0], nm->mkConst(isPre)}); + {proven, tidn, nm->mkConst(isPre)}); } else { diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index c57844f23..113749a75 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -80,7 +80,7 @@ class Rewriter { /** * Rewrite with proof production, which is managed by the term conversion * proof generator managed by this class (d_tpg). This method requires a call - * to setProofChecker prior to this call. + * to setProofNodeManager prior to this call. * * @param node The node to rewrite. * @param elimTheoryRewrite Whether we also want fine-grained proofs for @@ -94,8 +94,8 @@ class Rewriter { bool elimTheoryRewrite = false, bool isExtEq = false); - /** Set proof checker */ - void setProofChecker(ProofChecker* pc); + /** Set proof node manager */ + void setProofNodeManager(ProofNodeManager* pnm); /** * Garbage collects the rewrite caches. @@ -189,6 +189,7 @@ class Rewriter { TConvProofGenerator* tcpg = nullptr); /** processes a trust rewrite response */ RewriteResponse processTrustRewriteResponse( + theory::TheoryId theoryId, const TrustRewriteResponse& tresponse, bool isPre, TConvProofGenerator* tcpg); @@ -226,8 +227,6 @@ class Rewriter { RewriteEnvironment d_re; - /** The proof node manager */ - std::unique_ptr d_pnm; /** The proof generator */ std::unique_ptr d_tpg; #ifdef CVC4_ASSERTIONS -- 2.30.2