mlcuddidl 3.0.8 · OCaml Package

type t

type add =

| Leaf of float
| Ite of int * t * t

val manager : t -> Man.dt

val is_cst : t -> bool

val topvar : t -> int

val dthen : t -> t

val delse : t -> t

val dval : t -> float

val cofactors : int -> t -> t * t

val cofactor : t -> Bdd.dt -> t

val inspect : t -> add

val support : t -> Bdd.dt

val supportsize : t -> int

val is_var_in : int -> t -> bool

val vectorsupport : t array -> Bdd.dt

val vectorsupport2 : Bdd.dt array -> t array -> Bdd.dt

val cst : Man.dt -> float -> t

val background : Man.dt -> t

val ite : Bdd.dt -> t -> t -> t

val ite_cst : Bdd.dt -> t -> t -> t option

val eval_cst : t -> Bdd.dt -> t option

val compose : int -> Bdd.dt -> t -> t

val vectorcompose : ?memo:Memo.t -> Bdd.dt array -> t -> t

val varmap : t -> t

val permute : ?memo:Memo.t -> t -> int array -> t

val is_equal : t -> t -> bool

val is_equal_when : t -> t -> Bdd.dt -> bool

val is_eval_cst : t -> Bdd.dt -> float option

val is_ite_cst : Bdd.dt -> t -> t -> float option

val size : t -> int

val nbpaths : t -> float

val nbnonzeropaths : t -> float

val nbminterms : int -> t -> float

val density : int -> t -> float

val nbleaves : t -> int

val iter_cube : (Man.tbool array -> float -> unit) -> t -> unit

val iter_node : (t -> unit) -> t -> unit

val guard_of_node : t -> t -> Bdd.dt

val guard_of_nonbackground : t -> Bdd.dt

val nodes_below_level : t -> int option -> int -> t array

val guard_of_leaf : t -> float -> Bdd.dt

val leaves : t -> float array

val pick_leaf : t -> float

val guardleafs : t -> (Bdd.dt * float) array

val constrain : t -> Bdd.dt -> t

val tdconstrain : t -> Bdd.dt -> t

val restrict : t -> Bdd.dt -> t

val tdrestrict : t -> Bdd.dt -> t

val of_bdd : Bdd.dt -> t

val to_bdd : t -> Bdd.dt

val to_bdd_threshold : float -> t -> t

val to_bdd_strictthreshold : float -> t -> t

val to_bdd_interval : float -> float -> t -> t

val exist : Bdd.dt -> t -> t

val forall : Bdd.dt -> t -> t

val is_leq : t -> t -> bool

val add : t -> t -> t

val sub : t -> t -> t

val mul : t -> t -> t

val div : t -> t -> t

val min : t -> t -> t

val max : t -> t -> t

val agreement : t -> t -> t

val diff : t -> t -> t

val threshold : t -> t -> t

val setNZ : t -> t -> t

val log : t -> t

val matrix_multiply : int array -> t -> t -> t

val times_plus : int array -> t -> t -> t

val triangle : int array -> t -> t -> t

val mapleaf1 : default:t -> (Bdd.dt -> float -> float) -> t -> t

val mapleaf2 : default:t -> (Bdd.dt -> float -> float -> float) -> t -> t -> t

type op1 = (float, float) Custom.op1

type op2 = (float, float, float) Custom.op2

type op3 = (float, float, float, float) Custom.op3

type opN = {

commonN : Custom.common;
closureN : Bdd.dt array -> t array -> t option;
arityNbdd : int;

}

type opG = {

commonG : Custom.common;
arityGbdd : int;
closureG : Bdd.dt array -> t array -> t option;
oclosureBeforeRec : ((int * bool) -> Bdd.dt array -> t array -> Bdd.dt array * t array) option;
oclosureIte : (int -> t -> t -> t) option;

}

type test2 = (float, float) Custom.test2

type exist = float Custom.exist

type existand = float Custom.existand

type existop1 = (float, float) Custom.existop1

type existandop1 = (float, float) Custom.existandop1

