Functor Fixpoint.Make

module Make: 
functor (D : Domain) -> sig .. end
Parameters:
D : Domain

type var 
type system 
type fixpoint 
type f1 = D.t -> D.t 
type f2 = D.t -> D.t -> D.t 
type fn = D.t list -> D.t 
val create : unit -> system
val var : system -> var
val add : system -> var -> var -> unit
add x y requires x >= y
val add0 : system -> var -> D.t -> unit
add0 x d requires x >= d
val add1 : system ->
var -> f1 -> var -> unit
add x f y requires x >= f(y)
val add2 : system ->
var ->
f2 -> var -> var -> unit
add x f y z requires x >= f(y,z)
val addn : system ->
var -> fn -> var list -> unit
add x f ys requires x >= f(ys)
val fixpoint : system:system ->
root:var -> timeout:int -> fixpoint
Computes the least fixpoint solution satifying all added requirements. Chains of pure-copies (see add) are detected and optimized. Uses Bourdoncle's weak partial ordering to compute the solution. For each component, after timeout-steps of non-stable iteration, the widening operator of D is used to stabilize the computation.
val get : fixpoint -> var -> D.t