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