bddapron 2.3.3 · OCaml Package

type (!'a, !'b, !'c, !'d) man = {

typ : string;
man : 'c;
canonicalize : ?apron:bool -> 'c -> 'd -> unit;
size : 'c -> 'd -> int;
print : ?print_apron: ((int -> string) -> Format.formatter -> 'b Apron.Abstract0.t -> unit) -> 'a Env.t -> Format.formatter -> 'd -> unit;
bottom : 'c -> 'a Env.t -> 'd;
top : 'c -> 'a Env.t -> 'd;
of_apron : 'c -> 'a Env.t -> 'b Apron.Abstract0.t -> 'd;
of_bddapron : 'c -> 'a Env.t -> ('a Expr0.Bool.t * 'b Apron.Abstract0.t) list -> 'd;
is_bottom : 'c -> 'd -> bool;
is_top : 'c -> 'd -> bool;
is_leq : 'c -> 'd -> 'd -> bool;
is_eq : 'c -> 'd -> 'd -> bool;
to_bddapron : 'c -> 'd -> ('a Expr0.Bool.t * 'b Apron.Abstract0.t) list;
meet : 'c -> 'd -> 'd -> 'd;
join : 'c -> 'd -> 'd -> 'd;
meet_condition : 'c -> 'a Env.t -> 'a Cond.t -> 'd -> 'a Expr0.Bool.t -> 'd;
assign_lexpr : ?relational:bool -> ?nodependency:bool -> 'c -> 'a Env.t -> 'a Cond.t -> 'd -> 'a list -> 'a Expr0.t list -> 'd option -> 'd;
substitute_lexpr : 'c -> 'a Env.t -> 'a Cond.t -> 'd -> 'a list -> 'a Expr0.t list -> 'd option -> 'd;
forget_list : 'c -> 'a Env.t -> 'd -> 'a list -> 'd;
forall_bool_list : 'c -> 'a Env.t -> 'd -> 'a list -> 'd;
widening : 'c -> 'd -> 'd -> 'd;
widening_threshold : 'c -> 'd -> 'd -> Apron.Lincons0.t array -> 'd;
apply_change : bottom:'d -> 'c -> 'd -> Env.change -> 'd;
apply_permutation : 'c -> 'd -> (int array option * Apron.Dim.perm option) -> 'd;

}

type !'d t = 'd

val canonicalize : ?apron:bool -> ('a, 'b, 'c, 'd) man -> 'd t -> unit

val size : ('a, 'b, 'c, 'd) man -> 'd t -> int

val print : 
  ?print_apron:
    ((int -> string) -> Format.formatter -> 'b Apron.Abstract0.t -> unit) ->
  ('a, 'b, 'c, 'd) man ->
  'a Env.t ->
  Format.formatter ->
  'd t ->
  unit

val bottom : ('a, 'b, 'c, 'd) man -> 'a Env.t -> 'd t

val top : ('a, 'b, 'c, 'd) man -> 'a Env.t -> 'd t

val of_apron : ('a, 'b, 'c, 'd) man -> 'a Env.t -> 'b Apron.Abstract0.t -> 'd t

val of_bddapron : 
  ('a, 'b, 'c, 'd) man ->
  'a Env.t ->
  ('a Expr0.Bool.t * 'b Apron.Abstract0.t) list ->
  'd t

val is_bottom : ('a, 'b, 'c, 'd) man -> 'd t -> bool

val is_top : ('a, 'b, 'c, 'd) man -> 'd t -> bool

val is_leq : ('a, 'b, 'c, 'd) man -> 'd t -> 'd t -> bool

val is_eq : ('a, 'b, 'c, 'd) man -> 'd t -> 'd t -> bool

val to_bddapron : 
  ('a, 'b, 'c, 'd) man ->
  'd t ->
  ('a Expr0.Bool.t * 'b Apron.Abstract0.t) list

val meet : ('a, 'b, 'c, 'd) man -> 'd t -> 'd t -> 'd t

val join : ('a, 'b, 'c, 'd) man -> 'd t -> 'd t -> 'd t

val meet_condition : 
  ('a, 'b, 'c, 'd) man ->
  'a Env.t ->
  'a Cond.t ->
  'd t ->
  'a Expr0.Bool.t ->
  'd t

val assign_lexpr : 
  ?relational:bool ->
  ?nodependency:bool ->
  ('a, 'b, 'c, 'd) man ->
  'a Env.t ->
  'a Cond.t ->
  'd t ->
  'a list ->
  'a Expr0.t list ->
  'd t option ->
  'd t

val substitute_lexpr : 
  ('a, 'b, 'c, 'd) man ->
  'a Env.t ->
  'a Cond.t ->
  'd t ->
  'a list ->
  'a Expr0.t list ->
  'd t option ->
  'd t

val forget_list : ('a, 'b, 'c, 'd) man -> 'a Env.t -> 'd t -> 'a list -> 'd t

val forall_bool_list : 
  ('a, 'b, 'c, 'd) man ->
  'a Env.t ->
  'd t ->
  'a list ->
  'd t

val widening : ('a, 'b, 'c, 'd) man -> 'd t -> 'd t -> 'd t

val widening_threshold : 
  ('a, 'b, 'c, 'd) man ->
  'd t ->
  'd t ->
  Apron.Lincons0.t array ->
  'd t

val apply_change : 
  bottom:'d t ->
  ('a, 'b, 'c, 'd) man ->
  'd t ->
  Env.change ->
  'd t

val apply_permutation : 
  ('a, 'b, 'c, 'd) man ->
  'd t ->
  (int array option * Apron.Dim.perm option) ->
  'd t

val man_get_apron : ('a, 'b, 'c, 'd) man -> 'b Apron.Manager.t

type (!'a, !'b) mtbdd =
  ('a, 'b, ('a, 'b) Mtbdddomain0.man, 'b Mtbdddomain0.t) man

val mtbdd_of_mtbdddomain : ('a, 'b) Mtbdddomain0.man -> ('a, 'b) mtbdd

val make_mtbdd : ?global:bool -> 'b Apron.Manager.t -> ('a, 'b) mtbdd

val man_is_mtbdd : ('a, 'b, 'c, 'd) man -> bool

val man_of_mtbdd : ('a, 'b) mtbdd -> ('a, 'b, 'c, 'd) man

val man_to_mtbdd : ('a, 'b, 'c, 'd) man -> ('a, 'b) mtbdd

val of_mtbdd : 
  (('a, 'b) mtbdd * 'b Mtbdddomain0.t t) ->
  ('a, 'b, 'c, 'd) man * 'd t

val to_mtbdd : 
  (('a, 'b, 'c, 'd) man * 'd t) ->
  ('a, 'b) mtbdd * 'b Mtbdddomain0.t t

type (!'a, !'b) bdd = ('a, 'b, ('a, 'b) Bdddomain0.man, 'b Bdddomain0.t) man

val bdd_of_bdddomain : ('a, 'b) Bdddomain0.man -> ('a, 'b) bdd

val make_bdd : 'b Apron.Manager.t -> ('a, 'b) bdd

val man_is_bdd : ('a, 'b, 'c, 'd) man -> bool

val man_of_bdd : ('a, 'b) bdd -> ('a, 'b, 'c, 'd) man

val man_to_bdd : ('a, 'b, 'c, 'd) man -> ('a, 'b) bdd

val of_bdd : (('a, 'b) bdd * 'b Bdddomain0.t t) -> ('a, 'b, 'c, 'd) man * 'd t

val to_bdd : (('a, 'b, 'c, 'd) man * 'd t) -> ('a, 'b) bdd * 'b Bdddomain0.t t

package bddapron