Highlights of this commit are:

* add NodeManagerWhite unit test

* change kind::APPLY to kind::APPLY_UF

* better APPLY handling: operators are no longer considered children

* more efficient pool lookup; the NodeValue doesn't have to be as fully constructed for the lookup to proceed

* extend DSL for kind declarations
  + new "theory" command declares a theory and its header.  theory_def.h no longer required.
  + arity enforced on operators
  + constant mapping, hashing, equality

* CONSTANT metakinds supported (via Node::getConst<T>(), for example, Node::getConst<CVC4::Rational>() gets a Rational out of a Node (assuming it is of CONST_RATIONAL kind)

* added CONST_RATIONAL and CONST_INTEGER kinds

* builtin operators (AND, OR, PLUS, etc..) returned by Node::getOperator() are now CONSTANT metakind and are created by NodeManager

* Pretty-printing of Nodes now has a depth limit settable by a stream manipulator (e.g. "cout << Node::setdepth(5) << m << endl;" prints DAG rooted at m to a depth of 5)

* getters added to Node, TNode, NodeValue, etc., for operators and metakinds

* build-time generators for kind.h, metakind.h, and theoryof_table.h headers now have a simpler design and flag errors better, and the templates (kind_template.h etc.) are easier to understand.

* DISTINCT is now a kind, and the SMT parser now passes through DISTINCT nodes instead of blowing them up into ANDs.  Until theory rewriting is online, though, DISTINCTs are directly blown up into conjunctions in TheoryEngine::rewrite().

* add gmpxx detection and inclusion

* better Asserts throughout, some documentation, cleanup

1 files changed, 248 insertions, 0 deletions

diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
new file mode 100755
index 000000000..15551d54d
--- /dev/null
+++ b/src/expr/mkmetakind
@@ -0,0 +1,248 @@
+#!/bin/bash
+#
+# mkmetakind
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2010  The CVC4 Project
+#
+# The purpose of this script is to create metakind.h from a prologue,
+# two middle sections, epilogue, and a list of theory kinds.
+#
+# This is kept distinct from kind.h because kind.h is a public header
+# and metakind.h is intended for the expr package only.
+#
+# Invocation:
+#
+#   mkmetakind prologue-file middle1-file middle2-file epilogue-file theory-kind-files...
+#
+# Output is to standard out.
+#
+
+copyright=2010
+
+cat <<EOF
+/*********************                                           -*- C++ -*-  */
+/** metakind.h
+ **
+ ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ **
+ ** This header file automatically generated by:
+ **
+ **     $0 $@
+ **
+ ** for the CVC4 project.
+ **/
+
+EOF
+
+me=$(basename "$0")
+
+template=$1; shift
+
+metakind_includes=
+metakind_kinds=
+metakind_constantMaps=
+metakind_compares=
+metakind_constHashes=
+metakind_constPrinters=
+metakind_ubchildren=
+metakind_lbchildren=
+
+seen_theory=false
+seen_theory_builtin=false
+
+function theory {
+  # theory T header
+
+  lineno=${BASH_LINENO[0]}
+
+  # 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 $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
+    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
+    echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
+  fi
+
+  theory_class=$1
+  if [ "$1" != builtin ]; then
+    metakind_includes="${metakind_includes}
+// #include \"theory/$b/$2\""
+  fi
+}
+
+function variable {
+  # variable K ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+  register_metakind VARIABLE "$1" 0
+}
+
+function operator {
+  # operator K #children ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+  register_metakind OPERATOR "$1" "$2"
+}
+
+function parameterized {
+  # parameterized K #children ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+  register_metakind PARAMETERIZED "$1" "$2"
+}
+
+function constant {
+  # constant K T Hasher header ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+
+  if ! expr "$2" : '\(::*\)' >/dev/null; then
+    echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::CVC4::Rational)" >&2
+  fi
+  if ! expr "$3" : '\(::*\)' >/dev/null; then
+    echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFcn)" >&2
+  fi
+
+  if [ -n "$4" ]; then
+    metakind_includes="${metakind_includes}
+#include \"$4\""
+  fi
+  register_metakind CONSTANT "$1" 0
+  metakind_constantMaps="${metakind_constantMaps}
+}/* CVC4::kind::metakind namespace */
+}/* CVC4::kind namespace */
+
+namespace expr {
+
+template <>
+inline const $2 & NodeValue::getConst< $2 >() const {
+  Assert(getKind() == ::CVC4::kind::$1);
+  // To support non-inlined CONSTANT-kinded NodeValues (those that are
+  // \"constructed\" when initially checking them against the NodeManager
+  // pool), we must check d_nchildren here.
+  return d_nchildren == 0
+    ? *reinterpret_cast< const $2 * >(d_children)
+    : *reinterpret_cast< const $2 * >(d_children[0]);
+}
+
+}/* CVC4::expr namespace */
+
+namespace kind {
+namespace metakind {
+
+template <>
+struct ConstantMap< $2 > {
+  // typedef $theory_class OwningTheory;
+  enum { kind = ::CVC4::kind::$1 };
+};/* ConstantMap< $2 > */
+
+template <>
+struct ConstantMapReverse< ::CVC4::kind::$1 > {
+  typedef $2 T;
+};/* ConstantMapReverse< ::CVC4::kind::$1 > */
+
+"
+  metakind_compares="${metakind_compares}
+    case kind::$1:
+      return NodeValueConstCompare< kind::$1, pool >::compare(nv1, nv2);
+"
+  metakind_constHashes="${metakind_constHashes}
+  case kind::$1:
+    return $3::hash(nv->getConst< $2 >());
+"
+  metakind_constPrinters="${metakind_constPrinters}
+  case kind::$1:
+    out << nv->getConst< $2 >();
+    break;
+"
+}
+
+function register_metakind {
+  mk=$1
+  k=$2
+  nc=$3
+  metakind_kinds="${metakind_kinds}    metakind::$mk, /* $k */
+";
+
+  # figure out the range given by $nc
+  if expr "$nc" : '^[0-9]\+$' >/dev/null; then
+    lb=$nc
+    ub=$nc
+  elif expr "$nc" : '^[0-9]\+:$' >/dev/null; then
+    let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1}'`
+    ub=MAX_CHILDREN
+  elif expr "$nc" : '^[0-9]\+:[0-9]\+$' >/dev/null; then
+    let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1" ub="$2}'`
+    if [ $ub -lt $lb ]; then
+      echo "$kf:$lineno: error in range \`$nc': LB < UB (in definition of $k)" >&2
+      exit 1
+    fi
+  else
+    echo "$kf:$lineno: can't parse range \`$nc' in definition of $k" >&2
+    exit 1
+  fi
+
+  metakind_lbchildren="${metakind_lbchildren}
+    $lb, /* $k */"
+  metakind_ubchildren="${metakind_ubchildren}
+    $ub, /* $k */"
+}
+
+function check_theory_seen {
+  if ! $seen_theory; then
+    echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
+    exit 1
+  fi
+}
+
+function check_builtin_theory_seen {
+  if ! $seen_theory_builtin; then
+    echo "$me: warning: no declaration for the builtin theory found" >&2
+  fi
+}
+
+while [ $# -gt 0 ]; do
+  kf=$1
+  seen_theory=false
+  b=$(basename $(dirname "$kf"))
+  metakind_kinds="${metakind_kinds}
+    /* from $b */
+"
+  source "$kf"
+  check_theory_seen
+  shift
+done
+check_builtin_theory_seen
+
+## output
+
+text=$(cat "$template")
+for var in metakind_includes metakind_kinds metakind_constantMaps \
+           metakind_compares metakind_constHashes metakind_constPrinters \
+           metakind_ubchildren metakind_lbchildren; do
+  eval text="\${text//\\\$\\{$var\\}/\${$var}}"
+done
+error=`expr "$text" : '.*\${\([^}]*\)}.*'`
+if [ -n "$error" ]; then
+  echo "$template:0: error: undefined replacement \${$error}" >&2
+  exit 1
+fi
+echo "$text"