diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 605592d0a..33fff6844 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -154,6 +154,13 @@ class SynthConjecture Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth); /** print out debug information about this conjecture */ void debugPrint(const char* c); + /** check side condition + * + * This returns false if the solution { d_candidates -> cvals } does not + * satisfy the side condition of the conjecture maintained by this class, + * if it exists, and true otherwise. + */ + bool checkSideCondition(const std::vector<Node>& cvals) const; private: /** reference to quantifier engine */ @@ -367,10 +374,15 @@ class SynthConjecture * Prints the current synthesis solution to the output stream indicated by * the Options object, send a lemma blocking the current solution to the * output channel, which we refer to as a "stream exclusion lemma". + * + * The argument enums is the set of enumerators that comprise the current + * solution, and values is their current values. */ - void printAndContinueStream(); - /** exclude the current solution */ - void excludeCurrentSolution(); + void printAndContinueStream(const std::vector<Node>& enums, + const std::vector<Node>& values); + /** exclude the current solution { enums -> values } */ + void excludeCurrentSolution(const std::vector<Node>& enums, + const std::vector<Node>& values); /** * Whether we have guarded a stream exclusion lemma when using sygusStream. * This is an optimization that allows us to guard only the first stream |