search

ibex-team / ibex-lib

IBEX is a C++ library for constraint processing over real numbers.
http://ibex-team.github.io/ibex-lib/
GNU Lesser General Public License v3.0
67 stars 51 forks source link

Add SIGINT handling in Solver on POSIX systems #438

Open amarendet opened 4 years ago

amarendet commented 4 years ago

Proposition pour capturer les SIGINT sur les systèmes POSIX, via la fonction sigaction du header <signal.h> de la norme POSIX. Des fonctions additionnelles sont définies dans un nouveau header ibex_signals.h. Les gestion des signaux doit être activée manuellement.

amarendet commented 4 years ago

En réponse à #421

gchabert commented 4 years ago

Salut Antoine, Merci pour la PR. J'ai commencé à tester. J'observe plusieurs problèmes. Le premier est que les COV ne sont pas correctement sauvegardés: je soupçonne fortement que les 'pending' boxes aient été oubliées! Par exemple, si je résouds le problème suivant qui a 128 solutions: ./ibexsolve ../benchs/solver/polynom/ponts-geo.bch sans ^C, j'obtiens bien 128 solutions. Si je le lance et que je l'interromps dès le début, j'obtiens par exemple 9 solutions (c'est normal):

 user abort

 number of solution boxes:  9
 number of boundary boxes:  --
 number of unknown boxes:   --
 number of pending boxes:   --
 cpu time used:         0.292068s
 number of cells:       41

mais on voit qu'il manque les pending boxes, et si je poursuis la recherche, elle s'arrête immédiatement (et perd des solutions):

solving successful!

 number of solution boxes:  9
 number of boundary boxes:  --
 number of unknown boxes:   --
 number of pending boxes:   --
 cpu time used:         4.00001e-06s [total=0.292072]
 number of cells:       0 [total=41]

Le second problème est que le signal n'a pas l'air d'être capturé de façon asynchrone et que le temps de réaction semble dépendre du nombre de cellules... Prenons par exemple le problème synthesis. Si je lance ./ibexsolve ../benchs/solver/others/synthesis.bch et que j'interromps la recherche au bout de 5s, le programme met quelques secondes à s'arrêter (ça me paraît déjà un peu lent, mais c'est ok). Par contre, si je laisse ibexsolve tourner 30s et que je l'interromps, il met quaiment 30s à s'arrêter.

amarendet commented 4 years ago

Salut Gilles,

Oui, désolé, la pull request était un peu prématurée, je me suis emballé et je me suis arrêté uniquement aux signaux et j'ai oublié le solveur... Je vais retravailler ça.