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, 114 insertions, 42 deletions

diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds
index f687e3b81..bb224aa91 100644
--- a/src/expr/builtin_kinds
+++ b/src/expr/builtin_kinds
@@ -2,47 +2,119 @@
 #
 # This "kinds" file is written in a domain-specific language for
 # declaring CVC4 kinds.  Comments are marked with #, as this line is.
-# There are four basic commands:
-#
-#   special K ["comment"]
-#   operator K ["comment"]
-#   parameterized K ["comment"]
-#   constant K T ["comment"]
-#
-# special K (with an optional comment) declares a kind K that has no
-# operator (it's not conceptually an APPLY of an operator to
-# operands).  This is appropriate for special built-ins,
-# e.g. VARIABLE.
-#
-# operator K (with an optional comment) declares a "built-in"
-# operator.  Really this is the same as "special" except that it has
-# an operator (automatically generated by NodeManager).
-#
-# parameterized K (with an optional comment) declares a "built-in"
-# parameterized operator.  This is a theory-specific APPLY, e.g.,
-# APPLY_UF, which applies its first parameter (say, "f"), to its
-# operands (say, "x" and "y", making the full application "f(x,y)").
-# Nodes with such a kind will have an operator (Node::hasOperator()
-# returns true, and Node::getOperator() returns the Node of functional
-# type representing "f" here), and the "children" are defined to be
-# this operator's parameters, and don't include the operator itself
-# (here, there are only two children "x" and "y").  For consistency
-# these should probably start with "APPLY_", but this is not enforced.
-#
-# constant K T (with an optional comment) declares a constant kind.  T
-# is the C++ type representing the constant internally.  For
-# consistency, these should probably start with "CONST_", but this is
-# not enforced.
-#
-# This file is actually an executable Bourne shell script (sourced by
-# the processing scripts after defining functions called "special,"
-# "operator," "parameterized," and "constant").  So if you need a
-# multi-line comment string, do it the Bourne-like way.  Please don't
-# do anything else in this file than using these commands though.
 #
+# The first non-blank, non-comment line in this file must be a theory
+# declaration:
+#
+#   theory T header
+#
+# There are four basic commands for declaring kinds:
+#
+#   variable K ["comment"]
+#
+#     This declares a kind K that has no operator (it's conceptually a
+#     VARIABLE).  This is appropriate for things like VARIABLE and
+#     SKOLEM.
+#
+#   operator K #children ["comment"]
+#
+#     Declares a "built-in" operator kind K.  Really this is the same
+#     as "variable" except that it has an operator (automatically
+#     generated by NodeManager).
+#
+#     You can specify an exact # of children required as the second
+#     argument to the operator command.  In debug mode, assertions are
+#     automatically included to ensure that no Nodes can ever be
+#     created violating this.  (FIXME: the public Expr stuff should
+#     enforce them regardless of whether debugging or not.)  For
+#     example, a binary operator could be specified as:
+#
+#         operator LESS_THAN 2 "arithmetic comparison, x < y"
+#
+#     Alternatively, a range can be specified for #children as
+#     "LB:[UB]", LB and UB representing lower and upper bounds on the
+#     number of children (inclusive).  If there is no lower bound, put
+#     a "0".  If there is no upper bound, leave the colon after LB,
+#     but omit UB.  For example, an N-ary operator might be defined
+#     as:
+#
+#         operator PLUS 2: "addition on two or more arguments"
+#
+#   parameterized K #children ["comment"]
+#
+#     Declares a "built-in" parameterized operator kind K.  This is a
+#     theory-specific APPLY, e.g., APPLY_UF, which applies its first
+#     parameter (say, "f"), to its operands (say, "x" and "y", making
+#     the full application "f(x,y)").  Nodes with such a kind will
+#     have an operator (Node::hasOperator() returns true, and
+#     Node::getOperator() returns the Node of functional type
+#     representing "f" here), and the "children" are defined to be
+#     this operator's parameters, and don't include the operator
+#     itself (here, there are only two children "x" and "y").
+#
+#     LB and UB are the same as documented for the operator command.
+#     The first parameter (the function being applied) does not count
+#     as a child.
+#
+#     For consistency these should start with "APPLY_", but this is
+#     not enforced.
+#
+#   constant K T Hasher header ["comment"]
+#
+#     Declares a constant kind K.  T is the C++ type representing the
+#     constant internally (and it should be
+#     ::fully::qualified::like::this), and header is the header needed
+#     to define it.  Hasher is a hash functor type defined like this:
+#
+#       struct MyHashFcn {
+#         static size_t hash(const T& val);
+#       };
+#
+#     For consistency, constants taking a non-void payload should
+#     start with "CONST_", but this is not enforced.
+#
+# Lines may be broken with a backslash between arguments; for example:
+#
+#     constant CONST_INT \
+#         int IntHash \
+#         "" \
+#         "This is a constant representing an INT.
+#         Its payload is the C++ int type.
+#         It is used by the theory of arithmetic."
+#
+# As shown in the example, ["comment"] fields may be broken across
+# multiple lines too.
+#
+# The expr package guarantees that Nodes built with kinds have the
+# following constraints imposed on them.  (The #children guarantee
+# only holds when assertions are turned on.)
+#
+#   Node meta-kind      has operator?      # children
+#   ==================  =================  =======================
+#   variable            no                 zero
+#   operator            yes                as documented above
+#   parameterized       yes                as documented above
+#   constant            no                 zero
+#
+# NOTE THAT This file is actually an executable Bourne shell script
+# (sourced by the processing scripts after defining functions called
+# "theory," "variable," "operator," "parameterized," and "constant").
+# Please don't do anything else in this file other than using these
+# commands.
+#
+
+theory builtin
+
+# A kind representing "inlined" operators defined with OPERATOR
+# Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
+# not stored that way.  If you ask for the operator of (EQUAL a b),
+# you'll get a special, singleton (BUILTIN EQUAL) Node.
+constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashFcn \
+    "expr/kind.h" "The kind of nodes representing built-in operators"
 
-operator EQUAL "equality"
-operator ITE "if-then-else"
-special SKOLEM "skolem var"
-special VARIABLE "variable"
-operator TUPLE "a tuple"
+operator EQUAL 2 "equality"
+operator DISTINCT 2: "disequality"
+operator ITE 3 "if-then-else"
+variable SKOLEM "skolem var"
+variable VARIABLE "variable"
+operator TUPLE 2: "a tuple"