Make TheoryProxy use Env, simplify initialization of PropEngine (#7031)

This simplifies our management of how/when proofs are enabled in the PropEngine.

4 files changed, 28 insertions, 40 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 0308715e6..dd22416db 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -65,16 +65,13 @@ public:
   }
 };
 
-PropEngine::PropEngine(TheoryEngine* te,
-                       Env& env,
-                       ProofNodeManager* pnm)
+PropEngine::PropEngine(TheoryEngine* te, Env& env)
     : d_inCheckSat(false),
       d_theoryEngine(te),
       d_env(env),
       d_skdm(new SkolemDefManager(d_env.getContext(), d_env.getUserContext())),
       d_theoryProxy(nullptr),
       d_satSolver(nullptr),
-      d_pnm(pnm),
       d_cnfStream(nullptr),
       d_pfCnfStream(nullptr),
       d_ppm(nullptr),
@@ -84,6 +81,7 @@ PropEngine::PropEngine(TheoryEngine* te,
   Debug("prop") << "Constructing the PropEngine" << std::endl;
   context::Context* satContext = d_env.getContext();
   context::UserContext* userContext = d_env.getUserContext();
+  ProofNodeManager* pnm = d_env.getProofNodeManager();
   ResourceManager* rm = d_env.getResourceManager();
 
   options::DecisionMode dmode = options::decisionMode();
@@ -107,13 +105,8 @@ PropEngine::PropEngine(TheoryEngine* te,
 
   // CNF stream and theory proxy required pointers to each other, make the
   // theory proxy first
-  d_theoryProxy = new TheoryProxy(this,
-                                  d_theoryEngine,
-                                  d_decisionEngine.get(),
-                                  d_skdm.get(),
-                                  satContext,
-                                  userContext,
-                                  pnm);
+  d_theoryProxy = new TheoryProxy(
+      this, d_theoryEngine, d_decisionEngine.get(), d_skdm.get(), d_env);
   d_cnfStream = new CnfStream(d_satSolver,
                               d_theoryProxy,
                               userContext,
@@ -124,17 +117,15 @@ PropEngine::PropEngine(TheoryEngine* te,
 
   // connect theory proxy
   d_theoryProxy->finishInit(d_cnfStream);
+  bool satProofs = d_env.isSatProofProducing();
   // connect SAT solver
-  d_satSolver->initialize(
-      d_env.getContext(),
-      d_theoryProxy,
-      d_env.getUserContext(),
-      options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS
-          ? pnm
-          : nullptr);
+  d_satSolver->initialize(d_env.getContext(),
+                          d_theoryProxy,
+                          d_env.getUserContext(),
+                          satProofs ? pnm : nullptr);
 
   d_decisionEngine->finishInit(d_satSolver, d_cnfStream);
-  if (pnm && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS)
+  if (satProofs)
   {
     d_pfCnfStream.reset(new ProofCnfStream(
         userContext,
@@ -670,7 +661,7 @@ bool PropEngine::properExplanation(TNode node, TNode expl) const
 
 void PropEngine::checkProof(context::CDList<Node>* assertions)
 {
-  if (!d_pnm)
+  if (!d_env.isSatProofProducing())
   {
     return;
   }
@@ -681,7 +672,7 @@ ProofCnfStream* PropEngine::getProofCnfStream() { return d_pfCnfStream.get(); }
 
 std::shared_ptr<ProofNode> PropEngine::getProof()
 {
-  if (!d_pnm)
+  if (!d_env.isSatProofProducing())
   {
     return nullptr;
   }
@@ -706,7 +697,7 @@ std::shared_ptr<ProofNode> PropEngine::getRefutation()
   Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS);
   std::vector<Node> core;
   getUnsatCore(core);
-  CDProof cdp(d_pnm);
+  CDProof cdp(d_env.getProofNodeManager());
   Node fnode = NodeManager::currentNM()->mkConst(false);
   cdp.addStep(fnode, PfRule::SAT_REFUTATION, core, {});
   return cdp.getProofFor(fnode);
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 4d06adfba..d26a425c8 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -56,9 +56,7 @@ class PropEngine
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(TheoryEngine* te,
-             Env& env,
-             ProofNodeManager* pnm);
+  PropEngine(TheoryEngine* te, Env& env);
 
   /**
    * Destructor.
@@ -372,9 +370,6 @@ class PropEngine
   /** List of all of the assertions that need to be made */
   std::vector<Node> d_assertionList;
 
-  /** A pointer to the proof node maneger to be used by this engine. */
-  ProofNodeManager* d_pnm;
-
   /** The CNF converter in use */
   CnfStream* d_cnfStream;
   /** Proof-producing CNF converter */
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 47263af97..b4bc7fa60 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -24,6 +24,7 @@
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "prop/skolem_def_manager.h"
+#include "smt/env.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
@@ -36,16 +37,15 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
                          TheoryEngine* theoryEngine,
                          decision::DecisionEngine* decisionEngine,
                          SkolemDefManager* skdm,
-                         context::Context* context,
-                         context::UserContext* userContext,
-                         ProofNodeManager* pnm)
+                         Env& env)
     : d_propEngine(propEngine),
       d_cnfStream(nullptr),
       d_decisionEngine(decisionEngine),
       d_theoryEngine(theoryEngine),
-      d_queue(context),
-      d_tpp(*theoryEngine, userContext, pnm),
-      d_skdm(skdm)
+      d_queue(env.getContext()),
+      d_tpp(*theoryEngine, env.getUserContext(), env.getProofNodeManager()),
+      d_skdm(skdm),
+      d_env(env)
 {
 }
 
@@ -98,8 +98,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
 
   TrustNode tte = d_theoryEngine->getExplanation(lNode);
   Node theoryExplanation = tte.getNode();
-  if (options::produceProofs()
-      && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS)
+  if (d_env.isTheoryProofProducing())
   {
     Assert(options::unsatCoresMode() != options::UnsatCoresMode::FULL_PROOF
            || tte.getGenerator());
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index f988c00e2..0e54ff8c9 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -35,10 +35,12 @@
 
 namespace cvc5 {
 
+class Env;
+class TheoryEngine;
+
 namespace decision {
 class DecisionEngine;
 }
-class TheoryEngine;
 
 namespace prop {
 
@@ -56,9 +58,7 @@ class TheoryProxy : public Registrar
               TheoryEngine* theoryEngine,
               decision::DecisionEngine* decisionEngine,
               SkolemDefManager* skdm,
-              context::Context* context,
-              context::UserContext* userContext,
-              ProofNodeManager* pnm);
+              Env& env);
 
   ~TheoryProxy();
 
@@ -162,6 +162,9 @@ class TheoryProxy : public Registrar
 
   /** The skolem definition manager */
   SkolemDefManager* d_skdm;
+
+  /** Reference to the environment */
+  Env& d_env;
 }; /* class TheoryProxy */
 
 }  // namespace prop