drivers/z3_bv.gen

   1 (* bitvector modules, is not in smt-libv2.gen since cvc4 and z3 don't
   2    have the same name for the function to_uint *)
   3
   4 theory bv.BV_Gen
   5    syntax function to_uint "(bv2int %1)"
   6 end
   7
   8 theory bv.BV256
   9   (* mapping of_int to int2bv is disabled because it breaks proofs
  10      in examples/queens_bv, examples/bitwalker *)
  11
  12   (* syntax function of_int "((_ int2bv 256) %1)" *)
  13   syntax function t'int "(bv2int %1)"
  14
  15   remove prop Nth_bv_is_nth
  16   remove prop Nth_bv_is_nth2
  17 end
  18
  19 theory bv.BV128
  20   (* syntax function of_int "((_ int2bv 128) %1)" *)
  21   syntax function t'int "(bv2int %1)"
  22
  23   remove prop Nth_bv_is_nth
  24   remove prop Nth_bv_is_nth2
  25 end
  26
  27 theory bv.BV64
  28   (* syntax function of_int "((_ int2bv 64) %1)" *)
  29   syntax function t'int "(bv2int %1)"
  30
  31   remove prop Nth_bv_is_nth
  32   remove prop Nth_bv_is_nth2
  33 end
  34
  35 theory bv.BV32
  36   (* syntax function of_int "((_ int2bv 32) %1)" *)
  37   syntax function t'int "(bv2int %1)"
  38
  39   remove prop Nth_bv_is_nth
  40   remove prop Nth_bv_is_nth2
  41 end
  42
  43 theory bv.BV16
  44   (* syntax function of_int "((_ int2bv 16) %1)" *)
  45   syntax function t'int "(bv2int %1)"
  46
  47   remove prop Nth_bv_is_nth
  48   remove prop Nth_bv_is_nth2
  49 end
  50
  51 theory bv.BV8
  52   (* syntax function of_int "((_ int2bv 8) %1)" *)
  53   syntax function t'int "(bv2int %1)"
  54
  55   remove prop Nth_bv_is_nth
  56   remove prop Nth_bv_is_nth2
  57 end