7 files changed, 39 insertions, 22 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index 32ea1d2be..2891e64cf 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -23,12 +23,13 @@ EXTRA_DIST = \
 	@srcdir@/theoryof_table.h \
 	theoryof_table_template.h
 
-@srcdir@/theoryof_table.h: @srcdir@/mktheoryof theoryof_table_template.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+@srcdir@/theoryof_table.h: theoryof_table_template.h mktheoryof @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mktheoryof
+	$(AM_V_at)mv -f $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mktheoryof \
-		@srcdir@/theoryof_table_template.h \
+		$< \
 		`grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
-	> @srcdir@/theoryof_table.h) || (rm -f @srcdir@/theoryof_table.h && exit 1)
+	> $@) || (rm -f $@ && exit 1)
 
 BUILT_SOURCES = @srcdir@/theoryof_table.h
 dist-hook: @srcdir@/theoryof_table.h
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 2f2c77d36..3b79192d2 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -10,16 +10,14 @@ operator PLUS 2: "arithmetic addition"
 operator MULT 2: "arithmetic multiplication"
 operator UMINUS 1 "arithmetic negation"
 
-constant \
-    CONST_RATIONAL \
+constant CONST_RATIONAL \
     ::CVC4::Rational \
-    ::CVC4::RationalHashFcn \
+    ::CVC4::RationalHashStrategy \
     "util/rational.h" \
     "a multiple-precision rational constant"
 
-constant \
-    CONST_INTEGER \
+constant CONST_INTEGER \
     ::CVC4::Integer \
-    ::CVC4::IntegerHashFcn \
+    ::CVC4::IntegerHashStrategy \
     "util/integer.h" \
     "a multiple-precision integer constant"
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index 12869aad0..5fcf9299a 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -6,12 +6,18 @@
 
 theory ::CVC4::theory::booleans::TheoryBool "theory_bool.h"
 
-operator FALSE 0 "falsity"
-operator TRUE 0 "truth"
+constant CONST_BOOLEAN \
+    bool \
+    ::CVC4::BoolHashStrategy \
+    "util/bool.h" \
+    "truth and falsity"
 
-operator NOT 1 "logical not"
-operator AND 2: "logical and"
-operator IFF 2 "logical equivalence"
-operator IMPLIES 2 "logical implication"
-operator OR 2: "logical or"
-operator XOR 2: "exclusive or"
+# these are nonatomic because they have boolean structure.
+# i.e. nodes n with this kind return false for n.isAtomic()
+nonatomic_operator NOT 1 "logical not"
+nonatomic_operator AND 2: "logical and"
+nonatomic_operator IFF 2 "logical equivalence"
+nonatomic_operator IMPLIES 2 "logical implication"
+nonatomic_operator OR 2: "logical or"
+nonatomic_operator XOR 2: "exclusive or"
+nonatomic_operator ITE 3 "if-then-else"
diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof
index ef967342b..842e02a07 100755
--- a/src/theory/mktheoryof
+++ b/src/theory/mktheoryof
@@ -5,11 +5,11 @@
 # Copyright (c) 2010  The CVC4 Project
 #
 # The purpose of this script is to create theoryof_table.h from a
-# prologue, epilogue, and a list of theory kinds.
+# template and a list of theory kinds.
 #
 # Invocation:
 #
-#   mktheoryof prologue-file epilogue-file theory-kind-files...
+#   mktheoryof template-file theory-kind-files...
 #
 # Output is to standard out.
 #
@@ -17,7 +17,7 @@
 copyright=2010
 
 cat <<EOF
-/*********************                                           -*- C++ -*-  */
+/*********************                                                        */
 /** theoryof_table.h
  **
  ** Copyright $copyright  The AcSys Group, New York University, and as below.
@@ -84,6 +84,14 @@ function operator {
   do_theoryof "$1"
 }
 
+function nonatomic_operator {
+  # nonatomic_operator K #children ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  do_theoryof "$1"
+}
+
 function parameterized {
   # parameterized K #children ["comment"]
 
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 42bdaf2dd..4c3a43061 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -36,7 +36,7 @@ namespace theory {
 
 // rewrite cache support
 struct RewriteCacheTag {};
-typedef expr::Attribute<RewriteCacheTag, Node> RewriteCache;
+typedef expr::Attribute<RewriteCacheTag, TNode> RewriteCache;
 
 template <class T>
 class TheoryImpl;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f953f97b9..d29195011 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -111,7 +111,7 @@ Node TheoryEngine::rewrite(TNode in) {
   if(in.getKind() == kind::EQUAL) {
     Assert(in.getNumChildren() == 2);
     if(in[0] == in[1]) {
-      Node out = NodeManager::currentNM()->mkNode(kind::TRUE);
+      Node out = NodeManager::currentNM()->mkConst(true);
       //setRewriteCache(in, out);
       return out;
     }
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index b8c2d5a75..1d5daf7bd 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -129,6 +129,10 @@ class TheoryEngine {
    * while leaving the Node's kind alone.
    */
   Node rewriteChildren(TNode in) {
+    if(in.getMetaKind() == kind::metakind::CONSTANT) {
+      return in;
+    }
+
     NodeBuilder<> b(in.getKind());
     for(TNode::iterator c = in.begin(); c != in.end(); ++c) {
       b << rewrite(*c);