Time limit?

Skip to first unread message

Michele Lombardi

Jul 14, 2021, 9:12:54 AM7/14/21
to pySMT
Hi all,

I am trying to use PySMT for optimization (via binary search).

Anyone has experience with setting a limit?

1) PySMT itself does not seem to support it
2) Solutions based on SIGALRM or the "multiprocessing" python package do not seem to be effective, possibly due to solvers being C++ code with Python wrappers?

Any suggestion is welcome.



Andrea Micheli

Jul 15, 2021, 9:32:28 AM7/15/21
to Michele Lombardi, pySMT
Ciao Michele!

There was a similar question asked few months back: https://github.com/pysmt/pysmt/issues/689

TL;DR; without using the multiprocessing hack (if you kill the process it should reliably terminate), you must rely on solver-specific options to set a timeout. Z3 has something as shown in the issue, but mathsat does not.



You received this message because you are subscribed to the Google Groups "pySMT" group.
To unsubscribe from this group and stop receiving emails from it, send an email to pysmt+un...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/pysmt/ed6bf7ab-a2fa-4328-8ab4-b87b753f9046n%40googlegroups.com.

Le informazioni contenute nella presente comunicazione sono di natura privata e come tali sono da considerarsi riservate ed indirizzate esclusivamente ai destinatari indicati e per le finalità strettamente legate al relativo contenuto. Se avete ricevuto questo messaggio per errore, vi preghiamo di eliminarlo e di inviare una comunicazione all’indirizzo e-mail del mittente.
The information transmitted is intended only for the person or entity to which it is addressed and may contain confidential and/or privileged material. If you received this in error, please contact the sender and delete the material.

Michele Lombardi

Jul 15, 2021, 11:06:44 AM7/15/21
to Andrea Micheli, pySMT

We tried different approaches based on running external processes (or threads) and they seems to have some issues... We will try using pebble, as mentioned in the issue: let's see whether that does the trick :-)

Andrea Micheli

Jul 15, 2021, 11:42:49 AM7/15/21
to Michele Lombardi, pySMT
Did you also experience problems with the `Portfolio` meta-solver [1]? 
There, we use the normal `process.terminate()` of python and in our tests this works reliably on Linux and Windows (or at least we have not observed surviving behaviors yet).

Do you have an example where more extreme measures (like a SIGKILL) are needed? Which OS are you using?


Reply all
Reply to author
0 new messages