diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 5222c219f..9786ccc8d 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -33,7 +33,7 @@ protected: if (m_cancel) throw tactic_exception(TACTIC_CANCELED_MSG); } - + public: binary_tactical(tactic * t1, tactic * t2): m_t1(t1), @@ -44,7 +44,7 @@ public: m_t1->inc_ref(); m_t2->inc_ref(); } - + virtual ~binary_tactical() { tactic * t1 = m_t1; tactic * t2 = m_t2; @@ -56,32 +56,32 @@ public: t1->dec_ref(); t2->dec_ref(); } - + virtual void updt_params(params_ref const & p) { m_t1->updt_params(p); m_t2->updt_params(p); } - + virtual void collect_param_descrs(param_descrs & r) { m_t1->collect_param_descrs(r); m_t2->collect_param_descrs(r); } - + virtual void collect_statistics(statistics & st) const { m_t1->collect_statistics(st); m_t2->collect_statistics(st); } - virtual void reset_statistics() { + virtual void reset_statistics() { m_t1->reset_statistics(); m_t2->reset_statistics(); } - + virtual void cleanup() { m_t1->cleanup(); m_t2->cleanup(); } - + virtual void reset() { m_t1->reset(); m_t2->reset(); @@ -114,7 +114,7 @@ protected: } template - tactic * translate_core(ast_manager & m) { + tactic * translate_core(ast_manager & m) { tactic * new_t1 = m_t1->translate(m); tactic * new_t2 = m_t2->translate(m); return alloc(T, new_t1, new_t2); @@ -132,96 +132,96 @@ public: and_then_tactical(tactic * t1, tactic * t2):binary_tactical(t1, t2) {} virtual ~and_then_tactical() {} - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, expr_dependency_ref & core) { bool models_enabled = in->models_enabled(); bool proofs_enabled = in->proofs_enabled(); bool cores_enabled = in->unsat_core_enabled(); - ast_manager & m = in->m(); + ast_manager & m = in->m(); goal_ref_buffer r1; - model_converter_ref mc1; - proof_converter_ref pc1; - expr_dependency_ref core1(m); - result.reset(); - mc = 0; - pc = 0; + model_converter_ref mc1; + proof_converter_ref pc1; + expr_dependency_ref core1(m); + result.reset(); + mc = 0; + pc = 0; core = 0; - m_t1->operator()(in, r1, mc1, pc1, core1); + m_t1->operator()(in, r1, mc1, pc1, core1); SASSERT(!is_decided(r1) || (!pc1 && !core1)); // the pc and core of decided goals is 0 - unsigned r1_size = r1.size(); - SASSERT(r1_size > 0); - checkpoint(); - if (r1_size == 1) { + unsigned r1_size = r1.size(); + SASSERT(r1_size > 0); + checkpoint(); + if (r1_size == 1) { if (r1[0]->is_decided()) { - result.push_back(r1[0]); - if (models_enabled) mc = mc1; + result.push_back(r1[0]); + if (models_enabled) mc = mc1; SASSERT(!pc); SASSERT(!core); - return; - } - goal_ref r1_0 = r1[0]; - m_t2->operator()(r1_0, result, mc, pc, core); - if (models_enabled) mc = concat(mc1.get(), mc.get()); - if (proofs_enabled) pc = concat(pc1.get(), pc.get()); - if (cores_enabled) core = m.mk_join(core1.get(), core); - } - else { - if (cores_enabled) core = core1; - proof_converter_ref_buffer pc_buffer; - model_converter_ref_buffer mc_buffer; - sbuffer sz_buffer; - goal_ref_buffer r2; - for (unsigned i = 0; i < r1_size; i++) { - checkpoint(); - goal_ref g = r1[i]; - r2.reset(); - model_converter_ref mc2; - proof_converter_ref pc2; - expr_dependency_ref core2(m); - m_t2->operator()(g, r2, mc2, pc2, core2); + return; + } + goal_ref r1_0 = r1[0]; + m_t2->operator()(r1_0, result, mc, pc, core); + if (models_enabled) mc = concat(mc1.get(), mc.get()); + if (proofs_enabled) pc = concat(pc1.get(), pc.get()); + if (cores_enabled) core = m.mk_join(core1.get(), core); + } + else { + if (cores_enabled) core = core1; + proof_converter_ref_buffer pc_buffer; + model_converter_ref_buffer mc_buffer; + sbuffer sz_buffer; + goal_ref_buffer r2; + for (unsigned i = 0; i < r1_size; i++) { + checkpoint(); + goal_ref g = r1[i]; + r2.reset(); + model_converter_ref mc2; + proof_converter_ref pc2; + expr_dependency_ref core2(m); + m_t2->operator()(g, r2, mc2, pc2, core2); if (is_decided(r2)) { SASSERT(r2.size() == 1); - if (is_decided_sat(r2)) { - // found solution... + if (is_decided_sat(r2)) { + // found solution... result.push_back(r2[0]); if (models_enabled) { - // mc2 contains the actual model - model_ref md; + // mc2 contains the actual model + model_ref md; md = alloc(model, m); apply(mc2, md, 0); apply(mc1, md, i); - mc = model2model_converter(md.get()); + mc = model2model_converter(md.get()); } SASSERT(!pc); SASSERT(!core); - return; - } - else { - SASSERT(is_decided_unsat(r2)); + return; + } + else { + SASSERT(is_decided_unsat(r2)); // the proof and unsat core of a decided_unsat goal are stored in the node itself. // pc2 and core2 must be 0. SASSERT(!pc2); SASSERT(!core2); if (models_enabled) mc_buffer.push_back(0); if (proofs_enabled) pc_buffer.push_back(proof2proof_converter(m, r2[0]->pr(0))); - if (models_enabled || proofs_enabled) sz_buffer.push_back(0); + if (models_enabled || proofs_enabled) sz_buffer.push_back(0); if (cores_enabled) core = m.mk_join(core.get(), r2[0]->dep(0)); - } - } - else { - result.append(r2.size(), r2.c_ptr()); - if (models_enabled) mc_buffer.push_back(mc2.get()); - if (proofs_enabled) pc_buffer.push_back(pc2.get()); - if (models_enabled || proofs_enabled) sz_buffer.push_back(r2.size()); - if (cores_enabled) core = m.mk_join(core.get(), core2.get()); - } + } + } + else { + result.append(r2.size(), r2.c_ptr()); + if (models_enabled) mc_buffer.push_back(mc2.get()); + if (proofs_enabled) pc_buffer.push_back(pc2.get()); + if (models_enabled || proofs_enabled) sz_buffer.push_back(r2.size()); + if (cores_enabled) core = m.mk_join(core.get(), core2.get()); + } } - - if (result.empty()) { - // all subgoals were shown to be unsat. + + if (result.empty()) { + // all subgoals were shown to be unsat. // create an decided_unsat goal with the proof in->reset_all(); proof_ref pr(m); @@ -234,8 +234,8 @@ public: SASSERT(!mc); SASSERT(!pc); SASSERT(!core); } else { - if (models_enabled) mc = concat(mc1.get(), mc_buffer.size(), mc_buffer.c_ptr(), sz_buffer.c_ptr()); - if (proofs_enabled) pc = concat(pc1.get(), pc_buffer.size(), pc_buffer.c_ptr(), sz_buffer.c_ptr()); + if (models_enabled) mc = concat(mc1.get(), mc_buffer.size(), mc_buffer.c_ptr(), sz_buffer.c_ptr()); + if (proofs_enabled) pc = concat(pc1.get(), pc_buffer.size(), pc_buffer.c_ptr(), sz_buffer.c_ptr()); SASSERT(cores_enabled || core == 0); } } @@ -339,14 +339,14 @@ public: for (; it != end; ++it) (*it)->updt_params(p); } - + virtual void collect_param_descrs(param_descrs & r) { ptr_vector::iterator it = m_ts.begin(); ptr_vector::iterator end = m_ts.end(); for (; it != end; ++it) (*it)->collect_param_descrs(r); } - + virtual void collect_statistics(statistics & st) const { ptr_vector::const_iterator it = m_ts.begin(); ptr_vector::const_iterator end = m_ts.end(); @@ -354,20 +354,20 @@ public: (*it)->collect_statistics(st); } - virtual void reset_statistics() { + virtual void reset_statistics() { ptr_vector::const_iterator it = m_ts.begin(); ptr_vector::const_iterator end = m_ts.end(); for (; it != end; ++it) (*it)->reset_statistics(); } - + virtual void cleanup() { ptr_vector::iterator it = m_ts.begin(); ptr_vector::iterator end = m_ts.end(); for (; it != end; ++it) (*it)->cleanup(); } - + virtual void reset() { ptr_vector::iterator it = m_ts.begin(); ptr_vector::iterator end = m_ts.end(); @@ -409,7 +409,7 @@ protected: } template - tactic * translate_core(ast_manager & m) { + tactic * translate_core(ast_manager & m) { ptr_buffer new_ts; ptr_vector::iterator it = m_ts.begin(); ptr_vector::iterator end = m_ts.end(); @@ -429,10 +429,10 @@ public: virtual ~or_else_tactical() {} - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, expr_dependency_ref & core) { goal orig(*(in.get())); unsigned sz = m_ts.size(); @@ -525,10 +525,10 @@ public: par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) {} virtual ~par_tactical() {} - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, expr_dependency_ref & core) { bool use_seq; #ifdef _NO_OMP_ @@ -541,9 +541,9 @@ public: or_else_tactical::operator()(in, result, mc, pc, core); return; } - + ast_manager & m = in->m(); - + scoped_ptr_vector managers; goal_ref_vector in_copies; tactic_ref_vector ts; @@ -560,28 +560,27 @@ public: par_exception_kind ex_kind = DEFAULT_EX; std::string ex_msg; unsigned error_code = 0; - + #pragma omp parallel for for (int i = 0; i < static_cast(sz); i++) { goal_ref_buffer _result; - model_converter_ref _mc; - proof_converter_ref _pc; + model_converter_ref _mc; + proof_converter_ref _pc; expr_dependency_ref _core(*(managers[i])); - + goal_ref in_copy = in_copies[i]; tactic & t = *(ts.get(i)); - + try { t(in_copy, _result, _mc, _pc, _core); - bool successful = is_decided(_result); bool first = false; #pragma omp critical (par_tactical) { - if (successful && finished_id == UINT_MAX) { + if (finished_id == UINT_MAX) { finished_id = i; first = true; } - } + } if (first) { for (unsigned j = 0; j < sz; j++) { if (static_cast(i) != j) @@ -625,7 +624,7 @@ public: throw default_exception(ex_msg.c_str()); } } - } + } virtual tactic * translate(ast_manager & m) { return translate_core(m); } }; @@ -654,10 +653,10 @@ public: par_and_then_tactical(tactic * t1, tactic * t2):and_then_tactical(t1, t2) {} virtual ~par_and_then_tactical() {} - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, expr_dependency_ref & core) { bool use_seq; #ifdef _NO_OMP_ @@ -675,36 +674,36 @@ public: bool proofs_enabled = in->proofs_enabled(); bool cores_enabled = in->unsat_core_enabled(); - ast_manager & m = in->m(); + ast_manager & m = in->m(); goal_ref_buffer r1; - model_converter_ref mc1; - proof_converter_ref pc1; - expr_dependency_ref core1(m); - result.reset(); - mc = 0; - pc = 0; + model_converter_ref mc1; + proof_converter_ref pc1; + expr_dependency_ref core1(m); + result.reset(); + mc = 0; + pc = 0; core = 0; - m_t1->operator()(in, r1, mc1, pc1, core1); + m_t1->operator()(in, r1, mc1, pc1, core1); SASSERT(!is_decided(r1) || (!pc1 && !core1)); // the pc and core of decided goals is 0 - unsigned r1_size = r1.size(); - SASSERT(r1_size > 0); - checkpoint(); - if (r1_size == 1) { + unsigned r1_size = r1.size(); + SASSERT(r1_size > 0); + checkpoint(); + if (r1_size == 1) { // Only one subgoal created... no need for parallelism if (r1[0]->is_decided()) { - result.push_back(r1[0]); - if (models_enabled) mc = mc1; + result.push_back(r1[0]); + if (models_enabled) mc = mc1; SASSERT(!pc); SASSERT(!core); - return; - } - goal_ref r1_0 = r1[0]; - m_t2->operator()(r1_0, result, mc, pc, core); - if (models_enabled) mc = concat(mc1.get(), mc.get()); - if (proofs_enabled) pc = concat(pc1.get(), pc.get()); - if (cores_enabled) core = m.mk_join(core1.get(), core); - } - else { - if (cores_enabled) core = core1; + return; + } + goal_ref r1_0 = r1[0]; + m_t2->operator()(r1_0, result, mc, pc, core); + if (models_enabled) mc = concat(mc1.get(), mc.get()); + if (proofs_enabled) pc = concat(pc1.get(), pc.get()); + if (cores_enabled) core = m.mk_join(core1.get(), core); + } + else { + if (cores_enabled) core = core1; scoped_ptr_vector managers; tactic_ref_vector ts2; @@ -718,8 +717,8 @@ public: ts2.push_back(m_t2->translate(*new_m)); } - proof_converter_ref_buffer pc_buffer; - model_converter_ref_buffer mc_buffer; + proof_converter_ref_buffer pc_buffer; + model_converter_ref_buffer mc_buffer; scoped_ptr_vector core_buffer; scoped_ptr_vector goals_vect; @@ -735,19 +734,19 @@ public: std::string ex_msg; #pragma omp parallel for - for (int i = 0; i < static_cast(r1_size); i++) { + for (int i = 0; i < static_cast(r1_size); i++) { ast_manager & new_m = *(managers[i]); goal_ref new_g = g_copies[i]; goal_ref_buffer r2; - model_converter_ref mc2; - proof_converter_ref pc2; - expr_dependency_ref core2(new_m); - + model_converter_ref mc2; + proof_converter_ref pc2; + expr_dependency_ref core2(new_m); + bool curr_failed = false; try { - ts2[i]->operator()(new_g, r2, mc2, pc2, core2); + ts2[i]->operator()(new_g, r2, mc2, pc2, core2); } catch (tactic_exception & ex) { #pragma omp critical (par_and_then_tactical) @@ -769,7 +768,7 @@ public: ex_kind = ERROR_EX; error_code = err.error_code(); } - } + } } catch (z3_exception & z3_ex) { #pragma omp critical (par_and_then_tactical) @@ -792,8 +791,8 @@ public: else { if (is_decided(r2)) { SASSERT(r2.size() == 1); - if (is_decided_sat(r2)) { - // found solution... + if (is_decided_sat(r2)) { + // found solution... bool first = false; #pragma omp critical (par_and_then_tactical) { @@ -812,24 +811,24 @@ public: SASSERT(r2.size() == 1); result.push_back(r2[0]->translate(translator)); if (models_enabled) { - // mc2 contains the actual model + // mc2 contains the actual model mc2 = mc2 ? mc2->translate(translator) : 0; - model_ref md; + model_ref md; md = alloc(model, m); apply(mc2, md, 0); apply(mc1, md, i); - mc = model2model_converter(md.get()); + mc = model2model_converter(md.get()); } SASSERT(!pc); SASSERT(!core); - } - } - else { - SASSERT(is_decided_unsat(r2)); + } + } + else { + SASSERT(is_decided_unsat(r2)); // the proof and unsat core of a decided_unsat goal are stored in the node itself. // pc2 and core2 must be 0. SASSERT(!pc2); SASSERT(!core2); - + if (models_enabled) mc_buffer.set(i, 0); if (proofs_enabled) { proof * pr = r2[0]->pr(0); @@ -840,9 +839,9 @@ public: *new_dep = r2[0]->dep(0); core_buffer.set(i, new_dep); } - } - } - else { + } + } + else { goal_ref_buffer * new_r2 = alloc(goal_ref_buffer); goals_vect.set(i, new_r2); new_r2->append(r2.size(), r2.c_ptr()); @@ -853,10 +852,10 @@ public: *new_dep = core2; core_buffer.set(i, new_dep); } - } + } } } - + if (failed) { switch (ex_kind) { case ERROR_EX: throw z3_error(error_code); @@ -870,7 +869,7 @@ public: return; core = 0; - sbuffer sz_buffer; + sbuffer sz_buffer; for (unsigned i = 0; i < r1_size; i++) { ast_translation translator(*(managers[i]), m, false); goal_ref_buffer * r = goals_vect[i]; @@ -896,7 +895,7 @@ public: } if (result.empty()) { - // all subgoals were shown to be unsat. + // all subgoals were shown to be unsat. // create an decided_unsat goal with the proof in->reset_all(); proof_ref pr(m); @@ -909,8 +908,8 @@ public: SASSERT(!mc); SASSERT(!pc); SASSERT(!core); } else { - if (models_enabled) mc = concat(mc1.get(), mc_buffer.size(), mc_buffer.c_ptr(), sz_buffer.c_ptr()); - if (proofs_enabled) pc = concat(pc1.get(), pc_buffer.size(), pc_buffer.c_ptr(), sz_buffer.c_ptr()); + if (models_enabled) mc = concat(mc1.get(), mc_buffer.size(), mc_buffer.c_ptr(), sz_buffer.c_ptr()); + if (proofs_enabled) pc = concat(pc1.get(), pc_buffer.size(), pc_buffer.c_ptr(), sz_buffer.c_ptr()); SASSERT(cores_enabled || core == 0); } } @@ -949,14 +948,14 @@ protected: } public: - unary_tactical(tactic * t): + unary_tactical(tactic * t): m_t(t), - m_cancel(false) { - SASSERT(t); - t->inc_ref(); - } + m_cancel(false) { + SASSERT(t); + t->inc_ref(); + } - virtual ~unary_tactical() { + virtual ~unary_tactical() { tactic * t = m_t; #pragma omp critical (tactic_cancel) { @@ -965,31 +964,31 @@ public: t->dec_ref(); } - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, expr_dependency_ref & core) { m_t->operator()(in, result, mc, pc, core); } - + virtual void cleanup(void) { m_t->cleanup(); } virtual void collect_statistics(statistics & st) const { m_t->collect_statistics(st); } - virtual void reset_statistics() { m_t->reset_statistics(); } + virtual void reset_statistics() { m_t->reset_statistics(); } virtual void updt_params(params_ref const & p) { m_t->updt_params(p); } virtual void collect_param_descrs(param_descrs & r) { m_t->collect_param_descrs(r); } virtual void reset() { m_t->reset(); } - virtual void set_logic(symbol const& l) { m_t->set_logic(l); } + virtual void set_logic(symbol const& l) { m_t->set_logic(l); } virtual void set_progress_callback(progress_callback * callback) { m_t->set_progress_callback(callback); } protected: - virtual void set_cancel(bool f) { + virtual void set_cancel(bool f) { m_cancel = f; - if (m_t) + if (m_t) m_t->set_cancel(f); } template - tactic * translate_core(ast_manager & m) { + tactic * translate_core(ast_manager & m) { tactic * new_t = m_t->translate(m); return alloc(T, new_t); } @@ -997,12 +996,12 @@ protected: class repeat_tactical : public unary_tactical { unsigned m_max_depth; - + void operator()(unsigned depth, - goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, expr_dependency_ref & core) { // TODO: implement a non-recursive version. if (depth > m_max_depth) { @@ -1017,93 +1016,93 @@ class repeat_tactical : public unary_tactical { bool proofs_enabled = in->proofs_enabled(); bool cores_enabled = in->unsat_core_enabled(); - ast_manager & m = in->m(); - goal_ref_buffer r1; - model_converter_ref mc1; - proof_converter_ref pc1; - expr_dependency_ref core1(m); - result.reset(); - mc = 0; - pc = 0; + ast_manager & m = in->m(); + goal_ref_buffer r1; + model_converter_ref mc1; + proof_converter_ref pc1; + expr_dependency_ref core1(m); + result.reset(); + mc = 0; + pc = 0; core = 0; { goal orig_in(in->m()); orig_in.copy_from(*(in.get())); - m_t->operator()(in, r1, mc1, pc1, core1); + m_t->operator()(in, r1, mc1, pc1, core1); if (is_equal(orig_in, *(in.get()))) { - result.push_back(r1[0]); - if (models_enabled) mc = mc1; - if (proofs_enabled) pc = pc1; - if (cores_enabled) core = core1; - return; + result.push_back(r1[0]); + if (models_enabled) mc = mc1; + if (proofs_enabled) pc = pc1; + if (cores_enabled) core = core1; + return; } } - unsigned r1_size = r1.size(); - SASSERT(r1_size > 0); - checkpoint(); - if (r1_size == 1) { + unsigned r1_size = r1.size(); + SASSERT(r1_size > 0); + checkpoint(); + if (r1_size == 1) { if (r1[0]->is_decided()) { - result.push_back(r1[0]); - if (models_enabled) mc = mc1; + result.push_back(r1[0]); + if (models_enabled) mc = mc1; SASSERT(!pc); SASSERT(!core); - return; - } - goal_ref r1_0 = r1[0]; - operator()(depth+1, r1_0, result, mc, pc, core); - if (models_enabled) mc = concat(mc.get(), mc1.get()); - if (proofs_enabled) pc = concat(pc.get(), pc1.get()); - if (cores_enabled) core = m.mk_join(core1.get(), core); - } - else { - if (cores_enabled) core = core1; - proof_converter_ref_buffer pc_buffer; - model_converter_ref_buffer mc_buffer; - sbuffer sz_buffer; - goal_ref_buffer r2; - for (unsigned i = 0; i < r1_size; i++) { - checkpoint(); - goal_ref g = r1[i]; - r2.reset(); - model_converter_ref mc2; - proof_converter_ref pc2; - expr_dependency_ref core2(m); - operator()(depth+1, g, r2, mc2, pc2, core2); + return; + } + goal_ref r1_0 = r1[0]; + operator()(depth+1, r1_0, result, mc, pc, core); + if (models_enabled) mc = concat(mc.get(), mc1.get()); + if (proofs_enabled) pc = concat(pc.get(), pc1.get()); + if (cores_enabled) core = m.mk_join(core1.get(), core); + } + else { + if (cores_enabled) core = core1; + proof_converter_ref_buffer pc_buffer; + model_converter_ref_buffer mc_buffer; + sbuffer sz_buffer; + goal_ref_buffer r2; + for (unsigned i = 0; i < r1_size; i++) { + checkpoint(); + goal_ref g = r1[i]; + r2.reset(); + model_converter_ref mc2; + proof_converter_ref pc2; + expr_dependency_ref core2(m); + operator()(depth+1, g, r2, mc2, pc2, core2); if (is_decided(r2)) { SASSERT(r2.size() == 1); - if (is_decided_sat(r2)) { - // found solution... + if (is_decided_sat(r2)) { + // found solution... result.push_back(r2[0]); if (models_enabled) { - // mc2 contains the actual model - model_ref md; - if (mc2) (*mc2)(md, 0); - if (mc1) (*mc1)(md, i); - mc = model2model_converter(md.get()); + // mc2 contains the actual model + model_ref md; + if (mc2) (*mc2)(md, 0); + if (mc1) (*mc1)(md, i); + mc = model2model_converter(md.get()); } SASSERT(!pc); SASSERT(!core); - return; - } - else { + return; + } + else { SASSERT(is_decided_unsat(r2)); - SASSERT(!pc2); + SASSERT(!pc2); SASSERT(!core2); if (models_enabled) mc_buffer.push_back(0); if (proofs_enabled) pc_buffer.push_back(proof2proof_converter(m, r2[0]->pr(0))); - if (models_enabled || proofs_enabled) sz_buffer.push_back(0); + if (models_enabled || proofs_enabled) sz_buffer.push_back(0); if (cores_enabled) core = m.mk_join(core.get(), r2[0]->dep(0)); - } - } - else { - result.append(r2.size(), r2.c_ptr()); - if (models_enabled) mc_buffer.push_back(mc2.get()); - if (proofs_enabled) pc_buffer.push_back(pc2.get()); - if (models_enabled || proofs_enabled) sz_buffer.push_back(r2.size()); - if (cores_enabled) core = m.mk_join(core.get(), core2.get()); - } - } - - if (result.empty()) { - // all subgoals were shown to be unsat. + } + } + else { + result.append(r2.size(), r2.c_ptr()); + if (models_enabled) mc_buffer.push_back(mc2.get()); + if (proofs_enabled) pc_buffer.push_back(pc2.get()); + if (models_enabled || proofs_enabled) sz_buffer.push_back(r2.size()); + if (cores_enabled) core = m.mk_join(core.get(), core2.get()); + } + } + + if (result.empty()) { + // all subgoals were shown to be unsat. // create an decided_unsat goal with the proof in->reset_all(); proof_ref pr(m); @@ -1116,8 +1115,8 @@ class repeat_tactical : public unary_tactical { SASSERT(!mc); SASSERT(!pc); SASSERT(!core); } else { - if (models_enabled) mc = concat(mc1.get(), mc_buffer.size(), mc_buffer.c_ptr(), sz_buffer.c_ptr()); - if (proofs_enabled) pc = concat(pc1.get(), pc_buffer.size(), pc_buffer.c_ptr(), sz_buffer.c_ptr()); + if (models_enabled) mc = concat(mc1.get(), mc_buffer.size(), mc_buffer.c_ptr(), sz_buffer.c_ptr()); + if (proofs_enabled) pc = concat(pc1.get(), pc_buffer.size(), pc_buffer.c_ptr(), sz_buffer.c_ptr()); SASSERT(cores_enabled || core == 0); } } @@ -1125,19 +1124,19 @@ class repeat_tactical : public unary_tactical { public: repeat_tactical(tactic * t, unsigned max_depth): - unary_tactical(t), + unary_tactical(t), m_max_depth(max_depth) { } - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, expr_dependency_ref & core) { operator()(0, in, result, mc, pc, core); } - virtual tactic * translate(ast_manager & m) { + virtual tactic * translate(ast_manager & m) { tactic * new_t = m_t->translate(m); return alloc(repeat_tactical, new_t, m_max_depth); } @@ -1152,10 +1151,10 @@ class fail_if_branching_tactical : public unary_tactical { public: fail_if_branching_tactical(tactic * t, unsigned threshold):unary_tactical(t), m_threshold(threshold) {} - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, expr_dependency_ref & core) { m_t->operator()(in, result, mc, pc, core); if (result.size() > m_threshold) { @@ -1165,9 +1164,9 @@ public: core = 0; throw tactic_exception("failed-if-branching tactical"); } - }; + }; - virtual tactic * translate(ast_manager & m) { + virtual tactic * translate(ast_manager & m) { tactic * new_t = m_t->translate(m); return alloc(fail_if_branching_tactical, new_t, m_threshold); } @@ -1181,16 +1180,16 @@ class cleanup_tactical : public unary_tactical { public: cleanup_tactical(tactic * t):unary_tactical(t) {} - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, expr_dependency_ref & core) { m_t->operator()(in, result, mc, pc, core); m_t->cleanup(); - } + } - virtual tactic * translate(ast_manager & m) { + virtual tactic * translate(ast_manager & m) { tactic * new_t = m_t->translate(m); return alloc(cleanup_tactical, new_t); } @@ -1204,21 +1203,21 @@ class try_for_tactical : public unary_tactical { unsigned m_timeout; public: try_for_tactical(tactic * t, unsigned ts):unary_tactical(t), m_timeout(ts) {} - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, expr_dependency_ref & core) { cancel_eh eh(*m_t); - { + { // Warning: scoped_timer is not thread safe in Linux. scoped_timer timer(m_timeout, &eh); m_t->operator()(in, result, mc, pc, core); } } - virtual tactic * translate(ast_manager & m) { + virtual tactic * translate(ast_manager & m) { tactic * new_t = m_t->translate(m); return alloc(try_for_tactical, new_t, m_timeout); } @@ -1236,21 +1235,21 @@ public: } virtual void updt_params(params_ref const & p) { - TRACE("using_params", + TRACE("using_params", tout << "before p: " << p << "\n"; tout << "m_params: " << m_params << "\n";); - + params_ref new_p = p; new_p.append(m_params); unary_tactical::updt_params(new_p); - - TRACE("using_params", + + TRACE("using_params", tout << "after p: " << p << "\n"; tout << "m_params: " << m_params << "\n"; tout << "new_p: " << new_p << "\n";); } - virtual tactic * translate(ast_manager & m) { + virtual tactic * translate(ast_manager & m) { tactic * new_t = m_t->translate(m); return alloc(using_params_tactical, new_t, m_params); } @@ -1274,21 +1273,21 @@ class annotate_tactical : public unary_tactical { public: annotate_tactical(char const* name, tactic* t): unary_tactical(t), m_name(name) {} - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { scope _scope(m_name); m_t->operator()(in, result, mc, pc, core); } - virtual tactic * translate(ast_manager & m) { + virtual tactic * translate(ast_manager & m) { tactic * new_t = m_t->translate(m); return alloc(annotate_tactical, m_name.c_str(), new_t); } - + }; tactic * annotate_tactic(char const* name, tactic * t) { @@ -1300,27 +1299,27 @@ class cond_tactical : public binary_tactical { public: cond_tactical(probe * p, tactic * t1, tactic * t2): binary_tactical(t1, t2), - m_p(p) { + m_p(p) { SASSERT(m_p); - m_p->inc_ref(); + m_p->inc_ref(); } ~cond_tactical() { m_p->dec_ref(); } - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + 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); } - virtual tactic * translate(ast_manager & m) { + virtual tactic * translate(ast_manager & m) { tactic * new_t1 = m_t1->translate(m); tactic * new_t2 = m_t2->translate(m); return alloc(cond_tactical, m_p, new_t1, new_t2); @@ -1339,21 +1338,21 @@ class fail_if_tactic : public tactic { probe * m_p; public: fail_if_tactic(probe * p): - m_p(p) { + m_p(p) { SASSERT(m_p); - m_p->inc_ref(); + m_p->inc_ref(); } - + ~fail_if_tactic() { m_p->dec_ref(); } void cleanup() {} - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, expr_dependency_ref & core) { mc = 0; pc = 0; @@ -1364,7 +1363,7 @@ public: result.push_back(in.get()); } - virtual tactic * translate(ast_manager & m) { + virtual tactic * translate(ast_manager & m) { return this; } }; @@ -1380,11 +1379,11 @@ tactic * fail_if_not(probe * p) { class if_no_proofs_tactical : public unary_tactical { public: if_no_proofs_tactical(tactic * t):unary_tactical(t) {} - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, expr_dependency_ref & core) { if (in->proofs_enabled()) { mc = 0; pc = 0; core = 0; @@ -1402,11 +1401,11 @@ public: class if_no_unsat_cores_tactical : public unary_tactical { public: if_no_unsat_cores_tactical(tactic * t):unary_tactical(t) {} - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, expr_dependency_ref & core) { if (in->unsat_core_enabled()) { mc = 0; pc = 0; core = 0; @@ -1424,11 +1423,11 @@ public: class if_no_models_tactical : public unary_tactical { public: if_no_models_tactical(tactic * t):unary_tactical(t) {} - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, expr_dependency_ref & core) { if (in->models_enabled()) { mc = 0; pc = 0; core = 0; @@ -1459,4 +1458,4 @@ tactic * skip_if_failed(tactic * t) { return or_else(t, mk_skip_tactic()); } - +