cprover
boolbv_width.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
15class namespacet;
16class struct_typet;
17
19{
20public:
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
38protected:
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
boolbv_widtht(const namespacet &_ns)
const namespacet & ns
Definition: boolbv_width.h:39
const entryt & get_entry(const typet &type) const
virtual std::size_t operator()(const typet &type) const
Definition: boolbv_width.h:24
std::unordered_map< typet, entryt, irep_hash > cachet
Definition: boolbv_width.h:47
virtual ~boolbv_widtht()=default
const membert & get_member(const struct_typet &type, const irep_idt &member) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Structure type, corresponds to C style structs.
Definition: std_types.h:231
The type of an expression, extends irept.
Definition: type.h:29
std::size_t total_width
Definition: boolbv_width.h:43
std::vector< membert > members
Definition: boolbv_width.h:44
Defines typet, type_with_subtypet and type_with_subtypest.