cprover
boolbv_map.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
18
19class propt;
20
22{
23public:
24 explicit boolbv_mapt(propt &_prop) : prop(_prop)
25 {
26 }
27
29 {
30 public:
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
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
63 }
64
65 const mappingt &get_mapping() const
66 {
67 return mapping;
68 }
69
70protected:
73};
74
75#endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_MAP_H
std::string get_value(const propt &) const
Definition: boolbv_map.cpp:19
propt & prop
Definition: boolbv_map.h:72
mappingt mapping
Definition: boolbv_map.h:71
void erase_literals(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:118
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:75
optionalt< std::reference_wrapper< const map_entryt > > get_map_entry(const irep_idt &identifier) const
Definition: boolbv_map.h:56
void show(std::ostream &out) const
Definition: boolbv_map.cpp:35
const mappingt & get_mapping() const
Definition: boolbv_map.h:65
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
Definition: boolbv_map.cpp:41
boolbv_mapt(propt &_prop)
Definition: boolbv_map.h:24
std::unordered_map< irep_idt, map_entryt > mappingt
Definition: boolbv_map.h:37
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
TO_BE_DOCUMENTED.
Definition: prop.h:23
The type of an expression, extends irept.
Definition: type.h:29
std::vector< literalt > bvt
Definition: literal.h:201
nonstd::optional< T > optionalt
Definition: optional.h:35
Defines typet, type_with_subtypet and type_with_subtypest.