diff options
Diffstat (limited to 'src/parser/parser.cpp')
-rw-r--r-- | src/parser/parser.cpp | 82 |
1 files changed, 61 insertions, 21 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 39f61c16d..297a2d804 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -66,11 +66,15 @@ Expr Parser::getVariable(const std::string& name) { return getSymbol(name, SYM_VARIABLE); } +Expr Parser::getFunction(const std::string& name) { + return getSymbol(name, SYM_VARIABLE); +} + Type Parser::getType(const std::string& var_name, SymbolType type) { Assert( isDeclared(var_name, type) ); - Type t = getSymbol(var_name,type).getType(); + Type t = getSymbol(var_name, type).getType(); return t; } @@ -83,8 +87,7 @@ Type Parser::getSort(const std::string& name) { Type Parser::getSort(const std::string& name, const std::vector<Type>& params) { Assert( isDeclared(name, SYM_SORT) ); - Type t = d_declScope.lookupType(name); - Warning() << "FIXME use params to realize parameterized sort\n"; + Type t = d_declScope.lookupType(name, params); return t; } @@ -98,6 +101,11 @@ bool Parser::isFunction(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isFunction(); } +/* Returns true if name is bound to a defined function. */ +bool Parser::isDefinedFunction(const std::string& name) { + return isFunction(name) && d_declScope.isBoundDefinedFunction(name); +} + /* Returns true if name is bound to a function returning boolean. */ bool Parser::isPredicate(const std::string& name) { return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate(); @@ -105,32 +113,54 @@ bool Parser::isPredicate(const std::string& name) { Expr Parser::mkVar(const std::string& name, const Type& type) { - Debug("parser") << "mkVar(" << name << "," << type << ")" << std::endl; + Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; Expr expr = d_exprManager->mkVar(name, type); - defineVar(name,expr); + defineVar(name, expr); + return expr; +} + +Expr +Parser::mkFunction(const std::string& name, const Type& type) { + Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl; + Expr expr = d_exprManager->mkVar(name, type); + defineFunction(name, expr); return expr; } const std::vector<Expr> Parser::mkVars(const std::vector<std::string> names, - const Type& type) { + const Type& type) { std::vector<Expr> vars; for(unsigned i = 0; i < names.size(); ++i) { - vars.push_back(mkVar(names[i],type)); + vars.push_back(mkVar(names[i], type)); } return vars; } void Parser::defineVar(const std::string& name, const Expr& val) { - d_declScope.bind(name,val); - Assert(isDeclared(name)); + d_declScope.bind(name, val); + Assert( isDeclared(name) ); +} + +void +Parser::defineFunction(const std::string& name, const Expr& val) { + d_declScope.bindDefinedFunction(name, val); + Assert( isDeclared(name) ); } void Parser::defineType(const std::string& name, const Type& type) { - d_declScope.bindType(name,type); - Assert( isDeclared(name, SYM_SORT) ) ; + d_declScope.bindType(name, type); + Assert( isDeclared(name, SYM_SORT) ); +} + +void +Parser::defineType(const std::string& name, + const std::vector<Type>& params, + const Type& type) { + d_declScope.bindType(name, params, type); + Assert( isDeclared(name, SYM_SORT) ); } void @@ -139,20 +169,30 @@ Parser::defineParameterizedType(const std::string& name, const Type& type) { if(Debug.isOn("parser")) { Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", ["; - copy(params.begin(), params.end() - 1, - ostream_iterator<Type>(Debug("parser"), ", ") ); - Debug("parser") << params.back(); + if(params.size() > 0) { + copy(params.begin(), params.end() - 1, + ostream_iterator<Type>(Debug("parser"), ", ") ); + Debug("parser") << params.back(); + } Debug("parser") << "], " << type << ")" << std::endl; } - Warning("defineSort unimplemented\n"); - defineType(name,type); + defineType(name, params, type); +} + +Type +Parser::mkSort(const std::string& name) { + Debug("parser") << "newSort(" << name << ")" << std::endl; + Type type = d_exprManager->mkSort(name); + defineType(name, type); + return type; } Type -Parser::mkSort(const std::string& name, size_t arity) { - Debug("parser") << "newSort(" << name << ", " << arity << ")" << std::endl; - Type type = d_exprManager->mkSort(name, arity); - defineType(name,type); +Parser::mkSortConstructor(const std::string& name, size_t arity) { + Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" + << std::endl; + Type type = d_exprManager->mkSortConstructor(name, arity); + defineType(name, vector<Type>(arity), type); return type; } @@ -239,7 +279,7 @@ void Parser::checkOperator(Kind kind, unsigned int numArgs) throw (ParserExcepti if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) { parseError( "Operator is not defined in the current logic: " + kindToString(kind) ); } - checkArity(kind,numArgs); + checkArity(kind, numArgs); } void Parser::addOperator(Kind kind) { |