From c6e3264f83df54a886b28c14e2a911c176d89551 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 14 Jul 2020 11:30:47 -0500
Subject: (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>
---
 src/theory/theory_rewriter.h | 52 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)

(limited to 'src/theory/theory_rewriter.h')

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
-- 
cgit v1.2.3