diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 8 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 24 |
2 files changed, 29 insertions, 3 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 21f82f638..55e10724b 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -942,7 +942,7 @@ 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()); + Expr func = EXPR_MANAGER->mkVar(*i, t); PARSER_STATE->defineFunction(*i, f); Command* decl = new DefineFunctionCommand(*i, func, f); seq->addCommand(decl); @@ -2094,6 +2094,12 @@ NUMBER_OR_RANGEOP ) ; +// these empty fragments remove "no lexer rule corresponding to token" warnings +fragment INTEGER_LITERAL:; +fragment DECIMAL_LITERAL:; +fragment DOT:; +fragment DOTDOT:; + /** * Matches the hexidecimal digits (0-9, a-f, A-F) */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 07998b58f..84d75ceac 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -115,7 +115,11 @@ namespace CVC4 { #include "util/integer.h" #include "util/output.h" #include "util/rational.h" +#include "util/hash.h" #include <vector> +#include <set> +#include <string> +#include <sstream> using namespace CVC4; using namespace CVC4::parser; @@ -439,6 +443,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] std::string attr; Expr attexpr; std::vector<Expr> attexprs; + std::hash_set<std::string, StringHashFunction> names; + std::vector< std::pair<std::string, Expr> > binders; } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK @@ -540,8 +546,22 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | /* a let binding */ LPAREN_TOK LET_TOK LPAREN_TOK { PARSER_STATE->pushScope(); } - ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[expr, f2] RPAREN_TOK - { PARSER_STATE->defineVar(name,expr); } )+ + ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] term[expr, f2] RPAREN_TOK + // this is a parallel let, so we have to save up all the contributions + // of the let and define them only later on + { if(names.count(name) == 1) { + std::stringstream ss; + ss << "warning: symbol `" << name << "' bound multiple times by let; the last binding will be used, shadowing earlier ones"; + PARSER_STATE->warning(ss.str()); + } else { + names.insert(name); + } + binders.push_back(std::make_pair(name, expr)); } )+ + { // now implement these bindings + for(std::vector< std::pair<std::string, Expr> >::iterator i = binders.begin(); i != binders.end(); ++i) { + PARSER_STATE->defineVar((*i).first, (*i).second); + } + } RPAREN_TOK term[expr, f2] RPAREN_TOK |