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

11 files changed, 343 insertions, 15 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index a7c50d1e4..65ccabd89 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -222,6 +222,8 @@ libcvc4_add_sources(
   smt/preprocess_proof_generator.h
   smt/process_assertions.cpp
   smt/process_assertions.h
+  smt/proof_manager.cpp
+  smt/proof_manager.h
   smt/proof_post_processor.cpp
   smt/proof_post_processor.h
   smt/set_defaults.cpp
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 2c87158de..4e1a89259 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -174,6 +174,34 @@ header = "options/smt_options.h"
   help       = "check proofs eagerly with proof-new for local debugging"
 
 [[option]]
+  name       = "proofGranularityMode"
+  category   = "regular"
+  long       = "proof-granularity=MODE"
+  type       = "ProofGranularityMode"
+  default    = "THEORY_REWRITE"
+  help       = "modes for proof granularity"
+  help_mode  = "Modes for proof granularity."
+[[option.mode.OFF]]
+  name = "off"
+  help = "Do not improve the granularity of proofs."
+[[option.mode.REWRITE]]
+  name = "rewrite"
+  help = "allow rewrite or substitution steps, expand macros."
+[[option.mode.THEORY_REWRITE]]
+  name = "theory-rewrite"
+  help = "allow theory rewrite steps, expand macros, rewrite and substitution steps."
+[[option.mode.DSL_REWRITE]]
+  name = "dsl-rewrite"
+  help = "Allow DSL rewrites and evaluation steps, expand macros, rewrite, substitution, and theory rewrite steps."
+
+[[option]]
+  name       = "checkProofsNew"
+  category   = "regular"
+  long       = "check-proofs-new"
+  type       = "bool"
+  help       = "after UNSAT/VALID, check the generated proof (with proof-new)"
+
+[[option]]
   name       = "dumpInstantiations"
   category   = "regular"
   long       = "dump-instantiations"
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index a9e2d4d36..735a93f56 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -72,7 +72,7 @@ void AssertionPipeline::pushBackTrusted(theory::TrustNode trn)
 {
   Assert(trn.getKind() == theory::TrustNodeKind::LEMMA);
   // push back what was proven
-  push_back(trn.getProven(), false, trn.getGenerator());
+  push_back(trn.getProven(), false, false, trn.getGenerator());
 }
 
 void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 8019c383d..714622bae 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -197,7 +197,7 @@ void Assertions::addFormula(
   }
 
   // Add the normalized formula to the queue
-  d_assertions.push_back(n, isAssumption);
+  d_assertions.push_back(n, isAssumption, true);
 }
 
 void Assertions::addDefineFunRecDefinition(Node n, bool global)
@@ -234,5 +234,15 @@ void Assertions::ensureBoolean(const Node& n)
   }
 }
 
+void Assertions::setProofGenerator(smt::PreprocessProofGenerator* pppg)
+{
+  d_assertions.setProofGenerator(pppg);
+}
+
+bool Assertions::isProofEnabled() const
+{
+  return d_assertions.isProofEnabled();
+}
+
 }  // namespace smt
 }  // namespace CVC4
diff --git a/src/smt/assertions.h b/src/smt/assertions.h
index a74c58bd8..a73cd32d6 100644
--- a/src/smt/assertions.h
+++ b/src/smt/assertions.h
@@ -109,6 +109,12 @@ class Assertions
   /** Flip the global negation flag. */
   void flipGlobalNegated();
 
