Eliminate dependency of proof manager on SMT solver (cvc5#11238)

This moves ownership of the preprocess proof generator from the
preprocessor to the proof manager.

This allows us to eliminate a dependency on SMT solver for connecting
proofs to the input.

It furthermore generalizes modes for printing proofs.

This is work towards a proof logging mode.

src/proof/alf/alf_printer.cpp

@@ -635,6 +635,7 @@ void AlfPrinter::print(AlfPrintChannelOut& aout,
       dscope != nullptr ? dscope->getArguments() : d_emptyVec;
   const std::vector<Node>& assertions =
       ascope != nullptr ? ascope->getArguments() : d_emptyVec;
+
   bool wasAlloc;
   for (size_t i = 0; i < 2; i++)
   {

src/smt/env.cpp

@@ -28,6 +28,7 @@
 #include "options/strings_options.h"
 #include "printer/printer.h"
 #include "proof/conv_proof_generator.h"
+#include "smt/proof_manager.h"
 #include "smt/solver_engine_stats.h"
 #include "theory/evaluator.h"
 #include "theory/quantifiers/oracle_checker.h"
@@ -45,6 +46,7 @@ Env::Env(NodeManager* nm, const Options* opts)
     : d_nm(nm),
       d_context(new context::Context()),
       d_userContext(new context::UserContext()),
+      d_pfManager(nullptr),
       d_proofNodeManager(nullptr),
       d_rewriter(new theory::Rewriter(nm)),
       d_evalRew(nullptr),
@@ -76,12 +78,13 @@ Env::~Env() {}
 
 NodeManager* Env::getNodeManager() { return d_nm; }
 
-void Env::finishInit(ProofNodeManager* pnm)
+void Env::finishInit(smt::PfManager* pm)
 {
-  if (pnm != nullptr)
+  if (pm != nullptr)
   {
+    d_pfManager = pm;
     Assert(d_proofNodeManager == nullptr);
-    d_proofNodeManager = pnm;
+    d_proofNodeManager = pm->getProofNodeManager();
     d_rewriter->finishInit(*this);
   }
   d_topLevelSubs.reset(
@@ -104,6 +107,8 @@ context::Context* Env::getContext() { return d_context.get(); }
 
 context::UserContext* Env::getUserContext() { return d_userContext.get(); }
 
+smt::PfManager* Env::getProofManager() { return d_pfManager; }
+
 ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
 
 bool Env::isSatProofProducing() const

src/smt/env.h

@@ -88,7 +88,12 @@ class Env
 
   /** Get a pointer to the UserContext owned by this Env. */
   context::UserContext* getUserContext();
-
+  /**
+   * Get the underlying proof manager. Note since proofs depend on option
+   * initialization, this is only available after the SolverEngine that owns
+   * this environment is initialized, and only non-null if proofs are enabled.
+   */
+  smt::PfManager* getProofManager();
   /**
    * Get the underlying proof node manager. Note since proofs depend on option
    * initialization, this is only available after the SolverEngine that owns
@@ -317,7 +322,7 @@ class Env
   /* Private initialization ------------------------------------------------- */
 
   /** Set proof node manager if it exists */
-  void finishInit(ProofNodeManager* pnm);
+  void finishInit(smt::PfManager* pm);
 
   /* Private shutdown ------------------------------------------------------- */
   /**
@@ -333,6 +338,10 @@ class Env
   std::unique_ptr<context::Context> d_context;
   /** User level context owned by this Env */
   std::unique_ptr<context::UserContext> d_userContext;
+  /**
+   * The proof manager of the solver engine.
+   */
+  smt::PfManager* d_pfManager;
   /**
    * A pointer to the proof node manager, which is non-null if proofs are
    * enabled. This is owned by the proof manager of the SolverEngine that owns

src/smt/preprocessor.cpp

@@ -46,14 +46,15 @@ Preprocessor::Preprocessor(Env& env,
 
 Preprocessor::~Preprocessor() {}
 
-void Preprocessor::finishInit(TheoryEngine* te, prop::PropEngine* pe)
+void Preprocessor::finishInit(TheoryEngine* te,
+                              prop::PropEngine* pe,
+                              PreprocessProofGenerator* pppg)
 {
   // set up the preprocess proof generator, if necessary
-  if (options().smt.produceProofs && d_pppg == nullptr)
+  if (d_pppg == nullptr && pppg != nullptr)
   {
-    d_pppg = std::make_unique<PreprocessProofGenerator>(
-        d_env, userContext(), "smt::PreprocessProofGenerator");
-    d_propagator.enableProofs(userContext(), d_pppg.get());
+    d_pppg = pppg;
+    d_propagator.enableProofs(userContext(), d_pppg);
   }
 
   d_ppContext.reset(new preprocessing::PreprocessingPassContext(
@@ -129,7 +130,7 @@ void Preprocessor::applySubstitutions(std::vector<Node>& ns)
 
 PreprocessProofGenerator* Preprocessor::getPreprocessProofGenerator()
 {
-  return d_pppg.get();
+  return d_pppg;
 }
 
 }  // namespace smt

src/smt/preprocessor.h

@@ -57,7 +57,9 @@ class Preprocessor : protected EnvObj
   /**
    * Finish initialization
    */
-  void finishInit(TheoryEngine* te, prop::PropEngine* pe);
+  void finishInit(TheoryEngine* te,
+                  prop::PropEngine* pe,
+                  PreprocessProofGenerator* pppg);
   /**
    * Process the assertions that have been asserted in argument as. Returns
    * true if no conflict was discovered while preprocessing them.
@@ -91,8 +93,8 @@ class Preprocessor : protected EnvObj
   PreprocessProofGenerator* getPreprocessProofGenerator();
 
  private:
-  /** The preprocess proof generator. */
-  std::unique_ptr<PreprocessProofGenerator> d_pppg;
+  /** Pointer to the preprocess proof generator. */
+  PreprocessProofGenerator* d_pppg;
   /**
    * A circuit propagator for non-clausal propositional deduction.
    */

src/smt/proof_manager.cpp

@@ -45,7 +45,8 @@ PfManager::PfManager(Env& env)
       d_rewriteDb(nullptr),
       d_pchecker(nullptr),
       d_pnm(nullptr),
-      d_pfpp(nullptr)
+      d_pfpp(nullptr),
+      d_pppg(nullptr)
 {
   // construct the rewrite db only if DSL rewrites are enabled
   if (options().proof.proofGranularityMode
@@ -75,6 +76,7 @@ PfManager::PfManager(Env& env)
       output(OutputTag::RARE_DB) << ss.str();
     }
   }
+
   // enable the proof checker and the proof node manager
   d_pchecker.reset(
       new ProofChecker(statisticsRegistry(),
@@ -140,6 +142,9 @@ PfManager::PfManager(Env& env)
     d_pfpp->setEliminateRule(ProofRule::TRUST);
   }
   d_false = nodeManager()->mkConst(false);
+
+  d_pppg = std::make_unique<PreprocessProofGenerator>(
+      d_env, userContext(), "smt::PreprocessProofGenerator");
 }
 
 PfManager::~PfManager() {}
@@ -157,11 +162,8 @@ constexpr typename std::vector<T, Alloc>::size_type erase_if(
 }
 
 std::shared_ptr<ProofNode> PfManager::connectProofToAssertions(
-    std::shared_ptr<ProofNode> pfn, SmtSolver& smt, ProofScopeMode scopeMode)
+    std::shared_ptr<ProofNode> pfn, Assertions& as, ProofScopeMode scopeMode)
 {
-  Assertions& as = smt.getAssertions();
-  PreprocessProofGenerator* pppg =
-      smt.getPreprocessor()->getPreprocessProofGenerator();
   // Note this assumes that connectProofToAssertions is only called once per
   // unsat response. This method would need to cache its result otherwise.
   Trace("smt-proof")
@@ -210,7 +212,7 @@ std::shared_ptr<ProofNode> PfManager::connectProofToAssertions(
   {
     d_pfpp->setAssertions(assertions, false);
   }
-  d_pfpp->process(pfn, pppg);
+  d_pfpp->process(pfn, d_pppg.get());
 
   switch (scopeMode)
   {
@@ -268,9 +270,10 @@ std::shared_ptr<ProofNode> PfManager::connectProofToAssertions(
 void PfManager::printProof(std::ostream& out,
                            std::shared_ptr<ProofNode> fp,
                            options::ProofFormatMode mode,
+                           ProofScopeMode scopeMode,
                            const std::map<Node, std::string>& assertionNames)
 {
-  Trace("smt-proof") << "PfManager::printProof: start" << std::endl;
+  Trace("smt-proof") << "PfManager::printProof: start " << mode << std::endl;
   // We don't want to invalidate the proof nodes in fp, since these may be
   // reused in further check-sat calls, or they may be used again if the
   // user asks for the proof again (in non-incremental mode). We don't need to
@@ -290,10 +293,9 @@ void PfManager::printProof(std::ostream& out,
   }
   else if (mode == options::ProofFormatMode::CPC)
   {
-    Assert(fp->getRule() == ProofRule::SCOPE);
     proof::AlfNodeConverter atp(nodeManager());
     proof::AlfPrinter alfp(d_env, atp, d_rewriteDb.get());
-    alfp.print(out, fp);
+    alfp.print(out, fp, scopeMode);
   }
   else if (mode == options::ProofFormatMode::ALETHE)
   {
@@ -332,7 +334,7 @@ void PfManager::printProof(std::ostream& out,
 }
 
 void PfManager::translateDifficultyMap(std::map<Node, Node>& dmap,
-                                       SmtSolver& smt)
+                                       Assertions& as)
 {
   Trace("difficulty-proc") << "Translate difficulty start" << std::endl;
   Trace("difficulty") << "PfManager::translateDifficultyMap" << std::endl;
@@ -361,7 +363,7 @@ void PfManager::translateDifficultyMap(std::map<Node, Node>& dmap,
   cdp.addStep(fnode, ProofRule::SAT_REFUTATION, ppAsserts, {});
   std::shared_ptr<ProofNode> pf = cdp.getProofFor(fnode);
   Trace("difficulty-proc") << "Get final proof" << std::endl;
-  std::shared_ptr<ProofNode> fpf = connectProofToAssertions(pf, smt);
+  std::shared_ptr<ProofNode> fpf = connectProofToAssertions(pf, as);
   Trace("difficulty-debug") << "Final proof is " << *fpf.get() << std::endl;
   // We are typically a SCOPE here, although if we are not, then the proofs
   // have no free assumptions. If this is the case, then the only difficulty
@@ -408,6 +410,11 @@ rewriter::RewriteDb* PfManager::getRewriteDatabase() const
   return d_rewriteDb.get();
 }
 
+PreprocessProofGenerator* PfManager::getPreprocessProofGenerator() const
+{
+  return d_pppg.get();
+}
+
 void PfManager::getAssertions(Assertions& as, std::vector<Node>& assertions)
 {
   // note that the assertion list is always available

src/smt/proof_manager.h

@@ -48,7 +48,6 @@ enum class ProofScopeMode
 namespace smt {
 
 class Assertions;
-class SmtSolver;
 class PreprocessProofGenerator;
 class ProofPostprocess;
 
@@ -92,10 +91,17 @@ class PfManager : protected EnvObj
   ~PfManager();
   /**
    * Print the proof on the given output stream in the given format.
+   *
+   * @param out The output stream.
+   * @param fp The proof to print.
+   * @param mode The format (e.g. cpc, alethe) to print.
+   * @param scopeMode The expected form of fp (see ProofScopeMode).
+   * @param assertionNames The named assertions of the input.
    */
   void printProof(std::ostream& out,
                   std::shared_ptr<ProofNode> fp,
                   options::ProofFormatMode mode,
+                  ProofScopeMode scopeMode,
                   const std::map<Node, std::string>& assertionNames =
                       std::map<Node, std::string>());
 
@@ -115,7 +121,7 @@ class PfManager : protected EnvObj
    * @param smt The SMT solver that owns the assertions and the preprocess
    * proof generator.
    */
-  void translateDifficultyMap(std::map<Node, Node>& dmap, SmtSolver& smt);
+  void translateDifficultyMap(std::map<Node, Node>& dmap, Assertions& as);
 
   /**
    * Connect proof to assertions
@@ -128,10 +134,14 @@ class PfManager : protected EnvObj
    * respect to assertions in as. Note this includes equalities of the form
    * (= f (lambda (...) t)) which originate from define-fun commands for f.
    * These are considered assertions in the final proof.
+   *
+   * @param pfn The proof.
+   * @param as Reference to the assertions.
+   * @param scopeMode The expected form of fp (see ProofScopeMode).
    */
   std::shared_ptr<ProofNode> connectProofToAssertions(
       std::shared_ptr<ProofNode> pfn,
-      SmtSolver& smt,
+      Assertions& as,
       ProofScopeMode scopeMode = ProofScopeMode::UNIFIED);
   //--------------------------- access to utilities
   /** Get a pointer to the ProofChecker owned by this. */
@@ -140,6 +150,8 @@ class PfManager : protected EnvObj
   ProofNodeManager* getProofNodeManager() const;
   /** Get the rewrite database, containing definitions of rewrites from DSL. */
   rewriter::RewriteDb* getRewriteDatabase() const;
+  /** Get the preprocess proof generator */
+  PreprocessProofGenerator* getPreprocessProofGenerator() const;
   //--------------------------- end access to utilities
  private:
   /**
@@ -162,6 +174,8 @@ class PfManager : protected EnvObj
   std::unique_ptr<ProofNodeManager> d_pnm;
   /** The proof post-processor */
   std::unique_ptr<smt::ProofPostprocess> d_pfpp;
+  /** The preprocess proof generator. */
+  std::unique_ptr<PreprocessProofGenerator> d_pppg;
 }; /* class SolverEngine */
 
 }  // namespace smt

src/smt/smt_solver.cpp

@@ -24,6 +24,7 @@
 #include "smt/env.h"
 #include "smt/logic_exception.h"
 #include "smt/preprocessor.h"
+#include "smt/proof_manager.h"
 #include "smt/solver_engine_stats.h"
 #include "theory/logic_info.h"
 #include "theory/theory_engine.h"
@@ -81,7 +82,7 @@ void SmtSolver::finishInit()
   Trace("smt-debug") << "Finishing init for theory engine..." << std::endl;
   d_theoryEngine->finishInit();
   d_propEngine->finishInit();
-  d_pp.finishInit(d_theoryEngine.get(), d_propEngine.get());
+  finishInitPreprocessor();
 }
 
 void SmtSolver::resetAssertions()
@@ -98,7 +99,7 @@ void SmtSolver::resetAssertions()
   // depend on knowing the associated PropEngine.
   d_propEngine->finishInit();
   // must reset the preprocessor as well
-  d_pp.finishInit(d_theoryEngine.get(), d_propEngine.get());
+  finishInitPreprocessor();
 }
 
 void SmtSolver::interrupt()
@@ -232,5 +233,17 @@ void SmtSolver::resetTrail()
   d_propEngine->resetTrail();
 }
 
+void SmtSolver::finishInitPreprocessor()
+{
+  // determine if we are assigning a preprocess proof generator here
+  smt::PfManager* pm = d_env.getProofManager();
+  smt::PreprocessProofGenerator* pppg = nullptr;
+  if (pm != nullptr)
+  {
+    pppg = pm->getPreprocessProofGenerator();
+  }
+  d_pp.finishInit(d_theoryEngine.get(), d_propEngine.get(), pppg);
+}
+
 }  // namespace smt
 }  // namespace cvc5::internal

src/smt/smt_solver.h

@@ -135,6 +135,8 @@ class SmtSolver : protected EnvObj
  private:
   /** Whether we track information necessary for deep restarts */
   bool trackPreprocessedAssertions() const;
+  /** Finish initialization of preprocessor */
+  void finishInitPreprocessor();
   /** The preprocessor of this SMT solver */
   Preprocessor d_pp;
   /** Assertions manager */