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.

7 files changed, 175 insertions, 92 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index d2b9197cb..12e7f2ff0 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -10,7 +10,6 @@ libexpr_la_SOURCES = \
 	node.cpp \
 	type_node.h \
 	type_node.cpp \
-	type_constant.h \
 	node_builder.h \
 	convenience_node_builders.h \
 	type.h \
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 */
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 35a245a84..0b384d518 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -72,22 +72,42 @@ function theory {
   # this script doesn't care about the theory class information, but
   # makes does make sure it's there
   seen_theory=true
-  if [ "$1" = builtin ]; then
+  if [ "$1" = THEORY_BUILTIN ]; then
     if $seen_theory_builtin; then
       echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
       exit 1
     fi
     seen_theory_builtin=true
-  elif [ -z "$1" -o -z "$2" ]; then
+  elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then
     echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
     exit 1
-  elif ! expr "$1" : '\(::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
-  elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then
+  elif ! expr "$2" : '\(::*\)' >/dev/null; then
+    echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
+  elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then
     echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
   fi
 }
 
+function rewriter {
+  # rewriter class header
+  lineno=${BASH_LINENO[0]}
+}
+
+function properties {
+    # properties prop*
+    lineno=${BASH_LINENO[0]}
+}
+
+function endtheory {
+  # endtheory
+  lineno=${BASH_LINENO[0]}
+}
+
+function sort {
+  # sort TYPE ["comment"]
+  lineno=${BASH_LINENO[0]}
+}
+
 function variable {
   # variable K ["comment"]
 
diff --git a/src/expr/mkkind b/src/expr/mkkind
index ab80224eb..d790a0195 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -37,10 +37,18 @@ template=$1; shift
 
 kind_decls=
 kind_printers=
+kind_to_theory_id=
+
+type_constant_descriptions=
+type_constant_list=
+type_constant_to_theory_id= 
 
 seen_theory=false
 seen_theory_builtin=false
 
+theory_enum=
+theory_descriptions=
+
 function theory {
   # theory T header
 
@@ -49,20 +57,50 @@ function theory {
   # this script doesn't care about the theory class information, but
   # makes does make sure it's there
   seen_theory=true
-  if [ "$1" = builtin ]; then
+  if [ "$1" = THEORY_BUILTIN ]; then
     if $seen_theory_builtin; then
       echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
       exit 1
     fi
     seen_theory_builtin=true
-  elif [ -z "$1" -o -z "$2" ]; then
+  elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then
     echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
     exit 1
-  elif ! expr "$1" : '\(::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
-  elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then
+  elif ! expr "$2" : '\(::*\)' >/dev/null; then
+    echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
+  elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then
     echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
   fi
+  
+  theory_id="$1"
+  theory_enum="$1, 
+    ${theory_enum}" 
+  theory_descriptions="${theory_descriptions}    case ${theory_id}: out << \"${theory_id}\"; break;
+"
+}
+
+function properties {
+  # rewriter class header
+  lineno=${BASH_LINENO[0]}
+}
+
+function endtheory {
+  # endtheory
+  lineno=${BASH_LINENO[0]}
+}
+
+function rewriter {
+  # properties prop*
+  lineno=${BASH_LINENO[0]}
+}
+
+function sort {
+  # sort TYPE ["comment"]
+  
+  lineno=${BASH_LINENO[0]}
+  
+  check_theory_seen
+  register_sort "$1" "$2"
 }
 
 function variable {
@@ -101,6 +139,18 @@ function constant {
   register_kind "$1" 0 "$5"
 }
 
+function register_sort {
+  id=$1
+  comment=$2
+  
+  type_constant_list="${type_constant_list}   ${id}, /**< ${comment} */
+"
+  type_constant_descriptions="${type_constant_descriptions}   case $id:  out << \"${comment}\"; break;
+"
+  type_constant_to_theory_id="${type_constant_to_theory_id}   case $id: return $theory_id; break;
+" 
+}
+
 function register_kind {
   r=$1
   nc=$2
@@ -110,6 +160,8 @@ function register_kind {
 "
   kind_printers="${kind_printers}  case $r: out << \"$r\"; break;
 "
+  kind_to_theory_id="${kind_to_theory_id}   case kind::$r: return $theory_id; break;
+"
 }
 
 function check_theory_seen {
@@ -144,7 +196,7 @@ check_builtin_theory_seen
 ## output
 
 text=$(cat "$template")
-for var in kind_decls kind_printers; do
+for var in kind_decls kind_printers kind_to_theory_id theory_enum type_constant_list type_constant_descriptions type_constant_to_theory_id theory_descriptions; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
 error=`expr "$text" : '.*\${\([^}]*\)}.*'`
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 4ce0c6262..0d0ff4475 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -60,18 +60,18 @@ function theory {
   # this script doesn't care about the theory class information, but
   # makes does make sure it's there
   seen_theory=true
-  if [ "$1" = builtin ]; then
+  if [ "$1" = THEORY_BUILTIN ]; then
     if $seen_theory_builtin; then
       echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
       exit 1
     fi
     seen_theory_builtin=true
-  elif [ -z "$1" -o -z "$2" ]; then
+  elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then
     echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
     exit 1
-  elif ! expr "$1" : '\(::*\)' >/dev/null; then
+  elif ! expr "$2" : '\(::*\)' >/dev/null; then
     echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
-  elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then
+  elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then
     echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
   fi
 
@@ -80,6 +80,26 @@ function theory {
 // #include \"theory/$b/$2\""
 }
 
+function properties {
+  # properties prop*
+  lineno=${BASH_LINENO[0]}
+}
+
+function endtheory {
+  # endtheory
+  lineno=${BASH_LINENO[0]}
+}
+
+function rewriter {
+  # rewriter class header
+  lineno=${BASH_LINENO[0]}
+}
+
+function sort {
+  # sort TYPE ["comment"]
+  lineno=${BASH_LINENO[0]}
+}
+
 function variable {
   # variable K ["comment"]
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 04de81b1c..117497539 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -974,6 +974,7 @@ inline TypeNode NodeManager::mkTypeNode(Kind kind,
 
 inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
   Node n = mkVar(type);
+  n.setAttribute(TypeAttr(), type);
   n.setAttribute(expr::VarNameAttr(), name);
   return n;
 }
@@ -981,6 +982,7 @@ inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
 inline Node* NodeManager::mkVarPtr(const std::string& name,
                                    const TypeNode& type) {
   Node* n = mkVarPtr(type);
+  n->setAttribute(TypeAttr(), type);
   n->setAttribute(expr::VarNameAttr(), name);
   return n;
 }
diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h
deleted file mode 100644
index 23c23cc9f..000000000
--- a/src/expr/type_constant.h
+++ /dev/null
@@ -1,76 +0,0 @@
-/*********************                                                        */
-/*! \file type_constant.h
- ** \verbatim
- ** Original author: dejan
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Interface for expression types.
- **
- ** Interface for expression types
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__TYPE_CONSTANT_H
-#define __CVC4__TYPE_CONSTANT_H
-
-#include <iostream>
-
-namespace CVC4 {
-
-/**
- * The enumeration for the built-in atomic types.
- */
-enum TypeConstant {
-  /** The Boolean type */
-  BOOLEAN_TYPE,
-  /** The integer type */
-  INTEGER_TYPE,
-  /** The real type */
-  REAL_TYPE,
-  /** The kind type (type of types) */
-  KIND_TYPE,
-  /** The builtin operator type (type of non-PARAMETERIZED operators) */
-  BUILTIN_OPERATOR_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) {
-  case BOOLEAN_TYPE:
-    out << "BOOLEAN";
-    break;
-  case INTEGER_TYPE:
-    out << "INTEGER";
-    break;
-  case REAL_TYPE:
-    out << "REAL";
-    break;
-  case KIND_TYPE:
-    out << "KIND";
-    break;
-  default:
-    out << "UNKNOWN_TYPE_CONSTANT";
-    break;
-  }
-  return out;
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__TYPE_CONSTANT_H */