mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

Fix inconsistent emission of OCaml enumeration files. The ordering of emitted

Browse source 
enum values is not consistent between python 2 or 3. The root cause
of the problem was a dictionary's keys being iterated over which has
no defined order.

This has been fixed by iterating over the dictionary's items and
ordering by values.  We could order by key rather than the values but
seeing as these represent an enum, ordering by value makes more sense.
This commit is contained in:
Dan Liew 2016-11-21 00:05:59 +00:00
parent 251d1ec031
commit 0e03fe9bf2
1 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
scripts/mk_util.py
View file

@ -2986,21 +2986,22 @@ def mk_z3consts_ml(api_files):
if m:
name = words[1]
if name not in DeprecatedEnums:
sorted_decls = sorted(decls.items(), key=lambda pair: pair[1])
efile.write('(** %s *)\n' % name[3:])
efile.write('type %s =\n' % name[3:]) # strip Z3_
for k, i in decls.items():
for k, i in sorted_decls:
efile.write(' | %s \n' % k[3:]) # strip Z3_
efile.write('\n')
efile.write('(** Convert %s to int*)\n' % name[3:])
efile.write('let int_of_%s x : int =\n' % (name[3:])) # strip Z3_
efile.write(' match x with\n')
for k, i in decls.items():
for k, i in sorted_decls:
efile.write(' | %s -> %d\n' % (k[3:], i))
efile.write('\n')
efile.write('(** Convert int to %s*)\n' % name[3:])
efile.write('let %s_of_int x : %s =\n' % (name[3:],name[3:])) # strip Z3_
efile.write(' match x with\n')
for k, i in decls.items():
for k, i in sorted_decls:
efile.write(' | %d -> %s\n' % (i, k[3:]))
# use Z3.Exception?
efile.write(' | _ -> raise (Failure "undefined enum value")\n\n')
@ -3068,7 +3069,7 @@ def mk_z3consts_ml(api_files):
# if name not in DeprecatedEnums:
# efile.write('(** %s *)\n' % name[3:])
# efile.write('type %s =\n' % name[3:]) # strip Z3_
# for k, i in decls.items():
# for k, i in sorted(decls.items(), key=lambda pair: pair[1]):
# efile.write(' | %s \n' % k[3:]) # strip Z3_
# efile.write('\n')
# efile.write('(** Convert %s to int*)\n' % name[3:])