mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 04:11:21 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-11-19 08:09:55 -08:00
commit a5bae72bdf
2 changed files with 40 additions and 104 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/ast/rewriter/rewriter_def.h
View file

@ -27,7 +27,7 @@ void rewriter_tpl<Config>::process_var(var * v) {
SASSERT(v->get_sort() == m().get_sort(m_r)); SASSERT(v->get_sort() == m().get_sort(m_r));
if (ProofGen) { if (ProofGen) {
result_pr_stack().push_back(m_pr); result_pr_stack().push_back(m_pr);
m_pr = 0; m_pr = 0;
} }
set_new_child_flag(v); set_new_child_flag(v);
TRACE("rewriter", tout << mk_ismt2_pp(v, m()) << " -> " << m_r << "\n";); TRACE("rewriter", tout << mk_ismt2_pp(v, m()) << " -> " << m_r << "\n";);
@ -43,7 +43,7 @@ void rewriter_tpl<Config>::process_var(var * v) {
if (r != 0) { if (r != 0) {
SASSERT(v->get_sort() == m().get_sort(r)); SASSERT(v->get_sort() == m().get_sort(r));
if (!is_ground(r) && m_shifts[index] != m_bindings.size()) { if (!is_ground(r) && m_shifts[index] != m_bindings.size()) {
unsigned shift_amount = m_bindings.size() - m_shifts[index]; unsigned shift_amount = m_bindings.size() - m_shifts[index];
expr_ref tmp(m()); expr_ref tmp(m());
m_shifter(r, shift_amount, tmp); m_shifter(r, shift_amount, tmp);
@ -195,9 +195,9 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
// this optimization is only used when Proof generation is disabled. // this optimization is only used when Proof generation is disabled.
if (f->is_associative() && t->get_ref_count() <= 1 && frame_stack().size() > 1) { if (f->is_associative() && t->get_ref_count() <= 1 && frame_stack().size() > 1) {
frame & prev_fr = frame_stack()[frame_stack().size() - 2]; frame & prev_fr = frame_stack()[frame_stack().size() - 2];
if (is_app(prev_fr.m_curr) && if (is_app(prev_fr.m_curr) &&
to_app(prev_fr.m_curr)->get_decl() == f && to_app(prev_fr.m_curr)->get_decl() == f &&
prev_fr.m_state == PROCESS_CHILDREN && prev_fr.m_state == PROCESS_CHILDREN &&
flat_assoc(f)) { flat_assoc(f)) {
frame_stack().pop_back(); frame_stack().pop_back();
set_new_child_flag(t); set_new_child_flag(t);
@ -223,7 +223,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
} }
br_status st = m_cfg.reduce_app(f, new_num_args, new_args, m_r, m_pr2); br_status st = m_cfg.reduce_app(f, new_num_args, new_args, m_r, m_pr2);
SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t)); SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
TRACE("reduce_app", TRACE("reduce_app",
tout << mk_ismt2_pp(t, m()) << "\n"; tout << mk_ismt2_pp(t, m()) << "\n";
tout << "st: " << st; tout << "st: " << st;
if (m_r) tout << " --->\n" << mk_ismt2_pp(m_r, m()); if (m_r) tout << " --->\n" << mk_ismt2_pp(m_r, m());
@ -296,11 +296,11 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
expr * def; expr * def;
proof * def_pr; proof * def_pr;
quantifier * def_q; quantifier * def_q;
// When get_macro succeeds, then // When get_macro succeeds, then
// we know that: // we know that:
// forall X. f(X) = def[X] // forall X. f(X) = def[X]
// and def_pr is a proof for this quantifier. // and def_pr is a proof for this quantifier.
// //
// Remark: def_q is only used for proof generation. // Remark: def_q is only used for proof generation.
// It is the quantifier forall X. f(X) = def[X] // It is the quantifier forall X. f(X) = def[X]
if (get_macro(f, def, def_q, def_pr)) { if (get_macro(f, def, def_q, def_pr)) {
@ -318,7 +318,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
if (ProofGen) { if (ProofGen) {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
// We do not support the use of bindings in proof generation mode. // We do not support the use of bindings in proof generation mode.
// Thus we have to apply the subsitution here, and // Thus we have to apply the subsitution here, and
// beta_reducer subst(m()); // beta_reducer subst(m());
// subst.set_bindings(new_num_args, new_args); // subst.set_bindings(new_num_args, new_args);
// expr_ref r2(m()); // expr_ref r2(m());
@ -333,7 +333,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
unsigned i = num_args; unsigned i = num_args;
while (i > 0) { while (i > 0) {
--i; --i;
m_bindings.push_back(new_args[i]); // num_args - i - 1]); m_bindings.push_back(new_args[i]); // num_args - i - 1]);
m_shifts.push_back(sz); m_shifts.push_back(sz);
} }
result_stack().push_back(def); result_stack().push_back(def);
@ -465,7 +465,7 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
} }
else { else {
new_pats = q->get_patterns(); new_pats = q->get_patterns();
new_no_pats = q->get_no_patterns(); new_no_pats = q->get_no_patterns();
} }
if (ProofGen) { if (ProofGen) {
quantifier * new_q = m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body); quantifier * new_q = m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body);
@ -559,7 +559,7 @@ template<typename Config>
void rewriter_tpl<Config>::display_bindings(std::ostream& out) { void rewriter_tpl<Config>::display_bindings(std::ostream& out) {
out << "bindings:\n"; out << "bindings:\n";
for (unsigned i = 0; i < m_bindings.size(); i++) { for (unsigned i = 0; i < m_bindings.size(); i++) {
if (m_bindings[i]) if (m_bindings[i])
out << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n"; out << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";
} }
} }
@ -596,6 +596,7 @@ template<typename Config>
template<bool ProofGen> template<bool ProofGen>
void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & result_pr) { void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & result_pr) {
if (m_cancel_check && m().canceled()) { if (m_cancel_check && m().canceled()) {
reset();
throw rewriter_exception(m().limit().get_cancel_msg()); throw rewriter_exception(m().limit().get_cancel_msg());
} }
SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size()); SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
@ -630,6 +631,7 @@ void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr)
SASSERT(!frame_stack().empty()); SASSERT(!frame_stack().empty());
while (!frame_stack().empty()) { while (!frame_stack().empty()) {
if (m_cancel_check && m().canceled()) { if (m_cancel_check && m().canceled()) {
reset();
throw rewriter_exception(m().limit().get_cancel_msg()); throw rewriter_exception(m().limit().get_cancel_msg());
} }
SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size()); SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());

118
src/smt/theory_fpa.cpp
View file

@ -238,14 +238,7 @@ namespace smt {
if (m_fpa_util.is_fp(e)) { if (m_fpa_util.is_fp(e)) {
expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) }; expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };
res = m_bv_util.mk_concat(3, cargs); res = m_bv_util.mk_concat(3, cargs);
m_th_rw((expr_ref&)res);
try {
m_th_rw((expr_ref&)res);
}
catch (rewriter_exception &) {
m_th_rw.reset();
throw;
}
} }
else { else {
sort * es = m.get_sort(e); sort * es = m.get_sort(e);
@ -302,15 +295,8 @@ namespace smt {
TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, get_manager()) << std::endl;); TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, get_manager()) << std::endl;);
expr_ref res(m); expr_ref res(m);
proof_ref pr(m); proof_ref pr(m);
try { m_rw(e, res);
m_rw(e, res); m_th_rw(res, res);
m_th_rw(res, res);
}
catch (rewriter_exception &) {
m_rw.reset();
m_th_rw.reset();
throw;
}
SASSERT(is_app(res)); SASSERT(is_app(res));
SASSERT(m.is_bool(res)); SASSERT(m.is_bool(res));
return res; return res;
@ -323,41 +309,28 @@ namespace smt {
expr_ref e_conv(m), res(m); expr_ref e_conv(m), res(m);
proof_ref pr(m); proof_ref pr(m);
try { m_rw(e, e_conv);
m_rw(e, e_conv);
}
catch (rewriter_exception &) {
m_rw.reset();
throw;
}
TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << std::endl; TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << std::endl;
tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << std::endl;); tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << std::endl;);
try { if (m_fpa_util.is_rm(e)) {
if (m_fpa_util.is_rm(e)) { SASSERT(m_fpa_util.is_bv2rm(e_conv));
SASSERT(m_fpa_util.is_bv2rm(e_conv)); expr_ref bv_rm(m);
expr_ref bv_rm(m); m_th_rw(to_app(e_conv)->get_arg(0), bv_rm);
m_th_rw(to_app(e_conv)->get_arg(0), bv_rm); res = m_fpa_util.mk_bv2rm(bv_rm);
res = m_fpa_util.mk_bv2rm(bv_rm);
}
else if (m_fpa_util.is_float(e)) {
SASSERT(m_fpa_util.is_fp(e_conv));
expr_ref sgn(m), sig(m), exp(m);
m_converter.split_fp(e_conv, sgn, exp, sig);
m_th_rw(sgn);
m_th_rw(exp);
m_th_rw(sig);
res = m_fpa_util.mk_fp(sgn, exp, sig);
}
else
UNREACHABLE();
} }
catch (rewriter_exception &) else if (m_fpa_util.is_float(e)) {
{ SASSERT(m_fpa_util.is_fp(e_conv));
m_th_rw.reset(); expr_ref sgn(m), sig(m), exp(m);
throw; m_converter.split_fp(e_conv, sgn, exp, sig);
m_th_rw(sgn);
m_th_rw(exp);
m_th_rw(sig);
res = m_fpa_util.mk_fp(sgn, exp, sig);
} }
else
UNREACHABLE();
return res; return res;
} }
@ -366,15 +339,8 @@ namespace smt {
SASSERT(to_app(e)->get_family_id() == get_family_id()); SASSERT(to_app(e)->get_family_id() == get_family_id());
/* This is for the conversion functions fp.to_* */ /* This is for the conversion functions fp.to_* */
expr_ref res(get_manager()); expr_ref res(get_manager());
try { m_rw(e, res);
m_rw(e, res); m_th_rw(res, res);
m_th_rw(res, res);
}
catch (rewriter_exception &) {
m_rw.reset();
m_th_rw.reset();
throw;
}
return res; return res;
} }
@ -432,13 +398,7 @@ namespace smt {
} }
m_converter.m_extra_assertions.reset(); m_converter.m_extra_assertions.reset();
try { m_th_rw(res);
m_th_rw(res);
}
catch (rewriter_exception &) {
m_th_rw.reset();
throw;
}
CTRACE("t_fpa", !m.is_true(res), tout << "side condition: " << mk_ismt2_pp(res, m) << std::endl;); CTRACE("t_fpa", !m.is_true(res), tout << "side condition: " << mk_ismt2_pp(res, m) << std::endl;);
return res; return res;
@ -481,15 +441,7 @@ namespace smt {
expr_ref bv_atom(convert_atom(atom)); expr_ref bv_atom(convert_atom(atom));
expr_ref bv_atom_w_side_c(m), atom_eq(m); expr_ref bv_atom_w_side_c(m), atom_eq(m);
bv_atom_w_side_c = m.mk_and(bv_atom, mk_side_conditions()); bv_atom_w_side_c = m.mk_and(bv_atom, mk_side_conditions());
m_th_rw(bv_atom_w_side_c);
try {
m_th_rw(bv_atom_w_side_c);
}
catch (rewriter_exception &) {
m_th_rw.reset();
throw;
}
atom_eq = m.mk_eq(atom, bv_atom_w_side_c); atom_eq = m.mk_eq(atom, bv_atom_w_side_c);
assert_cnstr(atom_eq); assert_cnstr(atom_eq);
return true; return true;
@ -600,13 +552,7 @@ namespace smt {
else else
c = m.mk_eq(xc, yc); c = m.mk_eq(xc, yc);
try { m_th_rw(c);
m_th_rw(c);
}
catch (rewriter_exception &) {
m_th_rw.reset();
throw;
}
expr_ref xe_eq_ye(m), c_eq_iff(m); expr_ref xe_eq_ye(m), c_eq_iff(m);
xe_eq_ye = m.mk_eq(xe, ye); xe_eq_ye = m.mk_eq(xe, ye);
@ -652,13 +598,7 @@ namespace smt {
c = m.mk_not(xc_eq_yc); c = m.mk_not(xc_eq_yc);
} }
try { m_th_rw(c);
m_th_rw(c);
}
catch (rewriter_exception &) {
m_th_rw.reset();
throw;
}
expr_ref xe_eq_ye(m), not_xe_eq_ye(m), c_eq_iff(m); expr_ref xe_eq_ye(m), not_xe_eq_ye(m), c_eq_iff(m);
xe_eq_ye = m.mk_eq(xe, ye); xe_eq_ye = m.mk_eq(xe, ye);
@ -697,13 +637,7 @@ namespace smt {
expr_ref cnstr(m); expr_ref cnstr(m);
cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(converted, e); cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(converted, e);
try { m_th_rw(cnstr);
m_th_rw(cnstr);
}
catch (rewriter_exception &) {
m_th_rw.reset();
throw;
}
assert_cnstr(cnstr); assert_cnstr(cnstr);
} }