reworking cancellation

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

src/api/api_context.cpp

@@ -75,7 +75,8 @@ namespace api {
         m_dtutil(m()),
         m_last_result(m()),
         m_ast_trail(m()),
-        m_replay_stack() {
+        m_replay_stack(),
+        m_pmanager(m_limit) {
 
         m_error_code = Z3_OK;
         m_print_mode = Z3_PRINT_SMTLIB_FULL;
@@ -122,9 +123,8 @@ namespace api {
         {
             if (m_interruptable)
                 (*m_interruptable)();
-            m().set_cancel(true);
+            m_limit.cancel();
-            if (m_rcf_manager.get() != 0)
+            m().limit().cancel();
-                m_rcf_manager->set_cancel(true);
         }
     }
     
@@ -323,7 +323,7 @@ namespace api {
     // -----------------------
     realclosure::manager & context::rcfm() {
         if (m_rcf_manager.get() == 0) {
-            m_rcf_manager = alloc(realclosure::manager, m_rcf_qm);
+            m_rcf_manager = alloc(realclosure::manager, m_limit, m_rcf_qm);
         }
         return *(m_rcf_manager.get());
     }

src/api/api_context.h

@@ -187,10 +187,12 @@ namespace api {
         //
         // -----------------------
     private:
+        reslimit                   m_limit;
         pmanager                   m_pmanager;
     public:
         polynomial::manager & pm() { return m_pmanager.pm(); }
-
+        reslimit & poly_limit() { return m_limit; }
+        
         // ------------------------
         //
         // RCF manager

src/api/api_polynomial.cpp

@@ -29,17 +29,13 @@ Notes:
 
 namespace api {
 
-    pmanager::pmanager():
+    pmanager::pmanager(reslimit& lim):
-        m_pm(m_nm) {
+        m_pm(lim, m_nm) {
     }
 
     pmanager::~pmanager() {
     }
     
-    void pmanager::set_cancel(bool f) {
-        m_pm.set_cancel(f);
-    }
-
 };
 
 extern "C" {
@@ -66,7 +62,7 @@ extern "C" {
             polynomial_ref r(pm);
             expr_ref _r(mk_c(c)->m());
             {
-                cancel_eh<reslimit> eh(mk_c(c)->m().limit());
+                cancel_eh<reslimit> eh(mk_c(c)->poly_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_polynomial.h

@@ -28,10 +28,9 @@ namespace api {
         polynomial::manager m_pm;
         // TODO: add support for caching expressions -> polynomial and back
     public:
-        pmanager();
+        pmanager(reslimit& limx);
         virtual ~pmanager();
         polynomial::manager & pm() { return m_pm; }
-        void set_cancel(bool f);
     };
 
 };

src/api/api_rcf.cpp

@@ -30,7 +30,7 @@ static rcmanager & rcfm(Z3_context c) {
 }
 
 static void reset_rcf_cancel(Z3_context c) {
-    rcfm(c).reset_cancel();
+    // no-op
 }
 
 static Z3_rcf_num from_rcnumeral(rcnumeral a) { 

src/ast/arith_decl_plugin.cpp

@@ -110,10 +110,6 @@ parameter arith_decl_plugin::translate(parameter const & p, decl_plugin & target
     return parameter(_target.aw().mk_id(aw().idx2anum(p.get_ext_id())), true);
 }
 
-void arith_decl_plugin::set_cancel(bool f) {
-    if (m_aw)
-        m_aw->m_amanager.set_cancel(f);
-}
 
 void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
     decl_plugin::set_manager(m, id);

src/ast/arith_decl_plugin.h

@@ -211,7 +211,6 @@ public:
 
     virtual expr * get_some_value(sort * s);
 
-    virtual void set_cancel(bool f);
 };
 
 /**
@@ -398,9 +397,6 @@ public:
         return m_manager.mk_eq(lhs, rhs);
     }
 
-    void set_cancel(bool f) {
-        plugin().set_cancel(f);
-    }
 };
 
 #endif /* ARITH_DECL_PLUGIN_H_ */

src/ast/ast.cpp

@@ -1433,12 +1433,6 @@ ast_manager::~ast_manager() {
     }
 }
 
-void ast_manager::set_cancel(bool f) {
-    for (unsigned i = 0; i < m_plugins.size(); i++) {
-        m_plugins[i]->set_cancel(f);
-    }
-}
-
 void ast_manager::compact_memory() {
     m_alloc.consolidate();
     unsigned capacity = m_ast_table.capacity();

src/ast/ast.h

@@ -932,7 +932,6 @@ public:
     virtual ~decl_plugin() {}
     virtual void finalize() {}
 
-    virtual void set_cancel(bool f) {}
 
     virtual decl_plugin * mk_fresh() = 0;
 
@@ -1472,9 +1471,6 @@ public:
     ~ast_manager();
 
     // propagate cancellation signal to decl_plugins
-    void set_cancel(bool f);
-    void cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
 
     bool has_trace_stream() const { return m_trace_stream != 0; }
     std::ostream & trace_stream() { SASSERT(has_trace_stream()); return *m_trace_stream; }

src/ast/normal_forms/name_exprs.cpp

@@ -87,9 +87,6 @@ public:
         TRACE("name_exprs", tout << mk_ismt2_pp(n, m_rw.m()) << "\n---->\n" << mk_ismt2_pp(r, m_rw.m()) << "\n";);
     }
     
-    virtual void set_cancel(bool f) {
-        m_rw.set_cancel(f);
-    }
 
     virtual void reset() {
         m_rw.reset();

src/ast/normal_forms/name_exprs.h

@@ -37,9 +37,6 @@ public:
                             proof_ref & p                      // [OUT] proof for (iff n p)
                             ) = 0;
     
-    virtual void set_cancel(bool f) = 0;
-    void cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
     virtual void reset() = 0;
 };
 

src/ast/rewriter/arith_rewriter.cpp

@@ -1032,9 +1032,6 @@ br_status arith_rewriter::mk_abs_core(expr * arg, expr_ref & result) {
     return BR_REWRITE2;
 }
 
-void arith_rewriter::set_cancel(bool f) {
-    m_util.set_cancel(f);
-}
 
 // Return true if t is of the form  c*Pi where c is a numeral.
 // Store c into k

src/ast/rewriter/arith_rewriter.h

@@ -167,8 +167,6 @@ public:
     }
     br_status mk_is_int(expr * arg, expr_ref & result);
 
-    void set_cancel(bool f);
-
     br_status mk_sin_core(expr * arg, expr_ref & result);
     br_status mk_cos_core(expr * arg, expr_ref & result);
     br_status mk_tan_core(expr * arg, expr_ref & result);

src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp

@@ -649,10 +649,6 @@ void bit_blaster_rewriter::updt_params(params_ref const& p) {
     m_imp->m_cfg.updt_params(p);
 }
 
-void bit_blaster_rewriter::set_cancel(bool f) {
-    m_imp->set_cancel(f);
-    m_imp->m_blaster.set_cancel(f);
-}
 
 void bit_blaster_rewriter::push() {
     m_imp->push();

src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h

@@ -30,7 +30,6 @@ public:
     bit_blaster_rewriter(ast_manager & m, params_ref const & p);
     ~bit_blaster_rewriter();
     void updt_params(params_ref const & p);
-    void set_cancel(bool f);
     ast_manager & m() const;
     unsigned get_num_steps() const;
     void cleanup();

src/ast/rewriter/bit_blaster/bit_blaster_tpl.h

@@ -36,7 +36,6 @@ protected:
     void mk_ext_rotate_left_right(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
 
     unsigned long long m_max_memory;
-    volatile bool      m_cancel;
     bool               m_use_wtm; /* Wallace Tree Multiplier */
     bool               m_use_bcm; /* Booth Multiplier for constants */
     void checkpoint();
@@ -45,7 +44,6 @@ public:
     bit_blaster_tpl(Cfg const & cfg = Cfg(), unsigned long long max_memory = UINT64_MAX, bool use_wtm = false, bool use_bcm=false):
         Cfg(cfg),
         m_max_memory(max_memory),
-        m_cancel(false),
         m_use_wtm(use_wtm),
         m_use_bcm(use_bcm) {
     }
@@ -54,9 +52,6 @@ public:
         m_max_memory = max_memory;
     }
 
-    void set_cancel(bool f) { m_cancel = f; }
-    void cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
     
     // Cfg required API
     ast_manager & m() const { return Cfg::m(); }

src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h

@@ -27,7 +27,7 @@ template<typename Cfg>
 void bit_blaster_tpl<Cfg>::checkpoint() {
     if (memory::get_allocation_size() > m_max_memory)
         throw rewriter_exception(Z3_MAX_MEMORY_MSG);
-    if (m_cancel)
+    if (m().canceled())
         throw rewriter_exception(Z3_CANCELED_MSG);
     cooperate("bit-blaster");
 }

src/ast/rewriter/der.cpp

@@ -444,12 +444,6 @@ void der_rewriter::operator()(expr * t, expr_ref & result, proof_ref & result_pr
     m_imp->operator()(t, result, result_pr);
 }
 
-void der_rewriter::set_cancel(bool f) {
-    #pragma omp critical (der_rewriter)
-    {
-        m_imp->set_cancel(f);
-    }
-}
 
 void der_rewriter::cleanup() {
     ast_manager & m = m_imp->m();

src/ast/rewriter/der.h

@@ -174,9 +174,6 @@ public:
 
     void operator()(expr * t, expr_ref & result, proof_ref & result_pr);
 
-    void cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
-    void set_cancel(bool f);
     void cleanup();
     void reset();
 };

src/ast/rewriter/expr_replacer.cpp

@@ -107,9 +107,6 @@ public:
         }
     }
 
-    virtual void set_cancel(bool f) {
-        m_replacer.set_cancel(f);
-    }
 
     virtual unsigned get_num_steps() const {
         return m_replacer.get_num_steps();
@@ -146,10 +143,6 @@ public:
         m_r.reset_used_dependencies();
     }
 
-    virtual void set_cancel(bool f) {
-        m_r.set_cancel(f);
-    }
-
     virtual unsigned get_num_steps() const { 
         return m_r.get_num_steps();
     }

src/ast/rewriter/expr_replacer.h

@@ -39,9 +39,6 @@ public:
     virtual void operator()(expr * t, expr_ref & result);
     virtual void operator()(expr_ref & t) { expr_ref s(t, m()); (*this)(s, t); }
 
-    void cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
-    virtual void set_cancel(bool f) = 0;
     virtual unsigned get_num_steps() const { return 0; }
     virtual void reset() = 0;
     

src/ast/rewriter/rewriter.h

@@ -212,7 +212,6 @@ protected:
     };
     Config &                   m_cfg;
     unsigned                   m_num_steps;
-    volatile bool              m_cancel;
     ptr_vector<expr>           m_bindings;
     var_shifter                m_shifter;
     expr_ref                   m_r;
@@ -333,10 +332,6 @@ public:
     Config & cfg() { return m_cfg; }
     Config const & cfg() const { return m_cfg; }
 
-    void set_cancel(bool f) { m_cancel = f; }
-    void cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
-
     ~rewriter_tpl();
     
     void reset();

src/ast/rewriter/rewriter_def.h

@@ -495,7 +495,6 @@ rewriter_tpl<Config>::rewriter_tpl(ast_manager & m, bool proof_gen, Config & cfg
     rewriter_core(m, proof_gen),
     m_cfg(cfg),
     m_num_steps(0),
-    m_cancel(false),
     m_shifter(m),
     m_r(m),
     m_pr(m),
@@ -576,8 +575,6 @@ template<bool ProofGen>
 void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr) {
     SASSERT(!frame_stack().empty());
     while (!frame_stack().empty()) {
-        if (m_cancel)
-            throw rewriter_exception(Z3_CANCELED_MSG);
         if (!m().canceled()) {
             if (m().limit().cancel_flag_set()) {
                 throw rewriter_exception(Z3_CANCELED_MSG);

src/ast/rewriter/th_rewriter.cpp

@@ -685,9 +685,6 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         return false;
     }
 
-    void set_cancel(bool f) {
-        m_a_rw.set_cancel(f);
-    }
 };
 
 template class rewriter_tpl<th_rewriter_cfg>;
@@ -734,13 +731,6 @@ unsigned th_rewriter::get_num_steps() const {
     return m_imp->get_num_steps();
 }
 
-void th_rewriter::set_cancel(bool f) {
-    #pragma omp critical (th_rewriter)
-    {
-        m_imp->set_cancel(f);
-        m_imp->cfg().set_cancel(f);
-    }
-}
 
 void th_rewriter::cleanup() {
     ast_manager & m = m_imp->m();

src/ast/rewriter/th_rewriter.h

@@ -45,9 +45,6 @@ public:
     void operator()(expr * t, expr_ref & result, proof_ref & result_pr);
     void operator()(expr * n, unsigned num_bindings, expr * const * bindings, expr_ref & result);
 
-    void cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
-    void set_cancel(bool f);
     void cleanup();
     void reset();
 

src/cmd_context/cmd_context.cpp

@@ -352,16 +352,15 @@ cmd_context::~cmd_context() {
 }
 
 void cmd_context::set_cancel(bool f) {
-    if (m_solver) {
+    if (has_manager()) {
+        m().set_cancel(f);
         if (f) {
-            m_solver->cancel();
+            m().limit().cancel();
         }
         else {
-            m_solver->reset_cancel();
+            m().limit().reset_cancel();
         }
     }
-    if (has_manager())
-        m().set_cancel(f);
 }
 
 opt_wrapper* cmd_context::get_opt() {
@@ -1453,7 +1452,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     else if (m_solver) {
         m_check_sat_result = m_solver.get(); // solver itself stores the result.
         m_solver->set_progress_callback(this);
-        cancel_eh<solver> eh(*m_solver);
+        cancel_eh<reslimit> eh(m().limit());
         scoped_ctrl_c ctrlc(eh);
         scoped_timer timer(timeout, &eh);
         scoped_rlimit _rlimit(m().limit(), rlimit);
@@ -1612,7 +1611,7 @@ void cmd_context::validate_model() {
     model_evaluator evaluator(*(md.get()), p);
     contains_array_op_proc contains_array(m());
     {
-        cancel_eh<model_evaluator> eh(evaluator);
+        cancel_eh<reslimit> eh(m().limit());
         expr_ref r(m());
         scoped_ctrl_c ctrlc(eh);
         ptr_vector<expr>::const_iterator it  = begin_assertions();

src/cmd_context/eval_cmd.cpp

@@ -64,7 +64,7 @@ public:
         expr_ref r(ctx.m());
         unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
         model_evaluator ev(*(md.get()), m_params);
-        cancel_eh<model_evaluator> eh(ev);
+        cancel_eh<reslimit> eh(ctx.m().limit());
         { 
             scoped_ctrl_c ctrlc(eh);
             scoped_timer timer(timeout, &eh);

src/cmd_context/extra_cmds/polynomial_cmds.cpp

@@ -33,7 +33,7 @@ Notes:
 
 static void to_poly(cmd_context & ctx, expr * t) {
     polynomial::numeral_manager nm;
-    polynomial::manager pm(nm);
+    polynomial::manager pm(ctx.m().limit(), nm);
     default_expr2polynomial expr2poly(ctx.m(), pm);
     polynomial::polynomial_ref p(pm);
     polynomial::scoped_numeral d(nm);
@@ -52,7 +52,7 @@ static void to_poly(cmd_context & ctx, expr * t) {
 
 static void factor(cmd_context & ctx, expr * t, polynomial::factor_params const & ps) {
     polynomial::numeral_manager nm;
-    polynomial::manager pm(nm);
+    polynomial::manager pm(ctx.m().limit(), nm);
     default_expr2polynomial expr2poly(ctx.m(), pm);
     polynomial::polynomial_ref p(pm);
     polynomial::scoped_numeral d(nm);
@@ -95,7 +95,7 @@ class poly_isolate_roots_cmd : public cmd {
         
         context(ast_manager & m):
             m_util(m),
-            m_pm(m_qm),
+            m_pm(m.limit(), m_qm),
             m_am(m_lim, m_qm),
             m_p(m_pm),
             m_expr2poly(m, m_pm),

src/cmd_context/tactic_cmds.cpp

@@ -199,7 +199,7 @@ public:
         ctx.set_check_sat_result(result.get());
         {
             tactic & t = *tref;
-            cancel_eh<tactic>  eh(t);
+            cancel_eh<reslimit>  eh(m.limit());
             {
                 scoped_ctrl_c ctrlc(eh);
                 scoped_timer timer(timeout, &eh);
@@ -310,7 +310,7 @@ public:
 
             std::string reason_unknown;
             bool failed = false;
-            cancel_eh<tactic>  eh(t);
+            cancel_eh<reslimit>  eh(m.limit());
             {
                 scoped_ctrl_c ctrlc(eh);
                 scoped_timer timer(timeout, &eh);

src/duality/duality_wrapper.h

@@ -936,8 +936,7 @@ namespace Duality {
 	void cancel(){
             scoped_proof_mode spm(m(),m_mode); 
             canceled = true;
-            if(m_solver)
+            m().limit().cancel();
-                m_solver->cancel();
 	}
 
 	unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();}

src/math/interval/interval.h

@@ -21,6 +21,7 @@ Revision History:
 
 #include"mpq.h"
 #include"ext_numeral.h"
+#include"rlimit.h"
 
 /**
    \brief Default configuration for interval manager.
@@ -110,6 +111,7 @@ public:
     typedef typename numeral_manager::numeral numeral;
     typedef typename C::interval              interval;
 private:
+    reslimit&  m_limit;
     C          m_c;
     numeral    m_result_lower;
     numeral    m_result_upper;
@@ -127,7 +129,6 @@ private:
     interval   m_3_pi_div_2;
     interval   m_2_pi;
 
-    volatile bool m_cancel;     
     
     void round_to_minus_inf() { m_c.round_to_minus_inf(); }
     void round_to_plus_inf() { m_c.round_to_plus_inf(); }
@@ -161,11 +162,9 @@ private:
     void checkpoint();
 
 public:    
-    interval_manager(C const & c);
+    interval_manager(reslimit& lim, C const & c);
     ~interval_manager();
 
-    void set_cancel(bool f) { m_cancel = f; }
-
     numeral_manager & m() const { return m_c.m(); }    
 
     void del(interval & a);

src/math/interval/interval_def.h

@@ -30,11 +30,10 @@ Revision History:
 // #define TRACE_NTH_ROOT
 
 template<typename C>
-interval_manager<C>::interval_manager(C const & c):m_c(c) { 
+interval_manager<C>::interval_manager(reslimit& lim, C const & c): m_limit(lim), m_c(c) { 
     m().set(m_minus_one, -1); 
     m().set(m_one, 1);
     m_pi_n = 0;
-    m_cancel = false;
 }
 
 template<typename C>
@@ -63,7 +62,7 @@ void interval_manager<C>::del(interval & a) {
 
 template<typename C>
 void interval_manager<C>::checkpoint() {
-    if (m_cancel)
+    if (m_limit.canceled())
         throw default_exception("canceled");
     cooperate("interval");
 }

src/math/polynomial/algebraic_numbers.cpp

@@ -83,7 +83,6 @@ namespace algebraic_numbers {
         scoped_upoly             m_add_tmp;
         polynomial::var          m_x;
         polynomial::var          m_y;
-        volatile bool            m_cancel;
         
         // configuration
         int                        m_min_magnitude;
@@ -104,8 +103,8 @@ namespace algebraic_numbers {
             m_qmanager(m),
             m_bqmanager(m),
             m_bqimanager(m_bqmanager),
-            m_pmanager(m, &a),
+            m_pmanager(lim, m, &a),
-            m_upmanager(m),
+            m_upmanager(lim, m),
             m_is_rational_tmp(m),
             m_isolate_tmp1(upm()),
             m_isolate_tmp2(upm()),
@@ -118,7 +117,6 @@ namespace algebraic_numbers {
             m_add_tmp(upm()) {
             updt_params(p);
             reset_statistics();
-            m_cancel = false;
             m_x = pm().mk_var();
             m_y = pm().mk_var();
         }
@@ -126,14 +124,8 @@ namespace algebraic_numbers {
         ~imp() {
         }
         
-        void set_cancel(bool f) {
-            m_cancel = f;
-            pm().set_cancel(f);
-            upm().set_cancel(f);
-        }
-
         void checkpoint() {
-            if (m_cancel)
+            if (!m_limit.inc())
                 throw algebraic_exception("canceled");
             cooperate("algebraic");
         }
@@ -2785,10 +2777,6 @@ namespace algebraic_numbers {
     void manager::updt_params(params_ref const & p) {
     }
 
-    void manager::set_cancel(bool f) {
-        m_imp->set_cancel(f);
-    }
-
     unsynch_mpq_manager & manager::qm() const {
         return m_imp->qm();
     }

src/math/polynomial/algebraic_numbers.h

@@ -64,10 +64,6 @@ namespace algebraic_numbers {
         static void get_param_descrs(param_descrs & r);
         static void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
 
-        void set_cancel(bool f);
-        void cancel() { set_cancel(true); }
-        void reset_cancel() { set_cancel(false); }
-
         void updt_params(params_ref const & p);
 
         unsynch_mpq_manager & qm() const;

src/math/polynomial/polynomial.cpp

@@ -1829,6 +1829,7 @@ namespace polynomial {
         typedef _scoped_numeral<numeral_manager> scoped_numeral;
         typedef _scoped_numeral_vector<numeral_manager> scoped_numeral_vector;
 
+        reslimit&                m_limit;
         manager &                m_wrapper;
         numeral_manager          m_manager;
         up_manager               m_upm;
@@ -1847,7 +1848,6 @@ namespace polynomial {
         unsigned_vector          m_degree2pos;
         bool                     m_use_sparse_gcd;
         bool                     m_use_prs_gcd;
-        volatile bool            m_cancel;
 
         // Debugging method: check if the coefficients of p are in the numeral_manager.
         bool consistent_coeffs(polynomial const * p) {
@@ -2323,13 +2323,13 @@ namespace polynomial {
             inc_ref(m_unit_poly);
             m_use_sparse_gcd = true;
             m_use_prs_gcd = false;
-            m_cancel = false;
         }
 
-        imp(manager & w, unsynch_mpz_manager & m, monomial_manager * mm):
+        imp(reslimit& lim, manager & w, unsynch_mpz_manager & m, monomial_manager * mm):
+            m_limit(lim),
             m_wrapper(w),
             m_manager(m),
-            m_upm(m) {
+            m_upm(lim, m) {
             if (mm == 0)
                 mm = alloc(monomial_manager);
             m_monomial_manager = mm;
@@ -2337,10 +2337,11 @@ namespace polynomial {
             init();
         }
 
-        imp(manager & w, unsynch_mpz_manager & m, small_object_allocator * a):
+        imp(reslimit& lim, manager & w, unsynch_mpz_manager & m, small_object_allocator * a):
+            m_limit(lim),
             m_wrapper(w),
             m_manager(m),
-            m_upm(m) {
+            m_upm(lim, m) {
             m_monomial_manager = alloc(monomial_manager, a);
             m_monomial_manager->inc_ref();
             init();
@@ -2371,13 +2372,8 @@ namespace polynomial {
             m_monomial_manager->dec_ref();
         }
 
-        void set_cancel(bool f) {
-            m_cancel = f;
-            m_upm.set_cancel(f);
-        }
-
         void checkpoint() {
-            if (m_cancel) {
+            if (!m_limit.inc()) {
                 throw polynomial_exception("canceled");
             }
             cooperate("polynomial");
@@ -6883,12 +6879,12 @@ namespace polynomial {
         }
     };
 
-    manager::manager(numeral_manager & m, monomial_manager * mm) {
+    manager::manager(reslimit& lim, numeral_manager & m, monomial_manager * mm) {
-        m_imp = alloc(imp, *this, m, mm);
+        m_imp = alloc(imp, lim, *this, m, mm);
     }
 
-    manager::manager(numeral_manager & m, small_object_allocator * a) {
+    manager::manager(reslimit& lim, numeral_manager & m, small_object_allocator * a) {
-        m_imp = alloc(imp, *this, m, a);
+        m_imp = alloc(imp, lim, *this, m, a);
     }
 
     manager::~manager() {
@@ -6927,10 +6923,6 @@ namespace polynomial {
         return m_imp->mm().allocator();
     }
     
-    void manager::set_cancel(bool f) {
-        m_imp->set_cancel(f);
-    }
-
     void manager::add_del_eh(del_eh * eh) {
         m_imp->add_del_eh(eh);
     }

src/math/polynomial/polynomial.h

@@ -28,6 +28,7 @@ Notes:
 #include"scoped_numeral_vector.h"
 #include"params.h"
 #include"mpbqi.h"
+#include"rlimit.h"
 
 class small_object_allocator;
 
@@ -190,8 +191,8 @@ namespace polynomial {
     private:
         imp * m_imp;
     public:
-        manager(numeral_manager & m, monomial_manager * mm = 0);
+        manager(reslimit& lim, numeral_manager & m, monomial_manager * mm = 0);
-        manager(numeral_manager & m, small_object_allocator * a);
+        manager(reslimit& lim, numeral_manager & m, small_object_allocator * a);
         ~manager();
 
         numeral_manager & m() const;
@@ -218,10 +219,6 @@ namespace polynomial {
         void set_zp(numeral const & p);
         void set_zp(uint64 p);
 
-        void set_cancel(bool f);
-        void cancel() { set_cancel(true); }
-        void reset_cancel() { set_cancel(false); }
-
         /**
            \brief Abstract event handler.
         */

src/math/polynomial/rpolynomial.cpp

@@ -58,7 +58,6 @@ namespace rpolynomial {
         numeral_manager &                m_manager;
         small_object_allocator *         m_allocator;
         bool                             m_own_allocator;
-        volatile bool                    m_cancel;
         
         imp(manager & w, numeral_manager & m, small_object_allocator * a):
             m_wrapper(w),
@@ -67,7 +66,6 @@ namespace rpolynomial {
             m_own_allocator(a == 0) {
             if (a == 0)
                 m_allocator = alloc(small_object_allocator, "rpolynomial");
-            m_cancel = false;
         }
 
         ~imp() {

src/math/polynomial/rpolynomial.h

@@ -57,8 +57,6 @@ namespace rpolynomial {
         numeral_manager & m() const;
         small_object_allocator & allocator() const;
 
-        void set_cancel(bool f);
-
         /**
            \brief Create a new variable.
         */

src/math/polynomial/upolynomial.cpp

@@ -134,9 +134,9 @@ namespace upolynomial {
         std::swap(m_total_degree, other.m_total_degree);
     }
 
-    core_manager::core_manager(unsynch_mpz_manager & m):
+    core_manager::core_manager(reslimit& lim, unsynch_mpz_manager & m):
+        m_limit(lim),
         m_manager(m) {
-        m_cancel = false;
     }
 
     core_manager::~core_manager() {
@@ -153,12 +153,8 @@ namespace upolynomial {
         reset(m_pw_tmp);
     }
 
-    void core_manager::set_cancel(bool f) {
-        m_cancel = f;
-    }
-
     void core_manager::checkpoint() {
-        if (m_cancel)
+        if (!m_limit.inc()) 
             throw upolynomial_exception("canceled");
         cooperate("upolynomial");
     }

src/math/polynomial/upolynomial.h

@@ -29,6 +29,7 @@ Notes:
 #include"polynomial.h"
 #include"z3_exception.h"
 #include"mpbq.h"
+#include"rlimit.h"
 #define FACTOR_VERBOSE_LVL 1000
 
 namespace upolynomial {
@@ -101,6 +102,7 @@ namespace upolynomial {
         };
 
     protected:
+        reslimit&         m_limit;
         numeral_manager   m_manager;
         numeral_vector    m_basic_tmp;
         numeral_vector    m_div_tmp1;
@@ -114,7 +116,6 @@ namespace upolynomial {
         numeral_vector    m_sqf_tmp1;
         numeral_vector    m_sqf_tmp2;
         numeral_vector    m_pw_tmp;
-        volatile bool     m_cancel;
 
         static bool is_alias(numeral const * p, numeral_vector & buffer) { return buffer.c_ptr() != 0 && buffer.c_ptr() == p; }
         void neg_core(unsigned sz1, numeral const * p1, numeral_vector & buffer);
@@ -128,12 +129,12 @@ namespace upolynomial {
         void CRA_combine_images(numeral_vector const & q, numeral const & p, numeral_vector & C, numeral & bound);
 
     public:
-        core_manager(z_numeral_manager & m);
+        core_manager(reslimit& lim, z_numeral_manager & m);
         ~core_manager();
 
         z_numeral_manager & zm() const { return m_manager.m(); }
         numeral_manager & m() const { return const_cast<core_manager*>(this)->m_manager; }
-
+        reslimit& lim() const { return m_limit; }
         /**
            \brief Return true if Z_p[X]
         */
@@ -156,7 +157,6 @@ namespace upolynomial {
 
         void checkpoint();
 
-        void set_cancel(bool f);
 
         /**
            \brief set p size to 0. That is, p is the zero polynomial after this operation.
@@ -576,7 +576,7 @@ namespace upolynomial {
         bool factor_core(unsigned sz, numeral const * p, factors & r, factor_params const & params);
 
     public:
-        manager(z_numeral_manager & m):core_manager(m) {}
+        manager(reslimit& lim, z_numeral_manager & m):core_manager(lim, m) {}
         ~manager();
 
         void reset(numeral_vector & p) { core_manager::reset(p); }

src/math/polynomial/upolynomial_factorization.cpp

@@ -518,7 +518,7 @@ bool check_hansel_lift(z_manager & upm, numeral_vector const & C,
     scoped_mpz br(nm);
     nm.mul(b, r, br);
     
-    zp_manager br_upm(upm.zm());
+    zp_manager br_upm(upm.lim(), upm.zm());
     br_upm.set_zp(br);
 
     if (A_lifted.size() != A.size()) return false;
@@ -543,7 +543,7 @@ bool check_hansel_lift(z_manager & upm, numeral_vector const & C,
         return false;
     }
 
-    zp_manager b_upm(nm);
+    zp_manager b_upm(upm.lim(), nm);
     b_upm.set_zp(b);
 
     // test2: A_lifted = A (mod b)
@@ -596,7 +596,7 @@ void hensel_lift(z_manager & upm, numeral const & a, numeral const & b, numeral
         tout << "C = "; upm.display(tout, C); tout << ")" << endl;
     );
 
-    zp_manager r_upm(nm);
+    zp_manager r_upm(upm.lim(), nm);
     r_upm.set_zp(r);
 
     SASSERT(upm.degree(C) == upm.degree(A) + upm.degree(B));
@@ -717,7 +717,7 @@ void hensel_lift_quadratic(z_manager& upm, numeral_vector const & C,
     );
 
     // we create a new Z_p manager, since we'll be changing the input one
-    zp_manager zp_upm(nm);
+    zp_manager zp_upm(upm.lim(), nm);
     zp_upm.set_zp(zpe_upm.m().p());
 
     // get the U, V, such that A*U + B*V = 1 (mod p)
@@ -1055,7 +1055,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs,
     // the variables we'll be using and updating in Z_p
     scoped_numeral p(nm); 
     nm.set(p, 2);
-    zp_manager zp_upm(nm.m());
+    zp_manager zp_upm(upm.lim(), nm.m());
     zp_upm.set_zp(p);
     zp_factors zp_fs(zp_upm);
     scoped_numeral zp_fs_p(nm); nm.set(zp_fs_p, 2);
@@ -1163,7 +1163,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs,
           );
     
     // we got a prime factoring, so we do the lifting now
-    zp_manager zpe_upm(nm.m());
+    zp_manager zpe_upm(upm.lim(), nm.m());
     zpe_upm.set_zp(zp_fs_p);
     zp_numeral_manager & zpe_nm = zpe_upm.m();
     

src/math/realclosure/realclosure.cpp

@@ -369,6 +369,7 @@ namespace realclosure {
         typedef sbuffer<int, REALCLOSURE_INI_BUFFER_SIZE> int_buffer;
         typedef sbuffer<unsigned, REALCLOSURE_INI_BUFFER_SIZE> unsigned_buffer;
         
+        reslimit&                      m_limit;
         small_object_allocator *       m_allocator;
         bool                           m_own_allocator;
         unsynch_mpq_manager &          m_qm;
@@ -400,7 +401,6 @@ namespace realclosure {
 
         bool                           m_in_aux_values; // True if we are computing SquareFree polynomials or Sturm sequences. That is, the values being computed will be discarded.
 
-        volatile bool                  m_cancel;
 
         struct scoped_polynomial_seq {
             typedef ref_buffer<value, imp, REALCLOSURE_INI_SEQ_SIZE> value_seq;
@@ -494,7 +494,8 @@ namespace realclosure {
         #define INC_DEPTH() ((void) 0)
         #endif
 
-        imp(unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
+        imp(reslimit& lim, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
+            m_limit(lim),
             m_allocator(a == 0 ? alloc(small_object_allocator, "realclosure") : a),
             m_own_allocator(a == 0),
             m_qm(qm),
@@ -514,7 +515,6 @@ namespace realclosure {
 
             m_in_aux_values = false;
 
-            m_cancel = false;
             
             updt_params(p);
         }
@@ -547,7 +547,7 @@ namespace realclosure {
         small_object_allocator & allocator() { return *m_allocator; }
 
         void checkpoint() {
-            if (m_cancel)
+            if (!m_limit.inc())
                 throw exception("canceled");
             cooperate("rcf");
         }
@@ -730,9 +730,6 @@ namespace realclosure {
             return m_extensions[extension::ALGEBRAIC].size();
         }
         
-        void set_cancel(bool f) {
-            m_cancel = f;
-        }
         
         void updt_params(params_ref const & _p) {
             rcf_params p(_p);
@@ -6033,8 +6030,8 @@ namespace realclosure {
         ~save_interval_ctx() { m->restore_saved_intervals(); }
     };
 
-    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_imp = alloc(imp, m, p, a);
+        m_imp = alloc(imp, lim, m, p, a);
     }
         
     manager::~manager() {
@@ -6045,10 +6042,6 @@ namespace realclosure {
         rcf_params::collect_param_descrs(r);
     }
 
-    void manager::set_cancel(bool f) {
-        m_imp->set_cancel(f);
-    }
-
     void manager::updt_params(params_ref const & p) {
         m_imp->updt_params(p);
     }

src/math/realclosure/realclosure.h

@@ -28,6 +28,7 @@ Notes:
 #include"scoped_numeral_vector.h"
 #include"interval.h"
 #include"z3_exception.h"
+#include"rlimit.h"
 
 namespace realclosure {
     class num;
@@ -47,7 +48,7 @@ namespace realclosure {
         friend class save_interval_ctx;
         imp * m_imp;
     public:
-        manager(unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
+        manager(reslimit& lim, unsynch_mpq_manager & m, params_ref const & p = params_ref(), small_object_allocator * a = 0);
         ~manager();
         typedef num                             numeral;
         typedef svector<numeral>                numeral_vector;
@@ -57,9 +58,6 @@ namespace realclosure {
         static void get_param_descrs(param_descrs & r);
         static void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
 
-        void set_cancel(bool f);
-        void cancel() { set_cancel(true); }
-        void reset_cancel() { set_cancel(false); }
 
         void updt_params(params_ref const & p);
 

src/math/simplex/simplex.h

@@ -97,7 +97,6 @@ namespace simplex {
         mutable eps_manager         em;
         mutable matrix              M;
         unsigned                    m_max_iterations;
-        volatile bool               m_cancel;
         var_heap                    m_to_patch;
         vector<var_info>            m_vars;
         svector<var_t>              m_row2base;

src/math/subpaving/subpaving_t.h

@@ -31,6 +31,7 @@ Revision History:
 #include"statistics.h"
 #include"lbool.h"
 #include"id_gen.h"
+#include"rlimit.h"
 #ifdef _MSC_VER
 #pragma warning(disable : 4200)
 #pragma warning(disable : 4355)
@@ -526,8 +527,6 @@ private:
     numeral                   m_tmp1, m_tmp2, m_tmp3;
     interval                  m_i_tmp1, m_i_tmp2, m_i_tmp3;
 
-    // Cancel flag
-    volatile bool             m_cancel;
 
     friend class node;
 
@@ -759,7 +758,7 @@ private:
     bool check_invariant() const;
 
 public:
-    context_t(C const & c, params_ref const & p, small_object_allocator * a);
+    context_t(reslimit& lim, C const & c, params_ref const & p, small_object_allocator * a);
     ~context_t();
 
     /**
@@ -835,8 +834,6 @@ public:
 
     void set_display_proc(display_var_proc * p) { m_display_proc = p; }
 
-    void set_cancel(bool f) { m_cancel = f; im().set_cancel(f); }
-
     void updt_params(params_ref const & p);
 
     static void collect_param_descrs(param_descrs & d);

src/math/subpaving/subpaving_t_def.h

@@ -431,7 +431,6 @@ context_t<C>::context_t(C const & c, params_ref const & p, small_object_allocato
     m_node_selector = alloc(breadth_first_node_selector<C>, this);
     m_var_selector  = alloc(round_robing_var_selector<C>, this);
     m_node_splitter = alloc(midpoint_node_splitter<C>, this);
-    m_cancel        = false;
     m_num_nodes     = 0;
     updt_params(p);
     reset_statistics();
@@ -459,7 +458,7 @@ context_t<C>::~context_t() {
 
 template<typename C>
 void context_t<C>::checkpoint() {
-    if (m_cancel)
+    if (m_limit.canceled())
         throw default_exception("canceled");
     if (memory::get_allocation_size() > m_max_memory)
         throw default_exception(Z3_MAX_MEMORY_MSG);

src/math/subpaving/tactic/expr2subpaving.cpp

@@ -51,7 +51,6 @@ struct expr2subpaving::imp {
 
     obj_map<expr, subpaving::ineq*>    m_lit_cache;
 
-    volatile bool                      m_cancel;
 
     imp(ast_manager & m, subpaving::context & s, expr2var * e2v):
         m_manager(m),
@@ -71,7 +70,6 @@ struct expr2subpaving::imp {
             m_expr2var_owner = false;
         }
         
-        m_cancel = false;
     }
     
     ~imp() {
@@ -95,7 +93,7 @@ struct expr2subpaving::imp {
     }
 
     void checkpoint() {
-        if (m_cancel)
+        if (m().canceled())
             throw default_exception("canceled");
         cooperate("expr2subpaving");
     }
@@ -357,9 +355,6 @@ struct expr2subpaving::imp {
         return m_expr2var->is_var(t); 
     }
 
-    void set_cancel(bool f) {
-        m_cancel = f;
-    }
     
     subpaving::var internalize_term(expr * t, mpz & n, mpz & d) {
         return process(t, 0, n, d);
@@ -386,9 +381,6 @@ bool expr2subpaving::is_var(expr * t) const {
     return m_imp->is_var(t);
 }
     
-void expr2subpaving::set_cancel(bool f) {
-    m_imp->set_cancel(f);
-}
 
 subpaving::var expr2subpaving::internalize_term(expr * t, mpz & n, mpz & d) {
     return m_imp->internalize_term(t, n, d);

src/math/subpaving/tactic/expr2subpaving.h

@@ -40,12 +40,7 @@ public:
        \brief Return true if t was encoded as a variable by the translator.
     */
     bool is_var(expr * t) const;
-    
+       
-    /**
-       \brief Cancel/Interrupt execution.
-    */
-    void set_cancel(bool f);
-    
     /**
        \brief Internalize a Z3 arithmetical expression into the subpaving data-structure.
 

src/math/subpaving/tactic/subpaving_tactic.cpp

@@ -124,7 +124,6 @@ class subpaving_tactic : public tactic {
         }
 
         void set_cancel(bool f) {
-            m_e2s->set_cancel(f);
             m_ctx->set_cancel(f);
         }
 
@@ -279,11 +278,6 @@ public:
         }
     }
 
-protected:
-    virtual void set_cancel(bool f) {
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
 };
 
 

src/model/model_evaluator.cpp

@@ -256,12 +256,6 @@ unsigned model_evaluator::get_num_steps() const {
     return m_imp->get_num_steps();
 }
 
-void model_evaluator::set_cancel(bool f) {
-    #pragma omp critical (model_evaluator)
-    {
-        m_imp->set_cancel(f);
-    }
-}
 
 void model_evaluator::cleanup(params_ref const & p) {
     model & md = m_imp->cfg().m_model;

src/model/model_evaluator.h

@@ -41,9 +41,6 @@ public:
 
     void operator()(expr * t, expr_ref & r);
 
-    void set_cancel(bool f);
-    void cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
     void cleanup(params_ref const & p = params_ref());
     void reset(params_ref const & p = params_ref());
     

src/muz/fp/horn_tactic.cpp

@@ -63,9 +63,6 @@ class horn_tactic : public tactic {
             m_ctx.collect_statistics(st);
         }
 
-        void set_cancel(bool f) {
-        }
-
         void normalize(expr_ref& f) {
             bool is_positive = true;
             expr* e = 0;
@@ -420,11 +417,7 @@ public:
         }
     }
     
-protected:
+
-    virtual void set_cancel(bool f) {
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
 };
 
 tactic * mk_horn_tactic(ast_manager & m, params_ref const & p) {

src/nlsat/nlsat_solver.cpp

@@ -141,7 +141,6 @@ namespace nlsat {
         svector<trail>         m_trail;
 
         anum                   m_zero;
-        bool                   m_cancel;
 
         // configuration
         unsigned long long     m_max_memory;
@@ -164,7 +163,7 @@ namespace nlsat {
             m_solver(s),
             m_rlimit(rlim),
             m_allocator("nlsat"),
-            m_pm(m_qm, &m_allocator),
+            m_pm(rlim, m_qm, &m_allocator),
             m_cache(m_pm),
             m_am(rlim, m_qm, p, &m_allocator),
             m_asm(*this, m_allocator),
@@ -180,7 +179,6 @@ namespace nlsat {
             m_lemma_assumptions(m_asm) {
             updt_params(p);
             reset_statistics();
-            m_cancel = false;
             mk_true_bvar();
         }
         
@@ -218,15 +216,11 @@ namespace nlsat {
             m_am.updt_params(p.p);
         }
 
-        void set_cancel(bool f) {
-            m_pm.set_cancel(f);
-            m_am.set_cancel(f);
-            m_cancel = f;
-        }
-
         void checkpoint() {
-            if (m_cancel) throw solver_exception(Z3_CANCELED_MSG);
+            if (!m_rlimit.inc()) {
-            if (!m_rlimit.inc()) throw solver_exception(Z3_MAX_RESOURCE_MSG);
+                if (m_rlimit.cancel_flag_set()) throw solver_exception(Z3_CANCELED_MSG);
+                throw solver_exception(Z3_MAX_RESOURCE_MSG);
+            }
             if (memory::get_allocation_size() > m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG);
         }
 
@@ -2571,10 +2565,6 @@ namespace nlsat {
         return m_imp->check();
     }
 
-    void solver::set_cancel(bool f) {
-        m_imp->set_cancel(f);
-    }
-
     void solver::collect_param_descrs(param_descrs & d) {
         algebraic_numbers::manager::collect_param_descrs(d);
         nlsat_params::collect_param_descrs(d);

src/nlsat/nlsat_solver.h

@@ -154,7 +154,6 @@ namespace nlsat {
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
 
-        void set_cancel(bool f);
         void collect_statistics(statistics & st);
         void reset_statistics();
         void display_status(std::ostream & out) const;

src/nlsat/tactic/goal2nlsat.cpp

@@ -61,7 +61,6 @@ struct goal2nlsat::imp {
     unsigned long long        m_max_memory;
     bool                      m_factor;
 
-    volatile bool             m_cancel;
 
     imp(ast_manager & _m, params_ref const & p, nlsat::solver & s, expr2var & a2b, expr2var & t2x):
         m(_m),
@@ -73,7 +72,6 @@ struct goal2nlsat::imp {
         m_t2x(t2x),
         m_expr2poly(m_solver, m, m_solver.pm(), &m_t2x) {
         updt_params(p);
-        m_cancel = false;
     }
 
     void updt_params(params_ref const & p) {
@@ -82,11 +80,6 @@ struct goal2nlsat::imp {
         m_fparams.updt_params(p);
     }
 
-    void set_cancel(bool f) {
-        m_cancel = f;
-        m_pm.set_cancel(f);
-    }
-
     nlsat::atom::kind flip(nlsat::atom::kind k) {
         switch (k) {
         case nlsat::atom::EQ: return k;
@@ -303,7 +296,3 @@ void goal2nlsat::operator()(goal const & g, params_ref const & p, nlsat::solver
     local_imp(g);
 }
     
-void goal2nlsat::set_cancel(bool f) {
-    if (m_imp)
-        m_imp->set_cancel(f);
-}

src/nlsat/tactic/goal2nlsat.h

@@ -51,7 +51,6 @@ public:
     */
     void operator()(goal const & g, params_ref const & p, nlsat::solver & s, expr2var & a2b, expr2var & t2x);
     
-    void set_cancel(bool f);
 };
 
 class nlsat2goal {
@@ -69,7 +68,6 @@ public:
     void operator()(nlsat::solver const & s, expr2var const & a2b, expr2var const & t2x,
                     params_ref const & p, goal & g, model_converter_ref & mc);
     
-    void set_cancel(bool f);
 };
 
 #endif

src/nlsat/tactic/nlsat_tactic.cpp

@@ -57,11 +57,6 @@ class nlsat_tactic : public tactic {
             m_params = p;
             m_solver.updt_params(p);
         }
-
-        void set_cancel(bool f) {
-            m_solver.set_cancel(f);
-            m_g2nl.set_cancel(f);
-        }
         
         bool contains_unsupported(expr_ref_vector & b2a, expr_ref_vector & x2t) {
             for (unsigned x = 0; x < x2t.size(); x++) {
@@ -240,11 +235,6 @@ public:
     
     virtual void cleanup() {}
     
-    virtual void set_cancel(bool f) {
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
-
     virtual void collect_statistics(statistics & st) const {
         st.copy(m_stats);
     }

src/opt/mus.cpp

@@ -33,25 +33,20 @@ struct mus::imp {
     ast_manager&             m;
     expr_ref_vector          m_cls2expr;
     obj_map<expr, unsigned>  m_expr2cls;
-    volatile bool            m_cancel;
     model_ref                m_model;
     expr_ref_vector          m_soft;
     vector<rational>         m_weights;
     rational                 m_weight;
 
     imp(solver& s, ast_manager& m): 
-        m_s(s), m(m), m_cls2expr(m),  m_cancel(false), m_soft(m)
+        m_s(s), m(m), m_cls2expr(m),  m_soft(m)
     {}
 
     void reset() {
         m_cls2expr.reset();
         m_expr2cls.reset();
     }
-        
+            
-    void set_cancel(bool f) {
-        m_cancel = f;
-    }
-    
     
     unsigned add_soft(expr* cls) {
         SASSERT(is_uninterp_const(cls) || 
@@ -216,9 +211,6 @@ lbool mus::get_mus(unsigned_vector& mus) {
     return m_imp->get_mus(mus);
 }
 
-void mus::set_cancel(bool f) {
-    m_imp->set_cancel(f);
-}
 
 void mus::reset() {
     m_imp->reset();

src/opt/mus.h

@@ -39,8 +39,6 @@ namespace opt {
         
         void reset();
         
-        void set_cancel(bool f);
-
         /**
            Instrument MUS extraction to also provide the minimal
            penalty model, if any is found.

src/opt/opt_cmds.cpp

@@ -195,7 +195,7 @@ public:
             opt.add_hard_constraint(*it);
         }
         lbool r = l_undef;
-        cancel_eh<opt::context> eh(opt);        
+        cancel_eh<reslimit> eh(m.limit());
         {
             scoped_ctrl_c ctrlc(eh);
             scoped_timer timer(timeout, &eh);

src/opt/opt_solver.cpp

@@ -297,11 +297,7 @@ namespace opt {
         m_context.get_relevant_labels(0, tmp);
         r.append(tmp.size(), tmp.c_ptr());
     }
-    
+        
-    void opt_solver::set_cancel(bool f) {
-        m_context.set_cancel(f);
-    }
-    
     void opt_solver::set_progress_callback(progress_callback * callback) {
         m_callback = callback;
         m_context.set_progress_callback(callback);

src/opt/opt_solver.h

@@ -100,11 +100,11 @@ namespace opt {
         virtual proof * get_proof();
         virtual std::string reason_unknown() const;
         virtual void get_labels(svector<symbol> & r);
-        virtual void set_cancel(bool f);
         virtual void set_progress_callback(progress_callback * callback);
         virtual unsigned get_num_assertions() const;
         virtual expr * get_assertion(unsigned idx) const;
         virtual void display(std::ostream & out) const;
+        virtual ast_manager& get_manager() { return m; } 
         void set_logic(symbol const& logic);
 
         smt::theory_var add_objective(app* term);

src/sat/sat_mus.cpp

@@ -84,7 +84,7 @@ namespace sat {
                   tout << "core: " << core << "\n";
                   tout << "mus:  " << mus  << "\n";);
 
-            if (s.m_cancel) {
+            if (s.canceled()) {
                 set_core();
                 return l_undef;
             }

src/sat/sat_sls.cpp

@@ -50,7 +50,7 @@ namespace sat {
         return m_elems[rnd(num_elems())];
     }
 
-    sls::sls(solver& s): s(s), m_cancel(false) {
+    sls::sls(solver& s): s(s) {
         m_prob_choose_min_var = 43;
         m_clause_generation = 0;
     }
@@ -64,7 +64,7 @@ namespace sat {
     lbool sls::operator()(unsigned sz, literal const* tabu, bool reuse_model) {
         init(sz, tabu, reuse_model);
         unsigned i;
-        for (i = 0; !m_false.empty() && !m_cancel && i < m_max_tries; ++i) {
+        for (i = 0; !m_false.empty() && !s.canceled() && i < m_max_tries; ++i) {
             flip();
         }
         IF_VERBOSE(2, verbose_stream() << "tries " << i << "\n";);
@@ -378,7 +378,7 @@ namespace sat {
         }
         DEBUG_CODE(check_invariant(););
         unsigned i = 0;
-        for (; !m_cancel && m_best_value > 0 && i < m_max_tries; ++i) {
+        for (; !s.canceled() && m_best_value > 0 && i < m_max_tries; ++i) {
             wflip();
             if (m_false.empty()) {
                 double val = evaluate_model(m_model);

src/sat/sat_sls.h

@@ -54,12 +54,10 @@ namespace sat {
         clause_allocator m_alloc;              // clause allocator
         clause_vector    m_bin_clauses;        // binary clauses
         svector<bool>    m_tabu;               // variables that cannot be swapped
-        volatile bool    m_cancel;
     public:
         sls(solver& s);
         virtual ~sls();        
         lbool operator()(unsigned sz, literal const* tabu, bool reuse_model);
-        void set_cancel(bool f) { m_cancel = f; }
         void set_max_tries(unsigned mx) { m_max_tries = mx; }
         virtual void display(std::ostream& out) const;
     protected:

src/sat/sat_solver.cpp

@@ -32,7 +32,6 @@ Revision History:
 namespace sat {
 
     solver::solver(params_ref const & p, reslimit& l, extension * ext):
-        m_cancel(false),
         m_rlimit(l),
         m_config(p),
         m_ext(ext),
@@ -2714,11 +2713,6 @@ namespace sat {
         scc::collect_param_descrs(d);
     }
 
-    void solver::set_cancel(bool f) {
-        m_cancel = f;
-        m_wsls.set_cancel(f);
-    }
-
     void solver::collect_statistics(statistics & st) const {
         m_stats.collect_statistics(st);
         m_cleaner.collect_statistics(st);
@@ -2784,7 +2778,7 @@ namespace sat {
     //
     // -----------------------
     bool solver::check_invariant() const {
-        if (m_cancel) return true;
+        if (!m_rlimit.inc()) return true;
         integrity_checker checker(*this);
         SASSERT(checker());
         return true;

src/sat/sat_solver.h

@@ -71,7 +71,6 @@ namespace sat {
     public:
         struct abort_solver {};
     protected:
-        volatile bool           m_cancel;
         reslimit&               m_rlimit;
         config                  m_config;
         stats                   m_stats;
@@ -158,7 +157,6 @@ namespace sat {
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
 
-        void set_cancel(bool f);
         void collect_statistics(statistics & st) const;
         void reset_statistics();
         void display_status(std::ostream & out) const;
@@ -239,13 +237,13 @@ namespace sat {
         lbool status(clause const & c) const;        
         clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
         void checkpoint() {
-            if (m_cancel) throw solver_exception(Z3_CANCELED_MSG);
+            if (!m_rlimit.inc()) { throw solver_exception(Z3_CANCELED_MSG); }
-            if (!m_rlimit.inc()) { m_cancel = true; throw solver_exception(Z3_CANCELED_MSG); }
             ++m_num_checkpoints;
             if (m_num_checkpoints < 10) return;
             m_num_checkpoints = 0;
             if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG);
         }
+        bool canceled() { return !m_rlimit.inc(); }
         typedef std::pair<literal, literal> bin_clause;
     protected:
         watch_list & get_wlist(literal l) { return m_watches[l.index()]; }

src/sat/sat_solver/inc_sat_solver.cpp

@@ -85,7 +85,6 @@ public:
         simp2_p.set_bool("flat", true); // required by som
         simp2_p.set_bool("hoist_mul", false); // required by som
         simp2_p.set_bool("elim_and", true);
-
         m_preprocess = 
             and_then(mk_card2bv_tactic(m, m_params),
                      using_params(mk_simplify_tactic(m), simp2_p),
@@ -169,11 +168,6 @@ public:
         }
         return r;
     }
-    virtual void set_cancel(bool f) {
-        m_goal2sat.set_cancel(f);
-        m_solver.set_cancel(f);
-        if (f) m_preprocess->cancel(); else m_preprocess->reset_cancel();
-    }
     virtual void push() {
         internalize_formulas();
         m_solver.user_push();
@@ -215,6 +209,7 @@ public:
             assert_expr(t);
         }
     }
+    virtual ast_manager& get_manager() { return m; }
     virtual void assert_expr(expr * t) {
         TRACE("sat", tout << mk_pp(t, m) << "\n";);
         m_fmls.push_back(t);

src/sat/tactic/goal2sat.cpp

@@ -58,7 +58,6 @@ struct goal2sat::imp {
     sat::bool_var               m_true;
     bool                        m_ite_extra;
     unsigned long long          m_max_memory;
-    volatile bool               m_cancel;
     expr_ref_vector             m_trail;
     bool                        m_default_external;
     
@@ -70,7 +69,6 @@ struct goal2sat::imp {
         m_trail(m),
         m_default_external(default_external) {
         updt_params(p);
-        m_cancel = false;
         m_true = sat::null_bool_var;
     }
         
@@ -334,7 +332,7 @@ struct goal2sat::imp {
         while (!m_frame_stack.empty()) {
         loop:
             cooperate("goal2sat");
-            if (m_cancel)
+            if (m.canceled())
                 throw tactic_exception(TACTIC_CANCELED_MSG);
             if (memory::get_allocation_size() > m_max_memory)
                 throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
@@ -442,7 +440,6 @@ struct goal2sat::imp {
             process(fs[i]);
     }
 
-    void set_cancel(bool f) { m_cancel = f; }
 };
 
 struct unsupported_bool_proc {
@@ -507,14 +504,6 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t,
     proc(g);
 }
 
-void goal2sat::set_cancel(bool f) {
-    #pragma omp critical (goal2sat)
-    {
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
-}
-
 
 struct sat2goal::imp {
 
@@ -631,9 +620,8 @@ struct sat2goal::imp {
     expr_ref_vector         m_lit2expr;
     unsigned long long      m_max_memory;
     bool                    m_learned;
-    volatile bool           m_cancel;
     
-    imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m), m_cancel(false) {
+    imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m) {
         updt_params(p);
     }
 
@@ -643,7 +631,7 @@ struct sat2goal::imp {
     }
 
     void checkpoint() {
-        if (m_cancel)
+        if (m.canceled())
             throw tactic_exception(TACTIC_CANCELED_MSG);
         if (memory::get_allocation_size() > m_max_memory)
             throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
@@ -731,7 +719,6 @@ struct sat2goal::imp {
             assert_clauses(s.begin_learned(), s.end_learned(), r);
     }
 
-    void set_cancel(bool f) { m_cancel = f; }
 };
 
 sat2goal::sat2goal():m_imp(0) {
@@ -765,10 +752,3 @@ void sat2goal::operator()(sat::solver const & t, atom2bool_var const & m, params
     proc(t, m, g, mc);
 }
 
-void sat2goal::set_cancel(bool f) {
-    #pragma omp critical (sat2goal)
-    {
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
-}

src/sat/tactic/goal2sat.h

@@ -59,7 +59,6 @@ public:
     */
     void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false);
 
-    void set_cancel(bool f);
 
 };
 
@@ -83,7 +82,6 @@ public:
     */
     void operator()(sat::solver const & t, atom2bool_var const & m, params_ref const & p, goal & s, model_converter_ref & mc);
     
-    void set_cancel(bool f);
 };
 
 #endif

src/sat/tactic/sat_tactic.cpp

@@ -123,11 +123,6 @@ class sat_tactic : public tactic {
             result.push_back(g.get());
         }
         
-        void set_cancel(bool f) {
-            m_goal2sat.set_cancel(f);
-            m_sat2goal.set_cancel(f);
-            m_solver.set_cancel(f);
-        }
 
         void dep2assumptions(obj_map<expr, sat::literal>& dep2asm, 
                              sat::literal_vector& assumptions) {
@@ -223,13 +218,6 @@ public:
     }
 
 protected:
-    virtual void set_cancel(bool f) {
-        #pragma omp critical (sat_tactic)
-        {
-            if (m_imp)
-                m_imp->set_cancel(f);
-        }
-    }
 
 };
 

src/smt/asserted_formulas.cpp

@@ -54,8 +54,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
     m_macro_manager(m, m_simplifier),
     m_bit2int(m),
     m_bv_sharing(m),
-    m_inconsistent(false),
+    m_inconsistent(false){
-    m_cancel_flag(false) {
 
     m_bsimp = 0;
     m_bvsimp = 0;
@@ -223,9 +222,6 @@ void asserted_formulas::reset() {
     m_inconsistent = false;
 }
 
-void asserted_formulas::set_cancel_flag(bool f) {
-    m_cancel_flag = f; 
-}
 
 #ifdef Z3DEBUG
 bool asserted_formulas::check_well_sorted() const {

src/smt/asserted_formulas.h

@@ -62,7 +62,6 @@ class asserted_formulas {
         bool                    m_inconsistent_old;
     };
     svector<scope>              m_scopes;
-    volatile bool               m_cancel_flag;
 
     void setup_simplifier_plugins(simplifier & s, basic_simplifier_plugin * & bsimp, arith_simplifier_plugin * & asimp, bv_simplifier_plugin * & bvsimp);
     void reduce_asserted_formulas();
@@ -97,7 +96,7 @@ class asserted_formulas {
     unsigned get_total_size() const;
     bool has_bv() const;
     void max_bv_sharing();
-    bool canceled() { return m_cancel_flag; }
+    bool canceled() { return m_manager.canceled(); }
 
 public:
     asserted_formulas(ast_manager & m, smt_params & p);

src/smt/expr_context_simplifier.h

@@ -77,7 +77,6 @@ public:
     
     void collect_statistics(statistics & st) const { m_solver.collect_statistics(st); }
     void reset_statistics() { m_solver.reset_statistics(); }
-    void set_cancel(bool f) { m_solver.set_cancel(f); }
 };
 
 #endif /* EXPR_CONTEXT_SIMPLIFIER_H_ */

src/smt/smt_context.cpp

@@ -45,7 +45,6 @@ namespace smt {
         m_fparams(p),
         m_params(_p),
         m_setup(*this, p),
-        m_cancel_flag(false),
         m_asserted_formulas(m, p),
         m_qmanager(alloc(quantifier_manager, *this, p, _p)),
         m_model_generator(alloc(model_generator, m)),
@@ -3069,11 +3068,6 @@ namespace smt {
         if (m_manager.has_trace_stream())
             m_manager.trace_stream() << "[begin-check] " << m_scope_lvl << "\n";
 
-        if (reset_cancel) {
-            m_cancel_flag = false;
-            m_asserted_formulas.set_cancel_flag(false);
-        }
-
         if (memory::above_high_watermark()) {
             m_last_search_failure = MEMOUT;
             return false;
@@ -4154,11 +4148,6 @@ namespace smt {
         return m_last_search_failure; 
     }
 
-    void context::set_cancel_flag(bool f) {
-        m_cancel_flag = f;
-        m_asserted_formulas.set_cancel_flag(f);
-    }
-
 };
 
 #ifdef Z3DEBUG

src/smt/smt_context.h

@@ -79,7 +79,6 @@ namespace smt {
         smt_params &                m_fparams;
         params_ref                  m_params;
         setup                       m_setup;
-        volatile bool               m_cancel_flag;
         timer                       m_timer;
         asserted_formulas           m_asserted_formulas;
         scoped_ptr<quantifier_manager>   m_qmanager;
@@ -233,9 +232,8 @@ namespace smt {
             return m_params;
         }
 
-        virtual void set_cancel_flag(bool f = true);
 
-        bool get_cancel_flag() { return m_cancel_flag || !m_manager.limit().inc(); }
+        bool get_cancel_flag() { return !m_manager.limit().inc(); }
 
         region & get_region() {
             return m_region;

src/smt/smt_kernel.cpp

@@ -169,10 +169,6 @@ namespace smt {
         void display_istatistics(std::ostream & out) const {
             m_kernel.display_istatistics(out);
         }
-
-        void set_cancel(bool f) {
-            m_kernel.set_cancel_flag(f);
-        }
         
         bool canceled() {
             return m_kernel.get_cancel_flag();
@@ -328,14 +324,6 @@ namespace smt {
         m_imp->display_istatistics(out);
     }
 
-    void kernel::set_cancel(bool f) {
-        #pragma omp critical (smt_kernel)
-        {
-            if (m_imp)
-                m_imp->set_cancel(f);
-        }
-    }
-
     bool kernel::canceled() const {
         return m_imp->canceled();
     }

src/smt/smt_kernel.h

@@ -204,18 +204,7 @@ namespace smt {
            \brief Display statistics in low level format.
         */
         void display_istatistics(std::ostream & out) const;
-        
+                
-        /**
-           \brief Interrupt the kernel. 
-        */
-        void set_cancel(bool f = true);
-        void cancel() { set_cancel(true); }
-
-        /**
-           \brief Reset interruption.
-        */
-        void reset_cancel() { set_cancel(false); }
-        
         /**
            \brief Return true if the kernel was interrupted.
         */

src/smt/smt_solver.cpp

@@ -101,9 +101,8 @@ namespace smt {
             r.append(tmp.size(), tmp.c_ptr());
         }
 
-        virtual void set_cancel(bool f) {
+        virtual ast_manager& get_manager() { return m_context.m(); }
-            m_context.set_cancel(f);
+
-        }
 
         virtual void set_progress_callback(progress_callback * callback) {
             m_callback = callback;

src/smt/tactic/ctx_solver_simplify_tactic.cpp

@@ -35,12 +35,10 @@ class ctx_solver_simplify_tactic : public tactic {
     func_decl_ref         m_fn;
     obj_map<sort, func_decl*> m_fns;
     unsigned              m_num_steps;
-    volatile bool         m_cancel;
 public:
     ctx_solver_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()):
         m(m), m_params(p), m_solver(m, m_front_p),  
-        m_arith(m), m_mk_app(m), m_fn(m), m_num_steps(0), 
+        m_arith(m), m_mk_app(m), m_fn(m), m_num_steps(0) {
-        m_cancel(false) {
         sort* i_sort = m_arith.mk_int();
         m_fn = m.mk_func_decl(symbol(0xbeef101), i_sort, m.mk_bool_sort());
     }
@@ -86,15 +84,10 @@ public:
     virtual void cleanup() {
         reset_statistics();
         m_solver.reset();
-        m_cancel = false;
     }
 
 protected:
 
-    virtual void set_cancel(bool f) {
-        m_solver.set_cancel(f);
-        m_cancel = false;
-    }
 
     void reduce(goal& g) {
         SASSERT(g.is_well_sorted());
@@ -177,7 +170,7 @@ protected:
         names.push_back(n);
         m_solver.push();
 
-        while (!todo.empty() && !m_cancel) {            
+        while (!todo.empty() && !m.canceled()) {            
             expr_ref res(m);
             args.reset();
             expr* e    = todo.back().m_expr;
@@ -249,7 +242,7 @@ protected:
             names.pop_back();
             m_solver.pop(1);
         }
-        if (!m_cancel) {
+        if (!m.canceled()) {
             VERIFY(cache.find(fml, path_r));
             result = path_r.m_expr;
         }

src/smt/tactic/smt_tactic.cpp

@@ -132,10 +132,6 @@ public:
         smt_params_helper::collect_param_descrs(r);
     }
     
-    virtual void set_cancel(bool f) {
-        if (m_ctx)
-            m_ctx->set_cancel(f);
-    }
 
     virtual void collect_statistics(statistics & st) const {
         if (m_ctx)

src/smt/tactic/unit_subsumption_tactic.cpp

@@ -22,7 +22,6 @@ struct unit_subsumption_tactic : public tactic {
     ast_manager&    m;
     params_ref      m_params;
     smt_params      m_fparams;
-    volatile bool   m_cancel;
     smt::context    m_context;
     expr_ref_vector m_clauses;
     unsigned        m_clause_count;
@@ -34,19 +33,11 @@ struct unit_subsumption_tactic : public tactic {
         params_ref const& p):
         m(m), 
         m_params(p), 
-        m_cancel(false), 
         m_context(m, m_fparams, p),
         m_clauses(m) {
     }
-           
-    void set_cancel(bool f) {
-        m_cancel = f;
-        m_context.set_cancel_flag(f);
-    }
 
-    virtual void cleanup() {
+    void cleanup() {}
-        set_cancel(false);
-    }
 
     virtual void operator()(/* in */  goal_ref const & in, 
                             /* out */ goal_ref_buffer & result, 
@@ -66,7 +57,7 @@ struct unit_subsumption_tactic : public tactic {
     }
     
     void checkpoint() {
-        if (m_cancel) {
+        if (m.canceled()) {
             throw tactic_exception(TACTIC_CANCELED_MSG);
         }
     }

src/solver/check_sat_result.h

@@ -52,6 +52,7 @@ public:
     virtual proof * get_proof() = 0;
     virtual std::string reason_unknown() const = 0;
     virtual void get_labels(svector<symbol> & r) = 0;
+    virtual ast_manager& get_manager() = 0;
 };
 
 /**
@@ -63,9 +64,11 @@ struct simple_check_sat_result : public check_sat_result {
     expr_ref_vector m_core;
     proof_ref       m_proof;
     std::string     m_unknown;
+    
 
     simple_check_sat_result(ast_manager & m);
     virtual ~simple_check_sat_result();
+    virtual ast_manager& get_manager() { return m_proof.get_manager(); }
     virtual void collect_statistics(statistics & st) const;
     virtual void get_unsat_core(ptr_vector<expr> & r);
     virtual void get_model(model_ref & m);

src/solver/combined_solver.cpp

@@ -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->cancel();
+            m_solver->get_manager().cancel();
             m_canceled = true;
         }
     };
@@ -96,6 +96,8 @@ private:
         m_inc_unknown_behavior = static_cast<inc_unknown_behavior>(p.solver2_unknown());
     }
 
+    virtual ast_manager& get_manager() { return m_solver1->get_manager(); }
+
     bool has_quantifiers() const {
         unsigned sz = get_num_assertions();
         for (unsigned i = 0; i < sz; i++) {
@@ -220,25 +222,18 @@ public:
                     m_use_solver1_results = false;
                     return r;
                 }
+                if (eh.m_canceled) {
+                    m_solver1->get_manager().limit().reset_cancel();
+                }
             }
-            IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"solver 2 failed, trying solver1\")\n";);                        
+            IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"solver 2 failed, trying solver1\")\n";);
+
         }
         
         IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 1\")\n";);
         m_use_solver1_results = true;
         return m_solver1->check_sat(0, 0);
     }
-
-    virtual void set_cancel(bool f) {
-        if (f) {
-            m_solver1->cancel();
-            m_solver2->cancel();
-        }
-        else {
-            m_solver1->reset_cancel();
-            m_solver2->reset_cancel();
-        }
-    }
     
     virtual void set_progress_callback(progress_callback * callback) {
         m_solver1->set_progress_callback(callback);

src/solver/solver.h

@@ -108,11 +108,11 @@ public:
     /**
        \brief Interrupt this solver.
     */
-    void cancel() { set_cancel(true); }
+    //void cancel() { set_cancel(true); }
     /**
        \brief Reset the interruption.
     */
-    void reset_cancel() { set_cancel(false); }
+    //void reset_cancel() { set_cancel(false); }
 
     /**
        \brief Set a progress callback procedure that is invoked by this solver during check_sat.
@@ -158,7 +158,7 @@ public:
     };
 
 protected:
-    virtual void set_cancel(bool f) = 0;
+    //virtual void set_cancel(bool f) = 0;
 };
 
 #endif

src/solver/tactic2solver.cpp

@@ -59,7 +59,6 @@ public:
     virtual void pop_core(unsigned n);
     virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions);
 
-    virtual void set_cancel(bool f);
 
     virtual void collect_statistics(statistics & st) const;
     virtual void get_unsat_core(ptr_vector<expr> & r);
@@ -74,8 +73,11 @@ public:
     virtual expr * get_assertion(unsigned idx) const;
 
     virtual void display(std::ostream & out) const;
+    virtual ast_manager& get_manager(); 
 };
 
+ast_manager& tactic2solver::get_manager() { return m_assertions.get_manager(); }
+
 tactic2solver::tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic):
     solver_na2as(m),
     m_assertions(m) {
@@ -177,14 +179,6 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
     return m_result->status();
 }
 
-void tactic2solver::set_cancel(bool f) {
-    if (m_tactic.get()) {
-        if (f) 
-            m_tactic->cancel();
-        else
-            m_tactic->reset_cancel();
-    }
-}
 
 solver* tactic2solver::translate(ast_manager& m, params_ref const& p) {
     tactic* t = m_tactic->translate(m);

src/solver/tactic2solver.h

@@ -37,6 +37,7 @@ solver * mk_tactic2solver(ast_manager & m,
                           bool produce_unsat_cores = false, 
                           symbol const & logic = symbol::null);
 
+
 solver_factory * mk_tactic2solver_factory(tactic * t);
 solver_factory * mk_tactic_factory2solver_factory(tactic_factory * f);
 

src/tactic/aig/aig.cpp

@@ -119,7 +119,6 @@ struct aig_manager::imp {
     aig_lit                  m_false;
     bool                     m_default_gate_encoding;
     unsigned long long       m_max_memory;
-    volatile bool            m_cancel;
 
     void dec_ref_core(aig * n) {
         SASSERT(n->m_ref_count > 0);
@@ -131,7 +130,7 @@ struct aig_manager::imp {
     void checkpoint() {
         if (memory::get_allocation_size() > m_max_memory)
             throw aig_exception(TACTIC_MAX_MEMORY_MSG);
-        if (m_cancel)
+        if (m().canceled())
             throw aig_exception(TACTIC_CANCELED_MSG);
         cooperate("aig");
     }
@@ -1309,8 +1308,7 @@ public:
         m_num_aigs(0),
         m_var2exprs(m),
         m_allocator("aig"),
-        m_true(mk_var(m.mk_true())),
+        m_true(mk_var(m.mk_true())) {
-        m_cancel(false) {
         SASSERT(is_true(m_true));
         m_false = m_true;
         m_false.invert();
@@ -1328,7 +1326,6 @@ public:
 
     ast_manager & m() const { return m_var2exprs.get_manager(); }
 
-    void set_cancel(bool f) { m_cancel = f; }
 
     void inc_ref(aig * n) { n->m_ref_count++; }
     void inc_ref(aig_lit const & r) { inc_ref(r.ptr()); }
@@ -1754,8 +1751,5 @@ unsigned aig_manager::get_num_aigs() const {
     return m_imp->get_num_aigs();
 }
 
-void aig_manager::set_cancel(bool f) {
-    m_imp->set_cancel(f);
-}
 
 

src/tactic/aig/aig.h

@@ -73,7 +73,6 @@ public:
     void display(std::ostream & out, aig_ref const & r) const;
     void display_smt2(std::ostream & out, aig_ref const & r) const;
     unsigned get_num_aigs() const;
-    void set_cancel(bool f);
 };
 
 #endif

src/tactic/aig/aig_tactic.cpp

@@ -111,14 +111,6 @@ public:
 
     virtual void cleanup() {}
 
-protected:
-    virtual void set_cancel(bool f) {
-        #pragma omp critical (aig_tactic)
-        {
-            if (m_aig_manager)
-                m_aig_manager->set_cancel(f);
-        }
-    }
 };
 
 tactic * mk_aig_tactic(params_ref const & p) {

src/tactic/arith/add_bounds_tactic.cpp

@@ -62,7 +62,6 @@ class add_bounds_tactic : public tactic {
         ast_manager & m;
         rational      m_lower;
         rational      m_upper;
-        volatile bool m_cancel;
         
         imp(ast_manager & _m, params_ref const & p):
             m(_m) {
@@ -74,9 +73,6 @@ class add_bounds_tactic : public tactic {
             m_upper  = p.get_rat("add_bound_upper", rational(2));
         }
         
-        void set_cancel(bool f) {
-            m_cancel = f;
-        }
         
         struct add_bound_proc {
             arith_util       m_util;
@@ -180,11 +176,6 @@ public:
         dealloc(d);
     }
 
-protected:
-    virtual void set_cancel(bool f) {
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
 };
 
 tactic * mk_add_bounds_tactic(ast_manager & m, params_ref const & p) {

src/tactic/arith/arith_bounds_tactic.cpp

@@ -13,24 +13,15 @@ struct arith_bounds_tactic : public tactic {
 
     ast_manager& m;
     arith_util   a;
-    volatile bool m_cancel;
 
     arith_bounds_tactic(ast_manager& m):
         m(m),
-        a(m),
+        a(m)
-        m_cancel(false)
     {
     }        
 
     ast_manager& get_manager() { return m; }
 
-    void set_cancel(bool f) {
-        m_cancel = f;
-    }
-
-    virtual void cleanup() {
-        m_cancel = false;
-    }
 
     virtual void operator()(/* in */  goal_ref const & in, 
                             /* out */ goal_ref_buffer & result, 
@@ -45,7 +36,7 @@ struct arith_bounds_tactic : public tactic {
     }
     
     void checkpoint() {
-        if (m_cancel) {
+        if (m.canceled()) {
             throw tactic_exception(TACTIC_CANCELED_MSG);
         }
     }
@@ -155,6 +146,7 @@ struct arith_bounds_tactic : public tactic {
         TRACE("arith_subsumption", s->display(tout); );
     }
 
+    virtual void cleanup() {}
 
 };
 

src/tactic/arith/card2bv_tactic.cpp

@@ -462,10 +462,6 @@ public:
     virtual void collect_param_descrs(param_descrs & r) {  
     }
 
-    void set_cancel(bool f) {
-        m_rw1.set_cancel(f);
-        m_rw2.set_cancel(f);
-    }
     
     virtual void operator()(goal_ref const & g, 
                             goal_ref_buffer & result, 

src/tactic/arith/degree_shift_tactic.cpp

@@ -40,7 +40,6 @@ class degree_shift_tactic : public tactic {
         rational                 m_one;
         bool                     m_produce_models;
         bool                     m_produce_proofs;
-        volatile bool            m_cancel;
 
         expr * mk_power(expr * t, rational const & k) {
             if (k.is_one())
@@ -96,15 +95,11 @@ class degree_shift_tactic : public tactic {
             m_pinned(_m),
             m_one(1),
             m_rw(0) {
-            m_cancel = false;
         }
 
-        void set_cancel(bool f) {
-            m_cancel = f;
-        }
 
         void checkpoint() {
-            if (m_cancel)
+            if (m.canceled())
                 throw tactic_exception(TACTIC_CANCELED_MSG);
             cooperate("degree_shift");
         }
@@ -326,12 +321,7 @@ public:
         }
         dealloc(d);
     }
-    
+
-protected:
-    virtual void set_cancel(bool f) {
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
 };
 
 tactic * mk_degree_shift_tactic(ast_manager & m, params_ref const & p) {

src/tactic/arith/diff_neq_tactic.cpp

@@ -45,7 +45,6 @@ class diff_neq_tactic : public tactic {
         vector<diseqs>      m_var_diseqs;
         typedef svector<int> decision_stack;
         decision_stack       m_stack;
-        volatile bool        m_cancel;
         
         bool                m_produce_models;
         rational            m_max_k;
@@ -58,7 +57,6 @@ class diff_neq_tactic : public tactic {
             u(m),
             m_var2expr(m) {
             updt_params(p);
-            m_cancel = false;
         }
         
         void updt_params(params_ref const & p) {
@@ -67,11 +65,7 @@ class diff_neq_tactic : public tactic {
             if (m_max_k >= rational(INT_MAX/2)) 
                 m_max_k = rational(INT_MAX/2);
         }
-        
+                
-        void set_cancel(bool f) {
-            m_cancel = f;
-        }
-        
         void throw_not_supported() {
             throw tactic_exception("goal is not diff neq");
         }
@@ -294,7 +288,7 @@ class diff_neq_tactic : public tactic {
             init_forbidden();
             unsigned nvars = num_vars();
             while (m_stack.size() < nvars) {
-                if (m_cancel)
+                if (m.canceled())
                     throw tactic_exception(TACTIC_CANCELED_MSG);
                 TRACE("diff_neq_tactic", display_model(tout););
                 var x = m_stack.size();
@@ -407,11 +401,6 @@ public:
         dealloc(d);
     }
 
-protected:
-    virtual void set_cancel(bool f) {
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
 };
 
 tactic * mk_diff_neq_tactic(ast_manager & m, params_ref const & p) {

src/tactic/arith/elim01_tactic.cpp

@@ -136,10 +136,7 @@ public:
 
     virtual ~elim01_tactic() {
     }
-        
+                
-    void set_cancel(bool f) {
-    }
-        
     virtual void updt_params(params_ref const & p) {
         m_max_hi = rational(p.get_uint("max_coefficient", m_max_hi_default));
         m_params = p;

src/tactic/arith/eq2bv_tactic.cpp

@@ -139,9 +139,6 @@ public:
     virtual ~eq2bv_tactic() {
     }
         
-    void set_cancel(bool f) {
-        m_rw.set_cancel(f);
-    }
         
     void updt_params(params_ref const & p) {
     }

src/tactic/arith/factor_tactic.cpp

@@ -34,7 +34,7 @@ class factor_tactic : public tactic {
         rw_cfg(ast_manager & _m, params_ref const & p):
             m(_m),
             m_util(_m),
-            m_pm(m_qm),
+            m_pm(m.limit(), m_qm),
             m_expr2poly(m, m_pm) {
             updt_params(p);
         }
@@ -251,10 +251,6 @@ class factor_tactic : public tactic {
             m_rw(m, p) {
         }
 
-        void set_cancel(bool f) {
-            m_rw.set_cancel(f);
-            m_rw.cfg().m_pm.set_cancel(f);
-        }
 
         void updt_params(params_ref const & p) {
             m_rw.cfg().updt_params(p);
@@ -341,10 +337,7 @@ public:
         dealloc(d);
     }
 
-    virtual void set_cancel(bool f) {
+
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
 };
 
 tactic * mk_factor_tactic(ast_manager & m, params_ref const & p) {

src/tactic/arith/fix_dl_var_tactic.cpp

@@ -247,11 +247,7 @@ class fix_dl_var_tactic : public tactic {
         void updt_params(params_ref const & p) {
             m_rw.updt_params(p);
         }
-        
+                
-        void set_cancel(bool f) {
-            m_rw.set_cancel(f);
-        }
-        
         void operator()(goal_ref const & g, 
                         goal_ref_buffer & result, 
                         model_converter_ref & mc, 
@@ -345,11 +341,6 @@ public:
         }
         dealloc(d);
     }
-
-    virtual void set_cancel(bool f) {
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
 };
 
 tactic * mk_fix_dl_var_tactic(ast_manager & m, params_ref const & p) {

src/tactic/arith/fm_tactic.cpp

@@ -44,7 +44,6 @@ class fm_tactic : public tactic {
         ast_manager &         m;
         ptr_vector<func_decl> m_xs;
         vector<clauses>       m_clauses;
-        volatile bool         m_cancel;
 
         enum r_kind {
             NONE,
@@ -182,7 +181,6 @@ class fm_tactic : public tactic {
 
         virtual void operator()(model_ref & md, unsigned goal_idx) {
             TRACE("fm_mc", model_v2_pp(tout, *md); display(tout););
-            m_cancel = false;
             model_evaluator ev(*(md.get()));
             ev.set_model_completion(true);
             arith_util u(m);
@@ -199,7 +197,7 @@ class fm_tactic : public tactic {
                 clauses::iterator it  = m_clauses[i].begin();
                 clauses::iterator end = m_clauses[i].end();
                 for (; it != end; ++it) {
-                    if (m_cancel) throw tactic_exception(TACTIC_CANCELED_MSG);
+                    if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG);
                     switch (process(x, *it, u, ev, val)) {
                     case NONE: 
                         TRACE("fm_mc", tout << "no bound for:\n" << mk_ismt2_pp(*it, m) << "\n";);
@@ -244,9 +242,6 @@ class fm_tactic : public tactic {
             TRACE("fm_mc", model_v2_pp(tout, *md););
         }
 
-        virtual void cancel() {
-            m_cancel = true;
-        }
 
         virtual void display(std::ostream & out) {
             out << "(fm-model-converter";
@@ -394,7 +389,6 @@ class fm_tactic : public tactic {
         obj_hashtable<func_decl> m_forbidden_set; // variables that cannot be eliminated because occur in non OCC ineq part
         goal_ref                 m_new_goal;
         ref<fm_model_converter>  m_mc;
-        volatile bool            m_cancel;
         id_gen                   m_id_gen;
         bool                     m_produce_models;
         bool                     m_fm_real_only;
@@ -784,7 +778,6 @@ class fm_tactic : public tactic {
             m_var2expr(m),
             m_inconsistent_core(m) {
             updt_params(p);
-            m_cancel = false;
         }
         
         ~imp() {
@@ -801,9 +794,6 @@ class fm_tactic : public tactic {
             m_fm_occ         = p.get_bool("fm_occ", false);
         }
         
-        void set_cancel(bool f) {
-            m_cancel = f;
-        }
         
         struct forbidden_proc {
             imp & m_owner;
@@ -1552,7 +1542,7 @@ class fm_tactic : public tactic {
         
         void checkpoint() {
             cooperate("fm");
-            if (m_cancel)
+            if (m.canceled())
                 throw tactic_exception(TACTIC_CANCELED_MSG);
             if (memory::get_allocation_size() > m_max_memory)
                 throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
@@ -1676,10 +1666,6 @@ public:
         r.insert("fm_extra", CPK_UINT, "(default: 0) max. increase on the number of inequalities for each FM variable elimination step.");
     }
 
-    virtual void set_cancel(bool f) {
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
 
     virtual void cleanup() {
         imp * d = alloc(imp, m_imp->m, m_params);