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:
26  boolbv_mapt(propt &_prop, const boolbv_widtht &_boolbv_width)
27  : prop(_prop), boolbv_width(_boolbv_width)
28  {
29  }
30 
31  struct map_bitt
32  {
33  map_bitt():is_set(false) { }
34  bool is_set;
36  };
37 
38  typedef std::vector<map_bitt> literal_mapt;
39 
40  class map_entryt
41  {
42  public:
44  {
45  }
46 
47  std::size_t width;
51 
52  std::string get_value(const propt &) const;
53  };
54 
55  typedef std::unordered_map<irep_idt, map_entryt> mappingt;
57 
58  void show() const;
59 
61  const irep_idt &identifier,
62  const typet &type);
63 
64  void get_literals(
65  const irep_idt &identifier,
66  const typet &type,
67  const std::size_t width,
68  bvt &literals);
69 
70  void set_literals(
71  const irep_idt &identifier,
72  const typet &type,
73  const bvt &literals);
74 
75  void erase_literals(
76  const irep_idt &identifier,
77  const typet &type);
78 
79 protected:
82 };
83 
84 #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:155
boolbv_mapt::boolbv_mapt
boolbv_mapt(propt &_prop, const boolbv_widtht &_boolbv_width)
Definition: boolbv_map.h:26
boolbv_mapt::literal_mapt
std::vector< map_bitt > literal_mapt
Definition: boolbv_map.h:38
boolbv_mapt::map_entryt::bvtype
bvtypet bvtype
Definition: boolbv_map.h:48
boolbv_mapt::get_map_entry
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:49
boolbv_mapt::map_entryt::get_value
std::string get_value(const propt &) const
Definition: boolbv_map.cpp:21
typet
The type of an expression, extends irept.
Definition: type.h:29
boolbv_mapt::prop
propt & prop
Definition: boolbv_map.h:80
bvt
std::vector< literalt > bvt
Definition: literal.h:201
boolbv_mapt::map_bitt
Definition: boolbv_map.h:32
boolbv_mapt::map_bitt::map_bitt
map_bitt()
Definition: boolbv_map.h:33
boolbv_mapt::get_literals
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
Definition: boolbv_map.cpp:83
boolbv_type.h
boolbv_mapt::map_entryt::literal_map
literal_mapt literal_map
Definition: boolbv_map.h:50
boolbv_mapt::show
void show() const
Definition: boolbv_map.cpp:74
namespace.h
boolbv_mapt::map_entryt::width
std::size_t width
Definition: boolbv_map.h:47
type.h
Defines typet, type_with_subtypet and type_with_subtypest.
bvtypet
bvtypet
Definition: boolbv_type.h:17
boolbv_mapt::map_entryt
Definition: boolbv_map.h:41
boolbv_mapt::mapping
mappingt mapping
Definition: boolbv_map.h:56
boolbv_mapt::mappingt
std::unordered_map< irep_idt, map_entryt > mappingt
Definition: boolbv_map.h:55
prop.h
boolbv_mapt::boolbv_width
const boolbv_widtht & boolbv_width
Definition: boolbv_map.h:81
boolbv_mapt::map_entryt::type
typet type
Definition: boolbv_map.h:49
boolbv_widtht
Definition: boolbv_width.h:17
propt
TO_BE_DOCUMENTED.
Definition: prop.h:25
boolbv_width.h
literalt
Definition: literal.h:26
boolbv_mapt
Definition: boolbv_map.h:24
boolbv_mapt::map_bitt::is_set
bool is_set
Definition: boolbv_map.h:34
boolbv_mapt::map_bitt::l
literalt l
Definition: boolbv_map.h:35
boolbv_mapt::map_entryt::map_entryt
map_entryt()
Definition: boolbv_map.h:43
bvtypet::IS_UNKNOWN
@ IS_UNKNOWN
boolbv_mapt::set_literals
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
Definition: boolbv_map.cpp:123