Adding precedence regressions

17 files changed, 125 insertions, 0 deletions

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);