Refactor theory inference manager constructor (#7457)

Eliminates a style where proof node manager was passed as an argument to indicate proofs enabled if non-null. All theory inference managers now check Env::isTheoryProofProducing instead.

Since BV did not pass a proof node manager to its inference manager, this PR also incidentally enables equality engine proofs for BV.

diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index 0c6b18893279826326656d23769998845402c943..670f38c403b5bfac3d18bfde659aacbb9faaf511 100644 (file)
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -26,9 +26,8 @@ namespace arith {
 
 InferenceManager::InferenceManager(Env& env,
                                    TheoryArith& ta,
-                                   ArithState& astate,
-                                   ProofNodeManager* pnm)
-    : InferenceManagerBuffered(env, ta, astate, pnm, "theory::arith::"),
+                                   ArithState& astate)
+    : InferenceManagerBuffered(env, ta, astate, "theory::arith::"),
       // currently must track propagated literals if using the equality solver
       d_trackPropLits(options().arith.arithEqSolver),
       d_propLits(context())

diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h
index d327106d733750340cfbb0e766cfc82c3885f155..11532fd7219ef297aa5709e3acb9bbb8ca88ff24 100644 (file)
--- a/src/theory/arith/inference_manager.h
+++ b/src/theory/arith/inference_manager.h
@@ -46,10 +46,7 @@ class InferenceManager : public InferenceManagerBuffered
   using NodeSet = context::CDHashSet<Node>;
 
  public:
-  InferenceManager(Env& env,
-                   TheoryArith& ta,
-                   ArithState& astate,
-                   ProofNodeManager* pnm);
+  InferenceManager(Env& env, TheoryArith& ta, ArithState& astate);
 
   /**
    * Add a lemma as pending lemma to this inference manager.

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index cf2373b9fa6535f621c594e5a624aad9eb0a3f79..583b53d5e14da341ae7a7d934d8cf78981081b9a 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -40,7 +40,7 @@ TheoryArith::TheoryArith(Env& env, OutputChannel& out, Valuation valuation)
       d_ppRewriteTimer(
           statisticsRegistry().registerTimer("theory::arith::ppRewriteTimer")),
       d_astate(env, valuation),
-      d_im(env, *this, d_astate, d_pnm),
+      d_im(env, *this, d_astate),
       d_ppre(d_env),
       d_bab(env, d_astate, d_im, d_ppre, d_pnm),
       d_eqSolver(nullptr),

diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index 4eef9a018c7ca6a8b2098bb6e920e97bae078fc3..caef4502be767c7cfbce241a3a130a75e6e371e5 100644 (file)
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -27,13 +27,12 @@ namespace cvc5 {
 namespace theory {
 namespace arrays {
 
-InferenceManager::InferenceManager(Env& env,
-                                   Theory& t,
-                                   TheoryState& state,
-                                   ProofNodeManager* pnm)
-    : TheoryInferenceManager(env, t, state, pnm, "theory::arrays::", false),
-      d_lemmaPg(pnm ? new EagerProofGenerator(
-                    pnm, userContext(), "ArrayLemmaProofGenerator")
+InferenceManager::InferenceManager(Env& env, Theory& t, TheoryState& state)
+    : TheoryInferenceManager(env, t, state, "theory::arrays::", false),
+      d_lemmaPg(isProofEnabled()
+                    ? new EagerProofGenerator(env.getProofNodeManager(),
+                                              userContext(),
+                                              "ArrayLemmaProofGenerator")
                     : nullptr)
 {
 }

diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h
index 899df0a6be89ac7da8e2da8a558fc1857fbc117c..f0e3bfe9084ac26feb0674006bcc84bb803c08fb 100644 (file)
--- a/src/theory/arrays/inference_manager.h
+++ b/src/theory/arrays/inference_manager.h
@@ -33,10 +33,7 @@ namespace arrays {
 class InferenceManager : public TheoryInferenceManager
 {
  public:
-  InferenceManager(Env& env,
-                   Theory& t,
-                   TheoryState& state,
-                   ProofNodeManager* pnm);
+  InferenceManager(Env& env, Theory& t, TheoryState& state);
   ~InferenceManager() {}
 
   /**

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 93eadde43c609aa5deabdd0d4883fb7f019ba682..97cbec1d5baee0647a931d793ae0d06645f09459 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -81,7 +81,7 @@ TheoryArrays::TheoryArrays(Env& env,
       d_ppFacts(userContext()),
       d_rewriter(env.getRewriter(), d_pnm),
       d_state(env, valuation),
-      d_im(env, *this, d_state, d_pnm),
+      d_im(env, *this, d_state),
       d_literalsToPropagate(context()),
       d_literalsToPropagateIndex(context(), 0),
       d_isPreRegistered(context()),

diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp
index ee25861be3b4d3f1d34f30055d46ae4e125c60b1..92f5dfd82f0105f18b24ae73ba030f227cfc56ed 100644 (file)
--- a/src/theory/bags/inference_manager.cpp
+++ b/src/theory/bags/inference_manager.cpp
@@ -24,11 +24,8 @@ namespace cvc5 {
 namespace theory {
 namespace bags {
 
-InferenceManager::InferenceManager(Env& env,
-                                   Theory& t,
-                                   SolverState& s,
-                                   ProofNodeManager* pnm)
-    : InferenceManagerBuffered(env, t, s, pnm, "theory::bags::"), d_state(s)
+InferenceManager::InferenceManager(Env& env, Theory& t, SolverState& s)
+    : InferenceManagerBuffered(env, t, s, "theory::bags::"), d_state(s)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);

diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h
index a9e8d9121fced6f693a23dd48cc96cd5853b7935..45827f27b6e1e0cc6058410ebf2b5e8e6765d245 100644 (file)
--- a/src/theory/bags/inference_manager.h
+++ b/src/theory/bags/inference_manager.h
@@ -38,7 +38,7 @@ class InferenceManager : public InferenceManagerBuffered
   typedef context::CDHashSet<Node> NodeSet;
 
  public:
-  InferenceManager(Env& env, Theory& t, SolverState& s, ProofNodeManager* pnm);
+  InferenceManager(Env& env, Theory& t, SolverState& s);
 
   /**
    * Do pending method. This processes all pending facts, lemmas and pending

diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 004766d83a00480a2aff26e202cd6e21cf5719f6..4a6d345e98f0c57b860b713f4da1f29b9029447b 100644 (file)
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -30,7 +30,7 @@ namespace bags {
 TheoryBags::TheoryBags(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_BAGS, env, out, valuation),
       d_state(env, valuation),
-      d_im(env, *this, d_state, d_pnm),
+      d_im(env, *this, d_state),
       d_ig(&d_state, &d_im),
       d_notify(*this, d_im),
       d_statistics(),

diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index cd3b27b6e7180ca59e20eff254764158c6cc9668..e519cbed763d50558002ca3c111b6f9129e9dba0 100644 (file)
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -29,7 +29,7 @@ TheoryBuiltin::TheoryBuiltin(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_BUILTIN, env, out, valuation),
       d_checker(env),
       d_state(env, valuation),
-      d_im(env, *this, d_state, d_pnm, "theory::builtin::")
+      d_im(env, *this, d_state, "theory::builtin::")
 {
   // indicate we are using the default theory state and inference managers
   d_theoryState = &d_state;

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index f027b56fefe0381f52f38e193a9e9796e84fc23e..8e9c2da5b08f4285fcd5b3c6c2465a2a0bdf3dd7 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -40,7 +40,7 @@ TheoryBV::TheoryBV(Env& env,
       d_internal(nullptr),
       d_rewriter(),
       d_state(env, valuation),
-      d_im(env, *this, d_state, nullptr, "theory::bv::"),
+      d_im(env, *this, d_state, "theory::bv::"),
       d_notify(d_im),
       d_invalidateModelCache(context(), true),
       d_stats(statisticsRegistry(), "theory::bv::")

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 16a62101277b70d4ee4ea0b735770e22898a916b..fef85f4c662b1b1cce09ad0663ff221911473044 100644 (file)
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -30,16 +30,16 @@ namespace cvc5 {
 namespace theory {
 namespace datatypes {
 
-InferenceManager::InferenceManager(Env& env,
-                                   Theory& t,
-                                   TheoryState& state,
-                                   ProofNodeManager* pnm)
-    : InferenceManagerBuffered(env, t, state, pnm, "theory::datatypes::"),
-      d_pnm(pnm),
-      d_ipc(pnm == nullptr ? nullptr : new InferProofCons(context(), pnm)),
-      d_lemPg(pnm == nullptr ? nullptr
-                             : new EagerProofGenerator(
-                                 pnm, userContext(), "datatypes::lemPg"))
+InferenceManager::InferenceManager(Env& env, Theory& t, TheoryState& state)
+    : InferenceManagerBuffered(env, t, state, "theory::datatypes::"),
+      d_ipc(isProofEnabled()
+                ? new InferProofCons(context(), env.getProofNodeManager())
+                : nullptr),
+      d_lemPg(isProofEnabled()
+                  ? new EagerProofGenerator(env.getProofNodeManager(),
+                                            userContext(),
+                                            "datatypes::lemPg")
+                  : nullptr)
 {
   d_false = NodeManager::currentNM()->mkConst(false);
 }
@@ -103,15 +103,14 @@ void InferenceManager::sendDtConflict(const std::vector<Node>& conf, InferenceId
   conflictExp(id, conf, d_ipc.get());
 }
 
-bool InferenceManager::isProofEnabled() const { return d_ipc != nullptr; }
-
 TrustNode InferenceManager::processDtLemma(Node conc, Node exp, InferenceId id)
 {
   // set up a proof constructor
   std::shared_ptr<InferProofCons> ipcl;
   if (isProofEnabled())
   {
-    ipcl = std::make_shared<InferProofCons>(nullptr, d_pnm);
+    ipcl =
+        std::make_shared<InferProofCons>(nullptr, d_env.getProofNodeManager());
   }
   conc = prepareDtInference(conc, exp, id, ipcl.get());
   // send it as a lemma
@@ -133,7 +132,7 @@ TrustNode InferenceManager::processDtLemma(Node conc, Node exp, InferenceId id)
     {
       std::vector<Node> expv;
       expv.push_back(exp);
-      pn = d_pnm->mkScope(pbody, expv);
+      pn = d_env.getProofNodeManager()->mkScope(pbody, expv);
     }
     d_lemPg->setProofFor(lem, pn);
   }

diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h
index 27e0e90b6d2e260479a4d7ccd1e57f01c6b1b59e..2616eb40a701b1c07fd78eb839c5a4201481cca0 100644 (file)
--- a/src/theory/datatypes/inference_manager.h
+++ b/src/theory/datatypes/inference_manager.h
@@ -38,10 +38,7 @@ class InferenceManager : public InferenceManagerBuffered
   friend class DatatypesInference;
 
  public:
-  InferenceManager(Env& env,
-                   Theory& t,
-                   TheoryState& state,
-                   ProofNodeManager* pnm);
+  InferenceManager(Env& env, Theory& t, TheoryState& state);
   ~InferenceManager();
   /**
    * Add pending inference, which may be processed as either a fact or
@@ -78,8 +75,6 @@ class InferenceManager : public InferenceManagerBuffered
   void sendDtConflict(const std::vector<Node>& conf, InferenceId id);
 
  private:
-  /** Are proofs enabled? */
-  bool isProofEnabled() const;
   /**
    * Process datatype inference as a lemma
    */
@@ -103,8 +98,6 @@ class InferenceManager : public InferenceManagerBuffered
   Node prepareDtInference(Node conc, Node exp, InferenceId id, InferProofCons* ipc);
   /** The false node */
   Node d_false;
-  /** Pointer to the proof node manager */
-  ProofNodeManager* d_pnm;
   /** The inference to proof converter */
   std::unique_ptr<InferProofCons> d_ipc;
   /** An eager proof generator for lemmas */

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 0cbeaa515c202a76bd0cf31972eaa4b7fc3c308c..fe48aa59dc026c7b98eec5c06affb1a97af66951 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -63,7 +63,7 @@ TheoryDatatypes::TheoryDatatypes(Env& env,
       d_sygusExtension(nullptr),
       d_rewriter(env.getEvaluator()),
       d_state(env, valuation),
-      d_im(env, *this, d_state, d_pnm),
+      d_im(env, *this, d_state),
       d_notify(d_im, *this)
 {
 

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index d38b6d0fa2112870137627dd7ef5b4d33d04da01..8364aa81b98f9c0451ed688115501ca21de701cc 100644 (file)
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -68,7 +68,7 @@ TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation)
       d_abstractionMap(userContext()),
       d_rewriter(userContext()),
       d_state(env, valuation),
-      d_im(env, *this, d_state, d_pnm, "theory::fp::", true),
+      d_im(env, *this, d_state, "theory::fp::", true),
       d_wbFactsCache(userContext()),
       d_true(d_env.getNodeManager()->mkConst(true))
 {

diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 5b0dac776c149ee1cf1ea38cea10567464955d75..d38fcf3e335dfe9e4ab33119e3e10b9157c34842 100644 (file)
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -27,10 +27,9 @@ namespace theory {
 InferenceManagerBuffered::InferenceManagerBuffered(Env& env,
                                                    Theory& t,
                                                    TheoryState& state,
-                                                   ProofNodeManager* pnm,
                                                    const std::string& statsName,
                                                    bool cacheLemmas)
-    : TheoryInferenceManager(env, t, state, pnm, statsName, cacheLemmas),
+    : TheoryInferenceManager(env, t, state, statsName, cacheLemmas),
       d_processingPendingLemmas(false)
 {
 }

diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index 202948d26d85bdd9872230158166b56d943dfc06..e93152f72cb2c32fda65429d0378fd2f1e48b7c5 100644 (file)
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -35,7 +35,6 @@ class InferenceManagerBuffered : public TheoryInferenceManager
   InferenceManagerBuffered(Env& env,
                            Theory& t,
                            TheoryState& state,
-                           ProofNodeManager* pnm,
                            const std::string& statsName,
                            bool cacheLemmas = true);
   virtual ~InferenceManagerBuffered() {}

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index be04f94047004458f9efd4e9c8f97a2ad8d854a5..f47a71926dd40917247b7ed9d551adb5e85e8069 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -46,18 +46,18 @@ Instantiate::Instantiate(Env& env,
                          QuantifiersState& qs,
                          QuantifiersInferenceManager& qim,
                          QuantifiersRegistry& qr,
-                         TermRegistry& tr,
-                         ProofNodeManager* pnm)
+                         TermRegistry& tr)
     : QuantifiersUtil(env),
       d_qstate(qs),
       d_qim(qim),
       d_qreg(qr),
       d_treg(tr),
-      d_pnm(pnm),
       d_insts(userContext()),
       d_c_inst_match_trie_dom(userContext()),
-      d_pfInst(pnm ? new CDProof(pnm, userContext(), "Instantiate::pfInst")
-                   : nullptr)
+      d_pfInst(isProofEnabled() ? new CDProof(env.getProofNodeManager(),
+                                              userContext(),
+                                              "Instantiate::pfInst")
+                                : nullptr)
 {
 }
 
@@ -242,8 +242,10 @@ bool Instantiate::addInstantiation(Node q,
   std::shared_ptr<LazyCDProof> pfTmp;
   if (isProofEnabled())
   {
-    pfTmp.reset(new LazyCDProof(
-        d_pnm, nullptr, nullptr, "Instantiate::LazyCDProof::tmp"));
+    pfTmp.reset(new LazyCDProof(d_env.getProofNodeManager(),
+                                nullptr,
+                                nullptr,
+                                "Instantiate::LazyCDProof::tmp"));
   }
 
   // construct the instantiation
@@ -300,7 +302,8 @@ bool Instantiate::addInstantiation(Node q,
     // make the scope proof to get (=> q body)
     std::vector<Node> assumps;
     assumps.push_back(q);
-    std::shared_ptr<ProofNode> pfns = d_pnm->mkScope({pfn}, assumps);
+    std::shared_ptr<ProofNode> pfns =
+        d_env.getProofNodeManager()->mkScope({pfn}, assumps);
     Assert(assumps.size() == 1 && assumps[0] == q);
     // store in the main proof
     d_pfInst->addProof(pfns);
@@ -688,7 +691,10 @@ void Instantiate::getInstantiations(Node q, std::vector<Node>& insts)
   }
 }
 
-bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; }
+bool Instantiate::isProofEnabled() const
+{
+  return d_env.isTheoryProofProducing();
+}
 
 void Instantiate::notifyEndRound()
 {

diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index b4972a7b6f97d6a2250c2b5d96f524c9a4f52ae6..2e5bd1e2fe44bd0ccc0f25ccb8de61e7dddf239c 100644 (file)
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -108,8 +108,7 @@ class Instantiate : public QuantifiersUtil
               QuantifiersState& qs,
               QuantifiersInferenceManager& qim,
               QuantifiersRegistry& qr,
-              TermRegistry& tr,
-              ProofNodeManager* pnm = nullptr);
+              TermRegistry& tr);
   ~Instantiate();
   /** reset */
   bool reset(Theory::Effort e) override;
@@ -318,8 +317,6 @@ class Instantiate : public QuantifiersUtil
   QuantifiersRegistry& d_qreg;
   /** Reference to the term registry */
   TermRegistry& d_treg;
-  /** pointer to the proof node manager */
-  ProofNodeManager* d_pnm;
   /** instantiation rewriter classes */
   std::vector<InstantiationRewriter*> d_instRewrite;
 

diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp
index 20987b02e46fd2d427e83c299a5e1a1cd26ea77e..f282b8d119ec71757b6b9ae56f0c53af39ac91ab 100644 (file)
--- a/src/theory/quantifiers/quantifiers_inference_manager.cpp
+++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp
@@ -27,11 +27,10 @@ QuantifiersInferenceManager::QuantifiersInferenceManager(
     Theory& t,
     QuantifiersState& state,
     QuantifiersRegistry& qr,
-    TermRegistry& tr,
-    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(env, t, state, pnm, "theory::quantifiers::"),
-      d_instantiate(new Instantiate(env, state, *this, qr, tr, pnm)),
-      d_skolemize(new Skolemize(env, state, tr, pnm))
+    TermRegistry& tr)
+    : InferenceManagerBuffered(env, t, state, "theory::quantifiers::"),
+      d_instantiate(new Instantiate(env, state, *this, qr, tr)),
+      d_skolemize(new Skolemize(env, state, tr))
 {
 }
 

diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h
index 20981a795953debc9b117b12551f44d974f5cf0d..abd8d07613db22b14306e89f3fbf80a37819a78a 100644 (file)
--- a/src/theory/quantifiers/quantifiers_inference_manager.h
+++ b/src/theory/quantifiers/quantifiers_inference_manager.h
@@ -40,8 +40,7 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered
                               Theory& t,
                               QuantifiersState& state,
                               QuantifiersRegistry& qr,
-                              TermRegistry& tr,
-                              ProofNodeManager* pnm);
+                              TermRegistry& tr);
   ~QuantifiersInferenceManager();
   /** get instantiate utility */
   Instantiate* getInstantiate();

diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index a34547f453a372bad8c8a27c5d835e355d66ceca..830847b741f493e348f58265a4632331d9ce30f4 100644 (file)
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -36,18 +36,16 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-Skolemize::Skolemize(Env& env,
-                     QuantifiersState& qs,
-                     TermRegistry& tr,
-                     ProofNodeManager* pnm)
+Skolemize::Skolemize(Env& env, QuantifiersState& qs, TermRegistry& tr)
     : EnvObj(env),
       d_qstate(qs),
       d_treg(tr),
       d_skolemized(userContext()),
-      d_pnm(pnm),
-      d_epg(pnm == nullptr
+      d_epg(!isProofEnabled()
                 ? nullptr
-                : new EagerProofGenerator(pnm, userContext(), "Skolemize::epg"))
+                : new EagerProofGenerator(env.getProofNodeManager(),
+                                          userContext(),
+                                          "Skolemize::epg"))
 {
 }
 
@@ -397,7 +395,10 @@ void Skolemize::getSkolemTermVectors(
   }
 }
 
-bool Skolemize::isProofEnabled() const { return d_epg != nullptr; }
+bool Skolemize::isProofEnabled() const
+{
+  return d_env.isTheoryProofProducing();
+}
 
 }  // namespace quantifiers
 }  // namespace theory

diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index 294ad0084389bb8d703a5deb1a1ac9f9ebf67c72..604bc60e46677405d421a193c4b91430682a00a3 100644 (file)
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -69,10 +69,7 @@ class Skolemize : protected EnvObj
   typedef context::CDHashMap<Node, Node> NodeNodeMap;
 
  public:
-  Skolemize(Env& env,
-            QuantifiersState& qs,
-            TermRegistry& tr,
-            ProofNodeManager* pnm);
+  Skolemize(Env& env, QuantifiersState& qs, TermRegistry& tr);
   ~Skolemize() {}
   /** skolemize quantified formula q
    * If the return value ret of this function is non-null, then ret is a trust

diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 7e20c3a4ac1562575faf5e6aa3b7e813a4d44a88..bce827bbda8c5e78d15354371f63943fe328a48e 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -38,7 +38,7 @@ TheoryQuantifiers::TheoryQuantifiers(Env& env,
       d_qstate(env, valuation, logicInfo()),
       d_qreg(env),
       d_treg(env, d_qstate, d_qreg),
-      d_qim(env, *this, d_qstate, d_qreg, d_treg, d_pnm),
+      d_qim(env, *this, d_qstate, d_qreg, d_treg),
       d_qengine(nullptr)
 {
   // construct the quantifiers engine

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 88851e4078c8b01e044703188bda39b25320f803..ad41d832713c6420797d19acb3b2c4cc2aaf8aa0 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -47,7 +47,7 @@ TheorySep::TheorySep(Env& env, OutputChannel& out, Valuation valuation)
       d_lemmas_produced_c(userContext()),
       d_bounds_init(false),
       d_state(env, valuation),
-      d_im(env, *this, d_state, d_pnm, "theory::sep::"),
+      d_im(env, *this, d_state, "theory::sep::"),
       d_notify(*this),
       d_reduce(userContext()),
       d_spatial_assertions(context())

diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index 58fcbdae988254928928c6ac73b127f8cc92c7a2..15c4fd405b35e95216cc49b1a427fd7329a243a5 100644 (file)
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -25,11 +25,8 @@ namespace cvc5 {
 namespace theory {
 namespace sets {
 
-InferenceManager::InferenceManager(Env& env,
-                                   Theory& t,
-                                   SolverState& s,
-                                   ProofNodeManager* pnm)
-    : InferenceManagerBuffered(env, t, s, pnm, "theory::sets::"), d_state(s)
+InferenceManager::InferenceManager(Env& env, Theory& t, SolverState& s)
+    : InferenceManagerBuffered(env, t, s, "theory::sets::"), d_state(s)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   d_false = NodeManager::currentNM()->mkConst(false);

diff --git a/src/theory/sets/inference_manager.h b/src/theory/sets/inference_manager.h
index a9016ac3d11a1eee2f17090d756a39186db60c3f..36eec2cd3082a7d5d840dc55a8c710a0924bcd51 100644 (file)
--- a/src/theory/sets/inference_manager.h
+++ b/src/theory/sets/inference_manager.h
@@ -39,7 +39,7 @@ class InferenceManager : public InferenceManagerBuffered
   typedef context::CDHashSet<Node> NodeSet;
 
  public:
-  InferenceManager(Env& env, Theory& t, SolverState& s, ProofNodeManager* pnm);
+  InferenceManager(Env& env, Theory& t, SolverState& s);
   /**
    * Add facts corresponding to ( exp => fact ) via calls to the assertFact
    * method of TheorySetsPrivate.

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 833f4b22d0d1874b1e597e3a1df392aaea6adc98..2901703ddbc12d67c036fc5b0972317fea73d873 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -31,7 +31,7 @@ TheorySets::TheorySets(Env& env, OutputChannel& out, Valuation valuation)
     : Theory(THEORY_SETS, env, out, valuation),
       d_skCache(),
       d_state(env, valuation, d_skCache),
-      d_im(env, *this, d_state, d_pnm),
+      d_im(env, *this, d_state),
       d_internal(
           new TheorySetsPrivate(env, *this, d_state, d_im, d_skCache, d_pnm)),
       d_notify(*d_internal.get(), d_im)

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 1f531a97c9aeea9847fb01a29e662c357fc65253..a4f100c19bcc476c2ffc0a0af9adf51ad02836aa 100644 (file)
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -35,15 +35,20 @@ InferenceManager::InferenceManager(Env& env,
                                    SolverState& s,
                                    TermRegistry& tr,
                                    ExtTheory& e,
-                                   SequencesStatistics& statistics,
-                                   ProofNodeManager* pnm)
-    : InferenceManagerBuffered(env, t, s, pnm, "theory::strings::", false),
+                                   SequencesStatistics& statistics)
+    : InferenceManagerBuffered(env, t, s, "theory::strings::", false),
       d_state(s),
       d_termReg(tr),
       d_extt(e),
       d_statistics(statistics),
-      d_ipc(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr),
-      d_ipcl(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr)
+      d_ipc(isProofEnabled()
+                ? new InferProofCons(
+                      context(), env.getProofNodeManager(), d_statistics)
+                : nullptr),
+      d_ipcl(isProofEnabled()
+                 ? new InferProofCons(
+                       context(), env.getProofNodeManager(), d_statistics)
+                 : nullptr)
 {
   NodeManager* nm = NodeManager::currentNM();
   d_zero = nm->mkConst(Rational(0));

diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index 9f4cd1986f0ce2fe3a5e1644301bbd1e711fbdde..3ef83189bb05078f529e088433a0e55d6d4cacbe 100644 (file)
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -82,8 +82,7 @@ class InferenceManager : public InferenceManagerBuffered
                    SolverState& s,
                    TermRegistry& tr,
                    ExtTheory& e,
-                   SequencesStatistics& statistics,
-                   ProofNodeManager* pnm);
+                   SequencesStatistics& statistics);
   ~InferenceManager() {}
 
   /**

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 88698d9d81c33daadb664ebe09218259972f6688..25d0e73369dcb2de837400771ef12fdbc6694894 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -58,7 +58,7 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
       d_eagerSolver(d_state),
       d_termReg(env, d_state, d_statistics, d_pnm),
       d_extTheoryCb(),
-      d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics, d_pnm),
+      d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics),
       d_extTheory(env, d_extTheoryCb, d_im),
       d_rewriter(env.getRewriter(),
                  &d_statistics.d_rewrites,

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 22b5e9c442274d3478b3388213e424f160c96011..fdd1d07c8602962f9b719ca8842a45247c86fc83 100644 (file)
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -31,7 +31,6 @@ namespace theory {
 TheoryInferenceManager::TheoryInferenceManager(Env& env,
                                                Theory& t,
                                                TheoryState& state,
-                                               ProofNodeManager* pnm,
                                                const std::string& statsName,
                                                bool cacheLemmas)
     : EnvObj(env),
@@ -41,7 +40,6 @@ TheoryInferenceManager::TheoryInferenceManager(Env& env,
       d_ee(nullptr),
       d_decManager(nullptr),
       d_pfee(nullptr),
-      d_pnm(pnm),
       d_cacheLemmas(cacheLemmas),
       d_keep(context()),
       d_lemmasSent(userContext()),
@@ -71,7 +69,7 @@ void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
   // if it is non-null. If its proof equality engine has already been assigned,
   // use it. This is to ensure that all theories use the same proof equality
   // engine when in ee-mode=central.
-  if (d_pnm != nullptr && d_ee != nullptr)
+  if (isProofEnabled() && d_ee != nullptr)
   {
     d_pfee = d_ee->getProofEqualityEngine();
     if (d_pfee == nullptr)
@@ -88,7 +86,10 @@ void TheoryInferenceManager::setDecisionManager(DecisionManager* dm)
   d_decManager = dm;
 }
 
-bool TheoryInferenceManager::isProofEnabled() const { return d_pnm != nullptr; }
+bool TheoryInferenceManager::isProofEnabled() const
+{
+  return d_env.isTheoryProofProducing();
+}
 
 void TheoryInferenceManager::reset()
 {

diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 221d25fae64e1b5cc9d8f4639584f7fd023f718e..d7334d0e6db1d44d246f0f690f7de483656b8a0f 100644 (file)
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -89,7 +89,6 @@ class TheoryInferenceManager : protected EnvObj
   TheoryInferenceManager(Env& env,
                          Theory& t,
                          TheoryState& state,
-                         ProofNodeManager* pnm,
                          const std::string& statsName,
                          bool cacheLemmas = true);
   virtual ~TheoryInferenceManager();
@@ -441,8 +440,6 @@ class TheoryInferenceManager : protected EnvObj
   eq::ProofEqEngine* d_pfee;
   /** The proof equality engine we allocated */
   std::unique_ptr<eq::ProofEqEngine> d_pfeeAlloc;
-  /** The proof node manager of the theory */
-  ProofNodeManager* d_pnm;
   /** Whether this manager caches lemmas */
   bool d_cacheLemmas;
   /**

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index a76591b6ed46c8e810d2c2f52dc83ebc063d991a..498fe765e785a625c0b21284549238b37c8a1861 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -51,7 +51,7 @@ TheoryUF::TheoryUF(Env& env,
       d_symb(userContext(), instanceName),
       d_rewriter(logicInfo().isHigherOrder()),
       d_state(env, valuation),
-      d_im(env, *this, d_state, d_pnm, "theory::uf::" + instanceName, false),
+      d_im(env, *this, d_state, "theory::uf::" + instanceName, false),
       d_notify(d_im, *this)
 {
   d_true = NodeManager::currentNM()->mkConst( true );