smt-libv2.drv 11.1 KB
Newer Older
1
(* Why driver for SMTLIB2 syntax *)
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

prelude ";;; this is a prelude for smt-lib v2"

printer "smtv2"
filename "%f-%t-%g.smt2"
valid "^unsat"
unknown "^\\(unknown\\|sat\\|Fail\\)" ""
outofmemory "(error \".*out of memory\")\\|Cannot allocate memory"
timeout "interrupted by timeout"
time "why3cpulimit time : %s s"

(* À discuter *)
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_epsilon"

transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)

transformation "discriminate"
transformation "encoding_smt"

theory BuiltIn
  syntax type int   "Int"
  syntax type real  "Real"
  syntax predicate (=)  "(= %1 %2)"

  meta "encoding : kept" type int
end

theory int.Int

  prelude ";;; this is a prelude for smt-lib v2 integer arithmetic"

  syntax function zero "0"
  syntax function one  "1"

  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
45
  syntax function ( * )  "(* %1 %2)"
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
  syntax function (-_) "(- %1)"

  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc
  remove prop CommutativeGroup.Unit_def_l
  remove prop CommutativeGroup.Unit_def_r
  remove prop CommutativeGroup.Inv_def_l
  remove prop CommutativeGroup.Inv_def_r
  remove prop Assoc.Assoc
  remove prop Mul_distr_l
  remove prop Mul_distr_r
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop ZeroLessOne

end

theory real.Real

  prelude ";;; this is a prelude for smt-lib v2 real arithmetic"

  syntax function zero "0.0"
  syntax function one  "1.0"

  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
83
  syntax function ( * )  "(* %1 %2)"
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
  syntax function (/)  "(/ %1 %2)"
  syntax function (-_) "(- %1)"
  syntax function inv  "(/ 1.0 %1)"

  syntax predicate (<=) "(<= %1 %2)"
  syntax predicate (<)  "(< %1 %2)"
  syntax predicate (>=) "(>= %1 %2)"
  syntax predicate (>)  "(> %1 %2)"

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc
  remove prop CommutativeGroup.Unit_def_l
  remove prop CommutativeGroup.Unit_def_r
  remove prop CommutativeGroup.Inv_def_l
  remove prop CommutativeGroup.Inv_def_r
  remove prop Assoc.Assoc
  remove prop Mul_distr_l
  remove prop Mul_distr_r
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Inverse
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop ZeroLessOne

  meta "encoding : kept" type real

end

theory Bool
   syntax type     bool  "Bool"
   syntax function True  "true"
   syntax function False "false"
   meta "encoding : kept" type bool
end

theory bool.Bool
   syntax function andb  "(and %1 %2)"
   syntax function orb   "(or %1 %2)"
   syntax function xorb  "(xor %1 %2)"
   syntax function notb  "(not %1)"
   syntax function implb "(=> %1 %2)"
end

theory bool.Ite
  syntax function ite "(ite %1 %2 %3)"
  meta "encoding : lskept" function ite
end

(*
theory real.Truncate
  syntax function floor "(to_int %1)"
  remove prop Floor_down
  remove prop Floor_monotonic
end
*)

theory map.Map
  syntax type map "(Array %1 %2)"
  meta "encoding : lskept" function get
  meta "encoding : lskept" function set
  meta "encoding : lskept" function const

  syntax function get   "(select %1 %2)"
  syntax function set   "(store %1 %2 %3)"
(*  syntax function const "(const[%t0] %1)" *)
end

156
157
158
159
theory bitvec.BVConverter_32_64
  syntax function toBig "((_ zero_extend 32) %1)"
  syntax function toSmall "((_ extract 31 0) %1)"
end
160

161
162
163
164
theory bitvec.BVConverter_16_64
  syntax function toBig "((_ zero_extend 48) %1)"
  syntax function toSmall "((_ extract 15 0) %1)"
end
165

166
167
168
169
theory bitvec.BVConverter_8_64
  syntax function toBig "((_ zero_extend 56) %1)"
  syntax function toSmall "((_ extract 7 0) %1)"
end
170

171
172
173
174
theory bitvec.BVConverter_16_32
  syntax function toBig "((_ zero_extend 16) %1)"
  syntax function toSmall "((_ extract 15 0) %1)"
end
175

176
177
178
179
theory bitvec.BVConverter_8_32
  syntax function toBig "((_ zero_extend 24) %1)"
  syntax function toSmall "((_ extract 7 0) %1)"
end
180

181
182
183
theory bitvec.BVConverter_8_16
  syntax function toBig "((_ zero_extend 8) %1)"
  syntax function toSmall "((_ extract 7 0) %1)"
184
185
end

