(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>

1 files changed, 63 insertions, 0 deletions

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