Functor Fixpoint.Make

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

type var = int 
type sem = 
| F0 of D.t
| F1 of int * (D.t -> D.t)
| F2 of int * int * (D.t -> D.t -> D.t)
| Fn of int list * (D.t list -> D.t)
type system = rules Vector.t 
type rules = {
   mutable join : var list;
   mutable fct : sem list;
}
type f1 = D.t -> D.t 
type f2 = D.t -> D.t -> D.t 
type fn = D.t list -> D.t 
val add : rules Vector.t -> int -> var -> unit
add x y requires x >= y
val map : ('a -> 'b) -> 'a list -> 'b list
val create : unit -> 'a Vector.t
val var : rules Vector.t -> int
val add : rules Vector.t -> int -> var -> unit
add x y requires x >= y
val adds : rules Vector.t -> int -> sem -> unit
val add0 : rules Vector.t -> int -> D.t -> unit
add0 x d requires x >= d
val add1 : rules Vector.t -> int -> (D.t -> D.t) -> int -> unit
add x f y requires x >= f(y)
val add2 : rules Vector.t ->
int -> (D.t -> D.t -> D.t) -> int -> int -> unit
add x f y z requires x >= f(y,z)
val addn : rules Vector.t -> int -> (D.t list -> D.t) -> int list -> unit
add x f ys requires x >= f(ys)
type strategy = {
   root : int;
   sys : system;
   var : int array;
   dom : D.t array;
}
val visit : rules Vector.t ->
var array -> var -> var
val visit_k : rules Vector.t ->
var array -> var -> rules -> unit
val visit_r : rules Vector.t ->
var array ->
var -> rules -> var
val id : int array -> int -> int
val depend : int array -> 'a list array -> 'a -> int -> int
val fmap : (int -> int) -> sem -> sem
val sem : D.t array -> sem -> D.t
val update : rules Vector.t * D.t array * 'a -> int -> unit
val widen : rules Vector.t * D.t array * 'a -> level:'a -> int -> bool
type fixpoint = D.t array 
val get : 'a array -> int -> 'a
val fixpoint : system:rules Vector.t ->
root:var -> timeout:int -> D.t array
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.