1 files changed, 29 insertions, 27 deletions

diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index 20e4deec6..1eca56959 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -30,33 +30,6 @@ class SynthEngine : public QuantifiersModule
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 
- private:
-  /** the conjecture formula(s) we are waiting to assign */
-  std::vector<Node> d_waiting_conj;
-  /** The synthesis conjectures that this class is managing. */
-  std::vector<std::unique_ptr<SynthConjecture> > d_conjs;
-  /**
-   * The first conjecture in the above vector. We track this conjecture
-   * so that a synthesis conjecture can be preregistered during a call to
-   * preregisterAssertion.
-   */
-  SynthConjecture* d_conj;
-  /** assign quantified formula q as a conjecture
-   *
-   * This method either assigns q to a synthesis conjecture object in d_conjs,
-   * or otherwise reduces q to an equivalent form. This method does the latter
-   * if this class determines that it would rather rewrite q to an equivalent
-   * form r (in which case this method returns the lemma q <=> r). An example of
-   * this is the quantifier elimination step option::sygusQePreproc().
-   */
-  void assignConjecture(Node q);
-  /** check conjecture
-   *
-   * This method returns true if the conjecture is finished processing solutions
-   * for this call to SynthEngine::check().
-   */
-  bool checkConjecture(SynthConjecture* conj);
-
  public:
   SynthEngine(QuantifiersEngine* qe, context::Context* c);
   ~SynthEngine();
@@ -113,6 +86,35 @@ class SynthEngine : public QuantifiersModule
     ~Statistics();
   }; /* class SynthEngine::Statistics */
   Statistics d_statistics;
+
+ private:
+  /** term database sygus of d_qe */
+  TermDbSygus* d_tds;
+  /** the conjecture formula(s) we are waiting to assign */
+  std::vector<Node> d_waiting_conj;
+  /** The synthesis conjectures that this class is managing. */
+  std::vector<std::unique_ptr<SynthConjecture> > d_conjs;
+  /**
+   * The first conjecture in the above vector. We track this conjecture
+   * so that a synthesis conjecture can be preregistered during a call to
+   * preregisterAssertion.
+   */
+  SynthConjecture* d_conj;
+  /** assign quantified formula q as a conjecture
+   *
+   * This method either assigns q to a synthesis conjecture object in d_conjs,
+   * or otherwise reduces q to an equivalent form. This method does the latter
+   * if this class determines that it would rather rewrite q to an equivalent
+   * form r (in which case this method returns the lemma q <=> r). An example of
+   * this is the quantifier elimination step option::sygusQePreproc().
+   */
+  void assignConjecture(Node q);
+  /** check conjecture
+   *
+   * This method returns true if the conjecture is finished processing solutions
+   * for this call to SynthEngine::check().
+   */
+  bool checkConjecture(SynthConjecture* conj);
 }; /* class SynthEngine */
 
 }  // namespace quantifiers