2024-01-17 13:59:05 +01:00
|
|
|
(** ZKey *)
|
|
|
|
|
|
|
|
(*
|
|
|
|
* Encodes the powers of x, y, z in a compact form, suitable for being
|
|
|
|
* used as keys in a hash table.
|
|
|
|
*
|
|
|
|
* Internally, the ~Zkey.t~ is made of two integers, ~left~ and ~right~.
|
|
|
|
* The small integers x, y and z are stored compactly in this 126-bits
|
|
|
|
* space:
|
|
|
|
*
|
|
|
|
* Example:
|
|
|
|
* Left Right
|
|
|
|
* 3 [--------------------------------------------------------------] [------------------|---------------|---------------|---------------]
|
|
|
|
* x y z
|
|
|
|
*
|
|
|
|
* 6 [--------------------------------------------------------------] [---|----------|----------|----------|----------|----------|---------]
|
|
|
|
* x1 y1 z1 x2 y2 z2
|
|
|
|
*
|
|
|
|
* 9 [---------------------------------|----------|----------|---------] [---|----------|----------|----------|----------|----------|---------]
|
|
|
|
* x1 y1 z1 x2 y2 z2 x3 y3 z3
|
|
|
|
*
|
|
|
|
* 12 [---|----------|----------|----------|----------|----------|---------] [---|----------|----------|----------|----------|----------|---------]
|
|
|
|
* x1 y1 z1 x2 y2 z2 x3 y3 z3 x4 y4 z4
|
|
|
|
*
|
|
|
|
*
|
|
|
|
* The values of x,y,z should be positive and should not exceed 32767 for
|
|
|
|
* ~kind=3~. For all other kinds kinds the values should not exceed 1023.
|
|
|
|
*
|
|
|
|
*)
|
|
|
|
|
|
|
|
(** Types *)
|
|
|
|
|
|
|
|
type t =
|
2018-02-14 19:23:23 +01:00
|
|
|
{
|
2018-03-13 18:24:00 +01:00
|
|
|
mutable left : int;
|
|
|
|
mutable right : int;
|
2018-02-25 01:40:12 +01:00
|
|
|
kind : int ;
|
2018-02-14 19:23:23 +01:00
|
|
|
}
|
|
|
|
|
2020-12-28 01:08:55 +01:00
|
|
|
open Powers
|
|
|
|
|
2024-01-17 13:59:05 +01:00
|
|
|
type kind =
|
2020-12-28 01:08:55 +01:00
|
|
|
| Three of Powers.t
|
|
|
|
| Four of (int * int * int * int)
|
|
|
|
| Six of (Powers.t * Powers.t)
|
|
|
|
| Nine of (Powers.t * Powers.t * Powers.t)
|
|
|
|
| Twelve of (Powers.t * Powers.t * Powers.t * Powers.t)
|
|
|
|
|
|
|
|
|
2018-03-03 21:19:50 +01:00
|
|
|
(** Creates a Zkey. *)
|
|
|
|
let make ~kind right =
|
2018-02-25 01:40:12 +01:00
|
|
|
{ left = 0 ; right ; kind }
|
2018-02-14 19:23:23 +01:00
|
|
|
|
2018-03-03 21:19:50 +01:00
|
|
|
(** Move [right] to [left] and set [right = x] *)
|
2024-01-17 13:59:05 +01:00
|
|
|
let (<|) z x =
|
2018-02-25 01:40:12 +01:00
|
|
|
z.left <- z.right;
|
|
|
|
z.right <- x;
|
|
|
|
z
|
2018-01-22 23:19:24 +01:00
|
|
|
|
2018-03-03 21:19:50 +01:00
|
|
|
(** Shift left [right] by 10 bits, and add [x]. *)
|
2024-01-17 13:59:05 +01:00
|
|
|
let (<<) z x =
|
2018-02-25 01:40:12 +01:00
|
|
|
z.right <- (z.right lsl 10) lor x ;
|
|
|
|
z
|
2018-01-17 18:19:38 +01:00
|
|
|
|
2018-03-03 21:19:50 +01:00
|
|
|
(** Shift left [right] by 10 bits, and add [x]. *)
|
2024-01-17 13:59:05 +01:00
|
|
|
let (<+) z x =
|
2018-02-25 01:40:12 +01:00
|
|
|
z.right <- (z.right lsl 15) lor x ;
|
|
|
|
z
|
2018-01-17 18:19:38 +01:00
|
|
|
|
|
|
|
|
2018-03-09 00:08:12 +01:00
|
|
|
let of_powers_three { x=a ; y=b ; z=c ; _ } =
|
|
|
|
assert (
|
|
|
|
let alpha = a lor b lor c in
|
|
|
|
alpha >= 0 && alpha < (1 lsl 15)
|
|
|
|
);
|
2020-09-26 12:02:53 +02:00
|
|
|
make ~kind:3 a <+ b <+ c
|
2018-02-22 01:38:47 +01:00
|
|
|
|
2020-12-28 01:08:55 +01:00
|
|
|
|
2018-06-29 16:04:40 +02:00
|
|
|
let of_int_four i j k l =
|
|
|
|
assert (
|
|
|
|
let alpha = i lor j lor k lor l in
|
|
|
|
alpha >= 0 && alpha < (1 lsl 15)
|
|
|
|
);
|
2020-09-26 12:02:53 +02:00
|
|
|
make ~kind:4 i <+ j <+ k <+ l
|
2018-06-29 16:04:40 +02:00
|
|
|
|
2020-12-28 01:08:55 +01:00
|
|
|
|
2018-02-22 01:38:47 +01:00
|
|
|
let of_powers_six { x=a ; y=b ; z=c ; _ } { x=d ; y=e ; z=f ; _ } =
|
2018-03-09 00:08:12 +01:00
|
|
|
assert (
|
|
|
|
let alpha = a lor b lor c lor d lor e lor f in
|
2024-01-17 13:59:05 +01:00
|
|
|
alpha >= 0 && alpha < (1 lsl 10)
|
2018-03-09 00:08:12 +01:00
|
|
|
);
|
2024-01-17 13:59:05 +01:00
|
|
|
make ~kind:6 a << b << c << d << e << f
|
2018-02-22 01:38:47 +01:00
|
|
|
|
2020-12-28 01:08:55 +01:00
|
|
|
|
2018-02-22 01:38:47 +01:00
|
|
|
let of_powers_nine { x=a ; y=b ; z=c ; _ } { x=d ; y=e ; z=f ; _ }
|
2024-01-17 13:59:05 +01:00
|
|
|
{ x=g ; y=h ; z=i ; _ } =
|
2018-03-09 00:08:12 +01:00
|
|
|
assert (
|
|
|
|
let alpha = a lor b lor c lor d lor e lor f lor g lor h lor i in
|
2024-01-17 13:59:05 +01:00
|
|
|
alpha >= 0 && alpha < (1 lsl 10)
|
2018-03-09 00:08:12 +01:00
|
|
|
);
|
2020-09-26 12:02:53 +02:00
|
|
|
make ~kind:9 a << b << c << d << e << f
|
2024-01-17 13:59:05 +01:00
|
|
|
<| g << h << i
|
2020-12-28 01:08:55 +01:00
|
|
|
|
2018-03-09 00:08:12 +01:00
|
|
|
|
|
|
|
let of_powers_twelve { x=a ; y=b ; z=c ; _ } { x=d ; y=e ; z=f ; _ }
|
2024-01-17 13:59:05 +01:00
|
|
|
{ x=g ; y=h ; z=i ; _ } { x=j ; y=k ; z=l ; _ } =
|
2018-03-09 00:08:12 +01:00
|
|
|
assert (
|
|
|
|
let alpha = a lor b lor c lor d lor e lor f
|
2020-12-28 01:08:55 +01:00
|
|
|
lor g lor h lor i lor j lor k lor l
|
2018-03-09 00:08:12 +01:00
|
|
|
in
|
2024-01-17 13:59:05 +01:00
|
|
|
alpha >= 0 && alpha < (1 lsl 10)
|
2018-03-09 00:08:12 +01:00
|
|
|
);
|
2020-09-26 12:02:53 +02:00
|
|
|
make ~kind:12 a << b << c << d << e << f
|
2020-12-28 01:08:55 +01:00
|
|
|
<| g << h << i << j << k << l
|
2018-02-22 01:38:47 +01:00
|
|
|
|
|
|
|
|
2024-01-17 13:59:05 +01:00
|
|
|
let of_powers a =
|
2018-01-19 20:20:19 +01:00
|
|
|
match a with
|
2018-02-25 01:40:12 +01:00
|
|
|
| Three a -> of_powers_three a
|
|
|
|
| Six (a,b) -> of_powers_six a b
|
|
|
|
| Twelve (a,b,c,d) -> of_powers_twelve a b c d
|
|
|
|
| Nine (a,b,c) -> of_powers_nine a b c
|
2018-06-29 16:04:40 +02:00
|
|
|
| _ -> invalid_arg "of_powers"
|
2018-02-14 19:23:23 +01:00
|
|
|
|
2018-01-19 20:20:19 +01:00
|
|
|
|
2018-02-14 19:23:23 +01:00
|
|
|
let mask10 = 0x3ff
|
|
|
|
and mask15 = 0x7fff
|
2018-01-19 20:20:19 +01:00
|
|
|
|
2018-02-25 01:40:12 +01:00
|
|
|
|
2018-06-29 16:04:40 +02:00
|
|
|
let of_int_array = function
|
2020-12-28 01:08:55 +01:00
|
|
|
| [| a ; b ; c ; d |] -> of_int_four a b c d
|
|
|
|
| _ -> invalid_arg "of_int_array"
|
2018-06-29 16:04:40 +02:00
|
|
|
|
|
|
|
|
2018-01-17 18:19:38 +01:00
|
|
|
(** Transform the Zkey into an int array *)
|
2024-01-17 13:59:05 +01:00
|
|
|
let to_int_array { left ; right ; kind } =
|
2018-01-17 18:19:38 +01:00
|
|
|
match kind with
|
2018-02-25 01:40:12 +01:00
|
|
|
| 3 -> [|
|
2020-12-28 01:08:55 +01:00
|
|
|
mask15 land (right lsr 30) ;
|
|
|
|
mask15 land (right lsr 15) ;
|
|
|
|
mask15 land right
|
|
|
|
|]
|
2018-02-14 19:23:23 +01:00
|
|
|
|
2018-06-29 16:04:40 +02:00
|
|
|
| 4 -> [|
|
2020-12-28 01:08:55 +01:00
|
|
|
mask15 land (right lsr 45) ;
|
|
|
|
mask15 land (right lsr 30) ;
|
|
|
|
mask15 land (right lsr 15) ;
|
|
|
|
mask15 land right
|
|
|
|
|]
|
2018-06-29 16:04:40 +02:00
|
|
|
|
2024-01-17 13:59:05 +01:00
|
|
|
| 6 -> [|
|
2020-12-28 01:08:55 +01:00
|
|
|
mask10 land (right lsr 50) ;
|
|
|
|
mask10 land (right lsr 40) ;
|
|
|
|
mask10 land (right lsr 30) ;
|
|
|
|
mask10 land (right lsr 20) ;
|
|
|
|
mask10 land (right lsr 10) ;
|
|
|
|
mask10 land right
|
|
|
|
|]
|
|
|
|
|
2018-02-25 01:40:12 +01:00
|
|
|
| 12 -> [|
|
2020-12-28 01:08:55 +01:00
|
|
|
mask10 land (left lsr 50) ;
|
|
|
|
mask10 land (left lsr 40) ;
|
|
|
|
mask10 land (left lsr 30) ;
|
|
|
|
mask10 land (left lsr 20) ;
|
|
|
|
mask10 land (left lsr 10) ;
|
|
|
|
mask10 land left ;
|
|
|
|
mask10 land (right lsr 50) ;
|
|
|
|
mask10 land (right lsr 40) ;
|
|
|
|
mask10 land (right lsr 30) ;
|
|
|
|
mask10 land (right lsr 20) ;
|
|
|
|
mask10 land (right lsr 10) ;
|
|
|
|
mask10 land right
|
|
|
|
|]
|
2018-02-14 19:23:23 +01:00
|
|
|
|
2018-02-25 01:40:12 +01:00
|
|
|
| 9 -> [|
|
2020-12-28 01:08:55 +01:00
|
|
|
mask10 land (left lsr 20) ;
|
|
|
|
mask10 land (left lsr 10) ;
|
|
|
|
mask10 land left ;
|
|
|
|
mask10 land (right lsr 50) ;
|
|
|
|
mask10 land (right lsr 40) ;
|
|
|
|
mask10 land (right lsr 30) ;
|
|
|
|
mask10 land (right lsr 20) ;
|
|
|
|
mask10 land (right lsr 10) ;
|
|
|
|
mask10 land right
|
|
|
|
|]
|
2018-02-25 01:40:12 +01:00
|
|
|
| _ -> invalid_arg (__FILE__^": to_int_array")
|
2018-02-14 19:23:23 +01:00
|
|
|
|
2018-01-19 20:20:19 +01:00
|
|
|
|
2018-01-17 18:19:38 +01:00
|
|
|
|
2018-01-22 23:19:24 +01:00
|
|
|
(** Transform the Zkey into an int tuple *)
|
2024-01-17 13:59:05 +01:00
|
|
|
let to_powers { left ; right ; kind } =
|
2018-01-19 20:20:19 +01:00
|
|
|
match kind with
|
2018-02-25 01:40:12 +01:00
|
|
|
| 3 -> Three (Powers.of_int_tuple (
|
2020-12-28 01:08:55 +01:00
|
|
|
mask15 land (right lsr 30) ,
|
|
|
|
mask15 land (right lsr 15) ,
|
|
|
|
mask15 land right
|
|
|
|
))
|
2018-02-14 19:23:23 +01:00
|
|
|
|
2024-01-17 13:59:05 +01:00
|
|
|
| 6 -> Six (Powers.of_int_tuple
|
2020-12-28 01:08:55 +01:00
|
|
|
( mask10 land (right lsr 50) ,
|
|
|
|
mask10 land (right lsr 40) ,
|
|
|
|
mask10 land (right lsr 30)),
|
2018-02-25 01:40:12 +01:00
|
|
|
Powers.of_int_tuple
|
2020-12-28 01:08:55 +01:00
|
|
|
( mask10 land (right lsr 20) ,
|
|
|
|
mask10 land (right lsr 10) ,
|
|
|
|
mask10 land right )
|
|
|
|
)
|
|
|
|
|
2024-01-17 13:59:05 +01:00
|
|
|
| 12 -> Twelve (Powers.of_int_tuple
|
2020-12-28 01:08:55 +01:00
|
|
|
( mask10 land (left lsr 50) ,
|
|
|
|
mask10 land (left lsr 40) ,
|
|
|
|
mask10 land (left lsr 30)),
|
|
|
|
Powers.of_int_tuple
|
|
|
|
( mask10 land (left lsr 20) ,
|
|
|
|
mask10 land (left lsr 10) ,
|
|
|
|
mask10 land left ) ,
|
|
|
|
Powers.of_int_tuple
|
|
|
|
( mask10 land (right lsr 50) ,
|
|
|
|
mask10 land (right lsr 40) ,
|
|
|
|
mask10 land (right lsr 30)),
|
|
|
|
Powers.of_int_tuple
|
|
|
|
( mask10 land (right lsr 20) ,
|
|
|
|
mask10 land (right lsr 10) ,
|
|
|
|
mask10 land right )
|
|
|
|
)
|
2018-02-14 19:23:23 +01:00
|
|
|
|
2024-01-17 13:59:05 +01:00
|
|
|
| 9 -> Nine (Powers.of_int_tuple
|
2020-12-28 01:08:55 +01:00
|
|
|
( mask10 land (left lsr 20) ,
|
|
|
|
mask10 land (left lsr 10) ,
|
|
|
|
mask10 land left ) ,
|
2018-02-19 16:01:13 +01:00
|
|
|
Powers.of_int_tuple
|
2020-12-28 01:08:55 +01:00
|
|
|
( mask10 land (right lsr 50) ,
|
|
|
|
mask10 land (right lsr 40) ,
|
|
|
|
mask10 land (right lsr 30)),
|
2018-02-19 16:01:13 +01:00
|
|
|
Powers.of_int_tuple
|
2020-12-28 01:08:55 +01:00
|
|
|
( mask10 land (right lsr 20) ,
|
|
|
|
mask10 land (right lsr 10) ,
|
|
|
|
mask10 land right )
|
2018-02-14 19:23:23 +01:00
|
|
|
)
|
2018-06-29 16:04:40 +02:00
|
|
|
|
2018-02-25 01:40:12 +01:00
|
|
|
| _ -> invalid_arg (__FILE__^": to_powers")
|
2020-12-28 01:08:55 +01:00
|
|
|
|
|
|
|
|
2024-01-17 13:59:05 +01:00
|
|
|
let hash = Hashtbl.hash
|
2018-02-14 19:23:23 +01:00
|
|
|
|
|
|
|
let equal
|
2020-12-28 01:08:55 +01:00
|
|
|
{ right = r1 ; left = l1 ; kind = k1 }
|
|
|
|
{ right = r2 ; left = l2 ; kind = k2 } =
|
2018-02-25 01:40:12 +01:00
|
|
|
r1 = r2 && l1 = l2 && k1 = k2
|
2018-02-14 19:23:23 +01:00
|
|
|
|
2020-12-28 01:08:55 +01:00
|
|
|
|
2018-03-03 21:19:50 +01:00
|
|
|
let compare
|
2020-12-28 01:08:55 +01:00
|
|
|
{ right = r1 ; left = l1 ; kind = k1 }
|
|
|
|
{ right = r2 ; left = l2 ; kind = k2 } =
|
2018-02-25 01:40:12 +01:00
|
|
|
if k1 <> k2 then invalid_arg (__FILE__^": cmp");
|
2018-02-14 19:23:23 +01:00
|
|
|
if r1 < r2 then -1
|
|
|
|
else if r1 > r2 then 1
|
|
|
|
else if l1 < l2 then -1
|
|
|
|
else if l1 > l2 then 1
|
|
|
|
else 0
|
|
|
|
|
2020-12-28 01:08:55 +01:00
|
|
|
|
2018-02-25 01:40:12 +01:00
|
|
|
let to_string { left ; right ; kind } =
|
2018-02-14 19:23:23 +01:00
|
|
|
"< " ^ string_of_int left ^ string_of_int right ^ " | " ^ (
|
2020-12-28 01:08:55 +01:00
|
|
|
to_int_array { left ; right ; kind }
|
|
|
|
|> Array.map string_of_int
|
|
|
|
|> Array.to_list
|
|
|
|
|> String.concat ", "
|
2018-01-22 23:19:24 +01:00
|
|
|
) ^ " >"
|
|
|
|
|
2024-01-17 13:59:05 +01:00
|
|
|
(** Printers *)
|
2020-12-28 01:08:55 +01:00
|
|
|
let pp ppf t =
|
|
|
|
Format.fprintf ppf "@[%s@]" (to_string t)
|