From 868d2f9cf7c8dcdee6dbf7d88b4d002065e8ae68 Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Wed, 7 Jul 2010 00:01:13 +0000
Subject: [PATCH] Adding tests for precedence of arithmetic in CVC inputs

---
 test/regress/regress0/Makefile.am             | 47 ++++++++++++-------
 test/regress/regress0/ite.cvc                 |  3 ++
 test/regress/regress0/precedence/Makefile.am  | 17 ++++---
 test/regress/regress0/precedence/bool-cmp.cvc |  7 +++
 test/regress/regress0/precedence/cmp-plus.cvc |  8 ++++
 .../regress/regress0/precedence/plus-mult.cvc |  8 ++++
 test/regress/regress0/symmetric.smt           |  9 ++++
 7 files changed, 75 insertions(+), 24 deletions(-)
 create mode 100644 test/regress/regress0/ite.cvc
 create mode 100644 test/regress/regress0/precedence/bool-cmp.cvc
 create mode 100644 test/regress/regress0/precedence/cmp-plus.cvc
 create mode 100644 test/regress/regress0/precedence/plus-mult.cvc
 create mode 100644 test/regress/regress0/symmetric.smt

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 830b1022d..8eb745637 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -5,11 +5,16 @@ TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
 # These are run for all build profiles.
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
-TESTS =	\
-	boolean-prec.cvc \
+
+# Regression tests for SMT inputs
+SMT_TESTS = \
 	distinct.smt \
 	flet.smt \
 	flet2.smt \
+	fuzz_1.smt \
+	fuzz_3.smt \
+	ineq_basic.smt \
+	ineq_slack.smt \
 	ite_real_int_type.smt \
 	ite_real_valid.smt \
 	let.smt \
@@ -18,21 +23,21 @@ TESTS =	\
 	simple2.smt \
         simple-lra.smt \
         simple-rdl.smt \
-	simple-uf.smt \
-	ite.smt2 \
+	simple-uf.smt
+
+# Regression tests for SMT2 inputs
+SMT2_TESTS = \
 	ite2.smt2 \
 	ite3.smt2 \
 	ite4.smt2 \
         simple-lra.smt2 \
         simple-rdl.smt2 \
-	simple-uf.smt2 \
-	bug2.smt \
-	bug32.cvc \
-	bug49.smt \
-	bug161.smt \
-	bug164.smt \
-	bug167.smt \
-	bug168.smt \
+	simple-uf.smt2
+
+# Regression tests for PL inputs
+CVC_TESTS = \
+	boolean-prec.cvc \
+        ite.cvc \
 	hole6.cvc \
 	logops.01.cvc \
 	logops.02.cvc \
@@ -40,8 +45,6 @@ TESTS =	\
 	logops.04.cvc \
 	logops.05.cvc \
 	simple.cvc \
-	ineq_basic.smt \
-	ineq_slack.smt \
 	smallcnf.cvc \
 	test11.cvc \
 	test9.cvc \
@@ -66,9 +69,19 @@ TESTS =	\
 	wiki.18.cvc \
 	wiki.19.cvc \
 	wiki.20.cvc \
-	wiki.21.cvc \
-	fuzz_1.smt \
-	fuzz_3.smt
+	wiki.21.cvc
+
+# Regression tests derived from bug reports
+BUG_TESTS = \
+	bug2.smt \
+	bug32.cvc \
+	bug49.smt \
+	bug161.smt \
+	bug164.smt \
+	bug167.smt \
+	bug168.smt
+
+TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/ite.cvc b/test/regress/regress0/ite.cvc
new file mode 100644
index 000000000..79c3bce1e
--- /dev/null
+++ b/test/regress/regress0/ite.cvc
@@ -0,0 +1,3 @@
+% EXPECT: UNSAT
+x, y : REAL;
+CHECKSAT (NOT (x = IF TRUE THEN x ELSE y ENDIF));
diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am
index 4cf18f17d..ba9fda9a7 100644
--- a/test/regress/regress0/precedence/Makefile.am
+++ b/test/regress/regress0/precedence/Makefile.am
@@ -4,20 +4,23 @@ TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS = \
+	and-xor.cvc \
+	and-not.cvc \
+        bool-cmp.cvc \
+        cmp-plus.cvc \
+	eq-fun.cvc \
+	iff-assoc.cvc \
 	iff-implies.cvc \
+	implies-assoc.cvc \
 	implies-iff.cvc \
 	implies-or.cvc \
+	not-and.cvc \
+	not-eq.cvc \
 	or-implies.cvc \
 	or-xor.cvc \
+        plus-mult.cvc \
 	xor-or.cvc \
 	xor-and.cvc \
-	and-xor.cvc \
-	and-not.cvc \
-	not-and.cvc \
-	not-eq.cvc \
-	eq-fun.cvc \
-	iff-assoc.cvc \
-	implies-assoc.cvc \
 	xor-assoc.cvc
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/precedence/bool-cmp.cvc b/test/regress/regress0/precedence/bool-cmp.cvc
new file mode 100644
index 000000000..ef1345cc1
--- /dev/null
+++ b/test/regress/regress0/precedence/bool-cmp.cvc
@@ -0,0 +1,7 @@
+% EXPECT: VALID
+% Simple test for right precedence of comparisons and booleans
+
+x , y, z: INT;
+
+QUERY (x > y AND y = z OR x < z) <=> (((x > y) AND (y = z)) OR (x < z));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/cmp-plus.cvc b/test/regress/regress0/precedence/cmp-plus.cvc
new file mode 100644
index 000000000..af2823fcf
--- /dev/null
+++ b/test/regress/regress0/precedence/cmp-plus.cvc
@@ -0,0 +1,8 @@
+% EXPECT: VALID
+% Simple test for right precedence of comparisons and plus/minus
+
+x, y, z: INT;
+
+QUERY (x + y - z > 0 AND 0 < x - y + z) <=> 
+  ((((x + y) - z) > 0) AND (0 < ((x - y) + z)));
+% EXIT: 20
diff --git a/test/regress/regress0/precedence/plus-mult.cvc b/test/regress/regress0/precedence/plus-mult.cvc
new file mode 100644
index 000000000..c72b30d1c
--- /dev/null
+++ b/test/regress/regress0/precedence/plus-mult.cvc
@@ -0,0 +1,8 @@
+% EXPECT: VALID
+% Simple test for right precedence of plus/minus and mult/divide
+
+a, b, c, d: INT;
+
+QUERY (a + b * c - d = a * b + c * d) <=> 
+  (((a + (b * c)) - d) = ((a * b) + (c * d)));
+% EXIT: 20
diff --git a/test/regress/regress0/symmetric.smt b/test/regress/regress0/symmetric.smt
new file mode 100644
index 000000000..a6fecba44
--- /dev/null
+++ b/test/regress/regress0/symmetric.smt
@@ -0,0 +1,9 @@
+(benchmark symmetric
+:status unsat
+:logic QF_UF
+:extrapreds ((p U U))
+:extrafuns ((x U) (y U))
+:assumption (implies (p x y) (p y x))
+:assumption (p x y)
+:formula (not (p y x))
+)
-- 
2.30.2