Description de l'interface de programmation

A Description de l'interface de programmation

Pour des raisons de place limitée, dans les descriptions de ces modules, on ne fera apparaître que les fonctions principales. Le lecteur désirant une description complète de l'interface de programmation est invité à télécharger le logiciel (http://www.lifl.fr/~boulet/sppoc/).

A.1 Module Term

Un terme est le produit d'un nombre rationnel (représenté par un Num.num pour des calculs rationnels en précision infinie) et d'une variable (représentée par une chaîne de caractères, ou simplement un nombre.

module Term :
  sig
    type t
    val make : string -> Num.num -> t
    val of_int : int -> t
    val get_coef : t -> Num.num
    val get_var : t -> string
    val minus : t -> t
    ...
  end;;

A.2 Module Form

Une forme linéaire est une somme de termes. On peut utiliser les opérations arithmétiques suivantes : l'addition, la soustraction de deux formes, la multiplication et la division de deux formes par un nombre et l'opposé d'une forme. Ces formes étant représentées canoniquement (tri des variables), on peut définir un ordre total sur ces structures.

La fonction Form.subst effectue une substitution dans la forme qui lui est passée en premier argument. En effet, son deuxième argument est une liste d'association mettant en relation des variables avec des formes linéaires. Chaque occurrence de chaque variable de cette liste dans la forme initiale sera remplacée par la forme qui lui est associée dans la forme transformée.

Comme pour les autres modules, tout un ensemble de fonctions font office de constructeurs et de destructeurs de cette structure pour pouvoir la construire de différente façons et en extraire les composants.

module Form :
  sig
    type t
    val make : Term.t list -> t
    ...
    val add : t -> t -> t
    val mult : t -> Num.num -> t
    ...
    val eq : t -> t -> bool
    val lt : t -> t -> bool
    val subst : t -> (string * t) list -> t
    ...
  end;;

A.3 Module Expr

Le type défini ici permet d'exprimer des expressions arithmétiques symboliques générales, y compris non linéaires. Ces expressions sont automatiquement simplifiées et calculées lors de toute manipulation. On peut introduire des modulos et des quotients entiers dans ces expressions.

module Expr :
  sig
    type t
    val of_form : Form.t -> t
    val make : string -> t list -> t
    val add : t -> t -> t
    val mult : t -> t -> t
    val quo : t -> t -> t
    val modulo : t -> t -> t
    ...
    val eq : t -> t -> bool
    val subst : t -> (string * Form.t) list -> t
    ...
  end;;

A.4 Module Ineq

On manipule ici des équation et des inéquations symboliques. Chaque membre de l'(in)équation est une expression (du type Expr.t).

Les inconnues sont considérées comme des entiers uniquement lors de la conversion inégalité large, inégalité stricte (fonctions Ineq.e_of_t et Ineq.t_of_e).

module Ineq :
  sig
    type t
    val build_eq : Expr.t -> Expr.t -> t
    val build_le : Expr.t -> Expr.t -> t
    val build_gt : Expr.t -> Expr.t -> t
    ...
    val e_of_t : t -> t
    val t_of_e : t -> t
    val not : t -> t
    ...
  end;;

A.5 Module System

Le type abstrait System.t définit des systèmes d'inéquations entières. Tout au long des manipulations de tels systèmes, si on crée un système trivialement vide (deux inéquations sont contradictoires), l'exception System.Empty est levée.

Les fonctionnalités importantes disponibles ici sont la simplification et la linéarisation. Leur fonctionnement est décrit dans le chapitre 6.

module System :
  sig
    type t
    exception Empty
    val make : Ineq.t list -> t
    val add_ineq : Ineq.t -> t -> t
    val combine : t -> t -> t
    ...
    val simplify : string list -> string list -> t -> t
    val linearize : t -> t
    ...
  end;;

A.6 Module Quast

Un QUAST est un arbre de sélection quasi-affine. C'est-à-dire une arboressence de conditionnelles dont les prédicats sont des inégalités affines et les branches des listes de formes linéaires ou le signe ^ qui signifie que la branche en question est inatteignable ou qu'elle ne conduit pas à une valeur significative.

La fonction Quast.get_paths retourne la liste des contextes de chaque feuille : un contexte étant un systeme représentant le chemin parcouru dans l'arbre pour arriver à la feuille.

Les deux fonctions Quast.simpl et Quast.simplify ont le même but : la simplification de l'écriture d'un QUAST dans un contexte donné par un système d'(in)équations. On réduit le domaine d'existence des branches au domaine défini par ce contexte. Quast.simpl effectue une première simplification rapide et peu poussée alors que Quast.simplify fait appel à la programmation linéaire pour simplifier beaucoup plus précisément mais en un temps aussi beaucoup plus long.

On dispose aussi d'itérateurs et de fonctions calculant le minimum et/ou le maximum de deux QUAST.

module Quast =
  sig
    type tag;;
    type t;;

    val bottom : t
    val leaf : Form.t list -> tag -> t
    val branch : Ineq.t -> t -> t -> t
    ...
    val get_paths : t -> System.t list
    val flatten : t -> (System.t * (Form.t list) * tag) list
    ...
    val simpl : System.t -> t -> t
    val simplify : System.t -> t -> t
    ...
    val map : (t -> t) -> t -> t
    val min : System.t -> t -> t -> t
    val max : System.t -> t -> t -> t
    ...
  end;;

A.7 Module Modulo

On définit ici un type abstrait représentant le reste de la division euclidienne d'une forme linéaire par un entier. La seule fonction non évidente dans ce module est Modulo.to_system qui retourne un système d'inéquations linéaires équivalent au modulo considéré (définition de la division euclidienne).

module Modulo :
  sig
    type t
    val make : Form.t -> Num.num -> t
    val to_system : string -> t -> System.t
    ...
  end;;

A.8 Module NewPar

Ce module permet de gérer un ensemble de « nouveaux paramètres », ce sont des paramètres introduits par PIP lors de la résolution d'un problème de programmation linéaire paramétré qui donne une solution dépendant de modulos. Le résultat est alors exprimé par un « QUAST étendu » qui est un QUAST (type Quast.t) auquel on adjoint un ensemble de tels paramètres (association d'un nom de variable (string) et d'un modulo (Modulo.t)).

module NewPar :
  sig
    type t
    val make : (string * Modulo.t) list -> t
    val new_name : string list -> string
    val add : string -> Modulo.t -> t -> t
    val find : string -> t -> Modulo.t
    val remove : string -> t -> t
    val iter : (string -> Modulo.t -> unit) -> t -> unit
    val fold : (string -> Modulo.t -> 'a -> 'a) -> t -> 'a -> 'a
    val combine : t -> t -> t
    val to_system : t -> System.t
    ...
  end;;

A.9 Module EQuast

Un QUAST étendu est un couple formé par un ensemble de nouveaux paramètres (type NewPar.t) et un QUAST (type Quast.t).

Outre les fonctions agissant sur les deux composants d'un tel objet, on peut unifier des paramètres de meme valeur et ainsi simplifier le QUAST.

module EQuast =
  sig
    type tag
    type quast
    type t
    val make : quast -> NewPar.t -> t
    val flatten : t -> (System.t * (Form.t list) * tag) list
    val unify : t -> t
    val simplify : System.t -> t -> t
    val map : (quast -> quast) -> t -> t
    val min : System.t -> t -> t -> t
    val max : System.t -> t -> t -> t
    ...
  end;;

A.10 Module Question

Ce module définit le type des questions dont on peut demander la résolution au module PIP ci-dessous. Elles sont de quatre sortes et à chacune d'elles correspond un constructeur : le minimum lexicographique (Question.min_lex), le maximum lexicographique (Question.max_lex), le minimum d'une fonction, dite objective, (Question.min_fun) et le maximum d'une fonction (Question.max_fun). Ces fonctions sont définies par une forme linéaire.

module Question :
  sig
    type t
    val min_lex : string list -> t
    val max_lex : string list -> t
    val min_fun : Form.t -> t
    val max_fun : Form.t -> t
    ...
  end;;

A.11 Module PIP

Le type abstrait défini dans ce module est le type des problèmes de programmation linéaire entière paramétrée. Le constructeur PIP.make permet de construire un tel problème à partir d'un système d'inéquations entières représentant le domaine de recherche et d'une question.

Les fonctions PIP.solve et PIP.solve_ratio permettent de résoudre ces problèmes. La première résoud en nombres entiers avec introduction possible de nouveaux paramètres et la deuxième travaille en nombres rationnels. Le résultat retourné par ces fonctions est de type EQuast.t.

module PIP :
  sig
    type t
    val make : System.t -> Question.t -> t
    val solve : t -> EQuast.t
    val solve_ratio : t -> EQuast.t
    ...
  end;;

A.12 Modules d'interface à la PolyLib

Le module Function définit des applications affines (association de formes affines à des variables).

module Function :
sig
  type t
  val make : (string * Form.t) list -> t
  val list_invars : t -> string list
  val list_outvars : t -> string list
  ...
end;;

Le module Rays définit la représentation par sommets, rayons et lignes d'un polyèdre. On peut la convertir en une matrice de coefficients.

module Rays :
sig
  type t
  val of_matrix : string list -> Num.num array array -> t
  val to_matrix : t -> Num.num array array
  ...
end;;

Le module Polyhedron définit les polyèdres et réalise l'interface à la PolyLib . À part les fonctions d'entrée-sortie symboliques, elle offre exactement les mêmes fonctions que la PolyLib . Pour plus d'informations sur cette interface, voir chapitre 4.

module Polyhedron :
sig
  type t
  type expr_quast = ( t * Expr.t ) list
  val make : System.t -> Rays.t -> t
  val of_rays : Rays.t -> t
  val of_system : System.t -> t
  ...
  val rename : ( string * string ) list -> t -> t
  val expand : string list -> t -> t
  val subset : t -> t -> bool
  val inter : t -> t -> t
  val union : t -> t -> t
  ...
  val image : t -> Function.t -> t
  val enum : t -> t -> expr_quast
  val enumeration : string list -> t -> expr_quast
  ...
end;;