module Make:
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