Module rsmt2::asynch [−][src]
This modules handles asynchronous interactions with the solver.
The related function is
Solver::async_check_sat_or_unk
.
Presently, only asynchronous check-sat-s are supported. The idea is to wrap the whole solver in a new thread, and yield a future of the check-sat result. The new thread starts parsing the output right away, which is going to block it. Once it’s done, it sends a message to its parent thread with the result.
This module uses unsafe code so that the wrapper retains the &mut solver
(for lifetimes), but
the background thread can read the solver’s output. If none of your queries on the wrapper
produce a result, i.e. the solver is still trying to answer the check-sat, and the wrapper is
dropped, the drop action will wait for the slave thread to produce an answer. This is
because otherwise the background thread would keep on listening to solver
, making using
solver
after the wrapper is dropped unsafe. On this topic, do read the following remark.
NB: when the check runs forever, the slave process will keep on waiting for the solver to answer. If you want to be able to keep using the solver in this case, you should spawn the solver with the right options to add a timeout. For Z3,
-t:500
for a (soft, per query) timeout, which makes it reportunknown
. This is what the examples below do.This is why
Solver::async_check_sat_or_unk
is markedunsafe
: if not careful, one can end up with a background process burning 100% CPU.
Examples
These examples use the second SMT-LIB script from this stack overflow question as a script that Z3 struggles with.
fn do_smt_stuff() -> rsmt2::SmtRes<()> { use std::io::Write; let parser = () ; use rsmt2::SmtConf ; let mut conf = SmtConf::default_z3(); // Setting a timeout because our query will run "forever" otherwise. conf.option("-t:100"); let mut solver = conf.spawn(parser)? ; writeln!(solver, r#" (declare-fun f (Real) Real) (assert (forall ((a Real) (b Real)) ( = (+ (f a) (f b)) (f (+ a b)) ))) (assert (= (f 2) 4)) "#)?; { // The following mut-borrows `solver`, this scope lets us use `solver` again afterwards. let future = unsafe { solver.async_check_sat_or_unk() }; // Non-blocking. let maybe_result = future.try_get(); assert! { maybe_result.is_none() } // Blocking with timeout. let maybe_result = future.timeout_get(std::time::Duration::new(0, 50)); assert! { maybe_result.is_none() } // Blocking. let result = future.get(); assert! { result.expect("reached timeout").is_none() } } // We can re-use the solver now. let result = solver.check_sat_or_unk(); assert! { result.expect("reached timeout").is_none() } Ok(()) } do_smt_stuff().unwrap()
Structs
CheckSatFuture | Master thread. |