Adding precedence regressions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 09be302af4ac2cd0b224decf22e897e67d3fb5c1..5ec24400d6842fa0d4708c9126dd7969efc8d772 100644 (file)
--- 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 (file)
index 0000000..a77d94d
--- /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 (file)
index 0000000..36722b8
--- /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 (file)
index 0000000..d283ca8
--- /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 (file)
index 0000000..c726872
--- /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 (file)
index 0000000..43feeb1
--- /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 (file)
index 0000000..82e0cbc
--- /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 (file)
index 0000000..bebafce
--- /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 (file)
index 0000000..c73616c
--- /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 (file)
index 0000000..f44c4bc
--- /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 (file)
index 0000000..835da85
--- /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 (file)
index 0000000..44c27af
--- /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 (file)
index 0000000..1126926
--- /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 (file)
index 0000000..3b336db
--- /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 (file)
index 0000000..2198962
--- /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 (file)
index 0000000..ccdaeeb
--- /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 (file)
index 0000000..ffdb2c8
--- /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 (file)
index 0000000..959dec1
--- /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);