diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-05-13 20:42:57 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-05-13 20:42:57 +0000 |
commit | 69c9ec0e1e42f3f2f2f79d3e98398c5cd1559c66 (patch) | |
tree | 4761dc1485594a7d26630b3eea7f305dde0e2766 /test | |
parent | 9462ccde8b06aae3b13e271465ab74b2e312a095 (diff) |
* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio
branch)
* add Theory::isSharedTermFact() -- it currently always returns false,
pending theory combination work
* Add "unknown" cardinalities to Cardinality class
* Fix run_regression script to handle CRLF line terminators on Macs
(where sed is non-GNU)
* Convert CRLF line terminators in datatypes regressions to LF
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/datatypes/typed_v10l30054.cvc | 88 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/typed_v1l80005.cvc | 44 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/typed_v2l30079.cvc | 40 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/typed_v3l20092.cvc | 44 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/typed_v5l30069.cvc | 58 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/v10l40099.cvc | 90 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/v1l20009.cvc | 32 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/v2l40025.cvc | 42 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/v3l60006.cvc | 52 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/v5l30058.cvc | 58 | ||||
-rwxr-xr-x | test/regress/run_regression | 12 | ||||
-rw-r--r-- | test/unit/expr/type_cardinality_public.h | 3 |
12 files changed, 282 insertions, 281 deletions
diff --git a/test/regress/regress0/datatypes/typed_v10l30054.cvc b/test/regress/regress0/datatypes/typed_v10l30054.cvc index 80c148863..3714ece35 100644 --- a/test/regress/regress0/datatypes/typed_v10l30054.cvc +++ b/test/regress/regress0/datatypes/typed_v10l30054.cvc @@ -1,44 +1,44 @@ -% EXPECT: valid
-% EXIT: 20
-DATATYPE
- nat = succ(pred : nat) | zero,
- list = cons(car : tree, cdr : list) | null,
- tree = node(children : list) | leaf(data : nat)
-END;
-
-x1 : nat ;
-x2 : nat ;
-x3 : nat ;
-x4 : nat ;
-x5 : nat ;
-x6 : nat ;
-x7 : nat ;
-x8 : nat ;
-x9 : nat ;
-x10 : nat ;
-x11 : list ;
-x12 : list ;
-x13 : list ;
-x14 : list ;
-x15 : list ;
-x16 : list ;
-x17 : list ;
-x18 : list ;
-x19 : list ;
-x20 : list ;
-x21 : tree ;
-x22 : tree ;
-x23 : tree ;
-x24 : tree ;
-x25 : tree ;
-x26 : tree ;
-x27 : tree ;
-x28 : tree ;
-x29 : tree ;
-x30 : tree ;
-
-QUERY
-
-(NOT (((x4 = x4)
- AND (NOT is_leaf((LET x81 = null IN (IF is_cons(x81) THEN car(x81) ELSE leaf(zero) ENDIF)))))
- AND (NOT (x10 = x2))));
+% EXPECT: valid +% EXIT: 20 +DATATYPE + nat = succ(pred : nat) | zero, + list = cons(car : tree, cdr : list) | null, + tree = node(children : list) | leaf(data : nat) +END; + +x1 : nat ; +x2 : nat ; +x3 : nat ; +x4 : nat ; +x5 : nat ; +x6 : nat ; +x7 : nat ; +x8 : nat ; +x9 : nat ; +x10 : nat ; +x11 : list ; +x12 : list ; +x13 : list ; +x14 : list ; +x15 : list ; +x16 : list ; +x17 : list ; +x18 : list ; +x19 : list ; +x20 : list ; +x21 : tree ; +x22 : tree ; +x23 : tree ; +x24 : tree ; +x25 : tree ; +x26 : tree ; +x27 : tree ; +x28 : tree ; +x29 : tree ; +x30 : tree ; + +QUERY + +(NOT (((x4 = x4) + AND (NOT is_leaf((LET x81 = null IN (IF is_cons(x81) THEN car(x81) ELSE leaf(zero) ENDIF))))) + AND (NOT (x10 = x2)))); diff --git a/test/regress/regress0/datatypes/typed_v1l80005.cvc b/test/regress/regress0/datatypes/typed_v1l80005.cvc index 9a85f1b88..c4d69dd05 100644 --- a/test/regress/regress0/datatypes/typed_v1l80005.cvc +++ b/test/regress/regress0/datatypes/typed_v1l80005.cvc @@ -1,22 +1,22 @@ -% EXPECT: valid
-% EXIT: 20
-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 ((((((((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))))
- 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))))
- 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))))
- 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)))))
- AND is_node(leaf(zero)))
- AND (NOT (x2 = null)))
- AND (NOT is_zero((LET x76 = node(cons(leaf(succ(zero)),null)) IN (IF is_leaf(x76) THEN data(x76) ELSE zero ENDIF)))))
- 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)))));
+% EXPECT: valid +% EXIT: 20 +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 ((((((((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)))) + 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)))) + 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)))) + 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))))) + AND is_node(leaf(zero))) + AND (NOT (x2 = null))) + AND (NOT is_zero((LET x76 = node(cons(leaf(succ(zero)),null)) IN (IF is_leaf(x76) THEN data(x76) ELSE zero ENDIF))))) + 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))))); diff --git a/test/regress/regress0/datatypes/typed_v2l30079.cvc b/test/regress/regress0/datatypes/typed_v2l30079.cvc index 990cfbb24..4a144c9a5 100644 --- a/test/regress/regress0/datatypes/typed_v2l30079.cvc +++ b/test/regress/regress0/datatypes/typed_v2l30079.cvc @@ -1,20 +1,20 @@ -% 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 : nat ;
-x3 : list ;
-x4 : list ;
-x5 : tree ;
-x6 : tree ;
-
-QUERY
-
-(NOT ((is_node(x6)
- AND (x6 = x5))
- AND (NOT (null = cons(x6,x3)))));
+% 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 : nat ; +x3 : list ; +x4 : list ; +x5 : tree ; +x6 : tree ; + +QUERY + +(NOT ((is_node(x6) + AND (x6 = x5)) + AND (NOT (null = cons(x6,x3))))); diff --git a/test/regress/regress0/datatypes/typed_v3l20092.cvc b/test/regress/regress0/datatypes/typed_v3l20092.cvc index 43dfa3373..204c2d968 100644 --- a/test/regress/regress0/datatypes/typed_v3l20092.cvc +++ b/test/regress/regress0/datatypes/typed_v3l20092.cvc @@ -1,22 +1,22 @@ -% EXPECT: valid
-% EXIT: 20
-DATATYPE
- nat = succ(pred : nat) | zero,
- list = cons(car : tree, cdr : list) | null,
- tree = node(children : list) | leaf(data : nat)
-END;
-
-x1 : nat ;
-x2 : nat ;
-x3 : nat ;
-x4 : list ;
-x5 : list ;
-x6 : list ;
-x7 : tree ;
-x8 : tree ;
-x9 : tree ;
-
-QUERY
-
-(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)))
- 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)))));
+% EXPECT: valid +% EXIT: 20 +DATATYPE + nat = succ(pred : nat) | zero, + list = cons(car : tree, cdr : list) | null, + tree = node(children : list) | leaf(data : nat) +END; + +x1 : nat ; +x2 : nat ; +x3 : nat ; +x4 : list ; +x5 : list ; +x6 : list ; +x7 : tree ; +x8 : tree ; +x9 : tree ; + +QUERY + +(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))) + 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))))); diff --git a/test/regress/regress0/datatypes/typed_v5l30069.cvc b/test/regress/regress0/datatypes/typed_v5l30069.cvc index 662391b90..b03b1a88c 100644 --- a/test/regress/regress0/datatypes/typed_v5l30069.cvc +++ b/test/regress/regress0/datatypes/typed_v5l30069.cvc @@ -1,29 +1,29 @@ -% EXPECT: valid
-% EXIT: 20
-DATATYPE
- nat = succ(pred : nat) | zero,
- list = cons(car : tree, cdr : list) | null,
- tree = node(children : list) | leaf(data : nat)
-END;
-
-x1 : nat ;
-x2 : nat ;
-x3 : nat ;
-x4 : nat ;
-x5 : nat ;
-x6 : list ;
-x7 : list ;
-x8 : list ;
-x9 : list ;
-x10 : list ;
-x11 : tree ;
-x12 : tree ;
-x13 : tree ;
-x14 : tree ;
-x15 : tree ;
-
-QUERY
-
-(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)))
- AND (x15 = node(x6)))
- AND (NOT is_cons(x10))));
+% EXPECT: valid +% EXIT: 20 +DATATYPE + nat = succ(pred : nat) | zero, + list = cons(car : tree, cdr : list) | null, + tree = node(children : list) | leaf(data : nat) +END; + +x1 : nat ; +x2 : nat ; +x3 : nat ; +x4 : nat ; +x5 : nat ; +x6 : list ; +x7 : list ; +x8 : list ; +x9 : list ; +x10 : list ; +x11 : tree ; +x12 : tree ; +x13 : tree ; +x14 : tree ; +x15 : tree ; + +QUERY + +(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))) + AND (x15 = node(x6))) + AND (NOT is_cons(x10)))); diff --git a/test/regress/regress0/datatypes/v10l40099.cvc b/test/regress/regress0/datatypes/v10l40099.cvc index f2cc332f3..3471e8428 100644 --- a/test/regress/regress0/datatypes/v10l40099.cvc +++ b/test/regress/regress0/datatypes/v10l40099.cvc @@ -1,45 +1,45 @@ -% EXPECT: valid
-% EXIT: 20
-DATATYPE
- nat = succ(pred : nat) | zero,
- list = cons(car : tree, cdr : list) | null,
- tree = node(children : list) | leaf(data : nat)
-END;
-
-x1 : nat ;
-x2 : nat ;
-x3 : nat ;
-x4 : nat ;
-x5 : nat ;
-x6 : nat ;
-x7 : nat ;
-x8 : nat ;
-x9 : nat ;
-x10 : nat ;
-x11 : list ;
-x12 : list ;
-x13 : list ;
-x14 : list ;
-x15 : list ;
-x16 : list ;
-x17 : list ;
-x18 : list ;
-x19 : list ;
-x20 : list ;
-x21 : tree ;
-x22 : tree ;
-x23 : tree ;
-x24 : tree ;
-x25 : tree ;
-x26 : tree ;
-x27 : tree ;
-x28 : tree ;
-x29 : tree ;
-x30 : tree ;
-
-QUERY
-
-(NOT ((((NOT is_zero(x3))
- AND (x8 = zero))
- AND (NOT (x25 = x28)))
- AND (NOT is_zero(x8))));
+% EXPECT: valid +% EXIT: 20 +DATATYPE + nat = succ(pred : nat) | zero, + list = cons(car : tree, cdr : list) | null, + tree = node(children : list) | leaf(data : nat) +END; + +x1 : nat ; +x2 : nat ; +x3 : nat ; +x4 : nat ; +x5 : nat ; +x6 : nat ; +x7 : nat ; +x8 : nat ; +x9 : nat ; +x10 : nat ; +x11 : list ; +x12 : list ; +x13 : list ; +x14 : list ; +x15 : list ; +x16 : list ; +x17 : list ; +x18 : list ; +x19 : list ; +x20 : list ; +x21 : tree ; +x22 : tree ; +x23 : tree ; +x24 : tree ; +x25 : tree ; +x26 : tree ; +x27 : tree ; +x28 : tree ; +x29 : tree ; +x30 : tree ; + +QUERY + +(NOT ((((NOT is_zero(x3)) + AND (x8 = zero)) + AND (NOT (x25 = x28))) + AND (NOT is_zero(x8)))); diff --git a/test/regress/regress0/datatypes/v1l20009.cvc b/test/regress/regress0/datatypes/v1l20009.cvc index 9eea247a2..0adba1da7 100644 --- a/test/regress/regress0/datatypes/v1l20009.cvc +++ b/test/regress/regress0/datatypes/v1l20009.cvc @@ -1,16 +1,16 @@ -% EXPECT: valid
-% EXIT: 20
-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 ((NOT is_zero(pred(succ(pred(zero)))))
- AND (data(x3) = succ(pred(data(leaf(succ(data(car(null))))))))));
+% EXPECT: valid +% EXIT: 20 +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 ((NOT is_zero(pred(succ(pred(zero))))) + AND (data(x3) = succ(pred(data(leaf(succ(data(car(null)))))))))); diff --git a/test/regress/regress0/datatypes/v2l40025.cvc b/test/regress/regress0/datatypes/v2l40025.cvc index f78d5b2cf..f3cd83323 100644 --- a/test/regress/regress0/datatypes/v2l40025.cvc +++ b/test/regress/regress0/datatypes/v2l40025.cvc @@ -1,21 +1,21 @@ -% EXPECT: valid
-% EXIT: 20
-DATATYPE
- nat = succ(pred : nat) | zero,
- list = cons(car : tree, cdr : list) | null,
- tree = node(children : list) | leaf(data : nat)
-END;
-
-x1 : nat ;
-x2 : nat ;
-x3 : list ;
-x4 : list ;
-x5 : tree ;
-x6 : tree ;
-
-QUERY
-
-(NOT (((is_leaf(x5)
- AND (NOT (x2 = x1)))
- AND (x2 = pred(pred(zero))))
- AND (NOT is_node(node(null)))));
+% EXPECT: valid +% EXIT: 20 +DATATYPE + nat = succ(pred : nat) | zero, + list = cons(car : tree, cdr : list) | null, + tree = node(children : list) | leaf(data : nat) +END; + +x1 : nat ; +x2 : nat ; +x3 : list ; +x4 : list ; +x5 : tree ; +x6 : tree ; + +QUERY + +(NOT (((is_leaf(x5) + AND (NOT (x2 = x1))) + AND (x2 = pred(pred(zero)))) + AND (NOT is_node(node(null))))); diff --git a/test/regress/regress0/datatypes/v3l60006.cvc b/test/regress/regress0/datatypes/v3l60006.cvc index a681599ee..107c3e1a2 100644 --- a/test/regress/regress0/datatypes/v3l60006.cvc +++ b/test/regress/regress0/datatypes/v3l60006.cvc @@ -1,26 +1,26 @@ -% 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 : nat ;
-x3 : nat ;
-x4 : list ;
-x5 : list ;
-x6 : list ;
-x7 : tree ;
-x8 : tree ;
-x9 : tree ;
-
-QUERY
-
-(NOT ((((((NOT is_succ(pred(data(leaf(x3)))))
- AND (x1 = zero))
- AND (NOT is_zero(succ(succ(zero)))))
- AND (NOT (x3 = x2)))
- AND (x4 = cdr(x5)))
- AND is_cons(cons(x8,x5))));
+% 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 : nat ; +x3 : nat ; +x4 : list ; +x5 : list ; +x6 : list ; +x7 : tree ; +x8 : tree ; +x9 : tree ; + +QUERY + +(NOT ((((((NOT is_succ(pred(data(leaf(x3))))) + AND (x1 = zero)) + AND (NOT is_zero(succ(succ(zero))))) + AND (NOT (x3 = x2))) + AND (x4 = cdr(x5))) + AND is_cons(cons(x8,x5)))); diff --git a/test/regress/regress0/datatypes/v5l30058.cvc b/test/regress/regress0/datatypes/v5l30058.cvc index 4159f6c70..9691cf5c6 100644 --- a/test/regress/regress0/datatypes/v5l30058.cvc +++ b/test/regress/regress0/datatypes/v5l30058.cvc @@ -1,29 +1,29 @@ -% 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 : nat ;
-x3 : nat ;
-x4 : nat ;
-x5 : nat ;
-x6 : list ;
-x7 : list ;
-x8 : list ;
-x9 : list ;
-x10 : list ;
-x11 : tree ;
-x12 : tree ;
-x13 : tree ;
-x14 : tree ;
-x15 : tree ;
-
-QUERY
-
-(NOT (((NOT (node(x9) = car(x8)))
- AND (node(x6) = x11))
- AND (NOT is_node(x15))));
+% 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 : nat ; +x3 : nat ; +x4 : nat ; +x5 : nat ; +x6 : list ; +x7 : list ; +x8 : list ; +x9 : list ; +x10 : list ; +x11 : tree ; +x12 : tree ; +x13 : tree ; +x14 : tree ; +x15 : tree ; + +QUERY + +(NOT (((NOT (node(x9) = car(x8))) + AND (node(x6) = x11)) + AND (NOT is_node(x15)))); diff --git a/test/regress/run_regression b/test/regress/run_regression index 8f2e385d7..28bb5cb42 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -49,7 +49,7 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then if test -e "$benchmark.expect"; then expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` - expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | sed 's,^% EXIT: ,,;s,\r,,'` + expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` command_line=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'` if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" @@ -57,7 +57,7 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` - expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,;s,\r,,'` + expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle # this frustrates our auto-language-detection, so add explicit --lang @@ -83,7 +83,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then if test -e "$benchmark.expect"; then expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` - expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | sed 's,^% EXIT: ,,;s,\r,,'` + expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` command_line=`grep '^% COMMAND-LINE: ' "$benchmark.expect" | sed 's,^% COMMAND-LINE: ,,'` if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" @@ -91,7 +91,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then elif grep -q '^% \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark"; then expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` - expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,;s,\r,,'` + expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` # old mktemp from coreutils 7.x is broken, can't do XXXX in the middle # this frustrates our auto-language-detection, so add explicit --lang @@ -120,8 +120,8 @@ elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then error "cannot determine expected output of \`$benchmark': " \ "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures" fi - expected_output=$(echo "$expected_output" | sed 's,^% EXPECT: ,,;s,\r,,') - expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,;s,\r,,'` + expected_output=$(echo "$expected_output" | perl -pe 's,^% EXPECT: ,,;s,\r,,') + expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" fi diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h index 381d5fdea..6d6b0740b 100644 --- a/test/unit/expr/type_cardinality_public.h +++ b/test/unit/expr/type_cardinality_public.h @@ -5,7 +5,7 @@ ** Major contributors: none ** 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 @@ -70,6 +70,7 @@ public: TS_ASSERT( realToBool.getCardinality() > Cardinality::REALS ); TS_ASSERT( boolToReal.getCardinality() == Cardinality::REALS ); TS_ASSERT( boolToInt.getCardinality() == Cardinality::INTEGERS ); +cout << "boolToBool " << boolToBool.getCardinality() << endl; TS_ASSERT( boolToBool.getCardinality() == 4 ); } |