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 
22 {
23 public:
24  explicit boolbv_mapt(propt &_prop) : prop(_prop)
25  {
26  }
27 
28  class map_entryt
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 
70 protected:
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
optionalt< std::reference_wrapper< const map_entryt > > get_map_entry(const irep_idt &identifier) const
Definition: boolbv_map.h:56
void erase_literals(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:118
const mappingt & get_mapping() const
Definition: boolbv_map.h:65
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:75
void show(std::ostream &out) const
Definition: boolbv_map.cpp:35
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:28
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.