package mlcuddidl

  1. Overview
  2. Docs
type t
type add =
  1. | Leaf of float
  2. | 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 = {
  1. commonN : Custom.common;
  2. closureN : Bdd.dt array -> t array -> t option;
  3. arityNbdd : int;
}
type opG = {
  1. commonG : Custom.common;
  2. arityGbdd : int;
  3. closureG : Bdd.dt array -> t array -> t option;
  4. oclosureBeforeRec : ((int * bool) -> Bdd.dt array -> t array -> Bdd.dt array * t array) option;
  5. 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