jon.recoil.org

Module Ldd.Make

Lattice polynomial terms built from joins, meets, constants, and variables. The interface supports least and greatest fixpoint solving over these terms.

Parameters

module V : Ordered

Signature

include Ldd_intf.S with module Name = V
type node
type var
module Name = V
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