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.

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=$?