prove-rs / z3.rs

Rust bindings for the Z3 solver.
353 stars 113 forks source link

[Feature Request] Owned AST nodes #144

Open black-binary opened 3 years ago

black-binary commented 3 years ago

AST node structs, like ast::Bool and ast::BV, contain reference to the Context. So if I want to store these nodes into my struct, Vec, or something like that, I have to transmute the nodes into <'static>.

Therefore I think we can just implement some "owned" node structs, without lifetime annotations. Like this one:

pub struct OwnedBV {
    pub(crate) ctx: Z3_context,
    pub(crate) z3_ast: Z3_ast,
}

And when this struct drops, invoke Z3_dec_ref for both the context and the AST.

If you are ok with that, I'd like to try to implement this feature and make a PR for it. :smile:

GreenBeard commented 3 years ago

You can also just do something like:

struct Foo<'a> {
  a: z3::ast::Bool<'a>,
}

fn example() {
  let config: z3::Config = z3::Config::new();
  let context = z3::Context::new(&config);
  let foo = Foo {
    a: z3::ast::Bool::new_const(&context, "test"),
  };
  // Do something
}

I would recommend reading up on Rust lifetimes (the official Rust book is a good source of information).