3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

cleanup deprecated critical sections, fix cancellation for par_or_else tactic

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-12 09:43:00 -08:00 committed by Christoph M. Wintersteiger
parent 140b3de3aa
commit 16f1b72b7c
50 changed files with 105 additions and 276 deletions

View file

@ -734,11 +734,8 @@ unsigned th_rewriter::get_num_steps() const {
void th_rewriter::cleanup() {
ast_manager & m = m_imp->m();
#pragma omp critical (th_rewriter)
{
dealloc(m_imp);
m_imp = alloc(imp, m, m_params);
}
dealloc(m_imp);
m_imp = alloc(imp, m, m_params);
}
void th_rewriter::reset() {

View file

@ -796,12 +796,9 @@ void euclidean_solver::reset() {
numeral_manager * m = m_imp->m_manager;
bool owns_m = m_imp->m_owns_m;
m_imp->m_owns_m = false;
#pragma omp critical (euclidean_solver)
{
dealloc(m_imp);
m_imp = alloc(imp, m);
m_imp->m_owns_m = owns_m;
}
dealloc(m_imp);
m_imp = alloc(imp, m);
m_imp->m_owns_m = owns_m;
}
euclidean_solver::var euclidean_solver::mk_var() {

View file

@ -261,17 +261,8 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m();
imp * d = m_imp;
#pragma omp critical (tactic_cancel)
{
d = m_imp;
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
dealloc(m_imp);
m_imp = alloc(imp, m, m_params);
}
};

View file

@ -403,18 +403,10 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
d->collect_statistics(m_stats);
#pragma omp critical (tactic_cancel)
{
m_imp = 0;
}
dealloc(d);
d = alloc(imp, m_is_simplify, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
m_imp->collect_statistics(m_stats);
dealloc(m_imp);
m_imp = alloc(imp, m_is_simplify, m, m_params);
}

View file

@ -262,17 +262,11 @@ struct goal2nlsat::imp {
struct goal2nlsat::scoped_set_imp {
goal2nlsat & m_owner;
scoped_set_imp(goal2nlsat & o, imp & i):m_owner(o) {
#pragma omp critical (tactic_cancel)
{
m_owner.m_imp = &i;
}
m_owner.m_imp = &i;
}
~scoped_set_imp() {
#pragma omp critical (tactic_cancel)
{
m_owner.m_imp = 0;
}
m_owner.m_imp = 0;
}
};

View file

@ -175,18 +175,12 @@ class nlsat_tactic : public tactic {
struct scoped_set_imp {
nlsat_tactic & m_owner;
scoped_set_imp(nlsat_tactic & o, imp & i):m_owner(o) {
#pragma omp critical (tactic_cancel)
{
m_owner.m_imp = &i;
}
m_owner.m_imp = &i;
}
~scoped_set_imp() {
m_owner.m_imp->m_solver.collect_statistics(m_owner.m_stats);
#pragma omp critical (tactic_cancel)
{
m_owner.m_imp = 0;
}
m_owner.m_imp = 0;
}
};

View file

@ -2569,17 +2569,8 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
#pragma omp critical (tactic_cancel)
{
m_imp = 0;
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
dealloc(m_imp);
m_imp = alloc(imp, m, m_params);
}
};

View file

@ -121,17 +121,8 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
#pragma omp critical (tactic_cancel)
{
m_imp = 0;
}
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
dealloc(m_imp);
m_imp = alloc(imp, m, m_params);
}
};

View file

@ -485,16 +485,10 @@ void goal2sat::collect_param_descrs(param_descrs & r) {
struct goal2sat::scoped_set_imp {
goal2sat * m_owner;
scoped_set_imp(goal2sat * o, goal2sat::imp * i):m_owner(o) {
#pragma omp critical (goal2sat)
{
m_owner->m_imp = i;
}
m_owner->m_imp = i;
}
~scoped_set_imp() {
#pragma omp critical (goal2sat)
{
m_owner->m_imp = 0;
}
m_owner->m_imp = 0;
}
};
@ -732,16 +726,10 @@ void sat2goal::collect_param_descrs(param_descrs & r) {
struct sat2goal::scoped_set_imp {
sat2goal * m_owner;
scoped_set_imp(sat2goal * o, sat2goal::imp * i):m_owner(o) {
#pragma omp critical (sat2goal)
{
m_owner->m_imp = i;
}
m_owner->m_imp = i;
}
~scoped_set_imp() {
#pragma omp critical (sat2goal)
{
m_owner->m_imp = 0;
}
m_owner->m_imp = 0;
}
};

View file

@ -145,17 +145,11 @@ class sat_tactic : public tactic {
sat_tactic * m_owner;
scoped_set_imp(sat_tactic * o, imp * i):m_owner(o) {
#pragma omp critical (sat_tactic)
{
m_owner->m_imp = i;
}
m_owner->m_imp = i;
}
~scoped_set_imp() {
#pragma omp critical (sat_tactic)
{
m_owner->m_imp = 0;
}
m_owner->m_imp = 0;
}
};

View file

@ -167,18 +167,14 @@ public:
if (o.m_callback) {
new_ctx->set_progress_callback(o.m_callback);
}
#pragma omp critical (as_st_solver)
{
o.m_ctx = new_ctx;
}
o.m_ctx = new_ctx;
}
~scoped_init_ctx() {
smt::kernel * d = m_owner.m_ctx;
#pragma omp critical (as_st_cancel)
{
m_owner.m_ctx = 0;
}
m_owner.m_ctx = 0;
if (d)
dealloc(d);
}

View file

@ -394,10 +394,7 @@ public:
virtual void cleanup() {
imp * d = alloc(imp, m_imp->m, m_params);
d->m_num_conflicts = m_imp->m_num_conflicts;
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -330,10 +330,7 @@ public:
virtual void cleanup() {
imp * d = alloc(imp, m_imp->m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -335,10 +335,7 @@ public:
virtual void cleanup() {
imp * d = alloc(imp, m_imp->m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}
};

View file

@ -1669,10 +1669,7 @@ public:
virtual void cleanup() {
imp * d = alloc(imp, m_imp->m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -400,11 +400,8 @@ public:
virtual void cleanup() {
expr_set* d = alloc(expr_set);
ptr_vector<expr>* todo = alloc(ptr_vector<expr>);
#pragma omp critical (tactic_cancel)
{
std::swap(m_01s, d);
std::swap(m_todo, todo);
}
std::swap(m_01s, d);
std::swap(m_todo, todo);
dealloc(d);
dealloc(todo);
}

View file

@ -346,10 +346,7 @@ public:
virtual void cleanup() {
imp * d = alloc(imp, m_imp->m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -404,17 +404,11 @@ class nla2bv_tactic : public tactic {
nla2bv_tactic & m_owner;
scoped_set_imp(nla2bv_tactic & o, imp & i):
m_owner(o) {
#pragma omp critical (tactic_cancel)
{
m_owner.m_imp = &i;
}
m_owner.m_imp = &i;
}
~scoped_set_imp() {
#pragma omp critical (tactic_cancel)
{
m_owner.m_imp = 0;
}
m_owner.m_imp = 0;
}
};

View file

@ -189,10 +189,7 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}
};

View file

@ -1004,10 +1004,7 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -544,9 +544,6 @@ void propagate_ineqs_tactic::operator()(goal_ref const & g,
void propagate_ineqs_tactic::cleanup() {
imp * d = alloc(imp, m_imp->m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -423,10 +423,7 @@ public:
virtual void cleanup() {
imp * d = alloc(imp, m_imp->m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}
};

View file

@ -149,10 +149,7 @@ public:
virtual void cleanup() {
imp * d = alloc(imp, m_imp->m(), m_rewriter, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -464,10 +464,7 @@ public:
virtual void cleanup() {
imp * d = alloc(imp, m_imp->m(), m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -400,10 +400,7 @@ void bv_size_reduction_tactic::operator()(goal_ref const & g,
void bv_size_reduction_tactic::cleanup() {
imp * d = alloc(imp, m_imp->m);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -143,10 +143,7 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m();
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -307,10 +307,7 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -308,10 +308,7 @@ public:
virtual void cleanup() {
imp * d = alloc(imp, m_imp->m(), m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}
};

View file

@ -183,16 +183,11 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = m_imp;
#pragma omp critical (tactic_cancel)
{
m_imp = 0;
}
m_imp = 0;
dealloc(d);
d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
m_imp = d;
}
m_imp = d;
}
static void blast_term_ite(expr_ref& fml) {

View file

@ -697,10 +697,7 @@ void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) {
void cofactor_elim_term_ite::cleanup() {
ast_manager & m = m_imp->m;
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -540,10 +540,7 @@ void ctx_simplify_tactic::operator()(goal_ref const & in,
void ctx_simplify_tactic::cleanup() {
ast_manager & m = m_imp->m;
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -87,10 +87,7 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m();
imp * d = alloc(imp, m);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -108,10 +108,7 @@ public:
ast_manager & m = g->m();
bool produce_proofs = g->proofs_enabled();
rw r(m, produce_proofs);
#pragma omp critical (tactic_cancel)
{
m_rw = &r;
}
m_rw = &r;
mc = 0; pc = 0; core = 0; result.reset();
tactic_report report("distribute-forall", *g);
@ -134,10 +131,7 @@ public:
result.push_back(g.get());
TRACE("distribute-forall", g->display(tout););
SASSERT(g->is_well_sorted());
#pragma omp critical (tactic_cancel)
{
m_rw = 0;
}
m_rw = 0;
}
virtual void cleanup() {}

View file

@ -172,10 +172,7 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m;
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -895,10 +895,7 @@ class elim_uncnstr_tactic : public tactic {
}
void init_rw(bool produce_proofs) {
#pragma omp critical (tactic_cancel)
{
m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps);
}
m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps);
}
virtual void operator()(goal_ref const & g,
@ -968,10 +965,7 @@ class elim_uncnstr_tactic : public tactic {
}
}
m_mc = 0;
#pragma omp critical (tactic_cancel)
{
m_rw = 0;
}
m_rw = 0;
TRACE("elim_uncnstr", if (mc) mc->display(tout););
result.push_back(g.get());
g->inc_depth();
@ -1034,10 +1028,7 @@ public:
unsigned num_elim_apps = get_num_elim_apps();
ast_manager & m = m_imp->m_manager;
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
m_imp->m_num_elim_apps = num_elim_apps;
}

View file

@ -29,17 +29,11 @@ class nnf_tactic : public tactic {
set_nnf(nnf_tactic & owner, nnf & n):
m_owner(owner) {
#pragma omp critical (nnf_tactic)
{
m_owner.m_nnf = &n;
}
m_owner.m_nnf = &n;
}
~set_nnf() {
#pragma omp critical (nnf_tactic)
{
m_owner.m_nnf = 0;
}
m_owner.m_nnf = 0;
}
};
public:

View file

@ -220,10 +220,7 @@ public:
virtual void cleanup() {
imp * d = alloc(imp, m_imp->m);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -257,10 +257,7 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m();
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -532,10 +532,7 @@ void reduce_args_tactic::operator()(goal_ref const & g,
void reduce_args_tactic::cleanup() {
ast_manager & m = m_imp->m();
imp * d = alloc(imp, m);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -112,10 +112,7 @@ void simplify_tactic::operator()(goal_ref const & in,
void simplify_tactic::cleanup() {
ast_manager & m = m_imp->m();
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -751,10 +751,7 @@ public:
imp * d = alloc(imp, m, m_params, r, owner);
d->m_num_eliminated_vars = num_elim_vars;
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -896,10 +896,7 @@ public:
ast_manager & m = m_imp->m;
imp * d = alloc(imp, m, m_params);
d->m_num_aux_vars = m_imp->m_num_aux_vars;
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -155,10 +155,7 @@ public:
virtual void cleanup() {
imp * d = alloc(imp, m_imp->m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -80,10 +80,7 @@ public:
virtual void cleanup() {
sls_engine * d = alloc(sls_engine, m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_engine);
}
std::swap(d, m_engine);
dealloc(d);
}

View file

@ -461,10 +461,21 @@ enum par_exception_kind {
};
class par_tactical : public or_else_tactical {
struct scoped_limits {
reslimit& m_limit;
unsigned m_sz;
scoped_limits(reslimit& lim): m_limit(lim), m_sz(0) {}
~scoped_limits() { for (unsigned i = 0; i < m_sz; ++i) m_limit.pop_child(); }
void push_child(reslimit* lim) { m_limit.push_child(lim); ++m_sz; }
};
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,
@ -485,6 +496,7 @@ public:
ast_manager & m = in->m();
scoped_ptr_vector<ast_manager> managers;
scoped_limits scl(m.limit());
goal_ref_vector in_copies;
tactic_ref_vector ts;
unsigned sz = m_ts.size();
@ -494,6 +506,7 @@ public:
ast_translation translator(m, *new_m);
in_copies.push_back(in->translate(translator));
ts.push_back(m_ts.get(i)->translate(*new_m));
scl.push_child(&new_m->limit());
}
unsigned finished_id = UINT_MAX;

View file

@ -140,10 +140,7 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m();
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -148,10 +148,7 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m();
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -115,10 +115,7 @@ public:
virtual void cleanup() {
ast_manager & m = m_imp->m();
imp * d = alloc(imp, m, m_params);
#pragma omp critical (tactic_cancel)
{
std::swap(d, m_imp);
}
std::swap(d, m_imp);
dealloc(d);
}

View file

@ -56,3 +56,16 @@ void reslimit::pop() {
m_limits.pop_back();
m_cancel = false;
}
void reslimit::cancel() {
m_cancel = true;
for (unsigned i = 0; i < m_children.size(); ++i) {
m_children[i]->cancel();
}
}
void reslimit::reset_cancel() {
m_cancel = false;
for (unsigned i = 0; i < m_children.size(); ++i) {
m_children[i]->reset_cancel();
}
}

View file

@ -26,19 +26,22 @@ class reslimit {
uint64 m_count;
uint64 m_limit;
svector<uint64> m_limits;
ptr_vector<reslimit> m_children;
public:
reslimit();
void push(unsigned delta_limit);
void pop();
void push_child(reslimit* r) { m_children.push_back(r); }
void pop_child() { m_children.pop_back(); }
bool inc();
bool inc(unsigned offset);
uint64 count() const;
bool cancel_flag_set() { return m_cancel; }
void cancel() { m_cancel = true; }
void reset_cancel() { m_cancel = false; }
void cancel();
void reset_cancel();
};
class scoped_rlimit {