mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

Add more comments on comparison functions in the C layer of the OCaml bindings

Browse source
This commit is contained in:
martin-neuhaeusser 2016-04-06 12:36:11 +02:00
parent b873c6b508
commit 1662ba8353
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -159,6 +159,10 @@ void Z3_context_finalize(value v) {
}
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);
@ -172,6 +176,8 @@ int Z3_context_compare_ext(value v1, value 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;
}