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.

14 files changed, 236 insertions, 1 deletions

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))));