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

Expressions

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

Miscellaneous

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.

Printing

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