diff options
| -rw-r--r-- | src/parser/cvc/Cvc.g | 15 | ||||
| -rw-r--r-- | test/regress/regress0/Makefile.am | 2 | ||||
| -rw-r--r-- | test/unit/parser/parser_black.h | 2 |
3 files changed, 9 insertions, 10 deletions
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;"); |