z3_bv.gen 971 Bytes
Newer Older
1
(* bitvector modules, is not in smt-libv2.gen since cvc4 and z3 don't
2 3 4 5 6 7 8
   have the same name for the function to_uint *)

theory bv.BV_Gen
   syntax function to_uint "(bv2int %1)"
end

theory bv.BV64
MARCHE Claude's avatar
MARCHE Claude committed
9 10 11 12
  (* mapping of_int to int2bv is disabled because it breaks proofs
     in examples/queens_bv, examples/bitwalker *)

  (* syntax function of_int "((_ int2bv 64) %1)" *)
13 14 15 16 17 18 19
  syntax function t'int "(bv2int %1)"

  remove prop Nth_bv_is_nth
  remove prop Nth_bv_is_nth2
end

theory bv.BV32
MARCHE Claude's avatar
MARCHE Claude committed
20
  (* syntax function of_int "((_ int2bv 32) %1)" *)
21 22 23 24 25 26 27
  syntax function t'int "(bv2int %1)"

  remove prop Nth_bv_is_nth
  remove prop Nth_bv_is_nth2
end

theory bv.BV16
MARCHE Claude's avatar
MARCHE Claude committed
28
  (* syntax function of_int "((_ int2bv 16) %1)" *)
29 30 31 32 33 34 35
  syntax function t'int "(bv2int %1)"

  remove prop Nth_bv_is_nth
  remove prop Nth_bv_is_nth2
end

theory bv.BV8
MARCHE Claude's avatar
MARCHE Claude committed
36
  (* syntax function of_int "((_ int2bv 8) %1)" *)
37 38 39 40 41
  syntax function t'int "(bv2int %1)"

  remove prop Nth_bv_is_nth
  remove prop Nth_bv_is_nth2
end