diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-05-15 19:01:19 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-05-15 19:01:19 +0000 |
| commit | 488ae3f42d9d3e06978e11a42d1d47e76072f797 (patch) | |
| tree | f466859889ceee9947e20d695fd35f99065277f8 /src/parser | |
| parent | fe2088f892af594765fc50d8cc9f2b4f87286b7c (diff) | |
This commit removes the CONST_INTEGER kind from nodes. This code comes from the branch arithmetic/remove_const_int.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/antlr_input.h | 6 | ||||
| -rw-r--r-- | src/parser/cvc/Cvc.g | 4 |
2 files changed, 5 insertions, 5 deletions
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index a39defd14..bdf5fe59e 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -171,7 +171,7 @@ public: static unsigned tokenToUnsigned( pANTLR3_COMMON_TOKEN token ); /** Retrieve an Integer from the text of a token */ - static Integer tokenToInteger( pANTLR3_COMMON_TOKEN token ); + static Rational tokenToInteger( pANTLR3_COMMON_TOKEN token ); /** Retrieve a Rational from the text of a token */ static Rational tokenToRational(pANTLR3_COMMON_TOKEN token); @@ -263,8 +263,8 @@ inline unsigned AntlrInput::tokenToUnsigned(pANTLR3_COMMON_TOKEN token) { return result; } -inline Integer AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) { - return Integer( tokenText(token) ); +inline Rational AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) { + return Rational( tokenText(token) ); } inline Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) { diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 52d32606b..2da9f0f63 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1165,7 +1165,7 @@ parameterization[CVC4::parser::DeclarationCheck check, bound returns [CVC4::parser::cvc::mySubrangeBound bound] : UNDERSCORE { $bound = SubrangeBound(); } - | k=integer { $bound = SubrangeBound(k); } + | k=integer { $bound = SubrangeBound(k.getNumerator()); } ; typeLetDecl[CVC4::parser::DeclarationCheck check] @@ -1991,7 +1991,7 @@ numeral returns [unsigned k = 0] /** * Similar to numeral but for arbitrary-precision, signed integer. */ -integer returns [CVC4::Integer k = 0] +integer returns [CVC4::Rational k = 0] : INTEGER_LITERAL { $k = AntlrInput::tokenToInteger($INTEGER_LITERAL); } | MINUS_TOK INTEGER_LITERAL |