Make (proof) equality engine use Env (#7336)

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index e419f3ae1d54dafbfe79d306935277a5a1b051f6..4aee9e98164ccb6a621495803bff81231a9ae74b 100644 (file)
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -81,14 +81,13 @@ void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee)
   if (options().arith.arithEqSolver)
   {
     // use our own copy
-    d_allocEe.reset(
-        new eq::EqualityEngine(d_notify, context(), "arithCong::ee", true));
+    d_allocEe = std::make_unique<eq::EqualityEngine>(
+        d_env, context(), d_notify, "arithCong::ee", true);
     d_ee = d_allocEe.get();
     if (d_pnm != nullptr)
     {
       // allocate an internal proof equality engine
-      d_allocPfee.reset(
-          new eq::ProofEqEngine(context(), userContext(), *d_ee, d_pnm));
+      d_allocPfee = std::make_unique<eq::ProofEqEngine>(d_env, *d_ee);
       d_ee->setProofEqualityEngine(d_allocPfee.get());
     }
   }

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index cf31f0cb6c90c7da61f4a448dfe8a73103fc66fe..9e69c9f7188c9371b61577ea8d57a772ab73b3f8 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -77,7 +77,7 @@ TheoryArrays::TheoryArrays(Env& env,
           name + "number of setModelVal splits")),
       d_numSetModelValConflicts(statisticsRegistry().registerInt(
           name + "number of setModelVal conflicts")),
-      d_ppEqualityEngine(userContext(), name + "pp", true),
+      d_ppEqualityEngine(d_env, userContext(), name + "pp", true),
       d_ppFacts(userContext()),
       d_rewriter(env.getRewriter(), d_pnm),
       d_state(env, valuation),
@@ -85,7 +85,7 @@ TheoryArrays::TheoryArrays(Env& env,
       d_literalsToPropagate(context()),
       d_literalsToPropagateIndex(context(), 0),
       d_isPreRegistered(context()),
-      d_mayEqualEqualityEngine(context(), name + "mayEqual", true),
+      d_mayEqualEqualityEngine(d_env, context(), name + "mayEqual", true),
       d_notify(*this),
       d_infoMap(context(), name),
       d_mergeQueue(context()),

diff --git a/src/theory/ee_manager.cpp b/src/theory/ee_manager.cpp
index a91aea94ea27ea44ad4f3a4bd39060c7ec8cf1e5..142853b9575eb761801712898e79340d683ec37d 100644 (file)
--- a/src/theory/ee_manager.cpp
+++ b/src/theory/ee_manager.cpp
@@ -41,10 +41,11 @@ eq::EqualityEngine* EqEngineManager::allocateEqualityEngine(EeSetupInfo& esi,
   if (esi.d_notify != nullptr)
   {
     return new eq::EqualityEngine(
-        *esi.d_notify, c, esi.d_name, esi.d_constantsAreTriggers);
+        d_env, c, *esi.d_notify, esi.d_name, esi.d_constantsAreTriggers);
   }
   // the theory doesn't care about explicit notifications
-  return new eq::EqualityEngine(c, esi.d_name, esi.d_constantsAreTriggers);
+  return new eq::EqualityEngine(
+      d_env, c, esi.d_name, esi.d_constantsAreTriggers);
 }
 
 }  // namespace theory

