Eliminate more hard coded uses of user context (#7309)

This is in preparation to make the "lemma context" configurable.

4 files changed, 6 insertions, 7 deletions

diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp
index d5f06b6e9..da3e506fc 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp
@@ -54,7 +54,7 @@ void CandidateRewriteFilter::initialize(SygusSampler* ss,
   ssn << "_dyn_rewriter_" << drewrite_counter;
   drewrite_counter++;
   d_drewrite = std::unique_ptr<DynamicRewriter>(
-      new DynamicRewriter(ssn.str(), &d_fake_context));
+      new DynamicRewriter(ssn.str(), &d_fakeContext));
 }
 
 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 4995dc7c2..527632786 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.h
+++ b/src/theory/quantifiers/candidate_rewrite_filter.h
@@ -104,8 +104,8 @@ class CandidateRewriteFilter
   bool d_use_sygus_type;
 
   //----------------------------congruence filtering
-  /** a (dummy) user context, used for d_drewrite */
-  context::UserContext d_fake_context;
+  /** a (dummy) context, used for d_drewrite */
+  context::Context d_fakeContext;
   /** dynamic rewriter class */
   std::unique_ptr<DynamicRewriter> d_drewrite;
   //----------------------------end congruence filtering
diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp
index 4d69ea732..1fc08b288 100644
--- a/src/theory/quantifiers/dynamic_rewrite.cpp
+++ b/src/theory/quantifiers/dynamic_rewrite.cpp
@@ -25,9 +25,8 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-DynamicRewriter::DynamicRewriter(const std::string& name,
-                                 context::UserContext* u)
-    : d_equalityEngine(u, "DynamicRewriter::" + name, true), d_rewrites(u)
+DynamicRewriter::DynamicRewriter(const std::string& name, context::Context* c)
+    : d_equalityEngine(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 3187b7c03..5e1f45b35 100644
--- a/src/theory/quantifiers/dynamic_rewrite.h
+++ b/src/theory/quantifiers/dynamic_rewrite.h
@@ -55,7 +55,7 @@ class DynamicRewriter
   typedef context::CDList<Node> NodeList;
 
  public:
-  DynamicRewriter(const std::string& name, context::UserContext* u);
+  DynamicRewriter(const std::string& name, context::Context* c);
   ~DynamicRewriter() {}
   /** inform this class that the equality a = b holds. */
   void addRewrite(Node a, Node b);