moving to resource managed cancellation

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

src/cmd_context/cmd_context.cpp

@@ -1610,6 +1610,7 @@ void cmd_context::validate_model() {
     model_evaluator evaluator(*(md.get()), p);
     contains_array_op_proc contains_array(m());
     {
+        scoped_rlimit _rlimit(m().limit(), 0);
         cancel_eh<reslimit> eh(m().limit());
         expr_ref r(m());
         scoped_ctrl_c ctrlc(eh);

src/cmd_context/context_params.cpp

@@ -35,7 +35,7 @@ context_params::context_params() {
     m_smtlib2_compliant = false;
     m_well_sorted_check = false;
     m_timeout = UINT_MAX;
-    m_rlimit  = UINT_MAX;
+    m_rlimit  = 0;
     updt_params();
 }
 
@@ -153,7 +153,7 @@ void context_params::updt_params(params_ref const & p) {
 
 void context_params::collect_param_descrs(param_descrs & d) {
     d.insert("timeout", CPK_UINT, "default timeout (in milliseconds) used for solvers", "4294967295");
-    d.insert("rlimit", CPK_UINT, "default resource limit used for solvers", "4294967295");
+    d.insert("rlimit", CPK_UINT, "default resource limit used for solvers. Unrestricted when set to 0.", "0");
     d.insert("well_sorted_check", CPK_BOOL, "type checker", "false");
     d.insert("type_check", CPK_BOOL, "type checker (alias for well_sorted_check)", "true");
     d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true");

src/cmd_context/eval_cmd.cpp

@@ -63,11 +63,13 @@ public:
         last_result->get_model(md);
         expr_ref r(ctx.m());
         unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
+        unsigned rlimit  = m_params.get_uint("rlimit", 0);
         model_evaluator ev(*(md.get()), m_params);
         cancel_eh<reslimit> eh(ctx.m().limit());
         { 
             scoped_ctrl_c ctrlc(eh);
             scoped_timer timer(timeout, &eh);
+            scoped_rlimit _rlimit(ctx.m().limit(), rlimit);
             cmd_context::scoped_watch sw(ctx);
             try {
                 ev(m_target, r);

src/cmd_context/simplify_cmd.cpp

@@ -73,9 +73,11 @@ public:
         unsigned cache_sz;
         unsigned num_steps = 0;
         unsigned timeout   = m_params.get_uint("timeout", UINT_MAX);
+        unsigned rlimit    = m_params.get_uint("rlimit", UINT_MAX);
         bool failed = false;
         cancel_eh<reslimit> eh(ctx.m().limit());
         { 
+            scoped_rlimit _rlimit(ctx.m().limit(), rlimit);
             scoped_ctrl_c ctrlc(eh);
             scoped_timer timer(timeout, &eh);
             cmd_context::scoped_watch sw(ctx);

src/cmd_context/tactic_cmds.cpp

@@ -188,6 +188,7 @@ public:
         tref->set_logic(ctx.get_logic());
         ast_manager & m = ctx.m();
         unsigned timeout   = p.get_uint("timeout", UINT_MAX);
+        unsigned rlimit  =   p.get_uint("rlimit", 0);
         goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores());
         assert_exprs_from(ctx, *g);
         TRACE("check_sat_using", g->display(tout););
@@ -201,6 +202,7 @@ public:
             tactic & t = *tref;
             cancel_eh<reslimit>  eh(m.limit());
             {
+                scoped_rlimit _rlimit(m.limit(), rlimit);
                 scoped_ctrl_c ctrlc(eh);
                 scoped_timer timer(timeout, &eh);
                 cmd_context::scoped_watch sw(ctx);
@@ -302,6 +304,7 @@ public:
             assert_exprs_from(ctx, *g);
 
             unsigned timeout   = p.get_uint("timeout", UINT_MAX);
+            unsigned rlimit  =   p.get_uint("rlimit", 0);
 
             goal_ref_buffer     result_goals;
             model_converter_ref mc;
@@ -312,6 +315,7 @@ public:
             bool failed = false;
             cancel_eh<reslimit>  eh(m.limit());
             {
+                scoped_rlimit _rlimit(m.limit(), rlimit);
                 scoped_ctrl_c ctrlc(eh);
                 scoped_timer timer(timeout, &eh);
                 cmd_context::scoped_watch sw(ctx);

src/tactic/aig/aig_tactic.cpp

@@ -32,19 +32,11 @@ class aig_tactic : public tactic {
 
         mk_aig_manager(aig_tactic & o, ast_manager & m):m_owner(o) {
             aig_manager * mng = alloc(aig_manager, m, o.m_max_memory, o.m_aig_gate_encoding);
-            #pragma omp critical (aig_tactic)
-            {
             m_owner.m_aig_manager = mng;            
         }
-        }
         
         ~mk_aig_manager() {
-            aig_manager * mng = m_owner.m_aig_manager;
+            dealloc(m_owner.m_aig_manager);
-            #pragma omp critical (aig_tactic)
-            {
-                m_owner.m_aig_manager = 0;
-            }
-            dealloc(mng);
         }
     };
 

src/tactic/arith/add_bounds_tactic.cpp

@@ -169,10 +169,7 @@ public:
     
     virtual void cleanup() {
         imp * d = alloc(imp, m_imp->m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
         std::swap(d, m_imp);
-        }
         dealloc(d);
     }
 

src/tactic/arith/degree_shift_tactic.cpp

@@ -315,10 +315,7 @@ public:
     
     virtual void cleanup() {
         imp * d = alloc(imp, m_imp->m);
-        #pragma omp critical (tactic_cancel)
-        {
         std::swap(d, m_imp);        
-        }
         dealloc(d);
     }
 

src/tactic/tactical.cpp

@@ -40,15 +40,8 @@ public:
     }
     
     virtual ~binary_tactical() {
-        tactic * t1 = m_t1;
+        m_t1->dec_ref();
-        tactic * t2 = m_t2;
+        m_t2->dec_ref();
-        #pragma omp critical (tactic_cancel)
-        {
-            m_t1 = 0;
-            m_t2 = 0;
-        }
-        t1->dec_ref();
-        t2->dec_ref();
     }
     
     virtual void updt_params(params_ref const & p) {
@@ -291,17 +284,9 @@ public:
     }
 
     virtual ~nary_tactical() {
-        ptr_buffer<tactic> old_ts;
         unsigned sz = m_ts.size();
-        old_ts.append(sz, m_ts.c_ptr());
-        #pragma omp critical (tactic_cancel)
-        {
         for (unsigned i = 0; i < sz; i++) {
-                m_ts[i] = 0;
+            m_ts[i]->dec_ref();
-            }
-        }
-        for (unsigned i = 0; i < sz; i++) {
-            old_ts[i]->dec_ref();
         }
     }
 
@@ -906,12 +891,7 @@ public:
     }    
 
     virtual ~unary_tactical() { 
-        tactic * t = m_t;
+        m_t->dec_ref();
-        #pragma omp critical (tactic_cancel)
-        {
-            m_t = 0;
-        }
-        t->dec_ref();
     }
 
     virtual void operator()(goal_ref const & in, 

src/util/rlimit.cpp

@@ -45,6 +45,7 @@ void reslimit::push(unsigned delta_limit) {
     }
     m_limits.push_back(m_limit);
     m_limit = m_limit==0?new_limit:std::min(new_limit, m_limit);
+    m_cancel = false;
 }
 
 void reslimit::pop() {
@@ -53,4 +54,5 @@ void reslimit::pop() {
     }
     m_limit = m_limits.back();
     m_limits.pop_back();
+    m_cancel = false;
 }

src/util/statistics.cpp

@@ -227,6 +227,15 @@ double statistics::get_double_value(unsigned idx) const {
     return m_d_stats[idx - m_stats.size()].second;
 }
 
+static void get_uint64_stats(statistics& st, char const* name, unsigned long long value) {
+    if (value <= UINT_MAX) {
+        st.update(name, static_cast<unsigned>(value));
+    }
+    else {
+        st.update(name, static_cast<double>(value));
+    }
+}
+
 void get_memory_statistics(statistics& st) {
     unsigned long long max_mem = memory::get_max_used_memory();
     unsigned long long mem = memory::get_allocation_size();
@@ -234,9 +243,9 @@ void get_memory_statistics(statistics& st) {
     mem = (100*mem)/(1024*1024);
     st.update("max memory", static_cast<double>(max_mem)/100.0);    
     st.update("memory", static_cast<double>(mem)/100.0);
-    st.update("num allocs",  static_cast<double>(memory::get_allocation_count()));
+    get_uint64_stats(st, "num allocs",  memory::get_allocation_count());
 }
 
 void get_rlimit_statistics(reslimit& l, statistics& st) {
-    st.update("rlimit count",     static_cast<double>(l.count()));
+    get_uint64_stats(st, "rlimit count", l.count());
 }