ilsordo / SAT-SMT-Solver

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

Time limit #12

Closed yhamoudi closed 10 years ago

yhamoudi commented 10 years ago

Empecher tps execution trop long

ilsordo commented 10 years ago

Le script tourne chez moi, essaie d'installer ruby 2.0.0 et dis moi si ça marche toujours pas

yhamoudi commented 10 years ago

alors je pense que j'ai réussi à installer la version 2.0.0 (en tout cas quand je fait : ruby --version, j'obtient : ruby 2.0.0p353 (2013-11-22 revision 43784) [x86_64-linux-gnu]) Si je lance ton script, j'obtient un graphe avec toutes les droites confondues avec l'axe des abscisses. Si je change k = (1..5).map {|x| 10_x} par k = (1..5).map {|x| 100_x} (dans def main), j'ai une erreur :

stats_script/base.rb:117:in to_gnuplot': undefined methodkeys' for nil:NilClass (NoMethodError)

from ./stats_script/script.rb:31:in `main'

from ./stats_script/script.rb:82:in `

'

ilsordo commented 10 years ago

C'est juste que après on sélectionne k=10, j'ai mis un message d'erreur si l'ensemble des données est vide, par contre je n'arrive pas à reproduire le coup des droites confondues.

yhamoudi commented 10 years ago

ah oui, j'avais pas remarqué.

Par contre, si je modifie rien et que j'envoie ./stats_script/script.rb, j'ai le message :

Warning: empty y range [0:0], adjusting to [-1:1]

Et le graphe :

capture du 2014-03-28 18 11 06

