jon.recoil.org

Module Ldd.MakeSource

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
Sourcetype node
Sourcetype var
Sourcemodule Name = V
Sourceval bot : node

Constructors.

Sourceval const : Axis_lattice.t -> node
Sourceval rigid : Name.t -> var
Sourceval new_var : unit -> var
Sourceval node_of_var : var -> node
Sourceval join : node -> node -> node

Boolean algebra over nodes.

Sourceval meet : node -> node -> node
Sourceval sum : 'a list -> base:node -> f:('a -> node) -> node
Sourceval sub_subsets : node -> node -> node

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

Sourceval solve_lfp : var -> node -> unit

Solving interface.

Sourceval inline_solved_vars : node -> node
Sourceval enqueue_gfp : var -> node -> unit
Sourceval solve_pending : unit -> unit
Sourceval 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.

Sourceval 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.

Sourceval round_up : node -> Axis_lattice.t
Sourceval is_const : node -> bool
Sourceval map_rigid : (Name.t -> node) -> node -> node
Sourceval pp : node -> string

Pretty printers and checks.

Sourceval pp_debug : node -> string