package libabsolute

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Parameters
Signature

package libabsolute

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

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Utree.Make`

Parameters

module N : Signature.Numeric

Signature

include Signature.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

package libabsolute

Module Utree.Make

Parameters

Signature

Variables management

Measure

Set-theoretic operations

constraint conversion

Constraint management

Module `Utree.Make`