mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

Build system bugfixes.

Browse source 
Partially fixes #27
This commit is contained in:
Christoph M. Wintersteiger 2015-04-08 12:09:14 +01:00
parent ba066ff899
commit 03020b9f96
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
scripts/mk_util.py
View file

@ -2810,19 +2810,19 @@ 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.iteritems():
for k, i in decls.items():
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.iteritems():
for k, i in decls.items():
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.iteritems():
for k, i in decls.items():
efile.write(' | %d -> %s\n' % (i, k[3:]))
# use Z3.Exception?
efile.write(' | _ -> raise (Failure "undefined enum value")\n\n')
@ -2888,7 +2888,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.iteritems():
for k, i in decls.items():
efile.write(' | %s \n' % k[3:]) # strip Z3_
efile.write('\n')
efile.write('(** Convert %s to int*)\n' % name[3:])

2
scripts/update_api.py
View file

@ -1169,7 +1169,7 @@ def mk_ml():
ml_i.write('type ptr\n')
ml_native.write('and z3_symbol = ptr\n')
ml_i.write('and z3_symbol = ptr\n')
for k, v in Type2Str.iteritems():
for k, v in Type2Str.items():
if is_obj(k):
ml_native.write('and %s = ptr\n' % v.lower())
ml_i.write('and %s = ptr\n' % v.lower())