I am new to rust and am trying to parse SMT constraints from a file using the below code.
It seems to me that the rust compiler infers that the AST nodes have a reference to Solver. They should ideally only have a reference to the Context.
Is there a work around to convey to the compiler that the ast nodes should not have a reference to Solver. I tried translating the constraints to a different context before returning the assertions, that did not work. Does fixing this require changes to the crate or should I be using the APIs differently.
Code:
fn myfun<'a>(ctx: &'a z3::Context) -> Vec<z3::ast::Bool<'a>>{
let s = z3::Solver::new(&ctx);
let smt2 = std::fs::read_to_string("my_constr.smt2").unwrap();
s.from_string(smt2);
let assertions = s.get_assertions();
assertions
}
fn main() {
let config = z3::Config::new();
let ctx = z3::Context::new(&config);
let ret = myfun(&ctx);
}
Error message:
**error[E0515]: cannot return value referencing local variable `s`
--> src/scratch.rs:45:5
|
44 | let assertions = s.get_assertions();
| - `s` is borrowed here
45 | assertions
| ^^^^^^^^^^ returns a value referencing data owned by the current function
**
I am new to rust and am trying to parse SMT constraints from a file using the below code. It seems to me that the rust compiler infers that the AST nodes have a reference to Solver. They should ideally only have a reference to the Context.
Is there a work around to convey to the compiler that the ast nodes should not have a reference to Solver. I tried translating the constraints to a different context before returning the assertions, that did not work. Does fixing this require changes to the crate or should I be using the APIs differently.
Code:
Error message: