mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Bugfix for special-case handling in fp.fma.

Browse source 
Thanks to Florian Schanda for reporting this bug.
This commit is contained in:
Christoph M. Wintersteiger 2016-12-09 13:43:05 +00:00
parent 9df5c31485
commit 56b1a8b086
2 changed files with 31 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -1463,11 +1463,17 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
v6 = z;
// (x is 0) || (y is 0) -> z
expr_ref c71(m), xy_sgn(m), xyz_sgn(m);
m_simp.mk_or(x_is_zero, y_is_zero, c7);
expr_ref ite_c(m), rm_is_not_to_neg(m);
m_simp.mk_xor(x_is_neg, y_is_neg, xy_sgn);
m_simp.mk_xor(xy_sgn, z_is_neg, xyz_sgn);
m_simp.mk_and(z_is_zero, xyz_sgn, c71);
expr_ref zero_cond(m), rm_is_not_to_neg(m);
rm_is_not_to_neg = m.mk_not(rm_is_to_neg);
m_simp.mk_and(z_is_zero, rm_is_not_to_neg, ite_c);
mk_ite(ite_c, pzero, z, v7);
m_simp.mk_ite(rm_is_to_neg, nzero, pzero, zero_cond);
mk_ite(c71, zero_cond, z, v7);
// else comes the fused multiplication.
unsigned ebits = m_util.get_ebits(f->get_range());

43
src/smt/smt_model_checker.cpp
View file

@ -53,8 +53,8 @@ namespace smt {
}
void model_checker::set_qm(quantifier_manager & qm) {
SASSERT(m_qm == 0);
SASSERT(m_context == 0);
SASSERT(m_qm == 0);
SASSERT(m_context == 0);
m_qm = &qm;
m_context = &(m_qm->get_context());
}
@ -112,7 +112,7 @@ namespace smt {
if (!m_curr_model->eval(q->get_expr(), tmp, true)) {
return;
}
TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";);
TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";);
ptr_buffer<expr> subst_args;
unsigned num_decls = q->get_num_decls();
subst_args.resize(num_decls, 0);
@ -139,7 +139,7 @@ namespace smt {
bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) {
if (cex == 0) {
TRACE("model_checker", tout << "no model is available\n";);
return false;
return false;
}
unsigned num_decls = q->get_num_decls();
// Remark: sks were created for the flat version of q.
@ -187,20 +187,20 @@ namespace smt {
}
bindings.set(num_decls - i - 1, sk_value);
}
TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: ";
for (unsigned i = 0; i < num_decls; i++) {
tout << mk_ismt2_pp(bindings[i].get(), m) << " ";
}
tout << "\n";);
max_generation = std::max(m_qm->get_generation(q), max_generation);
add_instance(q, bindings, max_generation);
return true;
}
void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) {
for (unsigned i = 0; i < bindings.size(); i++)
for (unsigned i = 0; i < bindings.size(); i++)
m_new_instances_bindings.push_back(bindings[i]);
void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls()));
instance * new_inst = new (mem) instance(q, bindings.c_ptr(), max_generation);
@ -260,41 +260,42 @@ namespace smt {
bool model_checker::check(quantifier * q) {
SASSERT(!m_aux_context->relevancy());
m_aux_context->push();
quantifier * flat_q = get_flat_quantifier(q);
TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" <<
TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" <<
mk_ismt2_pp(flat_q->get_expr(), m) << "\n";);
expr_ref_vector sks(m);
assert_neg_q_m(flat_q, sks);
TRACE("model_checker", tout << "skolems:\n";
TRACE("model_checker", tout << "skolems:\n";
for (unsigned i = 0; i < sks.size(); i++) {
expr * sk = sks.get(i);
tout << mk_ismt2_pp(sk, m) << " " << mk_pp(m.get_sort(sk), m) << "\n";
});
lbool r = m_aux_context->check();
TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";);
if (r != l_true) {
m_aux_context->pop(1);
return r == l_false; // quantifier is satisfied by m_curr_model
}
model_ref complete_cex;
m_aux_context->get_model(complete_cex);
m_aux_context->get_model(complete_cex);
// try to find new instances using instantiation sets.
m_model_finder.restrict_sks_to_inst_set(m_aux_context.get(), q, sks);
unsigned num_new_instances = 0;
while (true) {
lbool r = m_aux_context->check();
TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);
if (r != l_true)
break;
break;
model_ref cex;
m_aux_context->get_model(cex);
TRACE("model_checker", tout << "[restricted] model-checker model cex:\n"; model_pp(tout, *cex););
if (!add_instance(q, cex.get(), sks, true)) {
break;
}
@ -302,7 +303,7 @@ namespace smt {
if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) {
TRACE("model_checker", tout << "Add blocking clause failed\n";);
// add_blocking_clause failed... stop the search for new counter-examples...
break;
break;
}
}
@ -396,7 +397,7 @@ namespace smt {
for (; it != end; ++it) {
quantifier * q = *it;
if(!m_qm->mbqi_enabled(q)) continue;
TRACE("model_checker",
TRACE("model_checker",
tout << "Check: " << mk_pp(q, m) << "\n";
tout << m_context->get_assignment(q) << "\n";);
@ -418,12 +419,12 @@ namespace smt {
}
}
}
if (found_relevant)
m_iteration_idx++;
TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md););
TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
m_max_cexs += m_params.m_mbqi_max_cexs;
if (num_failures == 0 && !m_context->validate_model()) {
@ -492,7 +493,7 @@ namespace smt {
expr * b = inst->m_bindings[i];
tout << mk_pp(b, m) << "\n";
});
TRACE("model_checker_instance",
TRACE("model_checker_instance",
expr_ref inst_expr(m);
instantiate(m, q, inst->m_bindings, inst_expr);
tout << "(assert " << mk_ismt2_pp(inst_expr, m) << ")\n";);