cleanup deprecated critical sections, fix cancellation for par_or_else tactic

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

src/tactic/arith/diff_neq_tactic.cpp

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

src/tactic/arith/factor_tactic.cpp

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

src/tactic/arith/fix_dl_var_tactic.cpp

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

src/tactic/arith/fm_tactic.cpp

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

src/tactic/arith/lia2card_tactic.cpp

@@ -400,11 +400,8 @@ public:
     virtual void cleanup() {        
         expr_set* d = alloc(expr_set);
         ptr_vector<expr>* todo = alloc(ptr_vector<expr>);
-        #pragma omp critical (tactic_cancel)
-        {
-            std::swap(m_01s, d);
-            std::swap(m_todo, todo);
-        }
+        std::swap(m_01s, d);
+        std::swap(m_todo, todo);        
         dealloc(d);
         dealloc(todo);
     }

src/tactic/arith/lia2pb_tactic.cpp

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

src/tactic/arith/nla2bv_tactic.cpp

@@ -404,17 +404,11 @@ class nla2bv_tactic : public tactic {
         nla2bv_tactic & m_owner; 
         scoped_set_imp(nla2bv_tactic & o, imp & i):
             m_owner(o) {
-            #pragma omp critical (tactic_cancel)
-            {
-                m_owner.m_imp = &i;
-            }
+            m_owner.m_imp = &i;            
         }
 
         ~scoped_set_imp() {
-            #pragma omp critical (tactic_cancel)
-            {
-                m_owner.m_imp = 0;
-            }
+            m_owner.m_imp = 0;            
         }
     };
     

src/tactic/arith/normalize_bounds_tactic.cpp

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

src/tactic/arith/pb2bv_tactic.cpp

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

src/tactic/arith/propagate_ineqs_tactic.cpp

@@ -544,9 +544,6 @@ void propagate_ineqs_tactic::operator()(goal_ref const & g,
  
 void propagate_ineqs_tactic::cleanup() {
     imp * d = alloc(imp, m_imp->m, m_params);
-    #pragma omp critical (tactic_cancel)
-    {
-        std::swap(d, m_imp);
-    }
+    std::swap(d, m_imp);    
     dealloc(d);
 }

src/tactic/arith/recover_01_tactic.cpp

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

src/tactic/bv/bit_blaster_tactic.cpp

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

src/tactic/bv/bv1_blaster_tactic.cpp

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

src/tactic/bv/bv_size_reduction_tactic.cpp

@@ -400,10 +400,7 @@ void bv_size_reduction_tactic::operator()(goal_ref const & g,
  
 void bv_size_reduction_tactic::cleanup() {
     imp * d = alloc(imp, m_imp->m);
-    #pragma omp critical (tactic_cancel)
-    {
-        std::swap(d, m_imp);
-    }
+    std::swap(d, m_imp);    
     dealloc(d);
 }
 

src/tactic/bv/bvarray2uf_tactic.cpp

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

src/tactic/bv/elim_small_bv_tactic.cpp

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

src/tactic/bv/max_bv_sharing_tactic.cpp

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

src/tactic/core/blast_term_ite_tactic.cpp

@@ -183,16 +183,11 @@ public:
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
         imp * d = m_imp;
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = 0;
-        }
+        m_imp = 0;
+        
         dealloc(d);
         d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
+        m_imp = d;        
     }
 
     static void blast_term_ite(expr_ref& fml) {

src/tactic/core/cofactor_elim_term_ite.cpp

@@ -697,10 +697,7 @@ void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) {
 void cofactor_elim_term_ite::cleanup() {
     ast_manager & m = m_imp->m;    
     imp * d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel)
-    {
-        std::swap(d, m_imp);
-    }
+    std::swap(d, m_imp);    
     dealloc(d);
 }
 

src/tactic/core/ctx_simplify_tactic.cpp

@@ -540,10 +540,7 @@ void ctx_simplify_tactic::operator()(goal_ref const & in,
 void ctx_simplify_tactic::cleanup() {
     ast_manager & m   = m_imp->m;
     imp * d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel)
-    {
-        std::swap(d, m_imp);
-    }
+    std::swap(d, m_imp);    
     dealloc(d);
 }
 

src/tactic/core/der_tactic.cpp

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

src/tactic/core/distribute_forall_tactic.cpp

@@ -108,10 +108,7 @@ public:
         ast_manager & m = g->m();
         bool produce_proofs = g->proofs_enabled();
         rw r(m, produce_proofs);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_rw = &r;
-        }
+        m_rw = &r;        
         mc = 0; pc = 0; core = 0; result.reset();
         tactic_report report("distribute-forall", *g);
         
@@ -134,10 +131,7 @@ public:
         result.push_back(g.get());
         TRACE("distribute-forall", g->display(tout););
         SASSERT(g->is_well_sorted());
-        #pragma omp critical (tactic_cancel)
-        {
-            m_rw = 0;
-        }
+        m_rw = 0;        
     }
 
     virtual void cleanup() {}

src/tactic/core/elim_term_ite_tactic.cpp

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

src/tactic/core/elim_uncnstr_tactic.cpp

