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.

7 files changed, 32 insertions, 33 deletions

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index be04f9404..f47a71926 100644
--- 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 b4972a7b6..2e5bd1e2f 100644
--- 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 20987b02e..f282b8d11 100644
--- 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 20981a795..abd8d0761 100644
--- 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 a34547f45..830847b74 100644
--- 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 294ad0084..604bc60e4 100644
--- 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 7e20c3a4a..bce827bbd 100644
--- 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