sig
type 'a leaf = 'a Apron.Abstract0.t
type 'a t = 'a Bddapron.ApronDD.leaf Cudd.Mtbddc.t
type 'a table = 'a Bddapron.ApronDD.leaf Cudd.Mtbddc.table
type 'a leaf_u = 'a Bddapron.ApronDD.leaf Cudd.Mtbddc.unique
type 'a global = {
op_is_leq :
('a Bddapron.ApronDD.leaf_u, 'a Bddapron.ApronDD.leaf_u)
Cudd.User.test2;
op_join :
('a Bddapron.ApronDD.leaf_u, 'a Bddapron.ApronDD.leaf_u,
'a Bddapron.ApronDD.leaf_u)
Cudd.User.op2;
op_meet :
('a Bddapron.ApronDD.leaf_u, 'a Bddapron.ApronDD.leaf_u,
'a Bddapron.ApronDD.leaf_u)
Cudd.User.op2;
op_exist : 'a Bddapron.ApronDD.leaf_u Cudd.User.exist;
}
type 'a man = {
apron : 'a Apron.Manager.t;
table : 'a Bddapron.ApronDD.table;
oglobal : 'a Bddapron.ApronDD.global option;
}
val make_table : 'a Apron.Manager.t -> 'a Bddapron.ApronDD.table
val neutral_join : 'a Apron.Abstract0.t -> bool
val special_is_leq :
'a Apron.Manager.t ->
'a Bddapron.ApronDD.t -> 'a Bddapron.ApronDD.t -> bool option
val special_join :
'a Apron.Manager.t ->
'a Bddapron.ApronDD.t ->
'a Bddapron.ApronDD.t -> 'a Bddapron.ApronDD.t option
val special_meet :
'a Apron.Manager.t ->
'a Bddapron.ApronDD.t ->
'a Bddapron.ApronDD.t -> 'a Bddapron.ApronDD.t option
val make_global :
'a Apron.Manager.t ->
'a Bddapron.ApronDD.table -> 'a Bddapron.ApronDD.global
val make_man :
?global:bool -> 'a Apron.Manager.t -> 'a Bddapron.ApronDD.man
val make_op_join :
'a Bddapron.ApronDD.man ->
('a Bddapron.ApronDD.leaf_u, 'a Bddapron.ApronDD.leaf_u,
'a Bddapron.ApronDD.leaf_u)
Cudd.User.op2
val print :
?print_apron:((int -> string) ->
Format.formatter -> 'a Apron.Abstract0.t -> unit) ->
(Format.formatter -> Cudd.Bdd.vt -> unit) ->
(int -> string) -> Format.formatter -> 'a Bddapron.ApronDD.t -> unit
val cst :
cudd:Cudd.Man.vt ->
'a Bddapron.ApronDD.man -> 'a Apron.Abstract0.t -> 'a Bddapron.ApronDD.t
val bottom :
cudd:Cudd.Man.vt ->
'a Bddapron.ApronDD.man -> Apron.Dim.dimension -> 'a Bddapron.ApronDD.t
val top :
cudd:Cudd.Man.vt ->
'a Bddapron.ApronDD.man -> Apron.Dim.dimension -> 'a Bddapron.ApronDD.t
val is_bottom : 'a Bddapron.ApronDD.man -> 'a Bddapron.ApronDD.t -> bool
val is_top : 'a Bddapron.ApronDD.man -> 'a Bddapron.ApronDD.t -> bool
val is_eq :
'a Bddapron.ApronDD.man ->
'a Bddapron.ApronDD.t -> 'a Bddapron.ApronDD.t -> bool
val is_leq :
'a Bddapron.ApronDD.man ->
'a Bddapron.ApronDD.t -> 'a Bddapron.ApronDD.t -> bool
val join :
'a Bddapron.ApronDD.man ->
'a Bddapron.ApronDD.t -> 'a Bddapron.ApronDD.t -> 'a Bddapron.ApronDD.t
val meet :
'a Bddapron.ApronDD.man ->
'a Bddapron.ApronDD.t -> 'a Bddapron.ApronDD.t -> 'a Bddapron.ApronDD.t
val widening :
'a Bddapron.ApronDD.man ->
'a Bddapron.ApronDD.t -> 'a Bddapron.ApronDD.t -> 'a Bddapron.ApronDD.t
val widening_threshold :
'a Bddapron.ApronDD.man ->
'a Bddapron.ApronDD.t ->
'a Bddapron.ApronDD.t -> Apron.Lincons0.t array -> 'a Bddapron.ApronDD.t
val meet_tcons_array :
'a Bddapron.ApronDD.man ->
'a Bddapron.ApronDD.t -> Apron.Tcons0.t array -> 'a Bddapron.ApronDD.t
val forget_array :
'a Bddapron.ApronDD.man ->
'a Bddapron.ApronDD.t -> Apron.Dim.t array -> 'a Bddapron.ApronDD.t
val permute_dimensions :
'a Bddapron.ApronDD.man ->
'a Bddapron.ApronDD.t -> Apron.Dim.perm -> 'a Bddapron.ApronDD.t
val add_dimensions :
'a Bddapron.ApronDD.man ->
'a Bddapron.ApronDD.t ->
Apron.Dim.change -> bool -> 'a Bddapron.ApronDD.t
val remove_dimensions :
'a Bddapron.ApronDD.man ->
'a Bddapron.ApronDD.t -> Apron.Dim.change -> 'a Bddapron.ApronDD.t
val apply_dimchange2 :
'a Bddapron.ApronDD.man ->
'a Bddapron.ApronDD.t ->
Apron.Dim.change2 -> bool -> 'a Bddapron.ApronDD.t
type asssub = Assign | Substitute
val asssub_texpr_array :
?asssub_bdd:(Cudd.Bdd.vt -> Cudd.Bdd.vt) ->
Bddapron.ApronDD.asssub ->
'b Bdd.Env.symbol ->
'a Bddapron.ApronDD.man ->
Apron.Environment.t ->
'a Bddapron.ApronDD.t ->
Apron.Dim.t array ->
'b Bddapron.ApronexprDD.t array ->
'a Bddapron.ApronDD.t option -> 'a Bddapron.ApronDD.t
val assign_texpr_array :
'b Bdd.Env.symbol ->
'a Bddapron.ApronDD.man ->
Apron.Environment.t ->
'a Bddapron.ApronDD.t ->
Apron.Dim.t array ->
'b Bddapron.ApronexprDD.t array ->
'a Bddapron.ApronDD.t option -> 'a Bddapron.ApronDD.t
val substitute_texpr_array :
'b Bdd.Env.symbol ->
'a Bddapron.ApronDD.man ->
Apron.Environment.t ->
'a Bddapron.ApronDD.t ->
Apron.Dim.t array ->
'b Bddapron.ApronexprDD.t array ->
'a Bddapron.ApronDD.t option -> 'a Bddapron.ApronDD.t
val exist :
'a Bddapron.ApronDD.man ->
supp:Cudd.Bdd.vt -> 'a Bddapron.ApronDD.t -> 'a Bddapron.ApronDD.t
val existand :
'a Bddapron.ApronDD.man ->
bottom:'a Apron.Abstract0.t Cudd.Mtbddc.unique ->
supp:Cudd.Bdd.vt ->
Cudd.Bdd.vt -> 'a Bddapron.ApronDD.t -> 'a Bddapron.ApronDD.t
end