mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

Refactor `mk_z3consts_py()` to that is usable externally via a new

Browse source 
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.
This commit is contained in:
Dan Liew 2016-03-02 11:59:48 +00:00
parent f6e946443e
commit 8bc7d319c7
2 changed files with 60 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

20
scripts/mk_util.py
View file

@ -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