From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 16 Apr 2019 20:06:00 +0000 (-0500)
Subject: Add interface for term enumeration (#2956)
X-Git-Tag: cvc5-1.0.0~4176
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=29a06b999c4637197282405df7040d6773bd3858;p=cvc5.git

Add interface for term enumeration (#2956)
---

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>