module Add:sig
..end
type
t
Man.d Man.t
).
Objects of this type contains both the top node of the ADD and the manager to which the node belongs. The manager can be retrieved with Cudd.Add.manager
. Objects of this type are automatically garbage collected.
type
add =
| |
Leaf of |
(* | Terminal value | *) |
| |
Ite of |
(* | Decision on CUDD variable | *) |
t
val manager : t -> Cudd.Man.dt
val is_cst : t -> bool
Cudd_IsConstant
. Is the ADD constant ?val topvar : t -> int
Cudd_NodeReadIndex
. Returns the index of the ADD (65535 for a constant ADD)val dthen : t -> t
Cudd_T
. Returns the positive subnode of the ADDval delse : t -> t
Cudd_E
. Returns the negative subnode of the ADDval dval : t -> float
Cudd_V
. Returns the value of the assumed constant ADDval cofactors : int -> t -> t * t
val cofactor : t -> Cudd.Bdd.dt -> t
val inspect : t -> add
val support : t -> Cudd.Bdd.dt
Cudd_Support
. Returns the support (positive cube) of the ADDval supportsize : t -> int
Cudd_SupportSize
. Returns the size of the support of the ADDval is_var_in : int -> t -> bool
Cuddaux_IsVarIn
. Does the given variable belong to the support of the ADD ?val vectorsupport : t array -> Cudd.Bdd.dt
Cudd_VectorSupport
. Returns the support of the array of ADDs.
Raises a Failure
exception in case where the array is of size 0 (in such
case, the manager is unknown, and we cannot return an empty support).
val vectorsupport2 : Cudd.Bdd.dt array -> t array -> Cudd.Bdd.dt
Cudd_VectorSupport
. Returns the support of the BDDs and ADDs arrays.
Raises a Failure
exception when both arrays are of size 0 (in such
case, the manager is unknown, and we cannot return an empty support).
val cst : Cudd.Man.dt -> float -> t
Cudd_addConst
. Return a constant ADD with the given value.val background : Cudd.Man.dt -> t
val ite : Cudd.Bdd.dt -> t -> t -> t
val ite_cst : Cudd.Bdd.dt -> t -> t -> t option
Cuddaux_addIteConstant
/Cudd_addIteConstant
. If-then-else operation, which succeeds only if the resulting node belongs to one of the two ADD.val eval_cst : t -> Cudd.Bdd.dt -> t option
val compose : int -> Cudd.Bdd.dt -> t -> t
val vectorcompose : ?memo:Cudd.Memo.t -> Cudd.Bdd.dt array -> t -> t
Cuddaux_addVectorCompose
/Cudd_addVectorCompose
.
Parallel substitution of every variable var
present in the manager by the
BDD table.(var)
in the ADD. You can optionnally control the memoization
policy, see Cudd.Memo
.val varmap : t -> t
Cuddaux_addVarMap
/Cudd_bddVarMap
. Permutes the variables as it has been specified with Cudd.Man.set_varmap
.val permute : ?memo:Cudd.Memo.t -> t -> int array -> t
Cudd_addPermute
.
Permutes the variables as it is specified by permut
(same format as in
Cudd.Man.set_varmap
). You can optionnally control the memoization policy, see
Cudd.Memo
.val is_equal : t -> t -> bool
Variation of Cudd_EquivDC
. Are the two ADDs equal when the BDD (careset) is true ?
val is_equal_when : t -> t -> Cudd.Bdd.dt -> bool
val is_eval_cst : t -> Cudd.Bdd.dt -> float option
Cuddaux_addEvalConst
/Cudd_addEvalConst
. Is the ADD constant when the BDD (careset) is true, and in this case what is its value ?val is_ite_cst : Cudd.Bdd.dt -> t -> t -> float option
ite
constant, and if it is the case, what is its value ?val size : t -> int
Cudd_DagSize
. Size if the ADD as a graph (the number of nodes).val nbpaths : t -> float
Cudd_CountPath
. Number of paths in the ADD from the root to the leafs.val nbnonzeropaths : t -> float
Cudd_CountPathsToNonZero
. Number of paths in the ADD from the root to non-zero leaves.val nbminterms : int -> t -> float
Cudd_CountMinterm
. Number of minterms of the ADD knowing that it depends on the given number of variables.val density : int -> t -> float
Cudd_Density
. Density of the ADD, which is the ratio of the number of minterms to the number of nodes. The ADD is assumed to depend on nvars
variables.val nbleaves : t -> int
Cudd_CountLeaves
. Number of leaves.val iter_cube : (Cudd.Man.tbool array -> float -> unit) -> t -> unit
Cudd.Bdd.iter_cube
val iter_node : (t -> unit) -> t -> unit
Cudd.Bdd.iter_node
val guard_of_node : t -> t -> Cudd.Bdd.dt
Cuddaux_addGuardOfNode
. guard_of_node f node
returns the sum of the paths leading from the root node f
to the node node
of f
.val guard_of_nonbackground : t -> Cudd.Bdd.dt
val nodes_below_level : t -> int option -> int -> t array
Cuddaux_NodesBelowLevel
. nodes_below_level f olevel max
returns all (if max<=0
), otherwise at most max
nodes pointed by the ADD, indexed by a variable of level greater or equal than level
, and encountered first in the top-down exploration (i.e., whenever a node is collected, its sons are not collected). If olevel=None
, then only constant nodes are collected. The background node may be in the result.val guard_of_leaf : t -> float -> Cudd.Bdd.dt
val leaves : t -> float array
val pick_leaf : t -> float
None
if the only leaf is the background leaf.val guardleafs : t -> (Cudd.Bdd.dt * float) array
Cudd.Bdd.constrain
, Cudd.Bdd.tdconstrain
, Cudd.Bdd.restrict
, Cudd.Bdd.tdrestrict
val constrain : t -> Cudd.Bdd.dt -> t
val tdconstrain : t -> Cudd.Bdd.dt -> t
val restrict : t -> Cudd.Bdd.dt -> t
val tdrestrict : t -> Cudd.Bdd.dt -> t
val of_bdd : Cudd.Bdd.dt -> t
Cudd_BddToAdd
. Conversion from BDD to 0-1 ADDval to_bdd : t -> Cudd.Bdd.dt
Cudd_addBddPattern
. Conversion from ADD to BDD by replacing all leaves different from 0 by true.val to_bdd_threshold : float -> t -> t
Cudd_addBddThreshold
. Conversion from ADD to BDD by replacing all leaves greater than or equal to the threshold by true.val to_bdd_strictthreshold : float -> t -> t
Cudd_addBddStrictThreshold
. Conversion from ADD to BDD by replacing all leaves strictly greater than the threshold by true.val to_bdd_interval : float -> float -> t -> t
Cudd_addBddInterval
. Conversion from ADD to BDD by replacing all leaves in the interval by true.val exist : Cudd.Bdd.dt -> t -> t
Cudd_addExistAbstract
. Abstracts all the variables in the cube from the ADD by summing over all possible values taken by those variables.val forall : Cudd.Bdd.dt -> t -> t
Cudd_addUnivAbstract
. Abstracts all the variables in the cube from the ADD by taking the product over all possible values taken by those variables.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
Cudd_addMatrixMultiply
.
matrix_multiply z A B
performs matrix multiplication of A
and B
, with z
being the summation variables, which means that they are used to refer columns
of A
and to rows of B
.
val times_plus : int array -> t -> t -> t
Cudd_addTimesPlus
.val triangle : int array -> t -> t -> t
Cudd_addTriangle
.val mapleaf1 : default:t ->
(Cudd.Bdd.dt -> float -> float) -> t -> t
val mapleaf2 : default:t ->
(Cudd.Bdd.dt -> float -> float -> float) ->
t -> t -> t
Cudd.User
for explanations.typeop1 =
(float, float) Cudd.Custom.op1
typeop2 =
(float, float, float) Cudd.Custom.op2
typeop3 =
(float, float, float, float) Cudd.Custom.op3
type
opN = {
|
commonN : |
|
closureN : |
|
arityNbdd : |
type
opG = {
|
commonG : |
|
arityGbdd : |
|
closureG : |
|
oclosureBeforeRec : |
|
oclosureIte : |
typetest2 =
(float, float) Cudd.Custom.test2
typeexist =
float Cudd.Custom.exist
typeexistand =
float Cudd.Custom.existand
typeexistop1 =
(float, float) Cudd.Custom.existop1
typeexistandop1 =
(float, float) Cudd.Custom.existandop1
val make_op1 : ?memo:Cudd.Memo.t -> (float -> float) -> op1
val make_op2 : ?memo:Cudd.Memo.t ->
?commutative:bool ->
?idempotent:bool ->
?special:(t -> t -> t option) ->
(float -> float -> float) -> op2
val make_op3 : ?memo:Cudd.Memo.t ->
?special:(t -> t -> t -> t option) ->
(float -> float -> float -> float) -> op3
val make_opN : ?memo:Cudd.Memo.t ->
int ->
int ->
(Cudd.Bdd.dt array -> t array -> t option) -> opN
val make_opG : ?memo:Cudd.Memo.t ->
?beforeRec:(int * bool ->
Cudd.Bdd.dt array ->
t array -> Cudd.Bdd.dt array * t array) ->
?ite:(int -> t -> t -> t) ->
int ->
int ->
(Cudd.Bdd.dt array -> t array -> t option) -> opG
val make_test2 : ?memo:Cudd.Memo.t ->
?symetric:bool ->
?reflexive:bool ->
?special:(t -> t -> bool option) ->
(float -> float -> bool) -> test2
val make_exist : ?memo:Cudd.Memo.t -> op2 -> exist
val make_existand : ?memo:Cudd.Memo.t -> bottom:float -> op2 -> existand
val make_existop1 : ?memo:Cudd.Memo.t -> op1:op1 -> op2 -> existop1
val make_existandop1 : ?memo:Cudd.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 -> Cudd.Bdd.dt array -> t array -> t
val apply_opG : opG -> Cudd.Bdd.dt array -> t array -> t
val apply_test2 : test2 -> t -> t -> bool
val apply_exist : exist -> supp:Cudd.Bdd.dt -> t -> t
val apply_existand : existand ->
supp:Cudd.Bdd.dt -> Cudd.Bdd.dt -> t -> t
val apply_existop1 : existop1 -> supp:Cudd.Bdd.dt -> t -> t
val apply_existandop1 : existandop1 ->
supp:Cudd.Bdd.dt -> Cudd.Bdd.dt -> t -> t
val map_op1 : ?memo:Cudd.Memo.t -> (float -> float) -> t -> t
val map_op2 : ?memo:Cudd.Memo.t ->
?commutative:bool ->
?idempotent:bool ->
?special:(t -> t -> t option) ->
(float -> float -> float) -> t -> t -> t
val map_op3 : ?memo:Cudd.Memo.t ->
?special:(t -> t -> t -> t option) ->
(float -> float -> float -> float) ->
t -> t -> t -> t
val map_opN : ?memo:Cudd.Memo.t ->
(Cudd.Bdd.dt array -> t array -> t option) ->
Cudd.Bdd.dt array -> t array -> t
val map_test2 : ?memo:Cudd.Memo.t ->
?symetric:bool ->
?reflexive:bool ->
?special:(t -> t -> bool option) ->
(float -> float -> bool) -> t -> t -> bool
val transfer : t -> Cudd.Man.d Cudd.Man.t -> t
val _print : t -> unit
val print__minterm : Format.formatter -> t -> unit
Cudd_Printminterm
.val print_minterm : (Format.formatter -> int -> unit) ->
(Format.formatter -> float -> unit) -> Format.formatter -> t -> unit
print_minterm print_id print_leaf fmt bdd
prints the minterms of the BDD using print_id
to print indices of variables and print_leaf
to print leaf values.val print : (Format.formatter -> int -> unit) ->
(Format.formatter -> float -> unit) -> Format.formatter -> t -> unit