sig
type ('a, 'b, 'c, 'd) man = ('a, 'b, 'c, 'd) Bddapron.Domain0.man
type ('a, 'b) mtbdd =
('a, 'b, ('a, 'b) Bddapron.Mtbdddomain0.man,
'b Bddapron.Mtbdddomain0.t)
Bddapron.Domain1.man
type ('a, 'b) bdd =
('a, 'b, ('a, 'b) Bddapron.Bdddomain0.man, 'b Bddapron.Bdddomain0.t)
Bddapron.Domain1.man
type ('a, 'd) t = ('a Bddapron.Env.t, 'd) Bddapron.Env.value
val canonicalize :
?apron:bool ->
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t -> unit
val print :
?print_apron:((int -> string) ->
Format.formatter -> 'b Apron.Abstract0.t -> unit) ->
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
Format.formatter -> ('a, 'd) Bddapron.Domain1.t -> unit
val get_env : ('a, 'd) Bddapron.Domain1.t -> 'a Bddapron.Env.t
val to_level0 : ('a, 'd) Bddapron.Domain1.t -> 'd
val of_level0 : 'a Bddapron.Env.t -> 'd -> ('a, 'd) Bddapron.Domain1.t
val size :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t -> int
val bottom :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
'a Bddapron.Env.t -> ('a, 'd) Bddapron.Domain1.t
val top :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
'a Bddapron.Env.t -> ('a, 'd) Bddapron.Domain1.t
val of_apron :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
'a Bddapron.Env.t -> 'b Apron.Abstract1.t -> ('a, 'd) Bddapron.Domain1.t
val of_bddapron :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
'a Bddapron.Env.t ->
('a Bddapron.Expr1.Bool.t * 'b Apron.Abstract1.t) list ->
('a, 'd) Bddapron.Domain1.t
val is_bottom :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t -> bool
val is_top :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t -> bool
val is_leq :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t -> ('a, 'd) Bddapron.Domain1.t -> bool
val is_eq :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t -> ('a, 'd) Bddapron.Domain1.t -> bool
val to_bddapron :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t ->
('a Bddapron.Expr1.Bool.t * 'b Apron.Abstract1.t) list
val meet :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t ->
('a, 'd) Bddapron.Domain1.t -> ('a, 'd) Bddapron.Domain1.t
val join :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t ->
('a, 'd) Bddapron.Domain1.t -> ('a, 'd) Bddapron.Domain1.t
val meet_condition :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
'a Bddapron.Cond.t ->
('a, 'd) Bddapron.Domain1.t ->
'a Bddapron.Expr1.Bool.t -> ('a, 'd) Bddapron.Domain1.t
val meet_condition2 :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t ->
'a Bddapron.Expr2.Bool.t -> ('a, 'd) Bddapron.Domain1.t
val assign_lexpr :
?relational:bool ->
?nodependency:bool ->
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
'a Bddapron.Cond.t ->
('a, 'd) Bddapron.Domain1.t ->
'a list ->
'a Bddapron.Expr1.t list ->
('a, 'd) Bddapron.Domain1.t option -> ('a, 'd) Bddapron.Domain1.t
val assign_listexpr2 :
?relational:bool ->
?nodependency:bool ->
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t ->
'a list ->
'a Bddapron.Expr2.List.t ->
('a, 'd) Bddapron.Domain1.t option -> ('a, 'd) Bddapron.Domain1.t
val substitute_lexpr :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
'a Bddapron.Cond.t ->
('a, 'd) Bddapron.Domain1.t ->
'a list ->
'a Bddapron.Expr1.t list ->
('a, 'd) Bddapron.Domain1.t option -> ('a, 'd) Bddapron.Domain1.t
val substitute_listexpr2 :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t ->
'a list ->
'a Bddapron.Expr2.List.t ->
('a, 'd) Bddapron.Domain1.t option -> ('a, 'd) Bddapron.Domain1.t
val forget_list :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t -> 'a list -> ('a, 'd) Bddapron.Domain1.t
val widening :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t ->
('a, 'd) Bddapron.Domain1.t -> ('a, 'd) Bddapron.Domain1.t
val widening_threshold :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t ->
('a, 'd) Bddapron.Domain1.t ->
Apron.Lincons1.earray -> ('a, 'd) Bddapron.Domain1.t
val change_environment :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t ->
'a Bddapron.Env.t -> ('a, 'd) Bddapron.Domain1.t
val unify :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t ->
('a, 'd) Bddapron.Domain1.t -> ('a, 'd) Bddapron.Domain1.t
val rename :
('a, 'b, 'c, 'd) Bddapron.Domain1.man ->
('a, 'd) Bddapron.Domain1.t ->
('a * 'a) list -> ('a, 'd) Bddapron.Domain1.t
val man_get_apron :
('a, 'b, 'c, 'd) Bddapron.Domain1.man -> 'b Apron.Manager.t
val mtbdd_of_mtbdddomain :
('a, 'b) Bddapron.Mtbdddomain0.man -> ('a, 'b) Bddapron.Domain1.mtbdd
val make_mtbdd :
?global:bool -> 'b Apron.Manager.t -> ('a, 'b) Bddapron.Domain1.mtbdd
val man_is_mtbdd : ('a, 'b, 'c, 'd) Bddapron.Domain1.man -> bool
val man_of_mtbdd :
('a, 'b) Bddapron.Domain1.mtbdd -> ('a, 'b, 'c, 'd) Bddapron.Domain1.man
val man_to_mtbdd :
('a, 'b, 'c, 'd) Bddapron.Domain1.man -> ('a, 'b) Bddapron.Domain1.mtbdd
val of_mtbdd :
('a, 'b) Bddapron.Domain1.mtbdd *
('a, 'b Bddapron.Mtbdddomain0.t) Bddapron.Domain1.t ->
('a, 'b, 'c, 'd) Bddapron.Domain1.man * ('a, 'd) Bddapron.Domain1.t
val to_mtbdd :
('a, 'b, 'c, 'd) Bddapron.Domain1.man * ('a, 'd) Bddapron.Domain1.t ->
('a, 'b) Bddapron.Domain1.mtbdd *
('a, 'b Bddapron.Mtbdddomain0.t) Bddapron.Domain1.t
val bdd_of_bdddomain :
('a, 'b) Bddapron.Bdddomain0.man -> ('a, 'b) Bddapron.Domain1.bdd
val make_bdd : 'b Apron.Manager.t -> ('a, 'b) Bddapron.Domain1.bdd
val man_is_bdd : ('a, 'b, 'c, 'd) Bddapron.Domain1.man -> bool
val man_of_bdd :
('a, 'b) Bddapron.Domain1.bdd -> ('a, 'b, 'c, 'd) Bddapron.Domain1.man
val man_to_bdd :
('a, 'b, 'c, 'd) Bddapron.Domain1.man -> ('a, 'b) Bddapron.Domain1.bdd
val of_bdd :
('a, 'b) Bddapron.Domain1.bdd *
('a, 'b Bddapron.Bdddomain0.t) Bddapron.Domain1.t ->
('a, 'b, 'c, 'd) Bddapron.Domain1.man * ('a, 'd) Bddapron.Domain1.t
val to_bdd :
('a, 'b, 'c, 'd) Bddapron.Domain1.man * ('a, 'd) Bddapron.Domain1.t ->
('a, 'b) Bddapron.Domain1.bdd *
('a, 'b Bddapron.Bdddomain0.t) Bddapron.Domain1.t
end