moving to resource managed cancellation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/api_algebraic.cpp

@@ -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);

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<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);

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<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);

src/api/api_polynomial.cpp

@@ -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);

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<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;
         {

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<tactic> eh(*to_tactic_ref(t));
+        cancel_eh<reslimit> eh(mk_c(c)->m().limit());
         
         to_tactic_ref(t)->updt_params(p);
 

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():
+    algebraic_numbers_wrapper(reslimit& lim):
-        m_amanager(m_qmanager),
+        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;
 }
 

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_skolemizer(m) {
-        m_cancel(false) {
         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();

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();
 };

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),

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() {

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<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);

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_goals(m)
-            m_cancel(false)
         {
             // m_fparams.m_relevancy_lvl = 0;
             m_fparams.m_mbqi = false;

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), 

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) {