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
18
class
boolbv_widtht
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
solvers
flattening
boolbv_width.h
Generated by
1.8.20