From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 26 Oct 2012 20:13:28 +0000 (+0000)
Subject: better parametric datatype arity checking; fixes bug 433
X-Git-Tag: cvc5-1.0.0~7665
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8745a7d237a14b4f6b899b651c2d99bbd68c1772;p=cvc5.git

better parametric datatype arity checking; fixes bug 433
---

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{