Module Bddenum


module Bddenum: sig .. end
Enumerated types with BDDs


Types


type label = Var.t 
A label is just a name
type typ = [ `Benum of Var.t ] 
A type is just a name
type typdef = [ `Benum of Var.t array ] 
An enumerated type is defined by its (ordered) set of labels

Datatype representing a BDD register of enumerated type



type t = {
   typ : Var.t; (*Type of the value (refers to the database, see below)*)
   reg : Bddreg.t; (*Value itself*)
}

Database



We need a global store where we register type names with their type definitions, and also an auxiliary table to efficiently associate types to labels.
class type [[[> typ ], [> typdef ]]] db = object .. end

Database


class [[[> typ ], [> typdef ]]] make_db : Manager.t -> [[[> typ ] as 'a, [> typdef ] as 'b]] db
Creation of a database

Constants and Operation(s)


val of_label : ([> typ ], [> typdef ]) #db ->
label -> t
Create a register of the type of the label containing the label
val is_cst : t -> bool
Does the register contain a constant value ?
val to_code : t -> int
Convert a constant register to its value as a code.
val to_label : ([> typ ], [> typdef ]) #db ->
t -> label
Convert a constant register to its value as a label.
val equal_label : ([> typ ], [> typdef ]) #db ->
t -> label -> Bdd.t
Under which condition the register is equal to the label ?
val equal : ([> typ ], [> typdef ]) #db ->
t -> t -> Bdd.t
Under which condition the 2 registers are equal ?
val ite : Bdd.t -> t -> t -> t
If-then-else operator. The types of the 2 branches should be the same.

Decomposition in guarded form


val guard_of_label : ([> typ ], [> typdef ]) #db ->
t -> label -> Bdd.t
Return the guard of the label in the BDD register.
val guardlabels : ([> typ ], [> typdef ]) #db ->
t -> (Bdd.t * label) list
Return the list g -> label represented by the BDD register.

Printing


val print_db : Format.formatter ->
([> typ ], [> typdef ]) #db -> unit
Print the database
val print : (int -> string) -> Format.formatter -> t -> unit
print f fmt t prints the register t using the formatter fmt and the function f to convert BDDs indices to names.
val print_minterm : (Format.formatter -> Bdd.t -> unit) ->
([> typ ], [> typdef ]) #db ->
Format.formatter -> t -> unit
print_minterm f fmt t prints the register t using the formatter fmt and the function f to convert BDDs indices to names.

Internal functions


val size_of_typ : ([> typ ], [> typdef ]) #db -> Var.t -> int
Return the cardinality of a type (the number of its labels)
val maxcode_of_typ : ([> typ ], [> typdef ]) #db -> Var.t -> int
Return the maximal integer corresponding to a label belonging to the type. Labels are indeed associated numbers from 0 to this number.
val mem_typcode : ([> typ ], [> typdef ]) #db -> Var.t -> int -> bool
Does the integer code some label of the given type ?
val labels_of_typ : ([> typ ], [> typdef ]) #db ->
Var.t -> label array
Return the array of labels defining the type
val code_of_label : ([> typ ], [> typdef ]) #db -> label -> int
Return the code associated to the label
val label_of_typcode : ([> typ ], [> typdef ]) #db ->
Var.t -> int -> label
Return the label associated to the given code interpreted as of type the given type.
module Minterm: sig .. end