Source file `ldd_intf.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
(**************************************************************************)
(*                                                                        *)
(*                                 OCaml                                  *)
(*                                                                        *)
(*                  Jules Jacobs, Jane Street                             *)
(*                                                                        *)
(*   Copyright 2025 Jane Street Group LLC                                 *)
(*                                                                        *)
(*   All rights reserved.  This file is distributed under the terms of    *)
(*   the GNU Lesser General Public License version 2.1, with the          *)
(*   special exception on linking described in the file LICENSE.          *)
(*                                                                        *)
(**************************************************************************)

module type Ordered = sig
  type t

  val compare : t -> t -> int

  val to_string : t -> string
end

(** Lattice polynomial terms built from joins, meets, constants, and
    variables. The interface supports least and greatest fixpoint solving
    over these terms. *)
module type S = sig
  type node

  type var

  module Name : Ordered

  (** Constructors. *)
  val bot : node

  val const : Axis_lattice.t -> node

  val rigid : Name.t -> var

  val new_var : unit -> var

  val node_of_var : var -> node

  (** Boolean algebra over nodes. *)
  val join : node -> node -> node

  val meet : node -> node -> node

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

  (** [sub_subsets a b] computes co-Heyting subtraction (a - b) for LDDs. *)
  val sub_subsets : node -> node -> node

  (** Solving interface. *)
  val solve_lfp : var -> node -> unit

  val inline_solved_vars : node -> node

  val enqueue_gfp : var -> node -> unit

  val solve_pending : unit -> unit

  (** [decompose_into_linear_terms ~universe n] returns a base term and a list
      of linear coefficients, one per variable in [universe]. *)
  val decompose_into_linear_terms :
    universe:var list -> node -> node * node 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 leq_with_reason :
    node -> node -> Jkind_axis.Axis.packed list

  val round_up : node -> Axis_lattice.t

  val is_const : node -> bool

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

  (** Pretty printers and checks. *)
  val pp : node -> string

  val pp_debug : node -> string
end
Source file ldd_intf.ml

Source file `ldd_intf.ml`
