From ef3dd32364da96a52e1d61ab9415dd366344ec60 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 4 Jan 2022 20:21:53 -0800 Subject: [PATCH] some cleanup Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 26 ++------------- scripts/update_api.py | 76 +++++-------------------------------------- 2 files changed, 11 insertions(+), 91 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index b73e1b329..042e6af46 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -92,7 +92,6 @@ DOTNET_CORE_ENABLED=False DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None) JAVA_ENABLED=False ML_ENABLED=False -JS_ENABLED=False PYTHON_INSTALL_ENABLED=False STATIC_LIB=False STATIC_BIN=False @@ -681,7 +680,7 @@ def display_help(exit_code): # Parse configuration option for mk_make script def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM - global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, JS_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED + global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC, SINGLE_THREADED global GUARD_CF, ALWAYS_DYNAMIC_BASE try: @@ -749,8 +748,6 @@ def parse_options(): GIT_DESCRIBE = True elif opt in ('', '--ml'): ML_ENABLED = True - elif opt == "--js": - JS_ENABLED = True elif opt in ('', '--log-sync'): LOG_SYNC = True elif opt == '--single-threaded': @@ -813,16 +810,6 @@ def set_build_dir(d): BUILD_DIR = norm_path(d) REV_BUILD_DIR = reverse_path(d) -def set_z3js_dir(p): - global SRC_DIR, Z3JS_SRC_DIR - p = norm_path(p) - full = os.path.join(SRC_DIR, p) - if not os.path.exists(full): - raise MKException("Python bindings directory '%s' does not exist" % full) - Z3JS_SRC_DIR = full - if VERBOSE: - print("Js bindings directory was detected.") - def set_z3py_dir(p): global SRC_DIR, Z3PY_SRC_DIR p = norm_path(p) @@ -858,9 +845,6 @@ def get_components(): def get_z3py_dir(): return Z3PY_SRC_DIR -# Return directory where the js bindings are located -def get_z3js_dir(): - return Z3JS_SRC_DIR # Return true if in verbose mode def is_verbose(): @@ -872,9 +856,6 @@ def is_java_enabled(): def is_ml_enabled(): return ML_ENABLED -def is_js_enabled(): - return JS_ENABLED - def is_dotnet_core_enabled(): return DOTNET_CORE_ENABLED @@ -3025,17 +3006,14 @@ def mk_bindings(api_files): ml_output_dir = None if is_ml_enabled(): ml_output_dir = get_component('ml').src_dir - if is_js_enabled(): - set_z3js_dir("api/js") - js_output_dir = get_component('js').src_dir # Get the update_api module to do the work for us + update_api.VERBOSE = is_verbose() update_api.generate_files(api_files=new_api_files, api_output_dir=get_component('api').src_dir, z3py_output_dir=get_z3py_dir(), dotnet_output_dir=dotnet_output_dir, java_output_dir=java_output_dir, java_package_name=java_package_name, - js_output_dir=get_z3js_dir(), ml_output_dir=ml_output_dir, ml_src_dir=ml_output_dir ) diff --git a/scripts/update_api.py b/scripts/update_api.py index 6392e439e..c4e4d78f0 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -15,7 +15,6 @@ several API header files. It can also optionally emit some of the files required for Z3's different language bindings. """ -import mk_util import mk_exception import argparse import logging @@ -23,6 +22,10 @@ import re import os import sys +VERBOSE = True +def is_verbose(): + return VERBOSE + ########################################################## # TODO: rewrite this file without using global variables. # This file is a big HACK. @@ -776,62 +779,9 @@ def mk_java(java_dir, package_name): java_wrapper.write('#ifdef __cplusplus\n') java_wrapper.write('}\n') java_wrapper.write('#endif\n') - if mk_util.is_verbose(): + if is_verbose(): print("Generated '%s'" % java_nativef) - -Type2Napi = { VOID : '', VOID_PTR : '', INT : 'number', UINT : 'number', INT64 : 'number', UINT64 : 'number', DOUBLE : 'number', - FLOAT : 'number', STRING : 'string', STRING_PTR : 'array', - BOOL : 'number', SYMBOL : 'external', PRINT_MODE : 'number', ERROR_CODE : 'number', CHAR : 'number' } - -def type2napi(t): - try: - return Type2Napi[t] - except: - return "external" - -Type2NapiBuilder = { VOID : '', VOID_PTR : '', INT : 'int32', UINT : 'uint32', INT64 : 'int64', UINT64 : 'uint64', DOUBLE : 'double', - FLOAT : 'float', STRING : 'string', STRING_PTR : 'array', - BOOL : 'bool', SYMBOL : 'external', PRINT_MODE : 'int32', ERROR_CODE : 'int32', CHAR : 'char' } - -def type2napibuilder(t): - try: - return Type2NapiBuilder[t] - except: - return "external" - - -def mk_js(js_output_dir): - with open(os.path.join(js_output_dir, "z3.json"), 'w') as ous: - ous.write("{\n") - ous.write(" \"api\": [\n") - for name, result, params in _dotnet_decls: - ous.write(" {\n") - ous.write(" \"name\": \"%s\",\n" % name) - ous.write(" \"c_type\": \"%s\",\n" % Type2Str[result]) - ous.write(" \"napi_type\": \"%s\",\n" % type2napi(result)) - ous.write(" \"arg_list\": [") - first = True - for p in params: - if first: - first = False - ous.write("\n {\n") - else: - ous.write(",\n {\n") - t = param_type(p) - k = t - ous.write(" \"name\": \"%s\",\n" % "") # TBD - ous.write(" \"c_type\": \"%s\",\n" % type2str(t)) - ous.write(" \"napi_type\": \"%s\",\n" % type2napi(t)) - ous.write(" \"napi_builder\": \"%s\"\n" % type2napibuilder(t)) - ous.write( " }") - ous.write("],\n") - ous.write(" \"napi_builder\": \"%s\"\n" % type2napibuilder(result)) - ous.write(" },\n") - ous.write(" ]\n") - ous.write("}\n") - - def mk_log_header(file, name, params): file.write("void log_%s(" % name) i = 0 @@ -1364,7 +1314,7 @@ def mk_ml(ml_src_dir, ml_output_dir): ml_native.write('(**/**)\n') ml_native.close() - if mk_util.is_verbose(): + if is_verbose(): print ('Generated "%s"' % ml_nativef) mk_z3native_stubs_c(ml_src_dir, ml_output_dir) @@ -1689,7 +1639,7 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface ml_wrapper.write('}\n') ml_wrapper.write('#endif\n') - if mk_util.is_verbose(): + if is_verbose(): print ('Generated "%s"' % ml_wrapperf) # Collect API(...) commands from @@ -1889,7 +1839,6 @@ def generate_files(api_files, dotnet_output_dir=None, java_output_dir=None, java_package_name=None, - js_output_dir=None, ml_output_dir=None, ml_src_dir=None): """ @@ -1950,7 +1899,7 @@ def generate_files(api_files, mk_py_wrappers() write_core_py_post(core_py) - if mk_util.is_verbose(): + if is_verbose(): print("Generated '{}'".format(log_h.name)) print("Generated '{}'".format(log_c.name)) print("Generated '{}'".format(exe_c.name)) @@ -1960,7 +1909,7 @@ def generate_files(api_files, with open(os.path.join(dotnet_output_dir, 'Native.cs'), 'w') as dotnet_file: mk_dotnet(dotnet_file) mk_dotnet_wrappers(dotnet_file) - if mk_util.is_verbose(): + if is_verbose(): print("Generated '{}'".format(dotnet_file.name)) if java_output_dir: @@ -1970,8 +1919,6 @@ def generate_files(api_files, assert not ml_src_dir is None mk_ml(ml_src_dir, ml_output_dir) - if js_output_dir: - mk_js(js_output_dir) def main(args): logging.basicConfig(level=logging.INFO) @@ -2006,10 +1953,6 @@ def main(args): dest="ml_output_dir", default=None, help="Directory to emit OCaml files. If not specified no files are emitted.") - parser.add_argument("--js_output_dir", - dest="js_output_dir", - default=None, - help="Directory to emit js bindings. If not specified no files are emitted.") pargs = parser.parse_args(args) if pargs.java_output_dir: @@ -2033,7 +1976,6 @@ def main(args): dotnet_output_dir=pargs.dotnet_output_dir, java_output_dir=pargs.java_output_dir, java_package_name=pargs.java_package_name, - js_output_dir=pargs.js_output_dir, ml_output_dir=pargs.ml_output_dir, ml_src_dir=pargs.ml_src_dir) return 0