* theory "tree" rewriting implemented and works

* added TheoryArith::preRewrite() to test and demonstrate
  the use of pre-rewriting.

* array types and type checking now supported

* array type checking now supported

* theoryOf() dispatching properly to arrays now

* theories now required to implement a (simple) identify()
  function that returns a string identifying them for
  debugging/user output purposes

* added "builtin" theory to hold all built-in kinds and their
  type rules and rewriting (currently only exploding distinct)

* fixed production build failure (regarding NodeSetDepth)

* removed an errant "using namespace std" in util/bitvector.h
  (and made associated trivial fixes elsewhere)

* fixes to make unexpected exceptions more verbose in debug builds

* fixes to make multiple, cascading assertion fails simpler

* minor other fixes to comments etc.

1 files changed, 0 insertions, 134 deletions

diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds
deleted file mode 100644
index 50b858b31..000000000
--- a/src/expr/builtin_kinds
+++ /dev/null
@@ -1,134 +0,0 @@
-# builtin_kinds                                                       -*- sh -*-
-#
-# This "kinds" file is written in a domain-specific language for
-# declaring CVC4 kinds.  Comments are marked with #, as this line is.
-#
-# 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::KindHashStrategy \
-    "expr/kind.h" "The kind of nodes representing built-in operators"
-
-operator EQUAL 2 "equality"
-operator DISTINCT 2: "disequality"
-variable SKOLEM "skolem var"
-variable VARIABLE "variable"
-operator TUPLE 2: "a tuple"
-
-constant TYPE_CONSTANT \
-    ::CVC4::TypeConstant \
-    ::CVC4::TypeConstantHashStrategy \
-    "expr/type_constant.h" \
-    "basic types"
-operator FUNCTION_TYPE 2: "function type"
-variable SORT_TYPE "sort type"
-
-constant BITVECTOR_TYPE \
-	::CVC4::BitVectorSize \
-	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \
-	"util/bitvector.h" \
-	"bit-vector type" 
-