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

6 files changed, 22 insertions, 11 deletions

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 3b4babe75..5a5d97064 100644
--- 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 da3e506fc..e856f1519 100644
--- 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 527632786..d92a9b40c 100644
--- 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 da8727c12..b98088a71 100644
--- 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 1fc08b288..79b509533 100644
--- 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 5e1f45b35..e20f5eea6 100644
--- 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);