diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-03-05 00:03:08 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-03-05 00:03:08 +0000 |
| commit | f3e75370a69e2d61d0b6eaf04593b600ce98c355 (patch) | |
| tree | f55a9599ab4c22a8d7d6f08a161c8a4d37934b69 /test/regress/regress0 | |
| parent | 3dbabefa475f034f07276dc0bb0d86f61f2239c3 (diff) | |
adding three features to CVC parser that drastically improve its support for the language: LET now supported (but not "type-lets" yet), OPTION now supported, and ^ operator (exponentiation) supported for nonnegative integer exponents. The latter simply expands to MULT, and of course fails assertions in arithmetic if a variable is raised to n >= 2. Also other CVC parser clean-up.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/let.cvc | 8 |
2 files changed, 9 insertions, 0 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 383cb01cb..50c43fcb9 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -41,6 +41,7 @@ CVC_TESTS = \ boolean-prec.cvc \ hole6.cvc \ ite.cvc \ + let.cvc \ logops.01.cvc \ logops.02.cvc \ logops.03.cvc \ diff --git a/test/regress/regress0/let.cvc b/test/regress/regress0/let.cvc new file mode 100644 index 000000000..da628de3e --- /dev/null +++ b/test/regress/regress0/let.cvc @@ -0,0 +1,8 @@ +% EXPECT: valid +U: TYPE; +a: U; +b: U; +f: U -> U; +QUERY LET v_0 = (a = b) +IN NOT (v_0 AND NOT v_0); +% EXIT: 20 |