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 <vector>
14 
15 #include <util/type.h>
16 #include <util/namespace.h>
17 
18 #include <solvers/prop/prop.h>
19 
20 #include "boolbv_type.h"
21 #include "boolbv_width.h"
22 
24 {
25 public:
27  propt &_prop,
28  const namespacet &_ns,
29  const boolbv_widtht &_boolbv_width):
30  prop(_prop), ns(_ns), boolbv_width(_boolbv_width)
31  {
32  }
33 
34  struct map_bitt
35  {
36  map_bitt():is_set(false) { }
37  bool is_set;
39  };
40 
41  typedef std::vector<map_bitt> literal_mapt;
42 
43  class map_entryt
44  {
45  public:
47  {
48  }
49 
50  std::size_t width;
54 
55  std::string get_value(const propt &) const;
56  };
57 
58  typedef std::unordered_map<irep_idt, map_entryt> mappingt;
60 
61  void show() const;
62 
64  const irep_idt &identifier,
65  const typet &type);
66 
67  void get_literals(
68  const irep_idt &identifier,
69  const typet &type,
70  const std::size_t width,
71  bvt &literals);
72 
73  void set_literals(
74  const irep_idt &identifier,
75  const typet &type,
76  const bvt &literals);
77 
78  void erase_literals(
79  const irep_idt &identifier,
80  const typet &type);
81 
82 protected:
84  const namespacet &ns;
86 };
87 
88 #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_MAP_H
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:49
The type of an expression, extends irept.
Definition: type.h:27
literal_mapt literal_map
Definition: boolbv_map.h:53
propt & prop
Definition: boolbv_map.h:83
void show() const
Definition: boolbv_map.cpp:77
const namespacet & ns
Definition: boolbv_map.h:84
const boolbv_widtht & boolbv_width
Definition: boolbv_map.h:85
boolbv_mapt(propt &_prop, const namespacet &_ns, const boolbv_widtht &_boolbv_width)
Definition: boolbv_map.h:26
mappingt mapping
Definition: boolbv_map.h:59
std::string get_value(const propt &) const
Definition: boolbv_map.cpp:21
void erase_literals(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:158
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:126
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
std::vector< map_bitt > literal_mapt
Definition: boolbv_map.h:41
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
TO_BE_DOCUMENTED.
Definition: prop.h:24
bvtypet
Definition: boolbv_type.h:16
std::unordered_map< irep_idt, map_entryt > mappingt
Definition: boolbv_map.h:58
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
Definition: boolbv_map.cpp:86
std::vector< literalt > bvt
Definition: literal.h:200
Defines typet, type_with_subtypet and type_with_subtypest.