diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-07 00:01:13 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-07 00:01:13 +0000 |
| commit | 868d2f9cf7c8dcdee6dbf7d88b4d002065e8ae68 (patch) | |
| tree | d905c11c5cb087c624be564d7815e930339150d9 /test/regress/regress0/precedence | |
| parent | 481c564c68b83925355c82e2d18ade8f1b3fa4db (diff) | |
Adding tests for precedence of arithmetic in CVC inputs
Diffstat (limited to 'test/regress/regress0/precedence')
| -rw-r--r-- | test/regress/regress0/precedence/Makefile.am | 17 | ||||
| -rw-r--r-- | test/regress/regress0/precedence/bool-cmp.cvc | 7 | ||||
| -rw-r--r-- | test/regress/regress0/precedence/cmp-plus.cvc | 8 | ||||
| -rw-r--r-- | test/regress/regress0/precedence/plus-mult.cvc | 8 |
4 files changed, 33 insertions, 7 deletions
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 |