search

prove-rs / z3.rs

Rust bindings for the Z3 solver.
337 stars 105 forks source link

Add consequences to solver #302

Open VadeveSi opened 1 month ago

VadeveSi commented 1 month ago

Hi,

I wanted to work towards adding support for Z3's consequences to the Solver. I figure something like

pub fn get_consequence(self,
                       mut assumptions: &[ast::Bool<'ctx>],
                       mut variables: &[ast::Bool<'ctx>]
                       ) -> &[ast::Bool<'ctx>] {
...
}

should work as a high-level wrapper around z3_sys::Z3_solver_get_consequences, but this requires the data to be in a Z3_ast_vector and I'm struggling on how to do that. Do you have any suggestions on how to do this? Am I overlooking something obvious?

Thanks.