From c6e3264f83df54a886b28c14e2a911c176d89551 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 14 Jul 2020 11:30:47 -0500 Subject: [PATCH] (proof-new) Skeleton proof support in the Rewriter (#4730) This adds support for skeleton proofs in the rewriter (REWRITE -> THEORY_REWRITE). It adds "extended equality rewrite" as a new method of the rewriter/theory rewriters. The unit test of this feature should be added on a followup PR. Co-authored-by: Andres Noetzli --- src/CMakeLists.txt | 1 + src/expr/proof_rule.cpp | 1 + src/expr/proof_rule.h | 9 ++ src/theory/builtin/proof_checker.cpp | 11 ++ src/theory/builtin/proof_checker.h | 11 ++ src/theory/rewriter.cpp | 131 +++++++++++++++++++++--- src/theory/rewriter.h | 61 ++++++++++- src/theory/strings/sequences_rewriter.h | 2 +- src/theory/theory_rewriter.cpp | 63 ++++++++++++ src/theory/theory_rewriter.h | 52 ++++++++++ 10 files changed, 322 insertions(+), 20 deletions(-) create mode 100644 src/theory/theory_rewriter.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 930bf2370..278632a90 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -771,6 +771,7 @@ libcvc4_add_sources( theory/theory_preprocessor.h theory/theory_proof_step_buffer.cpp theory/theory_proof_step_buffer.h + theory/theory_rewriter.cpp theory/theory_rewriter.h theory/theory_registrar.h theory/theory_test_utils.h diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 08998e66e..c9250f9ea 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -31,6 +31,7 @@ const char* toString(PfRule id) 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::PREPROCESS: return "PREPROCESS"; //================================================= Boolean rules case PfRule::SPLIT: return "SPLIT"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 87e8565ca..e7464dd24 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -163,6 +163,15 @@ 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 // ======== Preprocess diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index a8249ae7c..59f405337 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -59,9 +59,20 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this); pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this); pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this); + pc->registerChecker(PfRule::THEORY_REWRITE, this); pc->registerChecker(PfRule::PREPROCESS, this); } +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) { diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 6dc7023d5..7e46587b7 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -76,6 +76,17 @@ class BuiltinProofRuleChecker : public ProofRuleChecker * @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); /** * Get substitution. Updates vars/subs to the substitution specified by * exp (e.g. as an equality) for the substitution method ids. diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 0247a7277..d77f6fe83 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -70,7 +70,8 @@ struct RewriteStackElement { /** The node we're currently rewriting */ Node d_node; - /** Original node */ + /** Original node (either the unrewritten node or the node after prerewriting) + */ Node d_original; /** Id of the theory that's currently rewriting this node */ unsigned d_theoryId : 8; @@ -97,6 +98,41 @@ Node Rewriter::rewrite(TNode node) { return getInstance()->rewriteTo(theoryOf(node), node); } +TrustNode Rewriter::rewriteWithProof(TNode node, + bool elimTheoryRewrite, + bool isExtEq) +{ + // must set the proof checker before calling this + Assert(d_tpg != nullptr); + if (isExtEq) + { + // theory rewriter is responsible for rewriting the equality + TheoryRewriter* tr = getInstance()->d_theoryRewriters[theoryOf(node)]; + Assert(tr != nullptr); + return tr->rewriteEqualityExtWithProof(node); + } + Node ret = getInstance()->rewriteTo(theoryOf(node), node, d_tpg.get()); + return TrustNode::mkTrustRewrite(node, ret, d_tpg.get()); +} + +void Rewriter::setProofChecker(ProofChecker* pc) +{ + // 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())); + } +} + +Node Rewriter::rewriteEqualityExt(TNode node) +{ + Assert(node.getKind() == kind::EQUAL); + // note we don't force caching of this method currently + return getInstance()->d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt( + node); +} + void Rewriter::registerTheoryRewriter(theory::TheoryId tid, TheoryRewriter* trew) { @@ -136,8 +172,10 @@ Rewriter* Rewriter::getInstance() return smt::currentSmtEngine()->getRewriter(); } -Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { - +Node Rewriter::rewriteTo(theory::TheoryId theoryId, + Node node, + TConvProofGenerator* tcpg) +{ #ifdef CVC4_ASSERTIONS bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean()); @@ -151,7 +189,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Check if it's been cached already Node cached = getPostRewriteCache(theoryId, node); - if (!cached.isNull()) { + if (!cached.isNull() && (tcpg == nullptr || tcpg->hasRewriteStep(node))) + { return cached; } @@ -186,12 +225,15 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Check if the pre-rewrite has already been done (it's in the cache) cached = getPreRewriteCache(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node); - if (cached.isNull()) { + if (cached.isNull() + || (tcpg != nullptr && !tcpg->hasRewriteStep(rewriteStackTop.d_node))) + { // Rewrite until fix-point is reached for(;;) { // Perform the pre-rewrite - RewriteResponse response = - preRewrite(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node); + RewriteResponse response = preRewrite( + rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg); + // Put the rewritten node to the top of the stack rewriteStackTop.d_node = response.d_node; TheoryId newTheory = theoryOf(rewriteStackTop.d_node); @@ -203,6 +245,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { } rewriteStackTop.d_theoryId = newTheory; } + // Cache the rewrite setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(), rewriteStackTop.d_original, @@ -221,8 +264,9 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { cached = getPostRewriteCache(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node); // If not, go through the children - if(cached.isNull()) { - + if (cached.isNull() + || (tcpg != nullptr && !tcpg->hasRewriteStep(rewriteStackTop.d_node))) + { // The child we need to rewrite unsigned child = rewriteStackTop.d_nextChild++; @@ -261,8 +305,9 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Done with all pre-rewriting, so let's do the post rewrite for(;;) { // Do the post-rewrite - RewriteResponse response = - postRewrite(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node); + RewriteResponse response = postRewrite( + rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg); + // We continue with the response we got TheoryId newTheoryId = theoryOf(response.d_node); if (newTheoryId != rewriteStackTop.getTheoryId() @@ -276,7 +321,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { == d_rewriteStack->end()); d_rewriteStack->insert(response.d_node); #endif - Node rewritten = rewriteTo(newTheoryId, response.d_node); + Node rewritten = rewriteTo(newTheoryId, response.d_node, tcpg); rewriteStackTop.d_node = rewritten; #ifdef CVC4_ASSERTIONS d_rewriteStack->erase(response.d_node); @@ -301,11 +346,14 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { != rewriteStackTop.d_node); rewriteStackTop.d_node = response.d_node; } + // We're done with the post rewrite, so we add to the cache setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(), rewriteStackTop.d_original, rewriteStackTop.d_node); - } else { + } + else + { // We were already in cache, so just remember it rewriteStackTop.d_node = cached; rewriteStackTop.d_theoryId = theoryOf(cached); @@ -324,32 +372,83 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { } Unreachable(); -}/* Rewriter::rewriteTo() */ +} /* Rewriter::rewriteTo() */ -RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId, TNode n) +RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId, + TNode n, + TConvProofGenerator* tcpg) { Kind k = n.getKind(); std::function fn = (k == kind::EQUAL) ? d_preRewritersEqual[theoryId] : d_preRewriters[k]; if (fn == nullptr) { + if (tcpg != nullptr) + { + // call the trust rewrite response interface + TrustRewriteResponse tresponse = + 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 d_theoryRewriters[theoryId]->preRewrite(n); } return fn(&d_re, n); } -RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId, TNode n) +RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId, + TNode n, + TConvProofGenerator* tcpg) { Kind k = n.getKind(); std::function fn = (k == kind::EQUAL) ? d_postRewritersEqual[theoryId] : d_postRewriters[k]; if (fn == nullptr) { + if (tcpg != nullptr) + { + // same as above, for post-rewrite + TrustRewriteResponse tresponse = + d_theoryRewriters[theoryId]->postRewriteWithProof(n); + return processTrustRewriteResponse(tresponse, false, tcpg); + } return d_theoryRewriters[theoryId]->postRewrite(n); } return fn(&d_re, n); } +RewriteResponse Rewriter::processTrustRewriteResponse( + const TrustRewriteResponse& tresponse, + bool isPre, + TConvProofGenerator* tcpg) +{ + Assert(tcpg != nullptr); + TrustNode trn = tresponse.d_node; + Assert(trn.getKind() == TrustNodeKind::REWRITE); + Node proven = trn.getProven(); + if (proven[0] != proven[1]) + { + ProofGenerator* pg = trn.getGenerator(); + if (pg == nullptr) + { + // add small step trusted rewrite + NodeManager* nm = NodeManager::currentNM(); + tcpg->addRewriteStep(proven[0], + proven[1], + PfRule::THEORY_REWRITE, + {}, + {proven[0], nm->mkConst(isPre)}); + } + else + { + // store proven rewrite step + tcpg->addRewriteStep(proven[0], proven[1], pg); + } + } + return RewriteResponse(tresponse.d_status, trn.getNode()); +} + void Rewriter::clearCaches() { Rewriter* rewriter = getInstance(); diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index e021ac9e7..c57844f23 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -19,12 +19,18 @@ #pragma once #include "expr/node.h" +#include "expr/term_conversion_proof_generator.h" #include "theory/theory_rewriter.h" +#include "theory/trust_node.h" #include "util/unsafe_interrupt_exception.h" namespace CVC4 { namespace theory { +namespace builtin { +class BuiltinProofRuleChecker; +} + class RewriterInitializer; /** @@ -48,6 +54,8 @@ RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n); * The main rewriter class. */ class Rewriter { + friend builtin::BuiltinProofRuleChecker; + public: Rewriter(); @@ -57,6 +65,38 @@ class Rewriter { */ static Node rewrite(TNode node); + /** + * Rewrites the equality node using theoryOf() to determine which rewriter to + * use on the node corresponding to an equality s = t. + * + * Specifically, this method performs rewrites whose conclusion is not + * necessarily one of { s = t, t = s, true, false }, which is an invariant + * guaranted by the above method. This invariant is motivated by theory + * combination, which needs to guarantee that equalities between terms + * can be communicated for all pairs of terms. + */ + static Node rewriteEqualityExt(TNode node); + + /** + * 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. + * + * @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 checker */ + void setProofChecker(ProofChecker* pc); + /** * Garbage collects the rewrite caches. */ @@ -134,13 +174,24 @@ class Rewriter { /** * Rewrites the node using the given theory rewriter. */ - Node rewriteTo(theory::TheoryId theoryId, Node node); + Node rewriteTo(theory::TheoryId theoryId, + Node node, + TConvProofGenerator* tcpg = nullptr); /** Calls the pre-rewriter for the given theory */ - RewriteResponse preRewrite(theory::TheoryId theoryId, TNode n); + RewriteResponse preRewrite(theory::TheoryId theoryId, + TNode n, + TConvProofGenerator* tcpg = nullptr); /** Calls the post-rewriter for the given theory */ - RewriteResponse postRewrite(theory::TheoryId theoryId, TNode n); + RewriteResponse postRewrite(theory::TheoryId theoryId, + TNode n, + TConvProofGenerator* tcpg = nullptr); + /** processes a trust rewrite response */ + RewriteResponse processTrustRewriteResponse( + const TrustRewriteResponse& tresponse, + bool isPre, + TConvProofGenerator* tcpg); /** * Calls the equality-rewriter for the given theory. @@ -175,6 +226,10 @@ 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 std::unique_ptr> d_rewriteStack = nullptr; diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 3251579ff..47a20a7ca 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -145,7 +145,7 @@ class SequencesRewriter : public TheoryRewriter * Specifically, this function performs rewrites whose conclusion is not * necessarily one of { s = t, t = s, true, false }. */ - Node rewriteEqualityExt(Node node); + Node rewriteEqualityExt(Node node) override; /** rewrite string length * This is the entry point for post-rewriting terms node of the form * str.len( t ) diff --git a/src/theory/theory_rewriter.cpp b/src/theory/theory_rewriter.cpp new file mode 100644 index 000000000..a8dfbb2bb --- /dev/null +++ b/src/theory/theory_rewriter.cpp @@ -0,0 +1,63 @@ +/********************* */ +/*! \file theory_rewriter.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The TheoryRewriter class + ** + ** The TheoryRewriter class is the interface that theory rewriters implement. + **/ + +#include "theory/theory_rewriter.h" + +namespace CVC4 { +namespace theory { + +TrustRewriteResponse::TrustRewriteResponse(RewriteStatus status, + Node n, + Node nr, + ProofGenerator* pg) + : d_status(status) +{ + // we always make non-null, regardless of whether n = nr + d_node = TrustNode::mkTrustRewrite(n, nr, pg); +} + +TrustRewriteResponse TheoryRewriter::postRewriteWithProof(TNode node) +{ + RewriteResponse response = postRewrite(node); + // by default, we return a trust rewrite response with no proof generator + return TrustRewriteResponse( + response.d_status, node, response.d_node, nullptr); +} + +TrustRewriteResponse TheoryRewriter::preRewriteWithProof(TNode node) +{ + RewriteResponse response = preRewrite(node); + // by default, we return a trust rewrite response with no proof generator + return TrustRewriteResponse( + response.d_status, node, response.d_node, nullptr); +} + +Node TheoryRewriter::rewriteEqualityExt(Node node) { return node; } + +TrustNode TheoryRewriter::rewriteEqualityExtWithProof(Node node) +{ + Node nodeRew = rewriteEqualityExt(node); + if (nodeRew != node) + { + // by default, we return a trust rewrite response with no proof generator + return TrustNode::mkTrustRewrite(node, nodeRew, nullptr); + } + // no rewrite + return TrustNode::null(); +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/theory_rewriter.h b/src/theory/theory_rewriter.h index 4a9c8d14f..cabfad2fc 100644 --- a/src/theory/theory_rewriter.h +++ b/src/theory/theory_rewriter.h @@ -20,6 +20,7 @@ #define CVC4__THEORY__THEORY_REWRITER_H #include "expr/node.h" +#include "theory/trust_node.h" namespace CVC4 { namespace theory { @@ -53,6 +54,21 @@ struct RewriteResponse RewriteResponse(RewriteStatus status, Node n) : d_status(status), d_node(n) {} }; /* struct RewriteResponse */ +/** Same as above, with trust node instead of node. */ +struct TrustRewriteResponse +{ + TrustRewriteResponse(RewriteStatus status, + Node n, + Node nr, + ProofGenerator* pg); + /** The status of the rewrite */ + const RewriteStatus d_status; + /** + * The trust node corresponding to the rewrite. + */ + TrustNode d_node; +}; + /** * The interface that a theory rewriter has to implement. * @@ -79,12 +95,48 @@ class TheoryRewriter */ virtual RewriteResponse postRewrite(TNode node) = 0; + /** + * Performs a pre-rewrite step, with proofs. + * + * @param node The node to rewrite + */ + virtual TrustRewriteResponse postRewriteWithProof(TNode node); + /** * Performs a post-rewrite step. * * @param node The node to rewrite */ virtual RewriteResponse preRewrite(TNode node) = 0; + + /** + * Performs a pre-rewrite step, with proofs. + * + * @param node The node to rewrite + */ + virtual TrustRewriteResponse preRewriteWithProof(TNode node); + + /** rewrite equality extended + * + * This method returns a formula that is equivalent to the equality between + * two terms s = t, given by node. + * + * Specifically, this method performs rewrites whose conclusion is not + * necessarily one of { s = t, t = s, true, false }. This is in constrast + * to postRewrite and preRewrite above, where the rewritten form of an + * equality must be one of these. + * + * @param node The node to rewrite + */ + virtual Node rewriteEqualityExt(Node node); + + /** rewrite equality extended, with proofs + * + * @param node The node to rewrite + * @return A trust node of kind TrustNodeKind::REWRITE, or the null trust + * node if no rewrites are applied. + */ + virtual TrustNode rewriteEqualityExtWithProof(Node node); }; } // namespace theory -- 2.30.2