better parametric datatype arity checking; fixes bug 433

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index fc375431cc3a06de4864a9b3aa3df1e8f265047b..9f8fd8bfb7d73f0fb1a1325ede4021ff4932605b 100644 (file)
--- 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 fb8589b5d1710cda1e2fe2b722597fe557fbe133..a5f04aeb024f76434282413d4b2adcbc3796905c 100644 (file)
--- 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{