module Output: sig
.. end
Output of BDDs/MTBDDs
Types
type
bnode =
| |
BIte of int * int * bool * int |
| |
BTrue |
BDD node
type 'a
bdd = {
|
cond : int PSette.t Pervasives.ref ; |
|
mutable bdef : (int, bnode) PMappe.t ; |
|
bhash : ('a Cudd.Bdd.t, int) Hashhe.t ; |
|
mutable blastid : int ; |
}
Database
type 'a
vnode =
| |
VIte of int * int * int |
| |
VCst of 'a |
MTBDD node
type 'a
vdd = {
|
cond : int PSette.t Pervasives.ref ; |
|
mutable vdef : (int, 'a vnode) PMappe.t ; |
|
lhash : ('a, unit) PHashhe.t ; |
|
vhash : ('a Cudd.Vdd.t, int) Hashhe.t ; |
|
mutable vlastid : int ; |
}
Database
type
anode =
| |
AIte of int * int * int |
| |
ACst of float |
ADD node
type
add = {
|
cond : int PSette.t Pervasives.ref ; |
|
mutable adef : (int, anode) PMappe.t ; |
|
mutable lset : float Sette.t ; |
|
ahash : (Cudd.Add.t, int) Hashhe.t ; |
|
mutable alastid : int ; |
}
Database
val make_bdd : cond:int PSette.t Pervasives.ref -> 'a bdd
Functions
Create a database for printing BDDs
cond
allows to share the same set of conditions between
BDDs and MTBDDs.
val signid_of_bdd : 'a bdd -> 'a Cudd.Bdd.t -> bool * int
Output the BDD and return its identifier
val make_vdd : compare:'a Cudd.PWeakke.compare ->
cond:int PSette.t Pervasives.ref -> 'a vdd
val make_mtbdd : table:'a Cudd.Mtbdd.table ->
cond:int PSette.t Pervasives.ref -> 'a Cudd.Mtbdd.unique vdd
val make_mtbddc : table:'a Cudd.Mtbddc.table ->
cond:int PSette.t Pervasives.ref -> 'a Cudd.Mtbddc.unique vdd
Create a database for printing MTBDDs
cond
allows to share the same set of conditions between
BDDs and MTBDDs.
val id_of_vdd : 'a vdd -> 'a Cudd.Vdd.t -> int
Output the MTBDD and return its identifier
val iter_cond_ordered : int PSette.t -> 'a Cudd.Man.t -> (int -> unit) -> unit
Iterate the function on all the registered conditions, from level 0
to higher levels.
val iter_bdef_ordered : 'a bdd -> (int -> bnode -> unit) -> unit
Iterate on definitions of BDD identifiers, in a topological order.
val iter_vdef_ordered : 'a vdd -> (int -> 'a vnode -> unit) -> unit
Iterate on definitions of MTBDD identifiers, in a topological order.