mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 05:19:11 +00:00
some cleanup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
d1fb831030
commit
ef3dd32364
2 changed files with 11 additions and 91 deletions
|
|
@ -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
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue