mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 11:58:31 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-12-09 15:32:26 +01:00
commit a17e957362
3 changed files with 47 additions and 40 deletions
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; v6 = z;
// (x is 0) || (y is 0) -> 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); 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); 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); m_simp.mk_ite(rm_is_to_neg, nzero, pzero, zero_cond);
mk_ite(ite_c, pzero, z, v7); mk_ite(c71, zero_cond, z, v7);
// else comes the fused multiplication. // else comes the fused multiplication.
unsigned ebits = m_util.get_ebits(f->get_range()); 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) { void model_checker::set_qm(quantifier_manager & qm) {
SASSERT(m_qm == 0); SASSERT(m_qm == 0);
SASSERT(m_context == 0); SASSERT(m_context == 0);
m_qm = &qm; m_qm = &qm;
m_context = &(m_qm->get_context()); m_context = &(m_qm->get_context());
} }
@ -112,7 +112,7 @@ namespace smt {
if (!m_curr_model->eval(q->get_expr(), tmp, true)) { if (!m_curr_model->eval(q->get_expr(), tmp, true)) {
return; 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; ptr_buffer<expr> subst_args;
unsigned num_decls = q->get_num_decls(); unsigned num_decls = q->get_num_decls();
subst_args.resize(num_decls, 0); 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) { bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) {
if (cex == 0) { if (cex == 0) {
TRACE("model_checker", tout << "no model is available\n";); TRACE("model_checker", tout << "no model is available\n";);
return false; return false;
} }
unsigned num_decls = q->get_num_decls(); unsigned num_decls = q->get_num_decls();
// Remark: sks were created for the flat version of q. // Remark: sks were created for the flat version of q.
@ -187,20 +187,20 @@ namespace smt {
} }
bindings.set(num_decls - i - 1, sk_value); bindings.set(num_decls - i - 1, sk_value);
} }
TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: "; TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: ";
for (unsigned i = 0; i < num_decls; i++) { for (unsigned i = 0; i < num_decls; i++) {
tout << mk_ismt2_pp(bindings[i].get(), m) << " "; tout << mk_ismt2_pp(bindings[i].get(), m) << " ";
} }
tout << "\n";); tout << "\n";);
max_generation = std::max(m_qm->get_generation(q), max_generation); max_generation = std::max(m_qm->get_generation(q), max_generation);
add_instance(q, bindings, max_generation); add_instance(q, bindings, max_generation);
return true; return true;
} }
void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) { 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]); m_new_instances_bindings.push_back(bindings[i]);
void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls())); 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); instance * new_inst = new (mem) instance(q, bindings.c_ptr(), max_generation);
@ -260,41 +260,42 @@ namespace smt {
bool model_checker::check(quantifier * q) { bool model_checker::check(quantifier * q) {
SASSERT(!m_aux_context->relevancy()); SASSERT(!m_aux_context->relevancy());
m_aux_context->push(); m_aux_context->push();
quantifier * flat_q = get_flat_quantifier(q); 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";); mk_ismt2_pp(flat_q->get_expr(), m) << "\n";);
expr_ref_vector sks(m); expr_ref_vector sks(m);
assert_neg_q_m(flat_q, sks); 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++) { for (unsigned i = 0; i < sks.size(); i++) {
expr * sk = sks.get(i); expr * sk = sks.get(i);
tout << mk_ismt2_pp(sk, m) << " " << mk_pp(m.get_sort(sk), m) << "\n"; tout << mk_ismt2_pp(sk, m) << " " << mk_pp(m.get_sort(sk), m) << "\n";
}); });
lbool r = m_aux_context->check(); lbool r = m_aux_context->check();
TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";); TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";);
if (r != l_true) { if (r != l_true) {
m_aux_context->pop(1); m_aux_context->pop(1);
return r == l_false; // quantifier is satisfied by m_curr_model return r == l_false; // quantifier is satisfied by m_curr_model
} }
model_ref complete_cex; 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. // try to find new instances using instantiation sets.
m_model_finder.restrict_sks_to_inst_set(m_aux_context.get(), q, sks); m_model_finder.restrict_sks_to_inst_set(m_aux_context.get(), q, sks);
unsigned num_new_instances = 0; unsigned num_new_instances = 0;
while (true) { while (true) {
lbool r = m_aux_context->check(); lbool r = m_aux_context->check();
TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";); TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);
if (r != l_true) if (r != l_true)
break; break;
model_ref cex; model_ref cex;
m_aux_context->get_model(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)) { if (!add_instance(q, cex.get(), sks, true)) {
break; break;
} }
@ -302,7 +303,7 @@ namespace smt {
if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) { if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) {
TRACE("model_checker", tout << "Add blocking clause failed\n";); TRACE("model_checker", tout << "Add blocking clause failed\n";);
// add_blocking_clause failed... stop the search for new counter-examples... // add_blocking_clause failed... stop the search for new counter-examples...
break; break;
} }
} }
@ -396,7 +397,7 @@ namespace smt {
for (; it != end; ++it) { for (; it != end; ++it) {
quantifier * q = *it; quantifier * q = *it;
if(!m_qm->mbqi_enabled(q)) continue; if(!m_qm->mbqi_enabled(q)) continue;
TRACE("model_checker", TRACE("model_checker",
tout << "Check: " << mk_pp(q, m) << "\n"; tout << "Check: " << mk_pp(q, m) << "\n";
tout << m_context->get_assignment(q) << "\n";); tout << m_context->get_assignment(q) << "\n";);
@ -418,12 +419,12 @@ namespace smt {
} }
} }
} }
if (found_relevant) if (found_relevant)
m_iteration_idx++; m_iteration_idx++;
TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md);); 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; m_max_cexs += m_params.m_mbqi_max_cexs;
if (num_failures == 0 && !m_context->validate_model()) { if (num_failures == 0 && !m_context->validate_model()) {
@ -492,7 +493,7 @@ namespace smt {
expr * b = inst->m_bindings[i]; expr * b = inst->m_bindings[i];
tout << mk_pp(b, m) << "\n"; tout << mk_pp(b, m) << "\n";
}); });
TRACE("model_checker_instance", TRACE("model_checker_instance",
expr_ref inst_expr(m); expr_ref inst_expr(m);
instantiate(m, q, inst->m_bindings, inst_expr); instantiate(m, q, inst->m_bindings, inst_expr);
tout << "(assert " << mk_ismt2_pp(inst_expr, m) << ")\n";); tout << "(assert " << mk_ismt2_pp(inst_expr, m) << ")\n";);

