diff options
| -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> |