Adding tests for precedence of arithmetic in CVC inputs

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 830b1022de1bea0d77afb09e066573a89e553df5..8eb745637695937c0313c745ed533c911a2e315f 100644 (file)
--- 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 (file)
index 0000000..79c3bce
--- /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 4cf18f17dbb93608bc47b59c80d27c9cc43330a3..ba9fda9a742711d0c36d79aab53a70156ea1038d 100644 (file)
--- 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 (file)
index 0000000..ef1345c
--- /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 (file)
index 0000000..af2823f
--- /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 (file)
index 0000000..c72b30d
--- /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 (file)
index 0000000..a6fecba
--- /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))
+)