address race condition in cleanup methods

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

src/cmd_context/cmd_context.cpp

@@ -346,8 +346,14 @@ cmd_context::~cmd_context() {
 }
 
 void cmd_context::set_cancel(bool f) {
-    if (m_solver)
+    if (m_solver) {
-        m_solver->set_cancel(f);
+        if (f) {
+            m_solver->cancel(); 
+        }
+        else {
+            m_solver->reset_cancel();
+        }
+    }
     if (has_manager())
         m().set_cancel(f);
 }

src/solver/combined_solver.cpp

@@ -218,8 +218,14 @@ public:
     }
 
     virtual void set_cancel(bool f) {
-        m_solver1->set_cancel(f);
+        if (f) {
-        m_solver2->set_cancel(f);
+            m_solver1->cancel();
+            m_solver2->cancel();
+        }
+        else {
+            m_solver1->reset_cancel();
+            m_solver2->reset_cancel();
+        }
     }
     
     virtual void set_progress_callback(progress_callback * callback) {

src/solver/solver.h

@@ -99,7 +99,6 @@ public:
     */
     virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
 
-    virtual void set_cancel(bool f) {}
     /**
        \brief Interrupt this solver.
     */
@@ -130,6 +129,9 @@ public:
        \brief Display the content of this solver.
     */
     virtual void display(std::ostream & out) const;
+protected:
+    virtual void set_cancel(bool f) = 0;
+
 };
 
 #endif

src/solver/tactic2solver.cpp

@@ -173,8 +173,12 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
 }
 
 void tactic2solver::set_cancel(bool f) {
-    if (m_tactic.get())
+    if (m_tactic.get()) {
-        m_tactic->set_cancel(f);
+        if (f) 
+            m_tactic->cancel();
+        else
+            m_tactic->reset_cancel();
+    }
 }
 
 void tactic2solver::collect_statistics(statistics & st) const {

src/tactic/aig/aig.h

@@ -73,8 +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 cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
     void set_cancel(bool f);
 };
 

src/tactic/arith/add_bounds_tactic.cpp

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

src/tactic/arith/degree_shift_tactic.cpp

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

src/tactic/arith/diff_neq_tactic.cpp

@@ -398,20 +398,13 @@ public:
     }
     
     virtual void cleanup() {
-        unsigned num_conflicts = m_imp->m_num_conflicts;
+        imp * d = alloc(imp, m_imp->m, m_params);
-        ast_manager & m = m_imp->m;
+        d->m_num_conflicts = m_imp->m_num_conflicts;
-        imp * d = m_imp;
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
-        m_imp->m_num_conflicts = num_conflicts;
     }
 
 protected:

src/tactic/arith/factor_tactic.cpp