+  //------------------------------------ for proofs
+  /** Set proof generator */
+  void setProofGenerator(smt::PreprocessProofGenerator* pppg);
+  /** Is proof enabled? */
+  bool isProofEnabled() const;
+  //------------------------------------ end for proofs
  private:
   /**
    * Fully type-check the argument, and also type-check that it's
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
new file mode 100644
index 000000000..b78bb771a
--- /dev/null
+++ b/src/smt/proof_manager.cpp
@@ -0,0 +1,150 @@
+/*********************                                                        */
+/*! \file proof_manager.cpp
+ ** \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 the SMT engine
+ **/
+
+#include "smt/proof_manager.h"
+
+#include "expr/proof_node_algorithm.h"
+#include "options/base_options.h"
+#include "options/smt_options.h"
+#include "smt/assertions.h"
+
+namespace CVC4 {
+namespace smt {
+
+PfManager::PfManager(SmtEngine* smte)
+    : d_pchecker(new ProofChecker(options::proofNewPedantic())),
+      d_pnm(new ProofNodeManager(d_pchecker.get())),
+      d_pppg(new PreprocessProofGenerator(d_pnm.get())),
+      d_pfpp(new ProofPostproccess(d_pnm.get(), smte, d_pppg.get())),
+      d_finalProof(nullptr)
+{
+  // add rules to eliminate here
+  if (options::proofGranularityMode() != options::ProofGranularityMode::OFF)
+  {
+    d_pfpp->setEliminateRule(PfRule::MACRO_SR_EQ_INTRO);
+    d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_INTRO);
+    d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_ELIM);
+    d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_TRANSFORM);
+    if (options::proofGranularityMode()
+        != options::ProofGranularityMode::REWRITE)
+    {
+      d_pfpp->setEliminateRule(PfRule::SUBS);
+      d_pfpp->setEliminateRule(PfRule::REWRITE);
+      if (options::proofGranularityMode()
+          != options::ProofGranularityMode::THEORY_REWRITE)
+      {
+        // this eliminates theory rewriting steps with finer-grained DSL rules
+        d_pfpp->setEliminateRule(PfRule::THEORY_REWRITE);
+      }
+    }
+  }
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+PfManager::~PfManager() {}
+
+void PfManager::setFinalProof(ProofGenerator* pg, context::CDList<Node>* al)
+{
+  Assert(al != nullptr);
+  // Note this assumes that setFinalProof is only called once per unsat
+  // response. This method would need to cache its result otherwise.
+  Trace("smt-proof") << "SmtEngine::setFinalProof(): get proof body...\n";
+
+  // d_finalProof should just be a ProofNode
+  std::shared_ptr<ProofNode> body = pg->getProofFor(d_false)->clone();
+
+  if (Trace.isOn("smt-proof-debug"))
+  {
+    Trace("smt-proof-debug")
+        << "SmtEngine::setFinalProof(): Proof node for false:\n";
+    Trace("smt-proof-debug") << *body.get() << std::endl;
+    Trace("smt-proof-debug") << "=====" << std::endl;
+  }
+
+  if (Trace.isOn("smt-proof"))
+  {
+    std::vector<Node> fassumps;
+    expr::getFreeAssumptions(body.get(), fassumps);
+    Trace("smt-proof")
+        << "SmtEngine::setFinalProof(): initial free assumptions are:\n";
+    for (const Node& a : fassumps)
+    {
+      Trace("smt-proof") << "- " << a << std::endl;
+    }
+  }
+
+  std::vector<Node> assertions;
+  Trace("smt-proof") << "SmtEngine::setFinalProof(): assertions are:\n";
+  for (context::CDList<Node>::const_iterator i = al->begin(); i != al->end();
+       ++i)
+  {
+    Node n = *i;
+    Trace("smt-proof") << "- " << n << std::endl;
+    assertions.push_back(n);
+  }
+  Trace("smt-proof") << "=====" << std::endl;
+
+  Trace("smt-proof") << "SmtEngine::setFinalProof(): postprocess...\n";
+  Assert(d_pfpp != nullptr);
+  d_pfpp->process(body);
+
+  Trace("smt-proof") << "SmtEngine::setFinalProof(): make scope...\n";
+
+  // Now make the final scope, which ensures that the only open leaves
+  // of the proof are the assertions.
+  d_finalProof = d_pnm->mkScope(body, assertions);
+  Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n";
+}
+
+void PfManager::printProof(ProofGenerator* pg, Assertions& as)
+{
+  Trace("smt-proof") << "PfManager::printProof: start" << std::endl;
+  std::shared_ptr<ProofNode> fp = getFinalProof(pg, as);
+  // TODO (proj #37) according to the proof format, post process the proof node
+  // TODO (proj #37) according to the proof format, print the proof node
+  // leanPrinter(out, fp.get());
+  std::ostream& out = *options::out();
+  out << "(proof\n";
+  out << *fp;
+  out << "\n)\n";
+}
+
+void PfManager::checkProof(ProofGenerator* pg, Assertions& as)
+{
+  Trace("smt-proof") << "PfManager::checkProof: start" << std::endl;
+  std::shared_ptr<ProofNode> fp = getFinalProof(pg, as);
+  Trace("smt-proof") << "PfManager::checkProof: returned " << *fp.get()
+                     << std::endl;
+}
+
+ProofChecker* PfManager::getProofChecker() const { return d_pchecker.get(); }
+
+ProofNodeManager* PfManager::getProofNodeManager() const { return d_pnm.get(); }
+
+smt::PreprocessProofGenerator* PfManager::getPreprocessProofGenerator() const
+{
+  return d_pppg.get();
+}
+
+std::shared_ptr<ProofNode> PfManager::getFinalProof(ProofGenerator* pg,
+                                                    Assertions& as)
+{
+  context::CDList<Node>* al = as.getAssertionList();
+  setFinalProof(pg, al);
+  Assert(d_finalProof);
+  return d_finalProof;
+}
+
+}  // namespace smt
+}  // namespace CVC4
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 */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 81d4f594d..7f824bff3 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -50,12 +50,7 @@
 #include "expr/node_builder.h"
 #include "expr/node_self_iterator.h"
 #include "expr/node_visitor.h"
