diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-05 16:21:50 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-05 16:21:50 +0000 |
commit | 7342d1ca87397f3d5beb2c04b819243303e69a7c (patch) | |
tree | 9e166f1884275be7d4b33b13b8bcfe9418e61033 /test | |
parent | af25c3f8498198dd6dd114c3b4ef39af54611e1e (diff) |
updated preprocessing and rewriting input equalities into inequalities for LRA
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/Makefile | 8 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/Makefile.am | 45 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_00.cvc | 10 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_01.cvc | 12 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_02.cvc | 10 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_03.cvc | 11 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_04.cvc | 16 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_05.cvc | 16 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_06.cvc | 15 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_07.cvc | 11 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_08.cvc | 11 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_09.cvc | 15 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_10.cvc | 12 | ||||
-rw-r--r-- | test/regress/regress0/preprocess/preprocess_11.cvc | 11 | ||||
-rw-r--r-- | test/regress/regress0/push-pop/Makefile.am | 6 |
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 |