From cd98370b338a0cc5343067151884a06431a1d92c Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 19 Nov 2009 22:07:01 +0000
Subject: testing framework, configure fixes, incorporations from meeting,
 continued work

---
 src/expr/kind.h | 30 +++++++++++++++++++++---------
 1 file changed, 21 insertions(+), 9 deletions(-)

(limited to 'src/expr/kind.h')

diff --git a/src/expr/kind.h b/src/expr/kind.h
index 9c4e4d5ab..98cc7e2e3 100644
--- a/src/expr/kind.h
+++ b/src/expr/kind.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4_KIND_H
-#define __CVC4_KIND_H
+#ifndef __CVC4__KIND_H
+#define __CVC4__KIND_H
 
 namespace CVC4 {
 
@@ -19,20 +19,32 @@ namespace CVC4 {
 // placeholder for design & development work.
 
 enum Kind {
+  /* undefined */
   UNDEFINED_KIND = -1,
+
+  /* built-ins */
   EQUAL,
+  ITE,
+  SKOLEM,
+  VARIABLE,
+
+  /* propositional connectives */
+  FALSE,
+  TRUE,
+
+  NOT,
+
   AND,
+  IFF,
   OR,
   XOR,
-  NOT,
+
+  /* from arith */
   PLUS,
-  MINUS,
-  ITE,
-  IFF,
-  SKOLEM,
-  SUBST
+  MINUS
+
 };/* enum Kind */
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_KIND_H */
+#endif /* __CVC4__KIND_H */
-- 
cgit v1.2.3