z3.rs icon indicating copy to clipboard operation
z3.rs copied to clipboard

Update bindings for Z3 4.8.6

Open waywardmonkeys opened this issue 6 years ago • 2 comments

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);

waywardmonkeys avatar Sep 24 '19 06:09 waywardmonkeys

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?

Eh2406 avatar Feb 07 '20 22:02 Eh2406

I'm running z3 4.8.10; looks like this has been resolved.

jakeisnt avatar Jul 27 '21 04:07 jakeisnt