1 files changed, 14 insertions, 0 deletions
diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h
index 668d04beb..d8e6ae651 100644
--- a/src/theory/quantifiers/expr_miner_manager.h
+++ b/src/theory/quantifiers/expr_miner_manager.h
@@ -20,6 +20,8 @@
 #include "expr/node.h"
 #include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/extended_rewrite.h"
+#include "theory/quantifiers/query_generator.h"
+#include "theory/quantifiers/solution_filter.h"
 #include "theory/quantifiers/sygus_sampler.h"
 #include "theory/quantifiers_engine.h"
 
@@ -67,6 +69,10 @@ class ExpressionMinerManager
                        bool useSygusType);
   /** enable rewrite rule synthesis (--sygus-rr-synth) */
   void enableRewriteRuleSynth();
+  /** enable query generation (--sygus-query-gen) */
+  void enableQueryGeneration(unsigned deqThresh);
+  /** filter implied solutions (--sygus-sol-filter-implied) */
+  void enableFilterImpliedSolutions();
   /** add term
    *
    * Expression miners may print information on the output stream out, for
@@ -84,6 +90,10 @@ class ExpressionMinerManager
  private:
   /** whether we are doing rewrite synthesis */
   bool d_doRewSynth;
+  /** whether we are doing query generation */
+  bool d_doQueryGen;
+  /** whether we are filtering implied candidates */
+  bool d_doFilterImplied;
   /** the sygus function passed to initializeSygus, if any */
   Node d_sygus_fun;
   /** whether we are using sygus types */
@@ -94,6 +104,10 @@ class ExpressionMinerManager
   TermDbSygus* d_tds;
   /** candidate rewrite database */
   CandidateRewriteDatabase d_crd;
+  /** query generator */
+  QueryGenerator d_qg;
+  /** solution filter */
+  SolutionFilter d_solf;
   /** sygus sampler object */
   SygusSampler d_sampler;
   /** extended rewriter object */