package bddapron

  1. Overview
  2. Docs
type !'a typdef = 'a Bdd.Env.typdef
type !'a typ = [
  1. | `Benum of 'a
  2. | `Bint of bool * int
  3. | `Bool
  4. | `Int
  5. | `Real
]
type !'a symbol = 'a Bdd.Env.symbol = {
  1. compare : 'a -> 'a -> int;
  2. marshal : 'a -> string;
  3. unmarshal : string -> 'a;
  4. mutable print : Format.formatter -> 'a -> unit;
}
type (!'a, !'b) ext = {
  1. mutable table : 'a Apronexpr.t Cudd.Mtbdd.table;
  2. mutable eapron : Apron.Environment.t;
  3. mutable aext : 'b;
}
type (!'a, !'b, !'c, !'d) t0 = ('a, 'b, 'c, Cudd.Man.v, ('a, 'd) ext) Bdd.Env.t0
module O : sig ... end
type !'a t = ('a, 'a typ, 'a typdef, unit) O.t
val print_typ : (Format.formatter -> 'a -> unit) -> Format.formatter -> [> 'a typ ] -> unit
val print_typdef : (Format.formatter -> 'a -> unit) -> Format.formatter -> [> 'a typdef ] -> unit
val print_idcondb : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> Format.formatter -> (int * bool) -> unit
val print_order : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> Format.formatter -> unit
val print : Format.formatter -> ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> unit
val marshal : 'a -> string
val unmarshal : string -> 'a
val make_symbol : ?compare:('a -> 'a -> int) -> ?marshal:('a -> string) -> ?unmarshal:(string -> 'a) -> (Format.formatter -> 'a -> unit) -> 'a symbol
val string_symbol : string symbol
val make : symbol:'a symbol -> ?bddindex0:int -> ?bddsize:int -> ?relational:bool -> Cudd.Man.vt -> 'a t
val make_string : ?bddindex0:int -> ?bddsize:int -> ?relational:bool -> Cudd.Man.vt -> string t
val copy : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> ('a, 'b, 'c, 'd) O.t
val copy_ext : copy_aext:('b -> 'c) -> ('a, 'b) ext -> ('a, 'c) ext
val mem_typ : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a -> bool
val mem_var : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a -> bool
val mem_label : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a -> bool
val typdef_of_typ : ('a, [> 'a typ ], [> 'a typdef ] as 'b, 'd) O.t -> 'a -> 'b
val typ_of_var : ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd) O.t -> 'a -> 'b
val vars : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a PSette.t
val labels : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a PSette.t
val apron : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> Apron.Environment.t
val add_typ_with : ('a, [> 'a typ ], [> 'a typdef ] as 'b, 'd) O.t -> 'a -> 'b -> unit
val add_vars_with : ('a, [> 'a typ ] as 'b, [> 'a typdef ], 'd) O.t -> ?booking_factor:int -> ?packing:Bdd.Env.packing -> ('a * 'b) list -> int array option
val remove_vars_with : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a list -> int array option
val rename_vars_with : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> ('a * 'a) list -> int array option * Apron.Dim.perm option
val add_typ : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> 'a -> 'c -> ('a, 'b, 'c, 'd) O.t
val add_vars : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> ('a * 'b) list -> ('a, 'b, 'c, 'd) O.t
val remove_vars : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> 'a list -> ('a, 'b, 'c, 'd) O.t
val rename_vars : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> ('a * 'a) list -> ('a, 'b, 'c, 'd) O.t
val is_leq : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> ('a, 'b, 'c, 'd) O.t -> bool
val is_eq : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> ('a, 'b, 'c, 'd) O.t -> bool
val lce : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> ('a, 'b, 'c, 'd) O.t -> ('a, 'b, 'c, 'd) O.t
type change = {
  1. cbdd : Cudd.Man.v Bdd.Env.change;
  2. capron : Apron.Dim.change2;
}
val compute_change : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> ('a, 'b, 'c, 'd) O.t -> change
type (!'a, !'b) value = ('a, 'b) Bdd.Env.value = {
  1. env : 'a;
  2. val0 : 'b;
}
val make_value : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> 'e -> (('a, 'b, 'c, 'd) O.t, 'e) value
val get_env : ('a, 'b) value -> 'a
val get_val0 : ('a, 'b) value -> 'b
val check_var : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a -> unit
val check_lvar : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a list -> unit
val check_value : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> (('a, 'b, 'c, 'd) O.t, 'e) value -> unit
val check_value2 : (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t, 'e) value -> (('a, 'b, 'c, 'd) O.t, 'f) value -> unit
val check_value3 : (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t, 'e) value -> (('a, 'b, 'c, 'd) O.t, 'f) value -> (('a, 'b, 'c, 'd) O.t, 'g) value -> unit
val check_lvarvalue : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> ('a * (('a, 'b, 'c, 'd) O.t, 'e) value) list -> ('a * 'e) list
val check_lvalue : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> (('a, 'b, 'c, 'd) O.t, 'e) value list -> 'e list
val check_ovalue : ('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> (('a, 'b, 'c, 'd) O.t, 'e) value option -> 'e option
val mapunop : ('e -> 'f) -> (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t, 'e) value -> (('a, 'b, 'c, 'd) O.t, 'f) value
val mapbinop : ('e -> 'f -> 'g) -> (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t, 'e) value -> (('a, 'b, 'c, 'd) O.t, 'f) value -> (('a, 'b, 'c, 'd) O.t, 'g) value
val mapbinope : (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t -> 'e -> 'f -> 'g) -> (('a, 'b, 'c, 'd) O.t, 'e) value -> (('a, 'b, 'c, 'd) O.t, 'f) value -> (('a, 'b, 'c, 'd) O.t, 'g) value
val mapterop : ('e -> 'f -> 'g -> 'h) -> (('a, [> 'a typ ] as 'b, [> 'a typdef ] as 'c, 'd) O.t, 'e) value -> (('a, 'b, 'c, 'd) O.t, 'f) value -> (('a, 'b, 'c, 'd) O.t, 'g) value -> (('a, 'b, 'c, 'd) O.t, 'h) value
val var_of_aprondim : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> Apron.Dim.t -> 'a
val aprondim_of_var : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> 'a -> Apron.Dim.t
val string_of_aprondim : ('a, [> 'a typ ], [> 'a typdef ], 'd) O.t -> Apron.Dim.t -> string