(proof-new) SMT Preprocess proof generator (#4708)

This adds the proof generator for storing proofs of preprocessing. It stores assertions added via preprocessing passes and their rewrites. This utility will eventually live in SmtEngine.

It also adds 2 new proof rules, and fixes an issue in ProofNodeUpdater.

4 files changed, 35 insertions, 1 deletions

diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
index 6e7cabccd..6a8244ce0 100644
--- a/src/theory/booleans/proof_checker.cpp
+++ b/src/theory/booleans/proof_checker.cpp
@@ -21,6 +21,7 @@ namespace booleans {
 void BoolProofRuleChecker::registerTo(ProofChecker* pc)
 {
   pc->registerChecker(PfRule::SPLIT, this);
+  pc->registerChecker(PfRule::EQ_RESOLVE, this);
   pc->registerChecker(PfRule::AND_ELIM, this);
   pc->registerChecker(PfRule::AND_INTRO, this);
   pc->registerChecker(PfRule::NOT_OR_ELIM, this);
@@ -74,6 +75,16 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
     return NodeManager::currentNM()->mkNode(
         kind::OR, args[0], args[0].notNode());
   }
+  if (id == PfRule::EQ_RESOLVE)
+  {
+    Assert(children.size() == 2);
+    Assert(args.empty());
+    if (children[1].getKind() != kind::EQUAL || children[0] != children[1][0])
+    {
+      return Node::null();
+    }
+    return children[1][1];
+  }
   // natural deduction rules
   if (id == PfRule::AND_ELIM)
   {
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index f6b41104a..a8249ae7c 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -59,6 +59,7 @@ 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::PREPROCESS, this);
 }
 
 Node BuiltinProofRuleChecker::applySubstitutionRewrite(
@@ -309,6 +310,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
     }
     return args[0];
   }
+  else if (id == PfRule::PREPROCESS)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 1);
+    return args[0];
+  }
   // no rule
   return Node::null();
 }
diff --git a/src/theory/trust_node.cpp b/src/theory/trust_node.cpp
index af2d60241..25aef5a72 100644
--- a/src/theory/trust_node.cpp
+++ b/src/theory/trust_node.cpp
@@ -96,10 +96,20 @@ Node TrustNode::getNode() const
 }
 
 Node TrustNode::getProven() const { return d_proven; }
+
 ProofGenerator* TrustNode::getGenerator() const { return d_gen; }
 
 bool TrustNode::isNull() const { return d_proven.isNull(); }
 
+std::shared_ptr<ProofNode> TrustNode::toProofNode()
+{
+  if (d_gen == nullptr)
+  {
+    return nullptr;
+  }
+  return d_gen->getProofFor(d_proven);
+}
+
 Node TrustNode::getConflictProven(Node conf) { return conf.notNode(); }
 
 Node TrustNode::getLemmaProven(Node lem) { return lem; }
@@ -113,7 +123,7 @@ Node TrustNode::getRewriteProven(TNode n, Node nr) { return n.eqNode(nr); }
 
 std::ostream& operator<<(std::ostream& out, TrustNode n)
 {
-  out << "(trust " << n.getNode() << ")";
+  out << "(" << n.getKind() << " " << n.getProven() << ")";
   return out;
 }
 
diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h
index a3c0fbec5..ff174b63e 100644
--- a/src/theory/trust_node.h
+++ b/src/theory/trust_node.h
@@ -18,6 +18,7 @@
 #define CVC4__THEORY__TRUST_NODE_H
 
 #include "expr/node.h"
+#include "expr/proof_node.h"
 
 namespace CVC4 {
 
@@ -127,6 +128,11 @@ class TrustNode
   ProofGenerator* getGenerator() const;
   /** is null? */
   bool isNull() const;
+  /**
+   * Gets the proof node for this trust node, which is obtained by
+   * calling the generator's getProofFor method on the proven node.
+   */
+  std::shared_ptr<ProofNode> toProofNode();
 
   /** Get the proven formula corresponding to a conflict call */
   static Node getConflictProven(Node conf);