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

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

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.

The semantics of an abstract value is a subset

X -> (N+R).where

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; };

- creation, merging, destruction
- addition/removal/renaming of variables

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 dimensions are lifted to operations on variables:

- Projection/Elimination of one or several variables with constant environment;
- Addition/Removal/Renaming of variables with corresponding change of environment;
- Change of environment (possibly combining removal and addition of variables);
- Expansion and folding of variables.

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

This document was generated on