added 10 benchmarks to regress/regress0/datatypes from paper

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 8d6dbbf7340fbee5c0ad4ab019bdcdc380b50262..efc9954c29795f62e9d769fb92a78d6582d27db4 100644 (file)
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -16,7 +16,18 @@ TESTS =      \
        datatype13.cvc \
        mutually-recursive.cvc \
        rewriter.cvc \
-       typed_v1l50016-simp.cvc
+       typed_v1l50016-simp.cvc \
+       typed_v10l30054.cvc \
+       typed_v1l80005.cvc \
+       typed_v2l30079.cvc \
+       typed_v3l20092.cvc \
+       typed_v5l30069.cvc \
+       v10l40099.cvc \
+       v1l20009.cvc \
+       v2l40025.cvc \
+       v3l60006.cvc \
+       v5l30058.cvc
+
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress0/datatypes/typed_v10l30054.cvc b/test/regress/regress0/datatypes/typed_v10l30054.cvc
new file mode 100644 (file)
index 0000000..80c1488
--- /dev/null
+++ b/test/regress/regress0/datatypes/typed_v10l30054.cvc
@@ -0,0 +1,44 @@
+% EXPECT: valid\r
+% EXIT: 20\r
+DATATYPE\r
+  nat = succ(pred : nat) | zero,\r
+  list = cons(car : tree, cdr : list) | null,\r
+  tree = node(children : list) | leaf(data : nat)\r
+END;\r
+\r
+x1 : nat ;\r
+x2 : nat ;\r
+x3 : nat ;\r
+x4 : nat ;\r
+x5 : nat ;\r
+x6 : nat ;\r
+x7 : nat ;\r
+x8 : nat ;\r
+x9 : nat ;\r
+x10 : nat ;\r
+x11 : list ;\r
+x12 : list ;\r
+x13 : list ;\r
+x14 : list ;\r
+x15 : list ;\r
+x16 : list ;\r
+x17 : list ;\r
+x18 : list ;\r
+x19 : list ;\r
+x20 : list ;\r
+x21 : tree ;\r
+x22 : tree ;\r
+x23 : tree ;\r
+x24 : tree ;\r
+x25 : tree ;\r
+x26 : tree ;\r
+x27 : tree ;\r
+x28 : tree ;\r
+x29 : tree ;\r
+x30 : tree ;\r
+\r
+QUERY \r
+\r
+(NOT (((x4 = x4)\r
+ AND (NOT is_leaf((LET x81 = null IN (IF is_cons(x81) THEN car(x81) ELSE leaf(zero) ENDIF)))))\r
+ AND (NOT (x10 = x2))));\r