186
theory bv.BV32
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
  syntax type t "(_ BitVec 32)"

  syntax function zero "#x00000000"
  syntax function ones "#xFFFFFFFF"
  syntax function bw_and "(bvand %1 %2)"
  syntax function bw_or "(bvor %1 %2)"
  syntax function bw_xor "(bvxor %1 %2)"
  syntax function bw_not "(bvnot %1)"

  syntax function add "(bvadd %1 %2)"
  syntax function sub "(bvsub %1 %2)"
  syntax function neg "(bvneg %1)"
  syntax function mul "(bvmul %1 %2)"
  syntax function udiv "(bvudiv %1 %2)"
  syntax function urem "(bvurem %1 %2)"
  syntax function sdiv "(bvsdiv %1 %2)"
  syntax function srem "(bvsrem %1 %2)"
  syntax function smod "(bvsmod %1 %2)"

  syntax function rotate_left "((_ rotate_left 1) %1)"
  syntax function rotate_right "((_ rotate_right 1) %1)"

  syntax function lsr "(bvlshr %1 ((_ int2bv 32) %2))"
  syntax function lsl "(bvshl %1 ((_ int2bv 32) %2))"
  syntax function asr "(bvashr %1 ((_ int2bv 32) %2))"
  syntax function lsr_bv "(bvlshr %1 %2)"
  syntax function lsl_bv "(bvshl %1 %2)"
  syntax function asr_bv "(bvashr %1 %2)"
Clément Fumex's avatar
Clément Fumex committed
215
  syntax converter of_int_const "((_ int2bv 32) %1)"
216
  syntax predicate eq "(= %1 %2)"
217
  remove prop Extensionality
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257

  syntax predicate slt "(bvslt %1 %2)"
  syntax predicate sle "(bvsle %1 %2)"
  syntax predicate sgt "(bvsgt %1 %2)"
  syntax predicate sge "(bvsge %1 %2)"
  syntax predicate ult "(bvult %1 %2)"
  syntax predicate ule "(bvule %1 %2)"
  syntax predicate ugt "(bvugt %1 %2)"
  syntax predicate uge "(bvuge %1 %2)"
end

theory bv.BV64
  syntax type t "(_ BitVec 64)"

  syntax function zero "#x0000000000000000"
  syntax function ones "#xFFFFFFFFFFFFFFFF"
  syntax function bw_and "(bvand %1 %2)"
  syntax function bw_or "(bvor %1 %2)"
  syntax function bw_xor "(bvxor %1 %2)"
  syntax function bw_not "(bvnot %1)"

  syntax function add "(bvadd %1 %2)"
  syntax function sub "(bvsub %1 %2)"
  syntax function neg "(bvneg %1)"
  syntax function mul "(bvmul %1 %2)"
  syntax function udiv "(bvudiv %1 %2)"
  syntax function urem "(bvurem %1 %2)"
  syntax function sdiv "(bvsdiv %1 %2)"
  syntax function srem "(bvsrem %1 %2)"
  syntax function smod "(bvsmod %1 %2)"

  syntax function rotate_left "((_ rotate_left 1) %1)"
  syntax function rotate_right "((_ rotate_right 1) %1)"

  syntax function lsr "(bvlshr %1 ((_ int2bv 64) %2))"
  syntax function lsl "(bvshl %1 ((_ int2bv 64) %2))"
  syntax function asr "(bvashr %1 ((_ int2bv 64) %2))"
  syntax function lsr_bv "(bvlshr %1 %2)"
  syntax function lsl_bv "(bvshl %1 %2)"
  syntax function asr_bv "(bvashr %1 %2)"
Clément Fumex's avatar
Clément Fumex committed
258
  syntax converter of_int_const "((_ int2bv 64) %1)"
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
  syntax predicate eq "(= %1 %2)"

  syntax predicate slt "(bvslt %1 %2)"
  syntax predicate sle "(bvsle %1 %2)"
  syntax predicate sgt "(bvsgt %1 %2)"
  syntax predicate sge "(bvsge %1 %2)"
  syntax predicate ult "(bvult %1 %2)"
  syntax predicate ule "(bvule %1 %2)"
  syntax predicate ugt "(bvugt %1 %2)"
  syntax predicate uge "(bvuge %1 %2)"
end

