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

reworking cancellation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-11 16:43:48 -08:00 committed by Christoph M. Wintersteiger
parent 9769322690
commit a9723fb6c7
13 changed files with 42 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/cmd_context/cmd_context.cpp
View file

@ -353,7 +353,6 @@ cmd_context::~cmd_context() {
void cmd_context::set_cancel(bool f) {
if (has_manager()) {
m().set_cancel(f);
if (f) {
m().limit().cancel();
}

2
src/cmd_context/extra_cmds/subpaving_cmds.cpp
View file

@ -27,7 +27,7 @@ static void to_subpaving(cmd_context & ctx, expr * t) {
ast_manager & m = ctx.m();
unsynch_mpq_manager qm;
scoped_ptr<subpaving::context> s;
s = subpaving::mk_mpq_context(qm);
s = subpaving::mk_mpq_context(ctx.m().limit(), qm);
expr2var e2v(m);
expr2subpaving e2s(m, *s, &e2v);
params_ref p;

2
src/cmd_context/simplify_cmd.cpp
View file

@ -74,7 +74,7 @@ public:
unsigned num_steps = 0;
unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
bool failed = false;
cancel_eh<th_rewriter> eh(s);
cancel_eh<reslimit> eh(ctx.m().limit());
{
scoped_ctrl_c ctrlc(eh);
scoped_timer timer(timeout, &eh);

2
src/math/interval/interval_def.h
View file

@ -62,7 +62,7 @@ void interval_manager<C>::del(interval & a) {
template<typename C>
void interval_manager<C>::checkpoint() {
if (m_limit.canceled())
if (!m_limit.inc())
throw default_exception("canceled");
cooperate("interval");
}

4
src/math/realclosure/realclosure.cpp
View file

@ -501,8 +501,8 @@ namespace realclosure {
m_qm(qm),
m_mm(m_qm, *m_allocator),
m_bqm(m_qm),
m_qim(m_qm),
m_bqim(m_bqm),
m_qim(lim, m_qm),
m_bqim(lim, m_bqm),
m_plus_inf_approx(m_bqm),
m_minus_inf_approx(m_bqm) {
mpq one(1);

39
src/math/subpaving/subpaving.cpp
View file

@ -37,7 +37,7 @@ namespace subpaving {
protected:
CTX m_ctx;
public:
context_wrapper(typename CTX::numeral_manager & m, params_ref const & p, small_object_allocator * a):m_ctx(m, p, a) {}
context_wrapper(reslimit& lim, typename CTX::numeral_manager & m, params_ref const & p, small_object_allocator * a):m_ctx(lim, m, p, a) {}
virtual ~context_wrapper() {}
virtual unsigned num_vars() const { return m_ctx.num_vars(); }
virtual var mk_var(bool is_int) { return m_ctx.mk_var(is_int); }
@ -47,7 +47,6 @@ namespace subpaving {
virtual void dec_ref(ineq * a) { m_ctx.dec_ref(reinterpret_cast<typename CTX::ineq*>(a)); }
virtual void add_clause(unsigned sz, ineq * const * atoms) { m_ctx.add_clause(sz, reinterpret_cast<typename CTX::ineq * const *>(atoms)); }
virtual void display_constraints(std::ostream & out, bool use_star) const { m_ctx.display_constraints(out, use_star); }
virtual void set_cancel(bool f) { m_ctx.set_cancel(f); }
virtual void set_display_proc(display_var_proc * p) { m_ctx.set_display_proc(p); }
virtual void reset_statistics() { m_ctx.reset_statistics(); }
virtual void collect_statistics(statistics & st) const { m_ctx.collect_statistics(st); }
@ -61,8 +60,8 @@ namespace subpaving {
scoped_mpq m_c;
scoped_mpq_vector m_as;
public:
context_mpq_wrapper(unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a):
context_wrapper<context_mpq>(m, p, a),
context_mpq_wrapper(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a):
context_wrapper<context_mpq>(lim, m, p, a),
m_c(m),
m_as(m)
{}
@ -100,8 +99,8 @@ namespace subpaving {
}
public:
context_mpf_wrapper(f2n<mpf_manager> & fm, params_ref const & p, small_object_allocator * a):
context_wrapper<context_mpf>(fm, p, a),
context_mpf_wrapper(reslimit& lim, f2n<mpf_manager> & fm, params_ref const & p, small_object_allocator * a):
context_wrapper<context_mpf>(lim, fm, p, a),
m_qm(fm.m().mpq_manager()),
m_c(fm.m()),
m_as(fm.m()),
@ -161,8 +160,8 @@ namespace subpaving {
}
public:
context_hwf_wrapper(f2n<hwf_manager> & fm, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
context_wrapper<context_hwf>(fm, p, a),
context_hwf_wrapper(reslimit& lim,f2n<hwf_manager> & fm, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
context_wrapper<context_hwf>(lim, fm, p, a),
m_qm(qm) {
}
@ -215,8 +214,8 @@ namespace subpaving {
}
public:
context_fpoint_wrapper(typename context_fpoint::numeral_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
context_wrapper<context_fpoint>(m, p, a),
context_fpoint_wrapper(reslimit& lim, typename context_fpoint::numeral_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
context_wrapper<context_fpoint>(lim, m, p, a),
m_qm(qm),
m_c(m),
m_as(m),
@ -261,24 +260,24 @@ namespace subpaving {
typedef context_fpoint_wrapper<context_mpff> context_mpff_wrapper;
typedef context_fpoint_wrapper<context_mpfx> context_mpfx_wrapper;
context * mk_mpq_context(unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a) {
return alloc(context_mpq_wrapper, m, p, a);
context * mk_mpq_context(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a) {
return alloc(context_mpq_wrapper, lim, m, p, a);
}
context * mk_mpf_context(f2n<mpf_manager> & m, params_ref const & p, small_object_allocator * a) {
return alloc(context_mpf_wrapper, m, p, a);
context * mk_mpf_context(reslimit& lim, f2n<mpf_manager> & m, params_ref const & p, small_object_allocator * a) {
return alloc(context_mpf_wrapper, lim, m, p, a);
}
context * mk_hwf_context(f2n<hwf_manager> & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
return alloc(context_hwf_wrapper, m, qm, p, a);
context * mk_hwf_context(reslimit& lim, f2n<hwf_manager> & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
return alloc(context_hwf_wrapper, lim, m, qm, p, a);
}
context * mk_mpff_context(mpff_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
return alloc(context_mpff_wrapper, m, qm, p, a);
context * mk_mpff_context(reslimit& lim, mpff_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
return alloc(context_mpff_wrapper, lim, m, qm, p, a);
}
context * mk_mpfx_context(mpfx_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
return alloc(context_mpfx_wrapper, m, qm, p, a);
context * mk_mpfx_context(reslimit& lim, mpfx_manager & m, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a) {
return alloc(context_mpfx_wrapper, lim, m, qm, p, a);
}
};

11
src/math/subpaving/subpaving.h
View file

@ -95,7 +95,6 @@ public:
*/
virtual void display_constraints(std::ostream & out, bool use_star = false) const = 0;
virtual void set_cancel(bool f) = 0;
virtual void collect_param_descrs(param_descrs & r) = 0;
@ -112,11 +111,11 @@ public:
virtual void display_bounds(std::ostream & out) const = 0;
};
context * mk_mpq_context(unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
context * mk_mpf_context(f2n<mpf_manager> & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
context * mk_hwf_context(f2n<hwf_manager> & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
context * mk_mpff_context(mpff_manager & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
context * mk_mpfx_context(mpfx_manager & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
context * mk_mpq_context(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
context * mk_mpf_context(reslimit& lim, f2n<mpf_manager> & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
context * mk_hwf_context(reslimit& lim, f2n<hwf_manager> & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
context * mk_mpff_context(reslimit& lim, mpff_manager & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
context * mk_mpfx_context(reslimit& lim, mpfx_manager & m, unsynch_mpq_manager & qm, params_ref const & p = params_ref(), small_object_allocator * a = 0);
};

2
src/math/subpaving/subpaving_hwf.h
View file

@ -40,7 +40,7 @@ public:
class context_hwf : public context_t<config_hwf> {
public:
context_hwf(f2n<hwf_manager> & m, params_ref const & p, small_object_allocator * a):context_t<config_hwf>(config_hwf(m), p, a) {}
context_hwf(reslimit& lim, f2n<hwf_manager> & m, params_ref const & p, small_object_allocator * a):context_t<config_hwf>(lim, config_hwf(m), p, a) {}
};
};

2
src/math/subpaving/subpaving_mpf.h
View file

@ -41,7 +41,7 @@ public:
class context_mpf : public context_t<config_mpf> {
public:
context_mpf(f2n<mpf_manager> & m, params_ref const & p, small_object_allocator * a):context_t<config_mpf>(config_mpf(m), p, a) {}
context_mpf(reslimit& lim, f2n<mpf_manager> & m, params_ref const & p, small_object_allocator * a):context_t<config_mpf>(lim, config_mpf(m), p, a) {}
};
};

1
src/math/subpaving/subpaving_t.h
View file

@ -467,6 +467,7 @@ public:
typedef _scoped_numeral_vector<numeral_manager> scoped_numeral_vector;
private:
reslimit& m_limit;
C m_c;
bool m_arith_failed; //!< True if the arithmetic module produced an exception.
bool m_own_allocator;

7
src/math/subpaving/subpaving_t_def.h
View file

@ -413,12 +413,13 @@ void context_t<C>::polynomial::display(std::ostream & out, numeral_manager & nm,
}
template<typename C>
context_t<C>::context_t(C const & c, params_ref const & p, small_object_allocator * a):
context_t<C>::context_t(reslimit& lim, C const & c, params_ref const & p, small_object_allocator * a):
m_limit(lim),
m_c(c),
m_own_allocator(a == 0),
m_allocator(a == 0 ? alloc(small_object_allocator, "subpaving") : a),
m_bm(*this, *m_allocator),
m_im(interval_config(m_c.m())),
m_im(lim, interval_config(m_c.m())),
m_num_buffer(nm()) {
m_arith_failed = false;
m_timestamp = 0;
@ -458,7 +459,7 @@ context_t<C>::~context_t() {
template<typename C>
void context_t<C>::checkpoint() {
if (m_limit.canceled())
if (!m_limit.inc())
throw default_exception("canceled");
if (memory::get_allocation_size() > m_max_memory)
throw default_exception(Z3_MAX_MEMORY_MSG);

14
src/math/subpaving/tactic/subpaving_tactic.cpp
View file

@ -103,11 +103,11 @@ class subpaving_tactic : public tactic {
if (m_kind != new_kind) {
m_kind = new_kind;
switch (m_kind) {
case MPQ: m_ctx = subpaving::mk_mpq_context(m_qm); break;
case MPF: m_ctx = subpaving::mk_mpf_context(m_fm); break;
case HWF: m_ctx = subpaving::mk_hwf_context(m_hm, m_qm); break;
case MPFF: m_ctx = subpaving::mk_mpff_context(m_ffm, m_qm); break;
case MPFX: m_ctx = subpaving::mk_mpfx_context(m_fxm, m_qm); break;
case MPQ: m_ctx = subpaving::mk_mpq_context(m().limit(), m_qm); break;
case MPF: m_ctx = subpaving::mk_mpf_context(m().limit(), m_fm); break;
case HWF: m_ctx = subpaving::mk_hwf_context(m().limit(), m_hm, m_qm); break;
case MPFF: m_ctx = subpaving::mk_mpff_context(m().limit(), m_ffm, m_qm); break;
case MPFX: m_ctx = subpaving::mk_mpfx_context(m().limit(), m_fxm, m_qm); break;
default: UNREACHABLE(); break;
}
m_e2s = alloc(expr2subpaving, m_manager, *m_ctx, &m_e2v);
@ -123,10 +123,6 @@ class subpaving_tactic : public tactic {
m_ctx->reset_statistics();
}
void set_cancel(bool f) {
m_ctx->set_cancel(f);
}
subpaving::ineq * mk_ineq(expr * a) {
bool neg = false;
while (m().is_not(a, a))

2
src/solver/combined_solver.cpp
View file

@ -84,7 +84,7 @@ private:
volatile bool m_canceled;
aux_timeout_eh(solver * s):m_solver(s), m_canceled(false) {}
virtual void operator()() {
m_solver->get_manager().cancel();
m_solver->get_manager().limit().cancel();
m_canceled = true;
}
};