summaryrefslogtreecommitdiff
path: root/src/parser/cvc
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2012-05-15 19:01:19 +0000
committerTim King <taking@cs.nyu.edu>2012-05-15 19:01:19 +0000
commit488ae3f42d9d3e06978e11a42d1d47e76072f797 (patch)
treef466859889ceee9947e20d695fd35f99065277f8 /src/parser/cvc
parentfe2088f892af594765fc50d8cc9f2b4f87286b7c (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/cvc')
-rw-r--r--src/parser/cvc/Cvc.g4
1 files changed, 2 insertions, 2 deletions
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback