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 <iosfwd>
14
#include <vector>
15
16
#include <
util/type.h
>
17
18
#include <
solvers/prop/prop.h
>
19
20
class
boolbv_mapt
21
{
22
public
:
23
explicit
boolbv_mapt
(
propt
&_prop) :
prop
(_prop)
24
{
25
}
26
27
class
map_entryt
28
{
29
public
:
30
typet
type
;
31
bvt
literal_map
;
32
33
std::string
get_value
(
const
propt
&)
const
;
34
};
35
36
typedef
std::unordered_map<irep_idt, map_entryt>
mappingt
;
37
38
void
show
(std::ostream &out)
const
;
39
40
const
bvt
&
get_literals
(
41
const
irep_idt
&identifier,
42
const
typet
&type,
43
std::size_t width);
44
45
void
set_literals
(
46
const
irep_idt
&identifier,
47
const
typet
&type,
48
const
bvt
&literals);
49
50
void
erase_literals
(
51
const
irep_idt
&identifier,
52
const
typet
&type);
53
54
optionalt<std::reference_wrapper<const map_entryt>
>
55
get_map_entry
(
const
irep_idt
&identifier)
const
56
{
57
const
auto
entry =
mapping
.find(identifier);
58
if
(entry ==
mapping
.end())
59
return
{};
60
61
return
optionalt<std::reference_wrapper<const map_entryt>
>(entry->second);
62
}
63
64
const
mappingt
&
get_mapping
()
const
65
{
66
return
mapping
;
67
}
68
69
protected
:
70
mappingt
mapping
;
71
propt
&
prop
;
72
};
73
74
#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:118
boolbv_mapt::get_mapping
const mappingt & get_mapping() const
Definition:
boolbv_map.h:64
boolbv_mapt::map_entryt::get_value
std::string get_value(const propt &) const
Definition:
boolbv_map.cpp:19
typet
The type of an expression, extends irept.
Definition:
type.h:28
boolbv_mapt::prop
propt & prop
Definition:
boolbv_map.h:71
bvt
std::vector< literalt > bvt
Definition:
literal.h:201
boolbv_mapt::get_literals
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
Definition:
boolbv_map.cpp:41
boolbv_mapt::map_entryt::literal_map
bvt literal_map
Definition:
boolbv_map.h:31
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
boolbv_mapt::map_entryt
Definition:
boolbv_map.h:28
boolbv_mapt::mapping
mappingt mapping
Definition:
boolbv_map.h:70
boolbv_mapt::show
void show(std::ostream &out) const
Definition:
boolbv_map.cpp:35
boolbv_mapt::mappingt
std::unordered_map< irep_idt, map_entryt > mappingt
Definition:
boolbv_map.h:36
prop.h
optionalt
nonstd::optional< T > optionalt
Definition:
optional.h:35
boolbv_mapt::get_map_entry
optionalt< std::reference_wrapper< const map_entryt > > get_map_entry(const irep_idt &identifier) const
Definition:
boolbv_map.h:55
boolbv_mapt::map_entryt::type
typet type
Definition:
boolbv_map.h:30
boolbv_mapt::boolbv_mapt
boolbv_mapt(propt &_prop)
Definition:
boolbv_map.h:23
propt
TO_BE_DOCUMENTED.
Definition:
prop.h:25
boolbv_mapt
Definition:
boolbv_map.h:21
boolbv_mapt::set_literals
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition:
boolbv_map.cpp:75
solvers
flattening
boolbv_map.h
Generated by
1.8.20