@@ -333,18 +333,12 @@ public:
     }
 
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
+        imp * d = alloc(imp, m_imp->m, m_params);
-        imp * d = m_imp;
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {

src/tactic/arith/fix_dl_var_tactic.cpp

@@ -338,18 +338,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
+        imp * d = alloc(imp, m_imp->m, m_params);
-        imp * d = m_imp;
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {

src/tactic/arith/fm_tactic.cpp

@@ -1682,18 +1682,12 @@ public:
     }
 
     virtual void cleanup() {
-        ast_manager & m = m_imp->m;
+        imp * d = alloc(imp, m_imp->m, m_params);
-        imp * d = m_imp;
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
 
     virtual void operator()(goal_ref const & in, 

src/tactic/arith/lia2pb_tactic.cpp

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

src/tactic/arith/normalize_bounds_tactic.cpp

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

src/tactic/arith/pb2bv_tactic.cpp

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

src/tactic/arith/propagate_ineqs_tactic.cpp

@@ -548,16 +548,10 @@ void propagate_ineqs_tactic::set_cancel(bool f) {
 }
  
 void propagate_ineqs_tactic::cleanup() {
-    ast_manager & m = m_imp->m;
+    imp * d = alloc(imp, m_imp->m, m_params);
-    imp * d = m_imp;
     #pragma omp critical (tactic_cancel)
     {
-        d = m_imp;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel) 
-    {
-        m_imp = d;
-    }
 }

src/tactic/arith/recover_01_tactic.cpp

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

src/tactic/bv/bit_blaster_tactic.cpp

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

src/tactic/bv/bv1_blaster_tactic.cpp

@@ -465,18 +465,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m();
+        imp * d = alloc(imp, m_imp->m(), m_params);
-        imp * d = m_imp;
         #pragma omp critical (tactic_cancel)
         {
-            d = m_imp;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel) 
-        {
-            m_imp = d;
-        }
     }
     
     unsigned get_num_steps() const {

src/tactic/bv/bv_size_reduction_tactic.cpp

@@ -392,17 +392,11 @@ void bv_size_reduction_tactic::set_cancel(bool f) {
 }
  
 void bv_size_reduction_tactic::cleanup() {
-    ast_manager & m = m_imp->m;
+    imp * d = alloc(imp, m_imp->m);
-    imp * d = m_imp;
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 

src/tactic/bv/max_bv_sharing_tactic.cpp

@@ -311,18 +311,12 @@ public:
     }
     
     virtual void cleanup() {
-        ast_manager & m = m_imp->m();
+        imp * d = alloc(imp, m_imp->m(), m_params);
-        imp * d = m_imp;
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {

src/tactic/core/cofactor_elim_term_ite.cpp

@@ -683,12 +683,7 @@ cofactor_elim_term_ite::cofactor_elim_term_ite(ast_manager & m, params_ref const
 }
 
 cofactor_elim_term_ite::~cofactor_elim_term_ite() {
-    imp * d = m_imp;
+    dealloc(m_imp);
-    #pragma omp critical (cofactor_elim_term_ite)
-    {
-        m_imp = 0;
-    }
-    dealloc(d);
 }
 
 void cofactor_elim_term_ite::updt_params(params_ref const & p) {
@@ -704,19 +699,17 @@ void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) {
 }
     
 void cofactor_elim_term_ite::set_cancel(bool f) {
-    #pragma omp critical (cofactor_elim_term_ite)
+    if (m_imp)
-    {
+        m_imp->set_cancel(f);
-        if (m_imp)
-            m_imp->set_cancel(f);
-    }
 }
 
 void cofactor_elim_term_ite::cleanup() {
     ast_manager & m = m_imp->m;    
-    #pragma omp critical (cofactor_elim_term_ite) 
+    imp * d = alloc(imp, m, m_params);
+    #pragma omp critical (tactic_cancel)
     {
-        dealloc(m_imp);
+        std::swap(d, m_imp);
-        m_imp = alloc(imp, m, m_params);
     }
+    dealloc(d);
 }
 

src/tactic/core/cofactor_elim_term_ite.h

@@ -37,8 +37,9 @@ public:
     
     void cancel() { set_cancel(true); }
     void reset_cancel() { set_cancel(false); }
-    void set_cancel(bool f);
     void cleanup();
+    void set_cancel(bool f);
+
 };
 
 #endif

src/tactic/core/ctx_simplify_tactic.cpp

@@ -548,16 +548,11 @@ void ctx_simplify_tactic::set_cancel(bool f) {
 
 void ctx_simplify_tactic::cleanup() {
     ast_manager & m   = m_imp->m;
-    imp * d = m_imp;
+    imp * d = alloc(imp, m, m_params);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 

src/tactic/core/der_tactic.cpp

@@ -90,17 +90,12 @@ public:
 
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
     
     virtual void set_cancel(bool f) {

src/tactic/core/elim_term_ite_tactic.cpp

@@ -174,17 +174,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {

src/tactic/core/elim_uncnstr_tactic.cpp

@@ -1037,17 +1037,12 @@ public:
     virtual void cleanup() {
         unsigned num_elim_apps = get_num_elim_apps();
         ast_manager & m = m_imp->m_manager;        
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
         m_imp->m_num_elim_apps = num_elim_apps;
     }
 

src/tactic/core/occf_tactic.cpp

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

src/tactic/core/propagate_values_tactic.cpp

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

src/tactic/core/reduce_args_tactic.cpp

@@ -542,16 +542,11 @@ void reduce_args_tactic::set_cancel(bool f) {
 
 void reduce_args_tactic::cleanup() {
     ast_manager & m   = m_imp->m();    
-    imp * d = m_imp;
+    imp * d = alloc(imp, m);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 

src/tactic/core/simplify_tactic.cpp

@@ -115,17 +115,12 @@ void simplify_tactic::set_cancel(bool f) {
 
 void simplify_tactic::cleanup() {
     ast_manager & m = m_imp->m();
-    imp * d = m_imp;
+    imp * d = alloc(imp, m, m_params);
     #pragma omp critical (tactic_cancel)
     {
-        m_imp = 0;
+        std::swap(d, m_imp);
     }
     dealloc(d);
-    d = alloc(imp, m, m_params);
-    #pragma omp critical (tactic_cancel)
-    {
-        m_imp = d;
-    }
 }
 
 unsigned simplify_tactic::get_num_steps() const {

src/tactic/core/simplify_tactic.h

@@ -43,9 +43,11 @@ public:
     virtual void cleanup();
 
     unsigned get_num_steps() const;
-    virtual void set_cancel(bool f);
 
     virtual tactic * translate(ast_manager & m) { return alloc(simplify_tactic, m, m_params); }
+protected:
+    virtual void set_cancel(bool f);
+
 };
 
 tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());

src/tactic/core/solve_eqs_tactic.cpp

@@ -749,23 +749,19 @@ public:
     virtual void cleanup() {
         unsigned num_elim_vars = m_imp->m_num_eliminated_vars;
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
         expr_replacer * r = m_imp->m_r;
         if (r)
             r->set_substitution(0);
         bool owner = m_imp->m_r_owner;
         m_imp->m_r_owner  = false; // stole replacer
+
+        imp * d = alloc(imp, m, m_params, r, owner);
+        d->m_num_eliminated_vars = num_elim_vars;
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params, r, owner);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
-        m_imp->m_num_eliminated_vars = num_elim_vars;
     }
 
     virtual void collect_statistics(statistics & st) const {

src/tactic/core/tseitin_cnf_tactic.cpp

@@ -898,20 +898,14 @@ public:
     }
     
     virtual void cleanup() {
-        unsigned num_aux_vars = m_imp->m_num_aux_vars;
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
+        d->m_num_aux_vars = m_imp->m_num_aux_vars;
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
-        m_imp->m_num_aux_vars = num_aux_vars;
     }
 
     virtual void set_cancel(bool f) {

src/tactic/fpa/fpa2bv_tactic.cpp

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

src/tactic/tactic.h

@@ -47,7 +47,6 @@ public:
 
     void cancel();
     void reset_cancel();
-    virtual void set_cancel(bool f) {}
     
     /**
        \brief Apply tactic to goal \c in.
@@ -96,6 +95,13 @@ public:
 
     // translate tactic to the given manager
     virtual tactic * translate(ast_manager & m) = 0;
+private:
+    friend class nary_tactical;
+    friend class binary_tactical;
+    friend class unary_tactical;
+
+    virtual void set_cancel(bool f) {}
+
 };
 
 typedef ref<tactic>         tactic_ref;

src/tactic/tactical.cpp

@@ -102,11 +102,8 @@ protected:
        \brief Reset cancel flag of t if this was not canceled.
     */
     void parent_reset_cancel(tactic & t) {
-        #pragma omp critical (tactic_cancel)
+        if (!m_cancel) {
-        {
+            t.reset_cancel();
-            if (!m_cancel) {
-                t.set_cancel(false);
-            }
         }
     }
 
@@ -393,11 +390,8 @@ protected:
        \brief Reset cancel flag of st if this was not canceled.
     */
     void parent_reset_cancel(tactic & t) {
-        #pragma omp critical (tactic_cancel)
+        if (!m_cancel) {
-        {
+            t.reset_cancel();
-            if (!m_cancel) {
-                t.set_cancel(false);
-            }
         }
     }
 

src/tactic/ufbv/macro_finder_tactic.cpp

@@ -144,17 +144,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {

src/tactic/ufbv/quasi_macros_tactic.cpp

@@ -151,17 +151,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {

src/tactic/ufbv/ufbv_rewriter_tactic.cpp

@@ -119,17 +119,12 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m();
-        imp * d = m_imp;
+        imp * d = alloc(imp, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
-            m_imp = 0;
+            std::swap(d, m_imp);
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
-        #pragma omp critical (tactic_cancel)
-        {
-            m_imp = d;
-        }
     }
 
     virtual void set_cancel(bool f) {