From 34bf4b1d3cb63b51720cbb627865b5001e6eebec Mon Sep 17 00:00:00 2001 From: martin-neuhaeusser Date: Mon, 11 Apr 2016 15:06:28 +0200 Subject: [PATCH 1/2] Fix installation of custom error handler during context creation in OCaml bindings This patch fixes a bug detected by valgrind, where a custom error handler did not get installed correctly. --- src/api/ml/z3native_stubs.c.pre | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/api/ml/z3native_stubs.c.pre b/src/api/ml/z3native_stubs.c.pre index 02bafeef6..47655c57e 100644 --- a/src/api/ml/z3native_stubs.c.pre +++ b/src/api/ml/z3native_stubs.c.pre @@ -436,8 +436,10 @@ void MLErrorHandler(Z3_context c, Z3_error_code e) n_* wrapper functions. */ } -void DLL_PUBLIC n_set_internal_error_handler(value a0) +CAMLprim value DLL_PUBLIC n_set_internal_error_handler(value ctx_v) { - Z3_context _a0 = * (Z3_context*) Data_custom_val(a0); - Z3_set_error_handler(_a0, MLErrorHandler); + CAMLparam1(ctx_v); + Z3_context_plus ctx_p = *(Z3_context_plus*) Data_custom_val(ctx_v); + Z3_set_error_handler(ctx_p->ctx, MLErrorHandler); + CAMLreturn(Val_unit); } From 67ac1a003e35fc5c2d730d5f06ee98707ad320ce Mon Sep 17 00:00:00 2001 From: "Martin R. Neuhaeusser" Date: Mon, 18 Apr 2016 17:14:48 +0200 Subject: [PATCH 2/2] Avoid conversion between mutable arrays and lists in OCaml API. This patch eliminates the conversion between OCaml arrays and lists from Z3's OCaml API. --- scripts/update_api.py | 30 ++++-- src/api/ml/z3.ml | 212 ++++++++++++++++-------------------------- 2 files changed, 98 insertions(+), 144 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 909f324f0..09a10f6cf 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -265,9 +265,9 @@ def param2ml(p): else: return "ptr" elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: - return "%s array" % type2ml(param_type(p)) + return "%s list" % type2ml(param_type(p)) elif k == OUT_MANAGED_ARRAY: - return "%s array" % type2ml(param_type(p)) + return "%s list" % type2ml(param_type(p)) else: return type2ml(param_type(p)) @@ -1043,8 +1043,6 @@ def arrayparams(params): op.append(param) return op - - def ml_plus_type(ts): if ts == 'Z3_context': return 'Z3_context_plus' @@ -1309,6 +1307,8 @@ def mk_z3native_stubs_c(ml_dir): # C interface needs_tmp_value = needs_tmp_value or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY if needs_tmp_value: c = c + 1 + if len(ap) > 0: + c = c + 1 ml_wrapper.write(' CAMLlocal%s(result, z3rv_val' % (c+2)) for p in params: if is_out_param(p) or is_array_param(p): @@ -1316,10 +1316,12 @@ def mk_z3native_stubs_c(ml_dir): # C interface i = i + 1 if needs_tmp_value: ml_wrapper.write(', tmp_val') + if len(ap) != 0: + ml_wrapper.write(', _iter'); ml_wrapper.write(');\n') - if len(ap) != 0: + if len(ap) > 0: ml_wrapper.write(' unsigned _i;\n') # declare locals, preprocess arrays, strings, in/out arguments @@ -1360,9 +1362,13 @@ def mk_z3native_stubs_c(ml_dir): # C interface if k == IN_ARRAY or k == INOUT_ARRAY: t = param_type(param) ts = type2str(t) + ml_wrapper.write(' _iter = a' + str(i) + ';\n') ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) {\n' % param_array_capacity_pos(param)) - ml_wrapper.write(' _a%s[_i] = %s;\n' % (i, ml_unwrap(t, ts, 'Field(a' + str(i) + ', _i)'))) + ml_wrapper.write(' assert(iter != Val_emptylist);\n') + ml_wrapper.write(' _a%s[_i] = %s;\n' % (i, ml_unwrap(t, ts, 'Field(_iter, 0)'))) + ml_wrapper.write(' _iter = Field(_iter, 1);\n') ml_wrapper.write(' }\n') + ml_wrapper.write(' assert(iter == Val_emptylist);\n\n') i = i + 1 ml_wrapper.write('\n /* invoke Z3 function */\n ') @@ -1421,8 +1427,9 @@ def mk_z3native_stubs_c(ml_dir): # C interface pt = param_type(p) ts = type2str(pt) if param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY: - ml_wrapper.write(' _a%s_val = caml_alloc(_a%s, 0);\n' % (i, param_array_capacity_pos(p))) - ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) {\n' % param_array_capacity_pos(p)) + # convert a C-array into an OCaml list and return it + ml_wrapper.write('\n _a%s_val = Val_emptylist;\n' % i) + ml_wrapper.write(' for (_i = _a%s; _i > 0; _i--) {\n' % param_array_capacity_pos(p)) pts = ml_plus_type(ts) pops = ml_plus_ops_type(ts) if ml_has_plus_type(ts): @@ -1430,8 +1437,11 @@ def mk_z3native_stubs_c(ml_dir): # C interface ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, 'tmp_val', '_a%dp' % i)) else: ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, 'tmp_val', '_a%d[_i]' % i)) - ml_wrapper.write(' Store_field(_a%s_val, _i, tmp_val);\n' % i) - ml_wrapper.write(' }\n') + ml_wrapper.write(' _iter = caml_alloc(2,0);\n') + ml_wrapper.write(' Store_field(_iter, 0, tmp_val);\n') + ml_wrapper.write(' Store_field(_iter, 1, _a%s_val);\n' % i) + ml_wrapper.write(' _a%s_val = _iter;\n' % i) + ml_wrapper.write(' }\n\n') elif param_kind(p) == OUT_MANAGED_ARRAY: wrp = ml_set_wrap(pt, '_a%d_val' % i, '_a%d' % i) wrp = wrp.replace('*)', '**)') diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 3a797e5d8..bbbb9e74b 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -323,24 +323,22 @@ end = struct end let mk_func_decl (ctx:context) (name:Symbol.symbol) (domain:Sort.sort list) (range:Sort.sort) = - let dom_arr = Array.of_list domain in - Z3native.mk_func_decl ctx name (Array.length dom_arr) dom_arr range + Z3native.mk_func_decl ctx name (List.length domain) domain range let mk_func_decl_s (ctx:context) (name:string) (domain:Sort.sort list) (range:Sort.sort) = mk_func_decl ctx (Symbol.mk_string ctx name) domain range let mk_fresh_func_decl (ctx:context) (prefix:string) (domain:Sort.sort list) (range:Sort.sort) = - let dom_arr = Array.of_list domain in - Z3native.mk_fresh_func_decl ctx prefix (Array.length dom_arr) dom_arr range + Z3native.mk_fresh_func_decl ctx prefix (List.length domain) domain range let mk_const_decl (ctx:context) (name:Symbol.symbol) (range:Sort.sort) = - Z3native.mk_func_decl ctx name 0 [||] range + Z3native.mk_func_decl ctx name 0 [] range let mk_const_decl_s (ctx:context) (name:string) (range:Sort.sort) = - Z3native.mk_func_decl ctx (Symbol.mk_string ctx name) 0 [||] range + Z3native.mk_func_decl ctx (Symbol.mk_string ctx name) 0 [] range let mk_fresh_const_decl (ctx:context) (prefix:string) (range:Sort.sort) = - Z3native.mk_fresh_func_decl ctx prefix 0 [||] range + Z3native.mk_fresh_func_decl ctx prefix 0 [] range let equal a b = (a = b) || (gc a = gc b && Z3native.is_eq_func_decl (gc a) a b) @@ -477,8 +475,7 @@ end = struct let ast_of_expr e = e let expr_of_func_app ctx f args = - let arg_array = Array.of_list args in - Z3native.mk_app ctx f (Array.length arg_array) arg_array + Z3native.mk_app ctx f (List.length args) args let simplify (x:expr) (p:Params.params option) = match p with @@ -498,20 +495,18 @@ end = struct if AST.is_app x && List.length args <> get_num_args x then raise (Error "Number of arguments does not match") else - Z3native.update_term (gc x) x (List.length args) (Array.of_list args) + Z3native.update_term (gc x) x (List.length args) args let substitute (x:expr) (from:expr list) (to_:expr list) = - let from_array = Array.of_list from in - let to_array = Array.of_list to_ in - if Array.length from_array <> Array.length to_array then + let len = List.length from in + if List.length to_ <> len then raise (Error "Argument sizes do not match") else - Z3native.substitute (gc x) x (Array.length from_array) from_array to_array + Z3native.substitute (gc x) x len from to_ let substitute_one x from to_ = substitute x [ from ] [ to_ ] let substitute_vars x to_ = - let to_array = Array.of_list to_ in - Z3native.substitute_vars (gc x) x (Array.length to_array) to_array + Z3native.substitute_vars (gc x) x (List.length to_) to_ let translate (x:expr) to_ctx = if gc x = to_ctx then @@ -556,18 +551,12 @@ struct let mk_implies = Z3native.mk_implies let mk_xor = Z3native.mk_xor - let mk_and ctx args = - let arg_arr = Array.of_list args in - Z3native.mk_and ctx (Array.length arg_arr) arg_arr + let mk_and ctx args = Z3native.mk_and ctx (List.length args) args - let mk_or ctx args = - let arg_arr = Array.of_list args in - Z3native.mk_or ctx (Array.length arg_arr) arg_arr + let mk_or ctx args = Z3native.mk_or ctx (List.length args) args let mk_eq = Z3native.mk_eq - let mk_distinct ctx args = - let arg_arr = Array.of_list args in - Z3native.mk_distinct ctx (Array.length arg_arr) arg_arr + let mk_distinct ctx args = Z3native.mk_distinct ctx (List.length args) args let get_bool_value x = lbool_of_int (Z3native.get_bool_value (gc x) x) @@ -656,56 +645,50 @@ struct let mk_bound = Z3native.mk_bound let mk_pattern ctx terms = - let terms_arr = Array.of_list terms in - if Array.length terms_arr = 0 then + let len = List.length terms in + if len = 0 then raise (Error "Cannot create a pattern from zero terms") else - Z3native.mk_pattern ctx (Array.length terms_arr) terms_arr + Z3native.mk_pattern ctx len terms let _internal_mk_quantifier ~universal ctx sorts names body weight patterns nopatterns quantifier_id skolem_id = - let sorts_arr = Array.of_list sorts in - let names_arr = Array.of_list names in - if Array.length sorts_arr <> Array.length names_arr then + let len = List.length sorts in + if List.length names <> len then raise (Error "Number of sorts does not match number of names") else - let patterns_arr = Array.of_list patterns in match nopatterns, quantifier_id, skolem_id with | [], None, None -> Z3native.mk_quantifier ctx universal (match weight with | None -> 1 | Some x -> x) - (Array.length patterns_arr) patterns_arr - (Array.length sorts_arr) sorts_arr - names_arr body + (List.length patterns) patterns + len sorts + names body | _ -> - let nopatterns_arr = Array.of_list nopatterns in Z3native.mk_quantifier_ex ctx universal (match weight with | None -> 1 | Some x -> x) (match quantifier_id with | None -> Z3native.mk_null_symbol ctx | Some x -> x) (match skolem_id with | None -> Z3native.mk_null_symbol ctx | Some x -> x) - (Array.length patterns_arr) patterns_arr - (Array.length nopatterns_arr) nopatterns_arr - (Array.length sorts_arr) sorts_arr - names_arr body + (List.length patterns) patterns + (List.length nopatterns) nopatterns + len sorts + names body let _internal_mk_quantifier_const ~universal ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id = - let patterns_arr = Array.of_list patterns in - let bound_constants_arr = Array.of_list bound_constants in match nopatterns, quantifier_id, skolem_id with | [], None, None -> Z3native.mk_quantifier_const ctx universal (match weight with | None -> 1 | Some x -> x) - (Array.length bound_constants_arr) bound_constants_arr - (Array.length patterns_arr) patterns_arr + (List.length bound_constants) bound_constants + (List.length patterns) patterns body | _ -> - let nopatterns_arr = Array.of_list nopatterns in Z3native.mk_quantifier_const_ex ctx universal (match weight with | None -> 1 | Some x -> x) (match quantifier_id with | None -> Z3native.mk_null_symbol ctx | Some x -> x) (match skolem_id with | None -> Z3native.mk_null_symbol ctx | Some x -> x) - (Array.length bound_constants_arr) bound_constants_arr - (Array.length patterns_arr) patterns_arr - (Array.length nopatterns_arr) nopatterns_arr + (List.length bound_constants) bound_constants + (List.length patterns) patterns + (List.length nopatterns) nopatterns body let mk_forall = _internal_mk_quantifier ~universal:true @@ -754,8 +737,7 @@ struct let mk_const_array = Z3native.mk_const_array let mk_map ctx f args = - let args_arr = Array.of_list args in - Z3native.mk_map ctx f (Array.length args_arr) args_arr + Z3native.mk_map ctx f (List.length args) args let mk_term_array = Z3native.mk_array_default let mk_array_ext = Z3native.mk_array_ext @@ -777,12 +759,10 @@ struct let mk_set_add = Z3native.mk_set_add let mk_del = Z3native.mk_set_del let mk_union ctx args = - let args_arr = Array.of_list args in - Z3native.mk_set_union ctx (Array.length args_arr) args_arr + Z3native.mk_set_union ctx (List.length args) args let mk_intersection ctx args = - let args_arr = Array.of_list args in - Z3native.mk_set_intersect ctx (Array.length args_arr) args_arr + Z3native.mk_set_intersect ctx (List.length args) args let mk_difference = Z3native.mk_set_difference let mk_complement = Z3native.mk_set_complement @@ -855,20 +835,20 @@ struct let _field_nums = FieldNumTable.create 0 let create (ctx:context) (name:Symbol.symbol) (recognizer:Symbol.symbol) (field_names:Symbol.symbol list) (sorts:Sort.sort option list) (sort_refs:int list) = - let n = (List.length field_names) in - if n <> (List.length sorts) then + let n = List.length field_names in + if n <> List.length sorts then raise (Error "Number of field names does not match number of sorts") else - if n <> (List.length sort_refs) then + if n <> List.length sort_refs then raise (Error "Number of field names does not match number of sort refs") else let no = Z3native.mk_constructor ctx name recognizer n - (Array.of_list field_names) + field_names (let f x = match x with None -> Z3native.mk_null_ast ctx | Some s -> s in - Array.of_list (List.map f sorts)) - (Array.of_list sort_refs) in + List.map f sorts) + sort_refs in FieldNumTable.add _field_nums no n; no @@ -884,8 +864,7 @@ struct let get_accessor_decls (x:constructor) = let (_, _, c) = (Z3native.query_constructor (gc x) x (get_num_fields x)) in - let f i = Array.get c i in - mk_list f (Array.length c) + c end module ConstructorList = @@ -893,7 +872,7 @@ struct type constructor_list = Z3native.constructor_list let create (ctx:context) (c:Constructor.constructor list) = - Z3native.mk_constructor_list ctx (List.length c) (Array.of_list c) + Z3native.mk_constructor_list ctx (List.length c) c end let mk_constructor (ctx:context) (name:Symbol.symbol) (recognizer:Symbol.symbol) (field_names:Symbol.symbol list) (sorts:Sort.sort option list) (sort_refs:int list) = @@ -903,7 +882,7 @@ struct mk_constructor ctx (Symbol.mk_string ctx name) recognizer field_names sorts sort_refs let mk_sort (ctx:context) (name:Symbol.symbol) (constructors:Constructor.constructor list) = - let (x,_) = (Z3native.mk_datatype ctx name (List.length constructors) (Array.of_list constructors)) in + let (x,_) = Z3native.mk_datatype ctx name (List.length constructors) constructors in x let mk_sort_s (ctx:context) (name:string) (constructors:Constructor.constructor list) = @@ -912,10 +891,9 @@ struct let mk_sorts (ctx:context) (names:Symbol.symbol list) (c:Constructor.constructor list list) = let n = List.length names in let f e = ConstructorList.create ctx e in - let cla = Array.of_list (List.map f c) in - let (r, a) = Z3native.mk_datatypes ctx n (Array.of_list names) cla in - let g i = Array.get r i in - mk_list g (Array.length r) + let cla = List.map f c in + let (r, _) = Z3native.mk_datatypes ctx n names cla in + r let mk_sorts_s (ctx:context) (names:string list) (c:Constructor.constructor list list) = mk_sorts ctx (List.map (fun x -> Symbol.mk_string ctx x) names) c @@ -946,7 +924,7 @@ end module Enumeration = struct let mk_sort (ctx:context) (name:Symbol.symbol) (enum_names:Symbol.symbol list) = - let (a, _, _) = (Z3native.mk_enumeration_sort ctx name (List.length enum_names) (Array.of_list enum_names)) in + let (a, _, _) = Z3native.mk_enumeration_sort ctx name (List.length enum_names) enum_names in a let mk_sort_s (ctx:context) (name:string) (enum_names:string list) = @@ -995,7 +973,7 @@ end module Tuple = struct let mk_sort (ctx:context) (name:Symbol.symbol) (field_names:Symbol.symbol list) (field_sorts:Sort.sort list) = - let (r, _, _) = (Z3native.mk_tuple_sort ctx name (List.length field_names) (Array.of_list field_names) (Array.of_list field_sorts)) in + let (r, _, _) = Z3native.mk_tuple_sort ctx name (List.length field_names) field_names field_sorts in r let get_mk_decl (x:Sort.sort) = Z3native.get_tuple_sort_mk_decl (Sort.gc x) x @@ -1099,16 +1077,13 @@ struct end let mk_add (ctx:context) (t:expr list) = - let t_arr = Array.of_list t in - Z3native.mk_add ctx (Array.length t_arr) t_arr + Z3native.mk_add ctx (List.length t) t let mk_mul (ctx:context) (t:expr list) = - let t_arr = Array.of_list t in - Z3native.mk_mul ctx (Array.length t_arr) t_arr + Z3native.mk_mul ctx (List.length t) t let mk_sub (ctx:context) (t:expr list) = - let t_arr = Array.of_list t in - Z3native.mk_sub ctx (Array.length t_arr) t_arr + Z3native.mk_sub ctx (List.length t) t let mk_unary_minus = Z3native.mk_unary_minus let mk_div = Z3native.mk_div @@ -1674,7 +1649,7 @@ struct let fail_if_not_decided = Z3native.tactic_fail_if_not_decided let using_params = Z3native.tactic_using_params let with_ = using_params - let par_or (ctx:context) (t:tactic list) = Z3native.tactic_par_or ctx (List.length t) (Array.of_list t) + let par_or (ctx:context) (t:tactic list) = Z3native.tactic_par_or ctx (List.length t) t let par_and_then = Z3native.tactic_par_and_then let interrupt = Z3native.interrupt end @@ -1781,8 +1756,7 @@ struct match assumptions with | [] -> Z3native.solver_check (gc x) x | _::_ -> - let assumption_array = Array.of_list assumptions in - Z3native.solver_check_assumptions (gc x) x (Array.length assumption_array) assumption_array + Z3native.solver_check_assumptions (gc x) x (List.length assumptions) assumptions in match lbool_of_int result with | L_TRUE -> SATISFIABLE @@ -1837,7 +1811,7 @@ struct | Some y -> Z3native.fixedpoint_add_rule (gc x) x rule y let add_fact (x:fixedpoint) (pred:func_decl) (args:int list) = - Z3native.fixedpoint_add_fact (gc x) x pred (List.length args) (Array.of_list args) + Z3native.fixedpoint_add_fact (gc x) x pred (List.length args) args let query (x:fixedpoint) (query:expr) = match lbool_of_int (Z3native.fixedpoint_query (gc x) x query) with @@ -1846,7 +1820,7 @@ struct | _ -> Solver.UNKNOWN let query_r (x:fixedpoint) (relations:func_decl list) = - match lbool_of_int (Z3native.fixedpoint_query_relations (gc x) x (List.length relations) (Array.of_list relations)) with + match lbool_of_int (Z3native.fixedpoint_query_relations (gc x) x (List.length relations) relations) with | L_TRUE -> Solver.SATISFIABLE | L_FALSE -> Solver.UNSATISFIABLE | _ -> Solver.UNKNOWN @@ -1869,13 +1843,13 @@ struct let add_cover (x:fixedpoint) (level:int) (predicate:func_decl) (property:expr) = Z3native.fixedpoint_add_cover (gc x) x level predicate property - let to_string (x:fixedpoint) = Z3native.fixedpoint_to_string (gc x) x 0 [||] + let to_string (x:fixedpoint) = Z3native.fixedpoint_to_string (gc x) x 0 [] let set_predicate_representation (x:fixedpoint) (f:func_decl) (kinds:Symbol.symbol list) = - Z3native.fixedpoint_set_predicate_representation (gc x) x f (List.length kinds) (Array.of_list kinds) + Z3native.fixedpoint_set_predicate_representation (gc x) x f (List.length kinds) kinds let to_string_q (x:fixedpoint) (queries:expr list) = - Z3native.fixedpoint_to_string (gc x) x (List.length queries) (Array.of_list queries) + Z3native.fixedpoint_to_string (gc x) x (List.length queries) queries let get_rules (x:fixedpoint) = let av = Z3native.fixedpoint_get_rules (gc x) x in @@ -1944,24 +1918,19 @@ module SMT = struct let benchmark_to_smtstring (ctx:context) (name:string) (logic:string) (status:string) (attributes:string) (assumptions:expr list) (formula:expr) = Z3native.benchmark_to_smtlib_string ctx name logic status attributes - (List.length assumptions) (Array.of_list assumptions) + (List.length assumptions) assumptions formula let parse_smtlib_string (ctx:context) (str:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) = - let csn = (List.length sort_names) in - let cs = (List.length sorts) in - let cdn = (List.length decl_names) in - let cd = (List.length decls) in + let csn = List.length sort_names in + let cs = List.length sorts in + let cdn = List.length decl_names in + let cd = List.length decls in if (csn <> cs || cdn <> cd) then raise (Error "Argument size mismatch") else Z3native.parse_smtlib_string ctx str - cs - (Array.of_list sort_names) - (Array.of_list sorts) - cd - (Array.of_list decl_names) - (Array.of_list decls) + cs sort_names sorts cd decl_names decls let parse_smtlib_file (ctx:context) (file_name:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) = let csn = (List.length sort_names) in @@ -1972,12 +1941,7 @@ struct raise (Error "Argument size mismatch") else Z3native.parse_smtlib_file ctx file_name - cs - (Array.of_list sort_names) - (Array.of_list sorts) - cd - (Array.of_list decl_names) - (Array.of_list decls) + cs sort_names sorts cd decl_names decls let get_num_smtlib_formulas (ctx:context) = Z3native.get_smtlib_num_formulas ctx @@ -2008,34 +1972,26 @@ struct mk_list f n let parse_smtlib2_string (ctx:context) (str:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) = - let sort_names_arr = Array.of_list sort_names in - let sorts_arr = Array.of_list sorts in - let decl_names_arr = Array.of_list decl_names in - let decls_arr = Array.of_list decls in - let csn = Array.length sort_names_arr in - let cs = Array.length sorts_arr in - let cdn = Array.length decl_names_arr in - let cd = Array.length decls_arr in + let csn = List.length sort_names in + let cs = List.length sorts in + let cdn = List.length decl_names in + let cd = List.length decls in if csn <> cs || cdn <> cd then raise (Error "Argument size mismatch") else Z3native.parse_smtlib2_string ctx str - cs sort_names_arr sorts_arr cd decl_names_arr decls_arr + cs sort_names sorts cd decl_names decls let parse_smtlib2_file (ctx:context) (file_name:string) (sort_names:Symbol.symbol list) (sorts:Sort.sort list) (decl_names:Symbol.symbol list) (decls:func_decl list) = - let sort_names_arr = Array.of_list sort_names in - let sorts_arr = Array.of_list sorts in - let decl_names_arr = Array.of_list decl_names in - let decls_arr = Array.of_list decls in - let csn = Array.length sort_names_arr in - let cs = Array.length sorts_arr in - let cdn = Array.length decl_names_arr in - let cd = Array.length decls_arr in + let csn = List.length sort_names in + let cs = List.length sorts in + let cdn = List.length decl_names in + let cd = List.length decls in if csn <> cs || cdn <> cd then raise (Error "Argument size mismatch") else Z3native.parse_smtlib2_string ctx file_name - cs sort_names_arr sorts_arr cd decl_names_arr decls_arr + cs sort_names sorts cd decl_names decls end module Interpolation = @@ -2072,29 +2028,17 @@ struct in match r with | 0 -> raise (Error "Interpolation problem could not be read.") - | _ -> - let f1 i = Array.get cnsts i in - let f2 i = Array.get parents i in - let f3 i = Array.get theory i in - (mk_list f1 num, - mk_list f2 num, - mk_list f3 num_theory) + | _ -> (cnsts, parents, theory) let check_interpolant (ctx:context) (num:int) (cnsts:Expr.expr list) (parents:int list) (interps:Expr.expr list) (num_theory:int) (theory:Expr.expr list) = - let (r, str) = Z3native.check_interpolant ctx - num - (Array.of_list cnsts) - (Array.of_list parents) - (Array.of_list interps) - num_theory - (Array.of_list theory) in + let (r, str) = Z3native.check_interpolant ctx num cnsts parents interps num_theory theory in match (lbool_of_int r) with | L_UNDEF -> raise (Error "Interpolant could not be verified.") | L_FALSE -> raise (Error "Interpolant could not be verified.") | _ -> () let write_interpolation_problem (ctx:context) (num:int) (cnsts:Expr.expr list) (parents:int list) (filename:string) (num_theory:int) (theory:Expr.expr list) = - Z3native.write_interpolation_problem ctx num (Array.of_list cnsts) (Array.of_list parents) filename num_theory (Array.of_list theory) + Z3native.write_interpolation_problem ctx num cnsts parents filename num_theory theory end let set_global_param = Z3native.global_param_set