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

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.