cprover
boolbv_width.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_FLATTENING_BOOLBV_WIDTH_H
11 #define CPROVER_SOLVERS_FLATTENING_BOOLBV_WIDTH_H
12 
13 #include <util/type.h>
14 
15 class namespacet;
16 class struct_typet;
17 
19 {
20 public:
21  explicit boolbv_widtht(const namespacet &_ns);
22  virtual ~boolbv_widtht() = default;
23 
24  virtual std::size_t operator()(const typet &type) const
25  {
26  return get_entry(type).total_width;
27  }
28 
29  struct membert
30  {
31  std::size_t offset, width;
32  };
33 
34  const membert &get_member(
35  const struct_typet &type,
36  const irep_idt &member) const;
37 
38 protected:
39  const namespacet &ns;
40 
41  struct entryt
42  {
43  std::size_t total_width;
44  std::vector<membert> members;
45  };
46 
47  typedef std::unordered_map<typet, entryt, irep_hash> cachet;
48 
49  // the 'mutable' is allow const methods above
50  mutable cachet cache;
51 
52  const entryt &get_entry(const typet &type) const;
53 };
54 
55 #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_WIDTH_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
boolbv_widtht::membert
Definition: boolbv_width.h:30
typet
The type of an expression, extends irept.
Definition: type.h:28
boolbv_widtht::get_entry
const entryt & get_entry(const typet &type) const
Definition: boolbv_width.cpp:23
boolbv_widtht::membert::offset
std::size_t offset
Definition: boolbv_width.h:31
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
boolbv_widtht::entryt
Definition: boolbv_width.h:42
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
boolbv_widtht::operator()
virtual std::size_t operator()(const typet &type) const
Definition: boolbv_width.h:24
boolbv_widtht::cachet
std::unordered_map< typet, entryt, irep_hash > cachet
Definition: boolbv_width.h:47
boolbv_widtht::ns
const namespacet & ns
Definition: boolbv_width.h:39
boolbv_widtht::boolbv_widtht
boolbv_widtht(const namespacet &_ns)
Definition: boolbv_width.cpp:19
boolbv_widtht::cache
cachet cache
Definition: boolbv_width.h:50
boolbv_widtht
Definition: boolbv_width.h:19
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:231
boolbv_widtht::entryt::total_width
std::size_t total_width
Definition: boolbv_width.h:43
boolbv_widtht::entryt::members
std::vector< membert > members
Definition: boolbv_width.h:44
boolbv_widtht::membert::width
std::size_t width
Definition: boolbv_width.h:31
boolbv_widtht::~boolbv_widtht
virtual ~boolbv_widtht()=default
boolbv_widtht::get_member
const membert & get_member(const struct_typet &type, const irep_idt &member) const
Definition: boolbv_width.cpp:202