Use quantifiers inference manager for lemma management (#5867)

[cvc5.git] / src / theory / quantifiers / sygus / synth_conjecture.h

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 7786f57ad1ce3f9728a58c8f0b63c2c4d5f0f17f..ca3f2983b1d6fed2d8091ba138451a33a62e0038 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -82,7 +82,10 @@ class EnumValGenerator
 class SynthConjecture
 {
  public:
-  SynthConjecture(QuantifiersEngine* qe, SygusStatistics& s);
+  SynthConjecture(QuantifiersEngine* qe,
+                  QuantifiersState& qs,
+                  QuantifiersInferenceManager& qim,
+                  SygusStatistics& s);
   ~SynthConjecture();
   /** presolve */
   void presolve();
@@ -199,6 +202,10 @@ class SynthConjecture
  private:
   /** reference to quantifier engine */
   QuantifiersEngine* d_qe;
+  /** Reference to the quantifiers state */
+  QuantifiersState& d_qstate;
+  /** Reference to the quantifiers inference manager */
+  QuantifiersInferenceManager& d_qim;
   /** reference to the statistics of parent */
   SygusStatistics& d_stats;
   /** term database sygus of d_qe */