module O: sig .. end
val check_typ2 : ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b) Env.O.t ->
[< 'a Expr0.t ] -> [< 'a Expr0.t ] -> 'a Env.typ
module Bool: sig .. end
module Bint: sig .. end
module Benum: sig .. end
module Apron: sig .. end
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) Env.O.t ->
[< 'a Expr0.t ] -> 'a Env.typ
Type of an expression
val var : ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd) Env.O.t ->
('a, ('a, 'b, 'c, 'd) Env.O.t) Cond.O.t -> 'a -> 'a Expr0.t
Expression representing the litteral var
val ite : ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd) Env.O.t ->
('a, ('a, 'b, 'c, 'd) Env.O.t) Cond.O.t ->
'a Bool.t -> 'a Expr0.t -> 'a Expr0.t -> 'a Expr0.t
If-then-else operation
val cofactor : 'a Expr0.t -> 'a Bool.t -> 'a Expr0.t
val restrict : 'a Expr0.t -> 'a Bool.t -> 'a Expr0.t
val tdrestrict : 'a Expr0.t -> 'a Bool.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 varmap : 'a Expr0.t -> 'a Expr0.t
val substitute_by_var : ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd) Env.O.t ->
('a, ('a, 'b, 'c, 'd) Env.O.t) Cond.O.t ->
'a Expr0.t -> ('a * 'a) list -> 'a Expr0.t
Parallel substitution of variables by variables
val substitute : ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd) Env.O.t ->
('a, ('a, 'b, 'c, 'd) Env.O.t) Cond.O.t ->
'a Expr0.t -> ('a * 'a Expr0.t) list -> 'a Expr0.t
Parallel substitution of variables by expressions
val support : ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd) Env.O.t ->
('a, ('a, 'b, 'c, 'd) Env.O.t) Cond.O.t -> 'a Expr0.t -> 'a PSette.t
Return the full support of the expression
val eq : ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd) Env.O.t ->
('a, ('a, 'b, 'c, 'd) Env.O.t) Cond.O.t ->
'a Expr0.t -> 'a Expr0.t -> 'a Bool.t
Under which condition are the expressions equal ? In case of
arithmetic expressions, do not take into account the careset.
val support_cond : Cudd.Man.vt -> 'a Expr0.t -> Cudd.Bdd.vt
Return the support of an expression as a conjunction of the BDD
identifiers involved in the expression
Printing functions
val print : ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd) Env.O.t ->
('a, ('a, 'b, 'c, 'd) Env.O.t) Cond.O.t ->
Format.formatter -> [< 'a Expr0.t ] -> unit
val print_bdd : ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd) Env.O.t ->
('a, ('a, 'b, 'c, 'd) Env.O.t) Cond.O.t ->
Format.formatter -> Cudd.Bdd.vt -> unit
val normalize : ?reduce:bool ->
?careset:bool ->
('a, ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd) Env.O.t)
Cond.O.t * 'a Expr0.t list ->
('a, ('a, 'b, 'c, 'd) Env.O.t) Cond.O.t * 'a Expr0.t list
val compose_of_lvarexpr : ('a, [> 'a Env.typ ] as 'b, [> 'a Env.typdef ] as 'c, 'd) Env.O.t ->
('a, ('a, 'b, 'c, 'd) Env.O.t) Cond.O.t ->
('a * 'a Expr0.t) list ->
Cudd.Bdd.vt array option * ('a, 'a Expr0.t) PMappe.t