smt-libv2.drv 12.6 KB
Newer Older
1
(* Why3 driver for SMT-LIB2 syntax, excluding bit-vectors *)
2

3 4 5 6 7 8 9 10 11 12
prelude ";;; generated by SMT-LIB2 driver"

(*

Note: we do not insert any command "set-logic" because its
interpretation is specific to provers

prelude "(set-logic AUFNIRA)"

    A  : Array
13 14 15
    UF : Uninterpreted Function
    DT : Datatypes (not needed at the end ...)
    NIRA : NonLinear Integer Reals Arithmetic
16

17 18 19 20
*)

printer "smtv2"
filename "%f-%t-%g.smt2"
21
unknown "^\\(unknown\\|sat\\|Fail\\)$" ""
22
time "why3cpulimit time : %s s"
23
valid "^unsat$"
24 25 26 27 28 29 30 31 32 33 34 35


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

  meta "encoding : kept" type int
end

theory int.Int

36
  prelude ";;; SMT-LIB2: integer arithmetic"
37 38 39 40 41 42

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

  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
43
  syntax function ( * )  "(* %1 %2)"
44 45 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
  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

74
  prelude ";;; SMT-LIB2: real arithmetic"
75 76 77 78 79 80

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

  syntax function (+)  "(+ %1 %2)"
  syntax function (-)  "(- %1 %2)"
81
  syntax function ( * )  "(* %1 %2)"
82 83 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
  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

135
(* not uniformly interpreted by provers
136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153
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

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

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

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

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

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

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

184
theory bv.BV32
185 186 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
  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
213
  syntax converter of_int_const "((_ int2bv 32) %1)"
214
  syntax predicate eq "(= %1 %2)"
215
  remove prop Extensionality
216 217 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

  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
256
  syntax converter of_int_const "((_ int2bv 64) %1)"
257 258 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
  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
298
  syntax converter of_int_const "((_ int2bv 16) %1)"
299 300 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
  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
340
  syntax converter of_int_const "((_ int2bv 8) %1)"
341 342 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
  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
368
  syntax function toBig "((_ zero_extend 56) %1)"
369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393
  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
394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474

theory bitvec.Pow2int

  remove prop Power_0
  remove prop Power_s
  remove prop Power_1
  remove prop Power_sum
  remove prop pow2pos
  remove prop Div_mult_inst
  remove prop Div_double
  remove prop Div_pow
  remove prop Div_double_neg
  remove prop Div_pow2
  remove prop Div_div_pow
  remove prop Mod_pow2_gen
  remove prop pow2_0
  remove prop pow2_1
  remove prop pow2_2
  remove prop pow2_3
  remove prop pow2_4
  remove prop pow2_5
  remove prop pow2_6
  remove prop pow2_7
  remove prop pow2_8
  remove prop pow2_9
  remove prop pow2_10
  remove prop pow2_11
  remove prop pow2_12
  remove prop pow2_13
  remove prop pow2_14
  remove prop pow2_15
  remove prop pow2_16
  remove prop pow2_17
  remove prop pow2_18
  remove prop pow2_19
  remove prop pow2_20
  remove prop pow2_21
  remove prop pow2_22
  remove prop pow2_23
  remove prop pow2_24
  remove prop pow2_25
  remove prop pow2_26
  remove prop pow2_27
  remove prop pow2_28
  remove prop pow2_29
  remove prop pow2_30
  remove prop pow2_31
  remove prop pow2_32
  remove prop pow2_33
  remove prop pow2_34
  remove prop pow2_35
  remove prop pow2_36
  remove prop pow2_37
  remove prop pow2_38
  remove prop pow2_39
  remove prop pow2_40
  remove prop pow2_41
  remove prop pow2_42
  remove prop pow2_43
  remove prop pow2_44
  remove prop pow2_45
  remove prop pow2_46
  remove prop pow2_47
  remove prop pow2_48
  remove prop pow2_49
  remove prop pow2_50
  remove prop pow2_51
  remove prop pow2_52
  remove prop pow2_53
  remove prop pow2_54
  remove prop pow2_55
  remove prop pow2_56
  remove prop pow2_57
  remove prop pow2_58
  remove prop pow2_59
  remove prop pow2_60
  remove prop pow2_61
  remove prop pow2_62
  remove prop pow2_63
  remove prop pow2_64
end