Previous  Up  Next

Module Bddapron.Expr0

module Expr0: sig .. end

Important remark:

The following functions may require the creation of new external conditions in the conditional environment.



Expressions


type 'a t = [ `Apron of 'a Bddapron.ApronexprDD.t
       | `Benum of Cudd.Man.v Bdd.Enum.t
       | `Bint of Cudd.Man.v Bdd.Int.t
       | `Bool of Cudd.Man.v Cudd.Bdd.t ] 
type 'a expr = 'a t
Type of general expressions

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

Arithmetic expressions


type apron_coeff = Apron.Coeff.t 
type apron_typ = Apron.Texpr1.typ 
type apron_round = Apron.Texpr1.round 
module Apron: sig .. end

General expressions



The following operations raise a Failure exception in case of a typing error.
val typ_of_expr : 'a Bddapron.Env.t -> 'a t -> 'a Bddapron.Env.typ
Type of an expression
val var : 'a Bddapron.Env.t -> 'a Bddapron.Cond.t -> 'a -> 'a t
Expression representing the litteral var
val ite : 'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       'a Bool.t ->
       'a t -> 'a t -> 'a t
If-then-else operation
val cofactor : 'a t -> 'a Bool.t -> 'a t
Evaluate the expression. The BDD is assumed to be a cube
val substitute_by_var : ?memo:Cudd.Memo.t ->
       'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       'a t -> ('a * 'a) list -> 'a t
val substitute_by_var_list : ?memo:Cudd.Memo.t ->
       'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       'a t list -> ('a * 'a) list -> 'a t list
Parallel substitution of variables by variables
val substitute : ?memo:Cudd.Memo.t ->
       'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       'a t -> ('a * 'a t) list -> 'a t
val substitute_list : ?memo:Cudd.Memo.t ->
       'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       'a t list ->
       ('a * 'a t) list -> 'a t list
Parallel substitution of variables by expressions
val restrict : 'a t -> 'a Bool.t -> 'a t
val tdrestrict : 'a t -> 'a Bool.t -> 'a t
Simplify the expression knowing that the BDD is true. Generalizes cofactor.
val permute : ?memo:Cudd.Memo.t -> 'a t -> int array -> 'a t
val varmap : 'a t -> 'a t
Permutation (rather internal)
val support : 'a Bddapron.Env.t -> 'a Bddapron.Cond.t -> 'a t -> 'a PSette.t
Return the full support of the expression
val eq : 'a Bddapron.Env.t ->
       'a Bddapron.Cond.t ->
       'a t -> 'a 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 t -> Cudd.Bdd.vt
Return the support of an expression as a conjunction of the BDD identifiers involved in the expression
val print : 'a Bddapron.Env.t ->
       'a Bddapron.Cond.t -> Format.formatter -> [< 'a t ] -> unit
Printing functions
val normalize : ?reduce:bool ->
       ?careset:bool ->
       'a Bddapron.Cond.t * 'a t list ->
       'a Bddapron.Cond.t * 'a t list

Opened signature and Internal functions


module O: sig .. end