From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 16 Apr 2015 03:38:53 +0000 (-0400)
Subject: fp reorder tokens to match other occurences
X-Git-Tag: cvc5-1.0.0~6344^2~1^2~5
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7a22a0d20442035556f0f026c31f2d65f8c8fd1d;p=cvc5.git

fp reorder tokens to match other occurences
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index dd3464940..87dd18381 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2543,12 +2543,13 @@ EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
 // tokenized and handled directly when
 // processing a term
 
-FP_TOK : 'fp';
 FP_PINF_TOK : '+oo';
 FP_NINF_TOK : '-oo';
 FP_PZERO_TOK : '+zero';
 FP_NZERO_TOK : '-zero';
 FP_NAN_TOK : 'NaN';
+
+FP_TOK : 'fp';
 FP_EQ_TOK : 'fp.eq';
 FP_ABS_TOK : 'fp.abs';
 FP_NEG_TOK : 'fp.neg';
@@ -2573,6 +2574,8 @@ FP_ISINF_TOK : 'fp.isInfinite';
 FP_ISNAN_TOK : 'fp.isNaN';
 FP_ISNEG_TOK : 'fp.isNegative';
 FP_ISPOS_TOK : 'fp.isPositive';
+FP_TO_REAL_TOK : 'fp.to_real';
+
 FP_TO_FP_TOK : 'to_fp';
 FP_TO_FPBV_TOK : 'to_fp_bv';
 FP_TO_FPFP_TOK : 'to_fp_fp';
@@ -2581,7 +2584,6 @@ FP_TO_FPS_TOK : 'to_fp_signed';
 FP_TO_FPU_TOK : 'to_fp_unsigned';
 FP_TO_UBV_TOK : 'fp.to_ubv';
 FP_TO_SBV_TOK : 'fp.to_sbv';
-FP_TO_REAL_TOK : 'fp.to_real';
 FP_RNE_TOK : 'RNE';
 FP_RNA_TOK : 'RNA';
 FP_RTP_TOK : 'RTP';