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
(
propt
&_prop,
const
boolbv_widtht
&_boolbv_width)
27
:
prop
(_prop),
boolbv_width
(_boolbv_width)
28
{
29
}
30
31
struct
map_bitt
32
{
33
map_bitt
():
is_set
(false) { }
34
bool
is_set
;
35
literalt
l
;
36
};
37
38
typedef
std::vector<map_bitt>
literal_mapt
;
39
40
class
map_entryt
41
{
42
public
:
43
map_entryt
():
width
(0),
bvtype
(
bvtypet
::
IS_UNKNOWN
)
44
{
45
}
46
47
std::size_t
width
;
48
bvtypet
bvtype
;
49
typet
type
;
50
literal_mapt
literal_map
;
51
52
std::string
get_value
(
const
propt
&)
const
;
53
};
54
55
typedef
std::unordered_map<irep_idt, map_entryt>
mappingt
;
56
mappingt
mapping
;
57
58
void
show
()
const
;
59
60
map_entryt
&
get_map_entry
(
61
const
irep_idt
&identifier,
62
const
typet
&type);
63
64
void
get_literals
(
65
const
irep_idt
&identifier,
66
const
typet
&type,
67
const
std::size_t width,
68
bvt
&literals);
69
70
void
set_literals
(
71
const
irep_idt
&identifier,
72
const
typet
&type,
73
const
bvt
&literals);
74
75
void
erase_literals
(
76
const
irep_idt
&identifier,
77
const
typet
&type);
78
79
protected
:
80
propt
&
prop
;
81
const
boolbv_widtht
&
boolbv_width
;
82
};
83
84
#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:37
boolbv_mapt::erase_literals
void erase_literals(const irep_idt &identifier, const typet &type)
Definition:
boolbv_map.cpp:155
boolbv_mapt::boolbv_mapt
boolbv_mapt(propt &_prop, const boolbv_widtht &_boolbv_width)
Definition:
boolbv_map.h:26
boolbv_mapt::literal_mapt
std::vector< map_bitt > literal_mapt
Definition:
boolbv_map.h:38
boolbv_mapt::map_entryt::bvtype
bvtypet bvtype
Definition:
boolbv_map.h:48
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:29
boolbv_mapt::prop
propt & prop
Definition:
boolbv_map.h:80
bvt
std::vector< literalt > bvt
Definition:
literal.h:201
boolbv_mapt::map_bitt
Definition:
boolbv_map.h:32
boolbv_mapt::map_bitt::map_bitt
map_bitt()
Definition:
boolbv_map.h:33
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:83
boolbv_type.h
boolbv_mapt::map_entryt::literal_map
literal_mapt literal_map
Definition:
boolbv_map.h:50
boolbv_mapt::show
void show() const
Definition:
boolbv_map.cpp:74
namespace.h
boolbv_mapt::map_entryt::width
std::size_t width
Definition:
boolbv_map.h:47
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
bvtypet
bvtypet
Definition:
boolbv_type.h:17
boolbv_mapt::map_entryt
Definition:
boolbv_map.h:41
boolbv_mapt::mapping
mappingt mapping
Definition:
boolbv_map.h:56
boolbv_mapt::mappingt
std::unordered_map< irep_idt, map_entryt > mappingt
Definition:
boolbv_map.h:55
prop.h
boolbv_mapt::boolbv_width
const boolbv_widtht & boolbv_width
Definition:
boolbv_map.h:81
boolbv_mapt::map_entryt::type
typet type
Definition:
boolbv_map.h:49
boolbv_widtht
Definition:
boolbv_width.h:17
propt
TO_BE_DOCUMENTED.
Definition:
prop.h:25
boolbv_width.h
literalt
Definition:
literal.h:26
boolbv_mapt
Definition:
boolbv_map.h:24
boolbv_mapt::map_bitt::is_set
bool is_set
Definition:
boolbv_map.h:34
boolbv_mapt::map_bitt::l
literalt l
Definition:
boolbv_map.h:35
boolbv_mapt::map_entryt::map_entryt
map_entryt()
Definition:
boolbv_map.h:43
bvtypet::IS_UNKNOWN
@ IS_UNKNOWN
boolbv_mapt::set_literals
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition:
boolbv_map.cpp:123
solvers
flattening
boolbv_map.h
Generated by
1.8.20