(proof-new) Updates to SMT proof manager and SmtEngine (#5446)

This PR adds infrastructure in SmtEngine and ProofManager for checking and printing proofs. It updates a previous interface that used ProofGenerator in favor of ProofNode.

This makes it so that it only remains to make PropEngine to be proof producing.

2 files changed, 13 insertions, 0 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 4596972e9..26d1e615b 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -353,5 +353,11 @@ bool PropEngine::properExplanation(TNode node, TNode expl) const {
   return true;
 }
 
+std::shared_ptr<ProofNode> PropEngine::getProof()
+{
+  // TODO (proj #37) implement this
+  return nullptr;
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 1fb79231d..e4d536c29 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -219,6 +219,13 @@ class PropEngine
    */
   bool properExplanation(TNode node, TNode expl) const;
 
+  /**
+   * Return the prop engine proof. This should be called only when proofs are
+   * enabled. Returns a proof of false whose free assumptions are the
+   * preprocessed assertions.
+   */
+  std::shared_ptr<ProofNode> getProof();
+
  private:
   /** Dump out the satisfying assignment (after SAT result) */
   void printSatisfyingAssignment();