Module Bdd.Expr0.O

module O: sig .. end

val tid_of_var : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'a -> int array

val reg_of_expr : 'd Bdd.Expr0.expr -> 'd Cudd.Bdd.t array

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, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Expr0.t -> [> 'a Bdd.Env.typ ]

Type of an expression

val var : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'a -> 'd Bdd.Expr0.t

Expression representing the litteral var

val ite : 'd Bool.t -> 'd Bdd.Expr0.t -> 'd Bdd.Expr0.t -> 'd Bdd.Expr0.t

If-then-else operation

val eq : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Expr0.t -> 'd Bdd.Expr0.t -> 'd Bool.t

Equality operation

val substitute_by_var : ?memo:Cudd.Memo.t ->
       ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Expr0.t -> ('a * 'a) list -> 'd Bdd.Expr0.t

val substitute_by_var_list : ?memo:Cudd.Memo.t ->
       ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Expr0.t list -> ('a * 'a) list -> 'd Bdd.Expr0.t list

Variable renaming. The new variables should already have been declared

val substitute : ?memo:Cudd.Memo.t ->
       ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Expr0.t -> ('a * 'd Bdd.Expr0.t) list -> 'd Bdd.Expr0.t

val substitute_list : ?memo:Cudd.Memo.t ->
       ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Expr0.t list -> ('a * 'd Bdd.Expr0.t) list -> 'd Bdd.Expr0.t list

Parallel substitution of variables by expressions

val support : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Bdd.Expr0.t -> 'a PSette.t

Support of the expression

val support_cond : 'd Cudd.Man.t -> 'd Bdd.Expr0.t -> 'd 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, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'd Cudd.Bdd.t -> 'd 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 tbdd_of_texpr : 'd Bdd.Expr0.t array -> 'd Cudd.Bdd.t array

Concatenates in an array the BDDs involved in the expressions

val texpr_of_tbdd : 'd Bdd.Expr0.t array -> 'd Cudd.Bdd.t array -> 'd Bdd.Expr0.t array

Inverse operation: rebuild an array of expressions from the old array of expressions (for the types) and the array of BDDs.

Printing

val print : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
       ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       Format.formatter -> [< 'd Bdd.Expr0.t ] -> unit

Print an expression

val print_minterm : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
       ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       Format.formatter -> Cudd.Man.tbool array -> unit

Print a minterm

val print_bdd : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
       ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       Format.formatter -> 'd Cudd.Bdd.t -> unit

Print a BDD

val print_idcondb : ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
       ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.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, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       Format.formatter -> int -> unit

Print the condition

Internal functions

Permutation and composition

val permutation_of_rename : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       ('a * 'a) list -> int array

val composition_of_lvarexpr : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       ('a * 'd Bdd.Expr0.t) list -> 'd Cudd.Bdd.t array

val composition_of_lvarlexpr : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'a list -> 'd Bdd.Expr0.t list -> 'd Cudd.Bdd.t array

val bddsupport : ('a, [> 'a Bdd.Env.typ ], [> 'a Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
       'a list -> 'd Cudd.Bdd.t

val varmap : 'a Bdd.Expr0.t -> 'a Bdd.Expr0.t

val permute : ?memo:Cudd.Memo.t -> 'd Bdd.Expr0.t -> int array -> 'd Bdd.Expr0.t

val compose : ?memo:Cudd.Memo.t -> 'd Bdd.Expr0.t -> 'd Cudd.Bdd.t array -> 'd Bdd.Expr0.t

val permute_list : ?memo:Cudd.Memo.t -> 'd Bdd.Expr0.t list -> int array -> 'd Bdd.Expr0.t list

val compose_list : ?memo:Cudd.Memo.t ->
       'd Bdd.Expr0.t list -> 'd Cudd.Bdd.t array -> 'd Bdd.Expr0.t list

Conversion to expressions

module Expr: sig .. end