module Expr1: sig .. end
Expressions
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