Module Bddoutput


module Bddoutput: sig .. end
Output of BDDs/MTBDDs


Types



type bnode =
| BIte of int * int * bool * int (*BIte(idcond,idnodeThen,signElse,idnodeElse)*)
| BTrue (*Terminal case. Not needed in principle*)
BDD node

type inode =
| IIte of int * int * int (*IIte(idcond,idnodeThen,idnodeElse)*)
| ICst of int (*Leaf*)
IDD node

type 'a db = {
   mutable cond : SetteI.t; (*Reachable conditions*)
   mutable ileaf : SetteI.t; (*Reachable IDD leafs*)
   bhash : (Bdd.t, int) Hashtbl.t;
   ihash : (Idd.t, int) Hashtbl.t;
   mutable blastid : int;
   mutable ilastid : int; (*Hashtables and Counters for resp. first free BDD or IDD node*)
   mutable bdef : bnode MappeI.t; (*Global BDDs graph*)
   mutable idef : (inode * 'a) MappeI.t; (*Global IDDs graph*)
   mutable ileafattr : int -> 'a; (*Synthetized attribute for a leaf IDD node*)
   mutable inodeattr : int -> 'a -> 'a -> 'a; (*Synthetized attribute for a non-leaf IDD node*)
}
Database

Functions


val make_db : (int -> 'a) -> (int -> 'a -> 'a -> 'a) -> 'a db
Create a database for printing BDDs/IDDs.

make_db leafattr nodeattr creates a database with the attribute functions

val clear_db : 'a db -> unit
Clear the database
val signid_of_bdd : 'a db -> Bdd.t -> bool * int
Output the BDD and return its identifier
val idattr_of_idd : 'a db -> Idd.t -> int * 'a
Output the IDD and return its identifier
val iter_cond : 'a db -> (int -> unit) -> unit
Iterate the function on all the registered conditions
val iter_cond_ordered : 'a db -> Manager.t -> (int -> unit) -> unit
Iterate the function on all the registered conditions, from level 0 to higher levels.
val iter_bdef_ordered : 'a db -> (int -> bnode -> unit) -> unit
Iterate on definitions of BDD identifiers, in a topological order.
val iter_idef_ordered : 'a db -> (int -> inode * 'a -> unit) -> unit
Iterate on definitions of IDD identifiers, in a topological order.