diff options
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e33ab7a70..c72a4f99b 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2330,16 +2330,16 @@ termAtomic[CVC4::api::Term& atomTerm] } // Floating-point rounding mode constants - | FP_RNE_TOK { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_EVEN); } - | FP_RNA_TOK { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_AWAY); } - | FP_RTP_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_POSITIVE); } - | FP_RTN_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_NEGATIVE); } - | FP_RTZ_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_ZERO); } - | FP_RNE_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_EVEN); } - | FP_RNA_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_NEAREST_TIES_TO_AWAY); } - | FP_RTP_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_POSITIVE); } - | FP_RTN_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_NEGATIVE); } - | FP_RTZ_FULL_TOK { atomTerm = SOLVER->mkConst(api::ROUND_TOWARD_ZERO); } + | FP_RNE_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN); } + | FP_RNA_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY); } + | FP_RTP_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_POSITIVE); } + | FP_RTN_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE); } + | FP_RTZ_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_ZERO); } + | FP_RNE_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN); } + | FP_RNA_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY); } + | FP_RTP_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_POSITIVE); } + | FP_RTN_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE); } + | FP_RTZ_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_ZERO); } // String constant | str[s,false] { atomTerm = SOLVER->mkString(s, true); } |