diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 4 | ||||
-rw-r--r-- | src/parser/parser.cpp | 17 | ||||
-rw-r--r-- | src/parser/parser.h | 3 | ||||
-rw-r--r-- | src/parser/smt/Smt.g | 2 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 6 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 4 |
6 files changed, 24 insertions, 12 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 05fed15ea..3c4a51ad4 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1254,14 +1254,14 @@ prefixFormula[CVC4::Expr& f] { PARSER_STATE->pushScope(); } LPAREN boundVarDecl[ids,t] { for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) { - bvs.push_back(PARSER_STATE->mkVar(*i, t)); + bvs.push_back(PARSER_STATE->mkBoundVar(*i, t)); } ids.clear(); } ( COMMA boundVarDecl[ids,t] { for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) { - bvs.push_back(PARSER_STATE->mkVar(*i, t)); + bvs.push_back(PARSER_STATE->mkBoundVar(*i, t)); } ids.clear(); } diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 29db640c7..bf7c372b7 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -150,6 +150,14 @@ Parser::mkVar(const std::string& name, const Type& type, } Expr +Parser::mkBoundVar(const std::string& name, const Type& type) { + Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; + Expr expr = d_exprManager->mkBoundVar(name, type); + defineVar(name, expr, false); + return expr; +} + +Expr Parser::mkFunction(const std::string& name, const Type& type, bool levelZero) { Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; @@ -178,7 +186,8 @@ Parser::mkVars(const std::vector<std::string> names, void Parser::defineVar(const std::string& name, const Expr& val, - bool levelZero) { + bool levelZero) { + Debug("parser") << "defineVar( " << name << " := " << val << " , " << levelZero << ")" << std::endl;; d_symtab->bind(name, val, levelZero); Assert( isDeclared(name) ); } @@ -300,14 +309,14 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { Expr::printtypes::Scope pts(Debug("parser-idt"), true); Expr constructor = ctor.getConstructor(); Debug("parser-idt") << "+ define " << constructor << std::endl; - string constructorName = constructor.toString(); + string constructorName = ctor.getName(); if(isDeclared(constructorName, SYM_VARIABLE)) { throw ParserException(constructorName + " already declared"); } defineVar(constructorName, constructor); Expr tester = ctor.getTester(); Debug("parser-idt") << "+ define " << tester << std::endl; - string testerName = tester.toString(); + string testerName = ctor.getTesterName(); if(isDeclared(testerName, SYM_VARIABLE)) { throw ParserException(testerName + " already declared"); } @@ -318,7 +327,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { ++k) { Expr selector = (*k).getSelector(); Debug("parser-idt") << "+++ define " << selector << std::endl; - string selectorName = selector.toString(); + string selectorName = (*k).getName(); if(isDeclared(selectorName, SYM_VARIABLE)) { throw ParserException(selectorName + " already declared"); } diff --git a/src/parser/parser.h b/src/parser/parser.h index f3210ae29..7efc4d78c 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -347,6 +347,9 @@ public: mkVars(const std::vector<std::string> names, const Type& type, bool levelZero = false); + /** Create a new CVC4 bound variable expression of the given type. */ + Expr mkBoundVar(const std::string& name, const Type& type); + /** Create a new CVC4 function expression of the given type. */ Expr mkFunction(const std::string& name, const Type& type, bool levelZero = false); diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index f9c38385f..0298497e9 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -253,7 +253,7 @@ annotatedFormula[CVC4::Expr& expr] ( FORALL_TOK { kind = kind::FORALL; } | EXISTS_TOK { kind = kind::EXISTS; } ) { PARSER_STATE->pushScope(); } ( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK - { args.push_back(PARSER_STATE->mkVar(name, t)); } + { args.push_back(PARSER_STATE->mkBoundVar(name, t)); } )+ annotatedFormula[expr] RPAREN_TOK { args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) ); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 456e3c656..d8157acbc 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -407,7 +407,7 @@ rewriterulesCommand[CVC4::Command*& cmd] sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { - args.push_back(PARSER_STATE->mkVar((*i).first, (*i).second)); + args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); } bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); } @@ -448,7 +448,7 @@ rewriterulesCommand[CVC4::Command*& cmd] sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { - args.push_back(PARSER_STATE->mkVar((*i).first, (*i).second)); + args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); } bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); } @@ -597,7 +597,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { - args.push_back(PARSER_STATE->mkVar((*i).first, (*i).second)); + args.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); } Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args); args.clear(); diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 63774a087..068e92cd7 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -327,7 +327,7 @@ variable[CVC4::Expr & expr] if(!PARSER_STATE->cnf || PARSER_STATE->isDeclared(name)){ expr = PARSER_STATE->getVariable(name); } else { - expr = PARSER_STATE->mkVar(name, PARSER_STATE->d_unsorted); + expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted); if(PARSER_STATE->cnf) PARSER_STATE->addFreeVar(expr); } } @@ -402,7 +402,7 @@ bindvariable[CVC4::Expr & expr] : UPPER_WORD { std::string name = AntlrInput::tokenText($UPPER_WORD); - expr = PARSER_STATE->mkVar(name, PARSER_STATE->d_unsorted); + expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted); } ; |