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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
boolbv_mapt::erase_literals
void erase_literals(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:158
boolbv_mapt::literal_mapt
std::vector< map_bitt > literal_mapt
Definition: boolbv_map.h:41
boolbv_mapt::map_entryt::bvtype
bvtypet bvtype
Definition: boolbv_map.h:51
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:27
boolbv_mapt::prop
propt & prop
Definition: boolbv_map.h:83
bvt
std::vector< literalt > bvt
Definition: literal.h:200
boolbv_mapt::map_bitt
Definition: boolbv_map.h:34
boolbv_mapt::map_bitt::map_bitt
map_bitt()
Definition: boolbv_map.h:36
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:86
boolbv_type.h
boolbv_mapt::map_entryt::literal_map
literal_mapt literal_map
Definition: boolbv_map.h:53
boolbv_mapt::show
void show() const
Definition: boolbv_map.cpp:77
namespace.h
boolbv_mapt::ns
const namespacet & ns
Definition: boolbv_map.h:84
boolbv_mapt::map_entryt::width
std::size_t width
Definition: boolbv_map.h:50
type.h
bvtypet
bvtypet
Definition: boolbv_type.h:16
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
boolbv_mapt::map_entryt
Definition: boolbv_map.h:43
boolbv_mapt::mapping
mappingt mapping
Definition: boolbv_map.h:59
boolbv_mapt::mappingt
std::unordered_map< irep_idt, map_entryt > mappingt
Definition: boolbv_map.h:58
prop.h
boolbv_mapt::boolbv_width
const boolbv_widtht & boolbv_width
Definition: boolbv_map.h:85
boolbv_mapt::map_entryt::type
typet type
Definition: boolbv_map.h:52
boolbv_widtht
Definition: boolbv_width.h:16
propt
TO_BE_DOCUMENTED.
Definition: prop.h:24
boolbv_width.h
literalt
Definition: literal.h:24
boolbv_mapt::boolbv_mapt
boolbv_mapt(propt &_prop, const namespacet &_ns, const boolbv_widtht &_boolbv_width)
Definition: boolbv_map.h:26
boolbv_mapt
Definition: boolbv_map.h:23
boolbv_mapt::map_bitt::is_set
bool is_set
Definition: boolbv_map.h:37
boolbv_mapt::map_bitt::l
literalt l
Definition: boolbv_map.h:38
boolbv_mapt::map_entryt::map_entryt
map_entryt()
Definition: boolbv_map.h:46
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:126