Refactoring of proof manager initialization (#7073)

No longer takes a backwards reference to SmtEngine.

Also takes minor changes to proof post-processor from proof-new.

7 files changed, 100 insertions, 67 deletions

diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index b741ec5d5..0225cf24c 100644
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -60,6 +60,14 @@ name   = "Proof"
   help       = "do not check rule applications"
 
 [[option]]
+  name       = "proofPpMerge"
+  category   = "regular"
+  long       = "proof-pp-merge"
+  type       = "bool"
+  default    = "true"
+  help       = "merge subproofs in final proof post-processor"
+
+[[option]]
   name       = "proofGranularityMode"
   category   = "regular"
   long       = "proof-granularity=MODE"
diff --git a/src/smt/env.h b/src/smt/env.h
index e54f12fa5..d95e70226 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -40,6 +40,7 @@ class UserContext;
 
 namespace smt {
 class DumpManager;
+class PfManager;
 }
 
 namespace theory {
@@ -56,6 +57,7 @@ class TrustSubstitutionMap;
 class Env
 {
   friend class SmtEngine;
+  friend class smt::PfManager;
 
  public:
   /**
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index ae5de49e9..2c3a22a78 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -31,37 +31,42 @@
 namespace cvc5 {
 namespace smt {
 
-PfManager::PfManager(Env& env, SmtEngine* smte)
-    : d_env(env),
+PfManager::PfManager(Env& env)
+    : EnvObj(env),
       d_pchecker(new ProofChecker(
-          d_env.getOptions().proof.proofCheck == options::ProofCheckMode::EAGER,
-          d_env.getOptions().proof.proofPedantic)),
+          options().proof.proofCheck == options::ProofCheckMode::EAGER,
+          options().proof.proofPedantic)),
       d_pnm(new ProofNodeManager(d_pchecker.get())),
       d_pppg(new PreprocessProofGenerator(
           d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")),
-      d_pfpp(new ProofPostproccess(
-          d_pnm.get(),
-          smte,
-          d_pppg.get(),
-          // by default the post-processor will update all assumptions, which
-          // can lead to SCOPE subproofs of the form
-          //   A
-          //  ...
-          //   B1    B2
-          //  ...   ...
-          // ------------
-          //      C
-          // ------------- SCOPE [B1, B2]
-          // B1 ^ B2 => C
-          //
-          // where A is an available assumption from outside the scope (note
-          // that B1 was an assumption of this SCOPE subproof but since it could
-          // be inferred from A, it was updated). This shape is problematic for
-          // the veriT reconstruction, so we disable the update of scoped
-          // assumptions (which would disable the update of B1 in this case).
-          options::proofFormatMode() != options::ProofFormatMode::VERIT)),
+      d_pfpp(nullptr),
       d_finalProof(nullptr)
 {
+  // enable proof support in the environment/rewriter
+  d_env.setProofNodeManager(d_pnm.get());
+  // Now, initialize the proof postprocessor with the environment.
+  // By default the post-processor will update all assumptions, which
+  // can lead to SCOPE subproofs of the form
+  //   A
+  //  ...
+  //   B1    B2
+  //  ...   ...
+  // ------------
+  //      C
+  // ------------- SCOPE [B1, B2]
+  // B1 ^ B2 => C
+  //
+  // where A is an available assumption from outside the scope (note
+  // that B1 was an assumption of this SCOPE subproof but since it could
+  // be inferred from A, it was updated). This shape is problematic for
+  // the veriT reconstruction, so we disable the update of scoped
+  // assumptions (which would disable the update of B1 in this case).
+  d_pfpp.reset(new ProofPostproccess(
+      env,
+      d_pppg.get(),
+      nullptr,
+      options::proofFormatMode() != options::ProofFormatMode::VERIT));
+
   // add rules to eliminate here
   if (options::proofGranularityMode() != options::ProofGranularityMode::OFF)
   {
@@ -159,6 +164,7 @@ void PfManager::printProof(std::ostream& out,
   // 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
 
+  // according to the proof format, post process and print the proof node
   if (options::proofFormatMode() == options::ProofFormatMode::DOT)
   {
     proof::DotPrinter dotPrinter;
@@ -166,13 +172,16 @@ void PfManager::printProof(std::ostream& out,
   }
   else if (options::proofFormatMode() == options::ProofFormatMode::TPTP)
   {
-    out << "% SZS output start Proof for " << d_env.getOptions().driver.filename << std::endl;
+    out << "% SZS output start Proof for " << options().driver.filename
+        << std::endl;
     // TODO (proj #37) print in TPTP compliant format
     out << *fp << std::endl;
-    out << "% SZS output end Proof for " << d_env.getOptions().driver.filename << std::endl;
+    out << "% SZS output end Proof for " << options().driver.filename
+        << std::endl;
   }
   else
   {
+    // otherwise, print using default printer
     out << "(proof\n";
     out << *fp;
     out << "\n)\n";
@@ -190,6 +199,8 @@ ProofChecker* PfManager::getProofChecker() const { return d_pchecker.get(); }
 
 ProofNodeManager* PfManager::getProofNodeManager() const { return d_pnm.get(); }
 
+rewriter::RewriteDb* PfManager::getRewriteDatabase() const { return nullptr; }
+
 smt::PreprocessProofGenerator* PfManager::getPreprocessProofGenerator() const
 {
   return d_pppg.get();
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index fd24f62f6..034a4554f 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -20,15 +20,19 @@
 
 #include "context/cdhashmap.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
-class Env;
 class ProofChecker;
 class ProofNode;
 class ProofNodeManager;
 class SmtEngine;
 
+namespace rewriter {
+class RewriteDb;
+}
+
 namespace smt {
 
 class Assertions;
@@ -68,10 +72,10 @@ class ProofPostproccess;
  * - If SmtEngine has been configured in a way that is incompatible with proofs
  *   then unsat core production will be disabled.
  */
-class PfManager
+class PfManager : protected EnvObj
 {
  public:
-  PfManager(Env& env, SmtEngine* smte);
+  PfManager(Env& env);
   ~PfManager();
   /**
    * Print the proof on the given output stream.
@@ -103,6 +107,8 @@ class PfManager
   ProofChecker* getProofChecker() const;
   /** Get a pointer to the ProofNodeManager owned by this. */
   ProofNodeManager* getProofNodeManager() const;
+  /** Get the rewrite database, containing definitions of rewrites from DSL. */
+  rewriter::RewriteDb* getRewriteDatabase() const;
   /** Get the proof generator for proofs of preprocessing. */
   smt::PreprocessProofGenerator* getPreprocessProofGenerator() const;
   //--------------------------- end access to utilities
@@ -117,8 +123,6 @@ class PfManager
    */
   void getAssertions(Assertions& as,
                      std::vector<Node>& assertions);
-  /** Reference to the env of SmtEngine */
-  Env& d_env;
   /** The false node */
   Node d_false;
   /** For the new proofs module */
@@ -129,6 +133,7 @@ class PfManager
   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
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 5ad311f8d..9db8f1020 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -17,10 +17,10 @@
 
 #include "expr/skolem_manager.h"
 #include "options/proof_options.h"
-#include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "proof/proof_node_manager.h"
 #include "smt/smt_engine.h"
+#include "theory/arith/arith_utilities.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/bv/bitblast/proof_bitblaster.h"
 #include "theory/rewriter.h"
@@ -34,14 +34,14 @@ using namespace cvc5::theory;
 namespace cvc5 {
 namespace smt {
 
-ProofPostprocessCallback::ProofPostprocessCallback(ProofNodeManager* pnm,
-                                                   SmtEngine* smte,
+ProofPostprocessCallback::ProofPostprocessCallback(Env& env,
                                                    ProofGenerator* pppg,
+                                                   rewriter::RewriteDb* rdb,
                                                    bool updateScopedAssumptions)
-    : d_pnm(pnm),
-      d_smte(smte),
+    : d_env(env),
+      d_pnm(env.getProofNodeManager()),
       d_pppg(pppg),
-      d_wfpm(pnm),
+      d_wfpm(env.getProofNodeManager()),
       d_updateScopedAssumptions(updateScopedAssumptions)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
@@ -949,6 +949,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
   {
     // get the kind of rewrite
     MethodId idr = MethodId::RW_REWRITE;
+    TheoryId theoryId = Theory::theoryOf(args[0]);
     if (args.size() >= 2)
     {
       getMethodId(args[1], idr);
@@ -963,7 +964,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
       // rewrites from theory::Rewriter
       bool isExtEq = (idr == MethodId::RW_REWRITE_EQ_EXT);
       // use rewrite with proof interface
-      Rewriter* rr = d_smte->getRewriter();
+      Rewriter* rr = d_env.getRewriter();
       TrustNode trn = rr->rewriteWithProof(args[0], isExtEq);
       std::shared_ptr<ProofNode> pfn = trn.toProofNode();
       if (pfn == nullptr)
@@ -975,7 +976,6 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
         {
           // update to THEORY_REWRITE with idr
           Assert(args.size() >= 1);
-          TheoryId theoryId = Theory::theoryOf(args[0].getType());
           Node tid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
           cdp->addStep(eq, PfRule::THEORY_REWRITE, {}, {eq, tid, args[1]});
         }
@@ -1001,8 +1001,20 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     }
     else
     {
-      // don't know how to eliminate
-      return Node::null();
+      // try to reconstruct as a standalone rewrite
+      std::vector<Node> targs;
+      targs.push_back(eq);
+      targs.push_back(
+          builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId));
+      // in this case, must be a non-standard rewrite kind
+      Assert(args.size() >= 2);
+      targs.push_back(args[1]);
+      Node eqp = expandMacros(PfRule::THEORY_REWRITE, {}, targs, cdp);
+      if (eqp.isNull())
+      {
+        // don't know how to eliminate
+        return Node::null();
+      }
     }
     if (args[0] == ret)
     {
@@ -1194,16 +1206,15 @@ bool ProofPostprocessCallback::addToTransChildren(Node eq,
   return true;
 }
 
-ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
-                                     SmtEngine* smte,
+ProofPostproccess::ProofPostproccess(Env& env,
                                      ProofGenerator* pppg,
+                                     rewriter::RewriteDb* rdb,
                                      bool updateScopedAssumptions)
-    : d_pnm(pnm),
-      d_cb(pnm, smte, pppg, updateScopedAssumptions),
+    : d_cb(env, pppg, rdb, updateScopedAssumptions),
       // the update merges subproofs
-      d_updater(d_pnm, d_cb, true),
-      d_finalCb(pnm),
-      d_finalizer(d_pnm, d_finalCb)
+      d_updater(env.getProofNodeManager(), d_cb, options::proofPpMerge()),
+      d_finalCb(env.getProofNodeManager()),
+      d_finalizer(env.getProofNodeManager(), d_finalCb)
 {
 }
 
diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index 1aa52dd50..c0cc7bc17 100644
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -30,7 +30,11 @@
 
 namespace cvc5 {
 
-class SmtEngine;
+class Env;
+
+namespace rewriter {
+class RewriteDb;
+}
 
 namespace smt {
 
@@ -41,9 +45,9 @@ namespace smt {
 class ProofPostprocessCallback : public ProofNodeUpdaterCallback
 {
  public:
-  ProofPostprocessCallback(ProofNodeManager* pnm,
-                           SmtEngine* smte,
+  ProofPostprocessCallback(Env& env,
                            ProofGenerator* pppg,
+                           rewriter::RewriteDb* rdb,
                            bool updateScopedAssumptions);
   ~ProofPostprocessCallback() {}
   /**
@@ -73,10 +77,10 @@ class ProofPostprocessCallback : public ProofNodeUpdaterCallback
  private:
   /** Common constants */
   Node d_true;
-  /** The proof node manager */
+  /** Reference to the env */
+  Env& d_env;
+  /** Pointer to the proof node manager */
   ProofNodeManager* d_pnm;
-  /** Pointer to the SmtEngine, which should have proofs enabled */
-  SmtEngine* d_smte;
   /** The preprocessing proof generator */
   ProofGenerator* d_pppg;
   /** The witness form proof generator */
@@ -248,16 +252,15 @@ class ProofPostproccess
 {
  public:
   /**
-   * @param pnm The proof node manager we are using
-   * @param smte The SMT engine whose proofs are being post-processed
+   * @param env The environment we are using
    * @param pppg The proof generator for pre-processing proofs
    * @param updateScopedAssumptions Whether we post-process assumptions in
    * scope. Since doing so is sound and only problematic depending on who is
    * consuming the proof, it's true by default.
    */
-  ProofPostproccess(ProofNodeManager* pnm,
-                    SmtEngine* smte,
+  ProofPostproccess(Env& env,
                     ProofGenerator* pppg,
+                    rewriter::RewriteDb* rdb,
                     bool updateScopedAssumptions = true);
   ~ProofPostproccess();
   /** post-process */
@@ -266,8 +269,6 @@ class ProofPostproccess
   void setEliminateRule(PfRule rule);
 
  private:
-  /** The proof node manager */
-  ProofNodeManager* d_pnm;
   /** The post process callback */
   ProofPostprocessCallback d_cb;
   /**
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 582ca0c2c..cd8bd1d7b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -194,20 +194,15 @@ void SmtEngine::finishInit()
   SetDefaults sdefaults(d_isInternalSubsolver);
   sdefaults.setDefaults(d_env->d_logic, getOptions());
 
-  ProofNodeManager* pnm = nullptr;
   if (d_env->getOptions().smt.produceProofs)
   {
     // ensure bound variable uses canonical bound variables
     getNodeManager()->getBoundVarManager()->enableKeepCacheValues();
     // make the proof manager
-    d_pfManager.reset(new PfManager(*d_env.get(), this));
+    d_pfManager.reset(new PfManager(*d_env.get()));
     PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator();
     // start the unsat core manager
     d_ucManager.reset(new UnsatCoreManager());
-    // use this proof node manager
-    pnm = d_pfManager->getProofNodeManager();
-    // enable proof support in the environment/rewriter
-    d_env->setProofNodeManager(pnm);
     // enable it in the assertions pipeline
     d_asserts->setProofGenerator(pppg);
     // enabled proofs in the preprocessor