drivers/cvc4_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_int *)
   3
   4 theory bv.BV_Gen
   5   syntax function to_uint "(bv2nat %1)"
   6 end
   7
   8 theory bv.BV256
   9   (* mapping of_int to int2bv is disabled because it breaks proofs
  10      in examples/bitcount, examples/esterel,
  11      examples/isqrt_von_neumann, examples/rightmostbittrick,
  12      examples/bitwalker *)
  13
  14   (* syntax function of_int "((_ int2bv 256) %1)" *)
  15   syntax function t'int "(bv2nat %1)"
  16 end
  17
  18 theory bv.BV128
  19   (* syntax function of_int "((_ int2bv 128) %1)" *)
  20   syntax function t'int "(bv2nat %1)"
  21 end
  22
  23 theory bv.BV64
  24   (* syntax function of_int "((_ int2bv 64) %1)" *)
  25   syntax function t'int "(bv2nat %1)"
  26 end
  27
  28 theory bv.BV32
  29   (* syntax function of_int "((_ int2bv 32) %1)" *)
  30   syntax function t'int "(bv2nat %1)"
  31 end
  32
  33 theory bv.BV16
  34   (* syntax function of_int "((_ int2bv 16) %1)" *)
  35   syntax function t'int "(bv2nat %1)"
  36 end
  37
  38 theory bv.BV8
  39   (* syntax function of_int "((_ int2bv 8) %1)" *)
  40   syntax function t'int "(bv2nat %1)"
  41 end