Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.

1 files changed, 66 insertions, 0 deletions

diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 3b1232772..932ec31c8 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -24,6 +24,8 @@
 #include <iostream>
 #include <sstream>
 
+#include "util/Assert.h"
+
 namespace CVC4 {
 namespace kind {
 
@@ -88,6 +90,70 @@ struct KindHashStrategy {
 };/* struct KindHashStrategy */
 
 }/* CVC4::kind namespace */
+
+/**
+ * The enumeration for the built-in atomic types.
+ */
+enum TypeConstant {
+  ${type_constant_list}
+  LAST_TYPE
+};/* enum TypeConstant */
+
+/**
+ * We hash the constants with their values.
+ */
+struct TypeConstantHashStrategy {
+  static inline size_t hash(TypeConstant tc) {
+    return tc;
+  }
+};/* struct BoolHashStrategy */
+
+inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
+  switch(typeConstant) {
+  ${type_constant_descriptions}
+  default:
+    out << "UNKNOWN_TYPE_CONSTANT";
+    break;
+  }
+  return out;
+}
+
+namespace theory {
+
+enum TheoryId {
+  ${theory_enum}
+  THEORY_LAST
+};
+
+inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
+  switch(theoryId) {
+  ${theory_descriptions}
+  default:
+    out << "UNKNOWN_THEORY";
+    break;
+  }
+  return out;
+}
+
+inline TheoryId kindToTheoryId(::CVC4::Kind k) {
+  switch (k) {
+    ${kind_to_theory_id}
+  default:
+    Unreachable();
+  }
+}
+
+inline TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) {
+  switch (typeConstant) {
+    ${type_constant_to_theory_id}
+  default:
+    Unreachable();
+  }
+}
+
+}/* theory namespace */
+
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__KIND_H */