mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-16 07:45:27 +00:00
Code Activity

Merge pull request #2 from martin-neuhaeusser/ml_api_patch2

Browse source 
Correct reference counting and handling of NULL pointers in new OCaml bindings.
This commit is contained in:
Christoph M. Wintersteiger 2016-04-05 13:01:04 +01:00
commit 991eae8767
4 changed files with 514 additions and 521 deletions
Download patch file Download diff file Expand all files Collapse all files

80
scripts/update_api.py
View file

@ -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:
@ -1333,7 +1362,7 @@ def mk_z3native_stubs_c(ml_dir): # C interface
i = 0
for param in params:
if param_type(param) == CONTEXT and i == 0:
ml_wrapper.write(' Z3_context_plus * ctx_p = (Z3_context_plus*) Data_custom_val(a' + str(i) + ');\n')
ml_wrapper.write(' Z3_context_plus ctx_p = *(Z3_context_plus*) Data_custom_val(a' + str(i) + ');\n')
ml_wrapper.write(' Z3_context _a0 = ctx_p->ctx;\n')
have_context = True
else:
@ -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)

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

@ -10,10 +10,6 @@ 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 =
@ -702,8 +698,8 @@ 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)
@ -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,8 +736,8 @@ 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)
@ -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)
@ -914,7 +910,7 @@ struct
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 ;
@ -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
@ -1851,11 +1847,11 @@ struct
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
@ -1895,8 +1891,8 @@ struct
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
| 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)
@ -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 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
@ -1991,7 +1987,7 @@ struct
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
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

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

@ -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"

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

@ -68,50 +68,85 @@ static struct custom_operations default_custom_ops = {
CAMLprim DLL_PUBLIC value n_context_of_ ## X(value v) { \
CAMLparam1(v); \
CAMLlocal1(result); \
Z3_context_plus cp; \
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) = *p->cp; \
*(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); \
}
/* Context objects */
/* The Z3context_plus_data exists exactly once for each context,
no matter how many custom blocks for that context exist.
Each custom block only stores a pointer to the corresponding
Z3_context_plus_data. This ensures that the reference counting
is performed at exactly one place and not within the custom
blocks that get copied. */
typedef struct {
Z3_context ctx;
unsigned long obj_count:sizeof(unsigned long)-1;
unsigned ok_to_delete:1;
} Z3_context_plus;
unsigned long obj_count;
} Z3_context_plus_data;
/* A context is wrapped to an OCaml value by storing a pointer
to its associated Z3_context_plus_data instance.
This instance gets created in mk_context and is deleted
together with the Z3 context instance in try_to_delete_context
whenever the obj_count field is zero. */
typedef Z3_context_plus_data* Z3_context_plus;
Z3_context_plus Z3_context_plus_mk(Z3_context c) {
Z3_context_plus r;
r.ctx = c;
r.obj_count = 0;
r.ok_to_delete = 0;
/* printf("ctx++ %p\n", 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.
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;
}
Z3_context Z3_context_plus_raw(Z3_context_plus * cp) {
return cp->ctx;
return (*cp)->ctx;
}
void try_to_delete_context(Z3_context_plus * cp) {
if (!cp->ok_to_delete || cp->obj_count != 0)
/* printf("Trying to delete context %p.\n", cp->ctx) */ ;
else {
/* printf("Actually deleting context %p.\n", cp->ctx); */
inline void try_to_delete_context(Z3_context_plus cp) {
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 = 0;
cp->obj_count = 0;
cp->ok_to_delete = 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) {
Z3_context_plus * cp = (Z3_context_plus*)Data_custom_val(v);
/* printf("ctx--; cnt=%lu\n", cp->obj_count); */
cp->ok_to_delete = 1;
Z3_context_plus cp = *(Z3_context_plus*)Data_custom_val(v);
cp->obj_count--;
try_to_delete_context(cp);
}
@ -129,28 +164,30 @@ static struct custom_operations Z3_context_plus_custom_ops = {
/* AST objects */
typedef struct {
Z3_context_plus * cp;
Z3_ast a;
Z3_context_plus cp;
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);
}
@ -159,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)
@ -171,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)
@ -183,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 = {
@ -198,16 +251,13 @@ 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; \
Z3_context_plus cp; \
Z3_ ## X p; \
} Z3_ ## X ## _plus; \
\
Z3_ ## X ## _plus Z3_ ## X ## _plus_mk(Z3_context_plus * cp, Z3_ ## X p) { \
Z3_ ## X ## _plus Z3_ ## X ## _plus_mk(Z3_context_plus cp, Z3_ ## X p) { \
Z3_ ## X ## _plus r; \
r.cp = cp; \
r.p = p; \
@ -224,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, \
@ -239,16 +289,17 @@ MK_CTX_OF(ast)
#define MK_PLUS_OBJ(X) \
typedef struct { \
Z3_context_plus * cp; \
Z3_context_plus cp; \
Z3_ ## X p; \
} Z3_ ## X ## _plus; \
\
Z3_ ## X ## _plus Z3_ ## X ## _plus_mk(Z3_context_plus * cp, Z3_ ## X p) { \
Z3_ ## X ## _plus Z3_ ## X ## _plus_mk(Z3_context_plus cp, Z3_ ## X p) { \
Z3_ ## X ## _plus r; \
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; \
} \
\
@ -258,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); \
} \
@ -275,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)
@ -302,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()