mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 03:45:51 +00:00
moving to resource managed cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
Christoph M. Wintersteiger
parent
d4a90d7ec3
commit
267a1e962c
11 changed files with 34 additions and 48 deletions
|
|
@ -1610,6 +1610,7 @@ void cmd_context::validate_model() {
|
|||
model_evaluator evaluator(*(md.get()), p);
|
||||
contains_array_op_proc contains_array(m());
|
||||
{
|
||||
scoped_rlimit _rlimit(m().limit(), 0);
|
||||
cancel_eh<reslimit> eh(m().limit());
|
||||
expr_ref r(m());
|
||||
scoped_ctrl_c ctrlc(eh);
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ context_params::context_params() {
|
|||
m_smtlib2_compliant = false;
|
||||
m_well_sorted_check = false;
|
||||
m_timeout = UINT_MAX;
|
||||
m_rlimit = UINT_MAX;
|
||||
m_rlimit = 0;
|
||||
updt_params();
|
||||
}
|
||||
|
||||
|
|
@ -153,7 +153,7 @@ void context_params::updt_params(params_ref const & p) {
|
|||
|
||||
void context_params::collect_param_descrs(param_descrs & d) {
|
||||
d.insert("timeout", CPK_UINT, "default timeout (in milliseconds) used for solvers", "4294967295");
|
||||
d.insert("rlimit", CPK_UINT, "default resource limit used for solvers", "4294967295");
|
||||
d.insert("rlimit", CPK_UINT, "default resource limit used for solvers. Unrestricted when set to 0.", "0");
|
||||
d.insert("well_sorted_check", CPK_BOOL, "type checker", "false");
|
||||
d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true");
|
||||
d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true");
|
||||
|
|
|
|||
|
|
@ -63,11 +63,13 @@ public:
|
|||
last_result->get_model(md);
|
||||
expr_ref r(ctx.m());
|
||||
unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
|
||||
unsigned rlimit = m_params.get_uint("rlimit", 0);
|
||||
model_evaluator ev(*(md.get()), m_params);
|
||||
cancel_eh<reslimit> eh(ctx.m().limit());
|
||||
{
|
||||
scoped_ctrl_c ctrlc(eh);
|
||||
scoped_timer timer(timeout, &eh);
|
||||
scoped_rlimit _rlimit(ctx.m().limit(), rlimit);
|
||||
cmd_context::scoped_watch sw(ctx);
|
||||
try {
|
||||
ev(m_target, r);
|
||||
|
|
|
|||
|
|
@ -73,9 +73,11 @@ public:
|
|||
unsigned cache_sz;
|
||||
unsigned num_steps = 0;
|
||||
unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
|
||||
unsigned rlimit = m_params.get_uint("rlimit", UINT_MAX);
|
||||
bool failed = false;
|
||||
cancel_eh<reslimit> eh(ctx.m().limit());
|
||||
{
|
||||
scoped_rlimit _rlimit(ctx.m().limit(), rlimit);
|
||||
scoped_ctrl_c ctrlc(eh);
|
||||
scoped_timer timer(timeout, &eh);
|
||||
cmd_context::scoped_watch sw(ctx);
|
||||
|
|
|
|||
|
|
@ -188,6 +188,7 @@ public:
|
|||
tref->set_logic(ctx.get_logic());
|
||||
ast_manager & m = ctx.m();
|
||||
unsigned timeout = p.get_uint("timeout", UINT_MAX);
|
||||
unsigned rlimit = p.get_uint("rlimit", 0);
|
||||
goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores());
|
||||
assert_exprs_from(ctx, *g);
|
||||
TRACE("check_sat_using", g->display(tout););
|
||||
|
|
@ -201,6 +202,7 @@ public:
|
|||
tactic & t = *tref;
|
||||
cancel_eh<reslimit> eh(m.limit());
|
||||
{
|
||||
scoped_rlimit _rlimit(m.limit(), rlimit);
|
||||
scoped_ctrl_c ctrlc(eh);
|
||||
scoped_timer timer(timeout, &eh);
|
||||
cmd_context::scoped_watch sw(ctx);
|
||||
|
|
@ -302,6 +304,7 @@ public:
|
|||
assert_exprs_from(ctx, *g);
|
||||
|
||||
unsigned timeout = p.get_uint("timeout", UINT_MAX);
|
||||
unsigned rlimit = p.get_uint("rlimit", 0);
|
||||
|
||||
goal_ref_buffer result_goals;
|
||||
model_converter_ref mc;
|
||||
|
|
@ -312,6 +315,7 @@ public:
|
|||
bool failed = false;
|
||||
cancel_eh<reslimit> eh(m.limit());
|
||||
{
|
||||
scoped_rlimit _rlimit(m.limit(), rlimit);
|
||||
scoped_ctrl_c ctrlc(eh);
|
||||
scoped_timer timer(timeout, &eh);
|
||||
cmd_context::scoped_watch sw(ctx);
|
||||
|
|
|
|||
|
|
@ -32,19 +32,11 @@ class aig_tactic : public tactic {
|
|||
|
||||
mk_aig_manager(aig_tactic & o, ast_manager & m):m_owner(o) {
|
||||
aig_manager * mng = alloc(aig_manager, m, o.m_max_memory, o.m_aig_gate_encoding);
|
||||
#pragma omp critical (aig_tactic)
|
||||
{
|
||||
m_owner.m_aig_manager = mng;
|
||||
}
|
||||
m_owner.m_aig_manager = mng;
|
||||
}
|
||||
|
||||
~mk_aig_manager() {
|
||||
aig_manager * mng = m_owner.m_aig_manager;
|
||||
#pragma omp critical (aig_tactic)
|
||||
{
|
||||
m_owner.m_aig_manager = 0;
|
||||
}
|
||||
dealloc(mng);
|
||||
dealloc(m_owner.m_aig_manager);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -169,10 +169,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);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -315,10 +315,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);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -40,15 +40,8 @@ public:
|
|||
}
|
||||
|
||||
virtual ~binary_tactical() {
|
||||
tactic * t1 = m_t1;
|
||||
tactic * t2 = m_t2;
|
||||
#pragma omp critical (tactic_cancel)
|
||||
{
|
||||
m_t1 = 0;
|
||||
m_t2 = 0;
|
||||
}
|
||||
t1->dec_ref();
|
||||
t2->dec_ref();
|
||||
m_t1->dec_ref();
|
||||
m_t2->dec_ref();
|
||||
}
|
||||
|
||||
virtual void updt_params(params_ref const & p) {
|
||||
|
|
@ -291,17 +284,9 @@ public:
|
|||
}
|
||||
|
||||
virtual ~nary_tactical() {
|
||||
ptr_buffer<tactic> old_ts;
|
||||
unsigned sz = m_ts.size();
|
||||
old_ts.append(sz, m_ts.c_ptr());
|
||||
#pragma omp critical (tactic_cancel)
|
||||
{
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
m_ts[i] = 0;
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
old_ts[i]->dec_ref();
|
||||
m_ts[i]->dec_ref();
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -906,12 +891,7 @@ public:
|
|||
}
|
||||
|
||||
virtual ~unary_tactical() {
|
||||
tactic * t = m_t;
|
||||
#pragma omp critical (tactic_cancel)
|
||||
{
|
||||
m_t = 0;
|
||||
}
|
||||
t->dec_ref();
|
||||
m_t->dec_ref();
|
||||
}
|
||||
|
||||
virtual void operator()(goal_ref const & in,
|
||||
|
|
|
|||
|
|
@ -45,6 +45,7 @@ void reslimit::push(unsigned delta_limit) {
|
|||
}
|
||||
m_limits.push_back(m_limit);
|
||||
m_limit = m_limit==0?new_limit:std::min(new_limit, m_limit);
|
||||
m_cancel = false;
|
||||
}
|
||||
|
||||
void reslimit::pop() {
|
||||
|
|
@ -53,4 +54,5 @@ void reslimit::pop() {
|
|||
}
|
||||
m_limit = m_limits.back();
|
||||
m_limits.pop_back();
|
||||
m_cancel = false;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -227,16 +227,25 @@ double statistics::get_double_value(unsigned idx) const {
|
|||
return m_d_stats[idx - m_stats.size()].second;
|
||||
}
|
||||
|
||||
static void get_uint64_stats(statistics& st, char const* name, unsigned long long value) {
|
||||
if (value <= UINT_MAX) {
|
||||
st.update(name, static_cast<unsigned>(value));
|
||||
}
|
||||
else {
|
||||
st.update(name, static_cast<double>(value));
|
||||
}
|
||||
}
|
||||
|
||||
void get_memory_statistics(statistics& st) {
|
||||
unsigned long long max_mem = memory::get_max_used_memory();
|
||||
unsigned long long mem = memory::get_allocation_size();
|
||||
max_mem = (100*max_mem)/(1024*1024);
|
||||
mem = (100*mem)/(1024*1024);
|
||||
st.update("max memory", static_cast<double>(max_mem)/100.0);
|
||||
st.update("memory", static_cast<double>(mem)/100.0);
|
||||
st.update("num allocs", static_cast<double>(memory::get_allocation_count()));
|
||||
st.update("max memory", static_cast<double>(max_mem)/100.0);
|
||||
st.update("memory", static_cast<double>(mem)/100.0);
|
||||
get_uint64_stats(st, "num allocs", memory::get_allocation_count());
|
||||
}
|
||||
|
||||
void get_rlimit_statistics(reslimit& l, statistics& st) {
|
||||
st.update("rlimit count", static_cast<double>(l.count()));
|
||||
get_uint64_stats(st, "rlimit count", l.count());
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue