Partial merge from datatypes-merge branch:

1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.

No performance impact is expected outside of datatypes.  I'm verifying that that is the case with a cluster job this morning.

1 files changed, 12 insertions, 11 deletions

diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 40bf9992c..da2847d84 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -138,25 +138,26 @@ function constant {
   includes="${includes}
 #include \"$4\""
   mkConst_instantiations="${mkConst_instantiations}
-template <>
-Expr ExprManager::mkConst($2 const& val);
+#line $lineno \"$kf\"
+template <> Expr ExprManager::mkConst($2 const& val);
 "
   mkConst_implementations="${mkConst_implementations}
-template <>
-Expr ExprManager::mkConst($2 const& val) {
+#line $lineno \"$kf\"
+template <> Expr ExprManager::mkConst($2 const& val) {
+#line $lineno \"$kf\"
   return Expr(this, new Node(d_nodeManager->mkConst< $2 >(val)));
 }
 "
   getConst_instantiations="${getConst_instantiations}
-template <>
-$2 const & Expr::getConst< $2 >() const;
+#line $lineno \"$kf\"
+template <> $2 const & Expr::getConst< $2 >() const;
 "
   getConst_implementations="${getConst_implementations}
-template <>
-$2 const & Expr::getConst() const {
-  // check even for production builds
-  CheckArgument(getKind() == ::CVC4::kind::$1, *this,
-                \"Improper kind for getConst<$2>()\");
+#line $lineno \"$kf\"
+template <> $2 const & Expr::getConst() const {
+#line $lineno \"$kf\"
+  CheckArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\");
+#line $lineno \"$kf\"
   return d_node->getConst< $2 >();
 }
 "