mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into bvsls

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2014-12-19 12:33:03 +00:00
commit 1f29b3e0a9
205 changed files with 4767 additions and 2541 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/tactic/bv/bv_size_reduction_tactic.cpp
View file

@ -151,7 +151,7 @@ struct bv_size_reduction_tactic::imp {
// bound is infeasible.
}
else {
update_signed_upper(to_app(lhs), val);
update_signed_upper(to_app(rhs), val);
}
}
else update_signed_lower(to_app(rhs), val);
@ -229,17 +229,35 @@ struct bv_size_reduction_tactic::imp {
else {
// l < u
if (l.is_neg()) {
unsigned i_nb = (u - l).get_num_bits();
unsigned l_nb = (-l).get_num_bits();
unsigned v_nb = m_util.get_bv_size(v);
if (i_nb < v_nb) {
new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));
new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const);
if (u.is_neg())
{
// l <= v <= u <= 0
unsigned i_nb = l_nb;
TRACE("bv_size_reduction", tout << " l <= " << v->get_decl()->get_name() << " <= u <= 0 " << " --> " << i_nb << " bits\n";);
if (i_nb < v_nb) {
new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(-1), v_nb - i_nb), new_const);
}
}
else {
// l <= v <= 0 <= u
unsigned u_nb = u.get_num_bits();
unsigned i_nb = ((l_nb > u_nb) ? l_nb : u_nb) + 1;
TRACE("bv_size_reduction", tout << " l <= " << v->get_decl()->get_name() << " <= 0 <= u " << " --> " << i_nb << " bits\n";);
if (i_nb < v_nb) {
new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));
new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const);
}
}
}
else {
// 0 <= l <= v <= u
unsigned u_nb = u.get_num_bits();
unsigned v_nb = m_util.get_bv_size(v);
TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << " --> " << u_nb << " bits\n";);
if (u_nb < v_nb) {
new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);

19
src/tactic/fpa/fpa2bv_model_converter.cpp
View file

@ -111,14 +111,25 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
unsigned ebits = fu.get_ebits(var->get_range());
unsigned sbits = fu.get_sbits(var->get_range());
expr_ref sgn(m), sig(m), exp(m);
sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl());
sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl());
exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl());
expr_ref sgn(m), sig(m), exp(m);
bv_mdl->eval(a->get_arg(0), sgn, true);
bv_mdl->eval(a->get_arg(1), sig, true);
bv_mdl->eval(a->get_arg(2), exp, true);
SASSERT(a->is_app_of(fu.get_family_id(), OP_TO_FLOAT));
#ifdef Z3DEBUG
SASSERT(to_app(a->get_arg(0))->get_decl()->get_arity() == 0);
SASSERT(to_app(a->get_arg(1))->get_decl()->get_arity() == 0);
SASSERT(to_app(a->get_arg(1))->get_decl()->get_arity() == 0);
seen.insert(to_app(a->get_arg(0))->get_decl());
seen.insert(to_app(a->get_arg(1))->get_decl());
seen.insert(to_app(a->get_arg(2))->get_decl());
#else
SASSERT(a->get_arg(0)->get_kind() == OP_EXTRACT);
SASSERT(to_app(a->get_arg(0))->get_arg(0)->get_kind() == OP_EXTRACT);
seen.insert(to_app(to_app(a->get_arg(0))->get_arg(0))->get_decl());
#endif
if (!sgn && !sig && !exp)
continue;

2
src/tactic/tactical.cpp
View file

@ -1276,7 +1276,7 @@ public:
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
if (m_p->operator()(*(in.get())).is_true())
if (m_p->operator()(*(in.get())).is_true())
m_t1->operator()(in, result, mc, pc, core);
else
m_t2->operator()(in, result, mc, pc, core);