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
16
class
boolbv_widtht
17
{
18
public
:
19
explicit
boolbv_widtht
(
const
namespacet
&_ns);
20
~boolbv_widtht
();
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
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:28
boolbv_widtht::operator()
std::size_t operator()(const typet &type) const
Definition:
boolbv_width.h:22
typet
The type of an expression, extends irept.
Definition:
type.h:29
boolbv_widtht::get_entry
const entryt & get_entry(const typet &type) const
Definition:
boolbv_width.cpp:26
boolbv_widtht::membert::offset
std::size_t offset
Definition:
boolbv_width.h:29
namespace.h
boolbv_widtht::entryt
Definition:
boolbv_width.h:40
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:92
std_types.h
Pre-defined types.
boolbv_widtht::cachet
std::unordered_map< typet, entryt, irep_hash > cachet
Definition:
boolbv_width.h:45
boolbv_widtht::ns
const namespacet & ns
Definition:
boolbv_width.h:37
boolbv_widtht::boolbv_widtht
boolbv_widtht(const namespacet &_ns)
Definition:
boolbv_width.cpp:18
boolbv_widtht::cache
cachet cache
Definition:
boolbv_width.h:48
boolbv_widtht
Definition:
boolbv_width.h:17
struct_typet
Structure type, corresponds to C style structs.
Definition:
std_types.h:226
boolbv_widtht::entryt::total_width
std::size_t total_width
Definition:
boolbv_width.h:41
boolbv_widtht::entryt::members
std::vector< membert > members
Definition:
boolbv_width.h:42
boolbv_widtht::membert::width
std::size_t width
Definition:
boolbv_width.h:29
boolbv_widtht::get_member
const membert & get_member(const struct_typet &type, const irep_idt &member) const
Definition:
boolbv_width.cpp:204
boolbv_widtht::~boolbv_widtht
~boolbv_widtht()
Definition:
boolbv_width.cpp:22
solvers
flattening
boolbv_width.h
Generated by
1.8.20