diff options
author | Andres Noetzli <noetzli@stanford.edu> | 2017-05-16 11:33:38 -0700 |
---|---|---|
committer | Andres Noetzli <noetzli@stanford.edu> | 2017-05-16 11:33:38 -0700 |
commit | 9ef270c5853b629a6f883b0b601cc7188b58cc0a (patch) | |
tree | c0ac83f78f5be7a45f8406ad37bad56da51c1112 /src/parser | |
parent | f6215a3d10c11976cffbeb4c88223e8434ffc4d3 (diff) |
Avoid tokenizing FP tokens in non-FP input
This commit addresses bug 807. CVC4 was parsing floating-point related tokens
such as NaN as floating-point tokens even for inputs that do not use the FP
theory, which lead to failing SMT-LIB benchmarks that declare functions named
NaN.
Diffstat (limited to 'src/parser')
-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 |