diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-09 23:07:33 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-02-09 23:07:33 +0000 |
commit | 044329296028ad944b703929fad4d85aa6183472 (patch) | |
tree | b2a6d56fc5eb4d1bbc4d8d75a1b2814f5b4382be /test | |
parent | 0feb78d917ce5847ede01a5895611e54195bafcd (diff) |
Changes to the CNF conversion and the SAT solver. All regression pass now, and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser.
Diffstat (limited to 'test')
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=$? |