From 6cc52e04c3ea7e2534644a285d231bdaaafd8714 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Oct 2020 17:52:55 -0700 Subject: [PATCH] more fpa Signed-off-by: Nikolaj Bjorner --- src/sat/smt/fpa_solver.cpp | 20 ++++++-------------- 1 file changed, 6 insertions(+), 14 deletions(-) diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp index 122437fe434..fefce8c9cce 100644 --- a/src/sat/smt/fpa_solver.cpp +++ b/src/sat/smt/fpa_solver.cpp @@ -184,6 +184,7 @@ namespace fpa { mpf_manager& mpfm = m_fpa_util.fm(); if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) { + expr* a = nullptr, * b = nullptr, * c = nullptr; if (!m_fpa_util.is_fp(n)) { app_ref wrapped = m_converter.wrap(n); mpf_rounding_mode rm; @@ -194,14 +195,10 @@ namespace fpa { add_unit(b_internalize(ctx.mk_eq(wrapped, rm_num))); } else if (m_fpa_util.is_numeral(n, val)) { - expr_ref bv_val_e(m), cc_args(m); - bv_val_e = convert(n); - SASSERT(is_app(bv_val_e)); - SASSERT(to_app(bv_val_e)->get_num_args() == 3); - app_ref bv_val_a(m); - bv_val_a = to_app(bv_val_e.get()); - expr* args[] = { bv_val_a->get_arg(0), bv_val_a->get_arg(1), bv_val_a->get_arg(2) }; - cc_args = m_bv_util.mk_concat(3, args); + expr_ref bv_val_e(convert(n), m); + VERIFY(m_fpa_util.is_fp(bv_val_e, a, b, c)); + expr* args[] = { a, b, c }; + expr_ref cc_args(m_bv_util.mk_concat(3, args), m); add_unit(b_internalize(ctx.mk_eq(wrapped, cc_args))); add_units(mk_side_conditions()); } @@ -217,12 +214,7 @@ namespace fpa { SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n)); } else { - /* Theory variables can be merged when (= bv-term (bvwrap fp-term)), - in which case context::relevant_eh may call solver::relevant_eh - after theory_bv::relevant_eh, regardless of whether solver is - interested in this term. But, this can only happen because of - (bvwrap ...) terms, i.e., `n' must be a bit-vector expression, - which we can safely ignore. */ + /* Theory variables can be merged when (= bv-term (bvwrap fp-term)) */ SASSERT(m_bv_util.is_bv(n)); } }