Différences

Ci-dessous, les différences entre deux révisions de la page.

Lien vers cette vue comparative

Les deux révisions précédentes Révision précédente
Prochaine révision
Révision précédente
enseignement:logique:projet:2013 [2013/10/16 11:10]
ecoquery [Mise à jour du projet]
enseignement:logique:projet:2013 [2013/12/19 12:53] (Version actuelle)
ecoquery [Organisation du projet]
Ligne 36: Ligne 36:
     * une collection d'autres fichiers dont certains seront générés automatiquement. Il n'est pas utile de les lire. Leur principal objectif est de définir une fonction ''lit_formule'' qui crée l'arbre de syntaxe abstraite à partir d'une formule sous fourme de chaîne (typiquement, saisie au clavier ou lue dans un fichier).     * une collection d'autres fichiers dont certains seront générés automatiquement. Il n'est pas utile de les lire. Leur principal objectif est de définir une fonction ''lit_formule'' qui crée l'arbre de syntaxe abstraite à partir d'une formule sous fourme de chaîne (typiquement, saisie au clavier ou lue dans un fichier).
  
-<note tip>Il est demandé de ne pas héberger vos sources sur un dépôt public. L'UCBL met à votre disposition une [[http://forge.univ-lyon1.fr|forge]] avec un hébergement de dépôts [[http://mercurial.selenic.com/|mercurial]]. Le projet fourni((qui peut être cloné via ''hg clone https://forge.univ-lyon1.fr/hg/inf3034l-2013-base'')) peut être poussé vers cette forge.</note>+<note tip>Il est demandé de ne pas héberger vos sources sur un dépôt public. L'UCBL met à votre disposition une [[http://forge.univ-lyon1.fr|forge]] avec un hébergement de dépôts [[http://mercurial.selenic.com/|mercurial]]. Le projet fourni((qui peut être récupéré via ''hg pull https://forge.univ-lyon1.fr/hg/inf3034l-2013-base'')) peut être poussé vers cette forge. 
 + 
 +  * Pour créer un projet: http://forge.univ-lyon1.fr/projects/new 
 +  * Pour être ajouté à un projet, un étudiant doit s'être connecté au  moins une fois sur http://forge.univ-lyon1.fr. Le manager du projet pourra alors l'ajouter via Configuration -> Membres. 
 +  * L'url mercurial((pour le push/pull/clone)) de votre projet est accessible depuis Configuration -> Dépôt 
 +  * Quelques {{:enseignement:maven-forge-ic.pdf|slides}} pour la gestion de projet (regarder la partie forge) 
 +  * Voir [[:enseignement:aide:forge|l'aide sur la forge]] pour un scénario d'utilisation pour des TPs/projets 
 +</note>
 ==== Organisation du projet ==== ==== Organisation du projet ====
  
Ligne 48: Ligne 55:
 <note important> <note important>
 Le projet est à réaliser seul ou en binôme. Les différentes étapes permettent aux étudiants de situer leur avancement. //Avancer régulièrement et progresser hors des séances de TP afin que ces dernières vous soient le plus profitables possibles//. Vous pouvez vous aider les uns les autres, en gardant à l'esprit que ceci //n'implique pas// de devoir s'échanger les sources entre binômes. Le projet est à réaliser seul ou en binôme. Les différentes étapes permettent aux étudiants de situer leur avancement. //Avancer régulièrement et progresser hors des séances de TP afin que ces dernières vous soient le plus profitables possibles//. Vous pouvez vous aider les uns les autres, en gardant à l'esprit que ceci //n'implique pas// de devoir s'échanger les sources entre binômes.
-Le projet est à rendre après les vacances de Noël sous la forme d'une archive comme celle qui vous est fournie. //Les modalités exactes du rendu seront données en temps utile//. 
 </note> </note>
  
Ligne 185: Ligne 191:
   * la CNF est //l ∧ c//   * la CNF est //l ∧ c//
  
-On peut remarquer que les CNFs ne font que grossir, on peut ainsi passer la CNF en argument par référence  : les ensembles de clauses //c1// et //c2// dans //(p, ... ∧ c1 ∧ c2)// sont produites par les appels récursifs de //tseitin//. On passe également un compteur par référence ''var_t & next'' pour générer de nouvelles variables frâiches. Ainsi en C/C++ on définira les deux fonctions :+On peut remarquer que les CNFs ne font que grossir, on peut ainsi passer la CNF en argument par référence  : les ensembles de clauses //c1// et //c2// dans //(p, ... ∧ c1 ∧ c2)// sont produites par les appels récursifs de //tseitin//. On passe également un compteur par référence ''var_t & next'' pour générer de nouvelles variables fraiches. Ainsi en C/C++ on définira les deux fonctions :
 <code c++> <code c++>
-lit_t tseitin(formule f, const map<string, int> & m, cnf_t & c, var_t & next);+lit_t tseitin(formule f, const map<string, var_t> & m, cnf_t & c, var_t & next);
 cnf_t tseitin(formule f); cnf_t tseitin(formule f);
 </code> </code>
Ligne 203: Ligne 209:
  
 Il faut enfin ajouter ''{8}'' à cl pour obtenir finalement ''cl= {{7,0,2},{6,1},{6,3},{9,7,4},{8,6},{8,5},{8}}'' comme codage de Tseitin de //(a ∨ b) ⇒ c//. Il faut enfin ajouter ''{8}'' à cl pour obtenir finalement ''cl= {{7,0,2},{6,1},{6,3},{9,7,4},{8,6},{8,5},{8}}'' comme codage de Tseitin de //(a ∨ b) ⇒ c//.
 +</note>
 +
 +<note warning>
 +La fonction ''tseitin'' a ''m'' comme paramètre **en lecture seule** (déclaration ''**const** map<string, var_t> & m''), or si vous utilisez ''m[]'', comme pour un tableau, vous allez avoir une erreur assez peu intelligible car ''[[http://en.cppreference.com/w/cpp/container/map/operator_at|[] ]]'' **est une méthode qui peut modifier m**. A la place, il faut utiliser ''[[http://en.cppreference.com/w/cpp/container/map/find|find]]'' qui est une méthode en lecture seule.
 +
 </note> </note>
  
Ligne 244: Ligne 255:
   * ''suiv'' est une variable non affectée. On considère que toutes les variables dont le numéro est inférieur au numéro de ''suiv'' ont une valeur dans ''valeurs''.   * ''suiv'' est une variable non affectée. On considère que toutes les variables dont le numéro est inférieur au numéro de ''suiv'' ont une valeur dans ''valeurs''.
  
-La fonction procédera comme suit: +La fonction procèdera comme suit: 
-  - mettre la valeur de ''suiv'' à VRAI dans ''valeurs'' +  - si ''suiv'' est supérieur à la taille de ''valeurs'', alors évaluer la CNF et renvoyer VRAI si elle est satisfaite. 
-  s'il reste des variables à affecter, appeler récursivement la fonction avec ''suiv+1'' +  - sinon: 
-  sinon tester la valeur de la cnf +    - mettre la valeur de ''suiv'' à VRAI dans ''valeurs'' 
-    * si la formule est vaut VRAI, renvoyer ''true'' +    Appeler récursivement la fonction avec ''suiv+1'' 
-    sinonmettre la valeur de ''suiv'' à FAUX et tester à nouveau la satisfiabilité de la formule (comme en 2/3) +      - si l'appel récursif renvoie ''true'' la CNF est satisfiable et on peut renvoyer ''true'' 
-      si la formule est satisfiablerenvoyer ''true'' +      sinon mettre la valeur de ''suiv'' à FAUX dans ''valeurs'' 
-      sinonremettre la valeur de ''suiv'' à INDETERMINEE, puis renvoyer ''false''.+    - Appeler à nouveau récursivement la fonction avec ''suiv+1'' 
 +      si l'appel récursif renvoie ''true'' la CNF est satisfiable et on peut renvoyer ''true'' 
 +      sinon la CNF n'est pas satisfiable pour l'affectation courante: remettre la valeur de ''suiv'' à INDETERMINEE, puis renvoyer ''false''. 
 + 
 + 
 +<note warning>Dans la définition de la fonction ''cherche'', on suppose que la longueur du tableau ''vector<val_t> & valeurs'' passé en paramètre est //égale au nombre de variables (différentes) de la cnf//. Ainsi: 
 +  * il n'y a pas besoin de faire de ''push_back'' ou de ''resize'', l'allocation et l'initialisation est à la charge de la fonction qui appelle ''cherche''
 +  * on peut déterminer que toute les variables ont été affectées en comparant ''suiv'' et ''valeurs.size()''
 +  </note>
  
 Modifier la fonction main de façon à: Modifier la fonction main de façon à:
Ligne 280: Ligne 299:
 La première étape pour vérifier un additionneur n-bits consiste à générer sa spécification sous forme de formules.  La première étape pour vérifier un additionneur n-bits consiste à générer sa spécification sous forme de formules. 
  
-On considère que les entrées sont données par les variables ''p1'' ... ''p//n//'' et ''q1'' ... ''q//n//'' et que les sorties sont codées par les formules //A1// ... //An//, //Bn////B1// ... //Bn// sont les retenues générées par la somme dans la colonne //n//.+On considère que les 2 * n entrées sont données par les variables ''p1'' ... ''p//n//'' et ''q1'' ... ''q//n//'' et que les (//n+1//sorties sont codées par les formules //A1// ... //An//, //B// (//B// est le dernier bit de a somme, celui avec le poids le plus fort).
  
-On utilisera les formules suivantes:+On utilisera les formules suivantes qui expriment la somme et la retenue pour un additionneur qui calcule la somme de trois entrée à 1 bit :
   * S = t ⇔(u ⇔ w) : cette formule est vraie si le chiffre des unités de la somme des valeurs de t,u et w est 1 (première formule de l'exercice 2.1 du {{:enseignement:logique:logique-td2-enonce.pdf|TD2}})   * S = t ⇔(u ⇔ w) : cette formule est vraie si le chiffre des unités de la somme des valeurs de t,u et w est 1 (première formule de l'exercice 2.1 du {{:enseignement:logique:logique-td2-enonce.pdf|TD2}})
   * R = (t ⇒ (u ∨ w)) ∧ (¬t ⇒ (u ∧ w)) : cette formule est vrai si la retenue de la somme des valeurs de t, u et w est 1 (deuxième formule de l'exercice 2.1 du {{:enseignement:logique:logique-td2-enonce.pdf|TD2}}).   * R = (t ⇒ (u ∨ w)) ∧ (¬t ⇒ (u ∧ w)) : cette formule est vrai si la retenue de la somme des valeurs de t, u et w est 1 (deuxième formule de l'exercice 2.1 du {{:enseignement:logique:logique-td2-enonce.pdf|TD2}}).
  
-La génération de cette spécification par récurrence peut être définie comme suit:  +La génération de cette spécification par récurrence pour //n//-bits peut être définie comme suit:  
-  * Additionneur 1-bit: +  * Additionneur 1-bit : on retourne le vecteur V=[B,A1] de taille //2// avec  
-    * A1 = S [ p1/t, q1 / u, ⊥ / w] +    * A1 = S [ p1/t, q1 / u, ⊥ / w], on calcule cette formule en construisant la substitution  [ p1/t, q1 / u, ⊥ / w] en en l'appliquant à S avec la méthode ''applique'' 
-    * B1 = R [ p1/t, q1 / u, ⊥ / w] +    * = R [ p1/t, q1 / u, ⊥ / w], idem que précédemment, sauf que c'est R qui est modifiée et plus S. 
-  * Additionneur //n//-bits: +  * Additionneur //n//-bits : soit V'[B',A'n-1,...,A'1] le vecteur de taille //n// obtenu pour un additionneur de taille //n-1//, on va construire le vecteur résultat V =[B,An,An-1,...,A1] de taille //n+1// 
-    * A//n// = S [ p//n// / t, q//n// / u, B//n-1// / w ] +    * A//1// à A//n-1// : on ne change rien : A'//i//=A//i// ; 
-    * B//n// = R [ p//n// / t, q//n// / u, B//n-1// / w ]+    * A//n// = S [ p//n// / t, q//n// / u, B' / w ], B' est le dernier bit de sortie d'un additionneur à //n-1//-bit que l'on va l'additionner aux bits p//n//et  q//n//. Autrement dit, B', est la retenue de la somme de  p//n-1//et  q//n-1// quand on pose l'addition ; 
 +    * B = R [ p//n// / t, q//n// / u, B' / w ], où  B' est le dernier bit de sortie d'un additionneur à //n-1//-bits, c'est le bit de poids le plus fort du vecteur V', c'est la retenue de l'addition de  p//n// et  q//n// evec la retenue  de p//n-1//et  q//n-1//.
  
-Écrire la fonction ''additionneur'' suivante:<code c++>vector<formule> additionneur(int taille);</code> 
  
-On pourra procéder de manière itérative en s'appuyant sur deux ''vector<formule>''un qui contiendra les A//i//, l'autre contenant les B//i//. +=== Exercices === 
-A la fin de la fonction, il suffira de renvoyer les ''vector'' contenant les A//i// juste après lui avoir ajouté la formule B//n//+ 
 +  * Écrire la fonction ''additionneur'' suivante qui construira les formule A//i// en commençant par 1 :<code c++>vector<formule> additionneur(int taille);</code> 
 +  * Écrire les tests unitaires associé et vérifier  pour //n=2// que votre formule est bien celle d'un additionneur binaire 
 +  * Modifier ensuite le ''main'' de façon à accepter un argument ''<nowiki>--check-adder</nowiki>''. Si cet argument est présent on supposera par convention que le fichier de formules contient les formules A'//1//, ... ,  A'//n//, B'//n// d'un additionneur //n//-bitsOn appellera la fonction ''additionneur(//n//)'' pour récupérer les //n+1// formules de la spécification correspondante. On construira la formule ¬( (A//1// ⇔ A'//1//) ∧ ... ∧ (A//n// ⇔ A'//n//) ∧ (B//n// ⇔ B'//n//) ). On testera la satisfiabilité de cette formule: si elle est insatisfiable, l'additionneur passé en argument est correct.
  
-Modifier ensuite le ''main'' de façon à accepter un argument ''<nowiki>--check-adder</nowiki>''. Si cet argument est présent on supposera par convention que le fichier de formules contient les formules A'//1//... ,  A'//n//, B'//n// d'un additionneur //n//-bits. On appellera la fonction ''additionneur(//n//)'' pour récupérer les //n+1// formules de la spécification correspondante. On construira la formule ¬(A//1// ⇔ A'//1//) ∧ ... ∧ (A//n// ⇔ A'//n//) ∧ (B//n// ⇔ B'//n//) )On testera la satisfiabilité de cette formule: si elle est insatisfiable, l'additionneur passé en argument est correct.+<note tip>Vous disposez de la fonction ''lit_formule**__s__**'' qui fonctionne similairement à ''lit_formule'', mais en lit plusieurs d'un coup et renvoie un ''vector<formule>'' (//c.f.// ''parser.hpp'').</note>
  
-<note tip>En testant votre programme, même avec des additionneurs très petits, vous verrez que le temps de calcul est élevé. La partie suivante vise à améliorer cette situation.</note>+<note tip>En testant votre programme, même avec des additionneurs très petits, vous verrez que le temps de calcul est élevé. La partie suivante vise à améliorer cette situation. La partie suivante est indépendante de la présente, le deux peuvent donc être travaillées en parallèle.</note>
 ===== Quatrième partie: optimisations ===== ===== Quatrième partie: optimisations =====
  
Ligne 387: Ligne 409:
   * v1, 14/10/13: maj date rendu, dépôt spiral, projet initial et lien forge.   * v1, 14/10/13: maj date rendu, dépôt spiral, projet initial et lien forge.
   * v2, 15/10/13: ajout de fonctions: lit2var et positif.   * v2, 15/10/13: ajout de fonctions: lit2var et positif.
-  * v316/10/13: informations compilation Windows/MacOSX+  * v316/10/13: informations compilation Windows/MacOSX 
 +  * v4, 16/11/13: aide sur erreur ''m[]'' qui n'est pas const 
 +  * v5, 24/11/13: modif partie sur additionneur 
 +  * v6, 18/12/13: mise à jour de la description de la fonction ''cherche'' dans sa première version