replace remaining volatiles with atomic<>

volatiles are now deprecated in recent C++

src/ast/expr2polynomial.cpp

@@ -23,6 +23,7 @@ Notes:
 #include "ast/ast_smt2_pp.h"
 #include "util/z3_exception.h"
 #include "util/common_msgs.h"
+#include <atomic>
 
 struct expr2polynomial::imp {
     struct frame {
@@ -51,7 +52,7 @@ struct expr2polynomial::imp {
 
     bool                               m_use_var_idxs;
 
-    volatile bool                      m_cancel;
+    std::atomic<bool>                  m_cancel;
 
     imp(expr2polynomial & w, ast_manager & am, polynomial::manager & pm, expr2var * e2v, bool use_var_idxs):
         m_wrapper(w),

src/sat/sat_parallel.cpp

@@ -100,11 +100,9 @@ namespace sat {
 
     void parallel::init_solvers(solver& s, unsigned num_extra_solvers) {
         unsigned num_threads = num_extra_solvers + 1;
-        m_solvers.resize(num_extra_solvers);
+        m_solvers.init(num_extra_solvers);
+        m_limits.init(num_extra_solvers);
         symbol saved_phase = s.m_params.get_sym("phase", symbol("caching"));
-        for (unsigned i = 0; i < num_extra_solvers; ++i) {        
-            m_limits.push_back(reslimit());
-        }
         
         for (unsigned i = 0; i < num_extra_solvers; ++i) {
             s.m_params.set_uint("random_seed", s.m_rand());

src/solver/combined_solver.cpp

@@ -23,6 +23,7 @@ Notes:
 #include "ast/ast_pp.h"
 #include "solver/solver.h"
 #include "solver/combined_solver_params.hpp"
+#include <atomic>
 #define PS_VB_LVL 15
 
 /**
@@ -71,7 +72,7 @@ private:
 
     struct aux_timeout_eh : public event_handler {
         solver *        m_solver;
-        volatile bool   m_canceled;
+        std::atomic<bool> m_canceled;
         aux_timeout_eh(solver * s):m_solver(s), m_canceled(false) {}
         ~aux_timeout_eh() override {
             if (m_canceled) {                

src/solver/parallel_tactic.cpp

@@ -47,6 +47,7 @@ tactic * mk_parallel_tactic(solver* s, params_ref const& p) {
 
 #else
 
+#include <atomic>
 #include <thread>
 #include <mutex>
 #include <cmath>
@@ -63,7 +64,7 @@ class parallel_tactic : public tactic {
         ptr_vector<solver_state>     m_tasks;
         ptr_vector<solver_state>     m_active;
         unsigned                     m_num_waiters;
-        volatile bool                m_shutdown;
+        std::atomic<bool>            m_shutdown;
 
         void inc_wait() {
             std::lock_guard<std::mutex> lock(m_mutex);
@@ -365,7 +366,7 @@ private:
     unsigned      m_branches;
     unsigned      m_backtrack_frequency;
     unsigned      m_conquer_delay;
-    volatile bool m_has_undef;
+    std::atomic<bool> m_has_undef;
     bool          m_allsat;
     unsigned      m_num_unsat;
     unsigned      m_last_depth;

src/util/debug.cpp

@@ -21,11 +21,12 @@ Revision History:
 #include<unistd.h>
 #endif
 #include<iostream>
+#include "util/mutex.h"
 #include "util/str_hashtable.h"
 #include "util/z3_exception.h"
 #include "util/z3_version.h"
 
-static volatile bool g_enable_assertions = true;
+static atomic<bool> g_enable_assertions(true);
 
 void enable_assertions(bool f) {
     g_enable_assertions = f;

src/util/rlimit.h

@@ -19,6 +19,7 @@ Revision History:
 #pragma once
 
 #include "util/vector.h"
+#include <atomic>
 
 void initialize_rlimit();
 void finalize_rlimit();
@@ -28,7 +29,7 @@ void finalize_rlimit();
 */
 
 class reslimit {
-    volatile unsigned   m_cancel;
+    std::atomic<unsigned> m_cancel;
     bool            m_suspend;
     uint64_t        m_count;
     uint64_t        m_limit;

src/util/vector.h

@@ -133,8 +133,13 @@ public:
     }
 
     vector(SZ s) {
+        m_data = nullptr;
+        init(s);
+    }
+
+    void init(SZ s) {
+        SASSERT(m_data == nullptr;);
         if (s == 0) {
-            m_data = nullptr;
             return;
         }
         SZ * mem = reinterpret_cast<SZ*>(memory::allocate(sizeof(T) * s + sizeof(SZ) * 2));