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

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

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 0308715e63f65b6408bc7580f573b2d237eb0db7..dd22416dbc1fa9f3baa88c4ec110d0cbc2a174fb 100644 (file)
--- 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 4d06adfba914828bf63245160f5360cd1bcca444..d26a425c8f1d3b87574ee2bb4606b9163f55d25d 100644 (file)
--- 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 47263af978cbceb88b36131410cd8d15b8f8a4e8..b4bc7fa60194003d9d9f3598071dbe7e4b432388 100644 (file)
--- 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 f988c00e2060406274342f7ae90008786db905a0..0e54ff8c93f28451624d56534a08dfb48c18971c 100644 (file)
--- 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

diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 3ec9899ad3c2a5cbc7a8a7cc45a72fdfe5cfdc6d..d6677c3435470e9f2a0171e2881a86d8e0356818 100644 (file)
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -85,6 +85,14 @@ ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
 
 const std::string& Env::getFilename() const { return d_filename; }
 
+bool Env::isSatProofProducing() const
+{
+  return d_proofNodeManager != nullptr
+         && (!d_options.smt.unsatCores
+             || d_options.smt.unsatCoresMode
+                    != options::UnsatCoresMode::ASSUMPTIONS);
+}
+
 bool Env::isTheoryProofProducing() const
 {
   return d_proofNodeManager != nullptr

diff --git a/src/smt/env.h b/src/smt/env.h
index 9887aea081feb1f9d0f11454f0991fefa6e42b41..68148ec00a2b3b9cedd9a1fa8a6d62dae5fb46cc 100644 (file)
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -85,6 +85,13 @@ class Env
   /** Return the input name, or the empty string if not set */
   const std::string& getFilename() const;
 
+  /**
+   * Check whether the SAT solver should produce proofs. Other than whether
+   * the proof node manager is set, SAT proofs are only generated when the
+   * unsat core mode is not ASSUMPTIONS.
+   */
+  bool isSatProofProducing() const;
+
   /**
    * Check whether theories should produce proofs as well. Other than whether
    * the proof node manager is set, theory engine proofs are conditioned on the

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 43177a73a1dfdcf749ada39ed01f83474d201a6f..78bb9044a30cc3212a9b49bd3095b1f47119ee53 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -213,8 +213,6 @@ void SmtEngine::finishInit()
     d_env->setProofNodeManager(pnm);
     // enable it in the assertions pipeline
     d_asserts->setProofGenerator(pppg);
-    // enable it in the SmtSolver
-    d_smtSolver->setProofNodeManager(pnm);
     // enabled proofs in the preprocessor
     d_pp->setProofGenerator(pppg);
   }

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 1014b218d36327700dffe078da67a2c93623b698..214193b00701a2cf61442681765609a0972b2f84 100644 (file)
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -40,7 +40,6 @@ SmtSolver::SmtSolver(Env& env,
       d_state(state),
       d_pp(pp),
       d_stats(stats),
-      d_pnm(nullptr),
       d_theoryEngine(nullptr),
       d_propEngine(nullptr)
 {
@@ -61,16 +60,17 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
     theory::TheoryConstructor::addTheory(d_theoryEngine.get(), id);
   }
   // Add the proof checkers for each theory
-  if (d_pnm)
+  ProofNodeManager* pnm = d_env.getProofNodeManager();
+  if (pnm)
   {
-    d_theoryEngine->initializeProofChecker(d_pnm->getChecker());
+    d_theoryEngine->initializeProofChecker(pnm->getChecker());
   }
   Trace("smt-debug") << "Making prop engine..." << std::endl;
   /* force destruction of referenced PropEngine to enforce that statistics
    * are unregistered by the obsolete PropEngine object before registered
    * again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env, d_pnm));
+  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env));
 
   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
   d_theoryEngine->setPropEngine(getPropEngine());
@@ -86,7 +86,7 @@ void SmtSolver::resetAssertions()
    * statistics are unregistered by the obsolete PropEngine object before
    * registered again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env, d_pnm));
+  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), d_env));
   d_theoryEngine->setPropEngine(getPropEngine());
   // Notice that we do not reset TheoryEngine, nor does it require calling
   // finishInit again. In particular, TheoryEngine::finishInit does not
@@ -236,8 +236,6 @@ void SmtSolver::processAssertions(Assertions& as)
   as.clearCurrent();
 }
 
-void SmtSolver::setProofNodeManager(ProofNodeManager* pnm) { d_pnm = pnm; }
-
 TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); }
 
 prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); }

diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index cf82d93093eefb57f610e37d9232a9a5994b0171..cdc98606ceb6eb01138828a26b191bc8f3e8d9f9 100644 (file)
--- a/src/smt/smt_solver.h
+++ b/src/smt/smt_solver.h
@@ -114,11 +114,6 @@ class SmtSolver
    * into the SMT solver, and clears the buffer.
    */
   void processAssertions(Assertions& as);
-  /**
-   * Set proof node manager. Enables proofs in this SmtSolver. Should be
-   * called before finishInit.
-   */
-  void setProofNodeManager(ProofNodeManager* pnm);
   //------------------------------------------ access methods
   /** Get a pointer to the TheoryEngine owned by this solver. */
   TheoryEngine* getTheoryEngine();
@@ -139,11 +134,6 @@ class SmtSolver
   Preprocessor& d_pp;
   /** Reference to the statistics of SmtEngine */
   SmtEngineStatistics& d_stats;
-  /**
-   * Pointer to the proof node manager used by this SmtSolver. A non-null
-   * proof node manager indicates that proofs are enabled.
-   */
-  ProofNodeManager* d_pnm;
   /** The theory engine */
   std::unique_ptr<TheoryEngine> d_theoryEngine;
   /** The propositional engine */