Module Expr0.O

module O: sig .. end

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

val reg_of_expr : 'a Expr0.expr -> 'a 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 Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
       'b Expr0.t -> [> 'a Env.typ ]

Type of an expression

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

Expression representing the litteral var

val ite : 'a Bool.t -> 'a Expr0.t -> 'a Expr0.t -> 'a Expr0.t

If-then-else operation

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

Equality operation

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

Variable renaming. The new variables should already have been declared

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

Parallel substitution of variables by expressions

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

Support of the expression

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

Concatenates in an array the BDDs involved in the expressions

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

Print an expression

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

Print a BDD

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

Print the condition

Internal functions

Permutation and composition

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

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

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

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

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

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

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

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

Conversion to expressions

module Expr: sig .. end