diff --git a/test/regress/regress0/datatypes/typed_v1l80005.cvc b/test/regress/regress0/datatypes/typed_v1l80005.cvc
new file mode 100644 (file)
index 0000000..9a85f1b
--- /dev/null
+++ b/test/regress/regress0/datatypes/typed_v1l80005.cvc
@@ -0,0 +1,22 @@
+% EXPECT: valid\r
+% EXIT: 20\r
+DATATYPE\r
+  nat = succ(pred : nat) | zero,\r
+  list = cons(car : tree, cdr : list) | null,\r
+  tree = node(children : list) | leaf(data : nat)\r
+END;\r
+\r
+x1 : nat ;\r
+x2 : list ;\r
+x3 : tree ;\r
+\r
+QUERY \r
+\r
+(NOT ((((((((NOT is_succ((LET x90 = (LET x91 = node(cons(x3,cons((LET x92 = (LET x93 = cons(node(x2),(LET x94 = node((LET x95 = null IN (IF is_cons(x95) THEN cdr(x95) ELSE null ENDIF))) IN (IF is_node(x94) THEN children(x94) ELSE null ENDIF))) IN (IF is_cons(x93) THEN cdr(x93) ELSE null ENDIF)) IN (IF is_cons(x92) THEN car(x92) ELSE leaf(zero) ENDIF)),cons(node(cons(node((LET x96 = node(x2) IN (IF is_node(x96) THEN children(x96) ELSE null ENDIF))),cons((LET x97 = (LET x98 = leaf((LET x99 = node((LET x100 = null IN (IF is_cons(x100) THEN cdr(x100) ELSE null ENDIF))) IN (IF is_leaf(x99) THEN data(x99) ELSE zero ENDIF))) IN (IF is_node(x98) THEN children(x98) ELSE null ENDIF)) IN (IF is_cons(x97) THEN car(x97) ELSE leaf(zero) ENDIF)),(LET x101 = (LET x102 = (LET x103 = node(x2) IN (IF is_node(x103) THEN children(x103) ELSE null ENDIF)) IN (IF is_cons(x102) THEN car(x102) ELSE leaf(zero) ENDIF)) IN (IF is_node(x101) THEN children(x101) ELSE null ENDIF))))),cons(leaf(succ((LET x104 = (LET x105 = (LET x106 = null IN (IF is_cons(x106) THEN car(x106) ELSE leaf(zero) ENDIF)) IN (IF is_leaf(x105) THEN data(x105) ELSE zero ENDIF)) IN (IF is_succ(x104) THEN pred(x104) ELSE zero ENDIF)))),null))))) IN (IF is_leaf(x91) THEN data(x91) ELSE zero ENDIF)) IN (IF is_succ(x90) THEN pred(x90) ELSE zero ENDIF))))\r
+ AND (node((LET x87 = cons((LET x88 = null IN (IF is_cons(x88) THEN car(x88) ELSE leaf(zero) ENDIF)),(LET x89 = cons(node(cons(x3,x2)),null) IN (IF is_cons(x89) THEN cdr(x89) ELSE null ENDIF))) IN (IF is_cons(x87) THEN cdr(x87) ELSE null ENDIF))) = (LET x85 = (LET x86 = x3 IN (IF is_node(x86) THEN children(x86) ELSE null ENDIF)) IN (IF is_cons(x85) THEN car(x85) ELSE leaf(zero) ENDIF))))\r
+ AND is_null((LET x83 = cons(node(null),(LET x84 = x2 IN (IF is_cons(x84) THEN cdr(x84) ELSE null ENDIF))) IN (IF is_cons(x83) THEN cdr(x83) ELSE null ENDIF))))\r
+ AND is_null(cons(leaf((LET x77 = succ((LET x78 = (LET x79 = zero IN (IF is_succ(x79) THEN pred(x79) ELSE zero ENDIF)) IN (IF is_succ(x78) THEN pred(x78) ELSE zero ENDIF))) IN (IF is_succ(x77) THEN pred(x77) ELSE zero ENDIF))),(LET x80 = leaf((LET x81 = succ((LET x82 = x3 IN (IF is_leaf(x82) THEN data(x82) ELSE zero ENDIF))) IN (IF is_succ(x81) THEN pred(x81) ELSE zero ENDIF))) IN (IF is_node(x80) THEN children(x80) ELSE null ENDIF)))))\r
+ AND is_node(leaf(zero)))\r
+ AND (NOT (x2 = null)))\r
+ AND (NOT is_zero((LET x76 = node(cons(leaf(succ(zero)),null)) IN (IF is_leaf(x76) THEN data(x76) ELSE zero ENDIF)))))\r
+ AND is_null((LET x74 = (LET x75 = null IN (IF is_cons(x75) THEN cdr(x75) ELSE null ENDIF)) IN (IF is_cons(x74) THEN cdr(x74) ELSE null ENDIF)))));\r

diff --git a/test/regress/regress0/datatypes/typed_v2l30079.cvc b/test/regress/regress0/datatypes/typed_v2l30079.cvc
new file mode 100644 (file)
index 0000000..990cfbb
--- /dev/null
+++ b/test/regress/regress0/datatypes/typed_v2l30079.cvc
@@ -0,0 +1,20 @@
+% EXPECT: invalid\r
+% EXIT: 10\r
+DATATYPE\r
+  nat = succ(pred : nat) | zero,\r
+  list = cons(car : tree, cdr : list) | null,\r
+  tree = node(children : list) | leaf(data : nat)\r
+END;\r
+\r
+x1 : nat ;\r
+x2 : nat ;\r
+x3 : list ;\r
+x4 : list ;\r
+x5 : tree ;\r
+x6 : tree ;\r
+\r
+QUERY \r
+\r
+(NOT ((is_node(x6)\r
+ AND (x6 = x5))\r
+ AND (NOT (null = cons(x6,x3)))));\r

