5 Opérations sur les relations en nombres entiers
SPPoC intègre aussi une bibliothèque de manipulation de relations sur
des vecteurs d'entiers nommé Omega Library (voir [21]).
Cette bibliothèque permet de faire des opérations sur les polyèdres
entiers comme la PolyLib mais apporte aussi des fonctions
supplémentaires comme le calcul de la fermeture transitive d'une
relation. Le principal problème rencontré lors de l'intégration de
l'Omega Library dans SPPoC tient au fait que l'Omega Library est écrite en
C++. L'interfaçage d'Objective Caml avec ce langage est un peu moins aisé que
l'interfaçage avec C. Pour l'instant le support de l'Omega Library dans
SPPoC est expérimental.
5.1 Construction des relations
Il a déjà été dit que la structure de base de l'Omega Library est la relation entre
vecteurs d'entiers. Voici un exemple de relation de l'Omega Library telle
que l'affiche SPPoC :
{ [i; j] -> [i'; j'], {i = i', j <= m, j >= 1, i' <= n, i' >= 1} }
Celle-ci met en relation un vecteur d'entrée [i; j] et tous les
vecteurs de sortie [i; j'] avec j' compris entre
1 et m. Il faut noter, qu'à l'opposé de la PolyLib ,
l'Omega Library permet de manipuler directement des expressions
paramétriques. Par exemple, dans la relation ci-dessus, les symboles
n et m n'apparaissent pas dans les variables d'entrée ou
de sortie, ils sont donc considérés comme des paramètres.
Les relations de l'Omega Library peuvent être définies à l'aide de formules de
Presburger, c'est à dire avec les opérateurs logiques ¬, Ú et
Ù, des contraintes affines en les variables et des quantificateurs
$ et ". La méthode actuelle de construction des relations
avec SPPoC ne permet pas d'introduire de quantificateur ", par
contre les quantificateurs $ sont autorisés. En fait une relation
de l'Omega Library est construite à partir de la liste des paramètres, de la liste
des variables d'entrée, de la liste des variables de sortie et d'une liste
de systèmes de contraintes. Toutes les variables apparaissant dans les
systèmes mais dans aucune des trois listes de variables sont considérées
comme des variables quantifiées au sens de $. Voici un exemple
de construction d'une relation avec SPPoC :
# let p = Presburger.parameters_of_list <:v<n, m>>;;
val p : SPPoC.Presburger.parameters = ["n";"m"]
# let r = Presburger.of_systems p <:v<i, j>> <:v<i', j'>>
[<:s<i=i',1<=i<=n,1<=j<=m,j=10q+3,q>=0>>];;
val r : SPPoC.Presburger.t =
{ [i; j] -> [i'; j'], Exists alpha :
{i = i', j <= m, j >= 3, i' <= n, i' >= 1, 10*alpha-j = -3} }
Les paramètres sont traités à part (type Caml Presburger.parameters)
car plusieurs relations peuvent partager les mêmes paramètres.
5.2 Opérations ensemblistes
Il est possible de représenter un polyèdre avec une relation ; il
suffit de prendre un espace d'arrivée de dimension nulle. Par exemple
le carré déclaré à l'aide de la PolyLib dans la section
4 peut aussi se définir comme une relation :
# let p' = Presburger.parameters_of_list <:v<n>>;;
val p' : SPPoC.Presburger.parameters = ["n"]
# let r = Presburger.of_systems p' <:v<i, j>> []
[<:s<0<=i<=n, 0<=j<=n>>];;
val r : SPPoC.Presburger.t =
{ [i; j], {j <= n, j >= 0, i <= n, i >= 0 } }
On peut alors utiliser l'Omega Library pour effectuer des opérations ensemblistes
comme le montre l'exemple ci-dessous.
# let r' = Presburger.of_systems p' <:v<i, j>> []
[<:s< i<j >>];;
val r : SPPoC.Presburger.t = { [i; j], {i <= j} }
# let i = Presburger.inter r r';;
val i : SPPoC.Presburger.t = { [i; j], {i <= j, j <= n, i >= 0} }
Cette utilisation de l'Omega Library est redondante avec celle de la PolyLib mais
on peut imaginer de lancer les deux calculs en parallèle et d'utiliser le
résultat le plus rapidement obtenu ou le plus simple. L'implantation de ce
procédé dans SPPoC pourra faire l'objet de futurs travaux. Les opérations
ensemblistes s'appliquent aussi aux relations générales c'est à dire
celles possédant un espace d'arrivée de dimension non nulle.
5.3 Opérations spécifiques
L'Omega Library permet d'aller bien au-delà des opérations ensemblistes,
en particulier grâce à la possibilité d'introduire des variables
quantifiées. Pour le moment, SPPoC ne permet pas d'utiliser toute la
puissance de l'Omega Library . Cependant il est possible, dès maintenant,
d'utiliser une fonctionnalité intéressante de l'Omega Library : le
calcul de la fermeture transitive d'une relation. L'extrait de
session SPPoC ci-dessous donne un exemple de calcul de la fermeture
transitive d'une relation sur un domaine rectangulaire paramétrique.
# let r = Presburger.of_systems p <:v<i, j>> <:v<i', j'>>
[<:s<i'=i+1; j'=j>>]
and d = Presburger.of_systems p <:v<i, j>> []
[<:s<1<=i<=n; 1<=j<=m>>]
in Presburger.transitive_closure r d;;
- : SPPoC.Presburger.t = { [i; j] -> [i'; j'], {j = j', i-i' <= -1} }
L'intégration de l'Omega Library dans SPPoC est récente, un travail non
négligeable reste à faire pour tirer parti de cette bibliothèque. Citons
la possibilité d'introduire des variables quantifiées au sens de ",
l'interfaçage de toutes les fonctions de manipulation de relations,
l'ajout de conversions de ou vers les autres types majeurs de SPPoC , etc.