mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

Translate correctly between OCaml option values and NULL pointers

Browse source 
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.
This commit is contained in:
martin-neuhaeusser 2016-04-04 17:16:15 +02:00
parent b85516c271
commit f133f478c8
4 changed files with 451 additions and 475 deletions
Download patch file Download diff file Expand all files Collapse all files

74
scripts/update_api.py
View file

@ -1094,6 +1094,8 @@ def ml_plus_type(ts):
def ml_minus_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': if ts == 'Z3_ast' or ts == 'Z3_sort' or ts == 'Z3_func_decl' or ts == 'Z3_app' or ts == 'Z3_pattern':
return 'Z3_ast' 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': elif ts == 'Z3_constructor_plus':
return 'Z3_constructor' return 'Z3_constructor'
elif ts == 'Z3_constructor_list_plus': elif ts == 'Z3_constructor_list_plus':
@ -1151,7 +1153,7 @@ def ml_has_plus_type(ts):
def ml_unwrap(t, ts, s): def ml_unwrap(t, ts, s):
if t == STRING: if t == STRING:
return '(' + ts + ') String_val(' + s + ')' return '(' + ts + ') String_val(' + s + ')'
elif t == BOOL: elif t == BOOL or (type2str(t) == 'Z3_bool'):
return '(' + ts + ') Bool_val(' + s + ')' return '(' + ts + ') Bool_val(' + s + ')'
elif t == INT or t == PRINT_MODE or t == ERROR_CODE: elif t == INT or t == PRINT_MODE or t == ERROR_CODE:
return '(' + ts + ') Int_val(' + s + ')' return '(' + ts + ') Int_val(' + s + ')'
@ -1172,7 +1174,7 @@ def ml_unwrap(t, ts, s):
def ml_set_wrap(t, d, n): def ml_set_wrap(t, d, n):
if t == VOID: if t == VOID:
return d + ' = Val_unit;' return d + ' = Val_unit;'
elif t == BOOL: elif t == BOOL or (type2str(t) == 'Z3_bool'):
return d + ' = Val_bool(' + n + ');' return d + ' = Val_bool(' + n + ');'
elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE: elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE:
return d + ' = Val_int(' + n + ');' return d + ' = Val_int(' + n + ');'
@ -1186,6 +1188,15 @@ def ml_set_wrap(t, d, n):
pts = ml_plus_type(type2str(t)) pts = ml_plus_type(type2str(t))
return '*(' + pts + '*)Data_custom_val(' + d + ') = ' + n + ';' 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): def mk_ml(ml_dir):
global Type2Str global Type2Str
ml_nativef = os.path.join(ml_dir, 'z3native.ml') ml_nativef = os.path.join(ml_dir, 'z3native.ml')
@ -1258,6 +1269,18 @@ def mk_ml(ml_dir):
ml_native.write(' a%d' % i) ml_native.write(' a%d' % i)
i = i + 1 i = i + 1
ml_native.write('\n') 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.write('(**/**)\n')
ml_native.close() ml_native.close()
@ -1266,7 +1289,6 @@ def mk_ml(ml_dir):
mk_z3native_stubs_c(ml_dir) mk_z3native_stubs_c(ml_dir)
def mk_z3native_stubs_c(ml_dir): # C interface def mk_z3native_stubs_c(ml_dir): # C interface
ml_wrapperf = os.path.join(ml_dir, 'z3native_stubs.c') ml_wrapperf = os.path.join(ml_dir, 'z3native_stubs.c')
ml_wrapper = open(ml_wrapperf, 'w') 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') ml_wrapper.write(' CAMLlocal1(result);\n')
else: else:
c = 0 c = 0
needs_tmp_value = False
for p in params: for p in params:
if is_out_param(p) or is_array_param(p): if is_out_param(p) or is_array_param(p):
c = c + 1 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)) ml_wrapper.write(' CAMLlocal%s(result, z3rv_val' % (c+2))
for p in params: for p in params:
if is_out_param(p) or is_array_param(p): if is_out_param(p) or is_array_param(p):
ml_wrapper.write(', _a%s_val' % i) ml_wrapper.write(', _a%s_val' % i)
i = i + 1 i = i + 1
if needs_tmp_value:
ml_wrapper.write(', tmp_val')
ml_wrapper.write(');\n') ml_wrapper.write(');\n')
if len(ap) != 0: if len(ap) != 0:
@ -1371,20 +1400,14 @@ def mk_z3native_stubs_c(ml_dir): # C interface
ml_wrapper.write(' }\n') ml_wrapper.write(' }\n')
i = i + 1 i = i + 1
ml_wrapper.write(' ') ml_wrapper.write('\n /* invoke Z3 function */\n ')
if result != VOID: if result != VOID:
ts = type2str(result) ts = type2str(result)
if ml_has_plus_type(ts): if ml_has_plus_type(ts):
ml_wrapper.write('%s z3rv_m = ' % 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: else:
ml_wrapper.write('result = caml_alloc_custom(&default_custom_ops, sizeof(%s), 0, 1);\n ' % ts)
ml_wrapper.write('%s z3rv = ' % ts) ml_wrapper.write('%s z3rv = ' % ts)
elif len(op) != 0:
ml_wrapper.write('result = caml_alloc(%s, 0);\n ' % ret_size)
# invoke procedure # invoke procedure
ml_wrapper.write('%s(' % name) ml_wrapper.write('%s(' % name)
i = 0 i = 0
@ -1413,7 +1436,6 @@ def mk_z3native_stubs_c(ml_dir): # C interface
ts = type2str(result) ts = type2str(result)
if ml_has_plus_type(ts): if ml_has_plus_type(ts):
pts = ml_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: if name in NULLWrapped:
ml_wrapper.write(' %s z3rv = %s_mk(z3rv_m);\n' % (pts, pts)) ml_wrapper.write(' %s z3rv = %s_mk(z3rv_m);\n' % (pts, pts))
else: else:
@ -1421,6 +1443,14 @@ def mk_z3native_stubs_c(ml_dir): # C interface
# convert output params # convert output params
if len(op) > 0: 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 i = 0
for p in params: for p in params:
pt = param_type(p) 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)) ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) {\n' % param_array_capacity_pos(p))
pts = ml_plus_type(ts) pts = ml_plus_type(ts)
pops = ml_plus_ops_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): 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 _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: else:
ml_wrapper.write(' %s\n' % ml_set_wrap(pt, 't', '_a%d[_i]' % 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, t);\n' % i) ml_wrapper.write(' Store_field(_a%s_val, _i, tmp_val);\n' % i)
ml_wrapper.write(' }\n') ml_wrapper.write(' }\n')
elif param_kind(p) == OUT_MANAGED_ARRAY: elif param_kind(p) == OUT_MANAGED_ARRAY:
wrp = ml_set_wrap(pt, '_a%d_val' % i, '_a%d' % i) 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): if ml_has_plus_type(ts):
pts = ml_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 _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: 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 i = i + 1
# return tuples # return tuples
if len(op) == 0:
ml_wrapper.write(' %s\n' % ml_set_wrap(result, "result", "z3rv"))
else:
i = j = 0 i = j = 0
if result != VOID: 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') ml_wrapper.write(' Store_field(result, 0, z3rv_val);\n')
j = j + 1 j = j + 1
for p in params: 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)) ml_wrapper.write(' Store_field(result, %s, _a%s_val);\n' % (j, i))
j = j + 1 j = j + 1
i = i + 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 # local array cleanup
ml_wrapper.write('\n /* cleanup and return */\n')
i = 0 i = 0
for p in params: for p in params:
k = param_kind(p) k = param_kind(p)