diff --git a/test/regress/regress0/datatypes/typed_v3l20092.cvc b/test/regress/regress0/datatypes/typed_v3l20092.cvc
new file mode 100644 (file)
index 0000000..43dfa33
--- /dev/null
+++ b/test/regress/regress0/datatypes/typed_v3l20092.cvc
@@ -0,0 +1,22 @@
+% EXPECT: valid\r
+% EXIT: 20\r
+DATATYPE\r
+  nat = succ(pred : nat) | zero,\r
+  list = cons(car : tree, cdr : list) | null,\r
+  tree = node(children : list) | leaf(data : nat)\r
+END;\r
+\r
+x1 : nat ;\r
+x2 : nat ;\r
+x3 : nat ;\r
+x4 : list ;\r
+x5 : list ;\r
+x6 : list ;\r
+x7 : tree ;\r
+x8 : tree ;\r
+x9 : tree ;\r
+\r
+QUERY \r
+\r
+(NOT (((LET x137 = x1 IN (IF is_succ(x137) THEN pred(x137) ELSE zero ENDIF)) = (LET x135 = (LET x136 = null IN (IF is_cons(x136) THEN car(x136) ELSE leaf(zero) ENDIF)) IN (IF is_leaf(x135) THEN data(x135) ELSE zero ENDIF)))\r
+ AND (cons(node(x6),(LET x134 = x7 IN (IF is_node(x134) THEN children(x134) ELSE null ENDIF))) = (LET x132 = node((LET x133 = x6 IN (IF is_cons(x133) THEN cdr(x133) ELSE null ENDIF))) IN (IF is_node(x132) THEN children(x132) ELSE null ENDIF)))));\r

diff --git a/test/regress/regress0/datatypes/typed_v5l30069.cvc b/test/regress/regress0/datatypes/typed_v5l30069.cvc
new file mode 100644 (file)
index 0000000..662391b
--- /dev/null
+++ b/test/regress/regress0/datatypes/typed_v5l30069.cvc
@@ -0,0 +1,29 @@
+% EXPECT: valid\r
+% EXIT: 20\r
+DATATYPE\r
+  nat = succ(pred : nat) | zero,\r
+  list = cons(car : tree, cdr : list) | null,\r
+  tree = node(children : list) | leaf(data : nat)\r
+END;\r
+\r
+x1 : nat ;\r
+x2 : nat ;\r
+x3 : nat ;\r
+x4 : nat ;\r
+x5 : nat ;\r
+x6 : list ;\r
+x7 : list ;\r
+x8 : list ;\r
+x9 : list ;\r
+x10 : list ;\r
+x11 : tree ;\r
+x12 : tree ;\r
+x13 : tree ;\r
+x14 : tree ;\r
+x15 : tree ;\r
+\r
+QUERY \r
+\r
+(NOT ((is_cons((LET x121 = leaf((LET x122 = x13 IN (IF is_leaf(x122) THEN data(x122) ELSE zero ENDIF))) IN (IF is_node(x121) THEN children(x121) ELSE null ENDIF)))\r
+ AND (x15 = node(x6)))\r
+ AND (NOT is_cons(x10))));\r

diff --git a/test/regress/regress0/datatypes/v10l40099.cvc b/test/regress/regress0/datatypes/v10l40099.cvc
new file mode 100644 (file)
index 0000000..f2cc332
--- /dev/null
+++ b/test/regress/regress0/datatypes/v10l40099.cvc
@@ -0,0 +1,45 @@
+% EXPECT: valid\r
+% EXIT: 20\r
+DATATYPE\r
+  nat = succ(pred : nat) | zero,\r
+  list = cons(car : tree, cdr : list) | null,\r
+  tree = node(children : list) | leaf(data : nat)\r
+END;\r
+\r
+x1 : nat ;\r
+x2 : nat ;\r
+x3 : nat ;\r
+x4 : nat ;\r
+x5 : nat ;\r
+x6 : nat ;\r
+x7 : nat ;\r
+x8 : nat ;\r
+x9 : nat ;\r
+x10 : nat ;\r
+x11 : list ;\r
+x12 : list ;\r
+x13 : list ;\r
+x14 : list ;\r
+x15 : list ;\r
+x16 : list ;\r
+x17 : list ;\r
+x18 : list ;\r
+x19 : list ;\r
+x20 : list ;\r
+x21 : tree ;\r
+x22 : tree ;\r
+x23 : tree ;\r
+x24 : tree ;\r
+x25 : tree ;\r
+x26 : tree ;\r
+x27 : tree ;\r
+x28 : tree ;\r
+x29 : tree ;\r
+x30 : tree ;\r
+\r
+QUERY \r
+\r
+(NOT ((((NOT is_zero(x3))\r
+ AND (x8 = zero))\r
+ AND (NOT (x25 = x28)))\r
+ AND (NOT is_zero(x8))));\r

