Module Expr1

module Expr1: sig .. end

Finite-type and arithmetical expressions linked to normalized environments

Important remark:

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

Expressions

type 'a t = ('a Env.t, 'a Expr0.t) Env.value

type 'a expr = 'a t

Type of general expressions

module Bool: sig .. end

module Bint: sig .. end

module Benum: sig .. end

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

val typ_of_expr : 'a t -> 'a Env.typ

Type of an expression

val make : 'a Env.t -> 'a Expr0.t -> 'a t

val of_expr0 : 'a Env.t -> 'a Expr0.t -> 'a t

Creation from an expression of level 0 (without environment)

val get_env : 'a t -> 'a Env.t

val to_expr0 : 'a t -> 'a Expr0.t

Extract resp. the environment and the underlying expression of level 0

val extend_environment : 'a t -> 'a Env.t -> 'a t

Extend the underlying environment to a superenvironment, and adapt accordingly the underlying representation

val var : 'a Env.t -> 'a Cond.t -> 'a -> 'a t

Expression representing the litteral var

val ite : 'a Cond.t -> 'a Bool.t -> 'a t -> 'a t -> 'a t

If-then-else operation

val eq : 'a Cond.t -> 'a t -> 'a t -> 'a Bool.t

Equality operation

val substitute_by_var : 'a Cond.t -> 'a t -> ('a * 'a) list -> 'a t

Variable renaming. The new variables should already have been declared

val substitute : 'a Cond.t -> 'a t -> ('a * 'a t) list -> 'a t

Parallel substitution of variables by expressions

val support : 'a 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 Cond.t -> Format.formatter -> 'a t -> unit

val normalize : ?reduce:bool ->
       ?careset:bool -> 'a Cond.t * 'a t list -> 'a Cond.t * 'a t list

module List: sig .. end

module O: sig .. end