Refactoring initialization of proofs (#7834)

Eliminates one of the remaining calls to Rewriter::callExtendedRewrite, as well as making the initialization much clearer through use of Env.

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index f97c5bafb9f47ade31f14c81c16d7e157a14b23c..778931f7059fdffcb46db40d77a813111a32497a 100644 (file)
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -117,7 +117,7 @@ void AssertionPipeline::replaceTrusted(size_t i, TrustNode trn)
   replace(i, trn.getNode(), trn.getGenerator());
 }
 
-void AssertionPipeline::setProofGenerator(smt::PreprocessProofGenerator* pppg)
+void AssertionPipeline::enableProofs(smt::PreprocessProofGenerator* pppg)
 {
   d_pppg = pppg;
 }

diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index b6bd8a94ca0108e79fc93884a7dfb843dbb30ae3..5c75fba2b7ead957a8f48c891cdd20cb8d4420b4 100644 (file)
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -158,8 +158,14 @@ class AssertionPipeline
     return d_storeSubstsInAsserts && i == d_substsIndex;
   }
   //------------------------------------ for proofs
-  /** Set proof generator */
-  void setProofGenerator(smt::PreprocessProofGenerator* pppg);
+  /**
+   * Enable proofs for this assertions pipeline. This must be called
+   * explicitly since we construct the assertions pipeline before we know
+   * whether proofs are enabled.
+   *
+   * @param pppg The preprocess proof generator of the proof manager.
+   */
+  void enableProofs(smt::PreprocessProofGenerator* pppg);
   /** Is proof enabled? */
   bool isProofEnabled() const;
   //------------------------------------ end for proofs

diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 247a8b72ef5f5062f56ee17aff1800b8adc5b62e..ff672b3685191a7249cac6620cb838a21f928d0e 100644 (file)
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -54,10 +54,10 @@ NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
       d_statistics(statisticsRegistry()),
       d_pnm(d_env.getProofNodeManager()),
       d_llpg(d_pnm ? new smt::PreprocessProofGenerator(
-                         d_pnm, userContext(), "NonClausalSimp::llpg")
+                 d_env, userContext(), "NonClausalSimp::llpg")
                    : nullptr),
       d_llra(d_pnm ? new LazyCDProof(
-                         d_pnm, nullptr, userContext(), "NonClausalSimp::llra")
+                 d_pnm, nullptr, userContext(), "NonClausalSimp::llra")
                    : nullptr),
       d_tsubsList(userContext())
 {

diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 8d066c1ba6a2cef5f1813458309da2324cbe2325..0191bcb82976270abe0d9c6d6241ef612770c005 100644 (file)
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -251,9 +251,9 @@ void Assertions::ensureBoolean(const Node& n)
   }
 }
 
-void Assertions::setProofGenerator(smt::PreprocessProofGenerator* pppg)
+void Assertions::enableProofs(smt::PreprocessProofGenerator* pppg)
 {
-  d_assertions.setProofGenerator(pppg);
+  d_assertions.enableProofs(pppg);
 }
 
 bool Assertions::isProofEnabled() const

diff --git a/src/smt/assertions.h b/src/smt/assertions.h
index 5cda366e63c655d74d24ce52b2ec05f7385f1c67..96e5712a452c2008430633b1596f0e45c7a13a3a 100644 (file)
--- a/src/smt/assertions.h
+++ b/src/smt/assertions.h
@@ -126,8 +126,14 @@ class Assertions : protected EnvObj
   void flipGlobalNegated();
 
   //------------------------------------ for proofs
-  /** Set proof generator */
-  void setProofGenerator(smt::PreprocessProofGenerator* pppg);
+  /**
+   * Enable proofs for this assertions class. This must be called
+   * explicitly since we construct the assertions before we know
+   * whether proofs are enabled.
+   *
+   * @param pppg The preprocess proof generator of the proof manager.
+   */
+  void enableProofs(smt::PreprocessProofGenerator* pppg);
   /** Is proof enabled? */
   bool isProofEnabled() const;
   //------------------------------------ end for proofs

diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index 54aba6b71dbc6319e06d145ffb99e0319473638f..dd0cd36105b379d06eb10b2d5cc940e8f96d0d0d 100644 (file)
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -34,7 +34,7 @@ using namespace cvc5::kind;
 namespace cvc5 {
 namespace smt {
 
-ExpandDefs::ExpandDefs(Env& env) : d_env(env), d_tpg(nullptr) {}
+ExpandDefs::ExpandDefs(Env& env) : EnvObj(env), d_tpg(nullptr) {}
 
 ExpandDefs::~ExpandDefs() {}
 
@@ -164,11 +164,13 @@ TrustNode ExpandDefs::expandDefinitions(TNode n,
   return TrustNode::mkTrustRewrite(orig, res, tpg);
 }
 
-void ExpandDefs::setProofNodeManager(ProofNodeManager* pnm)
+void ExpandDefs::enableProofs()
 {
+  // initialize if not done already
   if (d_tpg == nullptr)
   {
-    d_tpg.reset(new TConvProofGenerator(pnm,
+    Assert(d_env.getProofNodeManager() != nullptr);
+    d_tpg.reset(new TConvProofGenerator(d_env.getProofNodeManager(),
                                         d_env.getUserContext(),
                                         TConvPolicy::FIXPOINT,
                                         TConvCachePolicy::NEVER,

diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index 8ecf276e245c529264964db639516cd1cf3bb7e3..669f56430f0b7237be88ef6cc7d52ba4402bc723 100644 (file)
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -22,10 +22,10 @@
 
 #include "expr/node.h"
 #include "proof/trust_node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
-class Env;
 class ProofNodeManager;
 class TConvProofGenerator;
 
@@ -37,7 +37,7 @@ namespace smt {
  * Its main features is expandDefinitions(TNode, ...), which returns the
  * expanded formula of a term.
  */
-class ExpandDefs
+class ExpandDefs : protected EnvObj
 {
  public:
   ExpandDefs(Env& env);
@@ -51,11 +51,8 @@ class ExpandDefs
    */
   Node expandDefinitions(TNode n, std::unordered_map<Node, Node>& cache);
 
-  /**
-   * Set proof node manager, which signals this class to enable proofs using the
-   * given proof node manager.
-   */
-  void setProofNodeManager(ProofNodeManager* pnm);
+  /** Enable proofs using the proof node manager of the env. */
+  void enableProofs();
 
  private:
   /**
@@ -65,8 +62,6 @@ class ExpandDefs
   TrustNode expandDefinitions(TNode n,
                               std::unordered_map<Node, Node>& cache,
                               TConvProofGenerator* tpg);
-  /** Reference to the environment. */
-  Env& d_env;
   /** A proof generator for the term conversion. */
   std::unique_ptr<TConvProofGenerator> d_tpg;
 };

diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index e2730151e6a851c08846a926b5836ccd6c952f2a..19a776587dcc93c3adb0d47e9ef4295409ed4af9 100644 (file)
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -23,22 +23,19 @@
 #include "proof/proof.h"
 #include "proof/proof_checker.h"
 #include "proof/proof_node.h"
+#include "smt/env.h"
 #include "theory/quantifiers/extended_rewrite.h"
-#include "theory/rewriter.h"
 
 namespace cvc5 {
 namespace smt {
 
-PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm,
-                                                   context::Context* c,
-                                                   std::string name,
-                                                   PfRule ra,
-                                                   PfRule rpp)
-    : d_pnm(pnm),
+PreprocessProofGenerator::PreprocessProofGenerator(
+    Env& env, context::Context* c, std::string name, PfRule ra, PfRule rpp)
+    : EnvObj(env),
       d_ctx(c ? c : &d_context),
       d_src(d_ctx),
-      d_helperProofs(pnm, d_ctx),
-      d_inputPf(pnm, c, "InputProof"),
+      d_helperProofs(env.getProofNodeManager(), d_ctx),
+      d_inputPf(env.getProofNodeManager(), c, "InputProof"),
       d_name(name),
       d_ra(ra),
       d_rpp(rpp)
@@ -131,7 +128,7 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
     return nullptr;
   }
   // make CDProof to construct the proof below
-  CDProof cdp(d_pnm);
+  CDProof cdp(d_env.getProofNodeManager());
 
   Node curr = f;
   std::vector<Node> transChildren;
@@ -180,7 +177,7 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
         if (!proofStepProcessed)
         {
           // maybe its just an (extended) rewrite?
-          Node pr = theory::Rewriter::callExtendedRewrite(proven[0]);
+          Node pr = extendedRewrite(proven[0]);
           if (proven[1] == pr)
           {
             Node idr = mkMethodId(MethodId::RW_EXT_REWRITE);
@@ -244,8 +241,6 @@ std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
   return cdp.getProofFor(f);
 }
 
-ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; }
-
 LazyCDProof* PreprocessProofGenerator::allocateHelperProof()
 {
   return d_helperProofs.allocateProof(nullptr, d_ctx);
@@ -259,7 +254,7 @@ void PreprocessProofGenerator::checkEagerPedantic(PfRule r)
   {
     // catch a pedantic failure now, which otherwise would not be
     // triggered since we are doing lazy proof generation
-    ProofChecker* pc = d_pnm->getChecker();
+    ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
     std::stringstream serr;
     if (pc->isPedanticFailure(r, serr))
     {

diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index a0e88b3e9e6bdedc40d546c67968a4209116e901..928ea7bf3297887fbe03d7f00ce615c8522bb483 100644 (file)
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -24,6 +24,7 @@
 #include "proof/proof_generator.h"
 #include "proof/proof_set.h"
 #include "proof/trust_node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
@@ -53,13 +54,13 @@ namespace smt {
  * whose free assumptions are intended to be input assertions, which are
  * implictly all assertions that are not notified to this class.
  */
-class PreprocessProofGenerator : public ProofGenerator
+class PreprocessProofGenerator : protected EnvObj, public ProofGenerator
 {
   typedef context::CDHashMap<Node, TrustNode> NodeTrustNodeMap;
 
  public:
   /**
-   * @param pnm The proof node manager
+   * @param env Reference to the environment
    * @param c The context this class depends on
    * @param name The name of this generator (for debugging)
    * @param ra The proof rule to use when no generator is provided for new
@@ -67,7 +68,7 @@ class PreprocessProofGenerator : public ProofGenerator
    * @param rpp The proof rule to use when no generator is provided for
    * preprocessing steps.
    */
-  PreprocessProofGenerator(ProofNodeManager* pnm,
+  PreprocessProofGenerator(Env& env,
                            context::Context* c = nullptr,
                            std::string name = "PreprocessProofGenerator",
                            PfRule ra = PfRule::PREPROCESS_LEMMA,
@@ -98,8 +99,6 @@ class PreprocessProofGenerator : public ProofGenerator
   std::shared_ptr<ProofNode> getProofFor(Node f) override;
   /** Identify */
   std::string identify() const override;
-  /** Get the proof manager */
-  ProofNodeManager* getManager();
   /**
    * Allocate a helper proof. This returns a fresh lazy proof object that
    * remains alive in the context. This feature is used to construct
@@ -114,8 +113,6 @@ class PreprocessProofGenerator : public ProofGenerator
    * to this class.
    */
   void checkEagerPedantic(PfRule r);
-  /** The proof node manager */
-  ProofNodeManager* d_pnm;
   /** A dummy context used by this class if none is provided */
   context::Context d_context;
   /** The context used here */

diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 0fdb569c82c07a0a7907f9a2b5b628552d4cd18e..d7167c04c4392a5c5cc4c1df1dec40d373fe1ebb 100644 (file)
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -42,8 +42,7 @@ Preprocessor::Preprocessor(Env& env,
       d_propagator(env, true, true),
       d_assertionsProcessed(env.getUserContext(), false),
       d_exDefs(env),
-      d_processor(env, stats),
-      d_pnm(nullptr)
+      d_processor(env, stats)
 {
 }
 
@@ -149,12 +148,11 @@ Node Preprocessor::simplify(const Node& node)
   return ret;
 }
 
-void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg)
+void Preprocessor::enableProofs(PreprocessProofGenerator* pppg)
 {
   Assert(pppg != nullptr);
-  d_pnm = pppg->getManager();
-  d_exDefs.setProofNodeManager(d_pnm);
-  d_propagator.setProof(d_pnm, userContext(), pppg);
+  d_exDefs.enableProofs();
+  d_propagator.enableProofs(userContext(), pppg);
 }
 
 }  // namespace smt

diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 957b5e36e6c5f263f6367dabd970eeff2b1c1a04..c91d106f5a38e643511dbc0f09485970ac7d1df7 100644 (file)
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -99,9 +99,13 @@ class Preprocessor : protected EnvObj
   /** Same as above, for a list of assertions, updating in place */
   void expandDefinitions(std::vector<Node>& ns);
   /**
-   * Set proof node manager. Enables proofs in this preprocessor.
+   * Enable proofs for this preprocessor. This must be called
+   * explicitly since we construct the preprocessor before we know
+   * whether proofs are enabled.
+   *
+   * @param pppg The preprocess proof generator of the proof manager.
    */
-  void setProofGenerator(PreprocessProofGenerator* pppg);
+  void enableProofs(PreprocessProofGenerator* pppg);
 
  private:
   /** Reference to the abstract values utility */
@@ -123,8 +127,6 @@ class Preprocessor : protected EnvObj
    * passes.
    */
   ProcessAssertions d_processor;
-  /** Proof node manager */
-  ProofNodeManager* d_pnm;
 };
 
 }  // namespace smt

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 04f6016808556b1e9ce5e06cff8a265173e091e0..798f7dd57eb68446d7d5ee9ce7909bf6108e94c6 100644 (file)
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -43,13 +43,15 @@ PfManager::PfManager(Env& env)
           options().proof.proofPedantic)),
       d_pnm(new ProofNodeManager(
           env.getOptions(), env.getRewriter(), d_pchecker.get())),
-      d_pppg(new PreprocessProofGenerator(
-          d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")),
+      d_pppg(nullptr),
       d_pfpp(nullptr),
       d_finalProof(nullptr)
 {
   // enable proof support in the environment/rewriter
   d_env.setProofNodeManager(d_pnm.get());
+  // now construct preprocess proof generator
+  d_pppg = std::make_unique<PreprocessProofGenerator>(
+      env, env.getUserContext(), "smt::PreprocessProofGenerator");
   // 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
@@ -67,11 +69,11 @@ PfManager::PfManager(Env& env)
   // be inferred from A, it was updated). This shape is problematic for
   // the Alethe reconstruction, so we disable the update of scoped
   // assumptions (which would disable the update of B1 in this case).
-  d_pfpp.reset(new ProofPostproccess(
+  d_pfpp = std::make_unique<ProofPostproccess>(
       env,
       d_pppg.get(),
       nullptr,
-      options().proof.proofFormatMode != options::ProofFormatMode::ALETHE));
+      options().proof.proofFormatMode != options::ProofFormatMode::ALETHE);
 
   // add rules to eliminate here
   if (options().proof.proofGranularityMode

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 32838eccff03ba574ab4d445a061859802decf02..13d061f1f8da2b09416a49960623245106c82730 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -192,9 +192,9 @@ void SolverEngine::finishInit()
     // start the unsat core manager
     d_ucManager.reset(new UnsatCoreManager());
     // enable it in the assertions pipeline
-    d_asserts->setProofGenerator(pppg);
+    d_asserts->enableProofs(pppg);
     // enabled proofs in the preprocessor
-    d_smtSolver->getPreprocessor()->setProofGenerator(pppg);
+    d_smtSolver->getPreprocessor()->enableProofs(pppg);
   }
 
   Trace("smt-debug") << "SolverEngine::finishInit" << std::endl;

diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index 95b31eab227a7a895f4bb568404b931ea1712600..1299a493a42b525d16f908c9e504c5a8277728f0 100644 (file)
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -81,8 +81,6 @@ class AbstractValues;
 class Assertions;
 class ResourceOutListener;
 class SmtNodeManagerListener;
-class OptionsManager;
-class Preprocessor;
 class CheckModels;
 /** Subsolvers */
 class SmtSolver;

diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 714dcfb01d721ceaafdd551c5544ea370616dc63..b570b6b3665352ab40cc4b4a0e2b08f727d8a37c 100644 (file)
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -767,21 +767,21 @@ TrustNode CircuitPropagator::propagate()
   return d_conflict;
 }
 
-void CircuitPropagator::setProof(ProofNodeManager* pnm,
-                                 context::Context* ctx,
-                                 ProofGenerator* defParent)
+void CircuitPropagator::enableProofs(context::Context* ctx,
+                                     ProofGenerator* defParent)
 {
-  d_pnm = pnm;
-  d_epg.reset(new EagerProofGenerator(pnm, ctx));
+  d_pnm = d_env.getProofNodeManager();
+  Assert(d_pnm != nullptr);
+  d_epg.reset(new EagerProofGenerator(d_pnm, ctx));
   d_proofInternal.reset(new LazyCDProofChain(
-      pnm, true, ctx, d_epg.get(), true, "CircuitPropInternalLazyChain"));
+      d_pnm, true, ctx, d_epg.get(), true, "CircuitPropInternalLazyChain"));
   if (defParent != nullptr)
   {
     // If we provide a parent proof generator (defParent), we want the ASSUME
     // leafs of proofs provided by this class to call the getProofFor method on
     // the parent. To do this, we use a LazyCDProofChain.
     d_proofExternal.reset(new LazyCDProofChain(
-        pnm, true, ctx, defParent, false, "CircuitPropExternalLazyChain"));
+        d_pnm, true, ctx, defParent, false, "CircuitPropExternalLazyChain"));
   }
 }
 

diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index fa55e2711f7aae010783a4dff6e18926af3d6f37..01bc0ad35b1ffd39a338303305806815ce4ea77d 100644 (file)
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -134,14 +134,12 @@ class CircuitPropagator : protected EnvObj
     return false;
   }
   /**
-   * Set proof node manager, context and parent proof generator.
+   * Enable proofs based on context and parent proof generator.
    *
    * If parent is non-null, then it is responsible for the proofs provided
    * to this class.
    */
-  void setProof(ProofNodeManager* pnm,
-                context::Context* ctx,
-                ProofGenerator* defParent);
+  void enableProofs(context::Context* ctx, ProofGenerator* defParent);
 
  private:
   /** A context-notify object that clears out stale data. */