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
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