bddapron

Logico-numerical domain(s) based on BDDs and APRON
Legend:
Library
Module
Module type
Parameter
Class
Class type
Manual
Module Bddapron . ApronDD
type 'a leaf = 'a Apron.Abstract0.t
type 'a t = 'a leaf Cudd.Mtbddc.t
type 'a table = 'a leaf Cudd.Mtbddc.table
type 'a leaf_u = 'a leaf Cudd.Mtbddc.unique
type !'a global = {
op_is_leq : ( 'a leaf_u, 'a leaf_u ) Cudd.User.test2;
op_join : ( 'a leaf_u, 'a leaf_u, 'a leaf_u ) Cudd.User.op2;
op_meet : ( 'a leaf_u, 'a leaf_u, 'a leaf_u ) Cudd.User.op2;
op_exist : 'a leaf_u Cudd.User.exist;
op_forall : 'a leaf_u Cudd.User.exist;
}
type !'a man = {
apron : 'a Apron.Manager.t;
table : 'a table;
oglobal : 'a global option;
}
val make_table : 'a Apron.Manager.t -> 'a table
val neutral_join : 'a Apron.Abstract0.t -> bool
val special_is_leq : 'a Apron.Manager.t -> 'a t -> 'a t -> bool option
val special_join : 'a Apron.Manager.t -> 'a t -> 'a t -> 'a t option
val special_meet : 'a Apron.Manager.t -> 'a t -> 'a t -> 'a t option
val make_global : 'a Apron.Manager.t -> 'a table -> 'a global
val make_man : ?global:bool -> 'a Apron.Manager.t -> 'a man
val make_op_join : 'a man -> ( 'a leaf_u, 'a leaf_u, 'a 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 t -> unit
val cst : cudd:Cudd.Man.vt -> 'a man -> 'a Apron.Abstract0.t -> 'a t
val bottom : cudd:Cudd.Man.vt -> 'a man -> Apron.Dim.dimension -> 'a t
val top : cudd:Cudd.Man.vt -> 'a man -> Apron.Dim.dimension -> 'a t
val is_bottom : 'a man -> 'a t -> bool
val is_top : 'a man -> 'a t -> bool
val is_eq : 'a man -> 'a t -> 'a t -> bool
val is_leq : 'a man -> 'a t -> 'a t -> bool
val join : 'a man -> 'a t -> 'a t -> 'a t
val meet : 'a man -> 'a t -> 'a t -> 'a t
val widening : 'a man -> 'a t -> 'a t -> 'a t
val widening_threshold : 'a man -> 'a t -> 'a t -> Apron.Lincons0.t array -> 'a t
val meet_tcons_array : 'a man -> 'a t -> Apron.Tcons0.t array -> 'a t
val forget_array : 'a man -> 'a t -> Apron.Dim.t array -> 'a t
val permute_dimensions : 'a man -> 'a t -> Apron.Dim.perm -> 'a t
val add_dimensions : 'a man -> 'a t -> Apron.Dim.change -> bool -> 'a t
val remove_dimensions : 'a man -> 'a t -> Apron.Dim.change -> 'a t
val apply_dimchange2 : 'a man -> 'a t -> Apron.Dim.change2 -> bool -> 'a t
type asssub =
| Assign
| Substitute
val asssub_texpr_array : ?asssub_bdd:( Cudd.Bdd.vt -> Cudd.Bdd.vt ) -> asssub -> 'b Bdd.Env.symbol -> 'a man -> Apron.Environment.t -> 'a t -> Apron.Dim.t array -> 'b ApronexprDD.t array -> 'a t option -> 'a t
val assign_texpr_array : 'b Bdd.Env.symbol -> 'a man -> Apron.Environment.t -> 'a t -> Apron.Dim.t array -> 'b ApronexprDD.t array -> 'a t option -> 'a t
val substitute_texpr_array : 'b Bdd.Env.symbol -> 'a man -> Apron.Environment.t -> 'a t -> Apron.Dim.t array -> 'b ApronexprDD.t array -> 'a t option -> 'a t
val exist : 'a man -> supp:Cudd.Bdd.vt -> 'a t -> 'a t
val existand : 'a man -> bottom:'a Apron.Abstract0.t Cudd.Mtbddc.unique -> supp:Cudd.Bdd.vt -> Cudd.Bdd.vt -> 'a t -> 'a t
val forall : 'a man -> supp:Cudd.Bdd.vt -> 'a t -> 'a t