Converting semantic predicates in parser to AlwaysAssertions

4 files changed, 44 insertions, 32 deletions

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index bd263f72d..24d0ac3d7 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -288,9 +288,9 @@ bool AntlrParser::isDeclared(string name, SymbolType type) {
   }
 }
 
-void AntlrParser::rethrow(antlr::SemanticException& e, string new_message)
+void AntlrParser::parseError(string message)
     throw (antlr::SemanticException) {
-  throw antlr::SemanticException(new_message, getFilename(),
+  throw antlr::SemanticException(message, getFilename(),
                                  LT(1).get()->getLine(),
                                  LT(1).get()->getColumn());
 }
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 76200368c..eec444af9 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -101,10 +101,9 @@ protected:
   AntlrParser(antlr::TokenStream& lexer, int k);
 
   /**
-   * Renames the antlr semantic expression to a given message.
+   * Throws an ANTLR semantic exception with the given message.
    */
-  void rethrow(antlr::SemanticException& e, std::string msg)
-      throw (antlr::SemanticException);
+  void parseError(std::string msg) throw (antlr::SemanticException);
 
   /**
    * Returns a variable, given a name and a type.
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 794f4706a..926430a5c 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -157,8 +157,8 @@ returns [std::string id]
     { checkDeclaration(id, check, type) }?
     exception catch [antlr::SemanticException& ex] {
       switch (check) {
-        case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared");
-        case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared");
+        case CHECK_DECLARED: parseError("Symbol " + id + " not declared");
+        case CHECK_UNDECLARED: parseError("Symbol " + id + " already declared");
         default: throw ex;
       }
     }
@@ -322,12 +322,12 @@ term returns [CVC4::Expr t]
   Debug("parser") << "term: " << LT(1)->getText() << endl;
 }
   : /* function application */
-    { isFunction(LT(1)->getText()) }? 
-    name = functionSymbol[CHECK_DECLARED]
-    {
-      std::vector<CVC4::Expr> args;
-      args.push_back( getFunction(name) ); 
-    }
+    // { isFunction(LT(1)->getText()) }? 
+    { Expr f; 
+      std::vector<CVC4::Expr> args; }
+    f = functionSymbol[CHECK_DECLARED]
+    { args.push_back( f ); }
+
     LPAREN formulaList[args] RPAREN
     // TODO: check arity
     { t = mkExpr(CVC4::APPLY, args); }
@@ -382,9 +382,15 @@ iteElseTerm returns [CVC4::Expr t]
  * @param what kind of check to perform on the id
  * @return the predicate symol
  */
-functionSymbol[DeclarationCheck check = CHECK_NONE] returns [std::string symbol]
+functionSymbol[DeclarationCheck check = CHECK_NONE] returns [CVC4::Expr f]
 {
   Debug("parser") << "function symbol: " << LT(1)->getText() << endl;
-
-}  : symbol = identifier[check,SYM_FUNCTION]
+  std::string name;
+}  
+  : name = identifier[check,SYM_FUNCTION]
+    { AlwaysAssert( isFunction(name) );  
+      f = getFunction(name); }
+    exception catch [CVC4::AssertionException& ex] {
+      parseError("Expected function symbol, found: " + name);
+    }
   ;
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index 4ecac0418..fc38871b0 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -16,6 +16,7 @@
 header "post_include_hpp" {
 #include "parser/antlr_parser.h"
 #include "expr/command.h"
+#include "util/Assert.h"
 }
 
 header "post_include_cpp" {
@@ -42,7 +43,7 @@ class AntlrSmtParser extends Parser("AntlrParser");
 options {
   genHashLines = true;              // Include line number information
   importVocab = SmtVocabulary;      // Import the common vocabulary
-  defaultErrorHandler = false;      // Skip the defaul error handling, just break with exceptions
+  defaultErrorHandler = false;      // Skip the default error handling, just break with exceptions
   k = 2;
 }
 
@@ -122,10 +123,10 @@ annotatedFormula returns [CVC4::Expr formula]
 }
   : /* a built-in operator application */
     LPAREN kind = builtinOp annotatedFormulas[args] RPAREN 
-    { args.size() >= minArity(kind) 
-      && args.size() <= maxArity(kind) }?
-    { formula = mkExpr(kind,args); }
-      exception catch [antlr::SemanticException& ex] {
+    { AlwaysAssert( args.size() >= minArity(kind) 
+                    && args.size() <= maxArity(kind) );
+      formula = mkExpr(kind,args); }
+      exception catch [CVC4::AssertionException& ex] {
         stringstream ss;
         ss << "Expected ";
         if( args.size() < minArity(kind) ) {
@@ -135,11 +136,15 @@ annotatedFormula returns [CVC4::Expr formula]
         }
         ss << "arguments for operator '" << kind << "'. ";
         ss << "Found: " << args.size();
-        rethrow(ex, ss.str());
+        parseError(ss.str());
       }
 
   | /* A non-built-in function application */
-    { isFunction(LT(2)->getText()) }? 
+
+    // Semantic predicate not necessary if parenthesized subexpressions
+    // are disallowed
+    // { isFunction(LT(2)->getText()) }? 
+
     { Expr f; }
     LPAREN f = functionSymbol
     { args.push_back(f); }
@@ -156,9 +161,6 @@ annotatedFormula returns [CVC4::Expr formula]
     RPAREN
     { formula = mkExpr(CVC4::ITE, test, trueExpr, falseExpr); }
 
-  | /* a parenthesized sub-formula */
-    LPAREN formula = annotatedFormula RPAREN
-
   | /* a variable */
     { std::string name; }
     name = identifier[CHECK_DECLARED]
@@ -224,7 +226,12 @@ functionSymbol returns [CVC4::Expr fun]
   string name;
 }
   : name = functionName[CHECK_DECLARED]
-    { fun = getFunction(name); }
+    { AlwaysAssert( isFunction(name) );
+      fun = getFunction(name); }
+    exception catch [CVC4::AssertionException& ex] {
+      parseError("Expected function symbol, found: " + name);
+    }
+
   ;
   
 /**
@@ -325,12 +332,12 @@ returns [std::string id]
                   << " type? " << toString(type) << endl;
 }
   : x:IDENTIFIER
-    { id = x->getText(); }
-    { checkDeclaration(id, check,type) }?
-    exception catch [antlr::SemanticException& ex] {
+    { id = x->getText();
+      AlwaysAssert( checkDeclaration(id, check,type) ); }
+    exception catch [CVC4::AssertionException& ex] {
       switch (check) {
-        case CHECK_DECLARED: rethrow(ex, "Symbol " + id + " not declared");
-        case CHECK_UNDECLARED: rethrow(ex, "Symbol " + id + " already declared");
+        case CHECK_DECLARED: parseError("Symbol " + id + " not declared");
+        case CHECK_UNDECLARED: parseError("Symbol " + id + " already declared");
         default: throw ex;
       }
     }