cprover
boolbv_map.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_MAP_H
11
#define CPROVER_SOLVERS_FLATTENING_BOOLBV_MAP_H
12
13
#include <vector>
14
15
#include <
util/type.h
>
16
#include <
util/namespace.h
>
17
18
#include <
solvers/prop/prop.h
>
19
20
#include "
boolbv_type.h
"
21
#include "
boolbv_width.h
"
22
23
class
boolbv_mapt
24
{
25
public
:
26
boolbv_mapt
(
27
propt
&_prop,
28
const
namespacet
&_ns,
29
const
boolbv_widtht
&_boolbv_width):
30
prop
(_prop),
ns
(_ns),
boolbv_width
(_boolbv_width)
31
{
32
}
33
34
struct
map_bitt
35
{
36
map_bitt
():
is_set
(false) { }
37
bool
is_set
;
38
literalt
l
;
39
};
40
41
typedef
std::vector<map_bitt>
literal_mapt
;
42
43
class
map_entryt
44
{
45
public
:
46
map_entryt
():
width
(0),
bvtype
(
bvtypet
::
IS_UNKNOWN
)
47
{
48
}
49
50
std::size_t
width
;
51
bvtypet
bvtype
;
52
typet
type
;
53
literal_mapt
literal_map
;
54
55
std::string
get_value
(
const
propt
&)
const
;
56
};
57
58
typedef
std::unordered_map<irep_idt, map_entryt>
mappingt
;
59
mappingt
mapping
;
60
61
void
show
()
const
;
62
63
map_entryt
&
get_map_entry
(
64
const
irep_idt
&identifier,
65
const
typet
&type);
66
67
void
get_literals
(
68
const
irep_idt
&identifier,
69
const
typet
&type,
70
const
std::size_t width,
71
bvt
&literals);
72
73
void
set_literals
(
74
const
irep_idt
&identifier,
75
const
typet
&type,
76
const
bvt
&literals);
77
78
void
erase_literals
(
79
const
irep_idt
&identifier,
80
const
typet
&type);
81
82
protected
:
83
propt
&
prop
;
84
const
namespacet
&
ns
;
85
const
boolbv_widtht
&
boolbv_width
;
86
};
87
88
#endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_MAP_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition:
dstring.h:35
boolbv_mapt::erase_literals
void erase_literals(const irep_idt &identifier, const typet &type)
Definition:
boolbv_map.cpp:158
boolbv_mapt::literal_mapt
std::vector< map_bitt > literal_mapt
Definition:
boolbv_map.h:41
boolbv_mapt::map_entryt::bvtype
bvtypet bvtype
Definition:
boolbv_map.h:51
boolbv_mapt::get_map_entry
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
Definition:
boolbv_map.cpp:49
boolbv_mapt::map_entryt::get_value
std::string get_value(const propt &) const
Definition:
boolbv_map.cpp:21
typet
The type of an expression, extends irept.
Definition:
type.h:27
boolbv_mapt::prop
propt & prop
Definition:
boolbv_map.h:83
bvt
std::vector< literalt > bvt
Definition:
literal.h:200
boolbv_mapt::map_bitt
Definition:
boolbv_map.h:34
boolbv_mapt::map_bitt::map_bitt
map_bitt()
Definition:
boolbv_map.h:36
boolbv_mapt::get_literals
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
Definition:
boolbv_map.cpp:86
boolbv_type.h
boolbv_mapt::map_entryt::literal_map
literal_mapt literal_map
Definition:
boolbv_map.h:53
boolbv_mapt::show
void show() const
Definition:
boolbv_map.cpp:77
namespace.h
boolbv_mapt::ns
const namespacet & ns
Definition:
boolbv_map.h:84
boolbv_mapt::map_entryt::width
std::size_t width
Definition:
boolbv_map.h:50
type.h
bvtypet
bvtypet
Definition:
boolbv_type.h:16
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:93
boolbv_mapt::map_entryt
Definition:
boolbv_map.h:43
boolbv_mapt::mapping
mappingt mapping
Definition:
boolbv_map.h:59
boolbv_mapt::mappingt
std::unordered_map< irep_idt, map_entryt > mappingt
Definition:
boolbv_map.h:58
prop.h
boolbv_mapt::boolbv_width
const boolbv_widtht & boolbv_width
Definition:
boolbv_map.h:85
boolbv_mapt::map_entryt::type
typet type
Definition:
boolbv_map.h:52
boolbv_widtht
Definition:
boolbv_width.h:16
propt
TO_BE_DOCUMENTED.
Definition:
prop.h:24
boolbv_width.h
literalt
Definition:
literal.h:24
boolbv_mapt::boolbv_mapt
boolbv_mapt(propt &_prop, const namespacet &_ns, const boolbv_widtht &_boolbv_width)
Definition:
boolbv_map.h:26
boolbv_mapt
Definition:
boolbv_map.h:23
boolbv_mapt::map_bitt::is_set
bool is_set
Definition:
boolbv_map.h:37
boolbv_mapt::map_bitt::l
literalt l
Definition:
boolbv_map.h:38
boolbv_mapt::map_entryt::map_entryt
map_entryt()
Definition:
boolbv_map.h:46
bvtypet::IS_UNKNOWN
boolbv_mapt::set_literals
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition:
boolbv_map.cpp:126
solvers
flattening
boolbv_map.h
Generated by
1.8.16