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

(limited to 'src/expr/mkexpr')

diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index e113a1e8f..8b21814dc 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -114,6 +114,12 @@ function endtheory {
   seen_endtheory=true
 }
 
+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