From: Andres Noetzli <noetzli@stanford.edu>
Date: Tue, 16 May 2017 18:33:38 +0000 (-0700)
Subject: Avoid tokenizing FP tokens in non-FP input
X-Git-Tag: cvc5-1.0.0~5795^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9ef270c5853b629a6f883b0b601cc7188b58cc0a;p=cvc5.git

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.
---

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