val make_op1 : ?memo:Memo.t -> (float -> float) -> op1

val make_op2 : 
  ?memo:Memo.t ->
  ?commutative:bool ->
  ?idempotent:bool ->
  ?special:(t -> t -> t option) ->
  (float -> float -> float) ->
  op2

val make_op3 : 
  ?memo:Memo.t ->
  ?special:(t -> t -> t -> t option) ->
  (float -> float -> float -> float) ->
  op3

val make_opN : 
  ?memo:Memo.t ->
  int ->
  int ->
  (Bdd.dt array -> t array -> t option) ->
  opN

val make_opG : 
  ?memo:Memo.t ->
  ?beforeRec:
    ((int * bool) -> Bdd.dt array -> t array -> Bdd.dt array * t array) ->
  ?ite:(int -> t -> t -> t) ->
  int ->
  int ->
  (Bdd.dt array -> t array -> t option) ->
  opG

val make_test2 : 
  ?memo:Memo.t ->
  ?symetric:bool ->
  ?reflexive:bool ->
  ?special:(t -> t -> bool option) ->
  (float -> float -> bool) ->
  test2

val make_exist : ?memo:Memo.t -> op2 -> exist

val make_existand : ?memo:Memo.t -> bottom:float -> op2 -> existand

val make_existop1 : ?memo:Memo.t -> op1:op1 -> op2 -> existop1

val make_existandop1 : 
  ?memo:Memo.t ->
  op1:op1 ->
  bottom:float ->
  op2 ->
  existandop1

val clear_op1 : op1 -> unit

val clear_op2 : op2 -> unit

val clear_op3 : op3 -> unit

val clear_opN : opN -> unit

val clear_opG : opG -> unit

val clear_test2 : test2 -> unit

val clear_exist : exist -> unit

val clear_existand : existand -> unit

val clear_existop1 : existop1 -> unit

val clear_existandop1 : existandop1 -> unit

val apply_op1 : op1 -> t -> t

val apply_op2 : op2 -> t -> t -> t

val apply_op3 : op3 -> t -> t -> t

val apply_opN : opN -> Bdd.dt array -> t array -> t

val apply_opG : opG -> Bdd.dt array -> t array -> t

val apply_test2 : test2 -> t -> t -> bool

val apply_exist : exist -> supp:Bdd.dt -> t -> t

val apply_existand : existand -> supp:Bdd.dt -> Bdd.dt -> t -> t

val apply_existop1 : existop1 -> supp:Bdd.dt -> t -> t

val apply_existandop1 : existandop1 -> supp:Bdd.dt -> Bdd.dt -> t -> t

val map_op1 : ?memo:Memo.t -> (float -> float) -> t -> t

val map_op2 : 
  ?memo:Memo.t ->
  ?commutative:bool ->
  ?idempotent:bool ->
  ?special:(t -> t -> t option) ->
  (float -> float -> float) ->
  t ->
  t ->
  t

val map_op3 : 
  ?memo:Memo.t ->
  ?special:(t -> t -> t -> t option) ->
  (float -> float -> float -> float) ->
  t ->
  t ->
  t ->
  t

val map_opN : 
  ?memo:Memo.t ->
  (Bdd.dt array -> t array -> t option) ->
  Bdd.dt array ->
  t array ->
  t

val map_test2 : 
  ?memo:Memo.t ->
  ?symetric:bool ->
  ?reflexive:bool ->
  ?special:(t -> t -> bool option) ->
  (float -> float -> bool) ->
  t ->
  t ->
  bool

val transfer : t -> Man.d Man.t -> t

val _print : t -> unit

val print__minterm : Format.formatter -> t -> unit

val print_minterm : 
  (Format.formatter -> int -> unit) ->
  (Format.formatter -> float -> unit) ->
  Format.formatter ->
  t ->
  unit

val print : 
  (Format.formatter -> int -> unit) ->
  (Format.formatter -> float -> unit) ->
  Format.formatter ->
  t ->
  unit

package mlcuddidl