diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-04-16 15:06:00 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-04-16 15:06:00 -0500 |
commit | 29a06b999c4637197282405df7040d6773bd3858 (patch) | |
tree | 8ca7cd03048db4d2e9dc5a5143d5216111577967 /src/theory/quantifiers/term_enumeration.h | |
parent | 2f7131c81078a964a4043ef79186cdcf91951974 (diff) |
Add interface for term enumeration (#2956)
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> |