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/24 21:48] rthion [Mise à jour du projet] |
enseignement:logique:projet:2013 [2013/12/19 12:53] (Version actuelle) ecoquery [Organisation du projet] |
<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> |
| |
* ''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'' |
* sinon, mettre 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 satisfiable, renvoyer ''true'' | - sinon mettre la valeur de ''suiv'' à FAUX dans ''valeurs'' |
* sinon, remettre 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 à: |
| |
La génération de cette spécification par récurrence pour //n//-bits 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'' |
* B = R [ p1/t, q1 / u, ⊥ / w] | * B = 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' / w ], où B' est le dernier bit de sortie d'un additionneur à //n-1//-bits (récurrence) | * A//1// à A//n-1// : on ne change rien : A'//i//=A//i// ; |
* B = R [ p//n// / t, q//n// / u, B' / w ], où B' est le dernier bit de sortie d'un additionneur à //n-1//-bits (récurrence) | * 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//. |
| |
| |
* 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. | * 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>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>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>La partie suivante est indépendante de la présente, le deux peuvent donc être travaillées en parallèle.</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 ===== |
| |
* 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 | * 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 |