Ci-dessous, les différences entre deux révisions de la page.
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/25 22:55] rthion [Exploration de l'espace de recherche] |
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// | 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// | ||
- | 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//. | ||
</ | </ | ||
Ligne 257: | Ligne 256: | ||
La fonction procèdera comme suit: | La fonction procèdera comme suit: | ||
- | - mettre la valeur de '' | + | |
- | - s'il reste des variables à affecter, appeler | + | - sinon: |
- | - sinon tester la valeur de la cnf | + | |
- | * si la formule | + | - Appeler |
- | | + | - si l' |
- | | + | |
- | | + | - Appeler |
+ | | ||
+ | | ||
- | <note warning> | + | |
- | * il n'y a pas besoin de faire de "push_back" | + | <note warning> |
- | * on peut déterminer que toute les variables ont été affectées en comparant | + | * il n'y a pas besoin de faire de '' |
+ | * on peut déterminer que toute les variables ont été affectées en comparant | ||
</ | </ | ||
Ligne 304: | Ligne 306: | ||
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 |
- | * B = R [ p1/t, q1 / u, ⊥ / w] | + | * B = R [ p1/t, q1 / u, ⊥ / w], idem que précédemment, |
- | * Additionneur // | + | * Additionneur //n//-bits : soit V' |
- | * A//n// = S [ p//n// / t, q//n// / u, B' / w ], où | + | * A//1// à A//n-1// : on ne change rien : A'// |
- | * B = R [ p//n// / t, q//n// / u, B' / w ], où B' est le dernier bit de sortie d'un additionneur à // | + | * 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' |
+ | * B = R [ p//n// / t, q//n// / u, B' / w ], où B' est le dernier bit de sortie d'un additionneur à // | ||
Ligne 409: | Ligne 412: | ||
* v4, 16/11/13: aide sur erreur '' | * v4, 16/11/13: aide sur erreur '' | ||
* 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 '' |