diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-14 11:30:47 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-14 11:30:47 -0500 |
commit | c6e3264f83df54a886b28c14e2a911c176d89551 (patch) | |
tree | b4f6ca2f4c1cedf6752dbcc90cc1eec1543011df /src/theory/rewriter.h | |
parent | c13527bfa6b47ff4675b429b5e7bb7c6f43ff595 (diff) |
(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 <andres.noetzli@gmail.com>
Diffstat (limited to 'src/theory/rewriter.h')
-rw-r--r-- | src/theory/rewriter.h | 61 |
1 files changed, 58 insertions, 3 deletions
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(); @@ -58,6 +66,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. */ static void clearCaches(); @@ -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<ProofNodeManager> d_pnm; + /** The proof generator */ + std::unique_ptr<TConvProofGenerator> d_tpg; #ifdef CVC4_ASSERTIONS std::unique_ptr<std::unordered_set<Node, NodeHashFunction>> d_rewriteStack = nullptr; |