mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

moving to resource managed cancellation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-11 13:36:47 -08:00 • committed by Christoph M. Wintersteiger
parent 589626b738
commit e08bfb62f8
15 changed files with 24 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_algebraic.cpp
View file

@ -372,7 +372,7 @@ extern "C" {
}
scoped_anum_vector roots(_am);
{
cancel_eh<algebraic_numbers::manager> eh(_am);
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
vector_var2anum v2a(as);
@ -407,7 +407,7 @@ extern "C" {
return 0;
}
{
cancel_eh<algebraic_numbers::manager> eh(_am);
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
vector_var2anum v2a(as);

2
src/api/api_ast.cpp
View file

@ -671,7 +671,7 @@ extern "C" {
bool use_ctrl_c = p.get_bool("ctrl_c", false);
th_rewriter m_rw(m, p);
expr_ref result(m);
cancel_eh<th_rewriter> eh(m_rw);
cancel_eh<reslimit> eh(m.limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);

2
src/api/api_interp.cpp
View file

@ -260,7 +260,7 @@ extern "C" {
unsigned timeout = to_params(p)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
unsigned rlimit = to_params(p)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
bool use_ctrl_c = to_params(p)->m_params.get_bool("ctrl_c", false);
cancel_eh<solver> eh(*m_solver.get());
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
ast *_pat = to_ast(pat);

2
src/api/api_polynomial.cpp
View file

@ -66,7 +66,7 @@ extern "C" {
polynomial_ref r(pm);
expr_ref _r(mk_c(c)->m());
{
cancel_eh<polynomial::manager> eh(pm);
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
scoped_timer timer(mk_c(c)->params().m_timeout, &eh);
pm.psc_chain(_p, _q, v_x, rs);

2
src/api/api_solver.cpp
View file

@ -271,7 +271,7 @@ extern "C" {
unsigned timeout = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
unsigned rlimit = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
bool use_ctrl_c = to_solver(s)->m_params.get_bool("ctrl_c", false);
cancel_eh<solver> eh(*to_solver_ref(s));
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
lbool result;
{

2
src/api/api_tactic.cpp
View file

@ -409,7 +409,7 @@ extern "C" {
unsigned timeout = p.get_uint("timeout", UINT_MAX);
bool use_ctrl_c = p.get_bool("ctrl_c", false);
cancel_eh<tactic> eh(*to_tactic_ref(t));
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
to_tactic_ref(t)->updt_params(p);

6
src/ast/arith_decl_plugin.cpp
View file

@ -28,8 +28,8 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
id_gen m_id_gen;
scoped_anum_vector m_nums;
algebraic_numbers_wrapper():
m_amanager(m_qmanager),
algebraic_numbers_wrapper(reslimit& lim):
m_amanager(lim, m_qmanager),
m_nums(m_amanager) {
}
@ -66,7 +66,7 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
arith_decl_plugin::algebraic_numbers_wrapper & arith_decl_plugin::aw() const {
if (m_aw == 0)
const_cast<arith_decl_plugin*>(this)->m_aw = alloc(algebraic_numbers_wrapper);
const_cast<arith_decl_plugin*>(this)->m_aw = alloc(algebraic_numbers_wrapper, m_manager->limit());
return *m_aw;
}

12
src/ast/normal_forms/nnf.cpp
View file

@ -250,7 +250,6 @@ struct nnf::imp {
name_exprs * m_name_nested_formulas;
name_exprs * m_name_quant;
volatile bool m_cancel;
unsigned long long m_max_memory; // in bytes
imp(ast_manager & m, defined_names & n, params_ref const & p):
@ -259,8 +258,7 @@ struct nnf::imp {
m_todo_defs(m),
m_todo_proofs(m),
m_result_pr_stack(m),
m_skolemizer(m),
m_cancel(false) {
m_skolemizer(m) {
updt_params(p);
for (unsigned i = 0; i < 4; i++) {
m_cache[i] = alloc(act_cache, m);
@ -369,15 +367,12 @@ struct nnf::imp {
return false;
}
void set_cancel(bool f) {
m_cancel = f;
}
void checkpoint() {
cooperate("nnf");
if (memory::get_allocation_size() > m_max_memory)
throw nnf_exception(Z3_MAX_MEMORY_MSG);
if (m_cancel)
if (m().canceled())
throw nnf_exception(Z3_CANCELED_MSG);
}
@ -916,9 +911,6 @@ void nnf::get_param_descrs(param_descrs & r) {
imp::get_param_descrs(r);
}
void nnf::set_cancel(bool f) {
m_imp->set_cancel(f);
}
void nnf::reset() {
m_imp->reset();

4
src/ast/normal_forms/nnf.h
View file

@ -44,10 +44,6 @@ public:
*/
static void get_param_descrs(param_descrs & r);
void cancel() { set_cancel(true); }
void reset_cancel() { set_cancel(false); }
void set_cancel(bool f);
void reset();
void reset_cache();
};

3
src/cmd_context/extra_cmds/polynomial_cmds.cpp
View file

@ -83,6 +83,7 @@ static void factor(cmd_context & ctx, expr * t, polynomial::factor_params const
class poly_isolate_roots_cmd : public cmd {
struct context {
arith_util m_util;
reslimit m_lim;
unsynch_mpq_manager m_qm;
polynomial::manager m_pm;
algebraic_numbers::manager m_am;
@ -95,7 +96,7 @@ class poly_isolate_roots_cmd : public cmd {
context(ast_manager & m):
m_util(m),
m_pm(m_qm),
m_am(m_qm),
m_am(m_lim, m_qm),
m_p(m_pm),
m_expr2poly(m, m_pm),
m_var(polynomial::null_var),

10
src/math/polynomial/algebraic_numbers.cpp
View file

@ -61,7 +61,8 @@ namespace algebraic_numbers {
algebraic_params::collect_param_descrs(r);
}
struct manager::imp {
struct manager::imp {
reslimit& m_limit;
manager & m_wrapper;
small_object_allocator & m_allocator;
unsynch_mpq_manager & m_qmanager;
@ -96,7 +97,8 @@ namespace algebraic_numbers {
unsigned m_compare_refine;
unsigned m_compare_poly_eq;
imp(manager & w, unsynch_mpq_manager & m, params_ref const & p, small_object_allocator & a):
imp(reslimit& lim, manager & w, unsynch_mpq_manager & m, params_ref const & p, small_object_allocator & a):
m_limit(lim),
m_wrapper(w),
m_allocator(a),
m_qmanager(m),
@ -2764,14 +2766,14 @@ namespace algebraic_numbers {
};
manager::manager(unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a) {
manager::manager(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p, small_object_allocator * a) {
m_own_allocator = false;
m_allocator = a;
if (m_allocator == 0) {
m_own_allocator = true;
m_allocator = alloc(small_object_allocator, "algebraic");
}
m_imp = alloc(imp, *this, m, p, *m_allocator);
m_imp = alloc(imp, lim, *this, m, p, *m_allocator);
}
manager::~manager() {

3
src/math/polynomial/algebraic_numbers.h
View file

@ -28,6 +28,7 @@ Notes:
#include"tptr.h"
#include"statistics.h"
#include"params.h"
#include"rlimit.h"
class small_object_allocator;
class mpbq_manager;
@ -57,7 +58,7 @@ namespace algebraic_numbers {
typedef _scoped_numeral<manager> scoped_numeral;
typedef _scoped_numeral_vector<manager> scoped_numeral_vector;
manager(unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
manager(reslimit& rl, unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
~manager();
static void get_param_descrs(param_descrs & r);

4
src/muz/clp/clp_context.cpp
View file

@ -44,7 +44,6 @@ namespace datalog {
var_subst m_var_subst;
expr_ref_vector m_ground;
app_ref_vector m_goals;
volatile bool m_cancel;
stats m_stats;
public:
imp(context& ctx):
@ -54,8 +53,7 @@ namespace datalog {
m_solver(m, m_fparams), // TBD: can be replaced by efficient BV solver.
m_var_subst(m, false),
m_ground(m),
m_goals(m),
m_cancel(false)
m_goals(m)
{
// m_fparams.m_relevancy_lvl = 0;
m_fparams.m_mbqi = false;

2
src/nlsat/nlsat_solver.cpp
View file

@ -166,7 +166,7 @@ namespace nlsat {
m_allocator("nlsat"),
m_pm(m_qm, &m_allocator),
m_cache(m_pm),
m_am(m_qm, p, &m_allocator),
m_am(rlim, m_qm, p, &m_allocator),
m_asm(*this, m_allocator),
m_assignment(m_am),
m_evaluator(m_assignment, m_pm, m_allocator),

7
src/tactic/core/nnf_tactic.cpp
View file

@ -113,13 +113,6 @@ public:
}
virtual void cleanup() {}
virtual void set_cancel(bool f) {
#pragma omp critical (nnf_tactic)
{
if (m_nnf)
m_nnf->set_cancel(f);
}
}
};
tactic * mk_snf_tactic(ast_manager & m, params_ref const & p) {