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

4 files changed, 18 insertions, 1 deletions

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]}
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 2f361cb63..89e77754f 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -124,6 +124,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]}
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 2e94e41be..654a1f94f 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -99,6 +99,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]}
diff --git a/src/expr/type.h b/src/expr/type.h
index 8e9190ac5..a813aec02 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -91,7 +91,6 @@ class CVC4_PUBLIC Type {
   friend class ExprManager;
   friend class NodeManager;
   friend class TypeNode;
-  friend struct TypeHashStrategy;
   friend std::ostream& CVC4::operator<<(std::ostream& out, const Type& t);
   friend TypeNode expr::exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap);