From f133f478c81d21124bce8214fae66caffb01d80a Mon Sep 17 00:00:00 2001 From: martin-neuhaeusser Date: Mon, 4 Apr 2016 17:16:15 +0200 Subject: [PATCH] Translate correctly between OCaml option values and NULL pointers This patch refactors the update_api script and the z3.ml implementation to properly translate between OCaml options and NULL pointers. Some unifications and simplifications (avoidance of unnecessary value allocation) in the script that creates the native bindings. --- scripts/update_api.py | 78 ++-- src/api/ml/z3.ml | 674 ++++++++++++++++---------------- src/api/ml/z3native.ml.pre | 70 ---- src/api/ml/z3native_stubs.c.pre | 104 +++-- 4 files changed, 451 insertions(+), 475 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index cd6895544..f1a06a63d 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -95,7 +95,7 @@ next_type_id = FIRST_OBJ_ID def def_Type(var, c_type, py_type): global next_type_id exec('%s = %s' % (var, next_type_id), globals()) - Type2Str[next_type_id] = c_type + Type2Str[next_type_id] = c_type Type2PyStr[next_type_id] = py_type next_type_id = next_type_id + 1 @@ -1094,6 +1094,8 @@ def ml_plus_type(ts): def ml_minus_type(ts): if ts == 'Z3_ast' or ts == 'Z3_sort' or ts == 'Z3_func_decl' or ts == 'Z3_app' or ts == 'Z3_pattern': return 'Z3_ast' + if ts == 'Z3_ast_plus' or ts == 'Z3_sort_plus' or ts == 'Z3_func_decl_plus' or ts == 'Z3_app_plus' or ts == 'Z3_pattern_plus': + return 'Z3_ast' elif ts == 'Z3_constructor_plus': return 'Z3_constructor' elif ts == 'Z3_constructor_list_plus': @@ -1151,7 +1153,7 @@ def ml_has_plus_type(ts): def ml_unwrap(t, ts, s): if t == STRING: return '(' + ts + ') String_val(' + s + ')' - elif t == BOOL: + elif t == BOOL or (type2str(t) == 'Z3_bool'): return '(' + ts + ') Bool_val(' + s + ')' elif t == INT or t == PRINT_MODE or t == ERROR_CODE: return '(' + ts + ') Int_val(' + s + ')' @@ -1172,7 +1174,7 @@ def ml_unwrap(t, ts, s): def ml_set_wrap(t, d, n): if t == VOID: return d + ' = Val_unit;' - elif t == BOOL: + elif t == BOOL or (type2str(t) == 'Z3_bool'): return d + ' = Val_bool(' + n + ');' elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE: return d + ' = Val_int(' + n + ');' @@ -1186,6 +1188,15 @@ def ml_set_wrap(t, d, n): pts = ml_plus_type(type2str(t)) return '*(' + pts + '*)Data_custom_val(' + d + ') = ' + n + ';' +def ml_alloc_and_store(t, lhs, rhs): + if t == VOID or t == BOOL or t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE or t == INT64 or t == UINT64 or t == DOUBLE or t == STRING or (type2str(t) == 'Z3_bool'): + return ml_set_wrap(t, lhs, rhs) + else: + pts = ml_plus_type(type2str(t)) + pops = ml_plus_ops_type(type2str(t)) + alloc_str = '%s = caml_alloc_custom(&%s, sizeof(%s), 0, 1); ' % (lhs, pops, pts) + return alloc_str + ml_set_wrap(t, lhs, rhs) + def mk_ml(ml_dir): global Type2Str ml_nativef = os.path.join(ml_dir, 'z3native.ml') @@ -1258,6 +1269,18 @@ def mk_ml(ml_dir): ml_native.write(' a%d' % i) i = i + 1 ml_native.write('\n') + + ml_native.write('\n') + + # null pointer helpers + for type_id in Type2Str: + type_name = Type2Str[type_id] + if ml_has_plus_type(type_name) and not type_name in ['Z3_context', 'Z3_sort', 'Z3_func_decl', 'Z3_app', 'Z3_pattern']: + ml_name = type2ml(type_id) + ml_native.write(' external context_of_%s : %s -> context = "n_context_of_%s"\n' % (ml_name, ml_name, ml_name)) + ml_native.write(' external is_null_%s : %s -> bool = "n_is_null_%s"\n' % (ml_name, ml_name, ml_name)) + ml_native.write(' external mk_null_%s : context -> %s = "n_mk_null_%s"\n\n' % (ml_name, ml_name, ml_name)) + ml_native.write('(**/**)\n') ml_native.close() @@ -1266,7 +1289,6 @@ def mk_ml(ml_dir): mk_z3native_stubs_c(ml_dir) - def mk_z3native_stubs_c(ml_dir): # C interface ml_wrapperf = os.path.join(ml_dir, 'z3native_stubs.c') ml_wrapper = open(ml_wrapperf, 'w') @@ -1315,14 +1337,21 @@ def mk_z3native_stubs_c(ml_dir): # C interface ml_wrapper.write(' CAMLlocal1(result);\n') else: c = 0 + needs_tmp_value = False for p in params: if is_out_param(p) or is_array_param(p): c = c + 1 + 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 ml_wrapper.write(' CAMLlocal%s(result, z3rv_val' % (c+2)) for p in params: if is_out_param(p) or is_array_param(p): ml_wrapper.write(', _a%s_val' % i) i = i + 1 + if needs_tmp_value: + ml_wrapper.write(', tmp_val') + ml_wrapper.write(');\n') if len(ap) != 0: @@ -1371,20 +1400,14 @@ def mk_z3native_stubs_c(ml_dir): # C interface ml_wrapper.write(' }\n') i = i + 1 - ml_wrapper.write(' ') + ml_wrapper.write('\n /* invoke Z3 function */\n ') if result != VOID: ts = type2str(result) if ml_has_plus_type(ts): ml_wrapper.write('%s z3rv_m = ' % ts) - elif (result == BOOL or result == INT or result == UINT or result == PRINT_MODE or result == ERROR_CODE or result ==INT64 or result == UINT64 or result == DOUBLE or result == STRING): - ml_wrapper.write('%s z3rv = ' % ts) else: - ml_wrapper.write('result = caml_alloc_custom(&default_custom_ops, sizeof(%s), 0, 1);\n ' % ts) ml_wrapper.write('%s z3rv = ' % ts) - elif len(op) != 0: - ml_wrapper.write('result = caml_alloc(%s, 0);\n ' % ret_size) - # invoke procedure ml_wrapper.write('%s(' % name) i = 0 @@ -1413,7 +1436,6 @@ def mk_z3native_stubs_c(ml_dir): # C interface ts = type2str(result) if ml_has_plus_type(ts): pts = ml_plus_type(ts) - ml_wrapper.write(' result = caml_alloc_custom(&%s, sizeof(%s), 0, 1);\n' % (ml_plus_ops_type(ts), pts)) if name in NULLWrapped: ml_wrapper.write(' %s z3rv = %s_mk(z3rv_m);\n' % (pts, pts)) else: @@ -1421,6 +1443,14 @@ def mk_z3native_stubs_c(ml_dir): # C interface # convert output params if len(op) > 0: + # we have output parameters (i.e. call-by-reference arguments to the Z3 native + # code function). Hence, the value returned by the OCaml native wrapper is a tuple + # which contains the Z3 native function's return value (if it is non-void) in its + # first and the output parameters in the following components. + + ml_wrapper.write('\n /* construct return tuple */\n') + ml_wrapper.write(' result = caml_alloc(%s, 0);\n' % ret_size) + i = 0 for p in params: pt = param_type(p) @@ -1430,14 +1460,12 @@ def mk_z3native_stubs_c(ml_dir): # C interface ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) {\n' % param_array_capacity_pos(p)) pts = ml_plus_type(ts) pops = ml_plus_ops_type(ts) - ml_wrapper.write(' value t;\n') - ml_wrapper.write(' t = caml_alloc_custom(&%s, sizeof(%s), 0, 1);\n' % (pops, pts)) if ml_has_plus_type(ts): ml_wrapper.write(' %s _a%dp = %s_mk(ctx_p, (%s) _a%d[_i]);\n' % (pts, i, pts, ml_minus_type(ts), i)) - ml_wrapper.write(' %s\n' % ml_set_wrap(pt, 't', '_a%dp' % i)) + ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, 'tmp_val', '_a%dp' % i)) else: - ml_wrapper.write(' %s\n' % ml_set_wrap(pt, 't', '_a%d[_i]' % i)) - ml_wrapper.write(' Store_field(_a%s_val, _i, t);\n' % i) + 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') elif param_kind(p) == OUT_MANAGED_ARRAY: wrp = ml_set_wrap(pt, '_a%d_val' % i, '_a%d' % i) @@ -1448,18 +1476,15 @@ def mk_z3native_stubs_c(ml_dir): # C interface if ml_has_plus_type(ts): pts = ml_plus_type(ts) ml_wrapper.write(' %s _a%dp = %s_mk(ctx_p, (%s) _a%d);\n' % (pts, i, pts, ml_minus_type(ts), i)) - ml_wrapper.write(' %s\n' % ml_set_wrap(pt, '_a%d_val' % i, '_a%dp' % i)) + ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, '_a%d_val' % i, '_a%dp' % i)) else: - ml_wrapper.write(' %s\n' % ml_set_wrap(pt, '_a%d_val' % i, '_a%d' % i)) + ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, '_a%d_val' % i, '_a%d' % i)) i = i + 1 - # return tuples - if len(op) == 0: - ml_wrapper.write(' %s\n' % ml_set_wrap(result, "result", "z3rv")) - else: + # return tuples i = j = 0 if result != VOID: - ml_wrapper.write(' %s\n' % ml_set_wrap(result, "z3rv_val", "z3rv")) + ml_wrapper.write(' %s' % ml_alloc_and_store(result, 'z3rv_val', 'z3rv')) ml_wrapper.write(' Store_field(result, 0, z3rv_val);\n') j = j + 1 for p in params: @@ -1467,8 +1492,13 @@ def mk_z3native_stubs_c(ml_dir): # C interface ml_wrapper.write(' Store_field(result, %s, _a%s_val);\n' % (j, i)) j = j + 1 i = i + 1 + else: + # As we have no output parameters, we simply return the result + ml_wrapper.write('\n /* construct simple return value */\n') + ml_wrapper.write(' %s' % ml_alloc_and_store(result, "result", "z3rv")) # local array cleanup + ml_wrapper.write('\n /* cleanup and return */\n') i = 0 for p in params: k = param_kind(p) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index a5beac6ec..e6e832572 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -10,13 +10,9 @@ open Z3enums exception Error of string let _ = Callback.register_exception "Z3EXCEPTION" (Error "") -(* Some helpers. *) -let null = Z3native.mk_null() -let is_null o = (Z3native.is_null o) - type context = Z3native.context -module Log = +module Log = struct let open_ filename = ((lbool_of_int (Z3native.open_log filename)) == L_TRUE) let close = Z3native.close_log @@ -30,7 +26,7 @@ struct let minor = let (_, x, _, _) = Z3native.get_version () in x let build = let (_, _, x, _) = Z3native.get_version () in x let revision = let (_, _, _, x) = Z3native.get_version () in x - let to_string = + let to_string = let (mj, mn, bld, rev) = Z3native.get_version () in string_of_int mj ^ "." ^ string_of_int mn ^ "." ^ @@ -41,7 +37,7 @@ end let mk_list (f:int -> 'a) (n:int) = let rec mk_list' (f:int -> 'a) (i:int) (n:int) (tail:'a list):'a list = - if (i >= n) then + if (i >= n) then tail else (f i) :: (mk_list' f (i+1) n tail) @@ -56,7 +52,7 @@ let mk_context (settings:(string * string) list) = Z3native.del_config(cfg) ; Z3native.set_ast_print_mode res (Z3enums.int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT) ; Z3native.set_internal_error_handler res ; - res + res @@ -64,8 +60,8 @@ module Symbol = struct type symbol = Z3native.symbol let gc (o:symbol) = (Z3native.context_of_symbol o) - - let kind (o:symbol) = (symbol_kind_of_int (Z3native.get_symbol_kind (gc o) o)) + + let kind (o:symbol) = (symbol_kind_of_int (Z3native.get_symbol_kind (gc o) o)) let is_int_symbol (o:symbol) = (kind o) == INT_SYMBOL let is_string_symbol (o:symbol) = (kind o) == STRING_SYMBOL let get_int (o:symbol) = (Z3native.get_symbol_int (gc o) o) @@ -75,7 +71,7 @@ struct | INT_SYMBOL -> (string_of_int (Z3native.get_symbol_int (gc o) o)) | STRING_SYMBOL -> (Z3native.get_symbol_string (gc o) o) - let mk_int (ctx:context) (i:int) = (Z3native.mk_int_symbol ctx i) + let mk_int (ctx:context) (i:int) = (Z3native.mk_int_symbol ctx i) let mk_string (ctx:context) (s:string) = (Z3native.mk_string_symbol ctx s) let mk_ints (ctx:context) (names:int list) = @@ -131,11 +127,11 @@ sig val equal : ast -> ast -> bool val compare : ast -> ast -> int val translate : ast -> context -> ast -end = struct +end = struct type ast = Z3native.ast let gc (x:ast) = Z3native.context_of_ast x - - module ASTVector = + + module ASTVector = struct type ast_vector = Z3native.ast_vector let gc (x:ast_vector) = Z3native.context_of_ast_vector x @@ -144,7 +140,7 @@ end = struct let get_size (x:ast_vector) = Z3native.ast_vector_size (gc x) x let get (x:ast_vector) (i:int) = Z3native.ast_vector_get (gc x) x i let set (x:ast_vector) (i:int) (value:ast) = Z3native.ast_vector_set (gc x) x i value - let resize (x:ast_vector) (new_size:int) = Z3native.ast_vector_resize (gc x) x new_size + let resize (x:ast_vector) (new_size:int) = Z3native.ast_vector_resize (gc x) x new_size let push (x:ast_vector) (a:ast) = Z3native.ast_vector_push (gc x) x a let translate (x:ast_vector) (to_ctx:context) = Z3native.ast_vector_translate (gc x) x to_ctx @@ -157,22 +153,22 @@ end = struct let xs = (get_size x) in let f i = get x i in mk_list f xs - + let to_string (x:ast_vector) = Z3native.ast_vector_to_string (gc x) x end module ASTMap = - struct + struct type ast_map = Z3native.ast_map let gc (x:ast_map) = Z3native.context_of_ast_map x - + let mk_ast_map (ctx:context) = Z3native.mk_ast_map ctx let contains (x:ast_map) (key:ast) = Z3native.ast_map_contains (gc x) x key - let find (x:ast_map) (key:ast) = Z3native.ast_map_find (gc x) x key + let find (x:ast_map) (key:ast) = Z3native.ast_map_find (gc x) x key let insert (x:ast_map) (key:ast) (value:ast) = Z3native.ast_map_insert (gc x) x key value - let erase (x:ast_map) (key:ast) = Z3native.ast_map_erase (gc x) x key + let erase (x:ast_map) (key:ast) = Z3native.ast_map_erase (gc x) x key let reset (x:ast_map) = Z3native.ast_map_reset (gc x) x - let get_size (x:ast_map) = Z3native.ast_map_size (gc x) x + let get_size (x:ast_map) = Z3native.ast_map_size (gc x) x let get_keys (x:ast_map) = let av = (Z3native.ast_map_keys (gc x) x) in @@ -184,17 +180,17 @@ end = struct let hash (x:ast) = Z3native.get_ast_hash (gc x) x let get_id (x:ast) = Z3native.get_ast_id (gc x) x let get_ast_kind (x:ast) = (ast_kind_of_int (Z3native.get_ast_kind (gc x) x)) - - let is_expr (x:ast) = + + let is_expr (x:ast) = match get_ast_kind (x:ast) with | APP_AST - | NUMERAL_AST + | NUMERAL_AST | QUANTIFIER_AST | VAR_AST -> true | _ -> false - + let is_app (x:ast) = (get_ast_kind x) == APP_AST - let is_var (x:ast) = (get_ast_kind x) == VAR_AST + let is_var (x:ast) = (get_ast_kind x) == VAR_AST let is_quantifier (x:ast) = (get_ast_kind x) == QUANTIFIER_AST let is_sort (x:ast) = (get_ast_kind x) == SORT_AST let is_func_decl (x:ast) = (get_ast_kind x) == FUNC_DECL_AST @@ -204,19 +200,19 @@ end = struct let equal (a:ast) (b:ast) = - (a == b) || - (if (gc a) != (gc b) then - false - else + (a == b) || + (if (gc a) != (gc b) then + false + else Z3native.is_eq_ast (gc a) a b) - - let compare a b = + + let compare a b = if (get_id a) < (get_id b) then -1 else if (get_id a) > (get_id b) then 1 else 0 - + let translate (x:ast) (to_ctx:context) = - if (gc x) == to_ctx then + if (gc x) == to_ctx then x else Z3native.translate (gc x) x to_ctx @@ -236,24 +232,24 @@ sig end = struct type sort = Z3native.sort let gc (x:sort) = Z3native.context_of_ast x - + let equal:sort -> sort -> bool = fun a b -> (a == b) || - (if (gc a) != (gc b) then - false - else + (if (gc a) != (gc b) then + false + else Z3native.is_eq_sort (gc a) a b) - + let get_id (x:sort) = Z3native.get_sort_id (gc x) x let get_sort_kind (x:sort) = sort_kind_of_int (Z3native.get_sort_kind (gc x) x) let get_name (x:sort) = Z3native.get_sort_name (gc x) x let to_string (x:sort) = Z3native.sort_to_string (gc x) x let mk_uninterpreted (ctx:context) (s:Symbol.symbol) = Z3native.mk_uninterpreted_sort ctx s let mk_uninterpreted_s (ctx:context) (s:string) = mk_uninterpreted ctx (Symbol.mk_string ctx s) -end +end and FuncDecl : -sig +sig type func_decl = Z3native.func_decl val gc : func_decl -> context module Parameter : @@ -266,7 +262,7 @@ val gc : func_decl -> context | P_Ast of AST.ast | P_Fdl of func_decl | P_Rat of string - + val get_kind : parameter -> Z3enums.parameter_kind val get_int : parameter -> int val get_float : parameter -> float @@ -299,8 +295,8 @@ end = struct let gc (x:func_decl) = Z3native.context_of_ast x module Parameter = - struct - type parameter = + struct + type parameter = | P_Int of int | P_Dbl of float | P_Sym of Symbol.symbol @@ -308,7 +304,7 @@ end = struct | P_Ast of AST.ast | P_Fdl of func_decl | P_Rat of string - + let get_kind (x:parameter) = (match x with | P_Int(_) -> PARAMETER_INT @@ -318,22 +314,22 @@ end = struct | P_Ast(_) -> PARAMETER_AST | P_Fdl(_) -> PARAMETER_FUNC_DECL | P_Rat(_) -> PARAMETER_RATIONAL) - + let get_int (x:parameter) = match x with | P_Int(x) -> x | _ -> raise (Error "parameter is not an int") - - let get_float (x:parameter) = + + let get_float (x:parameter) = match x with | P_Dbl(x) -> x | _ -> raise (Error "parameter is not a float") - + let get_symbol (x:parameter) = match x with | P_Sym(x) -> x | _ -> raise (Error "parameter is not a symbol") - + let get_sort (x:parameter) = match x with | P_Srt(x) -> x @@ -375,25 +371,25 @@ end = struct let equal (a:func_decl) (b:func_decl) = (a == b) || - (if (gc a) != (gc b) then - false - else + (if (gc a) != (gc b) then + false + else Z3native.is_eq_func_decl (gc a) a b) - let to_string (x:func_decl) = Z3native.func_decl_to_string (gc x) x + let to_string (x:func_decl) = Z3native.func_decl_to_string (gc x) x let get_id (x:func_decl) = Z3native.get_func_decl_id (gc x) x let get_arity (x:func_decl) = Z3native.get_arity (gc x) x let get_domain_size (x:func_decl) = Z3native.get_domain_size (gc x) x - let get_domain (x:func_decl) = + let get_domain (x:func_decl) = let n = (get_domain_size x) in let f i = Z3native.get_domain (gc x) x i in mk_list f n - + let get_range (x:func_decl) = Z3native.get_range (gc x) x let get_decl_kind (x:func_decl) = decl_kind_of_int (Z3native.get_decl_kind (gc x) x) let get_name (x:func_decl) = Z3native.get_decl_name (gc x) x - let get_num_parameters (x:func_decl) = Z3native.get_decl_num_parameters (gc x) x + let get_num_parameters (x:func_decl) = Z3native.get_decl_num_parameters (gc x) x let get_parameters (x:func_decl) = let n = (get_num_parameters x) in @@ -407,7 +403,7 @@ end = struct | PARAMETER_RATIONAL -> Parameter.P_Rat (Z3native.get_decl_rational_parameter (gc x) x i)) in mk_list f n - let apply (x:func_decl) (args:Expr.expr list) = Expr.expr_of_func_app (gc x) x args + let apply (x:func_decl) (args:Expr.expr list) = Expr.expr_of_func_app (gc x) x args end @@ -429,28 +425,28 @@ sig val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit val mk_params : context -> params val to_string : params -> string - + val update_param_value : context -> string -> string -> unit val set_print_mode : context -> Z3enums.ast_print_mode -> unit end = struct type params = Z3native.params let gc (x:params) = Z3native.context_of_params x - module ParamDescrs = - struct + module ParamDescrs = + struct type param_descrs = Z3native.param_descrs let gc (x:param_descrs) = Z3native.context_of_param_descrs x let validate (x:param_descrs) (p:params) = Z3native.params_validate (gc x) p x let get_kind (x:param_descrs) (name:Symbol.symbol) = param_kind_of_int (Z3native.param_descrs_get_kind (gc x) x name) - + let get_names (x:param_descrs) = let n = Z3native.param_descrs_size (gc x) x in let f i = Z3native.param_descrs_get_name (gc x) x i in mk_list f n - let get_size (x:param_descrs) = Z3native.param_descrs_size (gc x) x - let to_string (x:param_descrs) = Z3native.param_descrs_to_string (gc x) x + let get_size (x:param_descrs) = Z3native.param_descrs_size (gc x) x + let to_string (x:param_descrs) = Z3native.param_descrs_to_string (gc x) x end let add_bool (x:params) (name:Symbol.symbol) (value:bool) = Z3native.params_set_bool (gc x) x name value @@ -497,60 +493,60 @@ sig val mk_numeral_int : context -> int -> Sort.sort -> expr val equal : expr -> expr -> bool val apply1 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr - val apply2 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr - val apply3 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr -> expr + val apply2 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr + val apply3 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr -> expr val apply4 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr -> expr -> expr val compare : expr -> expr -> int -end = struct - type expr = AST.ast +end = struct + type expr = AST.ast let gc (e:expr) = Z3native.context_of_ast e - - let expr_of_ast (a:AST.ast) : expr = + + let expr_of_ast (a:AST.ast) : expr = let q = Z3enums.ast_kind_of_int (Z3native.get_ast_kind (gc a) a) in if (q != Z3enums.APP_AST && q != VAR_AST && q != QUANTIFIER_AST && q != NUMERAL_AST) then raise (Error "Invalid coercion") else a - + let ast_of_expr (e:expr) : AST.ast = e - let expr_of_func_app:context -> FuncDecl.func_decl -> expr list -> expr = + let expr_of_func_app:context -> FuncDecl.func_decl -> expr list -> expr = fun ctx f args -> (Z3native.mk_app ctx f (List.length args) (Array.of_list args)) - + let apply1 ctx f t = f ctx t let apply2 ctx f t1 t2 = f ctx t1 t2 let apply3 ctx f t1 t2 t3 = f ctx t1 t2 t3 let apply4 ctx f t1 t2 t3 t4 = f ctx t1 t2 t3 t4 - let simplify (x:expr) (p:Params.params option) = - match p with + let simplify (x:expr) (p:Params.params option) = + match p with | None -> Z3native.simplify (gc x) x | Some pp -> Z3native.simplify_ex (gc x) x pp - + let get_simplify_help (ctx:context) = Z3native.simplify_get_help ctx let get_simplify_parameter_descrs (ctx:context) = Z3native.simplify_get_param_descrs ctx let get_func_decl (x:expr) = Z3native.get_app_decl (gc x) x - let get_num_args (x:expr) = Z3native.get_app_num_args (gc x) x - let get_args (x:expr) = + let get_num_args (x:expr) = Z3native.get_app_num_args (gc x) x + let get_args (x:expr) = let n = (get_num_args x) in let f i = Z3native.get_app_arg (gc x) x i in mk_list f n - + let update (x:expr) (args:expr list) = 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) - - let substitute (x:expr) (from:expr list) (to_:expr list) = + + let substitute (x:expr) (from:expr list) (to_:expr list) = if (List.length from) <> (List.length to_) then raise (Error "Argument sizes do not match") else Z3native.substitute (gc x) x (List.length from) (Array.of_list from) (Array.of_list to_) - + let substitute_one (x:expr) (from:expr) (to_:expr) = substitute (x:expr) [ from ] [ to_ ] let substitute_vars (x:expr) (to_:expr list) = Z3native.substitute_vars (gc x) x (List.length to_) (Array.of_list to_) - + let translate (x:expr) to_ctx = if (gc x) == to_ctx then x @@ -561,11 +557,11 @@ end = struct let is_numeral (x:expr) = Z3native.is_numeral_ast (gc x) x let is_well_sorted (x:expr) = Z3native.is_well_sorted (gc x) x let get_sort (x:expr) = Z3native.get_sort (gc x) x - let is_const (x:expr) = + let is_const (x:expr) = (AST.is_app x) && (get_num_args x) == 0 && (FuncDecl.get_domain_size (get_func_decl x)) == 0 - + let mk_const (ctx:context) (name:Symbol.symbol) (range:Sort.sort) = Z3native.mk_const ctx name range let mk_const_s (ctx:context) (name:string) (range:Sort.sort) = mk_const ctx (Symbol.mk_string ctx name) range let mk_const_f (ctx:context) (f:FuncDecl.func_decl) = expr_of_func_app ctx f [] @@ -580,16 +576,16 @@ end open FuncDecl open Expr -module Boolean = -struct +module Boolean = +struct let mk_sort (ctx:context) = Z3native.mk_bool_sort ctx - let mk_const (ctx:context) (name:Symbol.symbol) = Expr.mk_const ctx name (mk_sort ctx) + let mk_const (ctx:context) (name:Symbol.symbol) = Expr.mk_const ctx name (mk_sort ctx) let mk_const_s (ctx:context) (name:string) = mk_const ctx (Symbol.mk_string ctx name) let mk_true (ctx:context) = Z3native.mk_true ctx let mk_false (ctx:context) = Z3native.mk_false ctx - let mk_val (ctx:context) (value:bool) = if value then mk_true ctx else mk_false ctx - let mk_not (ctx:context) (a:expr) = apply1 ctx Z3native.mk_not a - let mk_ite (ctx:context) (t1:expr) (t2:expr) (t3:expr) = apply3 ctx Z3native.mk_ite t1 t2 t3 + let mk_val (ctx:context) (value:bool) = if value then mk_true ctx else mk_false ctx + let mk_not (ctx:context) (a:expr) = apply1 ctx Z3native.mk_not a + let mk_ite (ctx:context) (t1:expr) (t2:expr) (t3:expr) = apply3 ctx Z3native.mk_ite t1 t2 t3 let mk_iff (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_iff t1 t2 let mk_implies (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_implies t1 t2 let mk_xor (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_xor t1 t2 @@ -599,7 +595,7 @@ struct let mk_distinct (ctx:context) (args:expr list) = Z3native.mk_distinct ctx (List.length args) (Array.of_list args) let get_bool_value (x:expr) = lbool_of_int (Z3native.get_bool_value (gc x) x) - let is_bool (x:expr) = + let is_bool (x:expr) = (AST.is_expr x) && (Z3native.is_eq_sort (gc x) (Z3native.mk_bool_sort (gc x)) (Z3native.get_sort (gc x) x)) let is_true (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (get_func_decl x) == OP_TRUE) @@ -616,11 +612,11 @@ struct end -module Quantifier = -struct +module Quantifier = +struct type quantifier = AST.ast let gc (x:quantifier) = Z3native.context_of_ast x - + let expr_of_quantifier (q:quantifier) : Expr.expr = q let quantifier_of_expr (e:Expr.expr) : quantifier = @@ -630,8 +626,8 @@ struct else e - - module Pattern = + + module Pattern = struct type pattern = Z3native.pattern let gc (x:pattern) = Z3native.context_of_ast x @@ -646,40 +642,40 @@ struct let to_string (x:pattern) = Z3native.pattern_to_string (gc x) x end - let get_index (x:expr) = + let get_index (x:expr) = if not (AST.is_var x) then raise (Error "Term is not a bound variable.") else Z3native.get_index_value (gc x) x - let is_universal (x:quantifier) = Z3native.is_quantifier_forall (gc x) x + let is_universal (x:quantifier) = Z3native.is_quantifier_forall (gc x) x let is_existential (x:quantifier) = not (is_universal x) let get_weight (x:quantifier) = Z3native.get_quantifier_weight (gc x) x - let get_num_patterns (x:quantifier) = Z3native.get_quantifier_num_patterns (gc x) x + let get_num_patterns (x:quantifier) = Z3native.get_quantifier_num_patterns (gc x) x let get_patterns (x:quantifier) = let n = (get_num_patterns x) in let f i = Z3native.get_quantifier_pattern_ast (gc x) x i in mk_list f n - + let get_num_no_patterns (x:quantifier) = Z3native.get_quantifier_num_no_patterns (gc x) x - + let get_no_patterns (x:quantifier) = let n = (get_num_patterns x) in let f i = Z3native.get_quantifier_no_pattern_ast (gc x) x i in mk_list f n - + let get_num_bound (x:quantifier) = Z3native.get_quantifier_num_bound (gc x) x - + let get_bound_variable_names (x:quantifier) = let n = (get_num_bound x) in let f i = Z3native.get_quantifier_bound_name (gc x) x i in mk_list f n - + let get_bound_variable_sorts (x:quantifier) = let n = (get_num_bound x) in let f i = Z3native.get_quantifier_bound_sort (gc x) x i in mk_list f n - + let get_body (x:quantifier) = Z3native.get_quantifier_body (gc x) x let mk_bound (ctx:context) (index:int) (ty:Sort.sort) = Z3native.mk_bound ctx index ty @@ -693,7 +689,7 @@ struct if (List.length sorts) != (List.length names) then raise (Error "Number of sorts does not match number of names") else if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then - Z3native.mk_quantifier ctx true + Z3native.mk_quantifier ctx true (match weight with | None -> 1 | Some(x) -> x) (List.length patterns) (Array.of_list patterns) (List.length sorts) (Array.of_list sorts) @@ -702,14 +698,14 @@ struct else Z3native.mk_quantifier_ex ctx true (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> null | Some(x) -> x) - (match skolem_id with | None -> null | 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) (List.length patterns) (Array.of_list patterns) (List.length nopatterns) (Array.of_list nopatterns) (List.length sorts) (Array.of_list sorts) (Array.of_list names) body - + let mk_forall_const (ctx:context) (bound_constants:expr list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) = if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then Z3native.mk_quantifier_const ctx true @@ -720,8 +716,8 @@ struct else Z3native.mk_quantifier_const_ex ctx true (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> null | Some(x) -> x) - (match skolem_id with | None -> null | 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) (List.length bound_constants) (Array.of_list bound_constants) (List.length patterns) (Array.of_list patterns) (List.length nopatterns) (Array.of_list nopatterns) @@ -740,14 +736,14 @@ struct else Z3native.mk_quantifier_ex ctx false (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> null | Some(x) -> x) - (match skolem_id with | None -> null | 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) (List.length patterns) (Array.of_list patterns) (List.length nopatterns) (Array.of_list nopatterns) (List.length sorts) (Array.of_list sorts) (Array.of_list names) body - + let mk_exists_const (ctx:context) (bound_constants:expr list) (body:expr) (weight:int option) (patterns:Pattern.pattern list) (nopatterns:expr list) (quantifier_id:Symbol.symbol option) (skolem_id:Symbol.symbol option) = if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then Z3native.mk_quantifier_const ctx false @@ -758,8 +754,8 @@ struct else Z3native.mk_quantifier_const_ex ctx false (match weight with | None -> 1 | Some(x) -> x) - (match quantifier_id with | None -> null | Some(x) -> x) - (match skolem_id with | None -> null | 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) (List.length bound_constants) (Array.of_list bound_constants) (List.length patterns) (Array.of_list patterns) (List.length nopatterns) (Array.of_list nopatterns) @@ -776,12 +772,12 @@ else mk_forall_const ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id else mk_exists_const ctx bound_constants body weight patterns nopatterns quantifier_id skolem_id - + let to_string (x:quantifier) = Expr.to_string x end -module Z3Array = +module Z3Array = struct let mk_sort (ctx:context) (domain:Sort.sort) (range:Sort.sort) = Z3native.mk_array_sort ctx domain range let is_store (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_STORE) @@ -789,7 +785,7 @@ struct let is_constant_array (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CONST_ARRAY) let is_default_array (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ARRAY_DEFAULT) let is_array_map (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ARRAY_MAP) - let is_as_array (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_AS_ARRAY) + let is_as_array (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_AS_ARRAY) let is_array (x:expr) = (Z3native.is_app (Expr.gc x) x) && @@ -798,12 +794,12 @@ struct let get_domain (x:Sort.sort) = Z3native.get_array_sort_domain (Sort.gc x) x let get_range (x:Sort.sort) = Z3native.get_array_sort_range (Sort.gc x) x - let mk_const (ctx:context) (name:Symbol.symbol) (domain:Sort.sort) (range:Sort.sort) = + let mk_const (ctx:context) (name:Symbol.symbol) (domain:Sort.sort) (range:Sort.sort) = Expr.mk_const ctx name (mk_sort ctx domain range) - - let mk_const_s (ctx:context) (name:string) (domain:Sort.sort) (range:Sort.sort) = + + let mk_const_s (ctx:context) (name:string) (domain:Sort.sort) (range:Sort.sort) = mk_const ctx (Symbol.mk_string ctx name) domain range - + let mk_select (ctx:context) (a:expr) (i:expr) = apply2 ctx Z3native.mk_select a i let mk_store (ctx:context) (a:expr) (i:expr) (v:expr) = apply3 ctx Z3native.mk_store a i v let mk_const_array (ctx:context) (domain:Sort.sort) (v:expr) = Z3native.mk_const_array ctx domain v @@ -813,23 +809,23 @@ struct end -module Set = -struct +module Set = +struct let mk_sort (ctx:context) (ty:Sort.sort) = Z3native.mk_set_sort ctx ty - + let is_union (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_UNION) let is_intersect (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_INTERSECT) let is_difference (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_DIFFERENCE) let is_complement (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_COMPLEMENT) let is_subset (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_SUBSET) - let mk_empty (ctx:context) (domain:Sort.sort) = Z3native.mk_empty_set ctx domain + let mk_empty (ctx:context) (domain:Sort.sort) = Z3native.mk_empty_set ctx domain let mk_full (ctx:context) (domain:Sort.sort) = Z3native.mk_full_set ctx domain - let mk_set_add (ctx:context) (set:expr) (element:expr) = apply2 ctx Z3native.mk_set_add set element + let mk_set_add (ctx:context) (set:expr) (element:expr) = apply2 ctx Z3native.mk_set_add set element let mk_del (ctx:context) (set:expr) (element:expr) = apply2 ctx Z3native.mk_set_del set element - let mk_union (ctx:context) (args:expr list) = Z3native.mk_set_union ctx (List.length args) (Array.of_list args) + let mk_union (ctx:context) (args:expr list) = Z3native.mk_set_union ctx (List.length args) (Array.of_list args) - let mk_intersection (ctx:context) (args:expr list) = + let mk_intersection (ctx:context) (args:expr list) = Z3native.mk_set_intersect ctx (List.length args) (Array.of_list args) let mk_difference (ctx:context) (arg1:expr) (arg2:expr) = apply2 ctx Z3native.mk_set_difference arg1 arg2 @@ -839,9 +835,9 @@ struct end -module FiniteDomain = -struct - let mk_sort (ctx:context) (name:Symbol.symbol) (size:int) = Z3native.mk_finite_domain_sort ctx name size +module FiniteDomain = +struct + let mk_sort (ctx:context) (name:Symbol.symbol) (size:int) = Z3native.mk_finite_domain_sort ctx name size let mk_sort_s (ctx:context) (name:string) (size:int) = mk_sort ctx (Symbol.mk_string ctx name) size let is_finite_domain (x:expr) = @@ -851,14 +847,14 @@ struct let is_lt (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FD_LT) - let get_size (x:Sort.sort) = + let get_size (x:Sort.sort) = let (r, v) = (Z3native.get_finite_domain_sort_size (Sort.gc x) x) in if r then v else raise (Error "Conversion failed.") end -module Relation = +module Relation = struct let is_relation (x:expr) = let nc = (Expr.gc x) in @@ -881,20 +877,20 @@ struct let get_arity (x:Sort.sort) = Z3native.get_relation_arity (Sort.gc x) x - let get_column_sorts (x:Sort.sort) = + let get_column_sorts (x:Sort.sort) = let n = get_arity x in let f i = Z3native.get_relation_column (Sort.gc x) x i in mk_list f n end - -module Datatype = + +module Datatype = struct - module Constructor = + module Constructor = struct type constructor = Z3native.constructor - - module FieldNumTable = Hashtbl.Make(struct + + module FieldNumTable = Hashtbl.Make(struct type t = AST.ast let equal x y = AST.compare x y = 0 let hash = AST.hash @@ -910,16 +906,16 @@ struct 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 + let no = Z3native.mk_constructor ctx name recognizer n (Array.of_list field_names) - (let f x = match x with None -> null | Some(s) -> s in + (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 FieldNumTable.add _field_nums no n ; no - + let get_num_fields (x:constructor) = FieldNumTable.find _field_nums x let get_constructor_decl (x:constructor) = @@ -930,7 +926,7 @@ struct let (_, b, _) = (Z3native.query_constructor (gc x) x (get_num_fields x)) in b - let get_accessor_decls (x:constructor) = + 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) @@ -943,7 +939,7 @@ struct let create (ctx:context) (c:Constructor.constructor list) = Z3native.mk_constructor_list ctx (List.length c) (Array.of_list 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) = Constructor.create ctx name recognizer field_names sorts sort_refs @@ -956,7 +952,7 @@ struct let mk_sort_s (ctx:context) (name:string) (constructors:Constructor.constructor list) = mk_sort ctx (Symbol.mk_string ctx name) constructors - + 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 @@ -970,16 +966,16 @@ struct let get_num_constructors (x:Sort.sort) = Z3native.get_datatype_sort_num_constructors (Sort.gc x) x - let get_constructors (x:Sort.sort) = + let get_constructors (x:Sort.sort) = let n = get_num_constructors x in let f i = Z3native.get_datatype_sort_constructor (Sort.gc x) x i in mk_list f n - let get_recognizers (x:Sort.sort) = + let get_recognizers (x:Sort.sort) = let n = (get_num_constructors x) in let f i = Z3native.get_datatype_sort_recognizer (Sort.gc x) x i in mk_list f n - + let get_accessors (x:Sort.sort) = let n = (get_num_constructors x) in let f i = ( @@ -991,8 +987,8 @@ struct end -module Enumeration = -struct +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 a @@ -1014,21 +1010,21 @@ struct let get_const (x:Sort.sort) (inx:int) = Expr.mk_const_f (Sort.gc x) (get_const_decl x inx) - let get_tester_decls (x:Sort.sort) = + let get_tester_decls (x:Sort.sort) = let n = Z3native.get_datatype_sort_num_constructors (Sort.gc x) x in let f i = Z3native.get_datatype_sort_recognizer (Sort.gc x) x i in mk_list f n - + let get_tester_decl (x:Sort.sort) (inx:int) = Z3native.get_datatype_sort_recognizer (Sort.gc x) x inx end -module Z3List = -struct +module Z3List = +struct let mk_sort (ctx:context) (name:Symbol.symbol) (elem_sort:Sort.sort) = let (r, _, _, _, _, _, _) = Z3native.mk_list_sort ctx name elem_sort in - r - + r + let mk_list_s (ctx:context) (name:string) elem_sort = mk_sort ctx (Symbol.mk_string ctx name) elem_sort let get_nil_decl (x:Sort.sort) = Z3native.get_datatype_sort_constructor (Sort.gc x) x 0 let get_is_nil_decl (x:Sort.sort) = Z3native.get_datatype_sort_recognizer (Sort.gc x) x 0 @@ -1040,16 +1036,16 @@ struct end -module Tuple = +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) (Array.of_list field_names) (Array.of_list field_sorts)) in r let get_mk_decl (x:Sort.sort) = Z3native.get_tuple_sort_mk_decl (Sort.gc x) x - let get_num_fields (x:Sort.sort) = Z3native.get_tuple_sort_num_fields (Sort.gc x) x + let get_num_fields (x:Sort.sort) = Z3native.get_tuple_sort_num_fields (Sort.gc x) x - let get_field_decls (x:Sort.sort) = + let get_field_decls (x:Sort.sort) = let n = get_num_fields x in let f i =Z3native.get_tuple_sort_field_decl (Sort.gc x) x i in mk_list f n @@ -1060,7 +1056,7 @@ module Arithmetic = struct let is_int (x:expr) = ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) == INT_SORT) - + let is_arithmetic_numeral (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ANUM) let is_le (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_LE) let is_ge (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_GE) @@ -1077,70 +1073,70 @@ struct let is_int2real (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_REAL) let is_real2int (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_TO_INT) let is_real_is_int (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_IS_INT) - let is_real (x:expr) = ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) == REAL_SORT) + let is_real (x:expr) = ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) == REAL_SORT) let is_int_numeral (x:expr) = (Expr.is_numeral x) && (is_int x) let is_rat_numeral (x:expr) = (Expr.is_numeral x) && (is_real x) let is_algebraic_number (x:expr) = Z3native.is_algebraic_number (Expr.gc x) x module Integer = - struct + struct let mk_sort (ctx:context) = Z3native.mk_int_sort ctx - let get_int (x:expr) = + let get_int (x:expr) = let (r, v) = Z3native.get_numeral_int (Expr.gc x) x in if r then v else raise (Error "Conversion failed.") - let get_big_int (x:expr) = - if (is_int_numeral x) then + let get_big_int (x:expr) = + if (is_int_numeral x) then let s = (Z3native.get_numeral_string (Expr.gc x) x) in Big_int.big_int_of_string s - else + else raise (Error "Conversion failed.") - + let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x - let mk_const (ctx:context) (name:Symbol.symbol) = Expr.mk_const ctx name (mk_sort ctx) + let mk_const (ctx:context) (name:Symbol.symbol) = Expr.mk_const ctx name (mk_sort ctx) let mk_const_s (ctx:context) (name:string) = mk_const ctx (Symbol.mk_string ctx name) - let mk_mod (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_mod t1 t2 + let mk_mod (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_mod t1 t2 let mk_rem (ctx:context) (t1:expr) (t2:expr) = apply2 ctx Z3native.mk_rem t1 t2 - let mk_numeral_s (ctx:context) (v:string) = Z3native.mk_numeral ctx v (mk_sort ctx) + let mk_numeral_s (ctx:context) (v:string) = Z3native.mk_numeral ctx v (mk_sort ctx) let mk_numeral_i (ctx:context) (v:int) = Z3native.mk_int ctx v (mk_sort ctx) let mk_int2real (ctx:context) (t:expr) = apply1 ctx Z3native.mk_int2real t let mk_int2bv (ctx:context) (n:int) (t:expr) = Z3native.mk_int2bv ctx n t end module Real = - struct + struct let mk_sort (ctx:context) = Z3native.mk_real_sort ctx - let get_numerator (x:expr) = apply1 (Expr.gc x) Z3native.get_numerator x + let get_numerator (x:expr) = apply1 (Expr.gc x) Z3native.get_numerator x let get_denominator (x:expr) = apply1 (Expr.gc x) Z3native.get_denominator x - - let get_ratio (x:expr) = + + let get_ratio (x:expr) = if (is_rat_numeral x) then let s = (Z3native.get_numeral_string (Expr.gc x) x) in Ratio.ratio_of_string s - else + else raise (Error "Conversion failed.") let to_decimal_string (x:expr) (precision:int) = Z3native.get_numeral_decimal_string (Expr.gc x) x precision let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x - let mk_const (ctx:context) (name:Symbol.symbol) = Expr.mk_const ctx name (mk_sort ctx) + let mk_const (ctx:context) (name:Symbol.symbol) = Expr.mk_const ctx name (mk_sort ctx) let mk_const_s (ctx:context) (name:string) = mk_const ctx (Symbol.mk_string ctx name) let mk_numeral_nd (ctx:context) (num:int) (den:int) = - if (den == 0) then + if (den == 0) then raise (Error "Denominator is zero") - else + else Z3native.mk_real ctx num den - - let mk_numeral_s (ctx:context) (v:string) = Z3native.mk_numeral ctx v (mk_sort ctx) - let mk_numeral_i (ctx:context) (v:int) = Z3native.mk_int ctx v (mk_sort ctx) - let mk_is_integer (ctx:context) (t:expr) = apply1 ctx Z3native.mk_is_int t + + let mk_numeral_s (ctx:context) (v:string) = Z3native.mk_numeral ctx v (mk_sort ctx) + let mk_numeral_i (ctx:context) (v:int) = Z3native.mk_int ctx v (mk_sort ctx) + let mk_is_integer (ctx:context) (t:expr) = apply1 ctx Z3native.mk_is_int t let mk_real2int (ctx:context) (t:expr) = apply1 ctx Z3native.mk_real2int t module AlgebraicNumber = - struct - let to_upper (x:expr) (precision:int) = Z3native.get_algebraic_number_upper (Expr.gc x) x precision - let to_lower (x:expr) (precision:int) = Z3native.get_algebraic_number_lower (Expr.gc x) x precision + struct + let to_upper (x:expr) (precision:int) = Z3native.get_algebraic_number_upper (Expr.gc x) x precision + let to_lower (x:expr) (precision:int) = Z3native.get_algebraic_number_lower (Expr.gc x) x precision let to_decimal_string (x:expr) (precision:int) = Z3native.get_numeral_decimal_string (Expr.gc x) x precision let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x end @@ -1160,7 +1156,7 @@ end module BitVector = -struct +struct let mk_sort (ctx:context) size = Z3native.mk_bv_sort ctx size let is_bv (x:expr) = ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gc x) (Z3native.get_sort (Expr.gc x) x))) == BV_SORT) @@ -1210,19 +1206,19 @@ struct let is_bv_rotateleft (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ROTATE_LEFT) let is_bv_rotateright (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_ROTATE_RIGHT) let is_bv_rotateleftextended (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_LEFT) - let is_bv_rotaterightextended (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_RIGHT) + let is_bv_rotaterightextended (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_EXT_ROTATE_RIGHT) let is_int2bv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_INT2BV) let is_bv2int (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BV2INT) let is_bv_carry (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CARRY) let is_bv_xor3 (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_XOR3) let get_size (x:Sort.sort) = Z3native.get_bv_sort_size (Sort.gc x) x - let get_int (x:expr) = + let get_int (x:expr) = let (r, v) = Z3native.get_numeral_int (Expr.gc x) x in if r then v else raise (Error "Conversion failed.") let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x let mk_const (ctx:context) (name:Symbol.symbol) (size:int) = - Expr.mk_const ctx name (mk_sort ctx size) + Expr.mk_const ctx name (mk_sort ctx size) let mk_const_s (ctx:context) (name:string) (size:int) = mk_const ctx (Symbol.mk_string ctx name) size let mk_not (ctx:context) (t:expr) = apply1 ctx Z3native.mk_bvnot t @@ -1276,9 +1272,9 @@ struct end -module FloatingPoint = +module FloatingPoint = struct - module RoundingMode = + module RoundingMode = struct let mk_sort (ctx:context) = Z3native.mk_fpa_rounding_mode_sort ctx let is_fprm (x:expr) = (Sort.get_sort_kind (Expr.get_sort(x))) == ROUNDING_MODE_SORT @@ -1287,18 +1283,18 @@ struct let mk_round_nearest_ties_to_away (ctx:context) = Z3native.mk_fpa_round_nearest_ties_to_away ctx let mk_rna (ctx:context) = Z3native.mk_fpa_rna ctx let mk_round_toward_positive (ctx:context) = Z3native.mk_fpa_round_toward_positive ctx - let mk_rtp (ctx:context) = Z3native.mk_fpa_rtp ctx + let mk_rtp (ctx:context) = Z3native.mk_fpa_rtp ctx let mk_round_toward_negative (ctx:context) = Z3native.mk_fpa_round_toward_negative ctx let mk_rtn (ctx:context) = Z3native.mk_fpa_rtn ctx let mk_round_toward_zero (ctx:context) = Z3native.mk_fpa_round_toward_zero ctx let mk_rtz (ctx:context) = Z3native.mk_fpa_rtz ctx end - + let mk_sort (ctx:context) (ebits:int) (sbits:int) = Z3native.mk_fpa_sort ctx ebits sbits let mk_sort_half (ctx:context) = Z3native.mk_fpa_sort_half ctx let mk_sort_16 (ctx:context) = Z3native.mk_fpa_sort_16 ctx let mk_sort_single (ctx:context) = Z3native.mk_fpa_sort_single ctx - let mk_sort_32 (ctx:context) = Z3native.mk_fpa_sort_32 ctx + let mk_sort_32 (ctx:context) = Z3native.mk_fpa_sort_32 ctx let mk_sort_double (ctx:context) = Z3native.mk_fpa_sort_double ctx let mk_sort_64 (ctx:context) = Z3native.mk_fpa_sort_64 ctx let mk_sort_quadruple (ctx:context) = Z3native.mk_fpa_sort_quadruple ctx @@ -1344,7 +1340,7 @@ struct let is_to_sbv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_SBV) let is_to_real (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_REAL) let is_to_ieee_bv (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_IEEE_BV) - + let numeral_to_string (x:expr) = Z3native.get_numeral_string (Expr.gc x) x let mk_const (ctx:context) (name:Symbol.symbol) (s:Sort.sort) = Expr.mk_const ctx name s @@ -1385,7 +1381,7 @@ struct let mk_to_real (ctx:context) (t:expr) = apply1 ctx Z3native.mk_fpa_to_real t let get_ebits (ctx:context) (s:Sort.sort) = Z3native.fpa_get_ebits ctx s let get_sbits (ctx:context) (s:Sort.sort) = Z3native.fpa_get_sbits ctx s - let get_numeral_sign (ctx:context) (t:expr) = Z3native.fpa_get_numeral_sign ctx t + let get_numeral_sign (ctx:context) (t:expr) = Z3native.fpa_get_numeral_sign ctx t let get_numeral_significand_string (ctx:context) (t:expr) = Z3native.fpa_get_numeral_significand_string ctx t let get_numeral_significand_uint (ctx:context) (t:expr) = Z3native.fpa_get_numeral_significand_uint64 ctx t let get_numeral_exponent_string (ctx:context) (t:expr) = Z3native.fpa_get_numeral_exponent_string ctx t @@ -1396,7 +1392,7 @@ struct end -module Proof = +module Proof = struct let is_true (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_TRUE) let is_asserted (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_PR_ASSERTED) @@ -1441,67 +1437,67 @@ end module Goal = -struct +struct type goal = Z3native.goal let gc (x:goal) = Z3native.context_of_goal x let get_precision (x:goal) = goal_prec_of_int (Z3native.goal_precision (gc x) x) - let is_precise (x:goal) = (get_precision x) == GOAL_PRECISE + let is_precise (x:goal) = (get_precision x) == GOAL_PRECISE let is_underapproximation (x:goal) = (get_precision x) == GOAL_UNDER let is_overapproximation (x:goal) = (get_precision x) == GOAL_OVER let is_garbage (x:goal) = (get_precision x) == GOAL_UNDER_OVER - + let add (x:goal) (constraints:expr list) = let f e = Z3native.goal_assert (gc x) x e in ignore (List.map f constraints) ; () - + let is_inconsistent (x:goal) = Z3native.goal_inconsistent (gc x) x - let get_depth (x:goal) = Z3native.goal_depth (gc x) x - let reset (x:goal) = Z3native.goal_reset (gc x) x + let get_depth (x:goal) = Z3native.goal_depth (gc x) x + let reset (x:goal) = Z3native.goal_reset (gc x) x let get_size (x:goal) = Z3native.goal_size (gc x) x let get_formulas (x:goal) = - let n = get_size x in + let n = get_size x in let f i = Z3native.goal_formula (gc x) x i in mk_list f n let get_num_exprs (x:goal) = Z3native.goal_num_exprs (gc x) x - let is_decided_sat (x:goal) = Z3native.goal_is_decided_sat (gc x) x - let is_decided_unsat (x:goal) = Z3native.goal_is_decided_unsat (gc x) x + let is_decided_sat (x:goal) = Z3native.goal_is_decided_sat (gc x) x + let is_decided_unsat (x:goal) = Z3native.goal_is_decided_unsat (gc x) x let translate (x:goal) (to_ctx:context) = Z3native.goal_translate (gc x) x to_ctx let simplify (x:goal) (p:Params.params option) = let tn = Z3native.mk_tactic (gc x) "simplify" in Z3native.tactic_inc_ref (gc x) tn ; let arn = match p with - | None -> Z3native.tactic_apply (gc x) tn x + | None -> Z3native.tactic_apply (gc x) tn x | Some(pn) -> Z3native.tactic_apply_ex (gc x) tn x pn in Z3native.apply_result_inc_ref (gc x) arn ; let sg = Z3native.apply_result_get_num_subgoals (gc x) arn in - let res = if sg == 0 then - raise (Error "No subgoals") - else + let res = if sg == 0 then + raise (Error "No subgoals") + else Z3native.apply_result_get_subgoal (gc x) arn 0 in Z3native.apply_result_dec_ref (gc x) arn ; Z3native.tactic_dec_ref (gc x) tn ; res - let mk_goal (ctx:context) (models:bool) (unsat_cores:bool) (proofs:bool) = + let mk_goal (ctx:context) (models:bool) (unsat_cores:bool) (proofs:bool) = Z3native.mk_goal ctx models unsat_cores proofs let to_string (x:goal) = Z3native.goal_to_string (gc x) x - let as_expr (x:goal) = + let as_expr (x:goal) = let n = get_size x in - if n = 0 then + if n = 0 then Boolean.mk_true (gc x) else if n = 1 then List.hd (get_formulas x) else Boolean.mk_and (gc x) (get_formulas x) -end +end module Model = @@ -1563,7 +1559,7 @@ struct raise (Error "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.") else let np = Z3native.model_get_const_interp (gc x) x f in - if (Z3native.is_null np) then + if Z3native.is_null_ast np then None else Some np @@ -1574,7 +1570,7 @@ struct let sk = sort_kind_of_int (Z3native.get_sort_kind (gc x) (Z3native.get_range (FuncDecl.gc f) f)) in if (FuncDecl.get_arity f) == 0 then let n = Z3native.model_get_const_interp (gc x) x f in - if (Z3native.is_null n) then + if Z3native.is_null_ast n then None else match sk with @@ -1587,7 +1583,7 @@ struct | _ -> raise (Error "Constant functions do not have a function interpretation; use ConstInterp"); else let n = Z3native.model_get_func_interp (gc x) x f in - if (Z3native.is_null n) then None else Some n + if Z3native.is_null_func_interp n then None else Some n (** The number of constants that have an interpretation in the model. *) let get_num_consts (x:model) = Z3native.model_get_num_consts (gc x) x @@ -1698,7 +1694,7 @@ struct let mk_tactic (ctx:context) (name:string) = Z3native.mk_tactic ctx name let and_then (ctx:context) (t1:tactic) (t2:tactic) (ts:tactic list) = - let f p c = (match p with + let f p c = (match p with | None -> Some c | Some(x) -> Some (Z3native.tactic_and_then ctx c x)) in match (List.fold_left f None ts) with @@ -1747,7 +1743,7 @@ struct } in res - let create_sd k v = + let create_sd k v = let res:statistics_entry = { m_key = k ; m_is_int = false ; @@ -1758,14 +1754,14 @@ struct res let get_key (x:statistics_entry) = x.m_key - let get_int (x:statistics_entry) = x.m_int + let get_int (x:statistics_entry) = x.m_int let get_float (x:statistics_entry) = x.m_float let is_int (x:statistics_entry) = x.m_is_int let is_float (x:statistics_entry) = x.m_is_float - let to_string_value (x:statistics_entry) = + let to_string_value (x:statistics_entry) = if (is_int x) then string_of_int (get_int x) - else if (is_float x) then + else if (is_float x) then string_of_float (get_float x) else raise (Error "Unknown statistical entry type") @@ -1774,7 +1770,7 @@ struct let to_string (x:statistics) = Z3native.stats_to_string (gc x) x let get_size (x:statistics) = Z3native.stats_size (gc x) x - + let get_entries (x:statistics) = let n = get_size x in let f i = ( @@ -1797,14 +1793,14 @@ end module Solver = -struct +struct type solver = Z3native.solver type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE let gc (x:solver) = Z3native.context_of_solver x let string_of_status (s:status) = match s with | UNSATISFIABLE -> "unsatisfiable" - | SATISFIABLE -> "satisfiable" + | SATISFIABLE -> "satisfiable" | _ -> "unknown" let get_help (x:solver) = Z3native.solver_get_help (gc x) x @@ -1825,8 +1821,8 @@ struct else let f a b = Z3native.solver_assert_and_track (gc x) x a b in ignore (List.iter2 f cs ps) - - let assert_and_track (x:solver) (c:expr) (p:expr) = + + let assert_and_track (x:solver) (c:expr) (p:expr) = Z3native.solver_assert_and_track (gc x) x c p let get_num_assertions (x:solver) = @@ -1838,39 +1834,39 @@ struct AST.ASTVector.to_expr_list av let check (x:solver) (assumptions:expr list) = - let r = + let r = if ((List.length assumptions) == 0) then lbool_of_int (Z3native.solver_check (gc x) x) else lbool_of_int (Z3native.solver_check_assumptions (gc x) x (List.length assumptions) (Array.of_list assumptions)) in - match r with + match r with | L_TRUE -> SATISFIABLE | L_FALSE -> UNSATISFIABLE | _ -> UNKNOWN - + let get_model (x:solver) = let q = Z3native.solver_get_model (gc x) x in - if (Z3native.is_null q) then None else Some q - + if Z3native.is_null_model q then None else Some q + let get_proof (x:solver) = let q = Z3native.solver_get_proof (gc x) x in - if (Z3native.is_null q) then None else Some q - + if Z3native.is_null_ast q then None else Some q + let get_unsat_core (x:solver) = - let av = Z3native.solver_get_unsat_core (gc x) x in + let av = Z3native.solver_get_unsat_core (gc x) x in AST.ASTVector.to_expr_list av let get_reason_unknown (x:solver) = Z3native.solver_get_reason_unknown (gc x) x let get_statistics (x:solver) = Z3native.solver_get_statistics (gc x) x - + let mk_solver (ctx:context) (logic:Symbol.symbol option) = match logic with | None -> Z3native.mk_solver ctx | Some (x) -> Z3native.mk_solver_for_logic ctx x - + let mk_solver_s (ctx:context) (logic:string) = mk_solver ctx (Some (Symbol.mk_string ctx logic)) - let mk_simple_solver (ctx:context) = Z3native.mk_simple_solver ctx + let mk_simple_solver (ctx:context) = Z3native.mk_simple_solver ctx let mk_solver_t (ctx:context) (t:Tactic.tactic) = Z3native.mk_solver_from_tactic ctx t let translate (x:solver) (to_ctx:context) = Z3native.solver_translate (gc x) x to_ctx let to_string (x:solver) = Z3native.solver_to_string (gc x) x @@ -1881,10 +1877,10 @@ module Fixedpoint = struct type fixedpoint = Z3native.fixedpoint let gc (x:fixedpoint) = Z3native.context_of_fixedpoint x - - let get_help (x:fixedpoint) = Z3native.fixedpoint_get_help (gc x) x - let set_parameters (x:fixedpoint) (p:Params.params) = Z3native.fixedpoint_set_params (gc x) x p - let get_param_descrs (x:fixedpoint) = Z3native.fixedpoint_get_param_descrs (gc x) x + + let get_help (x:fixedpoint) = Z3native.fixedpoint_get_help (gc x) x + let set_parameters (x:fixedpoint) (p:Params.params) = Z3native.fixedpoint_set_params (gc x) x p + let get_param_descrs (x:fixedpoint) = Z3native.fixedpoint_get_param_descrs (gc x) x let add (x:fixedpoint) (constraints:expr list) = let f e = Z3native.fixedpoint_assert (gc x) x e in @@ -1892,15 +1888,15 @@ struct () let register_relation (x:fixedpoint) (f:func_decl) = Z3native.fixedpoint_register_relation (gc x) x f - + let add_rule (x:fixedpoint) (rule:expr) (name:Symbol.symbol option) = - match name with - | None -> Z3native.fixedpoint_add_rule (gc x) x rule null - | Some(y) -> Z3native.fixedpoint_add_rule (gc x) x rule y - + match name with + | None -> Z3native.fixedpoint_add_rule (gc x) x rule (Z3native.mk_null_symbol (gc x)) + | 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) - + let query (x:fixedpoint) (query:expr) = match (lbool_of_int (Z3native.fixedpoint_query (gc x) x query)) with | L_TRUE -> Solver.SATISFIABLE @@ -1912,38 +1908,38 @@ struct | L_TRUE -> Solver.SATISFIABLE | L_FALSE -> Solver.UNSATISFIABLE | _ -> Solver.UNKNOWN - - let push (x:fixedpoint) = Z3native.fixedpoint_push (gc x) x + + let push (x:fixedpoint) = Z3native.fixedpoint_push (gc x) x let pop (x:fixedpoint) = Z3native.fixedpoint_pop (gc x) x let update_rule (x:fixedpoint) (rule:expr) (name:Symbol.symbol) = Z3native.fixedpoint_update_rule (gc x) x rule name let get_answer (x:fixedpoint) = - let q = (Z3native.fixedpoint_get_answer (gc x) x) in - if (Z3native.is_null q) then None else Some q + let q = Z3native.fixedpoint_get_answer (gc x) x in + if Z3native.is_null_ast q then None else Some q let get_reason_unknown (x:fixedpoint) = Z3native.fixedpoint_get_reason_unknown (gc x) x let get_num_levels (x:fixedpoint) (predicate:func_decl) = Z3native.fixedpoint_get_num_levels (gc x) x predicate let get_cover_delta (x:fixedpoint) (level:int) (predicate:func_decl) = - let q = (Z3native.fixedpoint_get_cover_delta (gc x) x level predicate) in - if (Z3native.is_null q) then None else Some q - + let q = Z3native.fixedpoint_get_cover_delta (gc x) x level predicate in + if Z3native.is_null_ast q then None else Some q + 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 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) let to_string_q (x:fixedpoint) (queries:expr list) = Z3native.fixedpoint_to_string (gc x) x (List.length queries) (Array.of_list queries) - let get_rules (x:fixedpoint) = + let get_rules (x:fixedpoint) = let av = Z3native.fixedpoint_get_rules (gc x) x in AST.ASTVector.to_expr_list av - let get_assertions (x:fixedpoint) = + let get_assertions (x:fixedpoint) = let av = Z3native.fixedpoint_get_assertions (gc x) x in (AST.ASTVector.to_expr_list av) @@ -1960,153 +1956,153 @@ struct end -module Optimize = -struct +module Optimize = +struct type optimize = Z3native.optimize - type handle = { opt:optimize; h:int } - - let mk_handle (x:optimize) h = { opt = x; h = h } + type handle = { opt:optimize; h:int } - let mk_opt (ctx:context) = Z3native.mk_optimize ctx - let get_help (x:optimize) = Z3native.optimize_get_help (gc x) x - let set_parameters (x:optimize) (p:Params.params) = Z3native.optimize_set_params (gc x) x p + let mk_handle (x:optimize) h = { opt = x; h = h } + + let mk_opt (ctx:context) = Z3native.mk_optimize ctx + let get_help (x:optimize) = Z3native.optimize_get_help (gc x) x + let set_parameters (x:optimize) (p:Params.params) = Z3native.optimize_set_params (gc x) x p let get_param_descrs (x:optimize) = Z3native.optimize_get_param_descrs (gc x) x - - let add (x:optimize) (constraints:expr list) = - let f e = Z3native.optimize_assert (gc x) x e in - List.iter f constraints - - let add_soft (x:optimize) (e:Expr.expr) (w:string) (s:Symbol.symbol) = + + let add (x:optimize) (constraints:expr list) = + let f e = Z3native.optimize_assert (gc x) x e in + List.iter f constraints + + let add_soft (x:optimize) (e:Expr.expr) (w:string) (s:Symbol.symbol) = mk_handle x (Z3native.optimize_assert_soft (gc x) x e w s) - + let maximize (x:optimize) (e:Expr.expr) = mk_handle x (Z3native.optimize_maximize (gc x) x e) let minimize (x:optimize) (e:Expr.expr) = mk_handle x (Z3native.optimize_minimize (gc x) x e) - - let check (x:optimize) = - let r = lbool_of_int (Z3native.optimize_check (gc x) x) in - match r with - | L_TRUE -> Solver.SATISFIABLE - | L_FALSE -> Solver.UNSATISFIABLE - | _ -> Solver.UNKNOWN - - let get_model (x:optimize) = - let q = Z3native.optimize_get_model (gc x) x in - if (Z3native.is_null q) then None else Some q - + + let check (x:optimize) = + let r = lbool_of_int (Z3native.optimize_check (gc x) x) in + match r with + | L_TRUE -> Solver.SATISFIABLE + | L_FALSE -> Solver.UNSATISFIABLE + | _ -> Solver.UNKNOWN + + let get_model (x:optimize) = + let q = Z3native.optimize_get_model (gc x) x in + if Z3native.is_null_model q then None else Some q + let get_lower (x:handle) (idx:int) = Z3native.optimize_get_lower (gc x.opt) x.opt idx - let get_upper (x:handle) (idx:int) = Z3native.optimize_get_upper (gc x.opt) x.opt idx - let push (x:optimize) = Z3native.optimize_push (gc x) x - let pop (x:optimize) = Z3native.optimize_pop (gc x) x + let get_upper (x:handle) (idx:int) = Z3native.optimize_get_upper (gc x.opt) x.opt idx + let push (x:optimize) = Z3native.optimize_push (gc x) x + let pop (x:optimize) = Z3native.optimize_pop (gc x) x let get_reason_unknown (x:optimize) = Z3native.optimize_get_reason_unknown (gc x) x let to_string (x:optimize) = Z3native.optimize_to_string (gc x) x let get_statistics (x:optimize) = Z3native.optimize_get_statistics (gc x) x -end - - +end + + 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) 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 - if (csn != cs || cdn != cd) then + if (csn != cs || cdn != cd) then raise (Error "Argument size mismatch") else - Z3native.parse_smtlib_string ctx str - cs + Z3native.parse_smtlib_string ctx str + cs (Array.of_list sort_names) (Array.of_list sorts) - cd + cd (Array.of_list decl_names) (Array.of_list 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 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 + if (csn != cs || cdn != cd) then raise (Error "Argument size mismatch") else Z3native.parse_smtlib_file ctx file_name - cs + cs (Array.of_list sort_names) (Array.of_list sorts) - cd + cd (Array.of_list decl_names) (Array.of_list decls) - + let get_num_smtlib_formulas (ctx:context) = Z3native.get_smtlib_num_formulas ctx - + let get_smtlib_formulas (ctx:context) = let n = get_num_smtlib_formulas ctx in let f i = Z3native.get_smtlib_formula ctx i in - mk_list f n - + mk_list f n + let get_num_smtlib_assumptions (ctx:context) = Z3native.get_smtlib_num_assumptions ctx - + let get_smtlib_assumptions (ctx:context) = let n = get_num_smtlib_assumptions ctx in let f i = Z3native.get_smtlib_assumption ctx i in mk_list f n - + let get_num_smtlib_decls (ctx:context) = Z3native.get_smtlib_num_decls ctx - - let get_smtlib_decls (ctx:context) = + + let get_smtlib_decls (ctx:context) = let n = get_num_smtlib_decls ctx in let f i = Z3native.get_smtlib_decl ctx i in mk_list f n - + let get_num_smtlib_sorts (ctx:context) = Z3native.get_smtlib_num_sorts ctx - - let get_smtlib_sorts (ctx:context) = + + let get_smtlib_sorts (ctx:context) = let n = get_num_smtlib_sorts ctx in let f i = Z3native.get_smtlib_sort ctx i in 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 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 + if (csn != cs || cdn != cd) then raise (Error "Argument size mismatch") else - Z3native.parse_smtlib2_string ctx str - cs + Z3native.parse_smtlib2_string ctx str + cs (Array.of_list sort_names) (Array.of_list sorts) - cd + cd (Array.of_list decl_names) (Array.of_list 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 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 + if (csn != cs || cdn != cd) then raise (Error "Argument size mismatch") else Z3native.parse_smtlib2_string ctx file_name - cs + cs (Array.of_list sort_names) (Array.of_list sorts) - cd + cd (Array.of_list decl_names) (Array.of_list decls) end - -module Interpolation = + +module Interpolation = struct let mk_interpolant (ctx:context) (a:expr) = Z3native.mk_interpolant ctx a - + let mk_interpolation_context (settings:(string * string) list) = let cfg = Z3native.mk_config () in let f e = Z3native.set_param_value cfg (fst e) (snd e) in @@ -2116,11 +2112,11 @@ struct Z3native.set_ast_print_mode res (int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT) ; Z3native.set_internal_error_handler res ; res - + let get_interpolant (ctx:context) (pf:expr) (pat:expr) (p:Params.params) = let av = Z3native.get_interpolant ctx pf pat p in AST.ASTVector.to_expr_list av - + let compute_interpolant (ctx:context) (pat:expr) (p:Params.params) = let (r, interp, model) = Z3native.compute_interpolant ctx pat p in let res = (lbool_of_int r) in @@ -2128,23 +2124,23 @@ struct | L_TRUE -> (res, None, Some(model)) | L_FALSE -> (res, Some(AST.ASTVector.to_expr_list interp), None) | _ -> (res, None, None) - + let get_interpolation_profile (ctx:context) = Z3native.interpolation_profile ctx - + let read_interpolation_problem (ctx:context) (filename:string) = let (r, num, cnsts, parents, error, num_theory, theory) = (Z3native.read_interpolation_problem ctx filename) in - match r with + 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 + let f3 i = Array.get theory i in ((mk_list f1 num), (mk_list f2 num), (mk_list f3 num_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 + let (r, str) = Z3native.check_interpolant ctx num (Array.of_list cnsts) (Array.of_list parents) @@ -2155,12 +2151,12 @@ struct | 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)) ; () end - + let set_global_param (id:string) (value:string) = (Z3native.global_param_set id value) @@ -2168,7 +2164,7 @@ let get_global_param (id:string) = let (r, v) = (Z3native.global_param_get id) in if not r then None - else + else Some v let global_param_reset_all = diff --git a/src/api/ml/z3native.ml.pre b/src/api/ml/z3native.ml.pre index 28c6c7d91..87a069df9 100644 --- a/src/api/ml/z3native.ml.pre +++ b/src/api/ml/z3native.ml.pre @@ -32,75 +32,5 @@ and optimize = ptr and param_descrs = ptr and rcf_num = ptr -external is_null : ptr -> bool - = "n_is_null" - -external mk_null : unit -> ptr - = "n_mk_null" - external set_internal_error_handler : ptr -> unit = "n_set_internal_error_handler" - - -external context_of_symbol : symbol -> context - = "n_context_of_symbol" - -external context_of_constructor : constructor -> context - = "n_context_of_constructor" - -external context_of_constructor_list : constructor_list -> context - = "n_context_of_constructor_list" - -external context_of_rcf_num : rcf_num -> context - = "n_context_of_rcf_num" - - -external context_of_ast : ast -> context - = "n_context_of_ast" - -external context_of_params : params -> context - = "n_context_of_params" - -external context_of_param_descrs : param_descrs -> context - = "n_context_of_param_descrs" - -external context_of_model : model -> context - = "n_context_of_model" - -external context_of_func_interp : func_interp -> context - = "n_context_of_func_interp" - -external context_of_func_entry : func_entry -> context - = "n_context_of_func_entry" - -external context_of_goal : goal -> context - = "n_context_of_goal" - -external context_of_tactic : tactic -> context - = "n_context_of_tactic" - -external context_of_probe : probe -> context - = "n_context_of_probe" - -external context_of_apply_result : apply_result -> context - = "n_context_of_apply_result" - -external context_of_solver : solver -> context - = "n_context_of_solver" - -external context_of_stats : stats -> context - = "n_context_of_stats" - -external context_of_ast_vector : ast_vector -> context - = "n_context_of_ast_vector" - -external context_of_ast_map : ast_map -> context - = "n_context_of_ast_map" - -external context_of_fixedpoint : fixedpoint -> context - = "n_context_of_fixedpoint" - -external context_of_optimize : optimize -> context - = "n_context_of_optimize" - - diff --git a/src/api/ml/z3native_stubs.c.pre b/src/api/ml/z3native_stubs.c.pre index de8ba62e6..c726d967f 100644 --- a/src/api/ml/z3native_stubs.c.pre +++ b/src/api/ml/z3native_stubs.c.pre @@ -72,10 +72,27 @@ static struct custom_operations default_custom_ops = { Z3_ ## X ## _plus * p = (Z3_ ## X ## _plus *) Data_custom_val(v); \ cp = p->cp; \ result = caml_alloc_custom(&Z3_context_plus_custom_ops, sizeof(Z3_context_plus), 0, 1); \ - *(Z3_context_plus*)Data_custom_val(result) = cp; \ - /* We increment the usage counter of the context */ \ + *(Z3_context_plus *)Data_custom_val(result) = cp; \ + /* We increment the usage counter of the context, as we just \ + created a second custom block holding that context */ \ cp->obj_count++; \ CAMLreturn(result); \ + } \ + \ + CAMLprim value DLL_PUBLIC n_is_null_ ## X (value v) { \ + CAMLparam1(v); \ + Z3_ ## X ## _plus* pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \ + CAMLreturn(Val_bool(pp->p == NULL)); \ + } \ + \ + CAMLprim value DLL_PUBLIC n_mk_null_ ## X (value v) { \ + CAMLparam1(v); \ + CAMLlocal1(result); \ + Z3_context_plus cp = *(Z3_context_plus*)(Data_custom_val(v)); \ + Z3_ ## X ## _plus a = Z3_ ## X ## _plus_mk(cp, NULL); \ + result = caml_alloc_custom(&Z3_ ## X ## _plus_custom_ops, sizeof(Z3_ ## X ## _plus), 0, 1); \ + *(Z3_ ## X ## _plus*)(Data_custom_val(result)) = a; \ + CAMLreturn(result); \ } @@ -103,7 +120,8 @@ Z3_context_plus Z3_context_plus_mk(Z3_context c) { Z3_context_plus r = (Z3_context_plus)malloc(sizeof(Z3_context_plus_data)); r->ctx = c; /* The context created here will be wrapped into a custom block. - Hence, we assign it a counter of one. */ + We regard custom blocks that point to a Z3_context_plus structure + as a usage of this structure. Hence, we assign it a counter of one. */ r->obj_count = 1; return r; } @@ -113,17 +131,17 @@ Z3_context Z3_context_plus_raw(Z3_context_plus * cp) { } inline void try_to_delete_context(Z3_context_plus cp) { - if (cp->obj_count > 0) - /* printf("try_to_delete_context: Not deleting context %p(%p) with cnt=%lu.\n", cp, cp->ctx, cp->obj_count) */ ; - else if (cp->obj_count < 0) - printf("try_to_delete_context: ERROR, found context %p(%p) with negative cnt=%lu.\n", cp, cp->ctx, cp->obj_count); - else { - printf("try_to_delete_context: Deleting context %p(%p) with cnt=%lu.\n", cp, cp->ctx, cp->obj_count); + if (cp->obj_count == 0) { + /* printf("try_to_delete_context: Deleting context %p(%p) with cnt=0.\n", cp, cp->ctx); */ Z3_del_context(cp->ctx); - cp->ctx = NULL; - cp->obj_count = 0; free(cp); } + /* + else if (cp->obj_count > 0) + printf("try_to_delete_context: Not deleting context %p(%p) with cnt=%lu.\n", cp, cp->ctx, cp->obj_count); + else if (cp->obj_count < 0) + printf("try_to_delete_context: ERROR, found context %p(%p) with negative cnt=%lu.\n", cp, cp->ctx, cp->obj_count); + */ } void Z3_context_finalize(value v) { @@ -147,27 +165,29 @@ static struct custom_operations Z3_context_plus_custom_ops = { typedef struct { Z3_context_plus cp; - Z3_ast a; + Z3_ast p; } Z3_ast_plus; -Z3_ast_plus Z3_ast_plus_mk(Z3_context_plus cp, Z3_ast a) { +Z3_ast_plus Z3_ast_plus_mk(Z3_context_plus cp, Z3_ast p) { Z3_ast_plus r; r.cp = cp; - r.a = a; + r.p = p; /* printf("++\n"); */ cp->obj_count++; - Z3_inc_ref(cp->ctx, a); + if (p != NULL) + Z3_inc_ref(cp->ctx, p); return r; } Z3_ast Z3_ast_plus_raw(Z3_ast_plus * ap) { - return ap->a; + return ap->p; } void Z3_ast_finalize(value v) { /* printf("--\n"); */ Z3_ast_plus * ap = (Z3_ast_plus*)(Data_custom_val(v)); - Z3_dec_ref(ap->cp->ctx, ap->a); + if (ap->p != NULL) + Z3_dec_ref(ap->cp->ctx, ap->p); ap->cp->obj_count--; try_to_delete_context(ap->cp); } @@ -176,8 +196,14 @@ int Z3_ast_compare(value v1, value v2) { Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1); Z3_ast_plus * a2 = (Z3_ast_plus*)Data_custom_val(v2); assert(a1->cp->ctx == a2->cp->ctx); - unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->a); - unsigned id2 = Z3_get_ast_id(a2->cp->ctx, a2->a); + if (a1->p == NULL && a2->p == NULL) + return 0; + if (a1->p == NULL) + return -1; + if (a2->p == NULL) + return +1; + unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->p); + unsigned id2 = Z3_get_ast_id(a2->cp->ctx, a2->p); if (id1 == id2) return 0; else if (id1 < id2) @@ -188,8 +214,15 @@ int Z3_ast_compare(value v1, value v2) { int Z3_ast_compare_ext(value v1, value v2) { Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1); - unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->a); + unsigned id1; int id2 = Val_int(v2); + if (a1->p == NULL && id2 == 0) + return 0; + if (a1->p == NULL) + return -1; + if (id2 == 0) + return +1; + id1 = Z3_get_ast_id(a1->cp->ctx, a1->p); if (id1 == id2) return 0; else if (id1 < id2) @@ -200,7 +233,10 @@ int Z3_ast_compare_ext(value v1, value v2) { intnat Z3_ast_hash(value v) { Z3_ast_plus * ap = (Z3_ast_plus*)Data_custom_val(v); - return Z3_get_ast_hash(ap->cp->ctx, ap->a); + if (ap->p == NULL) + return 0; + else + return Z3_get_ast_hash(ap->cp->ctx, ap->p); } static struct custom_operations Z3_ast_plus_custom_ops = { @@ -215,9 +251,6 @@ static struct custom_operations Z3_ast_plus_custom_ops = { MK_CTX_OF(ast) - - - #define MK_PLUS_OBJ_NO_REF(X) \ typedef struct { \ Z3_context_plus cp; \ @@ -241,7 +274,7 @@ MK_CTX_OF(ast) pp->cp->obj_count--; \ try_to_delete_context(pp->cp); \ } \ - \ + \ static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \ (char*) "Z3_" #X " ops", \ Z3_ ## X ## _finalize, \ @@ -265,7 +298,8 @@ MK_CTX_OF(ast) r.cp = cp; \ r.p = p; \ r.cp->obj_count++; \ - Z3_ ## X ## _inc_ref(cp->ctx, p); \ + if (p != NULL) \ + Z3_ ## X ## _inc_ref(cp->ctx, p); \ return r; \ } \ \ @@ -275,7 +309,8 @@ MK_CTX_OF(ast) \ void Z3_ ## X ## _finalize(value v) { \ Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \ - Z3_ ## X ## _dec_ref(pp->cp->ctx, pp->p); \ + if (pp->p != NULL) \ + Z3_ ## X ## _dec_ref(pp->cp->ctx, pp->p); \ pp->cp->obj_count--; \ try_to_delete_context(pp->cp); \ } \ @@ -292,8 +327,6 @@ MK_CTX_OF(ast) \ MK_CTX_OF(X) - - MK_PLUS_OBJ_NO_REF(symbol) MK_PLUS_OBJ_NO_REF(constructor) MK_PLUS_OBJ_NO_REF(constructor_list) @@ -319,19 +352,6 @@ MK_PLUS_OBJ(optimize) extern "C" { #endif -CAMLprim DLL_PUBLIC value n_is_null(value p) { - void * t = * (void**) Data_custom_val(p); - return Val_bool(t == 0); -} - -CAMLprim DLL_PUBLIC value n_mk_null( void ) { - CAMLparam0(); - CAMLlocal1(result); - result = caml_alloc(1, 0); - result = Val_int(0); - CAMLreturn (result); -} - void MLErrorHandler(Z3_context c, Z3_error_code e) { /* Internal do-nothing error handler. This is required to avoid that Z3 calls exit()