z3.rs
z3.rs copied to clipboard
Update bindings for Z3 4.8.6
The exported functions from the C API have changed:
+ pub fn Z3_mk_set_has_size(c: Z3_context, set: Z3_ast, k: Z3_ast) -> Z3_ast;
+ pub fn Z3_get_seq_sort_basis(c: Z3_context, s: Z3_sort) -> Z3_sort;
+ pub fn Z3_get_re_sort_basis(c: Z3_context, s: Z3_sort) -> Z3_sort;
+ pub fn Z3_mk_lstring(c: Z3_context, len: ::std::os::raw::c_uint, s: Z3_string) -> Z3_ast;
+ pub fn Z3_get_lstring(
+ pub fn Z3_mk_str_lt(c: Z3_context, prefix: Z3_ast, s: Z3_ast) -> Z3_ast;
+ pub fn Z3_mk_str_le(c: Z3_context, prefix: Z3_ast, s: Z3_ast) -> Z3_ast;
+ pub fn Z3_mk_seq_nth(c: Z3_context, s: Z3_ast, index: Z3_ast) -> Z3_ast;
+ pub fn Z3_mk_seq_last_index(c: Z3_context, arg1: Z3_ast, substr: Z3_ast) -> Z3_ast;
+ pub fn Z3_mk_linear_order(
+ pub fn Z3_mk_partial_order(
+ pub fn Z3_mk_piecewise_linear_order(
+ pub fn Z3_mk_tree_order(c: Z3_context, a: Z3_sort, id: ::std::os::raw::c_uint) -> Z3_func_decl;
+ pub fn Z3_mk_transitive_closure(c: Z3_context, f: Z3_func_decl) -> Z3_func_decl;
- pub fn Z3_get_parser_error(c: Z3_context) -> Z3_string;
- pub fn Z3_apply_result_convert_model(
+ pub fn Z3_solver_get_trail(c: Z3_context, s: Z3_solver) -> Z3_ast_vector;
+ pub fn Z3_solver_get_levels(
+ pub fn Z3_solver_to_dimacs_string(c: Z3_context, s: Z3_solver) -> Z3_string;
- pub fn Z3_fixedpoint_push(c: Z3_context, d: Z3_fixedpoint);
- pub fn Z3_fixedpoint_pop(c: Z3_context, d: Z3_fixedpoint);
+ pub fn Z3_optimize_assert_and_track(c: Z3_context, o: Z3_optimize, a: Z3_ast, t: Z3_ast);
I just tried to get set up with a project that relied on this one. But the z3 get model code was always returning 0s. I think it is because when I ran sudo apt get install libz3-dev I got a 4.x version.
a. As someone that has never used Z3 before, How can I help get this project compatible with new versions? b. As someone that is not very experienced with ubuntu, How can I get a compatible version of z3 set up? c. How can we change the build script so we get the error at build time instead of runtime?
I'm running z3 4.8.10; looks like this has been resolved.