Forcing a type check on Node construction in debug mode (Fixes: #188)

NOTE: mkNode/mkExpr/parsing functions can now throw type checking exceptions

4 files changed, 18 insertions, 6 deletions

diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 6b38abaab..3532b8aa7 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -59,12 +59,12 @@ CvcInput::~CvcInput() {
 }
 
 Command* CvcInput::parseCommand()
-  throw (ParserException, AssertionException) {
+  throw (ParserException, TypeCheckingException, AssertionException) {
   return d_pCvcParser->parseCommand(d_pCvcParser);
 }
 
 Expr CvcInput::parseExpr()
-  throw (ParserException, AssertionException) {
+  throw (ParserException, TypeCheckingException, AssertionException) {
   return d_pCvcParser->parseExpr(d_pCvcParser);
 }
 
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index 6a37680e8..cce935c0b 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -71,14 +71,16 @@ protected:
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Command* parseCommand() throw(ParserException, AssertionException);
+  Command* parseCommand() 
+    throw(ParserException, TypeCheckingException, AssertionException);
 
   /** Parse an expression from the input. Returns a null <code>Expr</code>
    * if there is no expression there to parse.
    *
    * @throws ParserException if an error is encountered during parsing.
    */
-  Expr parseExpr() throw(ParserException, AssertionException);
+  Expr parseExpr() 
+    throw(ParserException, TypeCheckingException, AssertionException);
 
 private:
 
diff --git a/src/parser/input.h b/src/parser/input.h
index 62015ba51..1a90a4191 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -155,7 +155,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   virtual Command* parseCommand()
-    throw (ParserException, AssertionException) = 0;
+    throw (ParserException, TypeCheckingException, AssertionException) = 0;
 
   /**
    * Throws a <code>ParserException</code> with the given message.
@@ -171,7 +171,7 @@ protected:
    * @throws ParserException if an error is encountered during parsing.
    */
   virtual Expr parseExpr()
-    throw (ParserException, AssertionException) = 0;
+    throw (ParserException, TypeCheckingException, AssertionException) = 0;
 
   /** Set the Parser object for this input. */
   virtual void setParser(Parser& parser) = 0;
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 2bad12e2c..f73e268a3 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -234,6 +234,11 @@ Command* Parser::nextCommand() throw(ParserException) {
     } catch(ParserException& e) {
       setDone();
       throw;
+    } catch(TypeCheckingException& e) {
+      setDone();
+      stringstream ss;
+      ss << e.getMessage() << ": " << e.getExpression();
+      parseError( ss.str() );
     }
   }
   Debug("parser") << "nextCommand() => " << cmd << std::endl;
@@ -252,6 +257,11 @@ Expr Parser::nextExpression() throw(ParserException) {
     } catch(ParserException& e) {
       setDone();
       throw;
+    } catch(TypeCheckingException& e) {
+      setDone();
+      stringstream ss;
+      ss << e.getMessage() << ": " << e.getExpression();
+      parseError( ss.str() );
     }
   }
   Debug("parser") << "nextExpression() => " << result << std::endl;