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

1 files changed, 11 insertions, 1 deletions

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;
 }