1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 85606adc6..3695270e1 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -19,15 +19,18 @@
 #define CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
 
 #include <map>
-#include "theory/evaluator.h"
 #include "theory/quantifiers/lazy_trie.h"
-#include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_enumeration.h"
 
 namespace cvc5 {
+
+class Env;
+
 namespace theory {
 namespace quantifiers {
 
+class TermDbSygus;
+
 /** SygusSampler
  *
  * This class can be used to test whether two expressions are equivalent
@@ -65,7 +68,7 @@ namespace quantifiers {
 class SygusSampler : public LazyTrieEvaluator
 {
  public:
-  SygusSampler();
+  SygusSampler(Env& env);
   ~SygusSampler() override {}
 
   /** initialize
@@ -178,14 +181,14 @@ class SygusSampler : public LazyTrieEvaluator
   void checkEquivalent(Node bv, Node bvr, std::ostream& out);
 
  protected:
+  /** The environment we are using to evaluate terms and samples */
+  Env& d_env;
   /** sygus term database of d_qe */
   TermDbSygus* d_tds;
   /** term enumerator object (used for random sampling) */
   TermEnumeration d_tenum;
   /** samples */
   std::vector<std::vector<Node> > d_samples;
-  /** evaluator class */
-  Evaluator d_eval;
   /** data structure to check duplication of sample points */
   class PtTrie
   {