Time limit?

[Michele Lombardi]

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.

Cheers,

Michele 

[Andrea Micheli]

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.

HTH

A.

--
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]

Thanks!

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]

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?

A. 

[1] https://github.com/pysmt/pysmt/blob/master/pysmt/solvers/portfolio.py