previous_group previous up next next_group
Previous: 3. Main Decisions Up: 3. Main Decisions Next: 2. Structure Manager

1. Levels and Problems

Two levels have been identified. The lowest layer, level $0$, consists of implementations of different engines such as $C^3$, New POLKA, PPL, Octagon, OMEGA, CUDD, etc (see the author's thesis for these libraries). At this level, overflow and timeout exception are dealt with. Memory management, thread-safety and performance are also considered at this level, as well as debugging functions such as printing functions which depend on the implementations.

Only at this level can we have abstract domain specific operators which are not shared with other domains. The interface for this level is minimal, except the case where algorithmic advantages can be achieved. Different implementations can be combined to produce a new library. Thus the Cartesian product implementation and dimension change approach [Mer05] can be integrated here.

The genericity versus comfortable use question has been raised, i.e., whether the interface should support or not functions with multiple arguments, e.g. convex hull of a list of constraint systems. It was decided that performance-related issues, which depend on the used domain, are treated at level $0$, while comfortability-related issues are treated at level $1$. However, it is difficult since some algorithms such as minimization, projection or convex hull require optimizations at level $1$. It was decided that dimension management, implemented in $C^3$, is to be dealt with at level $1$.

Problems at higher levels are dealt with in the static analyzers. For example, the question of precision and arithmetics for $8$, $16$, $32$, $64$, $128$ bits and gmp (GNU Multi Precision) computing is dealt with at some level higher than $1$, because it depends much on the techniques used by analyzers. Numeric types specified by Value in $C^3$ or pkint in New POLKA are defined at compile time.


previous_group previous up next next_group
Previous: 3. Main Decisions Up: 3. Main Decisions Next: 2. Structure Manager
Nguyen Que Duong
2006-09-16