cprover
cvc_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_CVC_CVC_CONV_H
11 #define CPROVER_SOLVERS_CVC_CVC_CONV_H
12 
13 
14 #include <solvers/prop/prop_conv.h>
16 
17 class cvc_convt:public prop_convt
18 {
19 public:
20  cvc_convt(const namespacet &_ns, std::ostream &_out):
21  prop_convt(_ns),
22  out(_out),
23  pointer_logic(_ns),
25  {
26  }
27 
28  virtual ~cvc_convt() { }
29 
30  // API methods
31  virtual void set_to(const exprt &expr, bool value);
32  virtual literalt convert(const exprt &expr);
33  virtual tvt l_get(literalt) const;
34  virtual void print_assignment(std::ostream &out) const;
35 
36 protected:
37  std::ostream &out;
38 
39  virtual void convert_expr(const exprt &expr);
40  virtual void convert_type(const typet &type);
41  virtual void convert_address_of_rec(const exprt &expr);
42 
45 
46  struct identifiert
47  {
50 
52  {
53  type.make_nil();
54  value.make_nil();
55  }
56  };
57 
58  typedef std::unordered_map<irep_idt, identifiert, irep_id_hash>
60 
62 
63  std::vector<bool> boolean_assignment;
64 
65 private:
66  void convert_identifier(const std::string &identifier);
67  void convert_typecast_expr(const exprt &expr);
68  void convert_binary_expr(const exprt &expr, const exprt &op);
69  void convert_struct_expr(const exprt &expr);
70  void convert_constant_expr(const exprt &expr);
71  void convert_equality_expr(const exprt &expr);
72  void convert_comparison_expr(const exprt &expr);
73  void convert_plus_expr(const exprt &expr);
74  void convert_minus_expr(const exprt &expr);
75  void convert_with_expr(const exprt &expr);
76  void convert_literal(const literalt l);
77  void find_symbols(const exprt &expr);
78  void find_symbols(const typet &type);
79  void convert_array_value(const exprt &expr);
80  void convert_as_bv(const exprt &expr);
81  void convert_array_index(const exprt &expr);
82  static typet gen_array_index_type();
83  static std::string bin_zero(unsigned bits);
84  static std::string array_index_type();
85  static std::string array_index(unsigned i);
86  static std::string cvc_pointer_type();
87 };
88 
89 #endif // CPROVER_SOLVERS_CVC_CVC_CONV_H
cvc_convt(const namespacet &_ns, std::ostream &_out)
Definition: cvc_conv.h:20
void convert_minus_expr(const exprt &expr)
Definition: cvc_conv.cpp:407
The type of an expression.
Definition: type.h:20
void convert_comparison_expr(const exprt &expr)
Definition: cvc_conv.cpp:360
void convert_binary_expr(const exprt &expr, const exprt &op)
Definition: cvc_conv.cpp:45
void convert_plus_expr(const exprt &expr)
Definition: cvc_conv.cpp:210
std::ostream & out
Definition: cvc_conv.h:37
virtual void convert_address_of_rec(const exprt &expr)
Definition: cvc_conv.cpp:541
static std::string array_index(unsigned i)
Definition: cvc_conv.cpp:522
void convert_constant_expr(const exprt &expr)
Definition: cvc_conv.cpp:126
static std::string bin_zero(unsigned bits)
Definition: cvc_conv.cpp:490
Definition: threeval.h:19
virtual literalt convert(const exprt &expr)
Definition: cvc_conv.cpp:627
void convert_literal(const literalt l)
Definition: cvc_conv.cpp:474
TO_BE_DOCUMENTED.
Definition: namespace.h:62
identifier_mapt identifier_map
Definition: cvc_conv.h:61
void convert_with_expr(const exprt &expr)
Definition: cvc_conv.cpp:431
virtual void print_assignment(std::ostream &out) const
Definition: cvc_conv.cpp:25
static typet gen_array_index_type()
Definition: cvc_conv.cpp:515
static std::string cvc_pointer_type()
Definition: cvc_conv.cpp:502
void convert_array_value(const exprt &expr)
Definition: cvc_conv.cpp:719
void convert_as_bv(const exprt &expr)
Definition: cvc_conv.cpp:700
void convert_identifier(const std::string &identifier)
Definition: cvc_conv.cpp:664
std::unordered_map< irep_idt, identifiert, irep_id_hash > identifier_mapt
Definition: cvc_conv.h:59
void convert_equality_expr(const exprt &expr)
Definition: cvc_conv.cpp:330
virtual void convert_type(const typet &type)
Definition: cvc_conv.cpp:1270
Base class for all expressions.
Definition: expr.h:46
void convert_struct_expr(const exprt &expr)
Definition: cvc_conv.cpp:304
virtual tvt l_get(literalt) const
Definition: cvc_conv.cpp:35
std::vector< bool > boolean_assignment
Definition: cvc_conv.h:63
unsigned no_boolean_variables
Definition: cvc_conv.h:44
void make_nil()
Definition: irep.h:243
static std::string array_index_type()
Definition: cvc_conv.cpp:509
virtual ~cvc_convt()
Definition: cvc_conv.h:28
void find_symbols(const exprt &expr)
Definition: cvc_conv.cpp:1223
void convert_typecast_expr(const exprt &expr)
Definition: cvc_conv.cpp:266
pointer_logict pointer_logic
Definition: cvc_conv.h:43
Pointer Logic.
void convert_array_index(const exprt &expr)
Definition: cvc_conv.cpp:527
virtual void set_to(const exprt &expr, bool value)
Definition: cvc_conv.cpp:1162
virtual void convert_expr(const exprt &expr)
Definition: cvc_conv.cpp:724