mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

Merge pull request #3 from martin-neuhaeusser/ml_api_patch3

Browse source 
Improvements of the OCaml API implementation
This commit is contained in:
Christoph M. Wintersteiger 2016-04-06 14:47:36 +01:00
commit ee7b09b3b6
4 changed files with 1503 additions and 1531 deletions
Download patch file Download diff file Expand all files Collapse all files

41
scripts/update_api.py
View file

@ -1208,9 +1208,9 @@ def mk_ml(ml_dir):
ml_native.write(s); ml_native.write(s);
ml_pref.close() ml_pref.close()
ml_native.write('module ML2C = struct\n\n') ml_native.write('\n')
for name, result, params in _dotnet_decls: for name, result, params in _dotnet_decls:
ml_native.write(' external n_%s : ' % ml_method_name(name)) ml_native.write('external %s : ' % ml_method_name(name))
ip = inparams(params) ip = inparams(params)
op = outparams(params) op = outparams(params)
if len(ip) == 0: if len(ip) == 0:
@ -1231,46 +1231,11 @@ def mk_ml(ml_dir):
ml_native.write('%s' % param2ml(p)) ml_native.write('%s' % param2ml(p))
if len(op) > 0: if len(op) > 0:
ml_native.write(')') ml_native.write(')')
ml_native.write('\n')
if len(ip) > 5: if len(ip) > 5:
ml_native.write(' = "n_%s_bytecode"\n' % ml_method_name(name)) ml_native.write(' = "n_%s_bytecode" "n_%s"\n' % (ml_method_name(name), ml_method_name(name)))
ml_native.write(' "n_%s"\n' % ml_method_name(name))
else: else:
ml_native.write(' = "n_%s"\n' % ml_method_name(name)) ml_native.write(' = "n_%s"\n' % ml_method_name(name))
ml_native.write('\n') ml_native.write('\n')
ml_native.write(' end\n\n')
# Exception wrappers
for name, result, params in _dotnet_decls:
ip = inparams(params)
op = outparams(params)
ml_native.write(' let %s ' % ml_method_name(name))
first = True
i = 0
for p in params:
if is_in_param(p):
if first:
first = False
else:
ml_native.write(' ')
ml_native.write('a%d' % i)
i = i + 1
if len(ip) == 0:
ml_native.write('()')
ml_native.write(' = ')
ml_native.write('ML2C.n_%s' % (ml_method_name(name)))
if len(ip) == 0:
ml_native.write(' ()')
first = True
i = 0
for p in params:
if is_in_param(p):
ml_native.write(' a%d' % i)
i = i + 1
ml_native.write('\n')
ml_native.write('\n')
# null pointer helpers # null pointer helpers
for type_id in Type2Str: for type_id in Type2Str:

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

File diff suppressed because it is too large Load diff

3
src/api/ml/z3.mli
View file

@ -3432,6 +3432,3 @@ val enable_trace : string -> unit
Remarks: It is a NOOP otherwise. Remarks: It is a NOOP otherwise.
*) *)
val disable_trace : string -> unit val disable_trace : string -> unit

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

