Module Bddapron.Expr1.O

module O: sig .. end

type ('a
       , ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'e)
         Bddapron.Env.O.t) t = (('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'e)
        Bddapron.Env.O.t, 'a Bddapron.Expr0.t)
       Bddapron.Env.value

type ('a
       , ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'b)
         Bddapron.Env.O.t) expr = ('a,
        ('a, [> 'a Bddapron.Env.typ ] as 'c, [> 'a Bddapron.Env.typdef ] as 'd, 'b)
        Bddapron.Env.O.t)
       t

Type of general expressions

module Bool: sig .. end

module Bint: sig .. end

module Benum: sig .. end

module Apron: sig .. end

val typ_of_expr : ('a,
        ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'b)
        Bddapron.Env.O.t)
       t -> 'a Bddapron.Env.typ

Type of an expression

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

Creation from an expression without environment

val extend_environment : ('a,
        ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t)
       t ->
       ('a, 'b, 'c, 'd) Bddapron.Env.O.t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t

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, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t

Expression representing the litteral var

val ite : ('a,
        ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t)
       Bddapron.Cond.O.t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bool.t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t

If-then-else operation

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

Equality operation

val substitute_by_var : ?memo:Cudd.Memo.t ->
       ('a,
        ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t)
       Bddapron.Cond.O.t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t ->
       ('a * 'a) list -> ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t

val substitute_by_var_list : ?memo:Cudd.Memo.t ->
       ('a,
        ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t)
       Bddapron.Cond.O.t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t list ->
       ('a * 'a) list ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t list

Variable renaming. The new variables should already have been declared

val substitute : ?memo:Cudd.Memo.t ->
       ('a,
        ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t)
       Bddapron.Cond.O.t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t ->
       ('a * ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t) list ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t

val substitute_list : ?memo:Cudd.Memo.t ->
       ('a,
        ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t)
       Bddapron.Cond.O.t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t list ->
       ('a * ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t) list ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t list

Parallel substitution of variables by expressions

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

Support of the expression

val support_cond : Cudd.Man.vt ->
       ('a,
        ('a, [> 'a Bddapron.Env.typ ], [> 'a Bddapron.Env.typdef ], 'b)
        Bddapron.Env.O.t)
       t -> Cudd.Bdd.vt

Return the support of an expression as a conjunction of the BDD identifiers involved in the expression

val cofactor : ('a,
        ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t)
       t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bool.t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t

Evaluate the expression. The BDD is assumed to be a cube

val restrict : ('a,
        ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t)
       t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bool.t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t

val tdrestrict : ('a,
        ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t)
       t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bool.t ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t

Simplify the expression knowing that the BDD is true. Generalizes cofactor.

val print : ('a,
        ('a, [> 'a Bddapron.Env.typ ] as 'b, [> 'a Bddapron.Env.typdef ] as 'c, 'd)
        Bddapron.Env.O.t)
       Bddapron.Cond.O.t ->
       Format.formatter ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t -> 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, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t list ->
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) Bddapron.Cond.O.t *
       ('a, ('a, 'b, 'c, 'd) Bddapron.Env.O.t) t list

List of expressions

module List: sig .. end