Module Bddapron.Expr1

module Expr1: sig .. end

Important remark:

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


type 'a t = ('a Bddapron.Env.t, 'a Bddapron.Expr0.t) Bddapron.Env.value 
type 'a expr = 'a t 
Type of general 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 
type apron_cons_typ = Apron.Tcons1.typ 
module Apron: sig .. end

General expressions

val typ_of_expr : 'a t -> 'a Bddapron.Env.typ
Type of an expression
val make : 'a Bddapron.Env.t -> 'a Bddapron.Expr0.t -> 'a t
val of_expr0 : 'a Bddapron.Env.t -> 'a Bddapron.Expr0.t -> 'a t
Creation from an expression of level 0 (without environment)
val get_env : 'a t -> 'a Bddapron.Env.t
val to_expr0 : 'a t -> 'a Bddapron.Expr0.t
Extract resp. the environment and the underlying expression of level 0
val extend_environment : 'a t -> 'a Bddapron.Env.t -> 'a t
Extend the underlying environment to a superenvironment, and adapt accordingly the underlying representation
val var : 'a Bddapron.Env.t -> 'a Bddapron.Cond.t -> 'a -> 'a t
Expression representing the litteral var
val ite : 'a Bddapron.Cond.t ->
'a Bool.t ->
'a t -> 'a t -> 'a t
If-then-else operation
val eq : 'a Bddapron.Cond.t ->
'a t -> 'a t -> 'a Bool.t
Equality operation
val substitute_by_var : ?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a t -> ('a * 'a) list -> 'a t
val substitute_by_var_list : ?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a t list -> ('a * 'a) list -> 'a t list
Variable renaming. The new variables should already have been declared
val substitute : ?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a t -> ('a * 'a t) list -> 'a t
val substitute_list : ?memo:Cudd.Memo.t ->
'a Bddapron.Cond.t ->
'a t list ->
('a * 'a t) list -> 'a t list
Parallel substitution of variables by expressions
val support : 'a Bddapron.Cond.t -> 'a t -> 'a PSette.t
Support of the expression
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 cofactor : 'a t -> 'a Bool.t -> 'a t
Evaluate the expression. The BDD is assumed to be a cube
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 print : 'a Bddapron.Cond.t -> Format.formatter -> 'a t -> unit
val normalize : ?reduce:bool ->
?careset:bool ->
'a Bddapron.Cond.t * 'a t list ->
'a Bddapron.Cond.t * 'a t list

List of expressions

module List: sig .. end

Opened signature and Internal functions

module O: sig .. end