Add consequences to solver

[VadeveSi]

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.