From 4fa28a57ea9a2db7b035bc21d4bccd344701c72f Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Thu, 11 Feb 2010 17:10:36 +0000
Subject: [PATCH] Adding precedence regressions

---
 test/regress/regress0/Makefile.am             |  2 ++
 test/regress/regress0/precedence/Makefile     |  8 ++++++
 test/regress/regress0/precedence/Makefile.am  | 25 +++++++++++++++++++
 test/regress/regress0/precedence/and-not.cvc  |  6 +++++
 test/regress/regress0/precedence/and-xor.cvc  |  6 +++++
 test/regress/regress0/precedence/eq-fun.cvc   |  8 ++++++
 .../regress/regress0/precedence/iff-assoc.cvc |  6 +++++
 .../regress0/precedence/iff-implies.cvc       |  6 +++++
 .../regress0/precedence/implies-assoc.cvc     |  6 +++++
 .../regress0/precedence/implies-iff.cvc       |  6 +++++
 .../regress0/precedence/implies-or.cvc        |  6 +++++
 test/regress/regress0/precedence/not-and.cvc  |  6 +++++
 test/regress/regress0/precedence/not-eq.cvc   |  6 +++++
 .../regress0/precedence/or-implies.cvc        |  6 +++++
 test/regress/regress0/precedence/or-xor.cvc   |  6 +++++
 test/regress/regress0/precedence/xor-and.cvc  |  6 +++++
 .../regress/regress0/precedence/xor-assoc.cvc |  6 +++++
 test/regress/regress0/precedence/xor-or.cvc   |  6 +++++
 18 files changed, 127 insertions(+)
 create mode 100644 test/regress/regress0/precedence/Makefile
 create mode 100644 test/regress/regress0/precedence/Makefile.am
 create mode 100644 test/regress/regress0/precedence/and-not.cvc
 create mode 100644 test/regress/regress0/precedence/and-xor.cvc
 create mode 100644 test/regress/regress0/precedence/eq-fun.cvc
 create mode 100644 test/regress/regress0/precedence/iff-assoc.cvc
 create mode 100644 test/regress/regress0/precedence/iff-implies.cvc
 create mode 100644 test/regress/regress0/precedence/implies-assoc.cvc
 create mode 100644 test/regress/regress0/precedence/implies-iff.cvc
 create mode 100644 test/regress/regress0/precedence/implies-or.cvc
 create mode 100644 test/regress/regress0/precedence/not-and.cvc
 create mode 100644 test/regress/regress0/precedence/not-eq.cvc
 create mode 100644 test/regress/regress0/precedence/or-implies.cvc
 create mode 100644 test/regress/regress0/precedence/or-xor.cvc
 create mode 100644 test/regress/regress0/precedence/xor-and.cvc
 create mode 100644 test/regress/regress0/precedence/xor-assoc.cvc
 create mode 100644 test/regress/regress0/precedence/xor-or.cvc

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 09be302af..5ec24400d 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,3 +1,5 @@
+SUBDIRS = precedence
+
 TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4
 TESTS =	hole6.cvc \
 	logops.01.cvc \
