diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-24 14:41:28 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-24 14:41:28 +0200 |
| commit | 349deb0522c4602b740d96f6a688b644dd84c64f (patch) | |
| tree | 9dadc1818f91082fec548ae1c04bcceea26ab95c /src/parser/smt2 | |
| parent | b09cdf3e0f407c69c8df8023b70c776d1b0a4589 (diff) | |
More parser related bug fixes (define-funs-rec, declare-funs). Bug fix for fmf mbqi=gen-ev for interpreted operators.
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d2e83702f..c7c82b2d8 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -912,7 +912,8 @@ smt25Command[CVC4::Command*& cmd] } t = EXPR_MANAGER->mkFunctionType(sorts, t); } - Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_DEFINED); + Expr func = PARSER_STATE->mkVar(fname, t); + static_cast<CommandSequence*>($cmd)->addCommand(new DeclareFunctionCommand(fname, func, t)); std::vector< Expr > f_app; f_app.push_back( func ); PARSER_STATE->pushScope(true); @@ -958,7 +959,8 @@ smt25Command[CVC4::Command*& cmd] t = EXPR_MANAGER->mkFunctionType(sorts, t); } sortedVarNames.clear(); - Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_DEFINED); + Expr func = PARSER_STATE->mkVar(fname, t); + static_cast<CommandSequence*>($cmd)->addCommand(new DeclareFunctionCommand(fname, func, t)); funcs.push_back( func ); } RPAREN_TOK @@ -1079,6 +1081,7 @@ extendedCommand[CVC4::Command*& cmd] } Expr func = PARSER_STATE->mkVar(name, t); static_cast<CommandSequence*>($cmd)->addCommand(new DeclareFunctionCommand(name, func, t)); + sorts.clear(); } )+ RPAREN_TOK @@ -1098,6 +1101,7 @@ extendedCommand[CVC4::Command*& cmd] } Expr func = PARSER_STATE->mkVar(name, t); static_cast<CommandSequence*>($cmd)->addCommand(new DeclareFunctionCommand(name, func, t)); + sorts.clear(); } )+ RPAREN_TOK |