From 981f8226feb17dc50d8b7335b7ff182c6089e25f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 11 Dec 2015 13:36:47 -0800 Subject: [PATCH] moving to resource managed cancellation Signed-off-by: Nikolaj Bjorner --- src/api/api_algebraic.cpp | 4 ++-- src/api/api_ast.cpp | 2 +- src/api/api_interp.cpp | 2 +- src/api/api_polynomial.cpp | 2 +- src/api/api_solver.cpp | 2 +- src/api/api_tactic.cpp | 2 +- src/ast/arith_decl_plugin.cpp | 6 +++--- src/ast/normal_forms/nnf.cpp | 12 ++---------- src/ast/normal_forms/nnf.h | 4 ---- src/cmd_context/extra_cmds/polynomial_cmds.cpp | 3 ++- src/math/polynomial/algebraic_numbers.cpp | 10 ++++++---- src/math/polynomial/algebraic_numbers.h | 3 ++- src/muz/clp/clp_context.cpp | 4 +--- src/nlsat/nlsat_solver.cpp | 2 +- src/tactic/core/nnf_tactic.cpp | 7 ------- 15 files changed, 24 insertions(+), 41 deletions(-) diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp index d03a6aff4..bee39aa2a 100644 --- a/src/api/api_algebraic.cpp +++ b/src/api/api_algebraic.cpp @@ -372,7 +372,7 @@ extern "C" { } scoped_anum_vector roots(_am); { - cancel_eh eh(_am); + cancel_eh 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 eh(_am); + cancel_eh 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); diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index de15c0c15..9f0ddbaa8 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -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 eh(m_rw); + cancel_eh eh(m.limit()); api::context::set_interruptable si(*(mk_c(c)), eh); { scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 2c1fd7d9b..0011b28ac 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -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 eh(*m_solver.get()); + cancel_eh eh(mk_c(c)->m().limit()); api::context::set_interruptable si(*(mk_c(c)), eh); ast *_pat = to_ast(pat); diff --git a/src/api/api_polynomial.cpp b/src/api/api_polynomial.cpp index 25d4ca292..93635507b 100644 --- a/src/api/api_polynomial.cpp +++ b/src/api/api_polynomial.cpp @@ -66,7 +66,7 @@ extern "C" { polynomial_ref r(pm); expr_ref _r(mk_c(c)->m()); { - cancel_eh eh(pm); + cancel_eh 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); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index b568f3613..94e91ae05 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -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 eh(*to_solver_ref(s)); + cancel_eh eh(mk_c(c)->m().limit()); api::context::set_interruptable si(*(mk_c(c)), eh); lbool result; { diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index adfd0fb71..78e042528 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -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 eh(*to_tactic_ref(t)); + cancel_eh eh(mk_c(c)->m().limit()); to_tactic_ref(t)->updt_params(p); diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 9d1f4343f..174082f8c 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -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(this)->m_aw = alloc(algebraic_numbers_wrapper); + const_cast(this)->m_aw = alloc(algebraic_numbers_wrapper, m_manager->limit()); return *m_aw; } diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 45f85e154..0d8aa90e3 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -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(); diff --git a/src/ast/normal_forms/nnf.h b/src/ast/normal_forms/nnf.h index 122b85974..60d50e3b6 100644 --- a/src/ast/normal_forms/nnf.h +++ b/src/ast/normal_forms/nnf.h @@ -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(); }; diff --git a/src/cmd_context/extra_cmds/polynomial_cmds.cpp b/src/cmd_context/extra_cmds/polynomial_cmds.cpp index e68789dac..b045c236f 100644 --- a/src/cmd_context/extra_cmds/polynomial_cmds.cpp +++ b/src/cmd_context/extra_cmds/polynomial_cmds.cpp @@ -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), diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 804a134e0..fd92c52b5 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -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() { diff --git a/src/math/polynomial/algebraic_numbers.h b/src/math/polynomial/algebraic_numbers.h index 2c63c9718..13e20233c 100644 --- a/src/math/polynomial/algebraic_numbers.h +++ b/src/math/polynomial/algebraic_numbers.h @@ -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 scoped_numeral; typedef _scoped_numeral_vector 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); diff --git a/src/muz/clp/clp_context.cpp b/src/muz/clp/clp_context.cpp index 7c5d9799f..7dec835a9 100644 --- a/src/muz/clp/clp_context.cpp +++ b/src/muz/clp/clp_context.cpp @@ -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; diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 6ba831cb1..1a90bb886 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -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), diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp index 19190c299..f921330e3 100644 --- a/src/tactic/core/nnf_tactic.cpp +++ b/src/tactic/core/nnf_tactic.cpp @@ -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) {