ensure limit children are safe for race conditions

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

src/ast/rewriter/rewriter_def.h

@@ -576,10 +576,7 @@ void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr)
     SASSERT(!frame_stack().empty());
     while (!frame_stack().empty()) {
         if (m().canceled()) {
-            if (m().limit().cancel_flag_set()) {
+            throw rewriter_exception(m().limit().get_cancel_msg());
-                throw rewriter_exception(Z3_CANCELED_MSG);
-            }
-            throw rewriter_exception(Z3_MAX_RESOURCE_MSG);
         }
         SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
         frame & fr = frame_stack().back();

src/solver/solver.h

@@ -41,7 +41,6 @@ public:
      - parameter setting (updt_params)
      - statistics
      - results based on check_sat_result API
-     - interruption (set_cancel)
 */
 class solver : public check_sat_result {
 public:
@@ -105,14 +104,6 @@ public:
     */
     virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
 
-    /**
-       \brief Interrupt this solver.
-    */
-    //void cancel() { set_cancel(true); }
-    /**
-       \brief Reset the interruption.
-    */
-    //void reset_cancel() { set_cancel(false); }
 
     /**
        \brief Set a progress callback procedure that is invoked by this solver during check_sat.
@@ -156,9 +147,6 @@ public:
         ~scoped_push() { if (!m_nopop) s.pop(1); }
         void disable_pop() { m_nopop = true; }
     };
-
-protected:
-    //virtual void set_cancel(bool f) = 0;
 };
 
 #endif

src/tactic/aig/aig_tactic.cpp

@@ -37,6 +37,7 @@ class aig_tactic : public tactic {
         
         ~mk_aig_manager() {
             dealloc(m_owner.m_aig_manager);
+            m_owner.m_aig_manager = 0;
         }
     };
 

src/tactic/core/blast_term_ite_tactic.cpp

@@ -182,12 +182,8 @@ public:
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
-        imp * d = m_imp;
+        dealloc(m_imp);
-        m_imp = 0;
+        m_imp = alloc(imp, m, m_params);
-        
-        dealloc(d);
-        d = alloc(imp, m, m_params);
-        m_imp = d;        
     }
 
     static void blast_term_ite(expr_ref& fml) {

src/util/rlimit.cpp

@@ -57,15 +57,47 @@ void reslimit::pop() {
     m_cancel = false;
 }
 
+char const* get_cancel_msg() const {
+    if (m_cancel) {
+        return Z3_CANCELED_MSG;
+    }
+    else {
+        return Z3_MAX_RESOURCE_MSG;
+    }
+}
+
+void reslimit::push_child(reslimit* r) {
+    #pragma omp critical (reslimit_cancel)
+    {
+        m_children.push_back(r); 
+    }
+}
+
+void reslimit::pop_child() {
+    #pragma omp critical (reslimit_cancel)
+    {
+        m_children.pop_back(); 
+    }
+}
+
 void reslimit::cancel() {
-    m_cancel = true; 
+    #pragma omp critical (reslimit_cancel)
-    for (unsigned i = 0; i < m_children.size(); ++i) {
+    {
-        m_children[i]->cancel();
+        set_cancel(false);
     }
 }
+
+
 void reslimit::reset_cancel() {
-    m_cancel = false; 
+    #pragma omp critical (reslimit_cancel)
-    for (unsigned i = 0; i < m_children.size(); ++i) {
+    {
-        m_children[i]->reset_cancel();
+        set_cancel(false);
+    }
+}
+
+void reslimit::set_cancel(bool f) { 
+    m_cancel = f; 
+    for (unsigned i = 0; i < m_children.size(); ++i) {
+        m_children[i]->set_cancel(f);
     }
 }

src/util/rlimit.h

@@ -27,19 +27,23 @@ class reslimit {
     uint64          m_limit;
     svector<uint64> m_limits;
     ptr_vector<reslimit> m_children;
+
+    void set_cancel(bool f);
+    
 public:    
     reslimit();
     void push(unsigned delta_limit);
     void pop();
-    void push_child(reslimit* r) { m_children.push_back(r); }
+    void push_child(reslimit* r);
-    void pop_child() { m_children.pop_back(); }
+    void pop_child();
 
     bool inc();
     bool inc(unsigned offset);
     uint64 count() const; 
 
 
-    bool cancel_flag_set() { return m_cancel; }
+    bool get_cancel_flag() const { return m_cancel; }
+    char const* get_cancel_msg() const;
     void cancel();
     void reset_cancel();
 };