theory bv.BV16
  syntax type t "(_ BitVec 16)"

  syntax function zero "#x0000"
  syntax function ones "#xFFFF"
  syntax function bw_and "(bvand %1 %2)"
  syntax function bw_or "(bvor %1 %2)"
  syntax function bw_xor "(bvxor %1 %2)"
  syntax function bw_not "(bvnot %1)"

  syntax function add "(bvadd %1 %2)"
  syntax function sub "(bvsub %1 %2)"
  syntax function neg "(bvneg %1)"
  syntax function mul "(bvmul %1 %2)"
  syntax function udiv "(bvudiv %1 %2)"
  syntax function urem "(bvurem %1 %2)"
  syntax function sdiv "(bvsdiv %1 %2)"
  syntax function srem "(bvsrem %1 %2)"
  syntax function smod "(bvsmod %1 %2)"

  syntax function rotate_left "((_ rotate_left 1) %1)"
  syntax function rotate_right "((_ rotate_right 1) %1)"

  syntax function lsr "(bvlshr %1 ((_ int2bv 16) %2))"
  syntax function lsl "(bvshl %1 ((_ int2bv 16) %2))"
  syntax function asr "(bvashr %1 ((_ int2bv 16) %2))"
  syntax function lsr_bv "(bvlshr %1 %2)"
  syntax function lsl_bv "(bvshl %1 %2)"
  syntax function asr_bv "(bvashr %1 %2)"
Clément Fumex's avatar
Clément Fumex committed
300
  syntax converter of_int_const "((_ int2bv 16) %1)"
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
  syntax predicate eq "(= %1 %2)"

  syntax predicate slt "(bvslt %1 %2)"
  syntax predicate sle "(bvsle %1 %2)"
  syntax predicate sgt "(bvsgt %1 %2)"
  syntax predicate sge "(bvsge %1 %2)"
  syntax predicate ult "(bvult %1 %2)"
  syntax predicate ule "(bvule %1 %2)"
  syntax predicate ugt "(bvugt %1 %2)"
  syntax predicate uge "(bvuge %1 %2)"
end

theory bv.BV8
  syntax type t "(_ BitVec 8)"

  syntax function zero "#x00"
  syntax function ones "#xFF"
  syntax function bw_and "(bvand %1 %2)"
  syntax function bw_or "(bvor %1 %2)"
  syntax function bw_xor "(bvxor %1 %2)"
  syntax function bw_not "(bvnot %1)"

  syntax function add "(bvadd %1 %2)"
  syntax function sub "(bvsub %1 %2)"
  syntax function neg "(bvneg %1)"
  syntax function mul "(bvmul %1 %2)"
  syntax function udiv "(bvudiv %1 %2)"
  syntax function urem "(bvurem %1 %2)"
  syntax function sdiv "(bvsdiv %1 %2)"
  syntax function srem "(bvsrem %1 %2)"
  syntax function smod "(bvsmod %1 %2)"

  syntax function rotate_left "((_ rotate_left 1) %1)"
  syntax function rotate_right "((_ rotate_right 1) %1)"

  syntax function lsr "(bvlshr %1 ((_ int2bv 8) %2))"
  syntax function lsl "(bvshl %1 ((_ int2bv 8) %2))"
  syntax function asr "(bvashr %1 ((_ int2bv 8) %2))"
  syntax function lsr_bv "(bvlshr %1 %2)"
  syntax function lsl_bv "(bvshl %1 %2)"
  syntax function asr_bv "(bvashr %1 %2)"
Clément Fumex's avatar
Clément Fumex committed
342
  syntax converter of_int_const "((_ int2bv 8) %1)"
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
  syntax predicate eq "(= %1 %2)"

  syntax predicate slt "(bvslt %1 %2)"
  syntax predicate sle "(bvsle %1 %2)"
  syntax predicate sgt "(bvsgt %1 %2)"
  syntax predicate sge "(bvsge %1 %2)"
  syntax predicate ult "(bvult %1 %2)"
  syntax predicate ule "(bvule %1 %2)"
  syntax predicate ugt "(bvugt %1 %2)"
  syntax predicate uge "(bvuge %1 %2)"
end

theory bv.BVConverter_32_64
  syntax function toBig "((_ zero_extend 32) %1)"
  syntax function toSmall "((_ extract 31 0) %1)"

  remove prop back_from_bigBV
end

theory bv.BVConverter_16_64
  syntax function toBig "((_ zero_extend 48) %1)"
  syntax function toSmall "((_ extract 15 0) %1)"

  remove prop back_from_bigBV
end

theory bv.BVConverter_8_64
370
  syntax function toBig "((_ zero_extend 56) %1)"
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
  syntax function toSmall "((_ extract 7 0) %1)"

  remove prop back_from_bigBV
end

theory bv.BVConverter_16_32
  syntax function toBig "((_ zero_extend 16) %1)"
  syntax function toSmall "((_ extract 15 0) %1)"

  remove prop back_from_bigBV
end

theory bv.BVConverter_8_32
  syntax function toBig "((_ zero_extend 24) %1)"
  syntax function toSmall "((_ extract 7 0) %1)"

  remove prop back_from_bigBV
end

theory bv.BVConverter_8_16
  syntax function toBig "((_ zero_extend 8) %1)"
  syntax function toSmall "((_ extract 7 0) %1)"

  remove prop back_from_bigBV
end