Converting semantic predicates in parser to AlwaysAssertions

1 files changed, 23 insertions, 16 deletions

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;
       }
     }