@@ -895,10 +895,7 @@ class elim_uncnstr_tactic : public tactic {
         }
         
         void init_rw(bool produce_proofs) {
-            #pragma omp critical (tactic_cancel)
-            {
-                m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps);
-            }
+            m_rw = alloc(rw, m(), produce_proofs, m_vars, m_mc.get(), m_max_memory, m_max_steps);            
         }
 
         virtual void operator()(goal_ref const & g, 
@@ -968,10 +965,7 @@ class elim_uncnstr_tactic : public tactic {
                         }
                     }
                     m_mc = 0;
-                    #pragma omp critical (tactic_cancel)
-                    {
-                        m_rw  = 0;
-                    }
+                    m_rw  = 0;                    
                     TRACE("elim_uncnstr", if (mc) mc->display(tout););
                     result.push_back(g.get());
                     g->inc_depth();
@@ -1034,10 +1028,7 @@ public:
         unsigned num_elim_apps = get_num_elim_apps();
         ast_manager & m = m_imp->m_manager;        
         imp * d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            std::swap(d, m_imp);
-        }
+        std::swap(d, m_imp);        
         dealloc(d);
         m_imp->m_num_elim_apps = num_elim_apps;
     }

src/tactic/core/nnf_tactic.cpp

@@ -29,17 +29,11 @@ class nnf_tactic : public tactic {
         
         set_nnf(nnf_tactic & owner, nnf & n):
             m_owner(owner) {
-            #pragma omp critical (nnf_tactic)
-            {
-                m_owner.m_nnf = &n;
-            }
+            m_owner.m_nnf = &n;            
         }
         
         ~set_nnf() {
-            #pragma omp critical (nnf_tactic)
-            {
-                m_owner.m_nnf = 0;
-            }
+            m_owner.m_nnf = 0;            
         }
     };
 public:

src/tactic/core/occf_tactic.cpp

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

src/tactic/core/propagate_values_tactic.cpp

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

src/tactic/core/reduce_args_tactic.cpp

@@ -532,10 +532,7 @@ void reduce_args_tactic::operator()(goal_ref const & g,
 void reduce_args_tactic::cleanup() {
     ast_manager & m   = m_imp->m();    
     imp * d = alloc(imp, m);
-    #pragma omp critical (tactic_cancel)
-    {
-        std::swap(d, m_imp);
-    }
+    std::swap(d, m_imp);    
     dealloc(d);
 }
 

src/tactic/core/simplify_tactic.cpp

@@ -112,10 +112,7 @@ void simplify_tactic::operator()(goal_ref const & in,
 void simplify_tactic::cleanup() {
     ast_manager & m = m_imp->m();
     imp * d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel)
-    {
-        std::swap(d, m_imp);
-    }
+    std::swap(d, m_imp);    
     dealloc(d);
 }
 

src/tactic/core/solve_eqs_tactic.cpp

@@ -751,10 +751,7 @@ public:
 
         imp * d = alloc(imp, m, m_params, r, owner);
         d->m_num_eliminated_vars = num_elim_vars;
-        #pragma omp critical (tactic_cancel)
-        {
-            std::swap(d, m_imp);
-        }
+        std::swap(d, m_imp);        
         dealloc(d);
     }
 

src/tactic/core/tseitin_cnf_tactic.cpp

@@ -896,10 +896,7 @@ public:
         ast_manager & m = m_imp->m;
         imp * d = alloc(imp, m, m_params);
         d->m_num_aux_vars = m_imp->m_num_aux_vars;
-        #pragma omp critical (tactic_cancel)
-        {
-            std::swap(d, m_imp);
-        }
+        std::swap(d, m_imp);        
         dealloc(d);
     }
 

src/tactic/fpa/fpa2bv_tactic.cpp

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

src/tactic/sls/sls_tactic.cpp

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

src/tactic/tactical.cpp

@@ -461,10 +461,21 @@ enum par_exception_kind {
 };
 
 class par_tactical : public or_else_tactical {
+
+    struct scoped_limits {
+        reslimit&  m_limit;
+        unsigned   m_sz;
+        scoped_limits(reslimit& lim): m_limit(lim), m_sz(0) {}
+        ~scoped_limits() { for (unsigned i = 0; i < m_sz; ++i) m_limit.pop_child(); }
+        void push_child(reslimit* lim) { m_limit.push_child(lim); ++m_sz; }
+    };
+
 public:
     par_tactical(unsigned num, tactic * const * ts):or_else_tactical(num, ts) {}
     virtual ~par_tactical() {}
 
+    
+
     virtual void operator()(goal_ref const & in, 
                             goal_ref_buffer & result, 
                             model_converter_ref & mc, 
@@ -485,6 +496,7 @@ public:
         ast_manager & m = in->m();
         
         scoped_ptr_vector<ast_manager> managers;
+        scoped_limits scl(m.limit());
         goal_ref_vector                in_copies;
         tactic_ref_vector              ts;
         unsigned sz = m_ts.size();
@@ -494,6 +506,7 @@ public:
             ast_translation translator(m, *new_m);
             in_copies.push_back(in->translate(translator));
             ts.push_back(m_ts.get(i)->translate(*new_m));
+            scl.push_child(&new_m->limit());
         }
 
         unsigned finished_id       = UINT_MAX;

src/tactic/ufbv/macro_finder_tactic.cpp

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

src/tactic/ufbv/quasi_macros_tactic.cpp

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

src/tactic/ufbv/ufbv_rewriter_tactic.cpp

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