diff options
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/boolean.cvc | 809 | ||||
-rw-r--r-- | test/regress/regress0/bug1.cvc | 11 | ||||
-rw-r--r-- | test/regress/regress0/hole6.cvc | 182 | ||||
-rw-r--r-- | test/regress/regress0/logops.cvc | 14 | ||||
-rw-r--r-- | test/regress/regress0/queries0.cvc | 11 | ||||
-rw-r--r-- | test/regress/regress0/simple-uf.smt | 7 | ||||
-rw-r--r-- | test/regress/regress0/simple.cvc | 6 | ||||
-rw-r--r-- | test/regress/regress0/simple.smt | 15 | ||||
-rw-r--r-- | test/regress/regress0/simple2.smt | 13 | ||||
-rw-r--r-- | test/regress/regress0/smallcnf.cvc | 9 | ||||
-rw-r--r-- | test/regress/regress0/test11.cvc | 11 | ||||
-rw-r--r-- | test/regress/regress0/test12.cvc | 151 | ||||
-rw-r--r-- | test/regress/regress0/test9.cvc | 7 | ||||
-rw-r--r-- | test/regress/regress0/uf20-03.cvc | 118 | ||||
-rw-r--r-- | test/regress/regress0/wiki.cvc | 38 |
15 files changed, 1402 insertions, 0 deletions
diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc new file mode 100644 index 000000000..ac9885703 --- /dev/null +++ b/test/regress/regress0/boolean.cvc @@ -0,0 +1,809 @@ +%% Regression level = 1 +%% Result = Valid +%% Runtime = 1 +%% Language = presentation +p : BOOLEAN; +q : BOOLEAN; +r : BOOLEAN; +s : BOOLEAN; +t : BOOLEAN; +u : BOOLEAN; +v : BOOLEAN; +P1 : BOOLEAN; +P2 : BOOLEAN; +P3 : BOOLEAN; +P4 : BOOLEAN; +P6 : BOOLEAN; +P5 : BOOLEAN; +a41 : BOOLEAN = + IF p THEN FALSE + ELSE TRUE + ENDIF; +a42 : BOOLEAN = + IF a41 THEN FALSE + ELSE TRUE + ENDIF; +a45 : BOOLEAN = + IF p THEN p + ELSE a41 + ENDIF; +a46 : BOOLEAN = + IF q THEN FALSE + ELSE TRUE + ENDIF; +a49 : BOOLEAN = + IF s THEN t + ELSE FALSE + ENDIF; +a58 : BOOLEAN = + IF q THEN q + ELSE a46 + ENDIF; +a59 : BOOLEAN = + IF r THEN FALSE + ELSE TRUE + ENDIF; +a61 : BOOLEAN = + IF s THEN FALSE + ELSE TRUE + ENDIF; +a62 : BOOLEAN = + IF s THEN s + ELSE a61 + ENDIF; +a65 : BOOLEAN = + IF t THEN FALSE + ELSE TRUE + ENDIF; +a67 : BOOLEAN = + IF u THEN FALSE + ELSE TRUE + ENDIF; +a73 : BOOLEAN = + IF p THEN q + ELSE FALSE + ENDIF; +a74 : BOOLEAN = + IF q THEN p + ELSE FALSE + ENDIF; +a77 : BOOLEAN = + IF r THEN TRUE + ELSE s + ENDIF; +a78 : BOOLEAN = + IF s THEN TRUE + ELSE r + ENDIF; +a81 : BOOLEAN = + IF t THEN u + ELSE a67 + ENDIF; +a82 : BOOLEAN = + IF u THEN t + ELSE a65 + ENDIF; +a88 : BOOLEAN = + IF q THEN r + ELSE FALSE + ENDIF; +a89 : BOOLEAN = + IF p THEN a88 + ELSE FALSE + ENDIF; +a92 : BOOLEAN = + IF s THEN TRUE + ELSE t + ENDIF; +a94 : BOOLEAN = + IF t THEN TRUE + ELSE u + ENDIF; +a95 : BOOLEAN = + IF s THEN TRUE + ELSE a94 + ENDIF; +a105 : BOOLEAN = + IF t THEN u + ELSE FALSE + ENDIF; +a111 : BOOLEAN = + IF p THEN q + ELSE TRUE + ENDIF; +a112 : BOOLEAN = + IF q THEN r + ELSE TRUE + ENDIF; +a114 : BOOLEAN = + IF p THEN r + ELSE TRUE + ENDIF; +a116 : BOOLEAN = + IF s THEN t + ELSE a65 + ENDIF; +a121 : BOOLEAN = + IF a46 THEN a41 + ELSE TRUE + ENDIF; +a126 : BOOLEAN = + IF a59 THEN a61 + ELSE + IF a61 THEN FALSE + ELSE TRUE + ENDIF + ENDIF; +a130 : BOOLEAN = + IF q THEN TRUE + ELSE r + ENDIF; +a132 : BOOLEAN = + IF p THEN r + ELSE FALSE + ENDIF; +a133 : BOOLEAN = + IF a73 THEN TRUE + ELSE a132 + ENDIF; +a138 : BOOLEAN = + IF a92 THEN + IF s THEN TRUE + ELSE u + ENDIF + ELSE FALSE + ENDIF; +a143 : BOOLEAN = + IF a114 THEN a112 + ELSE FALSE + ENDIF; +a145 : BOOLEAN = + IF + IF + IF p THEN TRUE + ELSE q + ENDIF THEN r + ELSE TRUE + ENDIF THEN a143 + ELSE + IF a143 THEN FALSE + ELSE TRUE + ENDIF + ENDIF; +a147 : BOOLEAN = + IF s THEN t + ELSE TRUE + ENDIF; +a148 : BOOLEAN = + IF s THEN u + ELSE TRUE + ENDIF; +a149 : BOOLEAN = + IF a147 THEN TRUE + ELSE a148 + ENDIF; +a153 : BOOLEAN = + IF a73 THEN r + ELSE TRUE + ENDIF; +a154 : BOOLEAN = + IF a114 THEN TRUE + ELSE a112 + ENDIF; +a158 : BOOLEAN = + IF a147 THEN a148 + ELSE FALSE + ENDIF; +a162 : BOOLEAN = + IF p THEN a112 + ELSE TRUE + ENDIF; +a167 : BOOLEAN = + IF a46 THEN TRUE + ELSE a59 + ENDIF; +a171 : BOOLEAN = + IF a61 THEN a65 + ELSE FALSE + ENDIF; +a176 : BOOLEAN = + IF p THEN q + ELSE r + ENDIF; +a178 : BOOLEAN = + IF p THEN a46 + ELSE a59 + ENDIF; +a183 : BOOLEAN = + IF s THEN a65 + ELSE + IF a65 THEN FALSE + ELSE TRUE + ENDIF + ENDIF; +a187 : BOOLEAN = + IF a41 THEN TRUE + ELSE q + ENDIF; +a192 : BOOLEAN = + IF + IF r THEN s + ELSE FALSE + ENDIF THEN TRUE + ELSE + IF a59 THEN t + ELSE FALSE + ENDIF + ENDIF; +a197 : BOOLEAN = + IF a111 THEN + IF a41 THEN r + ELSE TRUE + ENDIF + ELSE FALSE + ENDIF; +a200 : BOOLEAN = + IF a49 THEN TRUE + ELSE a171 + ENDIF; +a204 : BOOLEAN = + IF p THEN q + ELSE a46 + ENDIF; +a205 : BOOLEAN = + IF q THEN p + ELSE TRUE + ENDIF; +a206 : BOOLEAN = + IF a111 THEN a205 + ELSE FALSE + ENDIF; +a210 : BOOLEAN = + IF p THEN a46 + ELSE TRUE + ENDIF; +a214 : BOOLEAN = + IF a73 THEN FALSE + ELSE TRUE + ENDIF; +a221 : BOOLEAN = + IF + IF p THEN a46 + ELSE FALSE + ENDIF THEN r + ELSE TRUE + ENDIF; +a225 : BOOLEAN = + IF a187 THEN a132 + ELSE TRUE + ENDIF; +a228 : BOOLEAN = + IF q THEN r + ELSE a59 + ENDIF; +a231 : BOOLEAN = + IF a204 THEN r + ELSE a59 + ENDIF; +a237 : BOOLEAN = + IF q THEN a132 + ELSE + IF a41 THEN s + ELSE FALSE + ENDIF + ENDIF; +a288 : BOOLEAN = + IF + IF + IF p THEN a41 + ELSE a42 + ENDIF THEN FALSE + ELSE TRUE + ENDIF THEN + IF + IF a45 THEN + IF + IF q THEN TRUE + ELSE a46 + ENDIF THEN + IF + IF r THEN r + ELSE TRUE + ENDIF THEN + IF + IF a49 THEN s + ELSE TRUE + ENDIF THEN + IF u THEN + IF u THEN TRUE + ELSE v + ENDIF + ELSE TRUE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF a58 THEN + IF + IF r THEN r + ELSE a59 + ENDIF THEN a62 + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF a45 THEN + IF a62 THEN + IF + IF t THEN t + ELSE a65 + ENDIF THEN + IF a67 THEN a67 + ELSE + IF a67 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF a73 THEN a74 + ELSE + IF a74 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF a77 THEN a78 + ELSE + IF a78 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF a81 THEN a82 + ELSE + IF a82 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF + IF a73 THEN r + ELSE FALSE + ENDIF THEN a89 + ELSE + IF a89 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF a92 THEN TRUE + ELSE u + ENDIF THEN a95 + ELSE + IF a95 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF + IF p THEN p + ELSE FALSE + ENDIF THEN p + ELSE a41 + ENDIF THEN + IF + IF + IF q THEN TRUE + ELSE q + ENDIF THEN q + ELSE a46 + ENDIF THEN + IF + IF + IF r THEN a77 + ELSE FALSE + ENDIF THEN r + ELSE a59 + ENDIF THEN + IF + IF t THEN TRUE + ELSE a105 + ENDIF THEN t + ELSE a65 + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF THEN + IF a58 THEN + IF + IF + IF + IF a111 THEN a112 + ELSE FALSE + ENDIF THEN a114 + ELSE TRUE + ENDIF THEN + IF + IF a116 THEN a81 + ELSE FALSE + ENDIF THEN + IF s THEN u + ELSE a67 + ENDIF + ELSE TRUE + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF a111 THEN a121 + ELSE + IF a121 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF r THEN s + ELSE a61 + ENDIF THEN a126 + ELSE + IF a126 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF + IF p THEN a130 + ELSE FALSE + ENDIF THEN a133 + ELSE + IF a133 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF s THEN TRUE + ELSE a105 + ENDIF THEN a138 + ELSE + IF a138 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF a145 THEN + IF + IF s THEN a94 + ELSE TRUE + ENDIF THEN a149 + ELSE + IF a149 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF a153 THEN a154 + ELSE + IF a154 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF s THEN a105 + ELSE TRUE + ENDIF THEN a158 + ELSE + IF a158 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF a153 THEN a162 + ELSE + IF a162 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF + IF a42 THEN p + ELSE a41 + ENDIF THEN + IF + IF + IF a88 THEN FALSE + ELSE TRUE + ENDIF THEN a167 + ELSE + IF a167 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF a92 THEN FALSE + ELSE TRUE + ENDIF THEN a171 + ELSE + IF a171 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF + IF a176 THEN FALSE + ELSE TRUE + ENDIF THEN a178 + ELSE + IF a178 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF a116 THEN FALSE + ELSE TRUE + ENDIF THEN a183 + ELSE + IF a183 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF a111 THEN a187 + ELSE + IF a187 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF r THEN s + ELSE t + ENDIF THEN a192 + ELSE + IF a192 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF + IF a176 THEN a197 + ELSE + IF a197 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF a116 THEN a200 + ELSE + IF a200 THEN FALSE + ELSE TRUE + ENDIF + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF a204 THEN a206 + ELSE + IF a206 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF a111 THEN TRUE + ELSE a205 + ENDIF THEN + IF + IF a46 THEN TRUE + ELSE + IF + IF a210 THEN p + ELSE FALSE + ENDIF THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF a210 THEN a214 + ELSE + IF a214 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF a145 THEN + IF + IF a162 THEN a153 + ELSE + IF a153 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF + IF p THEN a130 + ELSE TRUE + ENDIF THEN a221 + ELSE + IF a221 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF + IF p THEN a112 + ELSE FALSE + ENDIF THEN a225 + ELSE + IF a225 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF + IF p THEN a228 + ELSE + IF a228 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN a231 + ELSE + IF a231 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF + IF p THEN a88 + ELSE + IF a46 THEN s + ELSE FALSE + ENDIF + ENDIF THEN a237 + ELSE + IF a237 THEN FALSE + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF + IF P1 THEN + IF P2 THEN TRUE + ELSE P3 + ENDIF + ELSE + IF P3 THEN TRUE + ELSE P4 + ENDIF + ENDIF THEN + IF + IF P3 THEN + IF P6 THEN FALSE + ELSE TRUE + ENDIF + ELSE + IF P4 THEN P1 + ELSE TRUE + ENDIF + ENDIF THEN + IF + IF + IF P2 THEN P5 + ELSE FALSE + ENDIF THEN FALSE + ELSE TRUE + ENDIF THEN + IF P2 THEN P5 + ELSE TRUE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF THEN + IF + IF P3 THEN P6 + ELSE TRUE + ENDIF THEN FALSE + ELSE TRUE + ENDIF + ELSE TRUE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF + ELSE FALSE + ENDIF; +QUERY a288; diff --git a/test/regress/regress0/bug1.cvc b/test/regress/regress0/bug1.cvc new file mode 100644 index 000000000..d2c24a438 --- /dev/null +++ b/test/regress/regress0/bug1.cvc @@ -0,0 +1,11 @@ +%% Regression level = 0 +%% Result = Valid +%% Runtime = 1 +%% Language = presentation +x : REAL; +y : REAL; +f : REAL -> REAL; +ASSERT ((x > y) => f(x) > f (y)); +ASSERT (x = 3); +ASSERT (y = 2); +QUERY(f(x) > f (y)); diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc new file mode 100644 index 000000000..28738fc24 --- /dev/null +++ b/test/regress/regress0/hole6.cvc @@ -0,0 +1,182 @@ +%% Regression level = 0 +%% Result = Valid +%% Runtime = 1 +%% Language = presentation +x_1 : BOOLEAN; +x_2 : BOOLEAN; +x_3 : BOOLEAN; +x_4 : BOOLEAN; +x_5 : BOOLEAN; +x_6 : BOOLEAN; +x_7 : BOOLEAN; +x_8 : BOOLEAN; +x_9 : BOOLEAN; +x_10 : BOOLEAN; +x_11 : BOOLEAN; +x_12 : BOOLEAN; +x_13 : BOOLEAN; +x_14 : BOOLEAN; +x_15 : BOOLEAN; +x_16 : BOOLEAN; +x_17 : BOOLEAN; +x_18 : BOOLEAN; +x_19 : BOOLEAN; +x_20 : BOOLEAN; +x_21 : BOOLEAN; +x_22 : BOOLEAN; +x_23 : BOOLEAN; +x_24 : BOOLEAN; +x_25 : BOOLEAN; +x_26 : BOOLEAN; +x_27 : BOOLEAN; +x_28 : BOOLEAN; +x_29 : BOOLEAN; +x_30 : BOOLEAN; +x_31 : BOOLEAN; +x_32 : BOOLEAN; +x_33 : BOOLEAN; +x_34 : BOOLEAN; +x_35 : BOOLEAN; +x_36 : BOOLEAN; +x_37 : BOOLEAN; +x_38 : BOOLEAN; +x_39 : BOOLEAN; +x_40 : BOOLEAN; +x_41 : BOOLEAN; +x_42 : BOOLEAN; +ASSERT NOT x_1 OR NOT x_7; +ASSERT NOT x_1 OR NOT x_13; +ASSERT NOT x_1 OR NOT x_19; +ASSERT NOT x_1 OR NOT x_25; +ASSERT NOT x_1 OR NOT x_31; +ASSERT NOT x_1 OR NOT x_37; +ASSERT NOT x_7 OR NOT x_13; +ASSERT NOT x_7 OR NOT x_19; +ASSERT NOT x_7 OR NOT x_25; +ASSERT NOT x_7 OR NOT x_31; +ASSERT NOT x_7 OR NOT x_37; +ASSERT NOT x_13 OR NOT x_19; +ASSERT NOT x_13 OR NOT x_25; +ASSERT NOT x_13 OR NOT x_31; +ASSERT NOT x_13 OR NOT x_37; +ASSERT NOT x_19 OR NOT x_25; +ASSERT NOT x_19 OR NOT x_31; +ASSERT NOT x_19 OR NOT x_37; +ASSERT NOT x_25 OR NOT x_31; +ASSERT NOT x_25 OR NOT x_37; +ASSERT NOT x_31 OR NOT x_37; +ASSERT NOT x_2 OR NOT x_8; +ASSERT NOT x_2 OR NOT x_14; +ASSERT NOT x_2 OR NOT x_20; +ASSERT NOT x_2 OR NOT x_26; +ASSERT NOT x_2 OR NOT x_32; +ASSERT NOT x_2 OR NOT x_38; +ASSERT NOT x_8 OR NOT x_14; +ASSERT NOT x_8 OR NOT x_20; +ASSERT NOT x_8 OR NOT x_26; +ASSERT NOT x_8 OR NOT x_32; +ASSERT NOT x_8 OR NOT x_38; +ASSERT NOT x_14 OR NOT x_20; +ASSERT NOT x_14 OR NOT x_26; +ASSERT NOT x_14 OR NOT x_32; +ASSERT NOT x_14 OR NOT x_38; +ASSERT NOT x_20 OR NOT x_26; +ASSERT NOT x_20 OR NOT x_32; +ASSERT NOT x_20 OR NOT x_38; +ASSERT NOT x_26 OR NOT x_32; +ASSERT NOT x_26 OR NOT x_38; +ASSERT NOT x_32 OR NOT x_38; +ASSERT NOT x_3 OR NOT x_9; +ASSERT NOT x_3 OR NOT x_15; +ASSERT NOT x_3 OR NOT x_21; +ASSERT NOT x_3 OR NOT x_27; +ASSERT NOT x_3 OR NOT x_33; +ASSERT NOT x_3 OR NOT x_39; +ASSERT NOT x_9 OR NOT x_15; +ASSERT NOT x_9 OR NOT x_21; +ASSERT NOT x_9 OR NOT x_27; +ASSERT NOT x_9 OR NOT x_33; +ASSERT NOT x_9 OR NOT x_39; +ASSERT NOT x_15 OR NOT x_21; +ASSERT NOT x_15 OR NOT x_27; +ASSERT NOT x_15 OR NOT x_33; +ASSERT NOT x_15 OR NOT x_39; +ASSERT NOT x_21 OR NOT x_27; +ASSERT NOT x_21 OR NOT x_33; +ASSERT NOT x_21 OR NOT x_39; +ASSERT NOT x_27 OR NOT x_33; +ASSERT NOT x_27 OR NOT x_39; +ASSERT NOT x_33 OR NOT x_39; +ASSERT NOT x_4 OR NOT x_10; +ASSERT NOT x_4 OR NOT x_16; +ASSERT NOT x_4 OR NOT x_22; +ASSERT NOT x_4 OR NOT x_28; +ASSERT NOT x_4 OR NOT x_34; +ASSERT NOT x_4 OR NOT x_40; +ASSERT NOT x_10 OR NOT x_16; +ASSERT NOT x_10 OR NOT x_22; +ASSERT NOT x_10 OR NOT x_28; +ASSERT NOT x_10 OR NOT x_34; +ASSERT NOT x_10 OR NOT x_40; +ASSERT NOT x_16 OR NOT x_22; +ASSERT NOT x_16 OR NOT x_28; +ASSERT NOT x_16 OR NOT x_34; +ASSERT NOT x_16 OR NOT x_40; +ASSERT NOT x_22 OR NOT x_28; +ASSERT NOT x_22 OR NOT x_34; +ASSERT NOT x_22 OR NOT x_40; +ASSERT NOT x_28 OR NOT x_34; +ASSERT NOT x_28 OR NOT x_40; +ASSERT NOT x_34 OR NOT x_40; +ASSERT NOT x_5 OR NOT x_11; +ASSERT NOT x_5 OR NOT x_17; +ASSERT NOT x_5 OR NOT x_23; +ASSERT NOT x_5 OR NOT x_29; +ASSERT NOT x_5 OR NOT x_35; +ASSERT NOT x_5 OR NOT x_41; +ASSERT NOT x_11 OR NOT x_17; +ASSERT NOT x_11 OR NOT x_23; +ASSERT NOT x_11 OR NOT x_29; +ASSERT NOT x_11 OR NOT x_35; +ASSERT NOT x_11 OR NOT x_41; +ASSERT NOT x_17 OR NOT x_23; +ASSERT NOT x_17 OR NOT x_29; +ASSERT NOT x_17 OR NOT x_35; +ASSERT NOT x_17 OR NOT x_41; +ASSERT NOT x_23 OR NOT x_29; +ASSERT NOT x_23 OR NOT x_35; +ASSERT NOT x_23 OR NOT x_41; +ASSERT NOT x_29 OR NOT x_35; +ASSERT NOT x_29 OR NOT x_41; +ASSERT NOT x_35 OR NOT x_41; +ASSERT NOT x_6 OR NOT x_12; +ASSERT NOT x_6 OR NOT x_18; +ASSERT NOT x_6 OR NOT x_24; +ASSERT NOT x_6 OR NOT x_30; +ASSERT NOT x_6 OR NOT x_36; +ASSERT NOT x_6 OR NOT x_42; +ASSERT NOT x_12 OR NOT x_18; +ASSERT NOT x_12 OR NOT x_24; +ASSERT NOT x_12 OR NOT x_30; +ASSERT NOT x_12 OR NOT x_36; +ASSERT NOT x_12 OR NOT x_42; +ASSERT NOT x_18 OR NOT x_24; +ASSERT NOT x_18 OR NOT x_30; +ASSERT NOT x_18 OR NOT x_36; +ASSERT NOT x_18 OR NOT x_42; +ASSERT NOT x_24 OR NOT x_30; +ASSERT NOT x_24 OR NOT x_36; +ASSERT NOT x_24 OR NOT x_42; +ASSERT NOT x_30 OR NOT x_36; +ASSERT NOT x_30 OR NOT x_42; +ASSERT NOT x_36 OR NOT x_42; +ASSERT x_6 OR x_5 OR x_4 OR x_3 OR x_2 OR x_1; +ASSERT x_12 OR x_11 OR x_10 OR x_9 OR x_8 OR x_7; +ASSERT x_18 OR x_17 OR x_16 OR x_15 OR x_14 OR x_13; +ASSERT x_24 OR x_23 OR x_22 OR x_21 OR x_20 OR x_19; +ASSERT x_30 OR x_29 OR x_28 OR x_27 OR x_26 OR x_25; +ASSERT x_36 OR x_35 OR x_34 OR x_33 OR x_32 OR x_31; +ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37; + + +QUERY FALSE; diff --git a/test/regress/regress0/logops.cvc b/test/regress/regress0/logops.cvc new file mode 100644 index 000000000..0cb00599d --- /dev/null +++ b/test/regress/regress0/logops.cvc @@ -0,0 +1,14 @@ + + +a, b, c: BOOLEAN; + +QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a); + +QUERY NOT c AND b; + +QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b)); + +QUERY (a => b) <=> (NOT a OR b); + +QUERY TRUE XOR FALSE; + diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/queries0.cvc new file mode 100644 index 000000000..8f7ceedd5 --- /dev/null +++ b/test/regress/regress0/queries0.cvc @@ -0,0 +1,11 @@ + +% Tests the invariants for multiple queries. + +a, b: BOOLEAN; + +%Valid query +QUERY (a AND b) OR NOT (a AND b); + +%Invalid query +QUERY (a OR b); + diff --git a/test/regress/regress0/simple-uf.smt b/test/regress/regress0/simple-uf.smt new file mode 100644 index 000000000..3aaba2ab0 --- /dev/null +++ b/test/regress/regress0/simple-uf.smt @@ -0,0 +1,7 @@ +(benchmark simple_uf + :logic QF_UF + :extrasorts (A B) + :extrafuns ((f A B) (x A) (y A)) + :formula (not (implies (= x y) (= (f x) (f y)))) + :status unsat +) diff --git a/test/regress/regress0/simple.cvc b/test/regress/regress0/simple.cvc new file mode 100644 index 000000000..3566053d9 --- /dev/null +++ b/test/regress/regress0/simple.cvc @@ -0,0 +1,6 @@ +x0, x1, x2, x3 : BOOLEAN; +ASSERT x1 OR NOT x0; +ASSERT x0 OR NOT x3; +ASSERT x3 OR x2; +ASSERT x1 AND NOT x1; +QUERY x2; diff --git a/test/regress/regress0/simple.smt b/test/regress/regress0/simple.smt new file mode 100644 index 000000000..56aa82d72 --- /dev/null +++ b/test/regress/regress0/simple.smt @@ -0,0 +1,15 @@ +(benchmark b +:status unknown +:logic QF_UF +:extrapreds ((x0)) +:extrapreds ((x1)) +:extrapreds ((x2)) +:extrapreds ((x3)) +:formula +(and (or x1 (not x0)) + (or x0 (not x3)) + (or x3 x2) + (not x1) + x2 + x3) +) diff --git a/test/regress/regress0/simple2.smt b/test/regress/regress0/simple2.smt new file mode 100644 index 000000000..e917d1b64 --- /dev/null +++ b/test/regress/regress0/simple2.smt @@ -0,0 +1,13 @@ +(benchmark b +:status unknown +:logic QF_UF +:extrapreds ((x0)) +:extrapreds ((x1)) +:extrapreds ((x2)) +:extrapreds ((x3)) +:formula +(and (or x1 (not x0)) + (or x0 (not x3)) + (or x3 x2) + (not x1)) +) diff --git a/test/regress/regress0/smallcnf.cvc b/test/regress/regress0/smallcnf.cvc new file mode 100644 index 000000000..3ad6f124a --- /dev/null +++ b/test/regress/regress0/smallcnf.cvc @@ -0,0 +1,9 @@ + +a, b, c : BOOLEAN; + +ASSERT NOT a OR NOT b; +ASSERT c OR b OR a; +ASSERT b OR NOT a; +ASSERT a OR NOT b OR c; +QUERY FALSE; + diff --git a/test/regress/regress0/test11.cvc b/test/regress/regress0/test11.cvc new file mode 100644 index 000000000..ff0880b2a --- /dev/null +++ b/test/regress/regress0/test11.cvc @@ -0,0 +1,11 @@ +%% Regression level = 0 +%% Result = Valid +%% Runtime = 1 +%% Language = presentation + +x, y : BOOLEAN; + +ASSERT (x OR y); +ASSERT NOT (x OR y); + +QUERY FALSE; diff --git a/test/regress/regress0/test12.cvc b/test/regress/regress0/test12.cvc new file mode 100644 index 000000000..31ec0864e --- /dev/null +++ b/test/regress/regress0/test12.cvc @@ -0,0 +1,151 @@ +%% Regression level = 1 +%% Result = Valid +%% Runtime = 1 +%% Language = presentation +A: TYPE; +P_1: BOOLEAN; +P_2: BOOLEAN; +P_3: BOOLEAN; +ASSERT (NOT P_1 OR P_2 OR P_2); +ASSERT (NOT P_1 OR P_2 OR P_3); +P_4: BOOLEAN; +P_5: BOOLEAN; +ASSERT (NOT P_1 OR NOT P_4 OR P_2); +ASSERT (NOT P_1 OR NOT P_5 OR P_2); +P_6: BOOLEAN; +P_7: BOOLEAN; +ASSERT (NOT P_2 OR P_6 OR P_1); +ASSERT (NOT P_2 OR P_7 OR P_1); +P_8: BOOLEAN; +P_9: BOOLEAN; +ASSERT (NOT P_2 OR NOT P_8 OR P_1); +ASSERT (NOT P_2 OR NOT P_9 OR P_1); +P_10: BOOLEAN; +ASSERT (P_2 OR P_1 OR P_4); +ASSERT (P_2 OR P_1 OR P_10); +ASSERT (NOT P_2 OR NOT P_1 OR P_4); +ASSERT (NOT P_2 OR NOT P_1 OR P_10); +P_11: BOOLEAN; +ASSERT (NOT P_6 OR P_2 OR P_1); +ASSERT (NOT P_11 OR P_2 OR P_1); +ASSERT (NOT P_6 OR NOT P_2 OR NOT P_1); +ASSERT (NOT P_11 OR NOT P_2 OR NOT P_1); +PUSH; +QUERY (NOT P_2 OR NOT P_3); +POP; +PUSH; +QUERY (P_1 OR NOT P_3); +POP; +PUSH; +QUERY (NOT P_2 OR P_1); +POP; +PUSH; +QUERY (P_5 OR NOT P_2); +POP; +PUSH; +QUERY (P_1 OR NOT P_2); +POP; +PUSH; +QUERY (P_5 OR P_1); +POP; +PUSH; +QUERY (NOT P_7 OR NOT P_1); +POP; +PUSH; +QUERY (P_2 OR NOT P_1); +POP; +PUSH; +QUERY P_2; +POP; +PUSH; +QUERY (P_9 OR NOT P_1); +POP; +PUSH; +QUERY (P_2 OR NOT P_1); +POP; +PUSH; +QUERY P_2; +POP; +PUSH; +QUERY (NOT P_1 OR NOT P_10); +POP; +PUSH; +QUERY (NOT P_2 OR NOT P_10); +POP; +PUSH; +QUERY (NOT P_1 OR NOT P_2); +POP; +PUSH; +QUERY (P_1 OR NOT P_10); +POP; +PUSH; +QUERY (P_2 OR NOT P_10); +POP; +PUSH; +QUERY (P_1 OR P_2); +POP; +PUSH; +QUERY (NOT P_2 OR NOT P_1); +POP; +PUSH; +QUERY (P_11 OR NOT P_1); +POP; +PUSH; +QUERY (NOT P_2 OR P_11); +POP; +PUSH; +QUERY (P_2 OR P_1); +POP; +PUSH; +QUERY (P_11 OR P_1); +POP; +PUSH; +QUERY (P_2 OR P_11); +POP; +P_12: BOOLEAN; +ASSERT (NOT P_12 OR P_2); +ASSERT (NOT P_12 OR P_3); +ASSERT (P_12 OR NOT P_1 OR P_2); +ASSERT (P_12 OR NOT P_1 OR P_2); +P_13: BOOLEAN; +ASSERT (NOT P_13 OR NOT P_4); +ASSERT (NOT P_13 OR NOT P_5); +ASSERT (P_13 OR NOT P_1 OR P_2); +ASSERT (P_13 OR NOT P_1 OR P_2); +ASSERT (NOT P_2 OR P_1); +ASSERT (NOT P_2 OR P_1); +ASSERT (NOT P_2 OR P_1); +ASSERT (NOT P_2 OR P_1); +P_14: BOOLEAN; +ASSERT (P_14 OR P_2 OR P_1); +ASSERT (P_14 OR P_2 OR P_1); +ASSERT (NOT P_14 OR P_4); +ASSERT (NOT P_14 OR P_10); +ASSERT (P_14 OR NOT P_2 OR NOT P_1); +ASSERT (P_14 OR NOT P_2 OR NOT P_1); +P_15: BOOLEAN; +ASSERT (P_15 OR P_2 OR P_1); +ASSERT (P_15 OR P_2 OR P_1); +ASSERT (NOT P_15 OR NOT P_6); +ASSERT (NOT P_15 OR NOT P_11); +ASSERT (P_15 OR NOT P_2 OR NOT P_1); +ASSERT (P_15 OR NOT P_2 OR NOT P_1); +PUSH; +QUERY NOT P_3; +POP; +PUSH; +QUERY P_12; +POP; +PUSH; +QUERY P_11; +POP; +PUSH; +QUERY P_15; +POP; +ASSERT NOT P_15; +ASSERT NOT P_15; +PUSH; +QUERY NOT P_10; +POP; +PUSH; +QUERY FALSE; diff --git a/test/regress/regress0/test9.cvc b/test/regress/regress0/test9.cvc new file mode 100644 index 000000000..eabbc9774 --- /dev/null +++ b/test/regress/regress0/test9.cvc @@ -0,0 +1,7 @@ +%% Regression level = 0 +%% Result = Valid +%% Runtime = 1 +%% Language = presentation +P,Q:BOOLEAN; +ASSERT (P OR Q); +QUERY (P OR Q); diff --git a/test/regress/regress0/uf20-03.cvc b/test/regress/regress0/uf20-03.cvc new file mode 100644 index 000000000..5e7b22b64 --- /dev/null +++ b/test/regress/regress0/uf20-03.cvc @@ -0,0 +1,118 @@ +%% Regression level = 0 +%% Result = Invalid +%% Runtime = 1 +%% Language = presentation +x_1 : BOOLEAN; +x_2 : BOOLEAN; +x_3 : BOOLEAN; +x_4 : BOOLEAN; +x_5 : BOOLEAN; +x_6 : BOOLEAN; +x_7 : BOOLEAN; +x_8 : BOOLEAN; +x_9 : BOOLEAN; +x_10 : BOOLEAN; +x_11 : BOOLEAN; +x_12 : BOOLEAN; +x_13 : BOOLEAN; +x_14 : BOOLEAN; +x_15 : BOOLEAN; +x_16 : BOOLEAN; +x_17 : BOOLEAN; +x_18 : BOOLEAN; +x_19 : BOOLEAN; +x_20 : BOOLEAN; +ASSERT NOT x_9 OR x_3 OR NOT x_15; +ASSERT NOT x_12 OR NOT x_4 OR NOT x_15; +ASSERT x_6 OR x_14 OR NOT x_17; +ASSERT x_10 OR x_16 OR x_11; +ASSERT NOT x_15 OR x_20 OR NOT x_7; +ASSERT NOT x_1 OR x_10 OR x_16; +ASSERT x_13 OR x_17 OR NOT x_7; +ASSERT NOT x_2 OR NOT x_14 OR NOT x_13; +ASSERT x_13 OR NOT x_6 OR x_15; +ASSERT NOT x_9 OR x_3 OR x_16; +ASSERT NOT x_20 OR NOT x_13 OR x_4; +ASSERT NOT x_7 OR x_15 OR NOT x_14; +ASSERT NOT x_15 OR NOT x_16 OR x_6; +ASSERT x_5 OR NOT x_18 OR x_20; +ASSERT NOT x_16 OR NOT x_19 OR x_7; +ASSERT x_20 OR NOT x_18 OR NOT x_2; +ASSERT x_10 OR NOT x_19 OR NOT x_14; +ASSERT x_16 OR NOT x_7 OR x_12; +ASSERT x_6 OR NOT x_5 OR NOT x_1; +ASSERT NOT x_9 OR x_11 OR x_15; +ASSERT x_19 OR NOT x_6 OR x_7; +ASSERT NOT x_11 OR x_17 OR NOT x_19; +ASSERT x_9 OR NOT x_16 OR x_6; +ASSERT x_15 OR NOT x_20 OR x_10; +ASSERT x_9 OR NOT x_1 OR NOT x_11; +ASSERT NOT x_8 OR NOT x_19 OR x_5; +ASSERT NOT x_19 OR x_11 OR x_20; +ASSERT NOT x_12 OR x_13 OR NOT x_3; +ASSERT NOT x_7 OR NOT x_17 OR NOT x_19; +ASSERT x_17 OR x_6 OR NOT x_11; +ASSERT NOT x_7 OR NOT x_17 OR x_10; +ASSERT NOT x_14 OR x_9 OR x_20; +ASSERT x_1 OR NOT x_18 OR NOT x_16; +ASSERT NOT x_2 OR NOT x_15 OR x_20; +ASSERT x_14 OR x_18 OR NOT x_1; +ASSERT NOT x_8 OR NOT x_4 OR x_1; +ASSERT x_13 OR x_3 OR NOT x_9; +ASSERT x_5 OR x_7 OR x_8; +ASSERT x_9 OR x_4 OR NOT x_20; +ASSERT NOT x_18 OR NOT x_15 OR NOT x_10; +ASSERT x_10 OR x_3 OR NOT x_20; +ASSERT x_20 OR NOT x_14 OR x_16; +ASSERT x_20 OR NOT x_3 OR NOT x_11; +ASSERT NOT x_12 OR x_19 OR NOT x_16; +ASSERT NOT x_3 OR x_5 OR x_10; +ASSERT x_8 OR x_13 OR NOT x_7; +ASSERT NOT x_2 OR NOT x_15 OR x_10; +ASSERT NOT x_3 OR x_9 OR x_16; +ASSERT NOT x_12 OR NOT x_16 OR NOT x_18; +ASSERT x_3 OR x_1 OR NOT x_12; +ASSERT NOT x_18 OR x_13 OR x_5; +ASSERT x_1 OR x_3 OR NOT x_19; +ASSERT NOT x_19 OR NOT x_5 OR x_6; +ASSERT NOT x_20 OR x_8 OR NOT x_2; +ASSERT x_17 OR NOT x_8 OR NOT x_13; +ASSERT x_7 OR NOT x_11 OR NOT x_12; +ASSERT NOT x_10 OR NOT x_14 OR NOT x_20; +ASSERT NOT x_1 OR x_16 OR NOT x_12; +ASSERT x_5 OR NOT x_3 OR x_9; +ASSERT NOT x_18 OR x_8 OR x_14; +ASSERT x_1 OR x_16 OR x_12; +ASSERT x_20 OR NOT x_1 OR NOT x_16; +ASSERT x_5 OR x_10 OR NOT x_13; +ASSERT x_9 OR NOT x_10 OR x_6; +ASSERT NOT x_12 OR x_10 OR NOT x_14; +ASSERT NOT x_13 OR x_1 OR x_4; +ASSERT NOT x_20 OR NOT x_7 OR x_3; +ASSERT x_12 OR x_1 OR NOT x_10; +ASSERT NOT x_1 OR NOT x_16 OR x_7; +ASSERT x_11 OR NOT x_6 OR NOT x_4; +ASSERT x_1 OR x_16 OR NOT x_20; +ASSERT x_9 OR x_7 OR x_15; +ASSERT NOT x_6 OR x_17 OR x_10; +ASSERT x_8 OR x_9 OR x_17; +ASSERT x_18 OR x_11 OR x_10; +ASSERT x_7 OR x_1 OR NOT x_8; +ASSERT NOT x_5 OR NOT x_12 OR x_18; +ASSERT NOT x_6 OR x_2 OR x_15; +ASSERT x_2 OR x_18 OR x_1; +ASSERT NOT x_7 OR NOT x_13 OR x_16; +ASSERT x_18 OR x_19 OR x_9; +ASSERT x_9 OR NOT x_14 OR x_18; +ASSERT x_14 OR x_12 OR NOT x_5; +ASSERT NOT x_13 OR NOT x_7 OR NOT x_14; +ASSERT NOT x_1 OR x_8 OR NOT x_16; +ASSERT NOT x_11 OR x_4 OR x_7; +ASSERT NOT x_4 OR x_20 OR x_5; +ASSERT NOT x_5 OR x_2 OR x_12; +ASSERT NOT x_5 OR x_13 OR NOT x_18; +ASSERT NOT x_18 OR x_9 OR x_1; +ASSERT x_10 OR NOT x_11 OR x_16; + + +QUERY FALSE; diff --git a/test/regress/regress0/wiki.cvc b/test/regress/regress0/wiki.cvc new file mode 100644 index 000000000..ab888039e --- /dev/null +++ b/test/regress/regress0/wiki.cvc @@ -0,0 +1,38 @@ + + +a, b, c : BOOLEAN; + +QUERY a OR (b OR c) <=> (a OR b) OR c; +QUERY a AND (b AND c) <=> (a AND b) AND c; + +QUERY a OR b <=> b OR a; +QUERY a AND b <=> b AND a; + +QUERY a OR (a AND b) <=> a; +QUERY a AND (a OR b) <=> a; + +QUERY a OR (b AND c) <=> (a OR b) AND (a OR c); +QUERY a AND (b OR c) <=> (a AND b) OR (a AND c); + +QUERY a OR NOT a; +QUERY a AND NOT a <=> FALSE; + +QUERY a OR a <=> a; +QUERY a AND a <=> a; + + +QUERY a OR FALSE <=> a; +QUERY a AND TRUE <=> a; + +QUERY a OR TRUE <=> TRUE; +QUERY a AND FALSE <=> FALSE; + +QUERY NOT FALSE <=> TRUE; +QUERY NOT TRUE <=> FALSE; + +QUERY NOT (a OR b) <=> NOT a AND NOT b; +QUERY NOT (a AND b) <=> NOT a OR NOT b; + +QUERY NOT NOT a <=> a; + + |