Up  Next

Module Bdd.Output

module Output: sig .. end

Types


type bnode =
| BIte of int * int * bool * int (*BIte(idcond,idnodeThen,signElse,idnodeElse)*)
| BTrue (*Terminal case. Not needed in principle*)
BDD node
type 'a bdd = {
   cond :int PSette.t Pervasives.ref; (*Reachable conditions*)
   mutable bdef :(int, bnode) PMappe.t; (*Global BDDs graph*)
   bhash :('a Cudd.Bdd.t, int) Hashhe.t;
   mutable blastid :int; (*Hashtables and Counters for resp. first free BDD or IDD node*)
}
Database
type 'a vnode =
| VIte of int * int * int (*VIte(idcond,idnodeThen,idnodeElse)*)
| VCst of 'a (*Leaf*)
MTBDD node
type 'a vdd = {
   cond :int PSette.t Pervasives.ref; (*Reachable conditions*)
   mutable vdef :(int, 'a vnode) PMappe.t; (*Global MTBDDs graph*)
   lhash :('a, unit) PHashhe.t;
   vhash :('a Cudd.Vdd.t, int) Hashhe.t;
   mutable vlastid :int; (*Hashtables and Counters for MTBDD nodes.*)
}
Database
type anode =
| AIte of int * int * int (*AIte(idcond,idnodeThen,idnodeElse)*)
| 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.