diff options
-rw-r--r-- | src/expr/symbol_table.cpp | 18 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 7 |
2 files changed, 16 insertions, 9 deletions
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index fc375431c..9f8fd8bfb 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -121,22 +121,22 @@ bool SymbolTable::isBoundType(const std::string& name) const throw() { Type SymbolTable::lookupType(const std::string& name) const throw() { pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second; - Assert(p.first.size() == 0, - "type constructor arity is wrong: " - "`%s' requires %u parameters but was provided 0", - name.c_str(), p.first.size()); + CheckArgument(p.first.size() == 0, name, + "type constructor arity is wrong: " + "`%s' requires %u parameters but was provided 0", + name.c_str(), p.first.size()); return p.second; } Type SymbolTable::lookupType(const std::string& name, const std::vector<Type>& params) const throw() { pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second; - Assert(p.first.size() == params.size(), - "type constructor arity is wrong: " - "`%s' requires %u parameters but was provided %u", + CheckArgument(p.first.size() == params.size(), params, + "type constructor arity is wrong: " + "`%s' requires %u parameters but was provided %u", name.c_str(), p.first.size(), params.size()); if(p.first.size() == 0) { - Assert(p.second.isSort()); + CheckArgument(p.second.isSort(), name); return p.second; } if(p.second.isSortConstructor()) { @@ -161,7 +161,7 @@ Type SymbolTable::lookupType(const std::string& name, return instantiation; } else if(p.second.isDatatype()) { - Assert( DatatypeType(p.second).isParametric() ); + CheckArgument(DatatypeType(p.second).isParametric(), name, "expected parametric datatype"); return DatatypeType(p.second).instantiate(params); } else { if(Debug.isOn("sort")) { diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index fb8589b5d..a5f04aeb0 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1104,6 +1104,13 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, PARSER_STATE->isDeclared(id, SYM_SORT)) { Debug("parser-param") << "param: getSort " << id << " " << types.size() << " " << PARSER_STATE->getArity( id ) << " " << PARSER_STATE->isDeclared(id, SYM_SORT) << std::endl; + if(types.size() != PARSER_STATE->getArity(id)) { + std::stringstream ss; + ss << "incorrect arity for symbol `" << id << "': expected " + << PARSER_STATE->getArity( id ) << " type arguments, got " + << types.size(); + PARSER_STATE->parseError(ss.str()); + } if(types.size() > 0) { t = PARSER_STATE->getSort(id, types); }else{ |