Module Domains.Poly

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 * Dom.t) list

returns the variables annoted by their type and their definition domain

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_along : ?prec:float -> string -> t -> t list

splits an abstract element along the specified variable

val split : ?prec:float -> t -> t list

splits an abstract element according to an internal heuristic

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

Constraint management

val sat : Instance.t -> internal_constr -> bool

satisfaction test on the internal constraint representation

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

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

val filter_diff : t -> internal_constr -> (t * Tools.VarSet.t) Consistency.t

same as filter but also return a set of variables that had their domains effectively reduced

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 : Stdlib.Format.formatter -> t -> unit

printing

val render : t -> Picasso.Drawable.t

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