Trait PrepareSynchronized

Source

pub trait PrepareSynchronized {
    type Inner;

    // Required method
    fn synchronized(&self) -> Synchronized<Self::Inner>;
}

Expand description

This trait allows a type to opt-in to multithreading through Synchronized.

Instead of implementing this trait, users should prefer to implement Translate to take advantage of its blanket implementation of PrepareSynchronized.

§Usage

Synchronized handles can be moved to another thread.

use z3::ast::{Bool, Int};
use z3::{Context, PrepareSynchronized, Solver, Translate};

// Creating a Synchronized<BV> and moving it to another thread.
let bv = Bool::from_bool(true);
let sendable = bv.synchronized();
std::thread::spawn(move || {
    let moved = sendable.recover();
    assert_eq!(moved.as_bool(), Some(true));
}).join().expect("Thread panicked");

Synchronized handles can hold anything that is Translate, including Asts, Solvers and Models. This allows the pattern of defining a set of Asts and Solvers in a main thread and offloading the actual Solver::check call to a worker thread, with the eventual resulting model being moved back into the main thread.

 // Creating a Solver with some assertions, checking it from a thread,
 // and moving the resulting model back out for inspection.
 use z3::ast::{Ast, Bool};
 use z3::{Context, PrepareSynchronized, Solver};
 let bool = Bool::new_const("hello");
 let sendable_solver = {
     let solver = Solver::new();
     solver.assert(&bool._eq(&Bool::from_bool(true)));
     solver.synchronized()
 };
 let model = std::thread::spawn(move || {
     let moved_solver = sendable_solver.recover();
     moved_solver.check();
     let model = moved_solver.get_model().unwrap();
     model.synchronized()
 }).join().expect("Thread panicked");
 let model = model.recover();
 assert_eq!(model.eval(&bool, true), Some(Bool::from_bool(true)));

Consumers of this library may implement Translate for their types that use Z3 structures, to directly enable their usage in multi-threaded scenarios.

 // Implementing Translate for a struct containing a BitVector and
 // an Int, and then creating a Synchronized from it and moving
 // it to a thread
 struct MyStruct {
     bv: Bool,
     int: Int,
 }

 unsafe impl Translate for MyStruct {
     fn translate(&self, ctx: &Context) -> Self {
         MyStruct {
             bv: self.bv.translate(ctx),
             int: self.int.translate(ctx),
         }
     }
 }

 let my_struct = MyStruct {
     bv: Bool::from_bool(true),
     int: Int::from_i64(42),
 };
 let sendable_struct = my_struct.synchronized();
 thread::spawn(move || {
     let moved = sendable_struct.recover();
     assert_eq!(moved.bv.as_bool(), Some(true));
     assert_eq!(moved.int.as_i64(), Some(42));
 }).join().expect("Thread panicked");