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/12/16 11:10]
rthion [Formules de spécification]
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 257: Ligne 256:
  
 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: <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:
Ligne 410: Ligne 412:
   * 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