From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 23 Apr 2011 05:36:09 +0000 (+0000)
Subject: fix for parser/tests for ANTLR 3.2 (it was working fine on 3.3)
X-Git-Tag: cvc5-1.0.0~8577
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e39882bd8a308711135a1ff644293fd9c46e6433;p=cvc5.git

fix for parser/tests for ANTLR 3.2 (it was working fine on 3.3)
---

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index bd0524f61..d9291c903 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -131,7 +131,7 @@ tokens {
   PARENHASH = '(#';
   HASHPAREN = '#)';
 
-  DOT = '.';
+  //DOT = '.';
   DOTDOT = '..';
 
   // Operators
@@ -215,7 +215,7 @@ bool isRightToLeft(int type) {
 int getOperatorPrecedence(int type) {
   switch(type) {
   case BITVECTOR_TOK: return 1;
-  case DOT:
+  //case DOT:
   case LPAREN:
   case LBRACE: return 2;
   case LBRACKET: return 3;
@@ -1418,7 +1418,7 @@ postfixTerm[CVC4::Expr& f]
       }
 
       /* record / tuple select */
-    | DOT
+    /*| DOT
       ( identifier[id,CHECK_NONE,SYM_VARIABLE]
         { UNSUPPORTED("record select not implemented yet");
           f = Expr(); }
@@ -1428,7 +1428,7 @@ postfixTerm[CVC4::Expr& f]
           // that's ok for now, once a TUPLE_SELECT operator exists,
           // that will do any necessary type checking
           f = EXPR_MANAGER->mkVar(TupleType(f.getType()).getTypes()[k]); }
-      )
+      )*/
     )*
     typeAscription[f]?
   ;
@@ -1596,7 +1596,7 @@ simpleTerm[CVC4::Expr& f]
     /* syntactic predicate: never match INTEGER.DIGIT as an integer and a dot!
      * This is a rational constant!  Otherwise the parser interprets it as a tuple
      * selector! */
-  | (INTEGER_LITERAL DOT DIGIT)=> r=decimal_literal { f = MK_CONST(r); }
+  | DECIMAL_LITERAL { f = MK_CONST(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
   | INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); }
     /* bitvector literals */
   | HEX_LITERAL
@@ -1769,9 +1769,8 @@ INTEGER_LITERAL
 /**
  * Matches a decimal literal.
  */
-decimal_literal returns [CVC4::Rational r]
-  : k=(INTEGER_LITERAL '.' DIGIT+)
-    { $r = AntlrInput::tokenToRational($k); }
+DECIMAL_LITERAL
+  : INTEGER_LITERAL '.' DIGIT+
   ;
 
 /**
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 323e61ca4..b898c4cc2 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -38,7 +38,6 @@ SMT2_TESTS = \
 
 # Regression tests for PL inputs
 CVC_TESTS = \
-	subranges.cvc \
 	boolean-prec.cvc \
 	hole6.cvc \
 	ite.cvc \
@@ -103,6 +102,7 @@ endif
 
 # and make sure to distribute it
 EXTRA_DIST += \
+	subranges.cvc \
 	error.cvc
 
 # synonyms for "check" in this directory
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 53050eece..3a9dd4418 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -227,7 +227,7 @@ public:
     tryGoodInput("a : INT = 5; a: INT;"); // decl after define, compatible
     tryGoodInput("a : TYPE; a : INT;"); // ok, sort and variable symbol spaces distinct
     tryGoodInput("a : TYPE; a : INT; b : a;"); // ok except a is both INT and sort `a'
-    tryGoodInput("a : [0..0]; b : [-5..5]; c : [-1..1]; d : [ _ .._];"); // subranges
+    //tryGoodInput("a : [0..0]; b : [-5..5]; c : [-1..1]; d : [ _ .._];"); // subranges
     tryGoodInput("a : [ _..1]; b : [_.. 0]; c :[_..-1];");
     tryGoodInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null END;");
     tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) END;");