From ca5ec6ea328417757aa4e393ed029b5ed2c76939 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Wed, 31 Mar 2010 20:45:31 +0000 Subject: [PATCH] More parser cleanup. Should fix problems with last commit. --- src/parser/cvc/Cvc.g | 59 +++++++++++++++++++++++++------------------- src/parser/input.cpp | 33 ------------------------- src/parser/input.h | 52 ++++---------------------------------- src/parser/smt/Smt.g | 55 +++++++++++++++++++++++------------------ 4 files changed, 69 insertions(+), 130 deletions(-) diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 84713fc59..f32da2eac 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -48,6 +48,7 @@ options { @parser::includes { #include "expr/command.h" +#include "parser/input.h" namespace CVC4 { class Expr; @@ -58,15 +59,21 @@ namespace CVC4 { #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" -#include "parser/cvc/cvc_input.h" +#include "parser/antlr_input.h" #include "util/output.h" #include using namespace CVC4; using namespace CVC4::parser; -#undef CVC_INPUT -#define CVC_INPUT ((CvcInput*)(PARSER->super)) +/* These need to be macros so they can refer to the PARSER macro, which will be defined + * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ +#undef ANTLR_INPUT +#define ANTLR_INPUT ((Input*)PARSER->super) +#undef EXPR_MANAGER +#define EXPR_MANAGER ANTLR_INPUT->getExprManager() +#undef MK_EXPR +#define MK_EXPR EXPR_MANAGER->mkExpr } /** @@ -98,7 +105,7 @@ command returns [CVC4::Command* cmd = 0] : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f); } | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f); } | CHECKSAT_TOK formula[f] SEMICOLON { cmd = new CheckSatCommand(f); } - | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(CVC_INPUT->getTrueExpr()); } + | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(MK_EXPR(CVC4::kind::TRUE)); } | PUSH_TOK SEMICOLON { cmd = new PushCommand(); } | POP_TOK SEMICOLON { cmd = new PopCommand(); } | declaration[cmd] @@ -126,9 +133,9 @@ declType[CVC4::Type*& t, std::vector& idList] Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl; } : /* A sort declaration (e.g., "T : TYPE") */ - TYPE_TOK { CVC_INPUT->newSorts(idList); t = CVC_INPUT->kindType(); } + TYPE_TOK { ANTLR_INPUT->newSorts(idList); t = ANTLR_INPUT->kindType(); } | /* A variable declaration */ - type[t] { CVC_INPUT->mkVars(idList,t); } + type[t] { ANTLR_INPUT->mkVars(idList,t); } ; /** @@ -145,13 +152,13 @@ type[CVC4::Type*& t] | /* Single-parameter function type */ baseType[t] { typeList.push_back(t); } ARROW_TOK baseType[t] - { t = CVC_INPUT->functionType(typeList,t); } + { t = ANTLR_INPUT->functionType(typeList,t); } | /* Multi-parameter function type */ LPAREN baseType[t] { typeList.push_back(t); } (COMMA baseType[t] { typeList.push_back(t); } )+ RPAREN ARROW_TOK baseType[t] - { t = CVC_INPUT->functionType(typeList,t); } + { t = ANTLR_INPUT->functionType(typeList,t); } ; /** @@ -179,7 +186,7 @@ identifier[std::string& id, CVC4::parser::SymbolType type] : IDENTIFIER { id = AntlrInput::tokenText($IDENTIFIER); - CVC_INPUT->checkDeclaration(id, check, type); } + ANTLR_INPUT->checkDeclaration(id, check, type); } ; /** @@ -191,7 +198,7 @@ baseType[CVC4::Type*& t] std::string id; Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl; } - : BOOLEAN_TOK { t = CVC_INPUT->booleanType(); } + : BOOLEAN_TOK { t = ANTLR_INPUT->booleanType(); } | typeSymbol[t] ; @@ -204,7 +211,7 @@ typeSymbol[CVC4::Type*& t] Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; } : identifier[id,CHECK_DECLARED,SYM_SORT] - { t = CVC_INPUT->getSort(id); } + { t = ANTLR_INPUT->getSort(id); } ; /** @@ -242,7 +249,7 @@ iffFormula[CVC4::Expr& f] : impliesFormula[f] ( IFF_TOK iffFormula[e] - { f = CVC_INPUT->mkExpr(CVC4::kind::IFF, f, e); } + { f = MK_EXPR(CVC4::kind::IFF, f, e); } )? ; @@ -256,7 +263,7 @@ impliesFormula[CVC4::Expr& f] } : orFormula[f] ( IMPLIES_TOK impliesFormula[e] - { f = CVC_INPUT->mkExpr(CVC4::kind::IMPLIES, f, e); } + { f = MK_EXPR(CVC4::kind::IMPLIES, f, e); } )? ; @@ -273,7 +280,7 @@ orFormula[CVC4::Expr& f] xorFormula[f] { exprs.push_back(f); } )* { if( exprs.size() > 0 ) { - f = CVC_INPUT->mkExpr(CVC4::kind::OR, exprs); + f = MK_EXPR(CVC4::kind::OR, exprs); } } ; @@ -288,7 +295,7 @@ xorFormula[CVC4::Expr& f] } : andFormula[f] ( XOR_TOK andFormula[e] - { f = CVC_INPUT->mkExpr(CVC4::kind::XOR,f, e); } + { f = MK_EXPR(CVC4::kind::XOR,f, e); } )* ; @@ -305,7 +312,7 @@ andFormula[CVC4::Expr& f] notFormula[f] { exprs.push_back(f); } )* { if( exprs.size() > 0 ) { - f = CVC_INPUT->mkExpr(CVC4::kind::AND, exprs); + f = MK_EXPR(CVC4::kind::AND, exprs); } } ; @@ -320,7 +327,7 @@ notFormula[CVC4::Expr& f] } : /* negation */ NOT_TOK notFormula[f] - { f = CVC_INPUT->mkExpr(CVC4::kind::NOT, f); } + { f = MK_EXPR(CVC4::kind::NOT, f); } | /* a boolean atom */ predFormula[f] ; @@ -332,7 +339,7 @@ predFormula[CVC4::Expr& f] } : term[f] (EQUAL_TOK term[e] - { f = CVC_INPUT->mkExpr(CVC4::kind::EQUAL, f, e); } + { f = MK_EXPR(CVC4::kind::EQUAL, f, e); } )? ; // TODO: lt, gt, etc. @@ -351,7 +358,7 @@ term[CVC4::Expr& f] { args.push_back( f ); } LPAREN formulaList[args] RPAREN // TODO: check arity - { f = CVC_INPUT->mkExpr(CVC4::kind::APPLY_UF, args); } + { f = MK_EXPR(CVC4::kind::APPLY_UF, args); } | /* if-then-else */ iteTerm[f] @@ -360,12 +367,12 @@ term[CVC4::Expr& f] LPAREN formula[f] RPAREN /* constants */ - | TRUE_TOK { f = CVC_INPUT->getTrueExpr(); } - | FALSE_TOK { f = CVC_INPUT->getFalseExpr(); } + | TRUE_TOK { f = MK_EXPR(CVC4::kind::TRUE); } + | FALSE_TOK { f = MK_EXPR(CVC4::kind::FALSE); } | /* variable */ identifier[name,CHECK_DECLARED,SYM_VARIABLE] - { f = CVC_INPUT->getVariable(name); } + { f = ANTLR_INPUT->getVariable(name); } ; /** @@ -380,7 +387,7 @@ iteTerm[CVC4::Expr& f] THEN_TOK formula[f] { args.push_back(f); } iteElseTerm[f] { args.push_back(f); } ENDIF_TOK - { f = CVC_INPUT->mkExpr(CVC4::kind::ITE, args); } + { f = MK_EXPR(CVC4::kind::ITE, args); } ; /** @@ -395,7 +402,7 @@ iteElseTerm[CVC4::Expr& f] | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); } THEN_TOK iteThen = formula[f] { args.push_back(f); } iteElse = iteElseTerm[f] { args.push_back(f); } - { f = CVC_INPUT->mkExpr(CVC4::kind::ITE, args); } + { f = MK_EXPR(CVC4::kind::ITE, args); } ; /** @@ -409,8 +416,8 @@ functionSymbol[CVC4::Expr& f] std::string name; } : identifier[name,CHECK_DECLARED,SYM_FUNCTION] - { CVC_INPUT->checkFunction(name); - f = CVC_INPUT->getFunction(name); } + { ANTLR_INPUT->checkFunction(name); + f = ANTLR_INPUT->getFunction(name); } ; diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 24ad93d05..06faf5106 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -209,39 +209,6 @@ bool Input::isPredicate(const std::string& name) { return isDeclared(name, SYM_FUNCTION) && getType(name)->isPredicate(); } -Expr Input::getTrueExpr() const { - return d_exprManager->mkExpr(TRUE); -} - -Expr Input::getFalseExpr() const { - return d_exprManager->mkExpr(FALSE); -} - -Expr Input::mkExpr(Kind kind, const Expr& child) { - Expr result = d_exprManager->mkExpr(kind, child); - Debug("parser") << "mkExpr() => " << result << std::endl; - return result; -} - -Expr Input::mkExpr(Kind kind, const Expr& child_1, const Expr& child_2) { - Expr result = d_exprManager->mkExpr(kind, child_1, child_2); - Debug("parser") << "mkExpr() => " << result << std::endl; - return result; -} - -Expr Input::mkExpr(Kind kind, const Expr& child_1, const Expr& child_2, - const Expr& child_3) { - Expr result = d_exprManager->mkExpr(kind, child_1, child_2, child_3); - Debug("parser") << "mkExpr() => " << result << std::endl; - return result; -} - -Expr Input::mkExpr(Kind kind, const std::vector& children) { - Expr result = d_exprManager->mkExpr(kind, children); - Debug("parser") << "mkExpr() => " << result << std::endl; - return result; -} - Type* Input::functionType(Type* domainType, Type* rangeType) { diff --git a/src/parser/input.h b/src/parser/input.h index af580d78e..42a94ab41 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -153,6 +153,11 @@ public: */ static Input* newStringParser(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name); + /** Get the ExprManager associated with this input. */ + inline ExprManager* getExprManager() const { + return d_exprManager; + } + /** * Parse the next command of the input. If EOF is encountered a EmptyCommand * is returned and done flag is set. @@ -258,53 +263,6 @@ public: Type* getType(const std::string& var_name, SymbolType type = SYM_VARIABLE); - /** - * Returns the true expression. - * @return the true expression - */ - Expr getTrueExpr() const; - - /** - * Returns the false expression. - * @return the false expression - */ - Expr getFalseExpr() const; - - /** - * Creates a new unary CVC4 expression using the expression manager. - * @param kind the kind of the expression - * @param child the child - * @return the new unary expression - */ - Expr mkExpr(Kind kind, const Expr& child); - - /** - * Creates a new binary CVC4 expression using the expression manager. - * @param kind the kind of the expression - * @param child1 the first child - * @param child2 the second child - * @return the new binary expression - */ - Expr mkExpr(Kind kind, const Expr& child_1, const Expr& child_2); - - /** - * Creates a new ternary CVC4 expression using the expression manager. - * @param kind the kind of the expression - * @param child_1 the first child - * @param child_2 the second child - * @param child_3 - * @return the new ternary expression - */ - Expr mkExpr(Kind kind, const Expr& child_1, const Expr& child_2, - const Expr& child_3); - - /** - * Creates a new CVC4 expression using the expression manager. - * @param kind the kind of the expression - * @param children the children of the expression - */ - Expr mkExpr(Kind kind, const std::vector& children); - /** Create a new CVC4 variable expression of the given type. */ Expr mkVar(const std::string& name, Type* type); diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index e97ced324..56bedce81 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -48,6 +48,7 @@ options { @parser::includes { #include "expr/command.h" +#include "parser/input.h" namespace CVC4 { class Expr; @@ -58,15 +59,21 @@ namespace CVC4 { #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" -#include "parser/smt/smt_input.h" +#include "parser/antlr_input.h" #include "util/output.h" #include using namespace CVC4; using namespace CVC4::parser; -#undef SMT_INPUT -#define SMT_INPUT ((SmtInput*)(PARSER->super)) +/* These need to be macros so they can refer to the PARSER macro, which will be defined + * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ +#undef ANTLR_INPUT +#define ANTLR_INPUT ((Input*)PARSER->super) +#undef EXPR_MANAGER +#define EXPR_MANAGER ANTLR_INPUT->getExprManager() +#undef MK_EXPR +#define MK_EXPR EXPR_MANAGER->mkExpr } /** @@ -120,7 +127,7 @@ benchAttribute returns [CVC4::Command* smt_command] Expr expr; } : LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE] - { SMT_INPUT->setLogic(name); + { ANTLR_INPUT->setLogic(name); smt_command = new SetBenchmarkLogicCommand(name); } | ASSUMPTION_TOK annotatedFormula[expr] { smt_command = new AssertCommand(expr); } @@ -148,13 +155,13 @@ annotatedFormula[CVC4::Expr& expr] } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK - { SMT_INPUT->checkArity(kind, args.size()); + { ANTLR_INPUT->checkArity(kind, args.size()); if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) { /* Unary AND/OR can be replaced with the argument. It just so happens expr should already by the only argument. */ Assert( expr == args[0] ); } else { - expr = SMT_INPUT->mkExpr(kind, args); + expr = MK_EXPR(kind, args); } } @@ -169,7 +176,7 @@ annotatedFormula[CVC4::Expr& expr] { args.push_back(expr); } annotatedFormulas[args,expr] RPAREN_TOK // TODO: check arity - { expr = SMT_INPUT->mkExpr(CVC4::kind::APPLY_UF,args); } + { expr = MK_EXPR(CVC4::kind::APPLY_UF,args); } | /* An ite expression */ LPAREN_TOK (ITE_TOK | IF_THEN_ELSE_TOK) @@ -180,27 +187,27 @@ annotatedFormula[CVC4::Expr& expr] annotatedFormula[expr] { args.push_back(expr); } RPAREN_TOK - { expr = SMT_INPUT->mkExpr(CVC4::kind::ITE, args); } + { expr = MK_EXPR(CVC4::kind::ITE, args); } | /* a let/flet binding */ LPAREN_TOK (LET_TOK LPAREN_TOK var_identifier[name,CHECK_UNDECLARED] | FLET_TOK LPAREN_TOK fun_identifier[name,CHECK_UNDECLARED] ) annotatedFormula[expr] RPAREN_TOK - { SMT_INPUT->defineVar(name,expr); } + { ANTLR_INPUT->defineVar(name,expr); } annotatedFormula[expr] RPAREN_TOK - { SMT_INPUT->undefineVar(name); } + { ANTLR_INPUT->undefineVar(name); } | /* a variable */ ( identifier[name,CHECK_DECLARED,SYM_VARIABLE] | var_identifier[name,CHECK_DECLARED] | fun_identifier[name,CHECK_DECLARED] ) - { expr = SMT_INPUT->getVariable(name); } + { expr = ANTLR_INPUT->getVariable(name); } /* constants */ - | TRUE_TOK { expr = SMT_INPUT->getTrueExpr(); } - | FALSE_TOK { expr = SMT_INPUT->getFalseExpr(); } + | TRUE_TOK { expr = MK_EXPR(CVC4::kind::TRUE); } + | FALSE_TOK { expr = MK_EXPR(CVC4::kind::FALSE); } /* TODO: let, flet, quantifiers, arithmetic constants */ ; @@ -259,8 +266,8 @@ functionSymbol[CVC4::Expr& fun] std::string name; } : functionName[name,CHECK_DECLARED] - { SMT_INPUT->checkFunction(name); - fun = SMT_INPUT->getFunction(name); } + { ANTLR_INPUT->checkFunction(name); + fun = ANTLR_INPUT->getFunction(name); } ; /** @@ -281,8 +288,8 @@ functionDeclaration t = sortSymbol // require at least one sort { sorts.push_back(t); } sortList[sorts] RPAREN_TOK - { t = SMT_INPUT->functionType(sorts); - SMT_INPUT->mkVar(name, t); } + { t = ANTLR_INPUT->functionType(sorts); + ANTLR_INPUT->mkVar(name, t); } ; /** @@ -294,8 +301,8 @@ predicateDeclaration std::vector p_sorts; } : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK - { Type *t = SMT_INPUT->predicateType(p_sorts); - SMT_INPUT->mkVar(name, t); } + { Type *t = ANTLR_INPUT->predicateType(p_sorts); + ANTLR_INPUT->mkVar(name, t); } ; sortDeclaration @@ -304,7 +311,7 @@ sortDeclaration } : sortName[name,CHECK_UNDECLARED] { Debug("parser") << "sort decl: '" << name << "'" << std::endl; - SMT_INPUT->newSort(name); } + ANTLR_INPUT->newSort(name); } ; /** @@ -327,7 +334,7 @@ sortSymbol returns [CVC4::Type* t] std::string name; } : sortName[name,CHECK_NONE] - { $t = SMT_INPUT->getSort(name); } + { $t = ANTLR_INPUT->getSort(name); } ; /** @@ -360,7 +367,7 @@ identifier[std::string& id, Debug("parser") << "identifier: " << id << " check? " << toString(check) << " type? " << toString(type) << std::endl; - SMT_INPUT->checkDeclaration(id, check, type); } + ANTLR_INPUT->checkDeclaration(id, check, type); } ; /** @@ -374,7 +381,7 @@ var_identifier[std::string& id, { id = AntlrInput::tokenText($VAR_IDENTIFIER); Debug("parser") << "var_identifier: " << id << " check? " << toString(check) << std::endl; - SMT_INPUT->checkDeclaration(id, check, SYM_VARIABLE); } + ANTLR_INPUT->checkDeclaration(id, check, SYM_VARIABLE); } ; /** @@ -388,7 +395,7 @@ fun_identifier[std::string& id, { id = AntlrInput::tokenText($FUN_IDENTIFIER); Debug("parser") << "fun_identifier: " << id << " check? " << toString(check) << std::endl; - SMT_INPUT->checkDeclaration(id, check, SYM_FUNCTION); } + ANTLR_INPUT->checkDeclaration(id, check, SYM_FUNCTION); } ; -- 2.30.2