diff options
| -rw-r--r-- | src/expr/proof_rule.cpp | 4 | ||||
| -rw-r--r-- | src/expr/proof_rule.h | 39 | ||||
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 68 | ||||
| -rw-r--r-- | src/theory/builtin/proof_checker.h | 40 | ||||
| -rw-r--r-- | src/theory/rewriter.cpp | 20 | ||||
| -rw-r--r-- | 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<Node>& 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<Node>& args, } } +bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid) +{ + uint32_t i; + if (!getUInt32(n, i)) + { + return false; + } + tid = static_cast<TheoryId>(i); + return true; +} + +Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid) +{ + return NodeManager::currentNM()->mkConst( + Rational(static_cast<uint32_t>(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<Node>& exp, - MethodId ids = MethodId::SB_DEFAULT, - MethodId idr = MethodId::RW_REWRITE); + Node applySubstitutionRewrite(Node n, + const std::vector<Node>& 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<Node>& 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<Node>& children, const std::vector<Node>& 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<ProofNodeManager> d_pnm; /** The proof generator */ std::unique_ptr<TConvProofGenerator> d_tpg; #ifdef CVC4_ASSERTIONS |