projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8a672c0) | patch
Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC printer...
authorTim King <taking@cs.nyu.edu>
Wed, 14 Nov 2012 23:49:07 +0000 (23:49 +0000)
committerTim King <taking@cs.nyu.edu>
Wed, 14 Nov 2012 23:49:07 +0000 (23:49 +0000)
commit19abe15ccc1e310ae3f726b351b0023670ba7962
tree66848c129df4493ab068885fcb0efcad53c5d5e5tree
parent8a672c060d2b3946c542c82bd6ca8f89892216eecommit | diff
Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC printer now properly prints LAMBDAs. Model builing now gives bound variables names that can be parsed bypresentation language.
src/parser/parser.cpp diff | blob | history
src/printer/cvc/cvc_printer.cpp diff | blob | history
src/theory/model.cpp diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/print_lambda.cvc [new file with mode: 0644] blob