bddapron

Logico-numerical domain(s) based on BDDs and APRON
Legend:
Library
Module
Module type
Parameter
Class
Class type
Manual
Module Bddapron . Bdddomain0
type (!'a, !'b) man = {
apron : 'b Apron.Manager.t;
mutable bdd_restrict : Cudd.Bdd.vt -> Cudd.Bdd.vt -> Cudd.Bdd.vt;
mutable expr_restrict : 'a Expr0.t -> Cudd.Bdd.vt -> 'a Expr0.t;
mutable meet_disjoint : bool;
mutable join_disjoint : bool;
mutable meet_cond_unique : bool;
mutable meet_cond_disjoint : bool;
mutable meet_cond_depth : int;
mutable assign_unique : bool;
mutable assign_disjoint : bool;
mutable substitute_unique : bool;
mutable substitute_disjoint : bool;
mutable forget_unique : bool;
mutable forget_disjoint : bool;
mutable forall_bool_unique : bool;
mutable forall_bool_disjoint : bool;
mutable change_environment_unique : bool;
mutable change_environment_disjoint : bool;
}
type !'b t = {
mutable list : 'b elt list;
bottom : 'b elt;
mutable unique : bool;
mutable disjoint : bool;
}
val make_man : 'b Apron.Manager.t -> ( 'a, 'b ) man
val canonicalize : ?apron:bool -> ?unique:bool -> ?disjoint:bool -> ( 'a, 'b ) man -> 'b t -> unit
val size : ( 'a, 'b ) man -> 'b t -> int
val print : ?print_apron: ( ( int -> string ) -> Format.formatter -> 'b Apron.Abstract0.t -> unit ) -> 'a Env.t -> Format.formatter -> 'b t -> unit
val bottom : ( 'a, 'b ) man -> 'a Env.t -> 'b t
val top : ( 'a, 'b ) man -> 'a Env.t -> 'b t
val of_apron : ( 'a, 'b ) man -> 'a Env.t -> 'b Apron.Abstract0.t -> 'b t
val of_bddapron : ( 'a, 'b ) man -> 'a Env.t -> ('a Expr0.Bool.t * 'b Apron.Abstract0.t) list -> 'b t
val is_bottom : ( 'a, 'b ) man -> 'b t -> bool
val is_top : ( 'a, 'b ) man -> 'b t -> bool
val is_leq : ( 'a, 'b ) man -> 'b t -> 'b t -> bool
val is_eq : ( 'a, 'b ) man -> 'b t -> 'b t -> bool
val to_bddapron : ( 'a, 'b ) man -> 'b t -> ('a Expr0.Bool.t * 'b Apron.Abstract0.t) list
val meet : ( 'a, 'b ) man -> 'b t -> 'b t -> 'b t
val join : ( 'a, 'b ) man -> 'b t -> 'b t -> 'b t
val meet_condition : ( 'a, 'b ) man -> 'a Env.t -> 'a Cond.t -> 'b t -> 'a Expr0.Bool.t -> 'b t
val assign_lexpr : ?relational:bool -> ?nodependency:bool -> ( 'a, 'b ) man -> 'a Env.t -> 'a Cond.t -> 'b t -> 'a list -> 'a Expr0.t list -> 'b t option -> 'b t
val substitute_lexpr : ( 'a, 'b ) man -> 'a Env.t -> 'a Cond.t -> 'b t -> 'a list -> 'a Expr0.t list -> 'b t option -> 'b t
val forget_list : ( 'a, 'b ) man -> 'a Env.t -> 'b t -> 'a list -> 'b t
val forall_bool_list : ( 'a, 'b ) man -> 'a Env.t -> 'b t -> 'a list -> 'b t
val widening : ( 'a, 'b ) man -> 'b t -> 'b t -> 'b t
val widening_threshold : ( 'a, 'b ) man -> 'b t -> 'b t -> Apron.Lincons0.t array -> 'b t
val apply_change : bottom:'b t -> ( 'a, 'b ) man -> 'b t -> Env.change -> 'b t
val apply_permutation : ( 'a, 'b ) man -> 'b t -> (int array option * Apron.Dim.perm option) -> 'b t
module O : sig ... end