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

1 files changed, 18 insertions, 1 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a55428b55..bce086202 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -534,7 +534,13 @@ class CVC4_PUBLIC SmtEngine
 
   /** Print all instantiations made by the quantifiers module.  */
   void printInstantiations(std::ostream& out);
-
+  /**
+   * Print the current proof. This method should be called after an UNSAT
+   * response. It gets the proof of false from the PropEngine and passes
+   * it to the ProofManager, which post-processes the proof and prints it
+   * in the proper format.
+   */
+  void printProof();
   /**
    * Print solution for synthesis conjectures found by counter-example guided
    * instantiation module.
@@ -870,6 +876,9 @@ class CVC4_PUBLIC SmtEngine
   /** Set solver instance that owns this SmtEngine. */
   void setSolver(api::Solver* solver) { d_solver = solver; }
 
+  /** Get a pointer to the (new) PfManager owned by this SmtEngine. */
+  smt::PfManager* getPfManager() { return d_pfManager.get(); };
+
   /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
   StatisticsRegistry* getStatisticsRegistry()
   {
@@ -885,6 +894,14 @@ class CVC4_PUBLIC SmtEngine
   UnsatCore getUnsatCoreInternal();
 
   /**
+   * Check that a generated proof checks. This method is the same as printProof,
+   * but does not print the proof. Like that method, it should be called
+   * after an UNSAT response. It ensures that a well-formed proof of false
+   * can be constructed by the combination of the PropEngine and ProofManager.
+   */
+  void checkProof();
+
+  /**
    * Check that an unsatisfiable core is indeed unsatisfiable.
    */
   void checkUnsatCore();