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

4 files changed, 164 insertions, 42 deletions

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 685032136..6bdc4ced0 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -18,6 +18,7 @@
 #include "options/base_options.h"
 #include "options/smt_options.h"
 #include "smt/assertions.h"
+#include "smt/defined_function.h"
 
 namespace CVC4 {
 namespace smt {
@@ -55,78 +56,80 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte)
 
 PfManager::~PfManager() {}
 
-void PfManager::setFinalProof(ProofGenerator* pg, context::CDList<Node>* al)
+void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn,
+                              Assertions& as,
+                              DefinedFunctionMap& df)
 {
-  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") << *pfn.get() << std::endl;
     Trace("smt-proof-debug") << "=====" << std::endl;
   }
 
+  std::vector<Node> assertions;
+  getAssertions(as, df, assertions);
+
   if (Trace.isOn("smt-proof"))
   {
+    Trace("smt-proof") << "SmtEngine::setFinalProof(): get free assumptions..."
+                       << std::endl;
     std::vector<Node> fassumps;
-    expr::getFreeAssumptions(body.get(), fassumps);
+    expr::getFreeAssumptions(pfn.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") << "SmtEngine::setFinalProof(): assertions are:\n";
+    for (const Node& n : assertions)
+    {
+      Trace("smt-proof") << "- " << n << std::endl;
+    }
+    Trace("smt-proof") << "=====" << std::endl;
   }
-  Trace("smt-proof") << "=====" << std::endl;
 
   Trace("smt-proof") << "SmtEngine::setFinalProof(): postprocess...\n";
   Assert(d_pfpp != nullptr);
-  d_pfpp->process(body);
+  d_pfpp->process(pfn);
 
   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);
+  d_finalProof = d_pnm->mkScope(pfn, assertions);
   Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n";
 }
 
-void PfManager::printProof(ProofGenerator* pg, Assertions& as)
+void PfManager::printProof(std::shared_ptr<ProofNode> pfn,
+                           Assertions& as,
+                           DefinedFunctionMap& df)
 {
   Trace("smt-proof") << "PfManager::printProof: start" << std::endl;
-  std::shared_ptr<ProofNode> fp = getFinalProof(pg, as);
+  std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as, df);
   // 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)
+void PfManager::checkProof(std::shared_ptr<ProofNode> pfn,
+                           Assertions& as,
+                           DefinedFunctionMap& df)
 {
   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;
+  std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as, df);
+  Trace("smt-proof-debug") << "PfManager::checkProof: returned " << *fp.get()
+                           << std::endl;
 }
 
 ProofChecker* PfManager::getProofChecker() const { return d_pchecker.get(); }
@@ -138,14 +141,40 @@ smt::PreprocessProofGenerator* PfManager::getPreprocessProofGenerator() const
   return d_pppg.get();
 }
 
-std::shared_ptr<ProofNode> PfManager::getFinalProof(ProofGenerator* pg,
-                                                    Assertions& as)
+std::shared_ptr<ProofNode> PfManager::getFinalProof(
+    std::shared_ptr<ProofNode> pfn, Assertions& as, DefinedFunctionMap& df)
 {
-  context::CDList<Node>* al = as.getAssertionList();
-  setFinalProof(pg, al);
+  setFinalProof(pfn, as, df);
   Assert(d_finalProof);
   return d_finalProof;
 }
 
+void PfManager::getAssertions(Assertions& as,
+                              DefinedFunctionMap& df,
+                              std::vector<Node>& assertions)
+{
+  context::CDList<Node>* al = as.getAssertionList();
+  Assert(al != nullptr);
+  for (context::CDList<Node>::const_iterator i = al->begin(); i != al->end();
+       ++i)
+  {
+    assertions.push_back(*i);
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  for (const std::pair<Node, smt::DefinedFunction>& dfn : df)
+  {
+    Node def = dfn.second.getFormula();
+    const std::vector<Node>& formals = dfn.second.getFormals();
+    if (!formals.empty())
+    {
+      Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, formals);
+      def = nm->mkNode(kind::LAMBDA, bvl, def);
+    }
+    // assume the (possibly higher order) equality
+    Node eq = dfn.first.eqNode(def);
+    assertions.push_back(eq);
+  }
+}
+
 }  // namespace smt
 }  // namespace CVC4
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 */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2faad7961..81294722f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -328,6 +328,8 @@ SmtEngine::~SmtEngine()
 #ifdef CVC4_PROOF
     d_proofManager.reset(nullptr);
 #endif
+    d_rewriter.reset(nullptr);
+    d_pfManager.reset(nullptr);
 
     d_absValues.reset(nullptr);
     d_asserts.reset(nullptr);
@@ -951,6 +953,12 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
     Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat")
                  << "(" << assumptions << ") => " << r << endl;
 
+    if (options::dumpProofs() && options::proofNew()
+        && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+    {
+      printProof();
+    }
+
     // Check that SAT results generate a model correctly.
     if(options::checkModels()) {
       if (r.asSatisfiabilityResult().isSat() == Result::SAT)
@@ -958,6 +966,20 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
         checkModel();
       }
     }
+    // Check that UNSAT results generate a proof correctly.
+    if (options::checkProofsNew() || options::proofNewEagerChecking())
+    {
+      if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+      {
+        if ((options::checkProofsNew() || options::proofNewEagerChecking())
+            && !options::proofNew())
+        {
+          throw ModalException(
+              "Cannot check-proofs-new because proof-new was disabled.");
+        }
+        checkProof();
+      }
+    }
     // Check that UNSAT results generate an unsat core correctly.
     if(options::checkUnsatCores()) {
       if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
@@ -1360,6 +1382,20 @@ Node SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
 
 Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
 
+void SmtEngine::checkProof()
+{
+  Assert(options::proofNew());
+  // internal check the proof
+  PropEngine* pe = getPropEngine();
+  Assert(pe != nullptr);
+  Assert(pe->getProof() != nullptr);
+  std::shared_ptr<ProofNode> pePfn = pe->getProof();
+  if (options ::checkProofsNew())
+  {
+    d_pfManager->checkProof(pePfn, *d_asserts, *d_definedFunctions);
+  }
+}
+
 UnsatCore SmtEngine::getUnsatCoreInternal()
 {
 #if IS_PROOFS_BUILD
@@ -1460,6 +1496,25 @@ UnsatCore SmtEngine::getUnsatCore() {
   return getUnsatCoreInternal();
 }
 
+void SmtEngine::printProof()
+{
+  if (d_pfManager == nullptr)
+  {
+    throw RecoverableModalException("Cannot print proof, no proof manager.");
+  }
+  if (getSmtMode() != SmtMode::UNSAT)
+  {
+    throw RecoverableModalException(
+        "Cannot print proof unless immediately preceded by "
+        "UNSAT/ENTAILED.");
+  }
+  PropEngine* pe = getPropEngine();
+  Assert(pe != nullptr);
+  Assert(pe->getProof() != nullptr);
+  // the prop engine has the proof of false
+  d_pfManager->printProof(pe->getProof(), *d_asserts, *d_definedFunctions);
+}
+
 void SmtEngine::printInstantiations( std::ostream& out ) {
   SmtScope smts(this);
   finishInit();
@@ -1664,6 +1719,7 @@ void SmtEngine::resetAssertions()
   // push the state to maintain global context around everything
   d_state->setup();
 
+  // reset SmtSolver, which will construct a new prop engine
   d_smtSolver->resetAssertions();
 }
 
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();