Module Lattices.Congruence

The congruence lattice: abstracts integers by modular constraints of the form x ≡ a (mod n). Captures properties like even/odd or divisibility.

type t = Z.t * Z.t

val compare : (Z.t * Z.t) -> (Z.t * Z.t) -> int

val equal : (Z.t * Z.t) -> (Z.t * Z.t) -> bool

val hash : (Z.t * Z.t) -> int

val bottom : size:'a -> unit -> Z.t * Z.t

val top : size:'a -> unit -> Z.t * Z.t

val singleton : size:int -> Z.t -> Z.t * Z.t