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).