mirror of
https://github.com/Z3Prover/z3
synced 2025-06-06 14:13:23 +00:00
Merge branch 'cmake_build_system4' of https://github.com/delcypher/z3-1 into delcypher-cmake_build_system4
This commit is contained in:
Christoph M. Wintersteiger
commit
a9ffc258d0
102 changed files with 3880 additions and 189 deletions
|
|
@ -2504,10 +2504,10 @@ DOUBLE = 2
|
|||
STRING = 3
|
||||
SYMBOL = 4
|
||||
UINT_MAX = 4294967295
|
||||
CURR_PYG = None
|
||||
CURRENT_PYG_HPP_DEST_DIR = None
|
||||
|
||||
def get_curr_pyg():
|
||||
return CURR_PYG
|
||||
def get_current_pyg_hpp_dest_dir():
|
||||
return CURRENT_PYG_HPP_DEST_DIR
|
||||
|
||||
TYPE2CPK = { UINT : 'CPK_UINT', BOOL : 'CPK_BOOL', DOUBLE : 'CPK_DOUBLE', STRING : 'CPK_STRING', SYMBOL : 'CPK_SYMBOL' }
|
||||
TYPE2CTYPE = { UINT : 'unsigned', BOOL : 'bool', DOUBLE : 'double', STRING : 'char const *', SYMBOL : 'symbol' }
|
||||
|
|
@ -2540,8 +2540,8 @@ def to_c_method(s):
|
|||
return s.replace('.', '_')
|
||||
|
||||
def def_module_params(module_name, export, params, class_name=None, description=None):
|
||||
pyg = get_curr_pyg()
|
||||
dirname = os.path.split(get_curr_pyg())[0]
|
||||
dirname = get_current_pyg_hpp_dest_dir()
|
||||
assert(os.path.exists(dirname))
|
||||
if class_name is None:
|
||||
class_name = '%s_params' % module_name
|
||||
hpp = os.path.join(dirname, '%s.hpp' % class_name)
|
||||
|
|
@ -2606,28 +2606,31 @@ def _execfile(file, globals=globals(), locals=locals()):
|
|||
|
||||
# Execute python auxiliary scripts that generate extra code for Z3.
|
||||
def exec_pyg_scripts():
|
||||
global CURR_PYG
|
||||
global CURRENT_PYG_HPP_DEST_DIR
|
||||
for root, dirs, files in os.walk('src'):
|
||||
for f in files:
|
||||
if f.endswith('.pyg'):
|
||||
script = os.path.join(root, f)
|
||||
CURR_PYG = script
|
||||
CURRENT_PYG_HPP_DEST_DIR = root
|
||||
_execfile(script, PYG_GLOBALS)
|
||||
|
||||
# TODO: delete after src/ast/pattern/expr_pattern_match
|
||||
# database.smt ==> database.h
|
||||
def mk_pat_db():
|
||||
c = get_component(PATTERN_COMPONENT)
|
||||
fin = open(os.path.join(c.src_dir, 'database.smt2'), 'r')
|
||||
fout = open(os.path.join(c.src_dir, 'database.h'), 'w')
|
||||
fout.write('static char const g_pattern_database[] =\n')
|
||||
for line in fin:
|
||||
fout.write('"%s\\n"\n' % line.strip('\n'))
|
||||
fout.write(';\n')
|
||||
fin.close()
|
||||
fout.close()
|
||||
fin = os.path.join(c.src_dir, 'database.smt2')
|
||||
fout = os.path.join(c.src_dir, 'database.h')
|
||||
mk_pat_db_internal(fin, fout)
|
||||
|
||||
def mk_pat_db_internal(inputFilePath, outputFilePath):
|
||||
with open(inputFilePath, 'r') as fin:
|
||||
with open(outputFilePath, 'w') as fout:
|
||||
fout.write('static char const g_pattern_database[] =\n')
|
||||
for line in fin:
|
||||
fout.write('"%s\\n"\n' % line.strip('\n'))
|
||||
fout.write(';\n')
|
||||
if VERBOSE:
|
||||
print("Generated '%s'" % os.path.join(c.src_dir, 'database.h'))
|
||||
print("Generated '%s'" % outputFilePath)
|
||||
|
||||
# Update version numbers
|
||||
def update_version():
|
||||
|
|
@ -2645,15 +2648,20 @@ def update_version():
|
|||
# Update files with the version number
|
||||
def mk_version_dot_h(major, minor, build, revision):
|
||||
c = get_component(UTIL_COMPONENT)
|
||||
fout = open(os.path.join(c.src_dir, 'version.h'), 'w')
|
||||
fout.write('// automatically generated file.\n')
|
||||
fout.write('#define Z3_MAJOR_VERSION %s\n' % major)
|
||||
fout.write('#define Z3_MINOR_VERSION %s\n' % minor)
|
||||
fout.write('#define Z3_BUILD_NUMBER %s\n' % build)
|
||||
fout.write('#define Z3_REVISION_NUMBER %s\n' % revision)
|
||||
fout.close()
|
||||
version_template = os.path.join(c.src_dir, 'version.h.in')
|
||||
version_header_output = os.path.join(c.src_dir, 'version.h')
|
||||
# Note the substitution names are what is used by the CMake
|
||||
# builds system. If you change these you should change them
|
||||
# in the CMake build too
|
||||
configure_file(version_template, version_header_output,
|
||||
{ 'Z3_VERSION_MAJOR': str(major),
|
||||
'Z3_VERSION_MINOR': str(minor),
|
||||
'Z3_VERSION_PATCH': str(build),
|
||||
'Z3_VERSION_TWEAK': str(revision),
|
||||
}
|
||||
)
|
||||
if VERBOSE:
|
||||
print("Generated '%s'" % os.path.join(c.src_dir, 'version.h'))
|
||||
print("Generated '%s'" % version_header_output)
|
||||
|
||||
# Generate AssemblyInfo.cs files with the right version numbers by using ``AssemblyInfo.cs.in`` files as a template
|
||||
def mk_all_assembly_infos(major, minor, build, revision):
|
||||
|
|
@ -2690,6 +2698,13 @@ def ADD_PROBE(name, descr, cmd):
|
|||
# It installs all tactics in the given component (name) list cnames
|
||||
# The procedure looks for ADD_TACTIC commands in the .h files of these components.
|
||||
def mk_install_tactic_cpp(cnames, path):
|
||||
component_src_dirs = []
|
||||
for cname in cnames:
|
||||
c = get_component(cname)
|
||||
component_src_dirs.append(c.src_dir)
|
||||
mk_install_tactic_cpp_internal(component_src_dirs, path)
|
||||
|
||||
def mk_install_tactic_cpp_internal(component_src_dirs, path):
|
||||
global ADD_TACTIC_DATA, ADD_PROBE_DATA
|
||||
ADD_TACTIC_DATA = []
|
||||
ADD_PROBE_DATA = []
|
||||
|
|
@ -2701,12 +2716,11 @@ def mk_install_tactic_cpp(cnames, path):
|
|||
fout.write('#include"cmd_context.h"\n')
|
||||
tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)')
|
||||
probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)')
|
||||
for cname in cnames:
|
||||
c = get_component(cname)
|
||||
h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(c.src_dir))
|
||||
for component_src_dir in component_src_dirs:
|
||||
h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
|
||||
for h_file in h_files:
|
||||
added_include = False
|
||||
fin = open(os.path.join(c.src_dir, h_file), 'r')
|
||||
fin = open(os.path.join(component_src_dir, h_file), 'r')
|
||||
for line in fin:
|
||||
if tactic_pat.match(line):
|
||||
if not added_include:
|
||||
|
|
@ -2759,6 +2773,13 @@ def mk_all_install_tactic_cpps():
|
|||
# void mem_finalize()
|
||||
# These procedures are invoked by the Z3 memory_manager
|
||||
def mk_mem_initializer_cpp(cnames, path):
|
||||
component_src_dirs = []
|
||||
for cname in cnames:
|
||||
c = get_component(cname)
|
||||
component_src_dirs.append(c.src_dir)
|
||||
mk_mem_initializer_cpp_internal(component_src_dirs, path)
|
||||
|
||||
def mk_mem_initializer_cpp_internal(component_src_dirs, path):
|
||||
initializer_cmds = []
|
||||
finalizer_cmds = []
|
||||
fullname = os.path.join(path, 'mem_initializer.cpp')
|
||||
|
|
@ -2768,12 +2789,11 @@ def mk_mem_initializer_cpp(cnames, path):
|
|||
# ADD_INITIALIZER with priority
|
||||
initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)')
|
||||
finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
|
||||
for cname in cnames:
|
||||
c = get_component(cname)
|
||||
h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(c.src_dir))
|
||||
for component_src_dir in component_src_dirs:
|
||||
h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
|
||||
for h_file in h_files:
|
||||
added_include = False
|
||||
fin = open(os.path.join(c.src_dir, h_file), 'r')
|
||||
fin = open(os.path.join(component_src_dir, h_file), 'r')
|
||||
for line in fin:
|
||||
m = initializer_pat.match(line)
|
||||
if m:
|
||||
|
|
@ -2818,11 +2838,18 @@ def mk_all_mem_initializer_cpps():
|
|||
cnames.append(c.name)
|
||||
mk_mem_initializer_cpp(cnames, c.src_dir)
|
||||
|
||||
# Generate an mem_initializer.cpp at path.
|
||||
# Generate an ``gparams_register_modules.cpp`` at path.
|
||||
# This file implements the procedure
|
||||
# void gparams_register_modules()
|
||||
# This procedure is invoked by gparams::init()
|
||||
def mk_gparams_register_modules(cnames, path):
|
||||
component_src_dirs = []
|
||||
for cname in cnames:
|
||||
c = get_component(cname)
|
||||
component_src_dirs.append(c.src_dir)
|
||||
mk_gparams_register_modules_internal(component_src_dirs, path)
|
||||
|
||||
def mk_gparams_register_modules_internal(component_src_dirs, path):
|
||||
cmds = []
|
||||
mod_cmds = []
|
||||
mod_descrs = []
|
||||
|
|
@ -2833,12 +2860,11 @@ def mk_gparams_register_modules(cnames, path):
|
|||
reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)')
|
||||
reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)')
|
||||
reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)')
|
||||
for cname in cnames:
|
||||
c = get_component(cname)
|
||||
h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(c.src_dir))
|
||||
for component_src_dir in component_src_dirs:
|
||||
h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir))
|
||||
for h_file in h_files:
|
||||
added_include = False
|
||||
fin = open(os.path.join(c.src_dir, h_file), 'r')
|
||||
fin = open(os.path.join(component_src_dir, h_file), 'r')
|
||||
for line in fin:
|
||||
m = reg_pat.match(line)
|
||||
if m:
|
||||
|
|
@ -2879,14 +2905,22 @@ def mk_all_gparams_register_modules():
|
|||
|
||||
# Generate a .def based on the files at c.export_files slot.
|
||||
def mk_def_file(c):
|
||||
pat1 = re.compile(".*Z3_API.*")
|
||||
defname = '%s.def' % os.path.join(c.src_dir, c.name)
|
||||
fout = open(defname, 'w')
|
||||
fout.write('LIBRARY "%s"\nEXPORTS\n' % c.dll_name)
|
||||
num = 1
|
||||
dll_name = c.dll_name
|
||||
export_header_files = []
|
||||
for dot_h in c.export_files:
|
||||
dot_h_c = c.find_file(dot_h, c.name)
|
||||
api = open(os.path.join(dot_h_c.src_dir, dot_h), 'r')
|
||||
api = os.path.join(dot_h_c.src_dir, dot_h)
|
||||
export_header_files.append(api)
|
||||
mk_def_file_internal(defname, dll_name, export_header_files)
|
||||
|
||||
def mk_def_file_internal(defname, dll_name, export_header_files):
|
||||
pat1 = re.compile(".*Z3_API.*")
|
||||
fout = open(defname, 'w')
|
||||
fout.write('LIBRARY "%s"\nEXPORTS\n' % dll_name)
|
||||
num = 1
|
||||
for export_header_file in export_header_files:
|
||||
api = open(export_header_file, 'r')
|
||||
for line in api:
|
||||
m = pat1.match(line)
|
||||
if m:
|
||||
|
|
@ -2952,7 +2986,28 @@ def mk_bindings(api_files):
|
|||
if is_java_enabled():
|
||||
check_java()
|
||||
mk_z3consts_java(api_files)
|
||||
_execfile(os.path.join('scripts', 'update_api.py'), g) # HACK
|
||||
# Generate some of the bindings and "api" module files
|
||||
import update_api
|
||||
dotnet_output_dir = None
|
||||
if is_dotnet_enabled():
|
||||
dotnet_output_dir = get_component('dotnet').src_dir
|
||||
java_output_dir = None
|
||||
java_package_name = None
|
||||
if is_java_enabled():
|
||||
java_output_dir = get_component('java').src_dir
|
||||
java_package_name = get_component('java').package_name
|
||||
ml_output_dir = None
|
||||
if is_ml_enabled():
|
||||
ml_output_dir = get_component('ml').src_dir
|
||||
# Get the update_api module to do the work for us
|
||||
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,
|
||||
ml_output_dir=ml_output_dir
|
||||
)
|
||||
cp_z3py_to_build()
|
||||
if is_ml_enabled():
|
||||
check_ml()
|
||||
|
|
@ -2965,6 +3020,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("^ *//.*$")
|
||||
|
|
@ -2973,14 +3039,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
|
||||
|
|
@ -3041,7 +3102,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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue