bddapron 2.2.4 · OCaml Package

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

symbol : 'a Env.symbol;
compare_cond : 'c -> 'c -> int;
negate_cond : 'b -> 'c -> 'c;
support_cond : 'b -> 'c -> 'a PSette.t;
mutable print_cond : 'b -> Format.formatter -> 'c -> unit;
mutable cudd : 'd Cudd.Man.t;
mutable bddindex0 : int;
mutable bddsize : int;
mutable bddindex : int;
mutable bddincr : int;
mutable condidb : ('c, int * bool) PDMappe.t;
mutable supp : 'd Cudd.Bdd.t;
mutable careset : 'd Cudd.Bdd.t;
bddmax : int option;

}

val print : 'b -> Format.formatter -> ('a, 'b, 'c, 'd) t -> unit

val make : 
  symbol:'a Env.symbol ->
  compare_cond:('c -> 'c -> int) ->
  negate_cond:('b -> 'c -> 'c) ->
  support_cond:('b -> 'c -> 'a PSette.t) ->
  print_cond:('b -> Format.formatter -> 'c -> unit) ->
  ?bddindex0:int ->
  ?bddsize:int ->
  ?bddmax:int ->
  'd Cudd.Man.t ->
  ('a, 'b, 'c, 'd) t

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

val permutation : ('a, 'b, 'c, 'd) t -> int array

val permute_with : ('a, 'b, 'c, 'd) t -> int array -> unit

val normalize_with : ('a, 'b, 'c, 'd) t -> int array

val reduce_with : ('a, 'b, 'c, 'd) t -> 'd Cudd.Bdd.t -> unit

val clear : ('a, 'b, 'c, 'd) t -> unit

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

val cond_of_idb : ('a, 'b, 'c, 'd) t -> (int * bool) -> 'c

val idb_of_cond : 'a -> ('b, 'a, 'c, 'd) t -> 'c -> int * bool

val compute_careset : ('a, 'b, 'c, 'd) t -> normalized:bool -> unit

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

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

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

val shift_with : ('a, 'b, 'c, 'd) t -> int -> int array

val extend_with : ('a, 'b, 'c, 'd) t -> int -> unit

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

val permutation12 : ('a, 'b, 'c, 'd) t -> ('a, 'b, 'c, 'd) t -> int array

val permutation21 : ('a, 'b, 'c, 'd) t -> ('a, 'b, 'c, 'd) t -> int array

type ('a, 'b, 'c, 'd) repo

val save : ('a, 'b, 'c, 'd) t -> ('a, 'b, 'c, 'd) repo

val restore_with : ('a, 'b, 'c, 'd) repo -> ('a, 'b, 'c, 'd) t -> unit

type (!'a, !'b) value = {

cond : 'a;
val1 : 'b;

}

val make_value : 'a -> 'b -> ('a, 'b) value

val get_cond : ('a, 'b) value -> 'a

val get_val1 : ('a, 'b) value -> 'b

val get_env : ('a, ('b, 'c) Env.value) value -> 'b

val get_val0 : ('a, ('b, 'c) Env.value) value -> 'c

package bddapron