diff --git a/test/regress/regress0/precedence/Makefile b/test/regress/regress0/precedence/Makefile
new file mode 100644
index 000000000..a77d94db1
--- /dev/null
+++ b/test/regress/regress0/precedence/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/precedence
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am
new file mode 100644
index 000000000..36722b81b
--- /dev/null
+++ b/test/regress/regress0/precedence/Makefile.am
@@ -0,0 +1,25 @@
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4
+TESTS =	iff-implies.cvc \
+	implies-iff.cvc \
+	implies-or.cvc \
+	or-implies.cvc \
+	or-xor.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
+
+
+# synonyms for "check"
+.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/precedence/and-not.cvc b/test/regress/regress0/precedence/and-not.cvc
new file mode 100644
index 000000000..d283ca881
--- /dev/null
+++ b/test/regress/regress0/precedence/and-not.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+% Simple test for right precedence of AND and NOT.
+
+A, B: BOOLEAN;
+
+QUERY (A AND NOT B) <=> (A AND (NOT B));
diff --git a/test/regress/regress0/precedence/and-xor.cvc b/test/regress/regress0/precedence/and-xor.cvc
new file mode 100644
index 000000000..c7268727a
--- /dev/null
+++ b/test/regress/regress0/precedence/and-xor.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+% Simple test for right precedence of XOR and AND.
+
+A, B, C: BOOLEAN;
+
+QUERY (A AND B XOR C) <=> ((A AND B) XOR C);
diff --git a/test/regress/regress0/precedence/eq-fun.cvc b/test/regress/regress0/precedence/eq-fun.cvc
new file mode 100644
index 000000000..43feeb1f8
--- /dev/null
+++ b/test/regress/regress0/precedence/eq-fun.cvc
@@ -0,0 +1,8 @@
+% EXPECT: VALID
+% Simple test for right precedence of function application and =
+
+T : TYPE;
+x , y: T;
+f : T -> T;
+
+QUERY (f(x) = f(y)) <=> ((f(x)) = (f(y)));
diff --git a/test/regress/regress0/precedence/iff-assoc.cvc b/test/regress/regress0/precedence/iff-assoc.cvc
new file mode 100644
index 000000000..82e0cbc72
--- /dev/null
+++ b/test/regress/regress0/precedence/iff-assoc.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+% Simple test for right associativity of <=>
+
+A, B, C: BOOLEAN;
+
+QUERY (A <=> B <=> C) <=> (A <=> (B <=> C));
diff --git a/test/regress/regress0/precedence/iff-implies.cvc b/test/regress/regress0/precedence/iff-implies.cvc
new file mode 100644
index 000000000..bebafce14
--- /dev/null
+++ b/test/regress/regress0/precedence/iff-implies.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+% Simple test for right precedence of <=> and =>.
+
+A, B, C: BOOLEAN;
+
+QUERY (A <=> B => C) <=> ((A <=> (B => C)));
diff --git a/test/regress/regress0/precedence/implies-assoc.cvc b/test/regress/regress0/precedence/implies-assoc.cvc
new file mode 100644
index 000000000..c73616caf
--- /dev/null
+++ b/test/regress/regress0/precedence/implies-assoc.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+% Simple test for right associativity of =>
+
+A, B, C: BOOLEAN;
+
+QUERY (A => B => C) <=> (A => (B => C));
diff --git a/test/regress/regress0/precedence/implies-iff.cvc b/test/regress/regress0/precedence/implies-iff.cvc
new file mode 100644
index 000000000..f44c4bc75
--- /dev/null
+++ b/test/regress/regress0/precedence/implies-iff.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+% Simple test for right precedence of <=> and =>.
+
+A, B, C: BOOLEAN;
+
+QUERY (A => B <=> C) <=> ((A => B) <=> C);
diff --git a/test/regress/regress0/precedence/implies-or.cvc b/test/regress/regress0/precedence/implies-or.cvc
new file mode 100644
index 000000000..835da8570
--- /dev/null
+++ b/test/regress/regress0/precedence/implies-or.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+% Simple test for right precedence of => and OR.
+
+A, B, C: BOOLEAN;
+
+QUERY (A => B OR C) <=> (A => (B OR C));
diff --git a/test/regress/regress0/precedence/not-and.cvc b/test/regress/regress0/precedence/not-and.cvc
new file mode 100644
index 000000000..44c27af53
--- /dev/null
+++ b/test/regress/regress0/precedence/not-and.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+% Simple test for right precedence of AND and NOT.
+
+A, B, C: BOOLEAN;
+
+QUERY (NOT A AND B) <=> ((NOT A) AND B);
diff --git a/test/regress/regress0/precedence/not-eq.cvc b/test/regress/regress0/precedence/not-eq.cvc
new file mode 100644
index 000000000..1126926b8
--- /dev/null
+++ b/test/regress/regress0/precedence/not-eq.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+% Simple test for right precedence of = and NOT.
+
+A, B: BOOLEAN;
+
+QUERY (NOT A = B) <=> (NOT (A = B));
diff --git a/test/regress/regress0/precedence/or-implies.cvc b/test/regress/regress0/precedence/or-implies.cvc
new file mode 100644
index 000000000..3b336db5a
--- /dev/null
+++ b/test/regress/regress0/precedence/or-implies.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+% Simple test for right precedence of => and OR.
+
+A, B, C: BOOLEAN;
+
+QUERY (A OR B => C) <=> ((A OR B) => C);
diff --git a/test/regress/regress0/precedence/or-xor.cvc b/test/regress/regress0/precedence/or-xor.cvc
new file mode 100644
index 000000000..2198962c8
--- /dev/null
+++ b/test/regress/regress0/precedence/or-xor.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+% Simple test for right precedence of OR and XOR.
+
+A, B, C: BOOLEAN;
+
+QUERY (A OR B XOR C) <=> (A OR (B XOR C));
diff --git a/test/regress/regress0/precedence/xor-and.cvc b/test/regress/regress0/precedence/xor-and.cvc
new file mode 100644
index 000000000..ccdaeebad
--- /dev/null
+++ b/test/regress/regress0/precedence/xor-and.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+% Simple test for right precedence of XOR and AND.
+
+A, B, C: BOOLEAN;
+
+QUERY (A XOR B AND C) <=> (A XOR (B AND C));
diff --git a/test/regress/regress0/precedence/xor-assoc.cvc b/test/regress/regress0/precedence/xor-assoc.cvc
new file mode 100644
index 000000000..ffdb2c8c9
--- /dev/null
+++ b/test/regress/regress0/precedence/xor-assoc.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+% Simple test for left associativity of XOR
+
+A, B, C: BOOLEAN;
+
+QUERY (A XOR B XOR C) <=> ((A XOR B) XOR C);
diff --git a/test/regress/regress0/precedence/xor-or.cvc b/test/regress/regress0/precedence/xor-or.cvc
new file mode 100644
index 000000000..959dec14e
--- /dev/null
+++ b/test/regress/regress0/precedence/xor-or.cvc
@@ -0,0 +1,6 @@
+% EXPECT: VALID
+% Simple test for right precedence of OR and XOR.
+
+A, B, C: BOOLEAN;
+
+QUERY (A XOR B OR C) <=> ((A XOR B) OR C);
-- 
2.30.2