cvc4_bv.gen 1.7 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 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 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
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
   have the same name for the function to_int *)
theory bv.BV64
  syntax converter of_int "(_ bv%1 64)"
  syntax function to_uint "(bv2nat %1)"
  remove prop to_uint_of_int
  remove prop to_uint_extensionality
  remove prop to_uint_bounds

  remove prop to_uint_add
  remove prop to_uint_sub
  remove prop to_uint_neg
  remove prop to_uint_mul
  remove prop to_uint_udiv
  remove prop to_uint_urem
  remove prop to_uint_lsr
  remove prop to_uint_lsl
end

theory bv.BV32
  syntax converter of_int "(_ bv%1 32)"
  syntax function to_uint "(bv2nat %1)"
  remove prop to_uint_of_int
  remove prop to_uint_extensionality
  remove prop to_uint_bounds

  remove prop to_uint_add
  remove prop to_uint_sub
  remove prop to_uint_neg
  remove prop to_uint_mul
  remove prop to_uint_udiv
  remove prop to_uint_urem
  remove prop to_uint_lsr
  remove prop to_uint_lsl
end

theory bv.BV16
  syntax converter of_int "(_ bv%1 16)"
  syntax function to_uint "(bv2nat %1)"
  remove prop to_uint_of_int
  remove prop to_uint_extensionality
  remove prop to_uint_bounds

  remove prop to_uint_add
  remove prop to_uint_sub
  remove prop to_uint_neg
  remove prop to_uint_mul
  remove prop to_uint_udiv
  remove prop to_uint_urem
  remove prop to_uint_lsr
  remove prop to_uint_lsl
end

theory bv.BV8
  syntax converter of_int "(_ bv%1 8)"
  syntax function to_uint "(bv2nat %1)"
  remove prop to_uint_of_int
  remove prop to_uint_extensionality
  remove prop to_uint_bounds

  remove prop to_uint_add
  remove prop to_uint_sub
  remove prop to_uint_neg
  remove prop to_uint_mul
  remove prop to_uint_udiv
  remove prop to_uint_urem
  remove prop to_uint_lsr
  remove prop to_uint_lsl
end