diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_engine.h')
-rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.h | 56 |
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 |