Type enumerator infrastructure and uninterpreted constant support. No support yet for enumerating arrays, or for enumerating non-trivial datatypes.

1 files changed, 6 insertions, 0 deletions

diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index 71a8ea097..ffdc1d4c6 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -100,6 +100,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]}