module Bddenum: sig .. end
Enumerated types with BDDs
Types
type Var.t
A label is just a name
type [ `Benum of Var.t ]
A type is just a name
type [ `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
}
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