Need help interrupting Z3 computation

Hi,

I am using Z3 for solving some model on graphs. However, I need to enforce some timeout to collect statistics. In Z3, you create a Context on which symbolic variables and expressions are defined, and solved. This context can be configured, including setting a timeout. This does work for very small examples (like in the test of the z3 crate), however, it seems not to work in some other cases, including those problems that I am solving. This problem is a known and still open issue of Z3. However, the Context itself can interrupt any computation from another thread. But the Context cannot be shared between threads (it implements !Send and !Sync). Fortunately, the Context can give you a ContextHandle that is Send + Sync. But, it is still only defined for the same lifetime as its Context (which of course makes sense). This prevents me, however, from sending that ContextHandle to another thread to terminate it.

// initialized
// ctx: &'ctx z3::Context
// timeout: f64
// solver: z3::Solver<'ctx>
let ctx_handle = ctx.handle();
let done = std::sync::atomic::AtomicBool::new(false);
let timeout_enforcer = std::thread::spawn(move || {
    let mut elapsed: f64 = 0.0;
    while done.load(std::sync::atomic::Ordering::Relaxed) {
        if elapsed > timeout {
            ctx_handle.interrupt();
        }
        thread::sleep(Duration::from_secs_f64(0.01));
        elapsed += 0.01;
    }
});
let result = solver.check();
done.store(true, std::sync::atomic::Ordering::Relaxed);
timeout_enforcer.join().unwrap();

This produces the following error:

error[E0495]: cannot infer an appropriate lifetime due to conflicting requirements
   --> src/graph_solvers/smt.rs:291:31
    |
291 |         let ctx_handle = self.ctx().handle();
    |                               ^^^
    |
note: first, the lifetime cannot outlive the lifetime `'ctx` as defined here...
   --> src/graph_solvers/smt.rs:131:6
    |
131 | impl<'ctx, 'g, N, E, Ix, S, T> GraphSolver<'ctx, 'g, N, E, Ix, Context, T>
    |      ^^^^
note: ...so that the types are compatible
   --> src/graph_solvers/smt.rs:291:31
    |
291 |         let ctx_handle = self.ctx().handle();
    |                               ^^^
    = note: expected `&SmtGraphSolver<'_, '_, N, E, Ix, S, T>`
               found `&SmtGraphSolver<'ctx, 'g, N, E, Ix, S, T>`
    = note: but, the lifetime must be valid for the static lifetime...
note: ...so that the type `[closure@src/graph_solvers/smt.rs:293:46: 302:10]` will meet its required lifetime bounds...
   --> src/graph_solvers/smt.rs:293:32
    |
293 |         let timeout_enforcer = thread::spawn(move || {
    |                                ^^^^^^^^^^^^^
note: ...that is required by this bound
   --> /home/tibor/.local/share/rustup/toolchains/stable-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/thread/mod.rs:627:15
    |
627 |     F: Send + 'static,
    |               ^^^^^^^

For more information about this error, try `rustc --explain E0495`

So, it seems like 'ctx needs to be 'static. But this is impossible for me, because I will eventually spawn multiple different threads that all compute a different model by themselves, and hence, the lifetime 'ctx will be at most the lifetime of that specific thread.

Is it possible to share the ContextHandle between threads, if its associated lifetime is not 'static? Do I need unsafe code for that? Or do you know a better way of forcefully quitting Z3 computation after the timeout? (I don't care about the result if the timeout is exceeded).

p.s.: This is part of a project where I want to evaluate different models (solving a particular problem on graphs) with different backends (one of which is Z3, while others are LP solvers CoinCBC and HIGHS) with different types (real numbers and integers), on any graph petgraph::Graph<N, E, Directed, Ix>. In the error message, Ctx is the type of context (for Z3, it is Context), and T is the type of the solver (either u64 or f64). Finally, S is the z3 equivalent of that type (z3::ast::int for u64, and z3::ast::Real for `f64).

You can do this with scoped threads such as those provided by crossbeam or rayon. (The difference between those being whether the threads are reused in a threadpool or not.)

1 Like

Thanks! That worked (it at least compiled). But unfortunately, the solver still does not terminate, even if I call ContextHandle::interrupt. So it seems like the only possibility to abort the computation is to kill the thread. I know that killing a thread is basically not possible in rust. So is the only alternative to compile a program separately that does the computation, spawn it using std::process, send data in some serialized form, and terminate it using std::process::Child::kill?

Indeed you cannot kill threads. Using a separate process would probably work, yes.

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.