-#include "options/arith_options.h"
-#include "options/arrays_options.h"
 #include "options/base_options.h"
-#include "options/booleans_options.h"
-#include "options/bv_options.h"
-#include "options/datatypes_options.h"
 #include "options/decision_options.h"
 #include "options/language.h"
 #include "options/main_options.h"
@@ -64,12 +59,9 @@
 #include "options/printer_options.h"
 #include "options/prop_options.h"
 #include "options/quantifiers_options.h"
-#include "options/sep_options.h"
 #include "options/set_language.h"
 #include "options/smt_options.h"
-#include "options/strings_options.h"
 #include "options/theory_options.h"
-#include "options/uf_options.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "preprocessing/preprocessing_pass_registry.h"
@@ -89,6 +81,7 @@
 #include "smt/model_core_builder.h"
 #include "smt/options_manager.h"
 #include "smt/preprocessor.h"
+#include "smt/proof_manager.h"
 #include "smt/quant_elim_solver.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_engine_state.h"
@@ -99,12 +92,9 @@
 #include "smt/update_ostream.h"
 #include "smt_util/boolean_simplification.h"
 #include "smt_util/nary_builder.h"
-#include "theory/booleans/circuit_propagator.h"
-#include "theory/bv/theory_bv_rewriter.h"
 #include "theory/logic_info.h"
 #include "theory/rewriter.h"
 #include "theory/sort_inference.h"
-#include "theory/strings/theory_strings.h"
 #include "theory/substitutions.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"
@@ -139,6 +129,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())),
       d_smtSolver(nullptr),
       d_proofManager(nullptr),
+      d_pfManager(nullptr),
       d_rewriter(new theory::Rewriter()),
       d_definedFunctions(nullptr),
       d_sygusSolver(nullptr),
@@ -262,6 +253,20 @@ void SmtEngine::finishInit()
   // based on our heuristics.
   d_optm->finishInit(d_logic, d_isInternalSubsolver);
 
+  ProofNodeManager* pnm = nullptr;
+  if (options::proofNew())
+  {
+    d_pfManager.reset(new PfManager(this));
+    // use this proof node manager
+    pnm = d_pfManager->getProofNodeManager();
+    // enable proof support in the rewriter
+    d_rewriter->setProofNodeManager(pnm);
+    // enable it in the assertions pipeline
+    d_asserts->setProofGenerator(d_pfManager->getPreprocessProofGenerator());
+    // enable it in the SmtSolver
+    d_smtSolver->setProofNodeManager(pnm);
+  }
+
   Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
   d_smtSolver->finishInit(const_cast<const LogicInfo&>(d_logic));
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5ef8b63c6..e95e36c3d 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -117,6 +117,7 @@ class DefinedFunction;
 struct SmtEngineStatistics;
 class SmtScope;
 class ProcessAssertions;
+class PfManager;
 
 ProofManager* currentProofManager();
 }/* CVC4::smt namespace */
@@ -900,7 +901,10 @@ class CVC4_PUBLIC SmtEngine
   /** Get a pointer to the PropEngine owned by this SmtEngine. */
   prop::PropEngine* getPropEngine();
 
-  /** Get a pointer to the ProofManager owned by this SmtEngine. */
+  /**
+   * Get a pointer to the ProofManager owned by this SmtEngine.
+   * TODO (project #37): this is the old proof manager and will be deleted
+   */
   ProofManager* getProofManager() { return d_proofManager.get(); };
 
   /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
@@ -1072,10 +1076,16 @@ class CVC4_PUBLIC SmtEngine
   /** The SMT solver */
   std::unique_ptr<smt::SmtSolver> d_smtSolver;
 
-  /** The proof manager */
+  /** The (old) proof manager TODO (project #37): delete this */
   std::unique_ptr<ProofManager> d_proofManager;
 
   /**
+   * The proof manager, which manages all things related to checking,
+   * processing, and printing proofs.
+   */
+  std::unique_ptr<smt::PfManager> d_pfManager;
+
+  /**
    * The rewriter associated with this SmtEngine. We have a different instance
    * of the rewriter for each SmtEngine instance. This is because rewriters may
    * hold references to objects that belong to theory solvers, which are
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 706c18416..c64689be6 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -35,6 +35,7 @@ SmtSolver::SmtSolver(SmtEngine& smt,
       d_rm(rm),
       d_pp(pp),
       d_stats(stats),
+      d_pnm(nullptr),
       d_theoryEngine(nullptr),
       d_propEngine(nullptr)
 {
@@ -245,6 +246,8 @@ void SmtSolver::processAssertions(Assertions& as)
   as.clearCurrent();
 }
 
+void SmtSolver::setProofNodeManager(ProofNodeManager* pnm) { d_pnm = pnm; }
+
 TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); }
 
 prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); }
diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index 8d0644800..07d81f92b 100644
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -28,6 +28,7 @@ namespace CVC4 {
 class SmtEngine;
 class TheoryEngine;
 class ResourceManager;
+class ProofNodeManager;
 
 namespace prop {
 class PropEngine;
@@ -108,6 +109,11 @@ class SmtSolver
    * into the SMT solver, and clears the buffer.
    */
   void processAssertions(Assertions& as);
+  /**
+   * Set proof node manager. Enables proofs in this SmtSolver. Should be
+   * called before finishInit.
+   */
+  void setProofNodeManager(ProofNodeManager* pnm);
   //------------------------------------------ access methods
   /** Get a pointer to the TheoryEngine owned by this solver. */
   TheoryEngine* getTheoryEngine();
@@ -125,6 +131,11 @@ class SmtSolver
   Preprocessor& d_pp;
   /** Reference to the statistics of SmtEngine */
   SmtEngineStatistics& d_stats;
+  /**
+   * Pointer to the proof node manager used by this SmtSolver. A non-null
+   * proof node manager indicates that proofs are enabled.
+   */
+  ProofNodeManager* d_pnm;
   /** The theory engine */
   std::unique_ptr<TheoryEngine> d_theoryEngine;
   /** The propositional engine */