diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-24 23:50:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-09-24 23:50:50 -0500 |
| commit | e9c115e82ea1341f1bbc37fb99c005aacec3d7ec (patch) | |
| tree | d274291c8b570e1ff383504e8eeccaafbffd7b15 /src/theory/quantifiers/sygus/synth_conjecture.h | |
| parent | b9cddd75ada97b4e1808b907125e366c3c03c412 (diff) | |
Allow partial models for multiple sygus enumerators (#2499)
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 1cbd4e949..53bc829cf 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -112,9 +112,15 @@ class SynthConjecture void assign(Node q); /** has a conjecture been assigned to this class */ bool isAssigned() { return !d_embed_quant.isNull(); } - /** get model values for terms n, store in vector v */ - void getModelValues(std::vector<Node>& n, std::vector<Node>& v); - /** get model value for term n */ + /** + * 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. + */ + bool getModelValues(std::vector<Node>& n, std::vector<Node>& v); + /** + * Get model value for term n. If n has a value that was excluded by + * datatypes sygus symmetry breaking, this method returns null. + */ Node getModelValue(Node n); /** get utility for static preprocessing and analysis of conjectures */ |