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 | |
parent | ee64b3fa49a22b89ffb3e62d8d7144fc9b99754e (diff) |
minor fixes to printing and parsing of CVC-language defined functions and lambdas; resolves bug 294
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/expr_template.cpp | 1 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 4 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 18 |
3 files changed, 15 insertions, 8 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 29aa1a737..3c376f632 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -206,6 +206,7 @@ Expr Expr::getOperator() const { Type Expr::getType(bool check) const throw (TypeCheckingException) { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + CheckArgument(!d_node->isNull(), this, "Can't get type of null expression!"); return d_exprManager->getType(*this, check); } diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 2d659cfe3..9f0c2cddb 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -897,6 +897,7 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri } } } else { + // f is not null-- meaning this is a definition not a declaration if(!topLevel) { // must be top-level; doesn't make sense to write something // like e.g. FORALL(x:INT = 4): [...] @@ -908,8 +909,9 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri i != i_end; ++i) { PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE); + Expr func = EXPR_MANAGER->mkVar(*i, f.getType()); PARSER_STATE->defineFunction(*i, f); - Command* decl = new DefineFunctionCommand(*i, Expr(), f); + Command* decl = new DefineFunctionCommand(*i, func, f); seq->addCommand(decl); } } 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() { |