diff options
Diffstat (limited to 'test/regress')
30 files changed, 129 insertions, 85 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index df0268f80..09be302af 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,19 +1,38 @@ TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 -TESTS = boolean.cvc \ - bug1.cvc \ - hole6.cvc \ - logops.cvc \ - queries0.cvc \ +TESTS = hole6.cvc \ + logops.01.cvc \ + logops.02.cvc \ + logops.03.cvc \ + logops.04.cvc \ + logops.05.cvc \ simple2.smt \ simple.cvc \ simple.smt \ - simple-uf.smt \ smallcnf.cvc \ test11.cvc \ - test12.cvc \ test9.cvc \ uf20-03.cvc \ - wiki.cvc + wiki.01.cvc \ + wiki.02.cvc \ + wiki.03.cvc \ + wiki.04.cvc \ + wiki.05.cvc \ + wiki.06.cvc \ + wiki.07.cvc \ + wiki.08.cvc \ + wiki.09.cvc \ + wiki.10.cvc \ + wiki.11.cvc \ + wiki.12.cvc \ + wiki.13.cvc \ + wiki.14.cvc \ + wiki.15.cvc \ + wiki.16.cvc \ + wiki.17.cvc \ + wiki.18.cvc \ + wiki.19.cvc \ + wiki.20.cvc \ + wiki.21.cvc # synonyms for "check" .PHONY: regress regress0 test diff --git a/test/regress/regress0/logops.01.cvc b/test/regress/regress0/logops.01.cvc new file mode 100644 index 000000000..d947d1a27 --- /dev/null +++ b/test/regress/regress0/logops.01.cvc @@ -0,0 +1,3 @@ +a, b, c: BOOLEAN; +% EXPECT: VALID +QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a); diff --git a/test/regress/regress0/logops.02.cvc b/test/regress/regress0/logops.02.cvc new file mode 100644 index 000000000..ba2d55b4f --- /dev/null +++ b/test/regress/regress0/logops.02.cvc @@ -0,0 +1,3 @@ +a, b, c: BOOLEAN; +% EXPECT: INVALID +QUERY NOT c AND b; diff --git a/test/regress/regress0/logops.03.cvc b/test/regress/regress0/logops.03.cvc new file mode 100644 index 000000000..85b23d2b0 --- /dev/null +++ b/test/regress/regress0/logops.03.cvc @@ -0,0 +1,3 @@ +a, b, c: BOOLEAN; +% EXPECT: VALID +QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b)); diff --git a/test/regress/regress0/logops.04.cvc b/test/regress/regress0/logops.04.cvc new file mode 100644 index 000000000..a71096542 --- /dev/null +++ b/test/regress/regress0/logops.04.cvc @@ -0,0 +1,3 @@ +a, b, c: BOOLEAN; +% EXPECT: VALID +QUERY (a => b) <=> (NOT a OR b); diff --git a/test/regress/regress0/logops.05.cvc b/test/regress/regress0/logops.05.cvc new file mode 100644 index 000000000..19bbae5b4 --- /dev/null +++ b/test/regress/regress0/logops.05.cvc @@ -0,0 +1,4 @@ +a, b, c: BOOLEAN; +% EXPECT: VALID +QUERY TRUE XOR FALSE; + diff --git a/test/regress/regress0/logops.cvc b/test/regress/regress0/logops.cvc deleted file mode 100644 index 7bd2a356d..000000000 --- a/test/regress/regress0/logops.cvc +++ /dev/null @@ -1,17 +0,0 @@ -a, b, c: BOOLEAN; - -% EXPECT: VALID -QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a); - -% EXPECT: INVALID -QUERY NOT c AND b; - -% EXPECT: VALID -QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b)); - -% EXPECT: VALID -QUERY (a => b) <=> (NOT a OR b); - -% EXPECT: VALID -QUERY TRUE XOR FALSE; - diff --git a/test/regress/regress0/wiki.01.cvc b/test/regress/regress0/wiki.01.cvc new file mode 100644 index 000000000..57660b5a1 --- /dev/null +++ b/test/regress/regress0/wiki.01.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR (b OR c) <=> (a OR b) OR c; diff --git a/test/regress/regress0/wiki.02.cvc b/test/regress/regress0/wiki.02.cvc new file mode 100644 index 000000000..baba45927 --- /dev/null +++ b/test/regress/regress0/wiki.02.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND (b AND c) <=> (a AND b) AND c; diff --git a/test/regress/regress0/wiki.03.cvc b/test/regress/regress0/wiki.03.cvc new file mode 100644 index 000000000..791cc45c8 --- /dev/null +++ b/test/regress/regress0/wiki.03.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR b <=> b OR a; diff --git a/test/regress/regress0/wiki.04.cvc b/test/regress/regress0/wiki.04.cvc new file mode 100644 index 000000000..f0f73ce1f --- /dev/null +++ b/test/regress/regress0/wiki.04.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND b <=> b AND a; diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc new file mode 100644 index 000000000..afb094dae --- /dev/null +++ b/test/regress/regress0/wiki.05.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR (a AND b) <=> a; diff --git a/test/regress/regress0/wiki.06.cvc b/test/regress/regress0/wiki.06.cvc new file mode 100644 index 000000000..421bfbdfd --- /dev/null +++ b/test/regress/regress0/wiki.06.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND (a OR b) <=> a; diff --git a/test/regress/regress0/wiki.07.cvc b/test/regress/regress0/wiki.07.cvc new file mode 100644 index 000000000..a28cbf553 --- /dev/null +++ b/test/regress/regress0/wiki.07.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR (b AND c) <=> (a OR b) AND (a OR c); diff --git a/test/regress/regress0/wiki.08.cvc b/test/regress/regress0/wiki.08.cvc new file mode 100644 index 000000000..70fc5f430 --- /dev/null +++ b/test/regress/regress0/wiki.08.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND (b OR c) <=> (a AND b) OR (a AND c); diff --git a/test/regress/regress0/wiki.09.cvc b/test/regress/regress0/wiki.09.cvc new file mode 100644 index 000000000..d3118536d --- /dev/null +++ b/test/regress/regress0/wiki.09.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR NOT a; diff --git a/test/regress/regress0/wiki.10.cvc b/test/regress/regress0/wiki.10.cvc new file mode 100644 index 000000000..41a9bcd3f --- /dev/null +++ b/test/regress/regress0/wiki.10.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND NOT a <=> FALSE; diff --git a/test/regress/regress0/wiki.11.cvc b/test/regress/regress0/wiki.11.cvc new file mode 100644 index 000000000..e9c0b9cce --- /dev/null +++ b/test/regress/regress0/wiki.11.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR a <=> a; diff --git a/test/regress/regress0/wiki.12.cvc b/test/regress/regress0/wiki.12.cvc new file mode 100644 index 000000000..d5e7bd776 --- /dev/null +++ b/test/regress/regress0/wiki.12.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND a <=> a; diff --git a/test/regress/regress0/wiki.13.cvc b/test/regress/regress0/wiki.13.cvc new file mode 100644 index 000000000..2674ba47b --- /dev/null +++ b/test/regress/regress0/wiki.13.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR FALSE <=> a; diff --git a/test/regress/regress0/wiki.14.cvc b/test/regress/regress0/wiki.14.cvc new file mode 100644 index 000000000..378b84dcd --- /dev/null +++ b/test/regress/regress0/wiki.14.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND TRUE <=> a; diff --git a/test/regress/regress0/wiki.15.cvc b/test/regress/regress0/wiki.15.cvc new file mode 100644 index 000000000..ca51c4632 --- /dev/null +++ b/test/regress/regress0/wiki.15.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a OR TRUE <=> TRUE; diff --git a/test/regress/regress0/wiki.16.cvc b/test/regress/regress0/wiki.16.cvc new file mode 100644 index 000000000..af47433f8 --- /dev/null +++ b/test/regress/regress0/wiki.16.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY a AND FALSE <=> FALSE; diff --git a/test/regress/regress0/wiki.17.cvc b/test/regress/regress0/wiki.17.cvc new file mode 100644 index 000000000..dc7e7a1c3 --- /dev/null +++ b/test/regress/regress0/wiki.17.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY NOT FALSE <=> TRUE; diff --git a/test/regress/regress0/wiki.18.cvc b/test/regress/regress0/wiki.18.cvc new file mode 100644 index 000000000..21a87f4b5 --- /dev/null +++ b/test/regress/regress0/wiki.18.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY NOT TRUE <=> FALSE; diff --git a/test/regress/regress0/wiki.19.cvc b/test/regress/regress0/wiki.19.cvc new file mode 100644 index 000000000..c6081c200 --- /dev/null +++ b/test/regress/regress0/wiki.19.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY NOT (a OR b) <=> NOT a AND NOT b; diff --git a/test/regress/regress0/wiki.20.cvc b/test/regress/regress0/wiki.20.cvc new file mode 100644 index 000000000..3bec9348b --- /dev/null +++ b/test/regress/regress0/wiki.20.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY NOT (a AND b) <=> NOT a OR NOT b; diff --git a/test/regress/regress0/wiki.21.cvc b/test/regress/regress0/wiki.21.cvc new file mode 100644 index 000000000..e99ba2d68 --- /dev/null +++ b/test/regress/regress0/wiki.21.cvc @@ -0,0 +1,4 @@ +a, b, c : BOOLEAN; + +% EXPECT: VALID +QUERY NOT NOT a <=> a; diff --git a/test/regress/regress0/wiki.cvc b/test/regress/regress0/wiki.cvc deleted file mode 100644 index b5894dbad..000000000 --- a/test/regress/regress0/wiki.cvc +++ /dev/null @@ -1,58 +0,0 @@ -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID -% EXPECT: VALID - -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; - - diff --git a/test/regress/run_regression b/test/regress/run_regression index c141cf43a..2be776b3f 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -56,8 +56,8 @@ expfile=`mktemp -t cvc4_expected.XXXXXXXXXX` outfile=`mktemp -t cvc4_output.XXXXXXXXXX` echo "$expected_output" >"$expfile" -echo "$cvc4" --segv-nospin "$benchmark" -"$cvc4" --segv-nospin "$benchmark" | tee "$outfile" +# echo "$cvc4" --segv-nospin "$benchmark" +"$cvc4" --segv-nospin "$benchmark" > "$outfile" diffs=`diff -u "$expfile" "$outfile"` diffexit=$? |