sig
type ('a, 'b, 'c, 'd) man = {
typ : string;
man : 'c;
canonicalize : ?apron:bool -> 'c -> 'd -> unit;
size : 'c -> 'd -> int;
print :
?print_apron:((int -> string) ->
Format.formatter -> 'b Apron.Abstract0.t -> unit) ->
'a Bddapron.Env.t -> Format.formatter -> 'd -> unit;
bottom : 'c -> 'a Bddapron.Env.t -> 'd;
top : 'c -> 'a Bddapron.Env.t -> 'd;
of_apron : 'c -> 'a Bddapron.Env.t -> 'b Apron.Abstract0.t -> 'd;
of_bddapron :
'c ->
'a Bddapron.Env.t ->
('a Bddapron.Expr0.Bool.t * 'b Apron.Abstract0.t) list -> 'd;
is_bottom : 'c -> 'd -> bool;
is_top : 'c -> 'd -> bool;
is_leq : 'c -> 'd -> 'd -> bool;
is_eq : 'c -> 'd -> 'd -> bool;
to_bddapron :
'c -> 'd -> ('a Bddapron.Expr0.Bool.t * 'b Apron.Abstract0.t) list;
meet : 'c -> 'd -> 'd -> 'd;
join : 'c -> 'd -> 'd -> 'd;
meet_condition :
'c ->
'a Bddapron.Env.t ->
'a Bddapron.Cond.t -> 'd -> 'a Bddapron.Expr0.Bool.t -> 'd;
assign_lexpr :
?relational:bool ->
?nodependency:bool ->
'c ->
'a Bddapron.Env.t ->
'a Bddapron.Cond.t ->
'd -> 'a list -> 'a Bddapron.Expr0.t list -> 'd option -> 'd;
substitute_lexpr :
'c ->
'a Bddapron.Env.t ->
'a Bddapron.Cond.t ->
'd -> 'a list -> 'a Bddapron.Expr0.t list -> 'd option -> 'd;
forget_list : 'c -> 'a Bddapron.Env.t -> 'd -> 'a list -> 'd;
widening : 'c -> 'd -> 'd -> 'd;
widening_threshold : 'c -> 'd -> 'd -> Apron.Lincons0.t array -> 'd;
apply_change : bottom:'d -> 'c -> 'd -> Bddapron.Env.change -> 'd;
apply_permutation :
'c -> 'd -> int array option * Apron.Dim.perm option -> 'd;
}
type 'd t = 'd
val canonicalize :
?apron:bool ->
('a, 'b, 'c, 'd) Bddapron.Domain0.man -> 'd Bddapron.Domain0.t -> unit
val size :
('a, 'b, 'c, 'd) Bddapron.Domain0.man -> 'd Bddapron.Domain0.t -> int
val print :
?print_apron:((int -> string) ->
Format.formatter -> 'b Apron.Abstract0.t -> unit) ->
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'a Bddapron.Env.t -> Format.formatter -> 'd Bddapron.Domain0.t -> unit
val bottom :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'a Bddapron.Env.t -> 'd Bddapron.Domain0.t
val top :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'a Bddapron.Env.t -> 'd Bddapron.Domain0.t
val of_apron :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'a Bddapron.Env.t -> 'b Apron.Abstract0.t -> 'd Bddapron.Domain0.t
val of_bddapron :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'a Bddapron.Env.t ->
('a Bddapron.Expr0.Bool.t * 'b Apron.Abstract0.t) list ->
'd Bddapron.Domain0.t
val is_bottom :
('a, 'b, 'c, 'd) Bddapron.Domain0.man -> 'd Bddapron.Domain0.t -> bool
val is_top :
('a, 'b, 'c, 'd) Bddapron.Domain0.man -> 'd Bddapron.Domain0.t -> bool
val is_leq :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'd Bddapron.Domain0.t -> 'd Bddapron.Domain0.t -> bool
val is_eq :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'd Bddapron.Domain0.t -> 'd Bddapron.Domain0.t -> bool
val to_bddapron :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'd Bddapron.Domain0.t ->
('a Bddapron.Expr0.Bool.t * 'b Apron.Abstract0.t) list
val meet :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'd Bddapron.Domain0.t -> 'd Bddapron.Domain0.t -> 'd Bddapron.Domain0.t
val join :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'd Bddapron.Domain0.t -> 'd Bddapron.Domain0.t -> 'd Bddapron.Domain0.t
val meet_condition :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'a Bddapron.Env.t ->
'a Bddapron.Cond.t ->
'd Bddapron.Domain0.t ->
'a Bddapron.Expr0.Bool.t -> 'd Bddapron.Domain0.t
val assign_lexpr :
?relational:bool ->
?nodependency:bool ->
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'a Bddapron.Env.t ->
'a Bddapron.Cond.t ->
'd Bddapron.Domain0.t ->
'a list ->
'a Bddapron.Expr0.t list ->
'd Bddapron.Domain0.t option -> 'd Bddapron.Domain0.t
val substitute_lexpr :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'a Bddapron.Env.t ->
'a Bddapron.Cond.t ->
'd Bddapron.Domain0.t ->
'a list ->
'a Bddapron.Expr0.t list ->
'd Bddapron.Domain0.t option -> 'd Bddapron.Domain0.t
val forget_list :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'a Bddapron.Env.t ->
'd Bddapron.Domain0.t -> 'a list -> 'd Bddapron.Domain0.t
val widening :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'd Bddapron.Domain0.t -> 'd Bddapron.Domain0.t -> 'd Bddapron.Domain0.t
val widening_threshold :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'd Bddapron.Domain0.t ->
'd Bddapron.Domain0.t -> Apron.Lincons0.t array -> 'd Bddapron.Domain0.t
val apply_change :
bottom:'d Bddapron.Domain0.t ->
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'd Bddapron.Domain0.t -> Bddapron.Env.change -> 'd Bddapron.Domain0.t
val apply_permutation :
('a, 'b, 'c, 'd) Bddapron.Domain0.man ->
'd Bddapron.Domain0.t ->
int array option * Apron.Dim.perm option -> 'd Bddapron.Domain0.t
val man_get_apron :
('a, 'b, 'c, 'd) Bddapron.Domain0.man -> 'b Apron.Manager.t
type ('a, 'b) mtbdd =
('a, 'b, ('a, 'b) Bddapron.Mtbdddomain0.man,
'b Bddapron.Mtbdddomain0.t)
Bddapron.Domain0.man
val mtbdd_of_mtbdddomain :
('a, 'b) Bddapron.Mtbdddomain0.man -> ('a, 'b) Bddapron.Domain0.mtbdd
val make_mtbdd :
?global:bool -> 'b Apron.Manager.t -> ('a, 'b) Bddapron.Domain0.mtbdd
val man_is_mtbdd : ('a, 'b, 'c, 'd) Bddapron.Domain0.man -> bool
val man_of_mtbdd :
('a, 'b) Bddapron.Domain0.mtbdd -> ('a, 'b, 'c, 'd) Bddapron.Domain0.man
val man_to_mtbdd :
('a, 'b, 'c, 'd) Bddapron.Domain0.man -> ('a, 'b) Bddapron.Domain0.mtbdd
val of_mtbdd :
('a, 'b) Bddapron.Domain0.mtbdd *
'b Bddapron.Mtbdddomain0.t Bddapron.Domain0.t ->
('a, 'b, 'c, 'd) Bddapron.Domain0.man * 'd Bddapron.Domain0.t
val to_mtbdd :
('a, 'b, 'c, 'd) Bddapron.Domain0.man * 'd Bddapron.Domain0.t ->
('a, 'b) Bddapron.Domain0.mtbdd *
'b Bddapron.Mtbdddomain0.t Bddapron.Domain0.t
type ('a, 'b) bdd =
('a, 'b, ('a, 'b) Bddapron.Bdddomain0.man, 'b Bddapron.Bdddomain0.t)
Bddapron.Domain0.man
val bdd_of_bdddomain :
('a, 'b) Bddapron.Bdddomain0.man -> ('a, 'b) Bddapron.Domain0.bdd
val make_bdd : 'b Apron.Manager.t -> ('a, 'b) Bddapron.Domain0.bdd
val man_is_bdd : ('a, 'b, 'c, 'd) Bddapron.Domain0.man -> bool
val man_of_bdd :
('a, 'b) Bddapron.Domain0.bdd -> ('a, 'b, 'c, 'd) Bddapron.Domain0.man
val man_to_bdd :
('a, 'b, 'c, 'd) Bddapron.Domain0.man -> ('a, 'b) Bddapron.Domain0.bdd
val of_bdd :
('a, 'b) Bddapron.Domain0.bdd *
'b Bddapron.Bdddomain0.t Bddapron.Domain0.t ->
('a, 'b, 'c, 'd) Bddapron.Domain0.man * 'd Bddapron.Domain0.t
val to_bdd :
('a, 'b, 'c, 'd) Bddapron.Domain0.man * 'd Bddapron.Domain0.t ->
('a, 'b) Bddapron.Domain0.bdd *
'b Bddapron.Bdddomain0.t Bddapron.Domain0.t
end