CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 <util/type.h>
14
16
17#include <functional>
18#include <iosfwd>
19
20class propt;
21
23{
24public:
26 {
27 }
28
30 {
31 public:
34
35 std::string get_value(const propt &) const;
36 };
37
38 typedef std::unordered_map<irep_idt, map_entryt> mappingt;
39
40 void show(std::ostream &out) const;
41
42 const bvt &get_literals(
43 const irep_idt &identifier,
44 const typet &type,
45 std::size_t width);
46
47 void set_literals(
48 const irep_idt &identifier,
49 const typet &type,
50 const bvt &literals);
51
52 void erase_literals(
53 const irep_idt &identifier,
54 const typet &type);
55
56 std::optional<std::reference_wrapper<const map_entryt>>
57 get_map_entry(const irep_idt &identifier) const
58 {
59 const auto entry = mapping.find(identifier);
60 if(entry == mapping.end())
61 return {};
62
63 return std::optional<std::reference_wrapper<const map_entryt>>(
64 entry->second);
65 }
66
67 const mappingt &get_mapping() const
68 {
69 return mapping;
70 }
71
72protected:
75};
76
77#endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_MAP_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
std::string get_value(const propt &) const
propt & prop
Definition boolbv_map.h:74
mappingt mapping
Definition boolbv_map.h:73
void erase_literals(const irep_idt &identifier, const typet &type)
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
void show(std::ostream &out) const
const mappingt & get_mapping() const
Definition boolbv_map.h:67
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
boolbv_mapt(propt &_prop)
Definition boolbv_map.h:25
std::optional< std::reference_wrapper< const map_entryt > > get_map_entry(const irep_idt &identifier) const
Definition boolbv_map.h:57
std::unordered_map< irep_idt, map_entryt > mappingt
Definition boolbv_map.h:38
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
TO_BE_DOCUMENTED.
Definition prop.h:25
The type of an expression, extends irept.
Definition type.h:29
std::vector< literalt > bvt
Definition literal.h:201
Defines typet, type_with_subtypet and type_with_subtypest.