projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3dbabef) | patch
adding three features to CVC parser that drastically improve its support for the...
authorMorgan Deters <mdeters@gmail.com>
Sat, 5 Mar 2011 00:03:08 +0000 (00:03 +0000)
committerMorgan Deters <mdeters@gmail.com>
Sat, 5 Mar 2011 00:03:08 +0000 (00:03 +0000)
commitf3e75370a69e2d61d0b6eaf04593b600ce98c355
treef55a9599ab4c22a8d7d6f08a161c8a4d37934b69tree
parent3dbabefa475f034f07276dc0bb0d86f61f2239c3commit | 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.
src/parser/cvc/Cvc.g diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/let.cvc [new file with mode: 0644] blob