updated preprocessing and rewriting input equalities into inequalities for LRA

16 files changed, 206 insertions, 6 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 89df462e5..fb0abfe25 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . arith precedence uf uflra bv arrays datatypes lemmas push-pop
+SUBDIRS = . arith precedence uf uflra bv arrays datatypes lemmas push-pop preprocess
 
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 MAKEFLAGS = -k
@@ -78,7 +78,6 @@ CVC_TESTS = \
 
 # Regression tests derived from bug reports
 BUG_TESTS = \
-	bug2.smt \
 	bug32.cvc \
 	bug49.smt \
 	bug161.smt \
diff --git a/test/regress/regress0/preprocess/Makefile b/test/regress/regress0/preprocess/Makefile
new file mode 100644
index 000000000..c5843db5f
--- /dev/null
+++ b/test/regress/regress0/preprocess/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/preprocess
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am
new file mode 100644
index 000000000..a4fe70946
--- /dev/null
+++ b/test/regress/regress0/preprocess/Makefile.am
@@ -0,0 +1,45 @@
+SUBDIRS = . 
+
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
+MAKEFLAGS = -k
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+
+# Regression tests for SMT inputs
+SMT_TESTS =
+
+# Regression tests for SMT2 inputs
+SMT2_TESTS =
+
+# Regression tests for PL inputs
+CVC_TESTS = \
+	preprocess_00.cvc \
+	preprocess_01.cvc \
+	preprocess_02.cvc \
+	preprocess_03.cvc \
+	preprocess_04.cvc \
+	preprocess_05.cvc \
+	preprocess_06.cvc \
+	preprocess_07.cvc \
+	preprocess_08.cvc \
+	preprocess_09.cvc \
+	preprocess_10.cvc \
+	preprocess_11.cvc \
+	preprocess_12.cvc
+
+# Regression tests derived from bug reports
+BUG_TESTS = 
+
+TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
+
+EXTRA_DIST = $(TESTS)
+
+# synonyms for "check" in this directory
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
diff --git a/test/regress/regress0/preprocess/preprocess_00.cvc b/test/regress/regress0/preprocess/preprocess_00.cvc
new file mode 100644
index 000000000..c91a8e775
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_00.cvc
@@ -0,0 +1,10 @@
+% EXPECT: valid
+
+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);
+
+% EXIT: 20
+
diff --git a/test/regress/regress0/preprocess/preprocess_01.cvc b/test/regress/regress0/preprocess/preprocess_01.cvc
new file mode 100644
index 000000000..e4b2e7dcf
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_01.cvc
@@ -0,0 +1,12 @@
+% 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;
+
+% EXIT: 20
+
diff --git a/test/regress/regress0/preprocess/preprocess_02.cvc b/test/regress/regress0/preprocess/preprocess_02.cvc
new file mode 100644
index 000000000..7907d87ec
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_02.cvc
@@ -0,0 +1,10 @@
+% EXPECT: valid
+
+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);
+
+% EXIT: 20
+
diff --git a/test/regress/regress0/preprocess/preprocess_03.cvc b/test/regress/regress0/preprocess/preprocess_03.cvc
new file mode 100644
index 000000000..e564936a6
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_03.cvc
@@ -0,0 +1,11 @@
+% 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;
+
+% EXIT: 20
+
diff --git a/test/regress/regress0/preprocess/preprocess_04.cvc b/test/regress/regress0/preprocess/preprocess_04.cvc
new file mode 100644
index 000000000..2728e0eb8
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_04.cvc
@@ -0,0 +1,16 @@
+% 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;
+
+% EXIT: 20
+
diff --git a/test/regress/regress0/preprocess/preprocess_05.cvc b/test/regress/regress0/preprocess/preprocess_05.cvc
new file mode 100644
index 000000000..7e337bb13
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_05.cvc
@@ -0,0 +1,16 @@
+% 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;
+
+% EXIT: 10
+
diff --git a/test/regress/regress0/preprocess/preprocess_06.cvc b/test/regress/regress0/preprocess/preprocess_06.cvc
new file mode 100644
index 000000000..e9631b3ac
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_06.cvc
@@ -0,0 +1,15 @@
+% EXPECT: valid
+
+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);
+
+% EXIT: 20
+
diff --git a/test/regress/regress0/preprocess/preprocess_07.cvc b/test/regress/regress0/preprocess/preprocess_07.cvc
new file mode 100644
index 000000000..57ccc6ef8
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_07.cvc
@@ -0,0 +1,11 @@
+% EXPECT: sat
+
+a0, a1, a2, a3, a4, a5: BOOLEAN;
+
+ASSERT ((a0 AND a1 AND a2) <=> (a3 OR a4 OR a5));
+ASSERT (a4);
+
+CHECKSAT;
+
+% EXIT: 10
+
diff --git a/test/regress/regress0/preprocess/preprocess_08.cvc b/test/regress/regress0/preprocess/preprocess_08.cvc
new file mode 100644
index 000000000..6e0edc5a9
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_08.cvc
@@ -0,0 +1,11 @@
+% EXPECT: sat
+
+a0, a1, a2, a3, a4, a5: BOOLEAN;
+
+ASSERT ((a0 AND a1 AND a2) <=> (a3 OR a4 OR a5));
+ASSERT (NOT a1);
+
+CHECKSAT;
+
+% EXIT: 10
+
diff --git a/test/regress/regress0/preprocess/preprocess_09.cvc b/test/regress/regress0/preprocess/preprocess_09.cvc
new file mode 100644
index 000000000..8b62bbafa
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_09.cvc
@@ -0,0 +1,15 @@
+% 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;
+
+% EXIT: 10
+
diff --git a/test/regress/regress0/preprocess/preprocess_10.cvc b/test/regress/regress0/preprocess/preprocess_10.cvc
new file mode 100644
index 000000000..d3b5bfe7e
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_10.cvc
@@ -0,0 +1,12 @@
+% EXPECT: sat
+x: REAL;
+b: BOOLEAN;
+
+ASSERT (x = IF b THEN 10 ELSE -10 ENDIF);
+ASSERT b;
+
+CHECKSAT;
+
+% EXIT: 10
+
+
diff --git a/test/regress/regress0/preprocess/preprocess_11.cvc b/test/regress/regress0/preprocess/preprocess_11.cvc
new file mode 100644
index 000000000..13a8f532c
--- /dev/null
+++ b/test/regress/regress0/preprocess/preprocess_11.cvc
@@ -0,0 +1,11 @@
+% 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;
+
+% EXIT: 10
+
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 3a57ada3f..85c3cb9c9 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -8,13 +8,11 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 
 # Regression tests for SMT inputs
-CVC_TESTS = \
-	test.00.cvc
+CVC_TESTS = 
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
-EXTRA_DIST = $(TESTS) \
-	test.01.cvc
+EXTRA_DIST = $(TESTS) 
 
 # synonyms for "check" in this directory
 .PHONY: regress regress0 test