From 4941b3c516361183b4623f5660128e4f1bcce809 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 14 Jul 2012 22:53:58 +0000
Subject: Type enumerator infrastructure and uninterpreted constant support. 
 No support yet for enumerating arrays, or for enumerating non-trivial
 datatypes.

---
 src/theory/arrays/kinds | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/theory/arrays/kinds')

diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 195a60035..eaef3746e 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -19,6 +19,10 @@ cardinality ARRAY_TYPE \
     "theory/arrays/theory_arrays_type_rules.h"
 well-founded ARRAY_TYPE false
 
+enumerator ARRAY_TYPE \
+    "::CVC4::theory::arrays::ArrayEnumerator" \
+    "theory/arrays/type_enumerator.h"
+
 # select a i  is  a[i]
 operator SELECT 2 "array select"
 
-- 
cgit v1.2.3