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 | |
parent | 2f7131c81078a964a4043ef79186cdcf91951974 (diff) |
Add interface for term enumeration (#2956)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/term_enumeration.cpp | 20 | ||||
-rw-r--r-- | src/theory/quantifiers/term_enumeration.h | 8 |
2 files changed, 28 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp index 90e307d99..0336700ad 100644 --- a/src/theory/quantifiers/term_enumeration.cpp +++ b/src/theory/quantifiers/term_enumeration.cpp @@ -87,6 +87,26 @@ bool TermEnumeration::mayComplete(TypeNode tn, unsigned maxCard) return mc; } +bool TermEnumeration::getDomain(TypeNode tn, std::vector<Node>& dom) +{ + if (!mayComplete(tn)) + { + return false; + } + Node curre; + unsigned counter = 0; + do + { + curre = getEnumerateTerm(tn, counter); + counter++; + if (!curre.isNull()) + { + dom.push_back(curre); + } + } while (!curre.isNull()); + return true; +} + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ 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> |