diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 53bc829cf..694e4a0cb 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -116,11 +116,15 @@ 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. */ - bool getModelValues(std::vector<Node>& n, std::vector<Node>& v); + bool getEnumeratedValues(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 getEnumeratedValue(Node n); + /** + * Get model value for term n. + */ Node getModelValue(Node n); /** get utility for static preprocessing and analysis of conjectures */ @@ -138,6 +142,8 @@ class SynthConjecture private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; + /** term database sygus of d_qe */ + TermDbSygus* d_tds; /** The feasible guard. */ Node d_feasible_guard; /** the decision strategy for the feasible guard */ |