diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-12-14 22:44:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-12-14 22:44:58 +0000 |
commit | 5b04e6f0b29be4f376ab1f306529bf8a22111bd5 (patch) | |
tree | f4569b4e67f617243ddb73ca7cf741607b43bac6 /src/printer/cvc/cvc_printer.cpp | |
parent | ee64b3fa49a22b89ffb3e62d8d7144fc9b99754e (diff) |
minor fixes to printing and parsing of CVC-language defined functions and lambdas; resolves bug 294
Diffstat (limited to 'src/printer/cvc/cvc_printer.cpp')
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 0d47c9c6c..8d76a7332 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -484,15 +484,19 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() Expr func = c->getFunction(); const vector<Expr>& formals = c->getFormals(); Expr formula = c->getFormula(); - out << func << " : " << func.getType() << " = LAMBDA("; - vector<Expr>::const_iterator i = formals.begin(); - while(i != formals.end()) { - out << (*i) << ":" << (*i).getType(); - if(++i != formals.end()) { - out << ", "; + out << func << " : " << func.getType() << " = "; + if(formals.size() > 0) { + out << "LAMBDA("; + vector<Expr>::const_iterator i = formals.begin(); + while(i != formals.end()) { + out << (*i) << ":" << (*i).getType(); + if(++i != formals.end()) { + out << ", "; + } } + out << "): "; } - out << "): " << formula << ";"; + out << formula << ";"; } static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() { |