(proof-new) Add SMT proof manager (#5054)

This module is responsible for constructing the proof checker, proof node manager, and implementing dumping and checking of the final proof.

This PR includes setting up some connections into the various modules for proof production.

1 files changed, 103 insertions, 0 deletions

diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
new file mode 100644
index 000000000..925d9fa02
--- /dev/null
+++ b/src/smt/proof_manager.h
@@ -0,0 +1,103 @@
+/*********************                                                        */
+/*! \file proof_manager.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The proof manager of SmtEngine
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__PROOF_MANAGER_H
+#define CVC4__SMT__PROOF_MANAGER_H
+
+#include "context/cdlist.h"
+#include "expr/expr.h"
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+#include "expr/proof_node_manager.h"
+#include "smt/preprocess_proof_generator.h"
+#include "smt/proof_post_processor.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+
+namespace smt {
+
+class Assertions;
+
+/**
+ * This class is responsible for managing the proof output of SmtEngine, as
+ * well as setting up the global proof checker and proof node manager.
+ */
+class PfManager
+{
+ public:
+  PfManager(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.
+   *
+   * Throws an assertion failure if pg cannot provide a closed proof with
+   * respect to assertions in as.
+   */
+  void printProof(ProofGenerator* pg, Assertions& as);
+  /**
+   * Check proof, same as above, without printing.
+   */
+  void checkProof(ProofGenerator* pg, Assertions& as);
+
+  /**
+   * Get final proof.
+   *
+   * The argument pg is the module that can provide a proof for false in the
+   * current context.
+   */
+  std::shared_ptr<ProofNode> getFinalProof(ProofGenerator* pg, Assertions& as);
+  //--------------------------- access to utilities
+  /** Get a pointer to the ProofChecker owned by this. */
+  ProofChecker* getProofChecker() const;
+  /** Get a pointer to the ProofNodeManager owned by this. */
+  ProofNodeManager* getProofNodeManager() const;
+  /** Get the proof generator for proofs of preprocessing. */
+  smt::PreprocessProofGenerator* getPreprocessProofGenerator() const;
+  //--------------------------- 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.
+   */
+  void setFinalProof(ProofGenerator* pg, context::CDList<Node>* al);
+  /** The false node */
+  Node d_false;
+  /** For the new proofs module */
+  std::unique_ptr<ProofChecker> d_pchecker;
+  /** A proof node manager based on the above checker */
+  std::unique_ptr<ProofNodeManager> d_pnm;
+  /** The preprocess proof generator. */
+  std::unique_ptr<smt::PreprocessProofGenerator> d_pppg;
+  /** The proof post-processor */
+  std::unique_ptr<smt::ProofPostproccess> d_pfpp;
+  /**
+   * The final proof produced by the SMT engine.
+   * Combines the proofs of preprocessing, prop engine and theory engine, to be
+   * connected by setFinalProof().
+   */
+  std::shared_ptr<ProofNode> d_finalProof;
+}; /* class SmtEngine */
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__PROOF_MANAGER_H */