Module rsmt2::asynch

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 report unknown. This is what the examples below do.

This is why Solver::async_check_sat_or_unk is marked unsafe: 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.