search

ilsordo / SAT-SMT-Solver

A SAT/SMT solver in OCaml
2 stars 2 forks source link

Assert failure (clause vide créée immédiatement après pari) #3

Closed yhamoudi closed 10 years ago

yhamoudi commented 10 years ago

C'est une erreur qui se manifeste sur ex5.cnf

Voir le fichier ex5.log dans le dossier tests pour le déroulement détaillé de l'algo (les lignes importantes sont suivies de **)

Déroulement de l'algo :

dans la clause 77 (-14 17 -3) : on pari 17 = faux on pari 14 = vrai

singleton sur clause 29 entraine 3 = true clause 77 devient vide on pari faux sur 14 clause 77 cachée dans "clauses" manifestement 77 n'est pas cachée dans les occ_neg de 3 (on devrait avoir le message "Clause_neg 77 hidden for var 3") il semble que 3 n'est pas visible à ce moment dans 77 on pari 3 = vraie on observe (via occ neg de 3) que 77 est vide !!! <<< il ne faut pas voir 77 à ce stade

La question principale : pourquoi jamais de "Clause_neg 77 hidden for var 3" ? (et en fait pour bcp d'autres vars on devrait avoir ce message alors qu'il n'apparait pas)

Pistes de réflexions : est-ce que set_val/reset_val/show_occ... sont correctes ? par ex, quand on fait show_occurences, est-ce qu'on ne rend pas visible d'anciennes clauses cachées ? faut-il traiter différement v_ref dans show_occ/hide_occ ?

yhamoudi commented 10 years ago

Peut-être une avancée (!) : dans reset_val : on écrit "let (annuler,restaurer)=if b...". J'ai l'impression que le couple (annuler,restaurer) devrait être inversé.

Avec l'inversement :

cf le commit pour le code (où j'ai juste changé "let (annuler,restaurer)=if b..." en "let (annuler,restaurer)=if (not b)...", ce qui revient (en plus sale) à permuter (annuler,restaurer))

Après tests plus poussés, je confirme que le bug vient de là ! Je remplace (not b) par l'inversion de la paire et ce sera bon.

ilsordo commented 10 years ago

Je confirme, j'avais inversé les noms, j'ai réécrit ce morceau pour que ce soit plus clair

yhamoudi commented 10 years ago

tu as push ? Sinon, tout semble marcher !!!

(par contre il y a un peu trop de printf, du coup ça devient dur de trouver le résultat au milieu. On les enlève tous ? on les commente ?)

Le 2014-02-26 21:05, nagaaym a écrit :

Je confirme, j'avais inversé les noms, j'ai réécrit ce morceau pour que ce soit plus clair

Reply to this email directly or view it on GitHub [1].

Links:

[1] https://github.com/nagaaym/projet2/issues/3#issuecomment-36170212

ilsordo commented 10 years ago

On enlève tout et si il faut les récupérer on peut remonter les commits, Je m'en occupe