Module Std.Solution

A solution to a system of fixed-point equations.

We represent the solution to a system of fixed-point equations as a pair of a finite mapping M that associates a variable (a node) with its value, and a default value, that is a value of all variables that are not in M.

type ('n, 'd) t

an abstract representation of a solution

val create : ('n, 'd, _) Core_kernel.Map.t -> 'd -> ('n, 'd) t

create constraints default creates an initial approximation of a solution. The default parameter defines the default value of all variables unspecified in the initial constraints.

  • parameter constraints

    a finite mapping from variables to their value approximations.

    For the returned value s the following is true:

    • not(is_fixpoint s)
    • iterations s = 0
    • get s x = constraints[x] if x in constraints else default
val equal : equal:('d -> 'd -> bool) -> ('n, 'd) t -> ('n, 'd) t -> bool

equal s1 s2 is true if s1 and s2 are equal solutions.

Two solutions are equal if for all x in the data domain 'd, we have that equal s1[x] s2[x].

val iterations : ('n, 'd) t -> int

iterations s returns the total number of iterations that was made to obtain the current solution.

val default : ('n, 'd) t -> 'd

default s return the default value assigned to all variables not in the internal finite mapping. This is usually a bottom or top value, depending on whether iteration increases or decreases.

val enum : ('n, 'd) t -> ('n * 'd) Core_kernel.Sequence.t

enum xs enumerates all non-trivial values in the solution.

A value is non-trivial if it differs from the default value.

val is_fixpoint : ('n, 'd) t -> bool

is_fixpoint s is true if the solution is a fixed point solution, i.e., is a solution that stabilizes the system of equations.

val get : ('n, 'd) t -> 'n -> 'd

get s x returns a value of x.

val derive : ('n, 'd) t -> f:('n -> 'd -> 'a option) -> 'a -> ('n, 'a) t

derive s ~f default creates a new solution from an old one with a new default and where for each node n in s's finite map, if f n (get s n) = Some v then n maps to v.