diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-01-10 10:47:53 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-01-10 10:47:53 -0800 |
| commit | 51cb061609e10ff68fb9db053d23ea9dd72ddea2 (patch) | |
| tree | 37e66c9a6200f45f90d48ab9d3b305e37f154d68 /src/parser/smt2 | |
| parent | fb145effd5bfe67090736969478ff54cf7f62984 (diff) | |
New C++ API: Get rid of mkConst functions (simplify API). (#2783)
Diffstat (limited to 'src/parser/smt2')
| -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); } |