[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

Functionalities of the interface at level 1

We focus on the changes brought by the level 1 w.r.t. the level 0.

Variables and Environments  
Semantics and Representation of an abstract value  
Operations on environments  
Dynamic typing w.r.t. environments  
Operations on variables in abstract values  

Variables

Dimensions are replaced by variables.

In the C interface, variables are defined by a generic type (char*, structured type, ...), equipped with the operations compare, copy, free, to_string. In the OCAML, for technical reasons, the type is just the string type.

Environments manages the correspondance between the numerical dimensions of level 0 and the variables of level 1.

Semantics and Representation of an abstract value

The semantics of an abstract value is a subset

X -> (N+R).
where X is a set of variables. Abstract values are typed according to their environment.

It is represented by a structure @verbatim struct ap_abstract1_t { ap_abstract0_t *abstract0; ap_environment_t *env; }; Other datatypes of level 0 are extend in the same way. For instance, @verbatim struct ap_linexpr1_t { ap_linexpr0_t *linexpr0; ap_environment_t *env; };

Operations on environments

Dynamic typing w.r.t. environments

For binary operations on abstract values, the environments should be the same.

For operations involving an abstract value and an other datatype (expression, constraint, ...), one checks that the environment of the expression is a subenvironment of the environment of the abstract value, and one resize if necessary.

Operations on variables in abstract values

Operations on dimensions are lifted to operations on variables:


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

This document was generated on September, 10 2009 using texi2html