module O: sig .. end
val check_typ2 : ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
Bddapron.Env.O.t ->
[< 'a Bddapron.Expr0.t ] -> [< 'a Bddapron.Expr0.t ] -> 'a Bddapron.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 Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'd)
Bddapron.Env.O.t -> [< 'a Bddapron.Expr0.t ] -> 'a Bddapron.Env.typ
Type of an expression
val var : ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
'a -> 'a Bddapron.Expr0.t
Expression representing the litteral var
val ite : ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
'a Bool.t ->
'a Bddapron.Expr0.t -> 'a Bddapron.Expr0.t -> 'a Bddapron.Expr0.t
If-then-else operation
val cofactor : 'a Bddapron.Expr0.t -> 'a Bool.t -> 'a Bddapron.Expr0.t
val restrict : 'a Bddapron.Expr0.t -> 'a Bool.t -> 'a Bddapron.Expr0.t
val tdrestrict : 'a Bddapron.Expr0.t -> 'a Bool.t -> 'a Bddapron.Expr0.t
val permute : ?memo:Cudd.Memo.t -> 'a Bddapron.Expr0.t -> int array -> 'a Bddapron.Expr0.t
val permute_list : ?memo:Cudd.Memo.t ->
'a Bddapron.Expr0.t list -> int array -> 'a Bddapron.Expr0.t list
val varmap : 'a Bddapron.Expr0.t -> 'a Bddapron.Expr0.t
val substitute_by_var : ?memo:Cudd.Memo.t ->
('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
'a Bddapron.Expr0.t -> ('a * 'a) list -> 'a Bddapron.Expr0.t
val substitute_by_var_list : ?memo:Cudd.Memo.t ->
('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
'a Bddapron.Expr0.t list -> ('a * 'a) list -> 'a Bddapron.Expr0.t list
Parallel substitution of variables by variables
val substitute : ?memo:Cudd.Memo.t ->
('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
'a Bddapron.Expr0.t -> ('a * 'a Bddapron.Expr0.t) list -> 'a Bddapron.Expr0.t
val substitute_list : ?memo:Cudd.Memo.t ->
('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
'a Bddapron.Expr0.t list ->
('a * 'a Bddapron.Expr0.t) list -> 'a Bddapron.Expr0.t list
Parallel substitution of variables by expressions
val support : ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
'a Bddapron.Expr0.t -> 'a PSette.t
Return the full support of the expression
val eq : ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
'a Bddapron.Expr0.t -> 'a Bddapron.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 Bddapron.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 Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
Format.formatter -> [< 'a Bddapron.Expr0.t ] -> unit
val print_bdd : ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
Format.formatter -> Cudd.Bdd.vt -> unit
val normalize : ?reduce:bool ->
?careset:bool ->
('a,
('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t)
Bddapron.Cond.O.t * 'a Bddapron.Expr0.t list ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t *
'a Bddapron.Expr0.t list
val compose_of_lvarexpr : ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
Bddapron.Env.O.t ->
('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t ->
('a * 'a Bddapron.Expr0.t) list ->
Cudd.Bdd.vt array option * ('a, 'a Bddapron.Expr0.t) PMappe.t