diff options
| author | Clark Barrett <barrett@cs.stanford.edu> | 2017-05-16 15:23:41 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-05-16 15:23:41 -0700 |
| commit | ecbafef0e1677d8fbc92068139d29868aa3a8f3c (patch) | |
| tree | 407584a466c276f1c27faceb6f0d99868bf1b008 /src | |
| parent | 6316705d252732e1a8abcae1b8b36d77cec8c95d (diff) | |
| parent | 9ef270c5853b629a6f883b0b601cc7188b58cc0a (diff) | |
Merge pull request #161 from 4tXJ7f/fix_parser
Avoid tokenizing FP tokens in non-FP input
Diffstat (limited to 'src')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a49190825..f01893a35 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -3118,26 +3118,26 @@ FP_PINF_TOK : '+oo'; FP_NINF_TOK : '-oo'; FP_PZERO_TOK : '+zero'; FP_NZERO_TOK : '-zero'; -FP_NAN_TOK : 'NaN'; - -FP_TO_FP_TOK : 'to_fp'; -FP_TO_FPBV_TOK : 'to_fp_bv'; -FP_TO_FPFP_TOK : 'to_fp_fp'; -FP_TO_FPR_TOK : 'to_fp_real'; -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_RNE_TOK : 'RNE'; -FP_RNA_TOK : 'RNA'; -FP_RTP_TOK : 'RTP'; -FP_RTN_TOK : 'RTN'; -FP_RTZ_TOK : 'RTZ'; -FP_RNE_FULL_TOK : 'roundNearestTiesToEven'; -FP_RNA_FULL_TOK : 'roundNearestTiesToAway'; -FP_RTP_FULL_TOK : 'roundTowardPositive'; -FP_RTN_FULL_TOK : 'roundTowardNegative'; -FP_RTZ_FULL_TOK : 'roundTowardZero'; +FP_NAN_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'NaN'; + +FP_TO_FP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp'; +FP_TO_FPBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_bv'; +FP_TO_FPFP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_fp'; +FP_TO_FPR_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_real'; +FP_TO_FPS_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_signed'; +FP_TO_FPU_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_unsigned'; +FP_TO_UBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'fp.to_ubv'; +FP_TO_SBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'fp.to_sbv'; +FP_RNE_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RNE'; +FP_RNA_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RNA'; +FP_RTP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTP'; +FP_RTN_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTN'; +FP_RTZ_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTZ'; +FP_RNE_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundNearestTiesToEven'; +FP_RNA_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundNearestTiesToAway'; +FP_RTP_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardPositive'; +FP_RTN_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardNegative'; +FP_RTZ_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardZero'; /** * A sequence of printable ASCII characters (except backslash) that starts |