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