Previous  Up  Next

Module Cudd.Vdd

module Vdd: sig .. end
type +'a t
Type of VDDs (that are necessarily attached to a manager of type Man.v 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.Vdd.manager. Objects of this type are automatically garbage collected.

type 'a vdd =
| Leaf of 'a (*Terminal value*)
| Ite of int * 'a t * 'a t (*Decision on CUDD variable*)
Public type for exploring the abstract type t

We refer to the module Cudd.Add for the description of the interface, as it is nearly identical to Cudd.Add, except that real leaves are replaced by OCaml leaves.

IMPORTANT NOTE: this is an internal module, which assumes that leaves are either immediate values (booleans, integers, constant sums), or values allocated with caml_alloc_shr (that can be moved only during a memory compaction).

The only case where you may use directly Cudd.Vdd without worrying is when the leaves are represented as immediate values (booleans, integers, constant sums) in the heap.

Otherwise, use module Cudd.Mtbdd or Cudd.Mtbddc to be safe, and also to ensure that you do not have two constant MTBDDs pointing to different but semantically equivalent values.

Extractors


val manager : 'a t -> Cudd.Man.v Cudd.Man.t
val is_cst : 'a t -> bool
val topvar : 'a t -> int
val dthen : 'a t -> 'a t
val delse : 'a t -> 'a t
val cofactors : int -> 'a t -> 'a t * 'a t
val cofactor : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a t
val dval : 'a t -> 'a
val inspect : 'a t -> 'a vdd

Supports


val support : 'a t -> Cudd.Man.v Cudd.Bdd.t
val supportsize : 'a t -> int
val is_var_in : int -> 'a t -> bool
val vectorsupport : 'a t array -> Cudd.Man.v Cudd.Bdd.t
val vectorsupport2 : Cudd.Man.v Cudd.Bdd.t array -> 'a t array -> Cudd.Man.v Cudd.Bdd.t

Classical operations


val cst : Cudd.Man.v Cudd.Man.t -> 'a -> 'a t
val _background : Cudd.Man.v Cudd.Man.t -> 'a t
Be cautious, it is not type safe (if you use Cudd.Vdd.nodes_below_level, etc...: you can try to retrieve a constant value of some type and () value of the background value will be treated as another type.
val ite : Cudd.Man.v Cudd.Bdd.t -> 'a t -> 'a t -> 'a t
val ite_cst : Cudd.Man.v Cudd.Bdd.t ->
       'a t -> 'a t -> 'a t option
val eval_cst : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a t option
val compose : int -> Cudd.Bdd.vt -> 'a t -> 'a t
val vectorcompose : ?memo:Cudd.Memo.t -> Cudd.Bdd.vt array -> 'a t -> 'a t

Logical tests


val is_equal : 'a t -> 'a t -> bool
val is_equal_when : 'a t -> 'a t -> Cudd.Man.v Cudd.Bdd.t -> bool
val is_eval_cst : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a option
val is_ite_cst : Cudd.Man.v Cudd.Bdd.t -> 'a t -> 'a t -> 'a option

Structural information


val size : 'a t -> int
val nbpaths : 'a t -> float
val nbnonzeropaths : 'a t -> float
val nbminterms : int -> 'a t -> float
val density : int -> 'a t -> float
val nbleaves : 'a t -> int

Variable mapping


val varmap : 'a t -> 'a t
val permute : ?memo:Cudd.Memo.t -> 'a t -> int array -> 'a t
Variant with controllable memoization policy.

Iterators


val iter_cube : (Cudd.Man.tbool array -> 'a -> unit) -> 'a t -> unit
val iter_node : ('a t -> unit) -> 'a t -> unit

Leaves and guards


val guard_of_node : 'a t -> 'a t -> Cudd.Man.v Cudd.Bdd.t
val guard_of_nonbackground : 'a t -> Cudd.Man.v Cudd.Bdd.t
val nodes_below_level : ?max:int -> 'a t -> int option -> 'a t array
Cuddaux_NodesBelowLevel. nodes_below_level ?max f olevel returns all (if max=None), otherwise at most Some 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.
val guard_of_leaf : 'a t -> 'a -> Cudd.Man.v Cudd.Bdd.t
Guard of the given leaf
val leaves : 'a t -> 'a array
Returns the set of leaf values (excluding the background value)
val pick_leaf : 'a t -> 'a
Picks (but not randomly) a non background leaf. Return None if the only leaf is the background leaf.
val guardleafs : 'a t -> (Cudd.Man.v Cudd.Bdd.t * 'a) array
Returns the set of leaf values together with their guard in the ADD

Minimizations


val constrain : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a t
val tdconstrain : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a t
val restrict : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a t
val tdrestrict : 'a t -> Cudd.Man.v Cudd.Bdd.t -> 'a t

Conversions



User operations



Two options:

Miscellaneous


val transfer : 'a t -> Cudd.Man.v Cudd.Man.t -> 'a t

Printing


val print__minterm : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
val print_minterm : (Format.formatter -> int -> unit) ->
       (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
val print : (Format.formatter -> Cudd.Man.v Cudd.Bdd.t -> unit) ->
       (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit