diff options
Diffstat (limited to 'test/regress/regress0/preprocess')
32 files changed, 220 insertions, 180 deletions
diff --git a/test/regress/regress0/preprocess/preprocess_00.cvc b/test/regress/regress0/preprocess/preprocess_00.cvc deleted file mode 100644 index 2e51a42ad..000000000 --- a/test/regress/regress0/preprocess/preprocess_00.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% EXPECT: entailed - -a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; - -ASSERT (a5); - -QUERY (a0 OR a1 OR a2 OR a3 OR a4 OR a5 OR a6 OR a7 OR a8 OR a9); - - diff --git a/test/regress/regress0/preprocess/preprocess_00.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_00.cvc.smt2 new file mode 100644 index 000000000..685718c3e --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_00.cvc.smt2 @@ -0,0 +1,15 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun a0 () Bool) +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(declare-fun a6 () Bool) +(declare-fun a7 () Bool) +(declare-fun a8 () Bool) +(declare-fun a9 () Bool) +(assert a5) +(check-sat-assuming ( (not (or (or (or (or (or (or (or (or (or a0 a1) a2) a3) a4) a5) a6) a7) a8) a9)) )) diff --git a/test/regress/regress0/preprocess/preprocess_01.cvc b/test/regress/regress0/preprocess/preprocess_01.cvc deleted file mode 100644 index 1d3fafae8..000000000 --- a/test/regress/regress0/preprocess/preprocess_01.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% EXPECT: unsat - -a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; - -ASSERT (a5); - -ASSERT NOT (a0 OR a1 OR a2 OR a3 OR a4 OR a5 OR a6 OR a7 OR a8 OR a9); - -CHECKSAT; - - diff --git a/test/regress/regress0/preprocess/preprocess_01.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_01.cvc.smt2 new file mode 100644 index 000000000..f6bf17ac5 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_01.cvc.smt2 @@ -0,0 +1,16 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun a0 () Bool) +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(declare-fun a6 () Bool) +(declare-fun a7 () Bool) +(declare-fun a8 () Bool) +(declare-fun a9 () Bool) +(assert a5) +(assert (not (or (or (or (or (or (or (or (or (or a0 a1) a2) a3) a4) a5) a6) a7) a8) a9))) +(check-sat) diff --git a/test/regress/regress0/preprocess/preprocess_02.cvc b/test/regress/regress0/preprocess/preprocess_02.cvc deleted file mode 100644 index 0f94103f6..000000000 --- a/test/regress/regress0/preprocess/preprocess_02.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% EXPECT: entailed - -a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; - -ASSERT (NOT a5); - -QUERY NOT (a0 AND a1 AND a2 AND a3 AND a4 AND a5 AND a6 AND a7 AND a8 AND a9); - - diff --git a/test/regress/regress0/preprocess/preprocess_02.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_02.cvc.smt2 new file mode 100644 index 000000000..d4bf1f3d4 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_02.cvc.smt2 @@ -0,0 +1,15 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun a0 () Bool) +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(declare-fun a6 () Bool) +(declare-fun a7 () Bool) +(declare-fun a8 () Bool) +(declare-fun a9 () Bool) +(assert (not a5)) +(check-sat-assuming ( (not (not (and (and (and (and (and (and (and (and (and a0 a1) a2) a3) a4) a5) a6) a7) a8) a9))) )) diff --git a/test/regress/regress0/preprocess/preprocess_03.cvc b/test/regress/regress0/preprocess/preprocess_03.cvc deleted file mode 100644 index 7503594df..000000000 --- a/test/regress/regress0/preprocess/preprocess_03.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: unsat - -a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; - -ASSERT (NOT a5); -ASSERT (a0 AND a1 AND a2 AND a3 AND a4 AND a5 AND a6 AND a7 AND a8 AND a9); - -CHECKSAT; - - diff --git a/test/regress/regress0/preprocess/preprocess_03.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_03.cvc.smt2 new file mode 100644 index 000000000..34d203dc7 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_03.cvc.smt2 @@ -0,0 +1,16 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun a0 () Bool) +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(declare-fun a6 () Bool) +(declare-fun a7 () Bool) +(declare-fun a8 () Bool) +(declare-fun a9 () Bool) +(assert (not a5)) +(assert (and (and (and (and (and (and (and (and (and a0 a1) a2) a3) a4) a5) a6) a7) a8) a9)) +(check-sat) diff --git a/test/regress/regress0/preprocess/preprocess_04.cvc b/test/regress/regress0/preprocess/preprocess_04.cvc deleted file mode 100644 index fd4121432..000000000 --- a/test/regress/regress0/preprocess/preprocess_04.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% EXPECT: unsat - -a0, a1, a2, a3, a4, a5, a6, a7, a8: BOOLEAN; - -ASSERT (NOT a1); -ASSERT (a4 AND a7); -ASSERT - IF (a0 AND a1 AND a2) - THEN (a3 AND a4 AND a5) - ELSE (a6 AND NOT a7 AND a8) - ENDIF; - -CHECKSAT; - - diff --git a/test/regress/regress0/preprocess/preprocess_04.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_04.cvc.smt2 new file mode 100644 index 000000000..3cf309173 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_04.cvc.smt2 @@ -0,0 +1,16 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun a0 () Bool) +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(declare-fun a6 () Bool) +(declare-fun a7 () Bool) +(declare-fun a8 () Bool) +(assert (not a1)) +(assert (and a4 a7)) +(assert (ite (and (and a0 a1) a2) (and (and a3 a4) a5) (and (and a6 (not a7)) a8))) +(check-sat) diff --git a/test/regress/regress0/preprocess/preprocess_05.cvc b/test/regress/regress0/preprocess/preprocess_05.cvc deleted file mode 100644 index 54e070ab5..000000000 --- a/test/regress/regress0/preprocess/preprocess_05.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% EXPECT: sat - -a0, a1, a2, a3, a4, a5, a6, a7, a8: BOOLEAN; - -ASSERT (NOT a1); -ASSERT (a4 AND a7); -ASSERT - IF (a0 AND a1 AND a2) - THEN (a3 AND a4 AND a5) - ELSE (a6 AND a7 AND a8) - ENDIF; - -CHECKSAT; - - diff --git a/test/regress/regress0/preprocess/preprocess_05.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_05.cvc.smt2 new file mode 100644 index 000000000..23d3c238b --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_05.cvc.smt2 @@ -0,0 +1,16 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun a0 () Bool) +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(declare-fun a6 () Bool) +(declare-fun a7 () Bool) +(declare-fun a8 () Bool) +(assert (not a1)) +(assert (and a4 a7)) +(assert (ite (and (and a0 a1) a2) (and (and a3 a4) a5) (and (and a6 a7) a8))) +(check-sat) diff --git a/test/regress/regress0/preprocess/preprocess_06.cvc b/test/regress/regress0/preprocess/preprocess_06.cvc deleted file mode 100644 index abcc7a6ac..000000000 --- a/test/regress/regress0/preprocess/preprocess_06.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% EXPECT: entailed - -a0, a1, a2, a3, a4, a5: BOOLEAN; - -ASSERT (a0 => a1); -ASSERT (a1 => a2); -ASSERT (a2 => a3); -ASSERT (a3 => a4); -ASSERT (a4 => a5); -ASSERT a0; - -QUERY (a0 <=> a5); - - diff --git a/test/regress/regress0/preprocess/preprocess_06.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_06.cvc.smt2 new file mode 100644 index 000000000..d86faccbb --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_06.cvc.smt2 @@ -0,0 +1,16 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun a0 () Bool) +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(assert (=> a0 a1)) +(assert (=> a1 a2)) +(assert (=> a2 a3)) +(assert (=> a3 a4)) +(assert (=> a4 a5)) +(assert a0) +(check-sat-assuming ( (not (= a0 a5)) )) diff --git a/test/regress/regress0/preprocess/preprocess_07.cvc b/test/regress/regress0/preprocess/preprocess_07.cvc deleted file mode 100644 index 3de66a9ac..000000000 --- a/test/regress/regress0/preprocess/preprocess_07.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: sat - -a0, a1, a2, a3, a4, a5: BOOLEAN; - -ASSERT ((a0 AND a1 AND a2) <=> (a3 OR a4 OR a5)); -ASSERT (a4); - -CHECKSAT; - - diff --git a/test/regress/regress0/preprocess/preprocess_07.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_07.cvc.smt2 new file mode 100644 index 000000000..b071c0641 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_07.cvc.smt2 @@ -0,0 +1,12 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun a0 () Bool) +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(assert (= (and (and a0 a1) a2) (or (or a3 a4) a5))) +(assert a4) +(check-sat) diff --git a/test/regress/regress0/preprocess/preprocess_08.cvc b/test/regress/regress0/preprocess/preprocess_08.cvc deleted file mode 100644 index 880c84912..000000000 --- a/test/regress/regress0/preprocess/preprocess_08.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: sat - -a0, a1, a2, a3, a4, a5: BOOLEAN; - -ASSERT ((a0 AND a1 AND a2) <=> (a3 OR a4 OR a5)); -ASSERT (NOT a1); - -CHECKSAT; - - diff --git a/test/regress/regress0/preprocess/preprocess_08.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_08.cvc.smt2 new file mode 100644 index 000000000..baf16dbfa --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_08.cvc.smt2 @@ -0,0 +1,12 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun a0 () Bool) +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(assert (= (and (and a0 a1) a2) (or (or a3 a4) a5))) +(assert (not a1)) +(check-sat) diff --git a/test/regress/regress0/preprocess/preprocess_09.cvc b/test/regress/regress0/preprocess/preprocess_09.cvc deleted file mode 100644 index 1ee07e301..000000000 --- a/test/regress/regress0/preprocess/preprocess_09.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% EXPECT: sat - -a0, a1, a2, a3, a4, a5: BOOLEAN; - -ASSERT ((a0 AND a1 AND a2) <=> (a3 OR a4 OR a5)); -ASSERT (a0); -ASSERT (a1); -ASSERT (a2); -ASSERT (NOT a3); -ASSERT (NOT a5); - -CHECKSAT; - - diff --git a/test/regress/regress0/preprocess/preprocess_09.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_09.cvc.smt2 new file mode 100644 index 000000000..e035c6071 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_09.cvc.smt2 @@ -0,0 +1,16 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun a0 () Bool) +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(assert (= (and (and a0 a1) a2) (or (or a3 a4) a5))) +(assert a0) +(assert a1) +(assert a2) +(assert (not a3)) +(assert (not a5)) +(check-sat) diff --git a/test/regress/regress0/preprocess/preprocess_10.cvc b/test/regress/regress0/preprocess/preprocess_10.cvc deleted file mode 100644 index 6158d6f2a..000000000 --- a/test/regress/regress0/preprocess/preprocess_10.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% EXPECT: sat -x: REAL; -b: BOOLEAN; - -ASSERT (x = IF b THEN 10 ELSE -10 ENDIF); -ASSERT b; - -CHECKSAT; - - - diff --git a/test/regress/regress0/preprocess/preprocess_10.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_10.cvc.smt2 new file mode 100644 index 000000000..f928a51e7 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_10.cvc.smt2 @@ -0,0 +1,8 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x () Real) +(declare-fun b () Bool) +(assert (= x (ite b 10 (- 10)))) +(assert b) +(check-sat) diff --git a/test/regress/regress0/preprocess/preprocess_11.cvc b/test/regress/regress0/preprocess/preprocess_11.cvc deleted file mode 100644 index fe0aed70c..000000000 --- a/test/regress/regress0/preprocess/preprocess_11.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: sat - -x: REAL; -y: REAL; - -ASSERT ((0 = IF TRUE THEN x ELSE 1 ENDIF) AND (0 = IF (x = 0) THEN 0 ELSE 1 ENDIF) AND (x = IF TRUE THEN y ELSE 0 ENDIF) AND (0 = IF TRUE THEN 0 ELSE 0 ENDIF)); - -CHECKSAT; - - diff --git a/test/regress/regress0/preprocess/preprocess_11.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_11.cvc.smt2 new file mode 100644 index 000000000..6cb631b6b --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_11.cvc.smt2 @@ -0,0 +1,7 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x () Real) +(declare-fun y () Real) +(assert (and (and (and (= 0 (ite true x 1)) (= 0 (ite (= x 0) 0 1))) (= x (ite true y 0))) (= 0 (ite true 0 0)))) +(check-sat) diff --git a/test/regress/regress0/preprocess/preprocess_12.cvc b/test/regress/regress0/preprocess/preprocess_12.cvc deleted file mode 100644 index a1da32c57..000000000 --- a/test/regress/regress0/preprocess/preprocess_12.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% EXPECT: sat - -x: REAL; -y: REAL; -b: BOOLEAN; - -ASSERT ((0 = IF b THEN x - y ELSE 2*x ENDIF)); - -CHECKSAT; - - diff --git a/test/regress/regress0/preprocess/preprocess_12.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_12.cvc.smt2 new file mode 100644 index 000000000..c1fd76ad5 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_12.cvc.smt2 @@ -0,0 +1,8 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x () Real) +(declare-fun y () Real) +(declare-fun b () Bool) +(assert (= 0 (ite b (- x y) (* 2 x)))) +(check-sat) diff --git a/test/regress/regress0/preprocess/preprocess_13.cvc b/test/regress/regress0/preprocess/preprocess_13.cvc deleted file mode 100644 index 9a6cd797c..000000000 --- a/test/regress/regress0/preprocess/preprocess_13.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% EXPECT: entailed - -a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; - -ASSERT (a5); - -QUERY (a0 OR (a1 OR (a2 OR (a3 OR (a4 OR (a5 OR (FALSE OR (a6 OR (a7 OR (a8 OR a9)))))))))); - - diff --git a/test/regress/regress0/preprocess/preprocess_13.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_13.cvc.smt2 new file mode 100644 index 000000000..757c98cbb --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_13.cvc.smt2 @@ -0,0 +1,15 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun a0 () Bool) +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(declare-fun a6 () Bool) +(declare-fun a7 () Bool) +(declare-fun a8 () Bool) +(declare-fun a9 () Bool) +(assert a5) +(check-sat-assuming ( (not (or a0 (or a1 (or a2 (or a3 (or a4 (or a5 (or false (or a6 (or a7 (or a8 a9))))))))))) )) diff --git a/test/regress/regress0/preprocess/preprocess_14.cvc b/test/regress/regress0/preprocess/preprocess_14.cvc deleted file mode 100644 index 4fbbce64b..000000000 --- a/test/regress/regress0/preprocess/preprocess_14.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% EXPECT: sat - -a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; - -ASSERT (a5); - -ASSERT (a0 OR (a1 AND (a2 OR (a3 AND (a4 AND (a5 AND (TRUE AND (a6 AND (a7 AND (a8 AND a9)))))))))); - -CHECKSAT; - - diff --git a/test/regress/regress0/preprocess/preprocess_14.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_14.cvc.smt2 new file mode 100644 index 000000000..a63ea247b --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_14.cvc.smt2 @@ -0,0 +1,16 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun a0 () Bool) +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(declare-fun a6 () Bool) +(declare-fun a7 () Bool) +(declare-fun a8 () Bool) +(declare-fun a9 () Bool) +(assert a5) +(assert (or a0 (and a1 (or a2 (and a3 (and a4 (and a5 (and true (and a6 (and a7 (and a8 a9))))))))))) +(check-sat) diff --git a/test/regress/regress0/preprocess/preprocess_15.cvc b/test/regress/regress0/preprocess/preprocess_15.cvc deleted file mode 100644 index ea468c8a4..000000000 --- a/test/regress/regress0/preprocess/preprocess_15.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% EXPECT: sat - -a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; - -ASSERT (a5); - -ASSERT (a0 OR (a1 AND (a2 OR (a3 AND (a4 AND (a5 AND (TRUE AND (a3 AND (a6 AND (a7 AND (a8 AND a9))))))))))); - -CHECKSAT; - - diff --git a/test/regress/regress0/preprocess/preprocess_15.cvc.smt2 b/test/regress/regress0/preprocess/preprocess_15.cvc.smt2 new file mode 100644 index 000000000..b480f0753 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_15.cvc.smt2 @@ -0,0 +1,16 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun a0 () Bool) +(declare-fun a1 () Bool) +(declare-fun a2 () Bool) +(declare-fun a3 () Bool) +(declare-fun a4 () Bool) +(declare-fun a5 () Bool) +(declare-fun a6 () Bool) +(declare-fun a7 () Bool) +(declare-fun a8 () Bool) +(declare-fun a9 () Bool) +(assert a5) +(assert (or a0 (and a1 (or a2 (and a3 (and a4 (and a5 (and true (and a3 (and a6 (and a7 (and a8 a9)))))))))))) +(check-sat) |