ilsordo
commented
10 years ago Ca me va, par contre est ce que tu utilises record_timer en dehors de debug.ml?
Pour next_pari je pense pas que ce soit nécessaire. J'imagine que tu voulais écrire un truc du genre :
let next_pari (heuristique : formule -> (bool*var) option) = heuristique (self:>formule)Qui devrait être bien typé mais c'est pas très joli.
yhamoudi
J'ai réécrit les outils pour timer dans debug.ml Maintenant il n'y a plus d'objet à faire sortir pour démarrer/arrêter un timer. Tu peux relire ce que j'ai écrit (il y a 2 endroits où j'ai des doutes, cf les commentaires).
J'ai ajouté un nouveau timer : Choosing qui indique le temps passé par l'heuristique pour choisir la variable sur laquelle parier. Au début je pensais ajouter une méthode "next_pari" dans formule.ml qui prendrait une heuristique et renverrait un littéral, ça aurait permis de démarrer/arrêter le timer à l'intérieur de cette méthode. Je ne l'ai pas fait pour 2 raisons : des problèmes de type que je n'ai pas réussi à résoudre + je ne sais pas si c'est pertinent d'utiliser les outils de debug en dehors de main.ml/algo_wl.ml/algo_dpll.ml. Actuellement, je manipule les timer directement dans algo_wl.ml et algo_dpll.ml. Si tu penses qu'une méthode next_pari est plus pertinent, je te laisse la faire.
Je voulais aussi ajouter un timer pour la propagation, mais après réflexion on mesure le temps total et le temps des paris, donc on a : temps(propagation)=temps(total)-temps(paris). On pourrait aussi définir la propagation comme le temps mis pour propager un pari le plus loin possible, sans prendre en compte le backtrack, et là un timer spécifique pourrait avoir une utilité.