(et j'ai aussi des "Hiya" dans le terminal depuis le dernier commit :)

ilsordo commented 10 years ago

Est ce que tu peux lancer ./test.rb, taper 'debug' et m'envoyer le résultat?

On Fri, Mar 28, 2014 at 6:11 PM, yhamoudi notifications@github.com wrote:

ah oui, j'avais pas remarqué.

Par contre, si je modifie rien et que j'envoie ./stats_script/script.rb, j'ai le message [image: :+1:]

Warning: empty y range [0:0], adjusting to [-1:1]

Et le graphe :

[image: capture du 2014-03-28 18 11 06]https://cloud.githubusercontent.com/assets/6659728/2552615/fdcda14c-b69b-11e3-8298-c2beca084cda.png

Reply to this email directly or view it on GitHubhttps://github.com/nagaaym/projet2/issues/12#issuecomment-38943909 .

yhamoudi commented 10 years ago

je n'arrive plus à entrer ./test.rb, j'ai l'erreur suivante :

/usr/lib/ruby/2.0.0/rubygems/core_ext/kernel_require.rb:53:in `require': cannot load such file -- pry (LoadError)

from /usr/lib/ruby/2.0.0/rubygems/core_ext/kernel_require.rb:53:in `require'

from ./test.rb:5:in `

'

Si je fait juste "pry", je n'ai pas de message d'erreur

ilsordo commented 10 years ago

Essaie de refaire

gem install pry

Mais apparemment c'est un problème avec ton installation de ruby.

On Fri, Mar 28, 2014 at 6:51 PM, yhamoudi notifications@github.com wrote:

je n'arrive plus à entrer ./test.rb, j'ai l'erreur suivante :

/usr/lib/ruby/2.0.0/rubygems/core_ext/kernel_require.rb:53:in `require': cannot load such file -- pry (LoadError)

from /usr/lib/ruby/2.0.0/rubygems/core_ext/kernel_require.rb:53:in `require'

from ./test.rb:5:in `'

Reply to this email directly or view it on GitHubhttps://github.com/nagaaym/projet2/issues/12#issuecomment-38948461 .

yhamoudi commented 10 years ago

oui, c'est ce que je suis en train de regarder (si je repasse sous la 1.9 ./tests.rb marche)

yhamoudi commented 10 years ago

j'ai placé un fichier debug.txt à la racine du projet avec le résultat du debuggage

Est-ce que c'est possible que mes temps d'exécutions sur les bornes définies soient trop rapide (et du coup tout est arrondi à 0) ? Si dans le main de script.rb, si je remplace :

k = (1..5).map {|x| 10*x}

par

k = (1..5).map {|x| 100*x}

puis je met 100 (à la place de 10) dans le filter, j'obtiens des belles courbes :

capture du 2014-03-28 19 10 26

ilsordo commented 10 years ago

C'est ce qui apparait dans la base de données en tout cas, essaie de lancer des ./gen 50 3 30 | ./resol pour comparer

yhamoudi commented 10 years ago

ah oui, j'ai systématiquement 0.00000 !!! Donc ça marche bien (avec ruby 1.9). Merci :) (tu peux cacher les messages de debug du coup)

ilsordo commented 10 years ago

C'est fait.

yhamoudi commented 10 years ago

tu as ajouté la time limit ? (vu que tu as fermé l'issue)

ilsordo commented 10 years ago

J'en avais oublié le sujet de l'issue.

Je vais essayer.

yhamoudi commented 10 years ago

J'ai des doutes sur les temps moyens renvoyés. Par exemple, si je prend le test (n,l,k)=(100,3,500), j'ai une moyenne à 0.05 s sur les graphes obtenus. Or, si je génère des cnf de cette taille et que je les résout à la volée, ma moyenne est plutôt 0,5s. Pourquoi un facteur 10 d'écart ?

yhamoudi commented 10 years ago

Et 2 autres questions :

ilsordo commented 10 years ago

Pour les processeurs il suffit de changer Threads, pour populate tu fais:

./test.rb
pry(main)>  populate "nom_du_fichier"

et au bout de 10 minutes (change le 600 en 30 pour vérifier) tu devrais voir un fichier apparaitre.

yhamoudi commented 10 years ago

J'ai un pb avec populate. Je fais : ./test.rb

populate "temp.db"

b=Database::new "temp.db" (à ce niveau, j'ai l'impression que la base est déjà vide, il n'y a rien qui se déroule)

names = {:title => "Titre", :xlabel=>"Axe x", :ylabel => "Axe y"}

l = select_data(nil,3,nil,nil,nil) { |p,r| [p.k/(p.n.to_f),r.result.timers["Time (s)"]/r.count] }

Et là, j'ai :

Empty database => nil

Ce qui est bizarre, c'est que si je lance les mêmes tests mais à l'intérieur de main (avec affichage direct, sans stockage), ça marche bien...

ilsordo commented 10 years ago

Tu attends entre le populate et b = ... ?

2014-03-29 12:09 GMT+01:00 yhamoudi notifications@github.com:

J'ai un pb avec populate. Je fais : ./test.rb

populate "temp.db"

b=Database::new "temp.db" (à ce niveau, j'ai l'impression que la base est déjà vide, il n'y a rien qui se déroule)

names = {:title => "Titre", :xlabel=>"Axe x", :ylabel => "Axe y"}

l = select_data(nil,3,nil,nil,nil) { |p,r| [p.k/(p.n.to_f),r.result.timers["Time (s)"]/r.count] }

Et là, j'ai :

Empty database => nil

Ce qui est bizarre, c'est que si je lance les mêmes tests mais à l'intérieur de main (avec affichage direct, sans stockage), ça marche bien...

Reply to this email directly or view it on GitHubhttps://github.com/nagaaym/projet2/issues/12#issuecomment-38992617 .

yhamoudi commented 10 years ago

oui, j'attends bien qu'il ait finit. J'ai intégré le code de main à populate pour voir s'il réussissait à tracer une courbe avec les données qu'ils obtenaient (dans db) et ça marche bien. En fait, c'est le stockage dans temp.db qui ne marche pas.

ilsordo commented 10 years ago

Est ce qu'il y a eu des time limits pendant l'execution?

yhamoudi commented 10 years ago

non, je le fait sur des tests simples.

yhamoudi commented 10 years ago

j'ai du nouveau : le problème semble être lié à la fréquence de sauvegarde dans le fichier.

Je prends le test (n,l,k)=(100,3,100..1000) (k est un multiple de 100). Si je lance populate avec enregistrement toutes les 30s (sleep 30), j'obtiens bien des résultats dans mon fichier, mais ils s'arrêtent à k=600 (parfois k=800). Ex : tm

Du coup, j'ai soupçonné le fait suivant :

J'ai joué sur la borne de 30s et effectivement ça change le nombre de tests enregistrés dans le fichier.

ça explique aussi pourquoi le fichier est vide parfois : si tous les tests sont finis avant le 1er enregistrement, populate quitte sans rien enregistrer.

Du coup, il faudrait sauvegarder la bdd dans name à la fin de populate pour voir si ça corrige les pbs. J'ai essayé en ajoutant " db.save name" juste avant le end final de populate, mais ça ne semble pas marcher (on obtient des fichiers complètement vide)

ilsordo commented 10 years ago

Effectivement j'avais pas écrit populate pour qu'il termine vite, j'avais donc oublié de faire une dernière sauvegarde, c'est corrigé.

2014-03-29 16:22 GMT+01:00 yhamoudi notifications@github.com:

j'ai du nouveau : le problème semble être lié à la fréquence de sauvegarde dans le fichier.

Je prends le test (n,l,k)=(100,3,100..1000) (k est un multiple de 100). Si je lance populate avec enregistrement toutes les 30s (sleep 30), j'obtiens bien des résultats dans mon fichier, mais ils s'arrêtent à k=600 (parfois k=800). Ex : [image: tm]https://cloud.githubusercontent.com/assets/6659728/2558669/aca52880-b754-11e3-952b-618619a3249d.png

Du coup, j'ai soupçonné le fait suivant :

  • populate fait tourner ses tests et les enregistre toutes les 30s
  • à un moment, populate a terminé tous ses tests
  • au lieu de sauvegarder dans le fichier les derniers résultats, populate quitte, et donc il manque les résultats effectués dans le dernier intervalle de 30s

J'ai joué sur la borne de 30s et effectivement ça change le nombre de tests enregistrés dans le fichier.

ça explique aussi pourquoi le fichier est vide parfois : si tous les tests sont finis avant le 1er enregistrement, populate quitte sans rien enregistrer.

Du coup, il faudrait sauvegarder la bdd dans name à la fin de populate pour voir si ça corrige les pbs. J'ai essayé en ajoutant " db.save name" juste avant le end final de populate, mais ça ne semble pas marcher (on obtient des fichiers complètement vide)

Reply to this email directly or view it on GitHubhttps://github.com/nagaaym/projet2/issues/12#issuecomment-38998561 .

yhamoudi commented 10 years ago

ça ne marche pas chez moi : si je regarde le fichier de sauvegarde pendant l'exécution de populate (avant le dernier save), il est rempli. mais le dernier save vide complètement le fichier


tu rencontres aussi ce pb (ou j'essaye d'investiguer sur mon ordi) ?

ilsordo commented 10 years ago

Je pense avori trouvé, tout fonctionne chez moi.

2014-03-29 16:36 GMT+01:00 yhamoudi notifications@github.com:

ça ne marche pas chez moi : si je regarde le fichier de sauvegarde pendant l'exécution de populate (avant le dernier save), il est rempli. mais le dernier save vide complètement le fichier

Reply to this email directly or view it on GitHubhttps://github.com/nagaaym/projet2/issues/12#issuecomment-38998984 .

yhamoudi commented 10 years ago

super, ça marche !

J'ai testé le time limit et il y a qqs pbs (je sais si pas si tu l'as fini) :

Peut-être que l'on pourrait faire la chose suivante pour résoudre certains des problèmes précédant : on continue de n'enregistrer que les temps inférieurs à la time limit mais :

Question subsidiaire :

ilsordo commented 10 years ago

En fait je ne controle pas le mécanisme de timeout ( c'est une bibliothèque ruby) mais ta solution semble raisonnable, je vais l'ajouter au niveau de select_data. Par contre si tu peux reproduire le coup de count = -1 je pourrais essayer de corriger.

ilsordo commented 10 years ago

Pour la question subsidiaire: Si tu veux lancer plusieurs batteries de test et stocker dans une même base de données il faut la charger (db = Database::new) puis lancer les tests comme dans main ou populate. Si tu veux t'arreter au milieu d'un test c'est plus difficile.

ilsordo commented 10 years ago

J'ai ajouté un paramètre min_count à select_data

yhamoudi commented 10 years ago

Pour le count=-1, j'ai l'impression que ça arrive lorsque aucun des tests n'est sous le time limit (et du coup ça met -1 au lieu de 0). Je l'obtiens par exemple avec dpll + next_rand sur (n,l,k)=(100,3,500) (mais si t'as pas de chance, il peut y avoir un test (100,3,500) qui passe...). Si tu exécute le populate actuel, tu devrais pouvoir apercevoir un count=-1 lorsque tu fais b=Database::new "ex.db".

Concernant le time out, il y a un pb. Si je lance dpll sur (1000,3,4300) (avec time limit à 2s), ça tourne sans s'arrêter. C'est le comportement normal du time out (dans ce cas, autant enregistrer les temps supérieurs au time out) ? J'ai essayé de comparer ton code sur le time out à http://stackoverflow.com/questions/16454287/how-to-set-a-time-limit-for-a-ruby-code-to-run , mais les corrections que j'ai essayées ne donnent rien.

(le paramètre &block de select_data sert à qq chose quand on extrait des donnée ?)

ilsordo commented 10 years ago

&block permet de composer (select_data(...) { |p,r| ... }) . Le timeout devrait stopper l'ex?cution. Je regarde ?a.

2014-03-29 21:18 GMT+01:00 yhamoudi notifications@github.com:

Pour le count=-1, j'ai l'impression que ?a arrive lorsque aucun des tests n'est sous le time limit (et du coup ?a met -1 au lieu de 0). Je l'obtiens par exemple avec dpll + next_rand sur (n,l,k)=(100,3,500) (mais si t'as pas de chance, il peut y avoir un test (100,3,500) qui passe...). Si tu ex?cute le populate actuel, tu devrais pouvoir apercevoir un count=-1 lorsque tu fais b=Database::new "ex.db".

Concernant le time out, il y a un pb. Si je lance dpll sur (1000,3,4300) (avec time limit ? 2s), ?a tourne sans s'arr?ter. C'est le comportement normal du time out (dans ce cas, autant enregistrer les temps sup?rieurs au time out) ? J'ai essay? de comparer ton code sur le time out ? http://stackoverflow.com/questions/16454287/how-to-set-a-time-limit-for-a-ruby-code-to-run, mais les corrections que j'ai essay?es ne donnent rien.

(le param?tre &block de select_data sert ? qq chose quand on extrait des donn?e ?)

Reply to this email directly or view it on GitHubhttps://github.com/nagaaym/projet2/issues/12#issuecomment-39007617 .

ilsordo commented 10 years ago

Pour le -1 c'était une typo ça devrait être correct.

2014-03-29 21:34 GMT+01:00 Maxime Lesourd maxime.lesourd@gmail.com:

&block permet de composer (select_data(...) { |p,r| ... }) . Le timeout devrait stopper l'exécution. Je regarde ça.

2014-03-29 21:18 GMT+01:00 yhamoudi notifications@github.com:

Pour le count=-1, j'ai l'impression que ça arrive lorsque aucun des tests

n'est sous le time limit (et du coup ça met -1 au lieu de 0). Je l'obtiens par exemple avec dpll + next_rand sur (n,l,k)=(100,3,500) (mais si t'as pas de chance, il peut y avoir un test (100,3,500) qui passe...). Si tu exécute le populate actuel, tu devrais pouvoir apercevoir un count=-1 lorsque tu fais b=Database::new "ex.db".

Concernant le time out, il y a un pb. Si je lance dpll sur (1000,3,4300) (avec time limit à 2s), ça tourne sans s'arrêter. C'est le comportement normal du time out (dans ce cas, autant enregistrer les temps supérieurs au time out) ? J'ai essayé de comparer ton code sur le time out à http://stackoverflow.com/questions/16454287/how-to-set-a-time-limit-for-a-ruby-code-to-run, mais les corrections que j'ai essayées ne donnent rien.

(le paramètre &block de select_data sert à qq chose quand on extrait des donnée ?)

Reply to this email directly or view it on GitHubhttps://github.com/nagaaym/projet2/issues/12#issuecomment-39007617 .

yhamoudi commented 10 years ago

Maintenant j'ai des count=23 (au lieu de 20 au max), alors que j'ai sat=20.00 au plus (en particulier pour k=100, sat indique indique très probablement le nombre de tests menés puisqu'ils doivent tous être satisfiables). On dirait qu'il y a bien 20 tests menés et 23 comptés...

Pour gnuplot, lorsqu'il n'y a pas de points, il y a moyen de ne pas afficher la portion de courbe concernée (actuellement, ça se comporte comme si les points absents sont des (x,0)). Apparemment, gnuplot fait ça automatiquement si tu mets un string qcq là où il n'y a pas de données, ou bien si tu spécifies set datafile missing "blabla" dans skelp.p (et "blabla" là où il n'y a pas de données, peut-être que ça peut marcher avec blabla=0 ?)

ilsordo commented 10 years ago

Une solution partielle est de ne pas enregistrer les instances qui timeout systématiquement. (De toute manière ça engendrait des bugs si on essayait de relancer un tel test). Je pense que ça devrait aussi arranger les problèmes avec gnuplot.

yhamoudi commented 10 years ago

C'est-à-dire ne pas enregistrer à partir du moment où au moins 1 test timeout ?

ilsordo commented 10 years ago

Si tous les tests d'une série (dans run_tests par exemple) font timeout alors le résultat est {count = 0, result = nil } et ça risque de pourrir la database donc je les filtre au moment du record. Si certains tests font timeout on enregistre juste ce qui n'a pas timeout.

2014-03-29 23:13 GMT+01:00 yhamoudi notifications@github.com:

C'est-à-dire ne pas enregistrer à partir du moment où au moins 1 test timeout ?

Reply to this email directly or view it on GitHubhttps://github.com/nagaaym/projet2/issues/12#issuecomment-39010830 .

yhamoudi commented 10 years ago

ah ok, c'est parfait alors. Du coup, il reste juste le truc de l’absence de points. Si count est inférieur à la borne min demandée (et à fortiori s'il n'y pas de test), il faudrait avoir une absence de point.

ilsordo commented 10 years ago

Est ce que tu peux mettre dans une fonction dans script.rb la série de commande qui conduit à un point (x,0) ? Je pensais que c'était réglé.

2014-03-29 23:26 GMT+01:00 yhamoudi notifications@github.com:

ah ok, c'est parfait alors. Du coup, il reste juste le truc de l'absence de points. Si count est inférieur à la borne min demandée (et à fortiori s'il n'y pas de test), il faudrait avoir une absence de point.

Reply to this email directly or view it on GitHubhttps://github.com/nagaaym/projet2/issues/12#issuecomment-39011169 .

yhamoudi commented 10 years ago

je pense qu'on ne parle pas de la même chose. Je pensais faire ce qui est évoqué dans ce post : http://superuser.com/questions/440947/in-gnuplot-how-to-plot-with-lines-but-skip-missing-data-points J'ai testé les solutions apportées sur des fichiers à part et elles ne marchent pas. Si je trouve un truc qui marche, je t'en reparlerai.

yhamoudi commented 10 years ago

C'est bon, j'ai trouvé (et implémenté) ce que je que je voulais : maintenant, quand il manque des points, gnuplot n'affiche pas la portion de courbe correspondante.

Je reviens sur le timeout : j'ai légèrement modifié ton code car je pense que le rescue n'était pas au bon endroit (il était dans le timeout). Ça n'a pas corrigé le pb pour autant : le timeout est toujours ineffectif. Je pense que ça vient de ce que tu fais dans gen (cf http://stackoverflow.com/questions/17237743/timeout-within-a-popen-works-but-popen-inside-a-timeout-doesnt )

yhamoudi commented 10 years ago

De ce que j'ai pu lire, il est utopique de vouloir faire marcher le timeout de ruby comme on veut.

A la place on peut (peut-être ?) faire la chose suivante : lorsque tu lances (après IO::popen) : "./main -algo #{@algo} -h #{@heuristic} #{temp.path} 2>&1", il faudrait intégrer un timeout à l'intérieur de cette commande. Dans le shell ça se fait facilement avec "timeout 2m com" (2 minutes de time out pour l'exécution de la commande com), et on obtient en sortie :

If the command has not completed within the specified time limit, the timeout utility will kill it (by sending it a TERM signal) and then exit with status 124.

(http://fahdshariff.blogspot.fr/2013/08/executing-shell-command-with-timeout.html)

On obtient ainsi plusieurs moyens de provoquer un timeout correct de manière détournée :

yhamoudi commented 10 years ago

juste une petite question : si j'ai des tests pour n=100, l=[3,4,5], k=100..1000, algo="dpll", heur="dlis", est-ce que les fonctions actuelles permettent de superposer 3 courbes : temps en fonction de k, où chaque courbe correspond à une valeur de l ?

ilsordo commented 10 years ago

non mais ça doit être faisable. je regarde demain après midi en même temps que le convertisseur de tseitin.

2014-04-02 20:05 GMT+02:00 yhamoudi notifications@github.com:

juste une petite question : si j'ai des tests pour n=100, l=[3,4,5], k=100..1000, algo="dpll", heur="dlis", est-ce que les fonctions actuelles permettent de superposer 3 courbes : temps en fonction de k, où chaque courbe correspond à une valeur de l ?

Reply to this email directly or view it on GitHubhttps://github.com/nagaaym/projet2/issues/12#issuecomment-39363237 .

yhamoudi commented 10 years ago

j'aimerai lancer le test suivant :