diff --git a/src/theory/ee_manager_central.cpp b/src/theory/ee_manager_central.cpp
index 0e6610833f3da04dc96a16e1bd29ff7fd5e673fb..079cdd9049a07fdf4c76f8467c2aa0584ee110ca 100644 (file)
--- a/src/theory/ee_manager_central.cpp
+++ b/src/theory/ee_manager_central.cpp
@@ -31,7 +31,8 @@ EqEngineManagerCentral::EqEngineManagerCentral(Env& env,
       d_masterEENotify(nullptr),
       d_masterEqualityEngine(nullptr),
       d_centralEENotify(*this),
-      d_centralEqualityEngine(d_centralEENotify, context(), "central::ee", true)
+      d_centralEqualityEngine(
+          env, context(), d_centralEENotify, "central::ee", true)
 {
   for (TheoryId theoryId = theory::THEORY_FIRST;
        theoryId != theory::THEORY_LAST;
@@ -41,10 +42,8 @@ EqEngineManagerCentral::EqEngineManagerCentral(Env& env,
   }
   if (env.isTheoryProofProducing())
   {
-    d_centralPfee.reset(new eq::ProofEqEngine(context(),
-                                              userContext(),
-                                              d_centralEqualityEngine,
-                                              env.getProofNodeManager()));
+    d_centralPfee =
+        std::make_unique<eq::ProofEqEngine>(env, d_centralEqualityEngine);
     d_centralEqualityEngine.setProofEqualityEngine(d_centralPfee.get());
   }
 }
@@ -112,8 +111,8 @@ void EqEngineManagerCentral::initializeTheories()
     d_masterEENotify.reset(new quantifiers::MasterNotifyClass(qe));
     if (!masterEqToCentral)
     {
-      d_masterEqualityEngineAlloc.reset(new eq::EqualityEngine(
-          *d_masterEENotify.get(), c, "master::ee", false));
+      d_masterEqualityEngineAlloc = std::make_unique<eq::EqualityEngine>(
+          d_env, c, *d_masterEENotify.get(), "master::ee", false);
       d_masterEqualityEngine = d_masterEqualityEngineAlloc.get();
     }
     else

diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp
index 6dee1910b377e6dc15e5d7cce545f42e8bad3027..1de625d481f7f14aabdbf1dbf62ba0803e1efe80 100644 (file)
--- a/src/theory/ee_manager_distributed.cpp
+++ b/src/theory/ee_manager_distributed.cpp
@@ -58,8 +58,8 @@ void EqEngineManagerDistributed::initializeTheories()
     QuantifiersEngine* qe = d_te.getQuantifiersEngine();
     Assert(qe != nullptr);
     d_masterEENotify.reset(new quantifiers::MasterNotifyClass(qe));
-    d_masterEqualityEngine.reset(new eq::EqualityEngine(
-        *d_masterEENotify.get(), c, "theory::master", false));
+    d_masterEqualityEngine = std::make_unique<eq::EqualityEngine>(
+        d_env, c, *d_masterEENotify.get(), "theory::master", false);
   }
   // allocate equality engines per theory
   for (TheoryId theoryId = theory::THEORY_FIRST;

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 3b4babe75ff7ffecb4fe172afc0fe0db84a4df97..5a5d970648ad40ea5e66a8c98d1bf7ba6fd64e77 100644 (file)
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -42,7 +42,8 @@ CandidateRewriteDatabase::CandidateRewriteDatabase(
       d_rewAccel(rewAccel),
       d_silent(silent),
       d_filterPairs(filterPairs),
-      d_using_sygus(false)
+      d_using_sygus(false),
+      d_crewrite_filter(env)
 {
 }
 void CandidateRewriteDatabase::initialize(const std::vector<Node>& vars,

diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp
index da3e506fc0563cc8d203ba8cabe0a2c6abec5b5e..e856f1519d98e6127a54df16945b05b4275df4d7 100644 (file)
--- a/src/theory/quantifiers/candidate_rewrite_filter.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp
@@ -30,8 +30,9 @@ namespace quantifiers {
 // the number of d_drewrite objects we have allocated (to avoid name conflicts)
 static unsigned drewrite_counter = 0;
 
-CandidateRewriteFilter::CandidateRewriteFilter()
-    : d_ss(nullptr),
+CandidateRewriteFilter::CandidateRewriteFilter(Env& env)
+    : EnvObj(env),
+      d_ss(nullptr),
       d_tds(nullptr),
       d_use_sygus_type(false),
       d_drewrite(nullptr),
@@ -53,8 +54,8 @@ void CandidateRewriteFilter::initialize(SygusSampler* ss,
   std::stringstream ssn;
   ssn << "_dyn_rewriter_" << drewrite_counter;
   drewrite_counter++;
-  d_drewrite = std::unique_ptr<DynamicRewriter>(
-      new DynamicRewriter(ssn.str(), &d_fakeContext));
+  d_drewrite =
+      std::make_unique<DynamicRewriter>(d_env, &d_fakeContext, ssn.str());
 }
 
 bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)

diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h
index 5276327867bf6cd9a4822bd5edd7737bac96010d..d92a9b40ca4ba8695c9e9a8c8f70b280cc913237 100644 (file)
--- a/src/theory/quantifiers/candidate_rewrite_filter.h
+++ b/src/theory/quantifiers/candidate_rewrite_filter.h
@@ -21,7 +21,9 @@
 #define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
 
 #include <map>
+
 #include "expr/match_trie.h"
+#include "smt/env_obj.h"
 #include "theory/quantifiers/dynamic_rewrite.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/sygus_sampler.h"
@@ -46,10 +48,10 @@ namespace quantifiers {
  * pairs". A relevant pair ( t, s ) typically corresponds to a (candidate)
  * rewrite t = s.
  */
-class CandidateRewriteFilter
+class CandidateRewriteFilter : protected EnvObj
 {
  public:
-  CandidateRewriteFilter();
+  CandidateRewriteFilter(Env& env);
 
   /** initialize
    *

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index da8727c125cd98c3a96a567368888ef234b836f9..b98088a710c970b9dc68b96a1551526e6ab1466a 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -93,7 +93,8 @@ ConjectureGenerator::ConjectureGenerator(Env& env,
                                          TermRegistry& tr)
     : QuantifiersModule(env, qs, qim, qr, tr),
       d_notify(*this),
-      d_uequalityEngine(d_notify, context(), "ConjectureGenerator::ee", false),
+      d_uequalityEngine(
+          env, context(), d_notify, "ConjectureGenerator::ee", false),
       d_ee_conjectures(context()),
       d_conj_count(0),
       d_subs_confirmCount(0),

diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp
index 1fc08b288ef2cad82ae0579a82157f2a197ca8f5..79b5095338893fc0ff587771df9fe4a7b45801e8 100644 (file)
--- a/src/theory/quantifiers/dynamic_rewrite.cpp
+++ b/src/theory/quantifiers/dynamic_rewrite.cpp
@@ -16,6 +16,7 @@
 #include "theory/quantifiers/dynamic_rewrite.h"
 
 #include "expr/skolem_manager.h"
+#include "smt/env.h"
 #include "theory/rewriter.h"
 
 using namespace std;
@@ -25,8 +26,10 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-DynamicRewriter::DynamicRewriter(const std::string& name, context::Context* c)
-    : d_equalityEngine(c, "DynamicRewriter::" + name, true), d_rewrites(c)
+DynamicRewriter::DynamicRewriter(Env& env,
+                                 context::Context* c,
+                                 const std::string& name)
+    : d_equalityEngine(env, c, "DynamicRewriter::" + name, true), d_rewrites(c)
 {
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
 }

diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h
index 5e1f45b3500bab5c8250357caeabad981e667dde..e20f5eea6f900ba10e94590c5368cdae3bf13465 100644 (file)
--- a/src/theory/quantifiers/dynamic_rewrite.h
+++ b/src/theory/quantifiers/dynamic_rewrite.h
@@ -24,6 +24,9 @@
 #include "theory/uf/equality_engine.h"
 
 namespace cvc5 {
+
+class Env;
+
 namespace theory {
 namespace quantifiers {
 
@@ -55,7 +58,7 @@ class DynamicRewriter
   typedef context::CDList<Node> NodeList;
 
  public:
-  DynamicRewriter(const std::string& name, context::Context* c);
+  DynamicRewriter(Env& env, context::Context* c, const std::string& name);
   ~DynamicRewriter() {}
   /** inform this class that the equality a = b holds. */
   void addRewrite(Node a, Node b);

diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 6c0f6ae10dbec384612db0141143a85ce2f4e6c2..9503d13789f1a98061f9edf479a07afb15eb0203 100644 (file)
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -52,9 +52,7 @@ void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee)
     d_pfee = d_equalityEngine->getProofEqualityEngine();
     if (d_pfee == nullptr)
     {
-      ProofNodeManager* pnm = d_env.getProofNodeManager();
-      d_pfeeAlloc.reset(new eq::ProofEqEngine(
-          d_env.getContext(), d_env.getUserContext(), *ee, pnm));
+      d_pfeeAlloc = std::make_unique<eq::ProofEqEngine>(d_env, *ee);
       d_pfee = d_pfeeAlloc.get();
       d_equalityEngine->setProofEqualityEngine(d_pfee);
     }

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 415672e9742647aab7a9c8493cd29928b1052fa0..9844d13bc6582875f957447a6c34470b67be2884 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -132,8 +132,12 @@ void Theory::finishInitStandalone()
   if (needsEqualityEngine(esi))
   {
     // always associated with the same SAT context as the theory
-    d_allocEqualityEngine.reset(new eq::EqualityEngine(
-        *esi.d_notify, context(), esi.d_name, esi.d_constantsAreTriggers));
+    d_allocEqualityEngine =
+        std::make_unique<eq::EqualityEngine>(d_env,
+                                             context(),
+                                             *esi.d_notify,
+                                             esi.d_name,
+                                             esi.d_constantsAreTriggers);
     // use it as the official equality engine
     setEqualityEngine(d_allocEqualityEngine.get());
   }

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 1699e91ad3f21936795d71b78da7f8ab543af979..22b5e9c442274d3478b3388213e424f160c96011 100644 (file)
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -76,8 +76,7 @@ void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
     d_pfee = d_ee->getProofEqualityEngine();
     if (d_pfee == nullptr)
     {
-      d_pfeeAlloc.reset(
-          new eq::ProofEqEngine(context(), userContext(), *d_ee, d_pnm));
+      d_pfeeAlloc = std::make_unique<eq::ProofEqEngine>(d_env, *d_ee);
       d_pfee = d_pfeeAlloc.get();
       d_ee->setProofEqualityEngine(d_pfee);
     }

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 34704181cb84efa3c2bd4cf5384e452e54f59cb0..a62bf876c65cdd140dab9304a3230776d0f44fe4 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -20,6 +20,7 @@
 
 #include "base/output.h"
 #include "options/smt_options.h"
+#include "smt/env.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/uf/eq_proof.h"
@@ -99,59 +100,63 @@ EqualityEngine::~EqualityEngine() {
   free(d_triggerDatabase);
 }
 
-EqualityEngine::EqualityEngine(context::Context* context,
+EqualityEngine::EqualityEngine(Env& env,
+                               context::Context* c,
                                std::string name,
                                bool constantsAreTriggers,
                                bool anyTermTriggers)
-    : ContextNotifyObj(context),
+    : ContextNotifyObj(c),
       d_masterEqualityEngine(0),
-      d_context(context),
-      d_done(context, false),
+      d_env(env),
+      d_context(c),
+      d_done(c, false),
       d_notify(&s_notifyNone),
-      d_applicationLookupsCount(context, 0),
-      d_nodesCount(context, 0),
-      d_assertedEqualitiesCount(context, 0),
-      d_equalityTriggersCount(context, 0),
-      d_subtermEvaluatesSize(context, 0),
+      d_applicationLookupsCount(c, 0),
+      d_nodesCount(c, 0),
+      d_assertedEqualitiesCount(c, 0),
+      d_equalityTriggersCount(c, 0),
+      d_subtermEvaluatesSize(c, 0),
       d_stats(name + "::"),
       d_inPropagate(false),
       d_constantsAreTriggers(constantsAreTriggers),
       d_anyTermsAreTriggers(anyTermTriggers),
-      d_triggerDatabaseSize(context, 0),
-      d_triggerTermSetUpdatesSize(context, 0),
-      d_deducedDisequalitiesSize(context, 0),
-      d_deducedDisequalityReasonsSize(context, 0),
-      d_propagatedDisequalities(context),
+      d_triggerDatabaseSize(c, 0),
+      d_triggerTermSetUpdatesSize(c, 0),
+      d_deducedDisequalitiesSize(c, 0),
+      d_deducedDisequalityReasonsSize(c, 0),
+      d_propagatedDisequalities(c),
       d_name(name)
 {
   init();
 }
 
-EqualityEngine::EqualityEngine(EqualityEngineNotify& notify,
-                               context::Context* context,
+EqualityEngine::EqualityEngine(Env& env,
+                               context::Context* c,
+                               EqualityEngineNotify& notify,
                                std::string name,
                                bool constantsAreTriggers,
                                bool anyTermTriggers)
-    : ContextNotifyObj(context),
+    : ContextNotifyObj(c),
       d_masterEqualityEngine(nullptr),
       d_proofEqualityEngine(nullptr),
-      d_context(context),
-      d_done(context, false),
+      d_env(env),
+      d_context(c),
+      d_done(c, false),
       d_notify(&s_notifyNone),
-      d_applicationLookupsCount(context, 0),
-      d_nodesCount(context, 0),
-      d_assertedEqualitiesCount(context, 0),
-      d_equalityTriggersCount(context, 0),
-      d_subtermEvaluatesSize(context, 0),
+      d_applicationLookupsCount(c, 0),
+      d_nodesCount(c, 0),
+      d_assertedEqualitiesCount(c, 0),
+      d_equalityTriggersCount(c, 0),
+      d_subtermEvaluatesSize(c, 0),
       d_stats(name + "::"),
       d_inPropagate(false),
       d_constantsAreTriggers(constantsAreTriggers),
       d_anyTermsAreTriggers(anyTermTriggers),
-      d_triggerDatabaseSize(context, 0),
-      d_triggerTermSetUpdatesSize(context, 0),
-      d_deducedDisequalitiesSize(context, 0),
-      d_deducedDisequalityReasonsSize(context, 0),
-      d_propagatedDisequalities(context),
+      d_triggerDatabaseSize(c, 0),
+      d_triggerTermSetUpdatesSize(c, 0),
+      d_deducedDisequalitiesSize(c, 0),
+      d_deducedDisequalityReasonsSize(c, 0),
+      d_propagatedDisequalities(c),
       d_name(name)
 {
   init();
@@ -1849,7 +1854,7 @@ Node EqualityEngine::evaluateTerm(TNode node) {
     builder << childRep;
   }
   Node newNode = builder;
-  return Rewriter::rewrite(newNode);
+  return d_env.getRewriter()->rewrite(newNode);
 }
 
 void EqualityEngine::processEvaluationQueue() {

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 0710ac6c7fd1d5d54a49bd9dd415d30287cadc6a..232f9059512f608a729c9fc5276b6cfe327e4167 100644 (file)
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -37,6 +37,9 @@
 #include "util/statistics_stats.h"
 
 namespace cvc5 {
+
+class Env;
+
 namespace theory {
 namespace eq {
 
@@ -70,11 +73,16 @@ class EqualityEngine : public context::ContextNotifyObj {
   /**
    * Initialize the equality engine, given the notification class.
    *
+   * @param env The environment, which is used for rewriting
+   * @param c The context which this equality engine depends, which is typically
+   * although not necessarily same as the SAT context of env.
+   * @param name The name of this equality engine, for statistics
    * @param constantTriggers Whether we treat constants as trigger terms
    * @param anyTermTriggers Whether we use any terms as triggers
    */
-  EqualityEngine(EqualityEngineNotify& notify,
-                 context::Context* context,
+  EqualityEngine(Env& env,
+                 context::Context* c,
+                 EqualityEngineNotify& notify,
                  std::string name,
                  bool constantTriggers,
                  bool anyTermTriggers = true);
@@ -82,7 +90,8 @@ class EqualityEngine : public context::ContextNotifyObj {
   /**
    * Initialize the equality engine with no notification class.
    */
-  EqualityEngine(context::Context* context,
+  EqualityEngine(Env& env,
+                 context::Context* c,
                  std::string name,
                  bool constantsAreTriggers,
                  bool anyTermTriggers = true);
@@ -120,7 +129,9 @@ class EqualityEngine : public context::ContextNotifyObj {
     Statistics(const std::string& name);
   };/* struct EqualityEngine::statistics */
 
-private:
+ private:
+  /** The environment we are using */
+  Env& d_env;
 
   /** The context we are using */
   context::Context* d_context;

diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index b6e44533407ea063851741b0bef6a97852935ca8..71688fc15da9b9937ba720ba2093a9fe5200b341 100644 (file)
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -18,6 +18,7 @@
 #include "proof/lazy_proof_chain.h"
 #include "proof/proof_node.h"
 #include "proof/proof_node_manager.h"
+#include "smt/env.h"
 #include "theory/rewriter.h"
 #include "theory/uf/eq_proof.h"
 #include "theory/uf/equality_engine.h"
@@ -29,22 +30,24 @@ namespace cvc5 {
 namespace theory {
 namespace eq {
 
-ProofEqEngine::ProofEqEngine(context::Context* c,
-                             context::Context* lc,
-                             EqualityEngine& ee,
-                             ProofNodeManager* pnm)
-    : EagerProofGenerator(pnm, lc, "pfee::" + ee.identify()),
+ProofEqEngine::ProofEqEngine(Env& env, EqualityEngine& ee)
+    : EagerProofGenerator(env.getProofNodeManager(),
+                          env.getUserContext(),
+                          "pfee::" + ee.identify()),
       d_ee(ee),
-      d_factPg(c, pnm),
-      d_assumpPg(pnm),
-      d_pnm(pnm),
-      d_proof(pnm, nullptr, c, "pfee::LazyCDProof::" + ee.identify()),
-      d_keep(c)
+      d_factPg(env.getContext(), env.getProofNodeManager()),
+      d_assumpPg(env.getProofNodeManager()),
+      d_pnm(env.getProofNodeManager()),
+      d_proof(env.getProofNodeManager(),
+              nullptr,
+              env.getContext(),
+              "pfee::LazyCDProof::" + ee.identify()),
+      d_keep(env.getContext())
 {
   NodeManager* nm = NodeManager::currentNM();
   d_true = nm->mkConst(true);
   d_false = nm->mkConst(false);
-  AlwaysAssert(pnm != nullptr)
+  AlwaysAssert(env.getProofNodeManager() != nullptr)
       << "Should not construct ProofEqEngine without proof node manager";
 }
 

diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 9ebdd03e5cc1da5cfe4303f272e58bb13c3702d5..fc8520dd153156c3fb4e2ee65537dec2af89f92f 100644 (file)
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -30,6 +30,7 @@
 
 namespace cvc5 {
 
+class Env;
 class ProofNode;
 class ProofNodeManager;
 
@@ -86,15 +87,10 @@ class ProofEqEngine : public EagerProofGenerator
 
  public:
   /**
-   * @param c The SAT context
-   * @param lc The context lemmas live in
+   * @param env The environment
    * @param ee The equality engine this is layered on
-   * @param pnm The proof node manager for producing proof nodes.
    */
-  ProofEqEngine(context::Context* c,
-                context::Context* lc,
-                EqualityEngine& ee,
-                ProofNodeManager* pnm);
+  ProofEqEngine(Env& env, EqualityEngine& ee);
   ~ProofEqEngine() {}
   //-------------------------- assert fact
   /**