package bddapron

  1. Overview
  2. Docs
package bddapron
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 = {
  1. op_is_leq : ('a leaf_u, 'a leaf_u) Cudd.User.test2;
  2. op_join : ('a leaf_u, 'a leaf_u, 'a leaf_u) Cudd.User.op2;
  3. op_meet : ('a leaf_u, 'a leaf_u, 'a leaf_u) Cudd.User.op2;
  4. op_exist : 'a leaf_u Cudd.User.exist;
  5. op_forall : 'a leaf_u Cudd.User.exist;
}
type !'a man = {
  1. apron : 'a Apron.Manager.t;
  2. table : 'a table;
  3. 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 =
  1. | Assign
  2. | 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