@ -63,6 +63,14 @@ static struct custom_operations default_custom_ops = {
custom_compare_ext_default, custom_compare_ext_default,
}; };
inline int compare_pointers(void* pt1, void* pt2) {
if (pt1 == pt2)
return 0;
else if ((intnat)pt1 < (intnat)pt2)
return -1;
else
return +1;
}
#define MK_CTX_OF(X) \ #define MK_CTX_OF(X) \
CAMLprim DLL_PUBLIC value n_context_of_ ## X(value v) { \ CAMLprim DLL_PUBLIC value n_context_of_ ## X(value v) { \
@ -150,14 +158,38 @@ void Z3_context_finalize(value v) {
try_to_delete_context(cp); try_to_delete_context(cp);
} }
int Z3_context_compare(value v1, value v2) {
/* As each context created within the OCaml bindings has a unique
Z3_context_plus_data allocated to store the handle and the ref counters,
we can just compare pointers here. This suffices to test for (in)equality
and induces an arbitrary (but fixed) ordering. */
Z3_context_plus cp1 = *(Z3_context_plus*)Data_custom_val(v1);
Z3_context_plus cp2 = *(Z3_context_plus*)Data_custom_val(v2);
return compare_pointers(cp1, cp2);
}
int Z3_context_compare_ext(value v1, value v2) {
Z3_context_plus cp = *(Z3_context_plus*)Data_custom_val(v1);
return compare_pointers(cp, (void*)Val_int(v2));
}
/* We use the pointer to the Z3_context_plus_data structure as
a hash value; it is unique, at least. */
intnat Z3_context_hash(value v) {
/* We use the address of the context's Z3_context_plus_data structure
as a hash value */
Z3_context_plus cp = *(Z3_context_plus*)Data_custom_val(v);
return (intnat)cp;
}
static struct custom_operations Z3_context_plus_custom_ops = { static struct custom_operations Z3_context_plus_custom_ops = {
(char*) "Z3_context ops", (char*) "Z3_context ops",
Z3_context_finalize, Z3_context_finalize,
custom_compare_default, Z3_context_compare,
custom_hash_default, Z3_context_hash,
custom_serialize_default, custom_serialize_default,
custom_deserialize_default, custom_deserialize_default,
custom_compare_ext_default, Z3_context_compare_ext
}; };
@ -195,13 +227,21 @@ void Z3_ast_finalize(value v) {
int Z3_ast_compare(value v1, value v2) { 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);
/* if the two ASTs belong to different contexts, we take
their contexts' addresses to order them (arbitrarily, but fixed) */
if (a1->cp->ctx != a2->cp->ctx)
return compare_pointers(a1->cp->ctx, a2->cp->ctx);
/* handling of NULL pointers */
if (a1->p == NULL && a2->p == NULL) if (a1->p == NULL && a2->p == NULL)
return 0; return 0;
if (a1->p == NULL) if (a1->p == NULL)
return -1; return -1;
if (a2->p == NULL) if (a2->p == NULL)
return +1; return +1;
/* Comparison according to AST ids. */
unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->p); unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->p);
unsigned id2 = Z3_get_ast_id(a2->cp->ctx, a2->p); unsigned id2 = Z3_get_ast_id(a2->cp->ctx, a2->p);
if (id1 == id2) if (id1 == id2)
@ -275,14 +315,33 @@ MK_CTX_OF(ast)
try_to_delete_context(pp->cp); \ try_to_delete_context(pp->cp); \
} \ } \
\ \
int Z3_ ## X ## _compare(value v1, value v2) { \
Z3_ ## X ## _plus * pp1 = (Z3_ ## X ## _plus*)Data_custom_val(v1); \
Z3_ ## X ## _plus * pp2 = (Z3_ ## X ## _plus*)Data_custom_val(v2); \
if (pp1->cp != pp2->cp) \
return compare_pointers(pp1->cp, pp2->cp); \
else \
return compare_pointers(pp1->p, pp2->p); \
} \
\
intnat Z3_ ## X ## _hash(value v) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
return (intnat)pp->p; \
} \
\
int Z3_ ## X ## _compare_ext(value v1, value v2) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v1); \
return compare_pointers(pp->p, (void*)Val_int(v2)); \
} \
\
static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \ static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \
(char*) "Z3_" #X " ops", \ (char*) "Z3_" #X " ops", \
Z3_ ## X ## _finalize, \ Z3_ ## X ## _finalize, \
custom_compare_default, \ Z3_ ## X ## _compare, \
custom_hash_default, \ Z3_ ## X ## _hash, \
custom_serialize_default, \ custom_serialize_default, \
custom_deserialize_default, \ custom_deserialize_default, \
custom_compare_ext_default, \ Z3_ ## X ## _compare_ext \
}; \ }; \
\ \
MK_CTX_OF(X) MK_CTX_OF(X)
@ -315,14 +374,33 @@ MK_CTX_OF(ast)
try_to_delete_context(pp->cp); \ try_to_delete_context(pp->cp); \
} \ } \
\ \
int Z3_ ## X ## _compare(value v1, value v2) { \
Z3_ ## X ## _plus * pp1 = (Z3_ ## X ## _plus*)Data_custom_val(v1); \
Z3_ ## X ## _plus * pp2 = (Z3_ ## X ## _plus*)Data_custom_val(v2); \
if (pp1->cp != pp2->cp) \
return compare_pointers(pp1->cp, pp2->cp); \
else \
return compare_pointers(pp1->p, pp2->p); \
} \
\
intnat Z3_ ## X ## _hash(value v) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
return (intnat)pp->p; \
} \
\
int Z3_ ## X ## _compare_ext(value v1, value v2) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v1); \
return compare_pointers(pp->p, (void*)Val_int(v2)); \
} \
\
static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \ static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \
(char*) "Z3_" #X " ops", \ (char*) "Z3_" #X " ops", \
Z3_ ## X ## _finalize, \ Z3_ ## X ## _finalize, \
custom_compare_default, \ Z3_ ## X ## _compare, \
custom_hash_default, \ Z3_ ## X ## _hash, \
custom_serialize_default, \ custom_serialize_default, \
custom_deserialize_default, \ custom_deserialize_default, \
custom_compare_ext_default, \ Z3_ ## X ## _compare_ext \
}; \ }; \
\ \
MK_CTX_OF(X) MK_CTX_OF(X)
@ -347,7 +425,6 @@ MK_PLUS_OBJ(ast_vector)
MK_PLUS_OBJ(fixedpoint) MK_PLUS_OBJ(fixedpoint)
MK_PLUS_OBJ(optimize) MK_PLUS_OBJ(optimize)
#ifdef __cplusplus #ifdef __cplusplus
extern "C" { extern "C" {
#endif #endif