module Vdd:sig
..end
type +'a
t
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 |
(* | Terminal value | *) |
| |
Ite of |
(* | Decision on CUDD variable | *) |
t
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
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
val cst : Cudd.Man.v Cudd.Man.t -> 'a -> 'a t
val _background : Cudd.Man.v Cudd.Man.t -> 'a t
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
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
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
val varmap : 'a t -> 'a t
val permute : ?memo:Cudd.Memo.t -> 'a t -> int array -> 'a t
val iter_cube : (Cudd.Man.tbool array -> 'a -> unit) -> 'a t -> unit
val iter_node : ('a t -> unit) -> 'a t -> unit
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
val leaves : 'a t -> 'a array
val pick_leaf : 'a t -> 'a
None
if the only leaf is the background leaf.val guardleafs : 'a t -> (Cudd.Man.v Cudd.Bdd.t * 'a) array
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
Cudd.Mapleaf
Cudd.User
val transfer : 'a t -> Cudd.Man.v Cudd.Man.t -> 'a t
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