Add interface for term enumeration (#2956)

diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp
index 90e307d99e3d99a1064d00271819794478b47196..0336700ad6abd870d90035dc1cda4f4b5034f214 100644 (file)
--- 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 e76b8e999500f08f346641885f971d104291792a..ed6529ef1bf19a4b5e9e68c90b6ea2fb277ee258 100644 (file)
--- 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>