From 29a06b999c4637197282405df7040d6773bd3858 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 16 Apr 2019 15:06:00 -0500
Subject: Add interface for term enumeration (#2956)

---
 src/theory/quantifiers/term_enumeration.h | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/theory/quantifiers/term_enumeration.h')

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>
-- 
cgit v1.2.3