Module Enum

module Enum: sig .. end

Enumerated expressions with BDDs

Types

type 'a typ = [ `Benum of 'a ]

A type is just a name

type 'a typdef = [ `Benum of 'a array ]

An enumerated type is defined by its (ordered) set of labels

Datatype representing a BDD register of enumerated type

type 'a t = {

	`typ : string;`	`(*`	Type of the value (refers to the database, see below)	`*)`
	`reg : 'a Reg.t;`	`(*`	Value itself	`*)`

}

type dt = Cudd.Man.d t

type vt = Cudd.Man.v t

Constants and Operation(s)

val of_label : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> 'a -> 'b t

Create a register of the type of the label containing the label

val is_cst : 'a t -> bool

Does the register contain a constant value ?

val to_code : 'a t -> int

Convert a constant register to its value as a code.

val to_label : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> 'b t -> 'a

Convert a constant register to its value as a label.

val equal_label : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
       'b t -> 'a -> 'b Cudd.Bdd.t

Under which condition the register is equal to the label ?

val equal : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
       'b t -> 'b t -> 'b Cudd.Bdd.t

Under which condition the 2 registers are equal ?

val ite : 'a Cudd.Bdd.t -> 'a t -> 'a t -> 'a t

If-then-else operator. The types of the 2 branches should be the same.

Decomposition in guarded form

val guard_of_label : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
       'b t -> 'a -> 'b Cudd.Bdd.t

Return the guard of the label in the BDD register.

val guardlabels : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
       'b t -> ('b Cudd.Bdd.t * 'a) list

Return the list g -> label represented by the BDD register.

Evaluation

val cofactor : 'a t -> 'a Cudd.Bdd.t -> 'a t

val restrict : 'a t -> 'a Cudd.Bdd.t -> 'a t

val tdrestrict : 'a t -> 'a Cudd.Bdd.t -> 'a t

Printing

val print : (Format.formatter -> int -> unit) -> Format.formatter -> 'a t -> unit

print f fmt t prints the register t using the formatter fmt and the function f to print BDDs indices.

val print_minterm : (Format.formatter -> 'a Cudd.Bdd.t -> unit) ->
       ('b, [> 'b Env.typ ], [> 'b Env.typdef ], 'a, 'c) Env.O.t ->
       Format.formatter -> 'a 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 : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> 'a -> int

Return the cardinality of a type (the number of its labels)

val maxcode_of_typ : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> 'a -> 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 : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
       'a -> int -> bool

Does the integer code some label of the given type ?

val labels_of_typ : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> 'a -> 'a array

Return the array of labels defining the type

val code_of_label : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> 'a -> int

Return the code associated to the label

val label_of_typcode : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t -> 'a -> int -> 'a

Return the label associated to the given code interpreted as of type the given type.

module Minterm: sig .. end

val permute : ?memo:Cudd.Memo.t -> 'a t -> int array -> 'a t

Permutation (scale Cudd.Bdd.permute and Cudd.Bdd.permute_memo)

val varmap : 'a t -> 'a t

Permutation (scale Cudd.Bdd.varmap)

val vectorcompose : ?memo:Cudd.Memo.t -> 'a Cudd.Bdd.t array -> 'a t -> 'a t

Composition (scale Cudd.Bdd.vectorcompose and Cudd.Bdd.vectorcompose_memo)