search

kino-mc / rsmt2

A generic library to interact with SMT-LIB 2 compliant solvers running in a separate system process, such as Z3 and CVC4.
Apache License 2.0
65 stars 14 forks source link

Non-blocking check-sat #9

Closed HiDefender closed 3 years ago

HiDefender commented 5 years ago

Is there a way to check-sat without blocking the current thread? Along with that a way to see if the solver has finished is needed.

I'm enjoying rsmt2, thank you for you effort!

AdrienChampion commented 5 years ago

Wow, I'm so sorry, for some reason I did not get notified of your issue :(

The answer is yes, you can issue a checksat, do some stuff, and then ask for the result. However the second call, which retrieves the result, will block the current thread (at least currently).

You want to take a look at the print_check_sat* and parse_check_sat* functions.

Check them out and let me know if they work for you (as rsmt2's main user I don't use this feature a lot).

And thank you for you interest and enthousiasm in rsmt2!

AdrienChampion commented 5 years ago

@HiDefender again, sorry I took so long to get back to you, did I answer your question in the previous post? If so, could you go ahead and close this issue?

HiDefender commented 5 years ago

@AdrienChampion now it is my turn to apologize for the delay in responding.

print_check_sat is lovely, but a non-blocking try_check_sat would be really useful.

Thank you

AdrienChampion commented 5 years ago

Hmmm, what you want is something like print_check_sat and then a try_check_sat which, typically, would return a Option<bool> depending on whether the solver has answered at this point?

If so then the answer is no, you cannot do this currently. As far as I can tell, to do this rsmt2 would need to put the actual solver in a separate thread which attempts to read the solver's stdout, and wait for that thread to send a message.

It's definitely possible, although it would be non-trivial. I'll look into it while you confirm (or not) that it's what you want.

AdrienChampion commented 5 years ago

@HiDefender Assuming what I describe above is what you want, take a look at the async_checksat branch of rsmt2 I just pushed.

There's a new asynch module with an example of what it allows to do. The relevant function on Solver is async_check_sat_or_unk. You can see it used in the example.

If this is what you are looking for, can you give it a try and tell me what you think?

The main limitation is that when you drop the "future/wrapper" to re-use your solver, rsmt2 will wait for the solver to produce an answer (or timeout, see the documentation for details). I could not find a portable way to cancel the query with a SIGINT. If you know how to do this I am interested, not only for this particular use-case but in general.

HiDefender commented 5 years ago

@AdrienChampion Thank you for your work, the result is nice.

As to canceling the query portably, I can't think of a way. Maybe someone as a library for SIGINT across platforms? Does SMT-LIB2 have a standardized way of interpreting SIGINT? Will z3, CVC4, etc behave the same?

If I come across something I will let you know.

Once again, thank you.

AdrienChampion commented 5 years ago

@HiDefender I'm re-opening this issue because other people might be interested in this feature.

I'm not sure how to make it safe in the sense that I don't know how to cancel the asynchronous query. If you don't mind, and if you've been using it, could you provide some feedback? In particular about how to make sure users are aware that they could leave a solver hanging, burning 100% CPU for a check-sat that will not end?

I thought about this a little bit and here's the best solution I have: mark all functions related to this feature as unsafe. It doesn't really solve the problem itself, but properly advertises that this feature is dangerous and (hopefully) forces users to RTFM and be aware of its pitfalls.

What do you think?

HiDefender commented 5 years ago

@AdrienChampion I did a little research online, including the SMT-LIB 2 standard. There doesn't seem to be any way other than timeout to cancel a solver.

I think it is fair to mark async_check_sat_or_unk() as unsafe, because as you said it "could leave a solver hanging, burning 100% CPU for a check-sat that will not end".

Likewise I think that get() for CheckSatFuture can be marked unsafe lest someone think that it is non-blocking because of async_check_sat_or_unk().

The other methods like try_get() and timeout_get() I would leave as safe though. These methods seem to be self explanatory, and unsafe in this context is being used to make sure someone RTFM as you said.

My two cents.

AdrienChampion commented 3 years ago

@HiDefender sorry it took so long to actually merge this. I will shortly release v0.11.0 which will include asynchronous check-sat-s.