Module `Types.Ldd`

type node

type var

module Name = Rigid_name

val bot : node

Constructors.

val const : Axis_lattice.t -> node

val rigid : Name.t -> var

val new_var : unit -> var

val node_of_var : var -> node

val join : node -> node -> node

Boolean algebra over nodes.

val meet : node -> node -> node

val sum : 'a list -> base:node -> f:('a -> node) -> node

val sub_subsets : node -> node -> node

sub_subsets a b computes co-Heyting subtraction (a - b) for LDDs.

val solve_lfp : var -> node -> unit

Solving interface.

val inline_solved_vars : node -> node

val enqueue_gfp : var -> node -> unit

val solve_pending : unit -> unit

val decompose_into_linear_terms : universe:var list -> node -> node * node list

decompose_into_linear_terms ~universe n returns a base term and a list of linear coefficients, one per variable in universe.

val leq_with_reason : node -> node -> Jkind_axis.Axis.packed list

If a ⊑ b fails, return witness axes where they differ. Empty list means a ⊑ b succeeds. Non-empty list is the witness axes where it fails.

val round_up : node -> Axis_lattice.t

val is_const : node -> bool

val map_rigid : (Name.t -> node) -> node -> node

val pp : node -> string

Pretty printers and checks.

val pp_debug : node -> string

Module Types.Ldd