mirror of
https://github.com/Z3Prover/z3
synced 2025-06-04 05:11:21 +00:00
Avoid using physical equality checks in OCaml bindings (z3.ml)
This patch avoids the use of physical equality wherever possible and improves some details of the OCaml implementation.
This commit is contained in:
martin-neuhaeusser
parent
f133f478c8
commit
71f991c5df
3 changed files with 1192 additions and 1171 deletions
1256
src/api/ml/z3.ml
1256
src/api/ml/z3.ml
File diff suppressed because it is too large
Load diff
|
|
@ -139,7 +139,7 @@ sig
|
|||
val get_size : ast_vector -> int
|
||||
|
||||
(** Retrieves the i-th object in the vector.
|
||||
@return An AST *)
|
||||
@return An AST *)
|
||||
val get : ast_vector -> int -> ast
|
||||
|
||||
(** Sets the i-th object in the vector. *)
|
||||
|
|
@ -149,11 +149,11 @@ sig
|
|||
val resize : ast_vector -> int -> unit
|
||||
|
||||
(** Add an ast to the back of the vector. The size
|
||||
is increased by 1. *)
|
||||
is increased by 1. *)
|
||||
val push : ast_vector -> ast -> unit
|
||||
|
||||
(** Translates all ASTs in the vector to another context.
|
||||
@return A new ASTVector *)
|
||||
@return A new ASTVector *)
|
||||
val translate : ast_vector -> context -> ast_vector
|
||||
|
||||
(** Translates the ASTVector into an (Ast.ast list) *)
|
||||
|
|
@ -175,11 +175,11 @@ sig
|
|||
val mk_ast_map : context -> ast_map
|
||||
|
||||
(** Checks whether the map contains a key.
|
||||
@return True if the key in the map, false otherwise. *)
|
||||
@return True if the key in the map, false otherwise. *)
|
||||
val contains : ast_map -> ast -> bool
|
||||
|
||||
(** Finds the value associated with the key.
|
||||
This function signs an error when the key is not a key in the map. *)
|
||||
This function signs an error when the key is not a key in the map. *)
|
||||
val find : ast_map -> ast -> ast
|
||||
|
||||
(** Stores or replaces a new key/value pair in the map. *)
|
||||
|
|
@ -285,7 +285,7 @@ sig
|
|||
sig
|
||||
(** Parameters of func_decls *)
|
||||
type parameter =
|
||||
P_Int of int
|
||||
P_Int of int
|
||||
| P_Dbl of float
|
||||
| P_Sym of Symbol.symbol
|
||||
| P_Srt of Sort.sort
|
||||
|
|
@ -3432,6 +3432,3 @@ val enable_trace : string -> unit
|
|||
Remarks: It is a NOOP otherwise.
|
||||
*)
|
||||
val disable_trace : string -> unit
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -63,6 +63,14 @@ static struct custom_operations default_custom_ops = {
|
|||
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) \
|
||||
CAMLprim DLL_PUBLIC value n_context_of_ ## X(value v) { \
|
||||
|
|
@ -150,14 +158,32 @@ void Z3_context_finalize(value v) {
|
|||
try_to_delete_context(cp);
|
||||
}
|
||||
|
||||
int Z3_context_compare(value v1, value v2) {
|
||||
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) {
|
||||
Z3_context_plus cp = *(Z3_context_plus*)Data_custom_val(v);
|
||||
return (intnat)cp;
|
||||
}
|
||||
|
||||
static struct custom_operations Z3_context_plus_custom_ops = {
|
||||
(char*) "Z3_context ops",
|
||||
Z3_context_finalize,
|
||||
custom_compare_default,
|
||||
custom_hash_default,
|
||||
Z3_context_compare,
|
||||
Z3_context_hash,
|
||||
custom_serialize_default,
|
||||
custom_deserialize_default,
|
||||
custom_compare_ext_default,
|
||||
Z3_context_compare_ext
|
||||
};
|
||||
|
||||
|
||||
|
|
@ -195,13 +221,21 @@ void Z3_ast_finalize(value v) {
|
|||
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);
|
||||
|
||||
/* 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)
|
||||
return 0;
|
||||
if (a1->p == NULL)
|
||||
return -1;
|
||||
if (a2->p == NULL)
|
||||
return +1;
|
||||
|
||||
/* Comparison according to AST ids. */
|
||||
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)
|
||||
|
|
@ -275,14 +309,33 @@ MK_CTX_OF(ast)
|
|||
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 = { \
|
||||
(char*) "Z3_" #X " ops", \
|
||||
Z3_ ## X ## _finalize, \
|
||||
custom_compare_default, \
|
||||
custom_hash_default, \
|
||||
Z3_ ## X ## _compare, \
|
||||
Z3_ ## X ## _hash, \
|
||||
custom_serialize_default, \
|
||||
custom_deserialize_default, \
|
||||
custom_compare_ext_default, \
|
||||
Z3_ ## X ## _compare_ext \
|
||||
}; \
|
||||
\
|
||||
MK_CTX_OF(X)
|
||||
|
|
@ -315,14 +368,33 @@ MK_CTX_OF(ast)
|
|||
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 = { \
|
||||
(char*) "Z3_" #X " ops", \
|
||||
Z3_ ## X ## _finalize, \
|
||||
custom_compare_default, \
|
||||
custom_hash_default, \
|
||||
Z3_ ## X ## _compare, \
|
||||
Z3_ ## X ## _hash, \
|
||||
custom_serialize_default, \
|
||||
custom_deserialize_default, \
|
||||
custom_compare_ext_default, \
|
||||
Z3_ ## X ## _compare_ext \
|
||||
}; \
|
||||
\
|
||||
MK_CTX_OF(X)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue