diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-31 23:07:12 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-03-31 23:07:12 +0000 |
commit | 1b054a43b2f5d6725eae8ef8677ae34cbe749e57 (patch) | |
tree | 1c08ad4ffccb80041d26b17938764a86a94cfcce /src/parser/input.cpp | |
parent | ca5ec6ea328417757aa4e393ed029b5ed2c76939 (diff) |
Finishing parser cleanup. Code is now review-ready.
Diffstat (limited to 'src/parser/input.cpp')
-rw-r--r-- | src/parser/input.cpp | 120 |
1 files changed, 5 insertions, 115 deletions
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<Type*>& argTypes, - Type* rangeType) { - Assert( argTypes.size() > 0 ); - return d_exprManager->mkFunctionType(argTypes,rangeType); -} - -Type* -Input::functionType(const std::vector<Type*>& sorts) { - Assert( sorts.size() > 0 ); - if( sorts.size() == 1 ) { - return sorts[0]; - } else { - std::vector<Type*> argTypes(sorts); - Type* rangeType = argTypes.back(); - argTypes.pop_back(); - return functionType(argTypes,rangeType); - } -} - -Type* Input::predicateType(const std::vector<Type*>& 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<std::string>& 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; |