Previous  Up  

Module Cudd.Add

module Add: sig .. end
type t
Abstract type for ADDs (that are necessarily attached to a manager of type 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 float (*Terminal value*)
| Ite of int * t * t (*Decision on CUDD variable*)
Public type for exploring the abstract type t

Extractors


val manager : t -> Cudd.Man.dt
Returns the manager associated to the ADD
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 ADD
val delse : t -> t
Cudd_E. Returns the negative subnode of the ADD
val dval : t -> float
Cudd_V. Returns the value of the assumed constant ADD
val cofactors : int -> t -> t * t
Returns the positive and negative cofactor of the ADD wrt the variable
val cofactor : t -> Cudd.Bdd.dt -> t
Cudd_Cofactor. cofactor add cube evaluates add on the cube cube
val inspect : t -> add
Decomposes the top node of the ADD

Supports


val support : t -> Cudd.Bdd.dt
Cudd_Support. Returns the support (positive cube) of the ADD
val supportsize : t -> int
Cudd_SupportSize. Returns the size of the support of the ADD
val 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).


Classical operations


val cst : Cudd.Man.dt -> float -> t
Cudd_addConst. Return a constant ADD with the given value.
val background : Cudd.Man.dt -> t
Cuddaux_addIte/Cudd_addIte. If-then-else operation, with the condition being a BDD.
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
Cuddaux_addEvalConst/Cudd_addEvalConst.
val compose : int -> Cudd.Bdd.dt -> t -> t
Cuddaux_addCompose/Cudd_addCompose. Substitutes the variable with the BDD in the ADD.
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.

Variable mapping


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.

Logical tests


val is_equal : t -> t -> bool
Equality test

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
Variation of 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
Is the result of ite constant, and if it is the case, what is its value ?

Structural information


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.

Iterators


val iter_cube : (Cudd.Man.tbool array -> float -> unit) -> t -> unit
Similar to Cudd.Bdd.iter_cube
val iter_node : (t -> unit) -> t -> unit
Similar to Cudd.Bdd.iter_node

Leaves and guards


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
Guard of non background leaves
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
Guard of the given leaf
val leaves : t -> float array
Returns the set of leaf values (excluding the background value)
val pick_leaf : t -> float
Picks (but not randomly) a non background leaf. Return None if the only leaf is the background leaf.
val guardleafs : t -> (Cudd.Bdd.dt * float) array
Returns the set of leaf values together with their guard in the ADD

Minimizations



See 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

Conversions


val of_bdd : Cudd.Bdd.dt -> t
Cudd_BddToAdd. Conversion from BDD to 0-1 ADD
val 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.

Quantifications


val exist : Cudd.Bdd.dt -> t -> t
Variation of 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
Variation of Cudd_addUnivAbstract. Abstracts all the variables in the cube from the ADD by taking the product over all possible values taken by those variables.

Algebraic operations


val is_leq : t -> t -> bool
Cudd_addLeq.
val add : t -> t -> t
Cudd_addPlus.
val sub : t -> t -> t
Cudd_addMinus.
val mul : t -> t -> t
Cudd_addTimes.
val div : t -> t -> t
Cudd_addDivide.
val min : t -> t -> t
Cudd_addMinimum.
val max : t -> t -> t
Cudd_addMaximum.
val agreement : t -> t -> t
Cudd_addAgreement.
val diff : t -> t -> t
Cudd_addDiff.
val threshold : t -> t -> t
Cudd_addThreshold.
val setNZ : t -> t -> t
Cudd_addSetNZ.
val log : t -> t
Cudd_addLog.

Matrix operations


val matrix_multiply : int array -> t -> t -> t
Variation of 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
Variation of Cudd_addTimesPlus.
val triangle : int array -> t -> t -> t
Variation of Cudd_addTriangle.

User operations



By decomposition into guards and leaves


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

By using CUDD cache



Consult Cudd.User for explanations.

Type of operations

type op1 = (float, float) Cudd.Custom.op1 
type op2 = (float, float, float) Cudd.Custom.op2 
type op3 = (float, float, float, float) Cudd.Custom.op3 
type opN = {
   commonN :Cudd.Custom.common;
   closureN :Cudd.Bdd.dt array -> t array -> t option;
   arityNbdd :int;
} 
type opG = {
   commonG :Cudd.Custom.common;
   arityGbdd :int;
   closureG :Cudd.Bdd.dt array -> t array -> t option;
   oclosureBeforeRec :(int * bool ->
Cudd.Bdd.dt array ->
t array -> Cudd.Bdd.dt array * t array)
option;
   oclosureIte :(int -> t -> t -> t) option;
} 
type test2 = (float, float) Cudd.Custom.test2 
type exist = float Cudd.Custom.exist 
type existand = float Cudd.Custom.existand 
type existop1 = (float, float) Cudd.Custom.existop1 
type existandop1 = (float, float) Cudd.Custom.existandop1 
val make_op1 : ?memo:Cudd.Memo.t -> (float -> float) -> op1
Making operations

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

Clearing memoization tables

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

Applying operations

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

Map functions

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

Miscellaneous


val transfer : t -> Cudd.Man.d Cudd.Man.t -> t
Cuddaux_addTransfer/Cudd_bddTransfer. Transfers a ADD to a different manager.

Printing


val _print : t -> unit
C printing function. The output may mix badly with the OCaml output.
val print__minterm : Format.formatter -> t -> unit
Prints the minterms of the BDD in the same way as 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
Prints a BDD by recursively decomposing it as monomial followed by a tree.