diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-14 23:49:07 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-14 23:49:07 +0000 |
commit | 19abe15ccc1e310ae3f726b351b0023670ba7962 (patch) | |
tree | 66848c129df4493ab068885fcb0efcad53c5d5e5 /src/printer | |
parent | 8a672c060d2b3946c542c82bd6ca8f89892216ee (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.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 4fc94947b..14347ff8e 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -212,8 +212,12 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo // no-op break; case kind::LAMBDA: - op << "LAMBDA"; - opType = PREFIX; + out << "(LAMBDA"; + toStream(out, n[0], depth, types, true); + out << ": "; + toStream(out, n[1], depth, types, true); + out << ")"; + return; break; case kind::APPLY: toStream(op, n.getOperator(), depth, types, true); |