32
src/util/mpf.cpp
View file

@ -1224,7 +1224,7 @@ void mpf_manager::renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, m
m_mpz_manager.machine_div2k(sig, 1); m_mpz_manager.machine_div2k(sig, 1);
exp++; exp++;
} }
const mpz & pl = m_powers2(sbits-1); const mpz & pl = m_powers2(sbits-1);
while (m_mpz_manager.lt(sig, pl)) { while (m_mpz_manager.lt(sig, pl)) {
m_mpz_manager.mul2k(sig, 1); m_mpz_manager.mul2k(sig, 1);
@ -1235,7 +1235,7 @@ void mpf_manager::renormalize(unsigned ebits, unsigned sbits, mpf_exp_t & exp, m
void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & exp_diff, bool partial) { void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & exp_diff, bool partial) {
unsigned ebits = x.ebits; unsigned ebits = x.ebits;
unsigned sbits = x.sbits; unsigned sbits = x.sbits;
SASSERT(-1 <= exp_diff && exp_diff < INT64_MAX); SASSERT(-1 <= exp_diff && exp_diff < INT64_MAX);
SASSERT(exp_diff < ebits+sbits || partial); SASSERT(exp_diff < ebits+sbits || partial);
@ -1252,7 +1252,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
SASSERT(m_mpz_manager.lt(y.significand, m_powers2(sbits))); SASSERT(m_mpz_manager.lt(y.significand, m_powers2(sbits)));
SASSERT(m_mpz_manager.ge(y.significand, m_powers2(sbits - 1))); SASSERT(m_mpz_manager.ge(y.significand, m_powers2(sbits - 1)));
// 1. Compute a/b // 1. Compute a/b
bool x_div_y_sgn = x.sign != y.sign; bool x_div_y_sgn = x.sign != y.sign;
mpf_exp_t x_div_y_exp = D; mpf_exp_t x_div_y_exp = D;
scoped_mpz x_sig_shifted(m_mpz_manager), x_div_y_sig_lrg(m_mpz_manager), x_div_y_rem(m_mpz_manager); scoped_mpz x_sig_shifted(m_mpz_manager), x_div_y_sig_lrg(m_mpz_manager), x_div_y_rem(m_mpz_manager);
@ -1271,7 +1271,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
mpf_exp_t Q_exp = x_div_y_exp; mpf_exp_t Q_exp = x_div_y_exp;
scoped_mpz Q_sig(m_mpz_manager), Q_rem(m_mpz_manager); scoped_mpz Q_sig(m_mpz_manager), Q_rem(m_mpz_manager);
unsigned Q_shft = (sbits-1) + (sbits+3) - (unsigned) (partial ? N :Q_exp); unsigned Q_shft = (sbits-1) + (sbits+3) - (unsigned) (partial ? N :Q_exp);
if (partial) { if (partial) {
// Round according to MPF_ROUND_TOWARD_ZERO // Round according to MPF_ROUND_TOWARD_ZERO
SASSERT(0 < N && N < Q_exp && Q_exp < INT_MAX); SASSERT(0 < N && N < Q_exp && Q_exp < INT_MAX);
m_mpz_manager.machine_div2k(x_div_y_sig_lrg, Q_shft, Q_sig); m_mpz_manager.machine_div2k(x_div_y_sig_lrg, Q_shft, Q_sig);
@ -1294,7 +1294,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
TRACE("mpf_dbg_rem", tout << "Q_exp=" << Q_exp << std::endl; TRACE("mpf_dbg_rem", tout << "Q_exp=" << Q_exp << std::endl;
tout << "Q_sig=" << m_mpz_manager.to_string(Q_sig) << std::endl; tout << "Q_sig=" << m_mpz_manager.to_string(Q_sig) << std::endl;
tout << "Q=" << to_string_hexfloat(Q_sgn, Q_exp, Q_sig, ebits, sbits, 0) << std::endl;); tout << "Q=" << to_string_hexfloat(Q_sgn, Q_exp, Q_sig, ebits, sbits, 0) << std::endl;);
if ((D == -1 || partial) && m_mpz_manager.is_zero(Q_sig)) if ((D == -1 || partial) && m_mpz_manager.is_zero(Q_sig))
return; // This means x % y = x. return; // This means x % y = x.
@ -1308,7 +1308,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
bool YQ_sgn = x.sign; bool YQ_sgn = x.sign;
scoped_mpz YQ_sig(m_mpz_manager); scoped_mpz YQ_sig(m_mpz_manager);
mpf_exp_t YQ_exp = Q_exp + y.exponent; mpf_exp_t YQ_exp = Q_exp + y.exponent;
m_mpz_manager.mul(y.significand, Q_sig, YQ_sig); m_mpz_manager.mul(y.significand, Q_sig, YQ_sig);
renormalize(ebits, 2*sbits-1, YQ_exp, YQ_sig); // YQ_sig has `sbits-1' extra bits. renormalize(ebits, 2*sbits-1, YQ_exp, YQ_sig); // YQ_sig has `sbits-1' extra bits.
(void)YQ_sgn; (void)YQ_sgn;
@ -1317,11 +1317,11 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
tout << "YQ_sig=" << m_mpz_manager.to_string(YQ_sig) << std::endl; tout << "YQ_sig=" << m_mpz_manager.to_string(YQ_sig) << std::endl;
tout << "YQ=" << to_string_hexfloat(YQ_sgn, YQ_exp, YQ_sig, ebits, sbits, sbits-1) << std::endl;); tout << "YQ=" << to_string_hexfloat(YQ_sgn, YQ_exp, YQ_sig, ebits, sbits, sbits-1) << std::endl;);
// `sbits-1' extra bits in YQ_sig. // `sbits-1' extra bits in YQ_sig.
SASSERT(m_mpz_manager.lt(YQ_sig, m_powers2(2*sbits-1))); SASSERT(m_mpz_manager.lt(YQ_sig, m_powers2(2*sbits-1)));
SASSERT(m_mpz_manager.ge(YQ_sig, m_powers2(2*sbits-2)) || YQ_exp <= mk_bot_exp(ebits)); SASSERT(m_mpz_manager.ge(YQ_sig, m_powers2(2*sbits-2)) || YQ_exp <= mk_bot_exp(ebits));
// 4. Compute X-Y*Q // 4. Compute X-Y*Q
mpf_exp_t X_YQ_exp = x.exponent; mpf_exp_t X_YQ_exp = x.exponent;
scoped_mpz X_YQ_sig(m_mpz_manager); scoped_mpz X_YQ_sig(m_mpz_manager);
mpf_exp_t exp_delta = exp(x) - YQ_exp; mpf_exp_t exp_delta = exp(x) - YQ_exp;
@ -1339,14 +1339,14 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
SASSERT(m_mpz_manager.ge(minuend, m_powers2(2*sbits-2))); SASSERT(m_mpz_manager.ge(minuend, m_powers2(2*sbits-2)));
SASSERT(m_mpz_manager.lt(subtrahend, m_powers2(2*sbits-1))); SASSERT(m_mpz_manager.lt(subtrahend, m_powers2(2*sbits-1)));
SASSERT(m_mpz_manager.ge(subtrahend, m_powers2(2*sbits-2))); SASSERT(m_mpz_manager.ge(subtrahend, m_powers2(2*sbits-2)));
if (exp_delta != 0) { if (exp_delta != 0) {
scoped_mpz sticky_rem(m_mpz_manager); scoped_mpz sticky_rem(m_mpz_manager);
m_mpz_manager.set(sticky_rem, 0); m_mpz_manager.set(sticky_rem, 0);
if (exp_delta > sbits+5) if (exp_delta > sbits+5)
sticky_rem.swap(subtrahend); sticky_rem.swap(subtrahend);
else if (exp_delta > 0) else if (exp_delta > 0)
m_mpz_manager.machine_div_rem(subtrahend, m_powers2((unsigned)exp_delta), subtrahend, sticky_rem); m_mpz_manager.machine_div_rem(subtrahend, m_powers2((unsigned)exp_delta), subtrahend, sticky_rem);
else { else {
SASSERT(exp_delta < 0); SASSERT(exp_delta < 0);
exp_delta = -exp_delta; exp_delta = -exp_delta;
@ -1356,7 +1356,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
m_mpz_manager.inc(subtrahend); m_mpz_manager.inc(subtrahend);
TRACE("mpf_dbg_rem", tout << "aligned subtrahend=" << m_mpz_manager.to_string(subtrahend) << std::endl;); TRACE("mpf_dbg_rem", tout << "aligned subtrahend=" << m_mpz_manager.to_string(subtrahend) << std::endl;);
} }
m_mpz_manager.sub(minuend, subtrahend, X_YQ_sig); m_mpz_manager.sub(minuend, subtrahend, X_YQ_sig);
TRACE("mpf_dbg_rem", tout << "X_YQ_sig'=" << m_mpz_manager.to_string(X_YQ_sig) << std::endl;); TRACE("mpf_dbg_rem", tout << "X_YQ_sig'=" << m_mpz_manager.to_string(X_YQ_sig) << std::endl;);
@ -1374,7 +1374,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
tout << "subtrahend=" << m_mpz_manager.to_string(subtrahend) << std::endl; tout << "subtrahend=" << m_mpz_manager.to_string(subtrahend) << std::endl;
tout << "X_YQ_sgn=" << X_YQ_sgn << std::endl; tout << "X_YQ_sgn=" << X_YQ_sgn << std::endl;
tout << "X_YQ_exp=" << X_YQ_exp << std::endl; tout << "X_YQ_exp=" << X_YQ_exp << std::endl;
tout << "X_YQ_sig=" << m_mpz_manager.to_string(X_YQ_sig) << std::endl; tout << "X_YQ_sig=" << m_mpz_manager.to_string(X_YQ_sig) << std::endl;
tout << "X-YQ=" << to_string_hexfloat(X_YQ_sgn, X_YQ_exp, X_YQ_sig, ebits, sbits, sbits-1) << std::endl;); tout << "X-YQ=" << to_string_hexfloat(X_YQ_sgn, X_YQ_exp, X_YQ_sig, ebits, sbits, sbits-1) << std::endl;);
// `sbits-1' extra bits in X_YQ_sig // `sbits-1' extra bits in X_YQ_sig
@ -1384,7 +1384,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
TRACE("mpf_dbg_rem", tout << "final sticky=" << m_mpz_manager.to_string(rnd_bits) << std::endl; ); TRACE("mpf_dbg_rem", tout << "final sticky=" << m_mpz_manager.to_string(rnd_bits) << std::endl; );
// Round to nearest, ties to even. // Round to nearest, ties to even.
if (m_mpz_manager.eq(rnd_bits, mpz(32))) { // tie. if (m_mpz_manager.eq(rnd_bits, mpz(32))) { // tie.
if (m_mpz_manager.is_odd(X_YQ_sig)) { if (m_mpz_manager.is_odd(X_YQ_sig)) {
m_mpz_manager.inc(X_YQ_sig); m_mpz_manager.inc(X_YQ_sig);
} }
@ -1430,7 +1430,7 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
mpf_exp_t D; mpf_exp_t D;
do { do {
if (ST0.exponent() < ST1.exponent() - 1) { if (ST0.exponent() < ST1.exponent() - 1) {
D = 0; D = 0;
} }
else { else {
D = ST0.exponent() - ST1.exponent(); D = ST0.exponent() - ST1.exponent();
@ -1889,7 +1889,7 @@ void mpf_manager::round(mpf_rounding_mode rm, mpf & o) {
const mpz & p_m1 = m_powers2(o.sbits+2); const mpz & p_m1 = m_powers2(o.sbits+2);
const mpz & p_m2 = m_powers2(o.sbits+3); const mpz & p_m2 = m_powers2(o.sbits+3);
(void)p_m1; (void)p_m1;
TRACE("mpf_dbg", tout << "p_m1 = " << m_mpz_manager.to_string(p_m1) << std::endl << TRACE("mpf_dbg", tout << "p_m1 = " << m_mpz_manager.to_string(p_m1) << std::endl <<
"p_m2 = " << m_mpz_manager.to_string(p_m2) << std::endl;); "p_m2 = " << m_mpz_manager.to_string(p_m2) << std::endl;);