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.

18 files changed, 396 insertions, 4 deletions

diff --git a/test/Makefile.am b/test/Makefile.am
index 10b724a7d..aceef1b68 100644
--- a/test/Makefile.am
+++ b/test/Makefile.am
@@ -26,7 +26,7 @@ test "X$(AM_COLOR_TESTS)" != Xno \
   blu=''; \
   std=''; \
 }
-subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/lemmas regress/regress0/push-pop regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
+subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/datatypes regress/regress0/lemmas regress/regress0/push-pop regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
 check-recursive: check-pre
 .PHONY: check-pre
 check-pre:
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index c732ffbb2..12e2bb347 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . arith precedence uf uflra bv lemmas push-pop
+SUBDIRS = . arith precedence uf uflra bv datatypes lemmas push-pop
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 MAKEFLAGS = -k
diff --git a/test/regress/regress0/datatypes/Makefile b/test/regress/regress0/datatypes/Makefile
new file mode 100644
index 000000000..dc577ad8b
--- /dev/null
+++ b/test/regress/regress0/datatypes/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/datatypes
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
new file mode 100644
index 000000000..8d6dbbf73
--- /dev/null
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -0,0 +1,39 @@
+SUBDIRS = .
+
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+MAKEFLAGS = -k
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	\
+	datatype.cvc \
+	datatype0.cvc \
+	datatype1.cvc \
+	datatype2.cvc \
+	datatype3.cvc \
+	datatype4.cvc \
+	datatype13.cvc \
+	mutually-recursive.cvc \
+	rewriter.cvc \
+	typed_v1l50016-simp.cvc
+
+EXTRA_DIST = $(TESTS)
+
+if CVC4_BUILD_PROFILE_COMPETITION
+else
+TESTS += \
+	error.cvc
+endif
+
+# and make sure to distribute it
+EXTRA_DIST += \
+	error.cvc
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
diff --git a/test/regress/regress0/datatypes/datatype.cvc b/test/regress/regress0/datatypes/datatype.cvc
new file mode 100644
index 000000000..38a7a017d
--- /dev/null
+++ b/test/regress/regress0/datatypes/datatype.cvc
@@ -0,0 +1,8 @@
+% EXPECT: invalid
+% EXIT: 10
+
+DATATYPE nat = succ(pred : nat) | zero END;
+
+x : nat;
+
+QUERY (NOT is_succ(x) AND NOT is_zero(x));
diff --git a/test/regress/regress0/datatypes/datatype0.cvc b/test/regress/regress0/datatypes/datatype0.cvc
new file mode 100644
index 000000000..02ba3c8ea
--- /dev/null
+++ b/test/regress/regress0/datatypes/datatype0.cvc
@@ -0,0 +1,8 @@
+% EXPECT: valid
+% EXIT: 20
+
+DATATYPE nat = succ(pred : nat) | zero END;
+
+x : nat;
+
+QUERY (is_succ(x) OR is_zero(x));
diff --git a/test/regress/regress0/datatypes/datatype1.cvc b/test/regress/regress0/datatypes/datatype1.cvc
new file mode 100644
index 000000000..4c5984cb9
--- /dev/null
+++ b/test/regress/regress0/datatypes/datatype1.cvc
@@ -0,0 +1,11 @@
+% EXPECT: valid
+% EXIT: 20
+
+DATATYPE
+  tree = node(left : tree, right : tree) | leaf
+END;
+
+x : tree;
+z : tree;
+
+QUERY NOT (left(left(z)) = x AND is_node(z) AND z = x);
diff --git a/test/regress/regress0/datatypes/datatype13.cvc b/test/regress/regress0/datatypes/datatype13.cvc
new file mode 100644
index 000000000..3cf4def42
--- /dev/null
+++ b/test/regress/regress0/datatypes/datatype13.cvc
@@ -0,0 +1,44 @@
+% EXPECT: valid
+% EXIT: 20
+
+DATATYPE enum = enum1
+| enum2
+| enum3
+| enum4
+| enum5
+| enum6
+| enum7
+| enum8
+| enum9
+| enum10
+| enum11
+| enum12
+| enum13
+| enum14
+| enum15
+| enum16
+| enum17
+| enum18
+| enum19
+| enum20
+| enum21
+| enum22
+| enum23
+| enum24
+| enum25
+| enum26
+| enum27
+| enum28
+| enum29
+| enum30
+| enum31
+| enum32
+| enum33
+END;
+
+x,y:enum;
+
+ASSERT x = enum1;
+ASSERT y = enum33;
+QUERY x /= y;
+
diff --git a/test/regress/regress0/datatypes/datatype2.cvc b/test/regress/regress0/datatypes/datatype2.cvc
new file mode 100644
index 000000000..2e43b37e2
--- /dev/null
+++ b/test/regress/regress0/datatypes/datatype2.cvc
@@ -0,0 +1,17 @@
+% EXPECT: valid
+% EXIT: 20
+
+DATATYPE
+  nat = succ(pred : nat) | zero,
+  list = cons(car : tree, cdr : list) | null,
+  tree = node(data : nat, children : list) | leaf
+END;
+
+x : nat;
+y : list;
+z : tree;
+
+ASSERT x = succ(zero);
+ASSERT z = IF is_cons(y) THEN car(y) ELSE node(x, null) ENDIF;
+
+QUERY (NOT is_cons(y)) => pred(data(z)) = zero;
diff --git a/test/regress/regress0/datatypes/datatype3.cvc b/test/regress/regress0/datatypes/datatype3.cvc
new file mode 100644
index 000000000..53c9e2ffc
--- /dev/null
+++ b/test/regress/regress0/datatypes/datatype3.cvc
@@ -0,0 +1,11 @@
+% EXPECT: valid
+% EXIT: 20
+
+DATATYPE
+  tree = node(left : tree, right : tree) | leaf
+END;
+
+x : tree;
+z : tree;
+
+QUERY NOT (left(left(left(left(left(left(left(left(left(left(z)))))))))) = x AND is_node(z) AND z = x);
diff --git a/test/regress/regress0/datatypes/datatype4.cvc b/test/regress/regress0/datatypes/datatype4.cvc
new file mode 100644
index 000000000..87800919d
--- /dev/null
+++ b/test/regress/regress0/datatypes/datatype4.cvc
@@ -0,0 +1,10 @@
+% EXPECT: invalid
+% EXIT: 10
+DATATYPE
+   TypeGeneric = generic
+END;
+
+f: TypeGeneric -> INT;
+a: TypeGeneric;
+
+QUERY(f(a) = 0);
diff --git a/test/regress/regress0/datatypes/error.cvc b/test/regress/regress0/datatypes/error.cvc
new file mode 100644
index 000000000..66fa17e02
--- /dev/null
+++ b/test/regress/regress0/datatypes/error.cvc
@@ -0,0 +1,7 @@
+% EXPECT-ERROR: CVC4 Error:
+% EXPECT-ERROR: Parse Error: foo already declared
+% EXIT: 1
+
+DATATYPE single_ctor = foo(bar:REAL) END;
+DATATYPE double_ctor = foo(bar:REAL) END;
+
diff --git a/test/regress/regress0/datatypes/mutually-recursive.cvc b/test/regress/regress0/datatypes/mutually-recursive.cvc
new file mode 100644
index 000000000..68d5cd868
--- /dev/null
+++ b/test/regress/regress0/datatypes/mutually-recursive.cvc
@@ -0,0 +1,15 @@
+% EXPECT: valid
+% EXIT: 20
+
+DATATYPE nat = succ(pred : nat2) | zero,
+         nat2 = succ2(pred2 : nat) | zero2 END;
+
+x : nat;
+
+DATATYPE list = cons(car : tree, cdr: list) | nil,
+         tree = node(left : tree, right : tree) | leaf(data : list) END;
+
+y : tree;
+
+QUERY (is_succ(x) => is_zero2(pred(x)) OR is_succ2(pred(x)))
+  AND (is_leaf(y) => is_cons(data(y)) OR is_nil(data(y)));
diff --git a/test/regress/regress0/datatypes/rewriter.cvc b/test/regress/regress0/datatypes/rewriter.cvc
new file mode 100644
index 000000000..f031e0462
--- /dev/null
+++ b/test/regress/regress0/datatypes/rewriter.cvc
@@ -0,0 +1,13 @@
+% EXPECT: valid
+% EXIT: 20
+
+% simple test for rewriter cases
+
+DATATYPE single_ctor = foo(bar:REAL) END;
+DATATYPE double_ctor = foo2(bar2:REAL) | baz END;
+
+x: single_ctor;
+y: double_ctor;
+
+QUERY is_foo(x) AND bar2(foo2(0.0)) = 0.0;
+
diff --git a/test/regress/regress0/datatypes/typed_v1l50016-simp.cvc b/test/regress/regress0/datatypes/typed_v1l50016-simp.cvc
new file mode 100644
index 000000000..b273d99e9
--- /dev/null
+++ b/test/regress/regress0/datatypes/typed_v1l50016-simp.cvc
@@ -0,0 +1,44 @@
+% EXPECT: invalid
+% EXIT: 10
+
+DATATYPE
+  nat = succ(pred : nat) | zero,
+  list = cons(car : tree, cdr : list) | null,
+  tree = node(children : list) | leaf(data : nat)
+END;
+
+x1 : nat ;
+x2 : list ;
+x3 : tree ;
+
+QUERY
+
+(NOT is_zero((LET x154 = (LET x155 = node((LET x156 = (LET x157 = (LET x158 = (LET x159 = (LET x160 = (LET x161 = (LET x162 = cons((LET x163 = (LET x164 = (LET x165 = (LET x166 = (LET x167 = (LET x168 = (LET x169 = (LET x170 = (LET x171 = (LET x172 = (LET x173 = x3 IN
+ (IF is_node(x173) THEN children(x173) ELSE null ENDIF)) IN
+ (IF is_cons(x172) THEN car(x172) ELSE leaf(zero) ENDIF)) IN
+ (IF is_node(x171) THEN children(x171) ELSE null ENDIF)) IN
+ (IF is_cons(x170) THEN cdr(x170) ELSE null ENDIF)) IN
+ (IF is_cons(x169) THEN car(x169) ELSE leaf(zero) ENDIF)) IN
+ (IF is_node(x168) THEN children(x168) ELSE null ENDIF)) IN
+ (IF is_cons(x167) THEN cdr(x167) ELSE null ENDIF)) IN
+ (IF is_cons(x166) THEN cdr(x166) ELSE null ENDIF)) IN
+ (IF is_cons(x165) THEN cdr(x165) ELSE null ENDIF)) IN
+ (IF is_cons(x164) THEN cdr(x164) ELSE null ENDIF)) IN
+ (IF is_cons(x163) THEN car(x163) ELSE leaf(zero) ENDIF)),cons((LET x174 = cons(x3,(LET x175 = node(cons(node((LET x176 = x3 IN
+ (IF is_node(x176) THEN children(x176) ELSE null ENDIF))),x2)) IN
+ (IF is_node(x175) THEN children(x175) ELSE null ENDIF))) IN
+ (IF is_cons(x174) THEN car(x174) ELSE leaf(zero) ENDIF)),cons(leaf(succ((LET x177 = node(null) IN
+ (IF is_leaf(x177) THEN data(x177) ELSE zero ENDIF)))),(LET x178 = (LET x179 = (LET x180 = (LET x181 = node(x2) IN
+ (IF is_node(x181) THEN children(x181) ELSE null ENDIF)) IN
+ (IF is_cons(x180) THEN car(x180) ELSE leaf(zero) ENDIF)) IN
+ (IF is_node(x179) THEN children(x179) ELSE null ENDIF)) IN
+ (IF is_cons(x178) THEN cdr(x178) ELSE null ENDIF))))) IN
+ (IF is_cons(x162) THEN cdr(x162) ELSE null ENDIF)) IN
+ (IF is_cons(x161) THEN cdr(x161) ELSE null ENDIF)) IN
+ (IF is_cons(x160) THEN car(x160) ELSE leaf(zero) ENDIF)) IN
+ (IF is_node(x159) THEN children(x159) ELSE null ENDIF)) IN
+ (IF is_cons(x158) THEN cdr(x158) ELSE null ENDIF)) IN
+ (IF is_cons(x157) THEN cdr(x157) ELSE null ENDIF)) IN
+ (IF is_cons(x156) THEN cdr(x156) ELSE null ENDIF))) IN
+ (IF is_leaf(x155) THEN data(x155) ELSE zero ENDIF)) IN
+ (IF is_succ(x154) THEN pred(x154) ELSE zero ENDIF))));
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index bc49a7fac..646ebf9bb 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -33,6 +33,7 @@ UNIT_TESTS = \
 	context/cdvector_black \
 	util/assert_white \
 	util/bitvector_black \
