Can solver::unsat_core() be interrupted by context::interrupt()?

[m-carrasco]

Hi,

I just wanted to ask if a solver computing unsat_core() can be interrupted by context::interrupt(). In other words, I'd like to know if solver::unsat_core() is interruptable. In this case, the solver is configured to minimise the unsat core.

Thanks in advance!

Best regards,
Manuel

[m-carrasco]

In case it helps anybody, context::interrupt() can interrupt unsat_core(). When unsat_core() is interrupted, it looks like it returns the best result found so far.

However, I am not sure if the interruption based on a timeout can be implemented using Z3 API. At the moment, I had to work around it using a different thread.

[NikolajBjorner]

I added handlers for timeout inside the API for unsat cores. It should now respect timeouts and resource limits

[m-carrasco]

Thank you so much! I will test it as soon as I can.

[m-carrasco]

@NikolajBjorner Just to learn, why is an exception thrown when the unsat core is empty?

[NikolajBjorner]

it isn't safe: if it ends up canceling before extracting the first core it will be empty because it wasn't filled in. This is unsound.
So choosing between unsoundness and inconvenience, I re-throw on timeout/exception and empty core.