diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py new file mode 100755 index 000000000..543c56e0e --- /dev/null +++ b/scripts/mk_consts_files.py @@ -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:])) + diff --git a/scripts/mk_util.py b/scripts/mk_util.py index f7a51b4da..56726b1cc 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -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("^ *//.*$") @@ -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 @@ -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