Previous  Up  Next

Module Bddvar


module Bddvar: sig .. end
BDDs and discrete variables

This module allows to manipulate structured BDDs, where variables involved in the Boolean formula are not only Boolean variables, but also of bounded integer or enumerated type (such types are encoded with several Boolean variables).

Datatypes


type expr = [ `Benum of Bddenum.t | `Bint of Bddint.t | `Bool of Bdd.t ]
Expression
type typdef = [ `Benum of Var.t array | `Bint of bool * int ]
Type defintion
type typ = [ `Benum of Var.t | `Bint of bool * int | `Bool ]
Types

type info = {
   tid : int array; (*(Sorted) array of involved BDD indices.*)
   var : expr; (*Expression representing the literal*)
}
Information associated to each variable
class type [[[> typ ], [> typdef ]]] db = object .. end
Database

Database


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

Expressions


val typ_of_expr : expr -> [> typ ]
Type of an expression
val var : ([> typ ], [> typdef ]) #db -> Var.t -> expr
Expression representing the litteral var
val ite : Bdd.t -> expr -> expr -> expr
If-then-else operation
val rename : ([> typ ], [> typdef ]) #db ->
       expr -> (Var.t * Var.t) list -> expr
Variable renaming. The new variables should already have been declared
val substitute : ([> typ ], [> typdef ]) #db ->
       expr -> (Var.t * expr) list -> expr
Parallel substitution of variables by expressions
val exist : ([> typ ], [> typdef ]) #db ->
       expr -> Var.t list -> expr
Existential quantification of a set of variables
val forall : ([> typ ], [> typdef ]) #db ->
       expr -> Var.t list -> expr
Universal quantification of a set of variables
val cofactor : expr -> Bdd.t -> expr
val tdrestrict : expr -> Bdd.t -> expr
val support_cond : ([> typ ], [> typdef ]) #db -> expr -> Bdd.t
Return the support of an expression as a conjunction of the BDD identifiers involved in the expression
val vectorsupport_cond : ([> typ ], [> typdef ]) #db ->
       expr array -> Bdd.t
Return the support of an array of expressions as a conjunction of the BDD identifiers involved in the expressions

Miscellaneous


val cube_of_bdd : ([> typ ], [> typdef ]) #db -> Bdd.t -> Bdd.t
Same as Bdd.cube_of_bdd, but keep only the the values of variables having a determinated value.

Example: the classical Bdd.cube_of_bdd could return b and (x=1 or x=3), whereas cube_of_bdd will return only b in such a case.

val iter_ordered : ([> typ ], [> typdef ]) #db ->
       (Var.t -> info -> unit) -> unit
Iter on all variables declared in the database

Printing


val print_db : Format.formatter -> ([> typ ], [> typdef ]) #db -> unit
Print the database
val print_typ : Format.formatter -> typ -> unit
Print a type
val print_typdef : Format.formatter -> typdef -> unit
Print a type definition
val print_expr : ([> typ ], [> typdef ]) #db ->
       Format.formatter -> expr -> unit
Print an expression
val print_minterm : ([> typ ], [> typdef ]) #db ->
       Format.formatter -> Manager.tbool array -> unit
Print a minterm
val print_bdd : ([> typ ], [> typdef ]) #db ->
       Format.formatter -> Bdd.t -> unit
Print a BDD
val print_idd : ([> typ ], [> typdef ]) #db ->
       (Format.formatter -> int -> unit) -> Format.formatter -> Idd.t -> unit
Print an IDD, using the function to associate to leaf indices strings.
val print_idcondb : ([> typ ], [> typdef ]) #db ->
       Format.formatter -> int * bool -> unit
Print the condition represented by the signed BDD index.
val print_idcond : ([> typ ], [> typdef ]) #db ->
       Format.formatter -> int -> unit
Print the condition

Internal


val print_info : Format.formatter -> info -> unit
Print an object of type info

Internal functions



Permutation and composition


val permutation_of_rename : ([> typ ], [> typdef ]) #db ->
       (Var.t * Var.t) list -> int array
val composition_of_substitution : ([> typ ], [> typdef ]) #db ->
       (Var.t * expr) list -> Bdd.t array
val bddsupport : ([> typ ], [> typdef ]) #db -> Var.t list -> Bdd.t
val permute : expr -> int array -> expr
val compose : expr -> Bdd.t array -> expr

Access functions


val mem_id : ([> typ ], [> typdef ]) #db -> int -> bool
Is the BDD index managed by the database ?
val varinfo_of_id : ([> typ ], [> typdef ]) #db ->
       int -> Var.t * info
Return the variable and info involved by the BDD index
val print_id : ([> typ ], [> typdef ]) #db ->
       Format.formatter -> int -> unit
Print the name associated to the single BDD index. If name is the name of the associated variable, and I the rank of the argument in the register, then it prints 
val info_of_var : ([> typ ], [> typdef ]) #db -> Var.t -> info
info associated to the variable in db
val reg_of_expr : expr -> Bdd.t array
Return the underlying array of BDD representing the expression

Conversion to expressions


module Expr: sig .. end