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/std_types.h>
14 #include <util/namespace.h>
15 
17 {
18 public:
19  explicit boolbv_widtht(const namespacet &_ns);
21 
22  std::size_t operator()(const typet &type) const
23  {
24  return get_entry(type).total_width;
25  }
26 
27  struct membert
28  {
29  std::size_t offset, width;
30  };
31 
32  const membert &get_member(
33  const struct_typet &type,
34  const irep_idt &member) const;
35 
36 protected:
37  const namespacet &ns;
38 
39  struct entryt
40  {
41  std::size_t total_width;
42  std::vector<membert> members;
43  };
44 
45  typedef std::unordered_map<typet, entryt, irep_hash> cachet;
46 
47  // the 'mutable' is allow const methods above
48  mutable cachet cache;
49 
50  const entryt &get_entry(const typet &type) const;
51 };
52 
53 #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_WIDTH_H
The type of an expression.
Definition: type.h:22
Structure type.
Definition: std_types.h:297
std::unordered_map< typet, entryt, irep_hash > cachet
Definition: boolbv_width.h:45
const membert & get_member(const struct_typet &type, const irep_idt &member) const
std::size_t operator()(const typet &type) const
Definition: boolbv_width.h:22
TO_BE_DOCUMENTED.
Definition: namespace.h:74
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const namespacet & ns
Definition: boolbv_width.h:37
boolbv_widtht(const namespacet &_ns)
std::vector< membert > members
Definition: boolbv_width.h:42
API to type classes.
std::size_t total_width
Definition: boolbv_width.h:41
const entryt & get_entry(const typet &type) const