Skip to content

Commit

Permalink
Refactor mk_z3consts_py() to that is usable externally via a new
Browse files Browse the repository at this point in the history
function ``mk_z3consts_py_internal()`` which called by a new
``mk_consts_files.py`` script. This will script will allow the const
declarations for the different Z3 language bindings to be generated.
Right now only support for python is implemented but more can be added
in the future.
  • Loading branch information
Dan Liew committed Mar 4, 2016
1 parent f6e9464 commit 8bc7d31
Show file tree
Hide file tree
Showing 2 changed files with 60 additions and 7 deletions.
47 changes: 47 additions & 0 deletions scripts/mk_consts_files.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,47 @@
#!/usr/bin/env python
"""
Reads a list of Z3 API header files and
generate the constant declarations need
by one or more Z3 language bindings
"""
import mk_util
import argparse
import logging
import os
import sys

def check_dir(output_dir):
if not os.path.isdir(output_dir):
logging.error('"{}" is not an existing directory'.format(output_dir))
return 1
return 0

def main(args):
logging.basicConfig(level=logging.INFO)
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("api_files", nargs="+")
parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None)
pargs = parser.parse_args(args)

for api_file in pargs.api_files:
if not os.path.exists(api_file):
logging.error('"{}" does not exist'.format(api_file))
return 1

count = 0

if pargs.z3py_output_dir:
if check_dir(pargs.z3py_output_dir) != 0:
return 1
mk_util.mk_z3consts_py_internal(pargs.api_files, pargs.z3py_output_dir)
count += 1

if count == 0:
logging.info('No files generated. You need to specific an output directory'
' for the relevant langauge bindings')
# TODO: Add support for other bindings
return 0

if __name__ == '__main__':
sys.exit(main(sys.argv[1:]))

20 changes: 13 additions & 7 deletions scripts/mk_util.py
Original file line number Diff line number Diff line change
Expand Up @@ -2999,6 +2999,17 @@ def mk_bindings(api_files):
def mk_z3consts_py(api_files):
if Z3PY_SRC_DIR is None:
raise MKException("You must invoke set_z3py_dir(path):")
full_path_api_files = []
api_dll = get_component(Z3_DLL_COMPONENT)
for api_file in api_files:
api_file_c = api_dll.find_file(api_file, api_dll.name)
api_file = os.path.join(api_file_c.src_dir, api_file)
full_path_api_files.append(api_file)
mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR)

def mk_z3consts_py_internal(api_files, output_dir):
assert os.path.isdir(output_dir)
assert isinstance(api_files, list)

blank_pat = re.compile("^ *\r?$")
comment_pat = re.compile("^ *//.*$")
Expand All @@ -3007,14 +3018,9 @@ def mk_z3consts_py(api_files):
openbrace_pat = re.compile("{ *")
closebrace_pat = re.compile("}.*;")

z3consts = open(os.path.join(Z3PY_SRC_DIR, 'z3consts.py'), 'w')
z3consts = open(os.path.join(output_dir, 'z3consts.py'), 'w')
z3consts.write('# Automatically generated file\n\n')

api_dll = get_component(Z3_DLL_COMPONENT)

for api_file in api_files:
api_file_c = api_dll.find_file(api_file, api_dll.name)
api_file = os.path.join(api_file_c.src_dir, api_file)
api = open(api_file, 'r')

SEARCHING = 0
Expand Down Expand Up @@ -3075,7 +3081,7 @@ def mk_z3consts_py(api_files):
api.close()
z3consts.close()
if VERBOSE:
print("Generated '%s'" % os.path.join(Z3PY_SRC_DIR, 'z3consts.py'))
print("Generated '%s'" % os.path.join(output_dir, 'z3consts.py'))


# Extract enumeration types from z3_api.h, and add .Net definitions
Expand Down

0 comments on commit 8bc7d31

Please sign in to comment.