libabsolute 0.1 · OCaml Package

Apron Polyhedra

type t

the type of (non-bottom) abstract elements

val empty : t

returns an empty element

Variables management

val add_var : t -> Csp.decl -> t

adds an unconstrained variable to the environnement

val rm_var : t -> string -> t

removes a variable from the environnement

val vars : t -> (Csp.typ * string) list

returns the variables annoted by their type

Measure

val volume : t -> float

computes the volume of an abstract element

Set-theoretic operations

val join : t -> t -> t * bool

Joins two abstract elements. The boolean flag indicates if the join was exact. It is always sound to return false

val join_list : t list -> t * bool

Joins a list of n abstract elements. May be faster than joining pairwise. The boolean flag indicates if the join was exact. It is always sound to return false

val meet : t -> t -> t option

meet two abstract elements

val diff : (t -> t -> t list) option

substracts the second abstract element from the first (difference operator) if an exact operator can not be defined (None), the solver doesn't use the pruning features. precondition: the two abstract elements must be defined onto the same set of variables.

val split : float -> t -> t list

splits an abstract element

constraint conversion

type internal_constr

domain's internal representation of a comparison

val internalize : ?elem:t -> Constraint.comparison -> internal_constr

may use a current abstract element to simplify the constaint

val externalize : internal_constr -> Constraint.comparison

Constraint management

val filter : t -> internal_constr -> t Consistency.t

filters an abstract element with respect to an arithmetic constraint, may raise bot found.

val is_representable : internal_constr -> Kleene.t

checks if a constraint is suited for this abstract domain

val forward_eval : t -> Expr.t -> Q.t * Q.t

computes the range of value of a given expression within an abstract element

val to_constraint : t -> Constraint.t

transforms an abstract element into constraints

val spawn : t -> Csp.instance

Random concretization function. useful to do tests, and to reuse the results. values are generated uniformly when possible

val is_abstraction : t -> Csp.instance -> bool

check if an abstract element is an abstraction of an instance

val print : Format.formatter -> t -> unit

printing

val render : t -> Picasso.Drawable.t

transforms an abstract element into a Picasso.Drawable.t for drawing

package libabsolute

Variables management

Measure

Set-theoretic operations

constraint conversion

Constraint management