mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-15 15:25:26 +00:00
Code Activity

more fpa

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-10-01 17:52:55 -07:00
parent 08a87b102c
commit 6cc52e04c3
1 changed files with 6 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/sat/smt/fpa_solver.cpp
View file

@ -184,6 +184,7 @@ namespace fpa {
mpf_manager& mpfm = m_fpa_util.fm(); mpf_manager& mpfm = m_fpa_util.fm();
if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) { 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)) { if (!m_fpa_util.is_fp(n)) {
app_ref wrapped = m_converter.wrap(n); app_ref wrapped = m_converter.wrap(n);
mpf_rounding_mode rm; mpf_rounding_mode rm;
@ -194,14 +195,10 @@ namespace fpa {
add_unit(b_internalize(ctx.mk_eq(wrapped, rm_num))); add_unit(b_internalize(ctx.mk_eq(wrapped, rm_num)));
} }
else if (m_fpa_util.is_numeral(n, val)) { else if (m_fpa_util.is_numeral(n, val)) {
expr_ref bv_val_e(m), cc_args(m); expr_ref bv_val_e(convert(n), m);
bv_val_e = convert(n); VERIFY(m_fpa_util.is_fp(bv_val_e, a, b, c));
SASSERT(is_app(bv_val_e)); expr* args[] = { a, b, c };
SASSERT(to_app(bv_val_e)->get_num_args() == 3); expr_ref cc_args(m_bv_util.mk_concat(3, args), m);
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);
add_unit(b_internalize(ctx.mk_eq(wrapped, cc_args))); add_unit(b_internalize(ctx.mk_eq(wrapped, cc_args)));
add_units(mk_side_conditions()); add_units(mk_side_conditions());
} }
@ -217,12 +214,7 @@ namespace fpa {
SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n)); SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n));
} }
else { else {
/* Theory variables can be merged when (= bv-term (bvwrap fp-term)), /* 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. */
SASSERT(m_bv_util.is_bv(n)); SASSERT(m_bv_util.is_bv(n));
} }
} }