diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 26 |
1 files changed, 21 insertions, 5 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index ef1b4459f..3a43eb83d 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -49,8 +49,14 @@ class EnumValGenerator virtual void initialize(Node e) = 0; /** Inform this generator that abstract value v was enumerated. */ virtual void addValue(Node v) = 0; - /** Get the next concrete value generated by this class. */ - virtual Node getNext() = 0; + /** + * Increment this value generator. If this returns false, then we are out of + * values. If this returns true, getCurrent(), if non-null, returns the + * current term. + */ + virtual bool increment() = 0; + /** Get the current concrete value generated by this class. */ + virtual Node getCurrent() = 0; }; /** a synthesis conjecture @@ -193,15 +199,25 @@ class SynthConjecture * Get model values for terms n, store in vector v. This method returns true * if and only if all values added to v are non-null. * + * The argument activeIncomplete indicates whether n contains an active + * enumerator that is currently not finished enumerating values, but returned + * null on a call to getEnumeratedValue. This value is used for determining + * whether we should call getEnumeratedValues again within a call to + * SynthConjecture::check. + * * It removes terms from n that correspond to "inactive" enumerators, that * is, enumerators whose values have been exhausted. */ - bool getEnumeratedValues(std::vector<Node>& n, std::vector<Node>& v); + bool getEnumeratedValues(std::vector<Node>& n, + std::vector<Node>& v, + bool& activeIncomplete); /** * Get model value for term n. If n has a value that was excluded by - * datatypes sygus symmetry breaking, this method returns null. + * datatypes sygus symmetry breaking, this method returns null. It sets + * activeIncomplete to true if there is an actively-generated enumerator whose + * current value is null but it has not finished generating values. */ - Node getEnumeratedValue(Node n); + Node getEnumeratedValue(Node n, bool& activeIncomplete); /** enumerator generators for each actively-generated enumerator */ std::map<Node, std::unique_ptr<EnumValGenerator> > d_evg; /** |