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] |
* 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 ==== |
| |
<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> |
| |
* 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> |
| |
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> |
| |
* ''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 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] | * 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//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//-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>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 ===== |
| |
* 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. |
* 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 |
| * 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 |