From a97358965be476b2e2fae224002ba4890646cf34 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Nov 2016 16:28:49 +0000 Subject: [PATCH 1/2] Fixed interruption/cancelation issue in rewriter. --- src/ast/rewriter/rewriter_def.h | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index cd6a63acc..61d177809 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -27,7 +27,7 @@ void rewriter_tpl::process_var(var * v) { SASSERT(v->get_sort() == m().get_sort(m_r)); if (ProofGen) { result_pr_stack().push_back(m_pr); - m_pr = 0; + m_pr = 0; } set_new_child_flag(v); TRACE("rewriter", tout << mk_ismt2_pp(v, m()) << " -> " << m_r << "\n";); @@ -43,7 +43,7 @@ void rewriter_tpl::process_var(var * v) { if (r != 0) { SASSERT(v->get_sort() == m().get_sort(r)); if (!is_ground(r) && m_shifts[index] != m_bindings.size()) { - + unsigned shift_amount = m_bindings.size() - m_shifts[index]; expr_ref tmp(m()); m_shifter(r, shift_amount, tmp); @@ -195,9 +195,9 @@ void rewriter_tpl::process_app(app * t, frame & fr) { // this optimization is only used when Proof generation is disabled. if (f->is_associative() && t->get_ref_count() <= 1 && frame_stack().size() > 1) { frame & prev_fr = frame_stack()[frame_stack().size() - 2]; - if (is_app(prev_fr.m_curr) && - to_app(prev_fr.m_curr)->get_decl() == f && - prev_fr.m_state == PROCESS_CHILDREN && + if (is_app(prev_fr.m_curr) && + to_app(prev_fr.m_curr)->get_decl() == f && + prev_fr.m_state == PROCESS_CHILDREN && flat_assoc(f)) { frame_stack().pop_back(); set_new_child_flag(t); @@ -223,7 +223,7 @@ void rewriter_tpl::process_app(app * t, frame & fr) { } 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)); - TRACE("reduce_app", + TRACE("reduce_app", tout << mk_ismt2_pp(t, m()) << "\n"; tout << "st: " << st; if (m_r) tout << " --->\n" << mk_ismt2_pp(m_r, m()); @@ -296,11 +296,11 @@ void rewriter_tpl::process_app(app * t, frame & fr) { expr * def; proof * def_pr; quantifier * def_q; - // When get_macro succeeds, then + // When get_macro succeeds, then // we know that: // forall X. f(X) = def[X] // and def_pr is a proof for this quantifier. - // + // // Remark: def_q is only used for proof generation. // It is the quantifier forall X. f(X) = def[X] if (get_macro(f, def, def_q, def_pr)) { @@ -318,7 +318,7 @@ void rewriter_tpl::process_app(app * t, frame & fr) { if (ProofGen) { NOT_IMPLEMENTED_YET(); // 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()); // subst.set_bindings(new_num_args, new_args); // expr_ref r2(m()); @@ -333,7 +333,7 @@ void rewriter_tpl::process_app(app * t, frame & fr) { unsigned i = num_args; while (i > 0) { --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); } result_stack().push_back(def); @@ -465,7 +465,7 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { } else { new_pats = q->get_patterns(); - new_no_pats = q->get_no_patterns(); + new_no_pats = q->get_no_patterns(); } 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); @@ -559,7 +559,7 @@ template void rewriter_tpl::display_bindings(std::ostream& out) { out << "bindings:\n"; 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"; } } @@ -596,6 +596,7 @@ template template void rewriter_tpl::main_loop(expr * t, expr_ref & result, proof_ref & result_pr) { if (m_cancel_check && m().canceled()) { + reset(); throw rewriter_exception(m().limit().get_cancel_msg()); } SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size()); @@ -630,6 +631,7 @@ void rewriter_tpl::resume_core(expr_ref & result, proof_ref & result_pr) SASSERT(!frame_stack().empty()); while (!frame_stack().empty()) { if (m_cancel_check && m().canceled()) { + reset(); throw rewriter_exception(m().limit().get_cancel_msg()); } SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size()); From b138a0f6d3f5c309f330c4e7969b520a6ff0e0c8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 17 Nov 2016 16:36:39 +0000 Subject: [PATCH 2/2] Cleaned up hacky rewriter cancelation fix in theory_fpa. --- src/smt/theory_fpa.cpp | 118 +++++++++-------------------------------- 1 file changed, 26 insertions(+), 92 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 57cd6a914..a3bf77180 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -238,14 +238,7 @@ namespace smt { 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) }; res = m_bv_util.mk_concat(3, cargs); - - try { - m_th_rw((expr_ref&)res); - } - catch (rewriter_exception &) { - m_th_rw.reset(); - throw; - } + m_th_rw((expr_ref&)res); } else { 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;); expr_ref res(m); proof_ref pr(m); - try { - m_rw(e, res); - m_th_rw(res, res); - } - catch (rewriter_exception &) { - m_rw.reset(); - m_th_rw.reset(); - throw; - } + m_rw(e, res); + m_th_rw(res, res); SASSERT(is_app(res)); SASSERT(m.is_bool(res)); return res; @@ -323,41 +309,28 @@ namespace smt { expr_ref e_conv(m), res(m); proof_ref pr(m); - try { - m_rw(e, e_conv); - } - catch (rewriter_exception &) { - m_rw.reset(); - throw; - } + m_rw(e, e_conv); 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;); - try { - if (m_fpa_util.is_rm(e)) { - SASSERT(m_fpa_util.is_bv2rm(e_conv)); - expr_ref bv_rm(m); - m_th_rw(to_app(e_conv)->get_arg(0), 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(); + if (m_fpa_util.is_rm(e)) { + SASSERT(m_fpa_util.is_bv2rm(e_conv)); + expr_ref bv_rm(m); + m_th_rw(to_app(e_conv)->get_arg(0), bv_rm); + res = m_fpa_util.mk_bv2rm(bv_rm); } - catch (rewriter_exception &) - { - m_th_rw.reset(); - throw; + 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(); return res; } @@ -366,15 +339,8 @@ namespace smt { SASSERT(to_app(e)->get_family_id() == get_family_id()); /* This is for the conversion functions fp.to_* */ expr_ref res(get_manager()); - try { - m_rw(e, res); - m_th_rw(res, res); - } - catch (rewriter_exception &) { - m_rw.reset(); - m_th_rw.reset(); - throw; - } + m_rw(e, res); + m_th_rw(res, res); return res; } @@ -432,13 +398,7 @@ namespace smt { } m_converter.m_extra_assertions.reset(); - try { - m_th_rw(res); - } - catch (rewriter_exception &) { - m_th_rw.reset(); - throw; - } + m_th_rw(res); CTRACE("t_fpa", !m.is_true(res), tout << "side condition: " << mk_ismt2_pp(res, m) << std::endl;); return res; @@ -481,15 +441,7 @@ namespace smt { expr_ref bv_atom(convert_atom(atom)); expr_ref bv_atom_w_side_c(m), atom_eq(m); bv_atom_w_side_c = m.mk_and(bv_atom, mk_side_conditions()); - - try { - m_th_rw(bv_atom_w_side_c); - } - catch (rewriter_exception &) { - m_th_rw.reset(); - throw; - } - + m_th_rw(bv_atom_w_side_c); atom_eq = m.mk_eq(atom, bv_atom_w_side_c); assert_cnstr(atom_eq); return true; @@ -600,13 +552,7 @@ namespace smt { else c = m.mk_eq(xc, yc); - try { - m_th_rw(c); - } - catch (rewriter_exception &) { - m_th_rw.reset(); - throw; - } + m_th_rw(c); expr_ref xe_eq_ye(m), c_eq_iff(m); xe_eq_ye = m.mk_eq(xe, ye); @@ -652,13 +598,7 @@ namespace smt { c = m.mk_not(xc_eq_yc); } - try { - m_th_rw(c); - } - catch (rewriter_exception &) { - m_th_rw.reset(); - throw; - } + m_th_rw(c); expr_ref xe_eq_ye(m), not_xe_eq_ye(m), c_eq_iff(m); xe_eq_ye = m.mk_eq(xe, ye); @@ -697,13 +637,7 @@ namespace smt { expr_ref cnstr(m); cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(converted, e); - try { - m_th_rw(cnstr); - } - catch (rewriter_exception &) { - m_th_rw.reset(); - throw; - } + m_th_rw(cnstr); assert_cnstr(cnstr); }