+	util/datatype_black \
 	util/configuration_black \
 	util/congruence_closure_white \
 	util/output_black \
diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h
index 14fb3406a..a56f05c0f 100644
--- a/test/unit/util/bitvector_black.h
+++ b/test/unit/util/bitvector_black.h
@@ -5,13 +5,13 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011  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 Black box testing of CVC4::BitVector.
+ ** \brief Black box testing of CVC4::BitVector
  **
  ** Black box testing of CVC4::BitVector.
  **/
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
new file mode 100644
index 000000000..d0de68e33
--- /dev/null
+++ b/test/unit/util/datatype_black.h
@@ -0,0 +1,156 @@
+/*********************                                                        */
+/*! \file datatype_black.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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 Black box testing of CVC4::Datatype
+ **
+ ** Black box testing of CVC4::Datatype.
+ **/
+
+#include <cxxtest/TestSuite.h>
+#include <sstream>
+
+#include "util/datatype.h"
+
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+
+using namespace CVC4;
+using namespace std;
+
+class DatatypeBlack : public CxxTest::TestSuite {
+
+  ExprManager* d_em;
+
+public:
+
+  void setUp() {
+    d_em = new ExprManager();
+  }
+
+  void tearDown() {
+    delete d_em;
+  }
+
+  void testNat() {
+    Datatype nat("nat");
+
+    Datatype::Constructor succ("succ", "is_succ");
+    succ.addArg("pred", Datatype::SelfType());
+    nat.addConstructor(succ);
+
+    Datatype::Constructor zero("zero", "is_zero");
+    nat.addConstructor(zero);
+
+    cout << nat << std::endl;
+    DatatypeType natType = d_em->mkDatatypeType(nat);
+    cout << natType << std::endl;
+  }
+
+  void testTree() {
+    Datatype tree("tree");
+    Type integerType = d_em->integerType();
+
+    Datatype::Constructor node("node", "is_node");
+    node.addArg("left", Datatype::SelfType());
+    node.addArg("right", Datatype::SelfType());
+    tree.addConstructor(node);
+
+    Datatype::Constructor leaf("leaf", "is_leaf");
+    leaf.addArg("leaf", integerType);
+    tree.addConstructor(leaf);
+
+    cout << tree << std::endl;
+    DatatypeType treeType = d_em->mkDatatypeType(tree);
+    cout << treeType << std::endl;
+  }
+
+  void testList() {
+    Datatype list("list");
+    Type integerType = d_em->integerType();
+
+    Datatype::Constructor cons("cons", "is_cons");
+    cons.addArg("car", integerType);
+    cons.addArg("cdr", Datatype::SelfType());
+    list.addConstructor(cons);
+
+    Datatype::Constructor nil("nil", "is_nil");
+    list.addConstructor(nil);
+
+    cout << list << std::endl;
+    DatatypeType listType = d_em->mkDatatypeType(list);
+    cout << listType << std::endl;
+  }
+
+  void testMutualListTrees() {
+    /* Create two mutual datatypes corresponding to this definition
+     * block:
+     *
+     *   DATATYPE
+     *     tree = node(left: tree, right: tree) | leaf(list),
+     *     list = cons(car: tree, cdr: list) | nil
+     *   END;
+     */
+    Datatype tree("tree");
+    Datatype::Constructor node("node", "is_node");
+    node.addArg("left", Datatype::SelfType());
+    node.addArg("right", Datatype::SelfType());
+    tree.addConstructor(node);
+
+    Datatype::Constructor leaf("leaf", "is_leaf");
+    leaf.addArg("leaf", Datatype::UnresolvedType("list"));
+    tree.addConstructor(leaf);
+
+    cout << tree << std::endl;
+
+    Datatype list("list");
+    Datatype::Constructor cons("cons", "is_cons");
+    cons.addArg("car", Datatype::UnresolvedType("tree"));
+    cons.addArg("cdr", Datatype::SelfType());
+    list.addConstructor(cons);
+
+    Datatype::Constructor nil("nil", "is_nil");
+    list.addConstructor(nil);
+
+    cout << list << std::endl;
+
+    TS_ASSERT(! tree.isResolved());
+    TS_ASSERT(! node.isResolved());
+    TS_ASSERT(! leaf.isResolved());
+    TS_ASSERT(! list.isResolved());
+    TS_ASSERT(! cons.isResolved());
+    TS_ASSERT(! nil.isResolved());
+
+    vector<Datatype> dts;
+    dts.push_back(tree);
+    dts.push_back(list);
+    vector<DatatypeType> dtts = d_em->mkMutualDatatypeTypes(dts);
+
+    TS_ASSERT(dtts[0].getDatatype().isResolved());
+    TS_ASSERT(dtts[1].getDatatype().isResolved());
+
+    // add another constructor to list datatype resulting in an
+    // "otherNil-list"
+    Datatype::Constructor otherNil("otherNil", "is_otherNil");
+    dts[1].addConstructor(otherNil);
+
+    // remake the types
+    vector<DatatypeType> dtts2 = d_em->mkMutualDatatypeTypes(dts);
+
+    TS_ASSERT_DIFFERS(dtts, dtts2);
+    TS_ASSERT_DIFFERS(dtts[1], dtts2[1]);
+
+    // tree is also different because it's a tree of otherNil-lists
+    TS_ASSERT_DIFFERS(dtts[0], dtts2[0]);
+  }
+
+};/* class DatatypeBlack */