Module Bdd.Expr1

module Expr1: sig .. end


type ('a, 'b) t = (('a, 'b) Bdd.Env.t, 'b Bdd.Expr0.t) Bdd.Env.value 
type ('a, 'b) expr = ('a, 'b) t 
Type of general expressions
type 'a dt = ('a, Cudd.Man.d) t 
type 'a vt = ('a, 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 expressions

val typ_of_expr : ('a, 'b) t -> 'a Bdd.Env.typ
Type of an expression
val make : ('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.t -> ('a, 'b) t
val of_expr0 : ('a, 'b) Bdd.Env.t -> 'b Bdd.Expr0.t -> ('a, 'b) t
Creation from an expression of level 0 (without environment) (make should be considered as obsolete)
val get_env : ('a, 'b) t -> ('a, 'b) Bdd.Env.t
val to_expr0 : ('a, 'b) t -> 'b Bdd.Expr0.t
Extract resp. the environment and the underlying expression of level 0
val extend_environment : ('a, 'b) t -> ('a, 'b) Bdd.Env.t -> ('a, 'b) t
Extend the underlying environment to a superenvironment, and adapt accordingly the underlying representation
val var : ('a, 'b) Bdd.Env.t -> 'a -> ('a, 'b) t
Expression representing the litteral var
val ite : ('a, 'b) Bool.t ->
('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t
If-then-else operation
val eq : ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) Bool.t
Equality operation
val substitute_by_var : ?memo:Cudd.Memo.t ->
('a, 'b) t -> ('a * 'a) list -> ('a, 'b) t
val substitute_by_var_list : ?memo:Cudd.Memo.t ->
('a, 'b) t list -> ('a * 'a) list -> ('a, 'b) t list
Variable renaming. The new variables should already have been declared
val substitute : ?memo:Cudd.Memo.t ->
('a, 'b) t ->
('a * ('a, 'b) t) list -> ('a, 'b) t
val substitute_list : ?memo:Cudd.Memo.t ->
('a, 'b) t list ->
('a * ('a, 'b) t) list -> ('a, 'b) t list
Parallel substitution of variables by expressions
val support : ('a, 'b) t -> 'a PSette.t
Support of the expression
val support_cond : ('a, 'b) t -> 'b Cudd.Bdd.t
Return the support of an expression as a conjunction of the BDD identifiers involved in the expression
val cofactor : ('a, 'b) t -> ('a, 'b) Bool.t -> ('a, 'b) t
Evaluate the expression. The BDD is assumed to be a cube
val restrict : ('a, 'b) t -> ('a, 'b) Bool.t -> ('a, 'b) t
val tdrestrict : ('a, 'b) t -> ('a, 'b) Bool.t -> ('a, 'b) t
Simplify the expression knowing that the BDD is true. Generalizes cofactor.
val print : Format.formatter -> ('a, 'b) t -> unit

List of expressions

module List: sig .. end

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 actually derived from the functions below by just constraining their types. We provide here also more internal functions
module O: sig .. end