dReal4
cds.h
1 #pragma once
2 
3 #include <memory>
4 
5 #include <cds/container/mspriority_queue.h>
6 #include <cds/container/treiber_stack.h>
7 #include <cds/gc/hp.h>
8 #include <cds/init.h>
9 
10 namespace dreal {
11 
12 using gc_type = cds::gc::HP;
13 
14 template <typename T>
15 using Stack = cds::container::TreiberStack<gc_type, T>;
16 
17 template <typename T, typename Comparator>
18 using PriorityQueue = cds::container::MSPriorityQueue<
19  T, typename cds::container::mspriority_queue::make_traits<
20  cds::opt::buffer<cds::opt::v::initialized_dynamic_buffer<char>>,
21  cds::opt::compare<Comparator>>::type>;
22 
24  public:
25  explicit CdsScopeGuard(bool use) : use_{use} {
26  if (use_) {
27  cds::threading::Manager::attachThread();
28  }
29  }
30  CdsScopeGuard(const CdsScopeGuard&) = delete;
31  CdsScopeGuard(CdsScopeGuard&&) = delete;
32  CdsScopeGuard& operator=(const CdsScopeGuard&) = delete;
33  CdsScopeGuard& operator=(CdsScopeGuard&&) = delete;
34 
35  ~CdsScopeGuard() {
36  if (use_) {
37  cds::threading::Manager::detachThread();
38  }
39  }
40 
41  private:
42  const bool use_{};
43 };
44 
45 class CdsInit {
46  public:
47  explicit CdsInit(bool use_lock_free_container) {
48  // Initialize libcds
49  cds::Initialize();
50  hpGC_ = std::make_unique<gc_type>();
51  if (use_lock_free_container) {
52  cds::threading::Manager::attachThread();
53  }
54  }
55  CdsInit(const CdsInit&) = delete;
56  CdsInit(CdsInit&&) = delete;
57  CdsInit& operator=(const CdsInit&) = delete;
58  CdsInit& operator=(CdsInit&&) = delete;
59 
60  ~CdsInit() {
61  // Terminate libcds
62  cds::Terminate();
63  }
64 
65  private:
66  // Initialize Hazard Pointer singleton
67  std::unique_ptr<gc_type> hpGC_;
68 };
69 
70 } // namespace dreal
Sum type of symbolic::Expression and symbolic::Formula.
Definition: api.cc:9
Definition: cds.h:23
Definition: cds.h:45