46
src/api/ml/z3.ml
View file

@ -10,10 +10,6 @@ open Z3enums
exception Error of string exception Error of string
let _ = Callback.register_exception "Z3EXCEPTION" (Error "") 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 type context = Z3native.context
module Log = module Log =
@ -702,8 +698,8 @@ struct
else else
Z3native.mk_quantifier_ex ctx true Z3native.mk_quantifier_ex ctx true
(match weight with | None -> 1 | Some(x) -> x) (match weight with | None -> 1 | Some(x) -> x)
(match quantifier_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 -> null | 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 patterns) (Array.of_list patterns)
(List.length nopatterns) (Array.of_list nopatterns) (List.length nopatterns) (Array.of_list nopatterns)
(List.length sorts) (Array.of_list sorts) (List.length sorts) (Array.of_list sorts)
@ -720,8 +716,8 @@ struct
else else
Z3native.mk_quantifier_const_ex ctx true Z3native.mk_quantifier_const_ex ctx true
(match weight with | None -> 1 | Some(x) -> x) (match weight with | None -> 1 | Some(x) -> x)
(match quantifier_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 -> null | 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 bound_constants) (Array.of_list bound_constants)
(List.length patterns) (Array.of_list patterns) (List.length patterns) (Array.of_list patterns)
(List.length nopatterns) (Array.of_list nopatterns) (List.length nopatterns) (Array.of_list nopatterns)
@ -740,8 +736,8 @@ struct
else else
Z3native.mk_quantifier_ex ctx false Z3native.mk_quantifier_ex ctx false
(match weight with | None -> 1 | Some(x) -> x) (match weight with | None -> 1 | Some(x) -> x)
(match quantifier_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 -> null | 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 patterns) (Array.of_list patterns)
(List.length nopatterns) (Array.of_list nopatterns) (List.length nopatterns) (Array.of_list nopatterns)
(List.length sorts) (Array.of_list sorts) (List.length sorts) (Array.of_list sorts)
@ -758,8 +754,8 @@ struct
else else
Z3native.mk_quantifier_const_ex ctx false Z3native.mk_quantifier_const_ex ctx false
(match weight with | None -> 1 | Some(x) -> x) (match weight with | None -> 1 | Some(x) -> x)
(match quantifier_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 -> null | 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 bound_constants) (Array.of_list bound_constants)
(List.length patterns) (Array.of_list patterns) (List.length patterns) (Array.of_list patterns)
(List.length nopatterns) (Array.of_list nopatterns) (List.length nopatterns) (Array.of_list nopatterns)
@ -914,7 +910,7 @@ struct
recognizer recognizer
n n
(Array.of_list field_names) (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 (List.map f sorts))
(Array.of_list sort_refs) in (Array.of_list sort_refs) in
FieldNumTable.add _field_nums no n ; FieldNumTable.add _field_nums no n ;
@ -1563,7 +1559,7 @@ struct
raise (Error "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.") raise (Error "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.")
else else
let np = Z3native.model_get_const_interp (gc x) x f in 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 None
else else
Some np 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 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 if (FuncDecl.get_arity f) == 0 then
let n = Z3native.model_get_const_interp (gc x) x f in 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 None
else else
match sk with match sk with
@ -1587,7 +1583,7 @@ struct
| _ -> raise (Error "Constant functions do not have a function interpretation; use ConstInterp"); | _ -> raise (Error "Constant functions do not have a function interpretation; use ConstInterp");
else else
let n = Z3native.model_get_func_interp (gc x) x f in 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. *) (** 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 let get_num_consts (x:model) = Z3native.model_get_num_consts (gc x) x
@ -1851,11 +1847,11 @@ struct
let get_model (x:solver) = let get_model (x:solver) =
let q = Z3native.solver_get_model (gc x) x in 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 get_proof (x:solver) =
let q = Z3native.solver_get_proof (gc x) x in 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 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
@ -1895,8 +1891,8 @@ struct
let add_rule (x:fixedpoint) (rule:expr) (name:Symbol.symbol option) = let add_rule (x:fixedpoint) (rule:expr) (name:Symbol.symbol option) =
match name with match name with
| None -> Z3native.fixedpoint_add_rule (gc x) x rule null | 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 | Some y -> Z3native.fixedpoint_add_rule (gc x) x rule y
let add_fact (x:fixedpoint) (pred:func_decl) (args:int list) = 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) (Array.of_list args)
@ -1918,15 +1914,15 @@ struct
let update_rule (x:fixedpoint) (rule:expr) (name:Symbol.symbol) = Z3native.fixedpoint_update_rule (gc x) x rule name 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 get_answer (x:fixedpoint) =
let q = (Z3native.fixedpoint_get_answer (gc x) x) in let q = Z3native.fixedpoint_get_answer (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_reason_unknown (x:fixedpoint) = Z3native.fixedpoint_get_reason_unknown (gc x) x 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_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 get_cover_delta (x:fixedpoint) (level:int) (predicate:func_decl) =
let q = (Z3native.fixedpoint_get_cover_delta (gc x) x level predicate) in let q = Z3native.fixedpoint_get_cover_delta (gc x) x level predicate in
if (Z3native.is_null q) then None else Some q if Z3native.is_null_ast q then None else Some q
let add_cover (x:fixedpoint) (level:int) (predicate:func_decl) (property:expr) = let add_cover (x:fixedpoint) (level:int) (predicate:func_decl) (property:expr) =
Z3native.fixedpoint_add_cover (gc x) x level predicate property Z3native.fixedpoint_add_cover (gc x) x level predicate property
@ -1991,7 +1987,7 @@ struct
let get_model (x:optimize) = let get_model (x:optimize) =
let q = Z3native.optimize_get_model (gc x) x in let q = Z3native.optimize_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_lower (x:handle) (idx:int) = Z3native.optimize_get_lower (gc x.opt) x.opt idx 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 get_upper (x:handle) (idx:int) = Z3native.optimize_get_upper (gc x.opt) x.opt idx

70
src/api/ml/z3native.ml.pre
View file

@ -32,75 +32,5 @@ and optimize = ptr
and param_descrs = ptr and param_descrs = ptr
and rcf_num = 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 external set_internal_error_handler : ptr -> unit
= "n_set_internal_error_handler" = "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"

98
src/api/ml/z3native_stubs.c.pre
View file

@ -72,10 +72,27 @@ static struct custom_operations default_custom_ops = {
Z3_ ## X ## _plus * p = (Z3_ ## X ## _plus *) Data_custom_val(v); \ Z3_ ## X ## _plus * p = (Z3_ ## X ## _plus *) Data_custom_val(v); \
cp = p->cp; \ cp = p->cp; \
result = caml_alloc_custom(&Z3_context_plus_custom_ops, sizeof(Z3_context_plus), 0, 1); \ result = caml_alloc_custom(&Z3_context_plus_custom_ops, sizeof(Z3_context_plus), 0, 1); \
*(Z3_context_plus*)Data_custom_val(result) = cp; \ *(Z3_context_plus *)Data_custom_val(result) = cp; \
/* We increment the usage counter of the context */ \ /* We increment the usage counter of the context, as we just \
created a second custom block holding that context */ \
cp->obj_count++; \ cp->obj_count++; \
CAMLreturn(result); \ 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)); Z3_context_plus r = (Z3_context_plus)malloc(sizeof(Z3_context_plus_data));
r->ctx = c; r->ctx = c;
/* The context created here will be wrapped into a custom block. /* 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; r->obj_count = 1;
return r; 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) { inline void try_to_delete_context(Z3_context_plus cp) {
if (cp->obj_count > 0) 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) */ ; /* printf("try_to_delete_context: Deleting context %p(%p) with cnt=0.\n", cp, cp->ctx); */
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);
Z3_del_context(cp->ctx); Z3_del_context(cp->ctx);
cp->ctx = NULL;
cp->obj_count = 0;
free(cp); 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) { void Z3_context_finalize(value v) {
@ -147,27 +165,29 @@ static struct custom_operations Z3_context_plus_custom_ops = {
typedef struct { typedef struct {
Z3_context_plus cp; Z3_context_plus cp;
Z3_ast a; Z3_ast p;
} Z3_ast_plus; } 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; Z3_ast_plus r;
r.cp = cp; r.cp = cp;
r.a = a; r.p = p;
/* printf("++\n"); */ /* printf("++\n"); */
cp->obj_count++; cp->obj_count++;
Z3_inc_ref(cp->ctx, a); if (p != NULL)
Z3_inc_ref(cp->ctx, p);
return r; return r;
} }
Z3_ast Z3_ast_plus_raw(Z3_ast_plus * ap) { Z3_ast Z3_ast_plus_raw(Z3_ast_plus * ap) {
return ap->a; return ap->p;
} }
void Z3_ast_finalize(value v) { void Z3_ast_finalize(value v) {
/* printf("--\n"); */ /* printf("--\n"); */
Z3_ast_plus * ap = (Z3_ast_plus*)(Data_custom_val(v)); 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--; ap->cp->obj_count--;
try_to_delete_context(ap->cp); 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 * a1 = (Z3_ast_plus*)Data_custom_val(v1);
Z3_ast_plus * a2 = (Z3_ast_plus*)Data_custom_val(v2); Z3_ast_plus * a2 = (Z3_ast_plus*)Data_custom_val(v2);
assert(a1->cp->ctx == a2->cp->ctx); assert(a1->cp->ctx == a2->cp->ctx);
unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->a); if (a1->p == NULL && a2->p == NULL)
unsigned id2 = Z3_get_ast_id(a2->cp->ctx, a2->a); 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) if (id1 == id2)
return 0; return 0;
else if (id1 < id2) 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) { int Z3_ast_compare_ext(value v1, value v2) {
Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1); 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); 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) if (id1 == id2)
return 0; return 0;
else if (id1 < id2) else if (id1 < id2)
@ -200,7 +233,10 @@ int Z3_ast_compare_ext(value v1, value v2) {
intnat Z3_ast_hash(value v) { intnat Z3_ast_hash(value v) {
Z3_ast_plus * ap = (Z3_ast_plus*)Data_custom_val(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 = { 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) MK_CTX_OF(ast)
#define MK_PLUS_OBJ_NO_REF(X) \ #define MK_PLUS_OBJ_NO_REF(X) \
typedef struct { \ typedef struct { \
Z3_context_plus cp; \ Z3_context_plus cp; \
@ -265,6 +298,7 @@ MK_CTX_OF(ast)
r.cp = cp; \ r.cp = cp; \
r.p = p; \ r.p = p; \
r.cp->obj_count++; \ r.cp->obj_count++; \
if (p != NULL) \
Z3_ ## X ## _inc_ref(cp->ctx, p); \ Z3_ ## X ## _inc_ref(cp->ctx, p); \
return r; \ return r; \
} \ } \
@ -275,6 +309,7 @@ MK_CTX_OF(ast)
\ \
void Z3_ ## X ## _finalize(value v) { \ void Z3_ ## X ## _finalize(value v) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \ Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
if (pp->p != NULL) \
Z3_ ## X ## _dec_ref(pp->cp->ctx, pp->p); \ Z3_ ## X ## _dec_ref(pp->cp->ctx, pp->p); \
pp->cp->obj_count--; \ pp->cp->obj_count--; \
try_to_delete_context(pp->cp); \ try_to_delete_context(pp->cp); \
@ -292,8 +327,6 @@ MK_CTX_OF(ast)
\ \
MK_CTX_OF(X) MK_CTX_OF(X)
MK_PLUS_OBJ_NO_REF(symbol) MK_PLUS_OBJ_NO_REF(symbol)
MK_PLUS_OBJ_NO_REF(constructor) MK_PLUS_OBJ_NO_REF(constructor)
MK_PLUS_OBJ_NO_REF(constructor_list) MK_PLUS_OBJ_NO_REF(constructor_list)
@ -319,19 +352,6 @@ MK_PLUS_OBJ(optimize)
extern "C" { extern "C" {
#endif #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) void MLErrorHandler(Z3_context c, Z3_error_code e)
{ {
/* Internal do-nothing error handler. This is required to avoid that Z3 calls exit() /* Internal do-nothing error handler. This is required to avoid that Z3 calls exit()