From: Christopher L. Conway Date: Wed, 31 Mar 2010 23:07:12 +0000 (+0000) Subject: Finishing parser cleanup. Code is now review-ready. X-Git-Tag: cvc5-1.0.0~9156 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1b054a43b2f5d6725eae8ef8677ae34cbe749e57;p=cvc5.git Finishing parser cleanup. Code is now review-ready. --- diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 0b0139118..4eda9805a 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -20,15 +20,17 @@ * Author: dejan */ -#include "expr/node.h" +#include "context/context.h" #include "expr/expr.h" -#include "expr/type.h" -#include "expr/node_manager.h" #include "expr/expr_manager.h" -#include "context/context.h" +#include "expr/kind.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "expr/type.h" using namespace std; using namespace CVC4::context; +using namespace CVC4::kind; namespace CVC4 { @@ -115,10 +117,25 @@ FunctionType* ExprManager::mkFunctionType(Type* domain, /** Make a function type with input types from argTypes. */ FunctionType* ExprManager::mkFunctionType(const std::vector& argTypes, Type* range) { + Assert( argTypes.size() >= 1 ); NodeManagerScope nms(d_nodeManager); return d_nodeManager->mkFunctionType(argTypes, range); } +FunctionType* +ExprManager::mkFunctionType(const std::vector& sorts) { + Assert( sorts.size() >= 2 ); + NodeManagerScope nms(d_nodeManager); + return d_nodeManager->mkFunctionType(sorts); +} + +FunctionType* +ExprManager::mkPredicateType(const std::vector& sorts) { + Assert( sorts.size() >= 1 ); + NodeManagerScope nms(d_nodeManager); + return d_nodeManager->mkPredicateType(sorts); +} + Type* ExprManager::mkSort(const std::string& name) { NodeManagerScope nms(d_nodeManager); return d_nodeManager->mkSort(name); @@ -134,6 +151,69 @@ Expr ExprManager::mkVar(Type* type) { return Expr(this, new Node(d_nodeManager->mkVar(type))); } +unsigned int ExprManager::minArity(Kind kind) { + switch(kind) { + case FALSE: + case SKOLEM: + case TRUE: + case VARIABLE: + return 0; + + case AND: + case NOT: + case OR: + return 1; + + case APPLY_UF: + case DISTINCT: + case EQUAL: + case IFF: + case IMPLIES: + case PLUS: + case XOR: + return 2; + + case ITE: + return 3; + + default: + Unhandled(kind); + } +} + +unsigned int ExprManager::maxArity(Kind kind) { + switch(kind) { + case FALSE: + case SKOLEM: + case TRUE: + case VARIABLE: + return 0; + + case NOT: + return 1; + + case EQUAL: + case IFF: + case IMPLIES: + case XOR: + return 2; + + case ITE: + return 3; + + case AND: + case APPLY_UF: + case DISTINCT: + case PLUS: + case OR: + return UINT_MAX; + + default: + Unhandled(kind); + } +} + + NodeManager* ExprManager::getNodeManager() const { return d_nodeManager; } diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 3c73e1ced..f2009ad80 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -99,11 +99,26 @@ public: mkFunctionType(Type* domain, Type* range); - /** Make a function type with input types from argTypes. */ + /** Make a function type with input types from argTypes. argTypes + * must have at least one element. */ FunctionType* mkFunctionType(const std::vector& argTypes, Type* range); + /** Make a function type with input types from sorts[0..sorts.size()-2] + * and result type sorts[sorts.size()-1]. sorts must have at + * least 2 elements. + */ + FunctionType* + mkFunctionType(const std::vector& sorts); + + /** Make a predicate type with input types from sorts. The result with + * be a function type with range BOOLEAN. sorts must have at + * least one element. + */ + FunctionType* + mkPredicateType(const std::vector& sorts); + /** Make a new sort with the given name. */ Type* mkSort(const std::string& name); @@ -111,6 +126,12 @@ public: Expr mkVar(Type* type, const std::string& name); Expr mkVar(Type* type); + /** Returns the minimum arity of the given kind. */ + static unsigned int minArity(Kind kind); + + /** Returns the maximum arity of the given kind. */ + static unsigned int maxArity(Kind kind); + private: /** The context */ context::Context* d_ctxt; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index c51c7fb77..f2718a06c 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -293,10 +293,25 @@ public: /** Make a function type from domain to range. */ inline FunctionType* mkFunctionType(Type* domain, Type* range) const; - /** Make a function type with input types from argTypes. */ + /** Make a function type with input types from argTypes. argTypes + * must have at least one element. */ inline FunctionType* mkFunctionType(const std::vector& argTypes, Type* range) const; + /** Make a function type with input types from sorts[0..sorts.size()-2] + * and result type sorts[sorts.size()-1]. sorts must have at + * least 2 elements. + */ + inline FunctionType* + mkFunctionType(const std::vector& sorts); + + /** Make a predicate type with input types from sorts. The result with + * be a function type with range BOOLEAN. sorts must have at + * least one element. + */ + inline FunctionType* + mkPredicateType(const std::vector& sorts); + /** Make a new sort with the given name. */ inline Type* mkSort(const std::string& name) const; @@ -437,6 +452,20 @@ NodeManager::mkFunctionType(const std::vector& argTypes, return new FunctionType(argTypes, range); } +inline FunctionType* +NodeManager::mkFunctionType(const std::vector& sorts) { + Assert( sorts.size() >= 2 ); + std::vector argTypes(sorts); + Type* rangeType = argTypes.back(); + argTypes.pop_back(); + return mkFunctionType(argTypes,rangeType); +} + +inline FunctionType* +NodeManager::mkPredicateType(const std::vector& sorts) { + Assert( sorts.size() >= 1 ); + return mkFunctionType(sorts,booleanType()); +} inline Type* NodeManager::mkSort(const std::string& name) const { return new SortType(name); } diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index f32da2eac..4cb4d577b 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -133,7 +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 { ANTLR_INPUT->newSorts(idList); t = ANTLR_INPUT->kindType(); } + TYPE_TOK + { ANTLR_INPUT->newSorts(idList); + t = EXPR_MANAGER->kindType(); } | /* A variable declaration */ type[t] { ANTLR_INPUT->mkVars(idList,t); } ; @@ -144,21 +146,21 @@ declType[CVC4::Type*& t, std::vector& idList] */ type[CVC4::Type*& t] @init { + Type* t2; std::vector typeList; Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl; } : /* Simple type */ baseType[t] | /* Single-parameter function type */ - baseType[t] { typeList.push_back(t); } - ARROW_TOK baseType[t] - { t = ANTLR_INPUT->functionType(typeList,t); } + baseType[t] ARROW_TOK baseType[t2] + { t = EXPR_MANAGER->mkFunctionType(t,t2); } | /* Multi-parameter function type */ LPAREN baseType[t] { typeList.push_back(t); } (COMMA baseType[t] { typeList.push_back(t); } )+ RPAREN ARROW_TOK baseType[t] - { t = ANTLR_INPUT->functionType(typeList,t); } + { t = EXPR_MANAGER->mkFunctionType(typeList,t); } ; /** @@ -198,7 +200,7 @@ baseType[CVC4::Type*& t] std::string id; Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl; } - : BOOLEAN_TOK { t = ANTLR_INPUT->booleanType(); } + : BOOLEAN_TOK { t = EXPR_MANAGER->booleanType(); } | typeSymbol[t] ; @@ -415,9 +417,9 @@ functionSymbol[CVC4::Expr& f] Debug("parser-extra") << "function symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; std::string name; } - : identifier[name,CHECK_DECLARED,SYM_FUNCTION] + : identifier[name,CHECK_DECLARED,SYM_VARIABLE] { ANTLR_INPUT->checkFunction(name); - f = ANTLR_INPUT->getFunction(name); } + f = ANTLR_INPUT->getVariable(name); } ; diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 06faf5106..01de4ea4f 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -163,7 +163,6 @@ Expr Input::getSymbol(const std::string& name, SymbolType type) { switch( type ) { case SYM_VARIABLE: // Functions share var namespace - case SYM_FUNCTION: return d_varSymbolTable.getObject(name); default: @@ -176,10 +175,6 @@ Expr Input::getVariable(const std::string& name) { return getSymbol(name, SYM_VARIABLE); } -Expr Input::getFunction(const std::string& name) { - return getSymbol(name, SYM_FUNCTION); -} - Type* Input::getType(const std::string& var_name, SymbolType type) { @@ -201,46 +196,12 @@ bool Input::isBoolean(const std::string& name) { /* Returns true if name is bound to a function. */ bool Input::isFunction(const std::string& name) { - return isDeclared(name, SYM_FUNCTION) && getType(name)->isFunction(); + return isDeclared(name, SYM_VARIABLE) && getType(name)->isFunction(); } /* Returns true if name is bound to a function returning boolean. */ bool Input::isPredicate(const std::string& name) { - return isDeclared(name, SYM_FUNCTION) && getType(name)->isPredicate(); -} - -Type* -Input::functionType(Type* domainType, - Type* rangeType) { - return d_exprManager->mkFunctionType(domainType,rangeType); -} - -Type* -Input::functionType(const std::vector& argTypes, - Type* rangeType) { - Assert( argTypes.size() > 0 ); - return d_exprManager->mkFunctionType(argTypes,rangeType); -} - -Type* -Input::functionType(const std::vector& sorts) { - Assert( sorts.size() > 0 ); - if( sorts.size() == 1 ) { - return sorts[0]; - } else { - std::vector argTypes(sorts); - Type* rangeType = argTypes.back(); - argTypes.pop_back(); - return functionType(argTypes,rangeType); - } -} - -Type* Input::predicateType(const std::vector& sorts) { - if(sorts.size() == 0) { - return d_exprManager->booleanType(); - } else { - return d_exprManager->mkFunctionType(sorts, d_exprManager->booleanType()); - } + return isDeclared(name, SYM_VARIABLE) && getType(name)->isPredicate(); } Expr @@ -303,80 +264,9 @@ Input::newSorts(const std::vector& names) { return types; } -BooleanType* Input::booleanType() { - return d_exprManager->booleanType(); -} - -KindType* Input::kindType() { - return d_exprManager->kindType(); -} - -unsigned int Input::minArity(Kind kind) { - switch(kind) { - case FALSE: - case SKOLEM: - case TRUE: - case VARIABLE: - return 0; - - case AND: - case NOT: - case OR: - return 1; - - case APPLY_UF: - case DISTINCT: - case EQUAL: - case IFF: - case IMPLIES: - case PLUS: - case XOR: - return 2; - - case ITE: - return 3; - - default: - Unhandled(kind); - } -} - -unsigned int Input::maxArity(Kind kind) { - switch(kind) { - case FALSE: - case SKOLEM: - case TRUE: - case VARIABLE: - return 0; - - case NOT: - return 1; - - case EQUAL: - case IFF: - case IMPLIES: - case XOR: - return 2; - - case ITE: - return 3; - - case AND: - case APPLY_UF: - case DISTINCT: - case PLUS: - case OR: - return UINT_MAX; - - default: - Unhandled(kind); - } -} - bool Input::isDeclared(const std::string& name, SymbolType type) { switch(type) { - case SYM_VARIABLE: // Functions share var namespace - case SYM_FUNCTION: + case SYM_VARIABLE: return d_varSymbolTable.isBound(name); case SYM_SORT: return d_sortTable.isBound(name); @@ -427,8 +317,8 @@ void Input::checkArity(Kind kind, unsigned int numArgs) return; } - unsigned int min = minArity(kind); - unsigned int max = maxArity(kind); + unsigned int min = d_exprManager->minArity(kind); + unsigned int max = d_exprManager->maxArity(kind); if( numArgs < min || numArgs > max ) { stringstream ss; diff --git a/src/parser/input.h b/src/parser/input.h index 42a94ab41..90cdc4e8d 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -66,8 +66,6 @@ inline std::string toString(DeclarationCheck check) { enum SymbolType { /** Variables */ SYM_VARIABLE, - /** Functions */ - SYM_FUNCTION, /** Sorts */ SYM_SORT }; @@ -77,7 +75,6 @@ enum SymbolType { inline std::string toString(SymbolType type) { switch(type) { case SYM_VARIABLE: return "SYM_VARIABLE"; - case SYM_FUNCTION: return "SYM_FUNCTION"; case SYM_SORT: return "SYM_SORT"; default: Unreachable(); } @@ -206,13 +203,6 @@ public: */ Expr getVariable(const std::string& var_name); - /** - * Returns a function, given a name and a type. - * @param name the name of the function - * @return the function expression - */ - Expr getFunction(const std::string& name); - /** * Returns a sort, given a name */ @@ -278,30 +268,6 @@ public: /** Remove a variable definition (e.g., from a let binding). */ void undefineVar(const std::string& name); - /** Returns a function type over the given domain and range types. */ - Type* functionType(Type* domain, Type* range); - - /** Returns a function type over the given types. argTypes must be - non-empty. */ - Type* functionType(const std::vector& argTypes, - Type* rangeType); - - /** - * Returns a function type over the given types. If types has only - * one element, then the type is just types[0]. - * - * @param types a non-empty list of input and output types. - */ - Type* functionType(const std::vector& types); - - /** - * Returns a predicate type over the given sorts. If sorts is empty, - * then the type is just BOOLEAN. - - * @param sorts a list of input types - */ - Type* predicateType(const std::vector& sorts); - /** * Creates a new sort with the given name. */ @@ -322,18 +288,6 @@ public: /** Is the symbol bound to a predicate? */ bool isPredicate(const std::string& name); - /** Returns the boolean type. */ - BooleanType* booleanType(); - - /** Returns the kind type (i.e., the type of types). */ - KindType* kindType(); - - /** Returns the minimum arity of the given kind. */ - static unsigned int minArity(Kind kind); - - /** Returns the maximum arity of the given kind. */ - static unsigned int maxArity(Kind kind); - /** Throws a ParserException with the given error message. * Implementations should fill in the ParserException with * line number information, etc. */ diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 56bedce81..d03cbf47e 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -255,7 +255,7 @@ predicateName[std::string& name, CVC4::parser::DeclarationCheck check] * @param check what kind of check to do with the symbol */ functionName[std::string& name, CVC4::parser::DeclarationCheck check] - : identifier[name,check,SYM_FUNCTION] + : identifier[name,check,SYM_VARIABLE] ; /** @@ -267,7 +267,7 @@ functionSymbol[CVC4::Expr& fun] } : functionName[name,CHECK_DECLARED] { ANTLR_INPUT->checkFunction(name); - fun = ANTLR_INPUT->getFunction(name); } + fun = ANTLR_INPUT->getVariable(name); } ; /** @@ -277,8 +277,6 @@ attribute : ATTR_IDENTIFIER ; - - functionDeclaration @declarations { std::string name; @@ -288,7 +286,11 @@ functionDeclaration t = sortSymbol // require at least one sort { sorts.push_back(t); } sortList[sorts] RPAREN_TOK - { t = ANTLR_INPUT->functionType(sorts); + { if( sorts.size() == 1 ) { + Assert( t == sorts[0] ); + } else { + t = EXPR_MANAGER->mkFunctionType(sorts); + } ANTLR_INPUT->mkVar(name, t); } ; @@ -301,7 +303,12 @@ predicateDeclaration std::vector p_sorts; } : LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK - { Type *t = ANTLR_INPUT->predicateType(p_sorts); + { Type *t; + if( p_sorts.empty() ) { + t = EXPR_MANAGER->booleanType(); + } else { + t = EXPR_MANAGER->mkPredicateType(p_sorts); + } ANTLR_INPUT->mkVar(name, t); } ; @@ -395,7 +402,7 @@ fun_identifier[std::string& id, { id = AntlrInput::tokenText($FUN_IDENTIFIER); Debug("parser") << "fun_identifier: " << id << " check? " << toString(check) << std::endl; - ANTLR_INPUT->checkDeclaration(id, check, SYM_FUNCTION); } + ANTLR_INPUT->checkDeclaration(id, check); } ; diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index b7c58ba99..6e2adb356 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -27,27 +27,6 @@ using namespace CVC4; using namespace CVC4::parser; using namespace std; -/* Set up declaration context for expr inputs */ - -void setupContext(Input* input) { - /* a, b, c: BOOLEAN */ - input->mkVar("a",(Type*)input->booleanType()); - input->mkVar("b",(Type*)input->booleanType()); - input->mkVar("c",(Type*)input->booleanType()); - /* t, u, v: TYPE */ - Type *t = input->newSort("t"); - Type *u = input->newSort("u"); - Type *v = input->newSort("v"); - /* f : t->u; g: u->v; h: v->t; */ - input->mkVar("f", input->functionType(t,u)); - input->mkVar("g", input->functionType(u,v)); - input->mkVar("h", input->functionType(v,t)); - /* x:t; y:u; z:v; */ - input->mkVar("x",t); - input->mkVar("y",u); - input->mkVar("z",v); -} - /************************** CVC test inputs ********************************/ @@ -162,6 +141,27 @@ const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); class ParserBlack : public CxxTest::TestSuite { ExprManager *d_exprManager; + /* Set up declaration context for expr inputs */ + + void setupContext(Input* input) { + /* a, b, c: BOOLEAN */ + input->mkVar("a",(Type*)d_exprManager->booleanType()); + input->mkVar("b",(Type*)d_exprManager->booleanType()); + input->mkVar("c",(Type*)d_exprManager->booleanType()); + /* t, u, v: TYPE */ + Type *t = input->newSort("t"); + Type *u = input->newSort("u"); + Type *v = input->newSort("v"); + /* f : t->u; g: u->v; h: v->t; */ + input->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u)); + input->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v)); + input->mkVar("h", (Type*)d_exprManager->mkFunctionType(v,t)); + /* x:t; y:u; z:v; */ + input->mkVar("x",t); + input->mkVar("y",u); + input->mkVar("z",v); + } + void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) { for(int i = 0; i < numInputs; ++i) { try {