Module Bdd.Expr0

module Expr0: sig .. end

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).


type 'a t = [ `Benum of 'a Bdd.Enum.t | `Bint of 'a Bdd.Int.t | `Bool of 'a Cudd.Bdd.t ] 
type 'a expr = 'a t 
Type of general expressions
type dt = Cudd.Man.d t 
type vt = Cudd.Man.v t 

General expressions are described below, after Boolean, bounded integer and enumerated types expressions

Boolean expressions

module Bool: sig .. end

Bounded integer expressions

module Bint: sig .. end

Enumerated expressions

module Benum: sig .. end

General (typed) expressions

The following operations raise a Failure exception in case of a typing error.
val typ_of_expr : ('a, 'b) Bdd.Env.t -> 'b t -> 'a Bdd.Env.typ
Type of an expression
val var : ('a, 'b) Bdd.Env.t -> 'a -> 'b t
Expression representing the litteral var
val ite : 'a Bool.t -> 'a t -> 'a t -> 'a t
If-then-else operation
val eq : ('a, 'b) Bdd.Env.t -> 'b t -> 'b t -> 'b Bool.t
Equality operation
val substitute_by_var : ?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Env.t -> 'b t -> ('a * 'a) list -> 'b t
val substitute_by_var_list : ?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Env.t ->
'b t list -> ('a * 'a) list -> 'b t list
Variable renaming.

The new variables should already have been declared

val substitute : ?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Env.t ->
'b t -> ('a * 'b t) list -> 'b t
val substitute_list : ?memo:Cudd.Memo.t ->
('a, 'b) Bdd.Env.t ->
'b t list -> ('a * 'b t) list -> 'b t list
Parallel substitution of variables by expressions
val cofactor : 'a t -> 'a Cudd.Bdd.t -> 'a t
Evaluate the expression. The BDD is assumed to be a cube
val restrict : 'a t -> 'a Cudd.Bdd.t -> 'a t
val tdrestrict : 'a t -> 'a Cudd.Bdd.t -> 'a t
Simplify the expression knowing that the BDD is true. Generalizes cofactor.
val support : ('a, 'b) Bdd.Env.t -> 'b t -> 'a PSette.t
Support of the expression
val support_cond : 'a Cudd.Man.t -> 'a t -> 'a Cudd.Bdd.t
Return the support of an expression as a conjunction of the BDD identifiers involved in the expression


val cube_of_bdd : ('a, 'b) Bdd.Env.t -> 'b Cudd.Bdd.t -> 'b Cudd.Bdd.t
Same as Cudd.Bdd.cube_of_bdd, but keep only the the values of variables having a determinated value.

Example: the classical Cudd.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 print : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t -> Format.formatter -> 'b t -> unit
Print an expression
val print_minterm : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t -> Format.formatter -> Cudd.Man.tbool array -> unit
Print a minterm
val print_bdd : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t -> Format.formatter -> 'b Cudd.Bdd.t -> unit
Print a BDD
val print_idcondb : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t -> Format.formatter -> int * bool -> unit
Print the condition represented by the signed BDD index.
val print_idcond : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
('a, 'b) Bdd.Env.t -> Format.formatter -> int -> unit
Print the condition

Opened signature and Internal functions

We provide here the same functions and modules as before, but with opened types (this allows etxensions). The functions above are axtually derived from the functions below by just constraining their types. We provide here also more internal functions
module O: sig .. end