Module Relations.XOR_RotateSource

Sourcetype (_, _) t = private
  1. | XR_Identity : ('a, 'a) t
  2. | XR_BNot : (Operator.Function_symbol.boolean, Operator.Function_symbol.boolean) t
    (*

    Boolean not

    *)
  3. | XR_XOR_rotate : {
    1. rotate : int;
    2. xor : Z.t;
    3. size : Units.In_bits.t;
    } -> (Operator.Function_symbol.bitvector, Operator.Function_symbol.bitvector) t
    (*

    On bounded integers, represents a rotation then a xor Invariant: xor fits on size bits, 0 <= rotate < size

    *)

Bitwise focused relation: xor and rotate.

Sourceval xr_identity : ('a, 'a) t
include Union_Find.Parameters.GENERIC_GROUP with type ('a, 'b) t := ('a, 'b) t
include Union_Find.Parameters.GENERIC_MONOID with type ('a, 'b) t := ('a, 'b) t
Sourceval equal : ('a, 'b) t -> ('a, 'b) t -> bool

Equality of relations

Sourceval pretty : Format.formatter -> ('a, 'b) t -> unit

Pretty printer for relations

Sourceval pretty_with_terms : (Format.formatter -> 'tl -> unit) -> 'tl -> (Format.formatter -> 'tr -> unit) -> 'tr -> Format.formatter -> ('a, 'b) t -> unit

pretty_with_terms pp_x x pp_y y rel pretty-prints the relation rel between terms x and y (respectively printed with pp_x and pp_y).

For placeholder variables, use pretty

Sourceval identity : ('a, 'a) t

The identity relation

Sourceval compose : ('b, 'c) t -> ('a, 'b) t -> ('a, 'c) t

Monoid composition, written using the functional convention compose f g is f \circ g. Should be associative, and compatible with identity:

  • For all x, G.compose x G.identity = G.compose G.identity x = x
  • For all x y z, G.compose x (G.compose y z) = G.compose (G.compose x y) z
Sourceval inverse : ('a, 'b) t -> ('b, 'a) t

Group inversion, should verify for all x: G.compose x (G.inverse x) = G.compose (G.inverse x) x = G.identity