diff options
Diffstat (limited to 'src/theory/quantifiers/term_enumeration.h')
| -rw-r--r-- | src/theory/quantifiers/term_enumeration.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h index e76b8e999..ed6529ef1 100644 --- a/src/theory/quantifiers/term_enumeration.h +++ b/src/theory/quantifiers/term_enumeration.h @@ -56,6 +56,14 @@ class TermEnumeration */ static bool mayComplete(TypeNode tn, unsigned cardMax); + /** get domain + * + * If tn is a type such that mayComplete(tn) returns true, this method + * adds all domain elements of tn to dom and returns true. Otherwise, this + * method returns false. + */ + bool getDomain(TypeNode tn, std::vector<Node>& dom); + private: /** ground terms enumerated for types */ std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction> |