cprover
dplib_conv.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_DPLIB_DPLIB_CONV_H
11 #define CPROVER_SOLVERS_DPLIB_DPLIB_CONV_H
12 
13 
14 #include <solvers/prop/prop_conv.h>
16 
17 #include "dplib_prop.h"
18 
19 class dplib_convt:public prop_convt
20 {
21 public:
23  const namespacet &_ns,
24  std::ostream &_out):
25  prop_convt(_ns),
26  out(_out),
27  pointer_logic(_ns) { }
28 
29  virtual ~dplib_convt() { }
30 
31 protected:
32  std::ostream &out;
33 
34  virtual literalt convert_rest(const exprt &expr);
35  virtual void convert_dplib_expr(const exprt &expr);
36  virtual void convert_dplib_type(const typet &type);
37  virtual void set_to(const exprt &expr, bool value);
38  virtual void convert_address_of_rec(const exprt &expr);
39 
41 
42 private:
43  void convert_identifier(const std::string &identifier);
44  void find_symbols(const exprt &expr);
45  void find_symbols(const typet &type);
46  void convert_array_value(const exprt &expr);
47  void convert_as_bv(const exprt &expr);
48  void convert_array_index(const exprt &expr);
49  static typet gen_array_index_type();
50  static std::string bin_zero(unsigned bits);
51  static std::string array_index_type();
52  static std::string array_index(unsigned i);
53  static std::string dplib_pointer_type();
54 
55  struct identifiert
56  {
59 
61  {
62  type.make_nil();
63  value.make_nil();
64  }
65  };
66 
67  typedef std::unordered_map<irep_idt, identifiert, irep_id_hash>
69 
71 };
72 
73 #endif // CPROVER_SOLVERS_DPLIB_DPLIB_CONV_H
static typet gen_array_index_type()
Definition: dplib_conv.cpp:44
The type of an expression.
Definition: type.h:20
void convert_as_bv(const exprt &expr)
Definition: dplib_conv.cpp:212
void find_symbols(const exprt &expr)
virtual ~dplib_convt()
Definition: dplib_conv.h:29
virtual void convert_dplib_expr(const exprt &expr)
Definition: dplib_conv.cpp:229
static std::string array_index_type()
Definition: dplib_conv.cpp:39
void convert_array_value(const exprt &expr)
Definition: dplib_conv.cpp:224
std::unordered_map< irep_idt, identifiert, irep_id_hash > identifier_mapt
Definition: dplib_conv.h:68
static std::string array_index(unsigned i)
Definition: dplib_conv.cpp:51
static std::string bin_zero(unsigned bits)
Definition: dplib_conv.cpp:24
static std::string dplib_pointer_type()
Definition: dplib_conv.cpp:32
dplib_convt(const namespacet &_ns, std::ostream &_out)
Definition: dplib_conv.h:22
std::ostream & out
Definition: dplib_conv.h:32
pointer_logict pointer_logic
Definition: dplib_conv.h:40
TO_BE_DOCUMENTED.
Definition: namespace.h:62
identifier_mapt identifier_map
Definition: dplib_conv.h:70
virtual literalt convert_rest(const exprt &expr)
Definition: dplib_conv.cpp:154
virtual void convert_dplib_type(const typet &type)
Base class for all expressions.
Definition: expr.h:46
void convert_identifier(const std::string &identifier)
Definition: dplib_conv.cpp:176
virtual void set_to(const exprt &expr, bool value)
Definition: dplib_conv.cpp:965
void make_nil()
Definition: irep.h:243
virtual void convert_address_of_rec(const exprt &expr)
Definition: dplib_conv.cpp:70
void convert_array_index(const exprt &expr)
Definition: dplib_conv.cpp:56
Pointer Logic.