1 files changed, 41 insertions, 3 deletions
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 24d0ac3d7..af3ce9d1b 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -297,12 +297,21 @@ void AntlrParser::parseError(string message)
 
 bool AntlrParser::checkDeclaration(string varName, 
                                    DeclarationCheck check,
-                                   SymbolType type) {
+                                   SymbolType type)
+    throw (antlr::SemanticException) {
   switch(check) {
   case CHECK_DECLARED:
-    return isDeclared(varName, type);
+    if( !isDeclared(varName, type) ) {
+      parseError("Symbol " + varName + " not declared");
+    } else {
+      return true;
+    }
   case CHECK_UNDECLARED:
-    return !isDeclared(varName, type);
+    if( isDeclared(varName, type) ) {
+      parseError("Symbol " + varName + " previously declared");
+    } else {
+      return true;
+    }
   case CHECK_NONE:
     return true;
   default:
@@ -310,5 +319,34 @@ bool AntlrParser::checkDeclaration(string varName,
   }
 }
 
+bool AntlrParser::checkFunction(string name)   
+  throw (antlr::SemanticException) {
+  if( !isFunction(name) ) {
+    parseError("Expecting function symbol, found '" + name + "'");
+  } 
+
+  return true;
+}
+
+bool AntlrParser::checkArity(Kind kind, unsigned int numArgs)
+  throw (antlr::SemanticException) {
+  unsigned int min = minArity(kind);
+  unsigned int max = maxArity(kind);
+
+  if( numArgs < min || numArgs > max ) {
+    stringstream ss;
+    ss << "Expecting ";
+    if( numArgs < min ) {
+      ss << "at least " << min << " ";
+    } else {
+      ss << "at most " << max << " ";
+    }
+    ss << "arguments for operator '" << kind << "', ";
+    ss << "found " << numArgs;
+    parseError(ss.str());
+  }
+  return true;
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */