Domain (libabsolute.Libabsolute.Signature.Domain)

include Numeric

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

Constraint management

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

type internal_constr

domain's internal representation of a constraint

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

constraint conversion

val externalize : internal_constr -> Constraint.t

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

satisfaction test on the internal constraint representation

val filter : t -> internal_constr -> (t * internal_constr) Consistency.t

redefinition of filter using boolean expression, it also computes a potentially simplified equivalent constraint e.g:

false || c <=> c
true && c <=> c

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

same as filter but also returns the set of variables that have been effectively filtered

val is_representable : internal_constr -> Kleene.t

checks if a constraint can be encoded without loss of precision; i.e $\forall x, \gamma(\rho(x,c)) = \{v \in \gamma(x) | c(v)\}$