diff --git a/test/regress/regress0/datatypes/v1l20009.cvc b/test/regress/regress0/datatypes/v1l20009.cvc
new file mode 100644 (file)
index 0000000..9eea247
--- /dev/null
+++ b/test/regress/regress0/datatypes/v1l20009.cvc
@@ -0,0 +1,16 @@
+% EXPECT: valid\r
+% EXIT: 20\r
+DATATYPE\r
+  nat = succ(pred : nat) | zero,\r
+  list = cons(car : tree, cdr : list) | null,\r
+  tree = node(children : list) | leaf(data : nat)\r
+END;\r
+\r
+x1 : nat ;\r
+x2 : list ;\r
+x3 : tree ;\r
+\r
+QUERY \r
+\r
+(NOT ((NOT is_zero(pred(succ(pred(zero)))))\r
+ AND (data(x3) = succ(pred(data(leaf(succ(data(car(null))))))))));\r

diff --git a/test/regress/regress0/datatypes/v2l40025.cvc b/test/regress/regress0/datatypes/v2l40025.cvc
new file mode 100644 (file)
index 0000000..f78d5b2
--- /dev/null
+++ b/test/regress/regress0/datatypes/v2l40025.cvc
@@ -0,0 +1,21 @@
+% EXPECT: valid\r
+% EXIT: 20\r
+DATATYPE\r
+  nat = succ(pred : nat) | zero,\r
+  list = cons(car : tree, cdr : list) | null,\r
+  tree = node(children : list) | leaf(data : nat)\r
+END;\r
+\r
+x1 : nat ;\r
+x2 : nat ;\r
+x3 : list ;\r
+x4 : list ;\r
+x5 : tree ;\r
+x6 : tree ;\r
+\r
+QUERY \r
+\r
+(NOT (((is_leaf(x5)\r
+ AND (NOT (x2 = x1)))\r
+ AND (x2 = pred(pred(zero))))\r
+ AND (NOT is_node(node(null)))));\r

diff --git a/test/regress/regress0/datatypes/v3l60006.cvc b/test/regress/regress0/datatypes/v3l60006.cvc
new file mode 100644 (file)
index 0000000..a681599
--- /dev/null
+++ b/test/regress/regress0/datatypes/v3l60006.cvc
@@ -0,0 +1,26 @@
+% EXPECT: invalid\r
+% EXIT: 10\r
+DATATYPE\r
+  nat = succ(pred : nat) | zero,\r
+  list = cons(car : tree, cdr : list) | null,\r
+  tree = node(children : list) | leaf(data : nat)\r
+END;\r
+\r
+x1 : nat ;\r
+x2 : nat ;\r
+x3 : nat ;\r
+x4 : list ;\r
+x5 : list ;\r
+x6 : list ;\r
+x7 : tree ;\r
+x8 : tree ;\r
+x9 : tree ;\r
+\r
+QUERY \r
+\r
+(NOT ((((((NOT is_succ(pred(data(leaf(x3)))))\r
+ AND (x1 = zero))\r
+ AND (NOT is_zero(succ(succ(zero)))))\r
+ AND (NOT (x3 = x2)))\r
+ AND (x4 = cdr(x5)))\r
+ AND is_cons(cons(x8,x5))));\r

diff --git a/test/regress/regress0/datatypes/v5l30058.cvc b/test/regress/regress0/datatypes/v5l30058.cvc
new file mode 100644 (file)
index 0000000..4159f6c
--- /dev/null
+++ b/test/regress/regress0/datatypes/v5l30058.cvc
@@ -0,0 +1,29 @@
+% EXPECT: invalid\r
+% EXIT: 10\r
+DATATYPE\r
+  nat = succ(pred : nat) | zero,\r
+  list = cons(car : tree, cdr : list) | null,\r
+  tree = node(children : list) | leaf(data : nat)\r
+END;\r
+\r
+x1 : nat ;\r
+x2 : nat ;\r
+x3 : nat ;\r
+x4 : nat ;\r
+x5 : nat ;\r
+x6 : list ;\r
+x7 : list ;\r
+x8 : list ;\r
+x9 : list ;\r
+x10 : list ;\r
+x11 : tree ;\r
+x12 : tree ;\r
+x13 : tree ;\r
+x14 : tree ;\r
+x15 : tree ;\r
+\r
+QUERY \r
+\r
+(NOT (((NOT (node(x9) = car(x8)))\r
+ AND (node(x6) = x11))\r
+ AND (NOT is_node(x15))));\r