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:
46  map_entryt():width(0), bvtype(bvtypet::IS_UNKNOWN)
47  {
48  }
49 
50  std::size_t width;
53  literal_mapt literal_map;
54 
55  std::string get_value(const propt &) const;
56  };
57 
58  typedef std::unordered_map<irep_idt, map_entryt, irep_id_hash> mappingt;
59  mappingt mapping;
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 protected:
80  const namespacet &ns;
82 };
83 
84 #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.
Definition: type.h:20
literal_mapt literal_map
Definition: boolbv_map.h:53
propt & prop
Definition: boolbv_map.h:79
void show() const
Definition: boolbv_map.cpp:75
const namespacet & ns
Definition: boolbv_map.h:80
const boolbv_widtht & boolbv_width
Definition: boolbv_map.h:81
boolbv_mapt(propt &_prop, const namespacet &_ns, const boolbv_widtht &_boolbv_width)
Definition: boolbv_map.h:26
mappingt mapping
Definition: boolbv_map.h:59
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:121
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::vector< map_bitt > literal_mapt
Definition: boolbv_map.h:41
TO_BE_DOCUMENTED.
Definition: prop.h:22
bvtypet
Definition: boolbv_type.h:16
std::unordered_map< irep_idt, map_entryt, irep_id_hash > 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:84
std::vector< literalt > bvt
Definition: literal.h:197