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/11/17 15:18]
rthion [Mise à jour du projet]
enseignement:logique:projet:2013 [2013/12/19 12:53] (Version actuelle)
ecoquery [Organisation du projet]
Ligne 55: 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 256: 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 292: 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 401: Ligne 411:
   * v3, 16/10/13: informations compilation Windows/MacOSX   * v3, 16/10/13: informations compilation Windows/MacOSX
   * v4, 16/11/13: aide sur erreur ''m[]'' qui n'est pas const   * 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