search

ilsordo / SAT-SMT-Solver

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

Assert_failure : tentative de double pari #2

Closed yhamoudi closed 10 years ago

yhamoudi commented 10 years ago

Pistes de recherche pour résoudre l'erreur "Fatal error: exception Assert_failure("formule.ml", 126, 18) " que l'on obtient par exemple en exécutant ex1.cnf

maj : il semble que ces 2 corrections suffisent. Maintenant sur ex1.cnf ça termine et on obtient UNSATISFIABLE...

ilsordo commented 10 years ago

minisat dit satisfiable sur ex1, j'ai commenté un morceau de code suspicieux dans mon dernier commit

yhamoudi commented 10 years ago

oui la réponse est mauvaise (c'est l'ex1 du prof). Sur reset_val il manquait bien le remove ?

ilsordo commented 10 years ago

effectivement, tu peux commit tes modifications?

ilsordo commented 10 years ago

Pour find_singleton je vais le réécrire en plus simple

yhamoudi commented 10 years ago

j'ai des modifs à envoyer mais je doit d'abord faire un merge

ilsordo commented 10 years ago

Ok

yhamoudi commented 10 years ago

j'ai push (avec recherche naive de doublons dans find_singleton). je regarde dpll + propagation

yhamoudi commented 10 years ago

en fait sur ex2.cnf le pb revient...

ilsordo commented 10 years ago

tu as push?

yhamoudi commented 10 years ago

à l'instant

ilsordo commented 10 years ago

Ok, on verra tout ça demain.

yhamoudi commented 10 years ago

ah je n'ai plus le pb sur ex2.cnf :? pour les gros tests ça envoie tjrs insatisfiable mais pour test.cnf ça marche

yhamoudi commented 10 years ago

Après réapparition du bug (immédiatement détruit), il y avait aussi la correction suivante à effectuer : dans constraint_propagation, on ne fait jamais List.iter (fun v -> formule#reset_val v) var_prop; alors qu'il fallait le faire lorsqu'on avait "try_pari var false;" suivi de "aux()=false"