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/mkinstantiator | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src/theory/mkinstantiator')

diff --git a/src/theory/mkinstantiator b/src/theory/mkinstantiator
index 1908d2e96..73b88986b 100755
--- a/src/theory/mkinstantiator
+++ b/src/theory/mkinstantiator
@@ -125,6 +125,12 @@ function endtheory {
 "
 }
 
+function enumerator {
+  # enumerator KIND enumerator-class header
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function typechecker {
   # typechecker header
   lineno=${BASH_LINENO[0]}
-- 
cgit v1.2.3