Mark self as mut borrow in solver methods?

[108anup]

I am new to rust, but I noticed that the functions like Solver::assert borrow an immutable reference to self. Should these be annotated as mutable given that such functions modify the solver object. If not, could you please explain the rationale behind it.

pub fn assert(&self, ast: &ast::Bool<'ctx>) {
    ///       ^^^^^ Here
    debug!("assert: {:?}", ast);
    unsafe { Z3_solver_assert(self.ctx.z3_ctx, self.z3_slv, ast.z3_ast) };
}

[Pat-Lafon]

I think this is best described as the Interior Mutability Pattern since all objects are secretly reference counted on the Z3 c side of things.

[108anup]

Okay, I guess the reference counting can ensure memory leaks are absent. But that may not protect against race conditions, right?

For example, one might borrow a solver for its model in a closure. Then one might update the solver assertions, and then query the closure. If now the closure is called, then the result is for the updated solver.

The onus is then on the user to ensure that such things don't happen. There are no compile-time or run-time checks for this, right? If the annotation is made mutable, then such behaviors would not be allowed by the compiler. What is the benefit of keeping the annotation immutable?

In the above example, the closure could just borrow the model and not the solver to avoid any inconsistency. But ideally IMO, the compiler should force the user to do this and this should not be a choice because isn't such safety the whole point of rust, otherwise one might as well use C++.

[waywardmonkeys]

IIRC, the underlying C++ code is already thread safe which is why we were able to remove the Z3_MUTEX that existed in earlier versions of the code.

If you start to use &mut self, you also make it harder to use some of this from multiple threads (which I think some people do or did do...)

[Pat-Lafon]

How does one write this program? I'm not super familiar with threads so more for my own benefit. So I think almost all of the major structures in the z3 crate are !Send and !Sync because raw pointers are one of the exceptions for auto-deriving these(https://doc.rust-lang.org/nomicon/send-and-sync.html). Thus you can't just trivially pass a reference into a spawned thread without a compiler error.

You can isolate everything into it's own thread, but that seems safe to me anyways given z3's guarantees here.

use std::{
    thread::{self, sleep},
    time::Duration,
};

use z3::{
    ast::{Ast, Int},
    Config, Context, Solver,
};

fn main() {
    let mut handles = Vec::new();
    for _ in 0..5 {
        let handle = thread::spawn(move || {
            let cfg = &Config::new();
            let ctx = Context::new(cfg);
            let x = Int::new_const(&ctx, "x");
            let solver = Solver::new(&ctx);
            sleep(Duration::from_secs(1));
            solver.assert(&x._eq(&x));
            sleep(Duration::from_secs(1));
            solver.check();
        });
        handles.push(handle);
    }

    for t in handles.into_iter() {
        t.join().unwrap();
    }

    println!("Hello, world!");
}