From e9c115e82ea1341f1bbc37fb99c005aacec3d7ec Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 24 Sep 2018 23:50:50 -0500 Subject: Allow partial models for multiple sygus enumerators (#2499) --- src/theory/quantifiers/sygus/synth_conjecture.h | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to '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 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& n, std::vector& 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& n, std::vector& 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 */ -- cgit v1.2.3