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/parser | |
| parent | ee64b3fa49a22b89ffb3e62d8d7144fc9b99754e (diff) | |
minor fixes to printing and parsing of CVC-language defined functions and lambdas; resolves bug 294
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 4 |
1 files changed, 3 insertions, 1 deletions
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); } } |