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