package libabsolute

You can search for identifiers within the package.

in-package search v0.2.0

package libabsolute

libabsolute
- Libabsolute
  - Consistency
  - Constant
  - Constraint
  - Csp
  - Dom
  - Domains
    
    ApronBox
    
    B
    
    Make
    
    N
    
    Boolean
    
    Make
    
    N
    
    BoxF
    
    BoxS
    
    D1
    
    Make
    
    D
    
    D2
    
    Make
    
    A
    
    B
    
    Oct
    
    Poly
    
    Product
    
    Make
    
    A
    
    B
    
    Utree
    
    Make
    
    N
  - Expr
  - F
  - I
  - Instance
  - Kleene
  - Parser
  - Polynom
    
    Float
    
    Int
    
    Make
    
    R
    
    Rational
  - Q
  - Result
  - Ring
    
    T
  - Signature
    
    Domain
    
    Numeric
  - Solver
    
    Make
    
    D
  - Tools
    
    VarMap
    
    VarSet

Legend:
Library
Module
Module type
Parameter
Class
Class type

Abstract domain with full handling of boolean expressions instead of only numeric comparisons

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) 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

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 : 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 filter : t -> internal_constr -> (t * internal_constr) Consistency.t

redefinition of filter and is_representable using boolean expression

val is_representable : internal_constr -> Kleene.t