cprover
smt1_conv.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: SMT Version 1 Backend
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 Revision: Roberto Bruttomesso, roberto.bruttomesso@unisi.ch
7 
8 \*******************************************************************/
9 
12 
13 #ifndef CPROVER_SOLVERS_SMT1_SMT1_CONV_H
14 #define CPROVER_SOLVERS_SMT1_SMT1_CONV_H
15 
16 #include <sstream>
17 #include <set>
18 
19 #include <util/std_expr.h>
20 
21 #include <solvers/prop/prop_conv.h>
24 
25 class byte_extract_exprt;
26 class typecast_exprt;
27 class constant_exprt;
28 class index_exprt;
29 class member_exprt;
30 
31 class smt1_convt:public prop_convt
32 {
33 public:
34  enum class solvert
35  {
36  GENERIC,
37  BOOLECTOR,
38  CVC3,
39  CVC4,
40  MATHSAT,
41  OPENSMT,
42  YICES,
43  Z3
44  };
45 
47  const namespacet &_ns,
48  const std::string &_benchmark,
49  const std::string &_source,
50  const std::string &_logic,
51  solvert _solver,
52  std::ostream &_out):
53  prop_convt(_ns),
54  benchmark(_benchmark),
55  source(_source),
56  logic(_logic),
57  solver(_solver),
58  out(_out),
59  boolbv_width(_ns),
60  pointer_logic(_ns),
61  array_index_bits(32),
63  {
64  write_header();
65  }
66 
67  virtual ~smt1_convt() { }
68  virtual resultt dec_solve();
69 
70  // overloading interfaces
71  virtual literalt convert(const exprt &expr);
72  virtual void set_to(const exprt &expr, bool value);
73  virtual exprt get(const exprt &expr) const;
74  virtual tvt l_get(literalt) const;
75  virtual std::string decision_procedure_text() const { return "SMT1"; }
76  virtual void print_assignment(std::ostream &out) const;
77 
78 protected:
79  std::string benchmark, source, logic;
81  std::ostream &out;
83 
84  void write_header();
85  void write_footer();
86 
87  // new stuff
88  void convert_expr(const exprt &expr, bool bool_as_bv);
89  void convert_type(const typet &type);
90 
91  // specific expressions go here
92  void convert_byte_update(const exprt &expr, bool bool_as_bv);
94  const byte_extract_exprt &expr,
95  bool bool_as_bv);
96  void convert_typecast(const typecast_exprt &expr, bool bool_as_bv);
97  void convert_struct(const exprt &expr);
98  void convert_union(const exprt &expr);
99  void convert_constant(const constant_exprt &expr, bool bool_as_bv);
100  void convert_relation(const exprt &expr, bool bool_as_bv);
101  void convert_is_dynamic_object(const exprt &expr, bool bool_as_bv);
102  void convert_plus(const plus_exprt &expr);
103  void convert_minus(const minus_exprt &expr);
104  void convert_div(const div_exprt &expr);
105  void convert_mult(const mult_exprt &expr);
106  void convert_floatbv_plus(const exprt &expr);
107  void convert_floatbv_minus(const exprt &expr);
108  void convert_floatbv_div(const exprt &expr);
109  void convert_floatbv_mult(const exprt &expr);
110  void convert_mod(const mod_exprt &expr);
111  void convert_index(const index_exprt &expr, bool bool_as_bv);
112  void convert_member(const member_exprt &expr, bool bool_as_bv);
113  void convert_overflow(const exprt &expr);
114  void convert_with(const exprt &expr);
115  void convert_update(const exprt &expr);
116 
117  std::string convert_identifier(const irep_idt &identifier);
118  void convert_literal(const literalt l);
119 
120  // auxiliary methods
121  std::set<irep_idt> quantified_symbols;
122  void find_symbols(const exprt &expr);
123  void find_symbols(const typet &type);
124  void find_symbols_rec(const typet &type, std::set<irep_idt> &recstack);
125  void flatten_array(const exprt &op);
126 
127  // booleans vs. bit-vector[1]
128  void from_bv_begin(const typet &type, bool bool_as_bv);
129  void from_bv_end(const typet &type, bool bool_as_bv);
130  void from_bool_begin(const typet &type, bool bool_as_bv);
131  void from_bool_end(const typet &type, bool bool_as_bv);
132 
133  // arrays
134  typet array_index_type() const;
135  void array_index(const exprt &expr);
136 
137  // pointers
140  const exprt &expr, const pointer_typet &result_type);
141 
142  // keeps track of all symbols
143  struct identifiert
144  {
147 
149  {
150  type.make_nil();
151  value.make_nil();
152  }
153  };
154 
155  void set_value(
156  identifiert &identifier,
157  const std::string &index,
158  const std::string &value)
159  {
160  exprt tmp=ce_value(identifier.type, index, value, false);
161  if(tmp.id()=="array-list" && identifier.value.id()=="array-list")
162  {
163  forall_operands(it, tmp)
164  identifier.value.copy_to_operands(*it);
165  }
166  else
167  identifier.value=tmp;
168  }
169 
170  typedef std::unordered_map<irep_idt, identifiert, irep_id_hash>
172 
174 
176 
177  // for replacing 'array_of' expressions
178  typedef std::map<exprt, irep_idt> array_of_mapt;
179  array_of_mapt array_of_map;
180 
181  // for replacing 'array' expressions
182  typedef std::map<exprt, irep_idt> array_expr_mapt;
183  array_expr_mapt array_expr_map;
184 
185  // for replacing string constants
186  typedef std::map<exprt, exprt> string2array_mapt;
187  string2array_mapt string2array_map;
188 
189  exprt ce_value(
190  const typet &type,
191  const std::string &index,
192  const std::string &v,
193  bool in_struct) const;
194 
196  const struct_typet &type,
197  const std::string &binary) const;
198 
200  const union_typet &type,
201  const std::string &binary) const;
202 
203  // flattens multi-operand expressions into binary
204  // expressions
205  void convert_nary(const exprt &expr,
206  const irep_idt op_string,
207  bool bool_as_bv);
208 
209  // Boolean part
211  std::vector<bool> boolean_assignment;
212 };
213 
214 #endif // CPROVER_SOLVERS_SMT1_SMT1_CONV_H
The type of an expression.
Definition: type.h:20
virtual void set_to(const exprt &expr, bool value)
Definition: smt1_conv.cpp:2747
void convert_overflow(const exprt &expr)
Definition: smt1_conv.cpp:2743
semantic type conversion
Definition: std_expr.h:1725
pointer_logict pointer_logic
Definition: smt1_conv.h:138
std::string source
Definition: smt1_conv.h:79
std::unordered_map< irep_idt, identifiert, irep_id_hash > identifier_mapt
Definition: smt1_conv.h:171
void convert_type(const typet &type)
Definition: smt1_conv.cpp:2916
void convert_mult(const mult_exprt &expr)
Definition: smt1_conv.cpp:2223
void convert_minus(const minus_exprt &expr)
Definition: smt1_conv.cpp:2129
void convert_expr(const exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:531
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
void write_footer()
Definition: smt1_conv.cpp:70
void convert_floatbv_minus(const exprt &expr)
Definition: smt1_conv.cpp:2168
void set_value(identifiert &identifier, const std::string &index, const std::string &value)
Definition: smt1_conv.h:155
smt1_convt(const namespacet &_ns, const std::string &_benchmark, const std::string &_source, const std::string &_logic, solvert _solver, std::ostream &_out)
Definition: smt1_conv.h:46
A constant literal expression.
Definition: std_expr.h:3685
Structure type.
Definition: std_types.h:296
std::map< exprt, irep_idt > array_expr_mapt
Definition: smt1_conv.h:182
std::string benchmark
Definition: smt1_conv.h:79
void convert_byte_extract(const byte_extract_exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:356
virtual void print_assignment(std::ostream &out) const
Definition: smt1_conv.cpp:35
void find_symbols(const exprt &expr)
Definition: smt1_conv.cpp:2789
Extract member of struct or union.
Definition: std_expr.h:3214
identifier_mapt identifier_map
Definition: smt1_conv.h:173
virtual resultt dec_solve()
Definition: smt1_conv.cpp:55
void convert_byte_update(const exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:365
const irep_idt & id() const
Definition: irep.h:189
void convert_div(const div_exprt &expr)
Definition: smt1_conv.cpp:2176
void convert_union(const exprt &expr)
Definition: smt1_conv.cpp:1775
division (integer and real)
Definition: std_expr.h:854
virtual literalt convert(const exprt &expr)
Definition: smt1_conv.cpp:442
void convert_update(const exprt &expr)
Definition: smt1_conv.cpp:2634
void convert_index(const index_exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:2642
The pointer type.
Definition: std_types.h:1343
typet array_index_type() const
Definition: smt1_conv.cpp:232
API to expression classes.
std::string logic
Definition: smt1_conv.h:79
unsigned array_index_bits
Definition: smt1_conv.h:175
Definition: threeval.h:19
std::map< exprt, irep_idt > array_of_mapt
Definition: smt1_conv.h:178
TO_BE_DOCUMENTED.
Definition: namespace.h:62
boolbv_widtht boolbv_width
Definition: smt1_conv.h:82
unsigned no_boolean_variables
Definition: smt1_conv.h:210
virtual ~smt1_convt()
Definition: smt1_conv.h:67
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:702
string2array_mapt string2array_map
Definition: smt1_conv.h:187
std::map< exprt, exprt > string2array_mapt
Definition: smt1_conv.h:186
void convert_struct(const exprt &expr)
Definition: smt1_conv.cpp:1721
std::vector< bool > boolean_assignment
Definition: smt1_conv.h:211
void convert_plus(const plus_exprt &expr)
Definition: smt1_conv.cpp:2040
void convert_floatbv_plus(const exprt &expr)
Definition: smt1_conv.cpp:2121
virtual tvt l_get(literalt) const
Definition: smt1_conv.cpp:45
void from_bool_end(const typet &type, bool bool_as_bv)
Definition: smt1_conv.cpp:3017
binary multiplication
Definition: std_expr.h:806
void from_bv_begin(const typet &type, bool bool_as_bv)
Definition: smt1_conv.cpp:2996
void convert_member(const member_exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:2693
void from_bool_begin(const typet &type, bool bool_as_bv)
Definition: smt1_conv.cpp:3010
array_of_mapt array_of_map
Definition: smt1_conv.h:179
void write_header()
Definition: smt1_conv.cpp:62
void convert_floatbv_mult(const exprt &expr)
Definition: smt1_conv.cpp:2286
virtual std::string decision_procedure_text() const
Definition: smt1_conv.h:75
void convert_typecast(const typecast_exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:1340
void convert_constant(const constant_exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:1804
exprt ce_value(const typet &type, const std::string &index, const std::string &v, bool in_struct) const
Definition: smt1_conv.cpp:118
Base class for all expressions.
Definition: expr.h:46
void convert_nary(const exprt &expr, const irep_idt op_string, bool bool_as_bv)
Definition: smt1_conv.cpp:3191
The union type.
Definition: std_types.h:424
void convert_literal(const literalt l)
Definition: smt1_conv.cpp:2978
void flatten_array(const exprt &op)
Definition: smt1_conv.cpp:3144
void convert_with(const exprt &expr)
Definition: smt1_conv.cpp:2294
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
Definition: smt1_conv.cpp:3030
void make_nil()
Definition: irep.h:243
void convert_relation(const exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:1975
void convert_floatbv_div(const exprt &expr)
Definition: smt1_conv.cpp:2215
solvert solver
Definition: smt1_conv.h:80
exprt binary2struct(const struct_typet &type, const std::string &binary) const
Definition: smt1_conv.cpp:3080
void convert_mod(const mod_exprt &expr)
Definition: smt1_conv.cpp:1905
binary minus
Definition: std_expr.h:758
std::ostream & out
Definition: smt1_conv.h:81
Pointer Logic.
exprt binary2union(const union_typet &type, const std::string &binary) const
Definition: smt1_conv.cpp:3114
TO_BE_DOCUMENTED.
binary modulo
Definition: std_expr.h:902
void convert_is_dynamic_object(const exprt &expr, bool bool_as_bv)
Definition: smt1_conv.cpp:1926
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
Definition: smt1_conv.cpp:252
void from_bv_end(const typet &type, bool bool_as_bv)
Definition: smt1_conv.cpp:3003
array_expr_mapt array_expr_map
Definition: smt1_conv.h:183
std::string convert_identifier(const irep_idt &identifier)
Definition: smt1_conv.cpp:478
void array_index(const exprt &expr)
Definition: smt1_conv.cpp:239
array index operator
Definition: std_expr.h:1170
std::set< irep_idt > quantified_symbols
Definition: smt1_conv.h:121