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
15
class
namespacet
;
16
17
class
boolbv_widtht
18
{
19
public
:
20
explicit
boolbv_widtht
(
const
namespacet
&_ns);
21
virtual
~boolbv_widtht
() =
default
;
22
23
virtual
std::size_t
operator()
(
const
typet
&type)
const
24
{
25
return
get_entry
(type).
total_width
;
26
}
27
28
struct
membert
29
{
30
std::size_t
offset
,
width
;
31
};
32
33
const
membert
&
get_member
(
34
const
struct_typet
&type,
35
const
irep_idt
&member)
const
;
36
37
protected
:
38
const
namespacet
&
ns
;
39
40
struct
entryt
41
{
42
std::size_t
total_width
;
43
std::vector<membert>
members
;
44
};
45
46
typedef
std::unordered_map<typet, entryt, irep_hash>
cachet
;
47
48
// the 'mutable' is allow const methods above
49
mutable
cachet
cache
;
50
51
const
entryt
&
get_entry
(
const
typet
&type)
const
;
52
};
53
54
#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:29
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:30
boolbv_widtht::entryt
Definition:
boolbv_width.h:41
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:92
boolbv_widtht::operator()
virtual std::size_t operator()(const typet &type) const
Definition:
boolbv_width.h:23
std_types.h
Pre-defined types.
boolbv_widtht::cachet
std::unordered_map< typet, entryt, irep_hash > cachet
Definition:
boolbv_width.h:46
boolbv_widtht::ns
const namespacet & ns
Definition:
boolbv_width.h:38
boolbv_widtht::boolbv_widtht
boolbv_widtht(const namespacet &_ns)
Definition:
boolbv_width.cpp:19
boolbv_widtht::cache
cachet cache
Definition:
boolbv_width.h:49
boolbv_widtht
Definition:
boolbv_width.h:18
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:42
boolbv_widtht::entryt::members
std::vector< membert > members
Definition:
boolbv_width.h:43
boolbv_widtht::membert::width
std::size_t width
Definition:
boolbv_width.h:30
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:201
solvers
flattening
boolbv_width.h
Generated by
1.8.20