CBMC
ref_expr_set.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_REF_EXPR_SET_H
13 #define CPROVER_UTIL_REF_EXPR_SET_H
14 
15 #include <unordered_set>
16 
17 #include "expr.h"
18 #include "reference_counting.h"
19 
20 extern const std::unordered_set<exprt, irep_hash> empty_expr_set;
21 
23 {
25  typedef std::unordered_set<exprt, irep_hash> expr_sett;
27 
28  static const ref_expr_set_dt blank;
29 };
30 
31 class ref_expr_sett:public reference_counting<ref_expr_set_dt>
32 {
33 public:
35 
36  bool empty() const
37  {
38  if(d==nullptr)
39  return true;
40  return d->expr_set.empty();
41  }
42 
43  const expr_sett &expr_set() const
44  {
45  return read().expr_set;
46  }
47 
49  {
50  return write().expr_set;
51  }
52 
54  {
55  if(s2.d==nullptr)
56  return false;
57 
58  if(s2.d==d)
59  return false;
60 
61  if(d==nullptr)
62  {
63  copy_from(s2);
64  return true;
65  }
66 
67  return make_union(s2.d->expr_set);
68  }
69 
70  bool make_union(const expr_sett &s2)
71  {
72  expr_sett tmp(read().expr_set);
73  size_t old_size=tmp.size();
74  tmp.insert(s2.begin(), s2.end());
75 
76  // anything new?
77  if(tmp.size()==old_size)
78  return false;
79  move(tmp);
80  return true;
81  }
82 
83  void move(expr_sett &s2)
84  {
85  clear();
86  write().expr_set.swap(s2);
87  }
88 };
89 
90 #endif // CPROVER_UTIL_REF_EXPR_SET_H
int16_t s2
Definition: bytecode_info.h:60
const expr_sett & expr_set() const
Definition: ref_expr_set.h:43
ref_expr_set_dt::expr_sett expr_sett
Definition: ref_expr_set.h:34
bool make_union(const ref_expr_sett &s2)
Definition: ref_expr_set.h:53
void move(expr_sett &s2)
Definition: ref_expr_set.h:83
expr_sett & expr_set_write()
Definition: ref_expr_set.h:48
bool empty() const
Definition: ref_expr_set.h:36
bool make_union(const expr_sett &s2)
Definition: ref_expr_set.h:70
const ref_expr_set_dt & read() const
void copy_from(const reference_counting &other)
const std::unordered_set< exprt, irep_hash > empty_expr_set
Reference Counting.
std::unordered_set< exprt, irep_hash > expr_sett
Definition: ref_expr_set.h:25
static const ref_expr_set_dt blank
Definition: ref_expr_set.h:28
expr_sett expr_set
Definition: ref_expr_set.h:26