projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6a5fb6d) | patch
* Fix ITEs and functions in CVC language printer.
authorMorgan Deters <mdeters@gmail.com>
Fri, 6 Apr 2012 22:06:52 +0000 (22:06 +0000)
committerMorgan Deters <mdeters@gmail.com>
Fri, 6 Apr 2012 22:06:52 +0000 (22:06 +0000)
commit7237456b4e2e5a119feacf98f52ec9e55d7a62a5
treeea510f4987dadcdbbb361684445419e4939cdf00tree
parent6a5fb6d945b109921cb9b6117f4ede0b6d110c08commit | diff
* Fix ITEs and functions in CVC language printer.
* Permit "BOOL = BOOL" in CVC language parser (auto-replaced with IFF
  internally, except in strict mode).
* SExpr atoms now can be string-, integer-, or rational-valued.
* SmtEngine::setInfo(":status", ...) now properly dumps a
  SetBenchmarkStatusCommand rather than a SetInfoCommand.
* Some dumping fixes (resolves bug 313)
src/expr/command.h diff | blob | history
src/parser/cvc/Cvc.g diff | blob | history
src/parser/smt/Smt.g diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/printer/cvc/cvc_printer.cpp diff | blob | history
src/printer/smt/smt_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/util/sexpr.h diff | blob | history