sig
module type S =
sig
module Graph : SHGraph.S
type ('a, 'b) manager = {
mutable bottom : Graph.vertex -> 'a;
mutable canonical : Graph.vertex -> 'a -> unit;
mutable is_bottom : Graph.vertex -> 'a -> bool;
mutable is_leq : Graph.vertex -> 'a -> 'a -> bool;
mutable join : Graph.vertex -> 'a -> 'a -> 'a;
mutable join_list : Graph.vertex -> 'a list -> 'a;
mutable widening : Graph.vertex -> 'a -> 'a -> 'a;
mutable apply : Graph.hedge -> 'a array -> 'b * 'a;
mutable arc_init : Graph.hedge -> 'b;
mutable get_init : Graph.vertex -> 'a;
mutable print_abstract : Format.formatter -> 'a -> unit;
mutable print_arc : Format.formatter -> 'b -> unit;
mutable print_vertex : Format.formatter -> Graph.vertex -> unit;
mutable print_hedge : Format.formatter -> Graph.hedge -> unit;
mutable widening_first : bool;
mutable widening_start : int;
mutable widening_freq : int;
mutable widening_descend : int;
mutable print_analysis : bool;
mutable print_step : bool;
mutable print_state : bool;
mutable print_postpre : bool;
}
type strategy_vertex = {
mutable vertex : Graph.vertex;
mutable hedges : Graph.hedge list;
mutable widen : bool;
}
type strategy = MkFixpoint.S.strategy_vertex Ilist.t
type stat = { time : float; iterations : int; descendings : int; }
type ('a, 'b) output = ('a, 'b, MkFixpoint.S.stat) Graph.t
type ('a, 'b) graph
val print_strategy_vertex :
('a, 'b) MkFixpoint.S.manager ->
Format.formatter -> MkFixpoint.S.strategy_vertex -> unit
val print_strategy :
('a, 'b) MkFixpoint.S.manager ->
Format.formatter -> MkFixpoint.S.strategy -> unit
val print_graph :
('a, 'b) MkFixpoint.S.manager ->
Format.formatter -> ('a, 'b) MkFixpoint.S.graph -> unit
val print_stat : Format.formatter -> MkFixpoint.S.stat -> unit
val print_output :
('a, 'b) MkFixpoint.S.manager ->
Format.formatter -> ('a, 'b) MkFixpoint.S.output -> unit
val init :
('a, 'b) MkFixpoint.S.manager ->
('c, 'd, 'e) Graph.t -> Graph.SetV.t -> ('a, 'b) MkFixpoint.S.graph
val fixpoint :
('a, 'b) MkFixpoint.S.manager ->
('a, 'b) MkFixpoint.S.graph -> MkFixpoint.S.strategy -> unit
val descend :
('a, 'b) MkFixpoint.S.manager ->
('a, 'b) MkFixpoint.S.graph -> MkFixpoint.S.strategy -> bool
val analysis :
('a, 'b) MkFixpoint.S.manager ->
('c, 'd, 'e) Graph.t ->
Graph.SetV.t -> MkFixpoint.S.strategy -> ('a, 'b) MkFixpoint.S.graph
val analysis_guided :
?depth:int ->
?priority:(Graph.hedge -> int) ->
?modify_strategy:(MkFixpoint.S.strategy -> MkFixpoint.S.strategy) ->
('a, 'b) MkFixpoint.S.manager ->
('c, 'd, 'e) Graph.t -> Graph.SetV.t -> ('a, 'b) MkFixpoint.S.graph
val output_of_graph :
('a, 'b) MkFixpoint.S.graph -> ('a, 'b) MkFixpoint.S.output
val strategy_default :
?depth:int ->
?priority:(Graph.hedge -> int) ->
('a, 'b, 'c) Graph.t -> Graph.SetV.t -> MkFixpoint.S.strategy
end
module Make :
functor (Graph : SHGraph.S) ->
sig
module Graph :
sig
type vertex = Graph.vertex
type hedge = Graph.hedge
module SetV :
sig
type elt = vertex
type t = Graph.SetV.t
module Ord : sig type t = elt val compare : t -> t -> int end
val repr : t -> elt Sette.tzz
val obj : elt Sette.tzz -> t
val splitzz :
elt ->
elt Sette.tzz -> elt Sette.tzz * bool * elt Sette.tzz
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val max_elt : t -> elt
val choose : t -> elt
val print :
?first:(unit, Format.formatter, unit) format ->
?sep:(unit, Format.formatter, unit) format ->
?last:(unit, Format.formatter, unit) format ->
(Format.formatter -> elt -> unit) ->
Format.formatter -> t -> unit
end
module SetH :
sig
type elt = hedge
type t = Graph.SetH.t
module Ord : sig type t = elt val compare : t -> t -> int end
val repr : t -> elt Sette.tzz
val obj : elt Sette.tzz -> t
val splitzz :
elt ->
elt Sette.tzz -> elt Sette.tzz * bool * elt Sette.tzz
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val max_elt : t -> elt
val choose : t -> elt
val print :
?first:(unit, Format.formatter, unit) format ->
?sep:(unit, Format.formatter, unit) format ->
?last:(unit, Format.formatter, unit) format ->
(Format.formatter -> elt -> unit) ->
Format.formatter -> t -> unit
end
type ('a, 'b, 'c) t = ('a, 'b, 'c) Graph.t
val create : int -> 'a -> ('b, 'c, 'a) t
val clear : ('a, 'b, 'c) t -> unit
val is_empty : ('a, 'b, 'c) t -> bool
val size_vertex : ('a, 'b, 'c) t -> int
val size_hedge : ('a, 'b, 'c) t -> int
val size_edgevh : ('a, 'b, 'c) t -> int
val size_edgehv : ('a, 'b, 'c) t -> int
val size : ('a, 'b, 'c) t -> int * int * int * int
val attrvertex : ('a, 'b, 'c) t -> vertex -> 'a
val attrhedge : ('a, 'b, 'c) t -> hedge -> 'b
val info : ('a, 'b, 'c) t -> 'c
val is_vertex : ('a, 'b, 'c) t -> vertex -> bool
val is_hedge : ('a, 'b, 'c) t -> hedge -> bool
val succhedge : ('a, 'b, 'c) t -> vertex -> SetH.t
val predhedge : ('a, 'b, 'c) t -> vertex -> SetH.t
val succvertex : ('a, 'b, 'c) t -> hedge -> vertex array
val predvertex : ('a, 'b, 'c) t -> hedge -> vertex array
val succ_vertex : ('a, 'b, 'c) t -> vertex -> SetV.t
val pred_vertex : ('a, 'b, 'c) t -> vertex -> SetV.t
val add_vertex : ('a, 'b, 'c) t -> vertex -> 'a -> unit
val add_hedge :
('a, 'b, 'c) t ->
hedge -> 'b -> pred:vertex array -> succ:vertex array -> unit
val remove_vertex : ('a, 'b, 'c) t -> vertex -> unit
val remove_hedge : ('a, 'b, 'c) t -> hedge -> unit
val iter_vertex :
('a, 'b, 'c) t ->
(vertex -> 'a -> pred:SetH.t -> succ:SetH.t -> unit) -> unit
val iter_hedge :
('a, 'b, 'c) t ->
(hedge -> 'b -> pred:vertex array -> succ:vertex array -> unit) ->
unit
val fold_vertex :
('a, 'b, 'c) t ->
(vertex -> 'a -> pred:SetH.t -> succ:SetH.t -> 'd -> 'd) ->
'd -> 'd
val fold_hedge :
('a, 'b, 'c) t ->
(hedge ->
'b -> pred:vertex array -> succ:vertex array -> 'd -> 'd) ->
'd -> 'd
val map :
('a, 'b, 'c) t ->
(vertex -> 'a -> pred:SetH.t -> succ:SetH.t -> 'd) ->
(hedge -> 'b -> pred:vertex array -> succ:vertex array -> 'e) ->
('c -> 'f) -> ('d, 'e, 'f) t
val copy :
(vertex -> 'a -> 'b) ->
(hedge -> 'c -> 'd) ->
('e -> 'f) -> ('a, 'c, 'e) t -> ('b, 'd, 'f) t
val transpose :
(vertex -> 'a -> 'b) ->
(hedge -> 'c -> 'd) ->
('e -> 'f) -> ('a, 'c, 'e) t -> ('b, 'd, 'f) t
val min : ('a, 'b, 'c) t -> SetV.t
val max : ('a, 'b, 'c) t -> SetV.t
val topological_sort : ('a, 'b, 'c) t -> vertex -> vertex list
val topological_sort_multi :
('a, 'b, 'c) t -> SetV.t -> vertex list
val topological_sort_filter_multi :
('a, 'b, 'c) t -> (hedge -> bool) -> SetV.t -> vertex list
val reachable : ('a, 'b, 'c) t -> vertex -> SetV.t * SetH.t
val reachable_multi : ('a, 'b, 'c) t -> SetV.t -> SetV.t * SetH.t
val reachable_filter_multi :
('a, 'b, 'c) t -> (hedge -> bool) -> SetV.t -> SetV.t * SetH.t
val cfc : ('a, 'b, 'c) t -> vertex -> vertex list list
val cfc_multi : ('a, 'b, 'c) t -> SetV.t -> vertex list list
val cfc_filter_multi :
('a, 'b, 'c) t -> (hedge -> bool) -> SetV.t -> vertex list list
val cfc_priority_multi :
('a, 'b, 'c) t -> (hedge -> int) -> SetV.t -> vertex list list
val scfc : ('a, 'b, 'c) t -> vertex -> vertex Ilist.t
val scfc_multi : ('a, 'b, 'c) t -> SetV.t -> vertex Ilist.t
val scfc_filter_multi :
('a, 'b, 'c) t -> (hedge -> bool) -> SetV.t -> vertex Ilist.t
val scfc_priority_multi :
('a, 'b, 'c) t -> (hedge -> int) -> SetV.t -> vertex Ilist.t
val print :
(Format.formatter -> vertex -> unit) ->
(Format.formatter -> hedge -> unit) ->
(Format.formatter -> 'a -> unit) ->
(Format.formatter -> 'b -> unit) ->
(Format.formatter -> 'c -> unit) ->
Format.formatter -> ('a, 'b, 'c) t -> unit
val print_dot :
?titlestyle:string ->
?vertexstyle:string ->
?hedgestyle:string ->
?title:string ->
(Format.formatter -> vertex -> unit) ->
(Format.formatter -> hedge -> unit) ->
(Format.formatter -> vertex -> 'a -> unit) ->
(Format.formatter -> hedge -> 'b -> unit) ->
Format.formatter -> ('a, 'b, 'c) t -> unit
end
type ('a, 'b) manager = {
mutable bottom : Graph.vertex -> 'a;
mutable canonical : Graph.vertex -> 'a -> unit;
mutable is_bottom : Graph.vertex -> 'a -> bool;
mutable is_leq : Graph.vertex -> 'a -> 'a -> bool;
mutable join : Graph.vertex -> 'a -> 'a -> 'a;
mutable join_list : Graph.vertex -> 'a list -> 'a;
mutable widening : Graph.vertex -> 'a -> 'a -> 'a;
mutable apply : Graph.hedge -> 'a array -> 'b * 'a;
mutable arc_init : Graph.hedge -> 'b;
mutable get_init : Graph.vertex -> 'a;
mutable print_abstract : Format.formatter -> 'a -> unit;
mutable print_arc : Format.formatter -> 'b -> unit;
mutable print_vertex : Format.formatter -> Graph.vertex -> unit;
mutable print_hedge : Format.formatter -> Graph.hedge -> unit;
mutable widening_first : bool;
mutable widening_start : int;
mutable widening_freq : int;
mutable widening_descend : int;
mutable print_analysis : bool;
mutable print_step : bool;
mutable print_state : bool;
mutable print_postpre : bool;
}
type strategy_vertex = {
mutable vertex : Graph.vertex;
mutable hedges : Graph.hedge list;
mutable widen : bool;
}
type strategy = strategy_vertex Ilist.t
type stat = { time : float; iterations : int; descendings : int; }
type ('a, 'b) output = ('a, 'b, stat) Graph.t
type ('a, 'b) graph
val print_strategy_vertex :
('a, 'b) manager -> Format.formatter -> strategy_vertex -> unit
val print_strategy :
('a, 'b) manager -> Format.formatter -> strategy -> unit
val print_graph :
('a, 'b) manager -> Format.formatter -> ('a, 'b) graph -> unit
val print_stat : Format.formatter -> stat -> unit
val print_output :
('a, 'b) manager -> Format.formatter -> ('a, 'b) output -> unit
val init :
('a, 'b) manager ->
('c, 'd, 'e) Graph.t -> Graph.SetV.t -> ('a, 'b) graph
val fixpoint : ('a, 'b) manager -> ('a, 'b) graph -> strategy -> unit
val descend : ('a, 'b) manager -> ('a, 'b) graph -> strategy -> bool
val analysis :
('a, 'b) manager ->
('c, 'd, 'e) Graph.t -> Graph.SetV.t -> strategy -> ('a, 'b) graph
val analysis_guided :
?depth:int ->
?priority:(Graph.hedge -> int) ->
?modify_strategy:(strategy -> strategy) ->
('a, 'b) manager ->
('c, 'd, 'e) Graph.t -> Graph.SetV.t -> ('a, 'b) graph
val output_of_graph : ('a, 'b) graph -> ('a, 'b) output
val strategy_default :
?depth:int ->
?priority:(Graph.hedge -> int) ->
('a, 'b, 'c) Graph.t -> Graph.SetV.t -> strategy
end
end