(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, 31 insertions, 11 deletions

diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index 1916f0162..be05fc2f7 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -17,6 +17,7 @@
 #ifndef CVC4__SMT__PROOF_MANAGER_H
 #define CVC4__SMT__PROOF_MANAGER_H
 
+#include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "expr/node.h"
 #include "expr/proof_checker.h"
@@ -32,6 +33,7 @@ class SmtEngine;
 namespace smt {
 
 class Assertions;
+class DefinedFunction;
 
 /**
  * This class is responsible for managing the proof output of SmtEngine, as
@@ -39,31 +41,41 @@ class Assertions;
  */
 class PfManager
 {
+  /** The type of our internal map of defined functions */
+  using DefinedFunctionMap =
+      context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>;
+
  public:
   PfManager(context::UserContext* u, SmtEngine* smte);
   ~PfManager();
   /**
    * Print the proof on the output channel of the current options in scope.
    *
-   * The argument pg is the module that can provide a proof for false in the
-   * current context.
+   * The argument pfn is the proof for false in the current context.
    *
    * Throws an assertion failure if pg cannot provide a closed proof with
-   * respect to assertions in as.
+   * respect to assertions in as and df. For the latter, entries in the defined
+   * function map correspond to equalities of the form (= f (lambda (...) t)),
+   * which are considered assertions in the final proof.
    */
-  void printProof(ProofGenerator* pg, Assertions& as);
+  void printProof(std::shared_ptr<ProofNode> pfn,
+                  Assertions& as,
+                  DefinedFunctionMap& df);
   /**
    * Check proof, same as above, without printing.
    */
-  void checkProof(ProofGenerator* pg, Assertions& as);
+  void checkProof(std::shared_ptr<ProofNode> pfn,
+                  Assertions& as,
+                  DefinedFunctionMap& df);
 
   /**
    * Get final proof.
    *
-   * The argument pg is the module that can provide a proof for false in the
-   * current context.
+   * The argument pfn is the proof for false in the current context.
    */
-  std::shared_ptr<ProofNode> getFinalProof(ProofGenerator* pg, Assertions& as);
+  std::shared_ptr<ProofNode> getFinalProof(std::shared_ptr<ProofNode> pfn,
+                                           Assertions& as,
+                                           DefinedFunctionMap& df);
   //--------------------------- access to utilities
   /** Get a pointer to the ProofChecker owned by this. */
   ProofChecker* getProofChecker() const;
@@ -74,10 +86,18 @@ class PfManager
   //--------------------------- end access to utilities
  private:
   /**
-   * Set final proof, which initializes d_finalProof to the proof of false
-   * from pg, postprocesses it, and stores it in d_finalProof.
+   * Set final proof, which initializes d_finalProof to the given proof node of
+   * false, postprocesses it, and stores it in d_finalProof.
+   */
+  void setFinalProof(std::shared_ptr<ProofNode> pfn,
+                     Assertions& as,
+                     DefinedFunctionMap& df);
+  /**
+   * Get assertions from the assertions
    */
-  void setFinalProof(ProofGenerator* pg, context::CDList<Node>* al);
+  void getAssertions(Assertions& as,
+                     DefinedFunctionMap& df,
+                     std::vector<Node>& assertions);
   /** The false node */
   Node d_false;
   /** For the new proofs module */