mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-04 16:44:07 +00:00
Code Activity

update header include generation to use relative paths #534

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-03 08:50:04 -07:00
parent 4d07fa5db3
commit 8844112418
3 changed files with 24 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
scripts/mk_genfile_common.py
View file

@ -587,6 +587,14 @@ def mk_def_file_internal(defname, dll_name, export_header_files):
###############################################################################
# Functions for generating ``gparams_register_modules.cpp``
###############################################################################
def path_after_src(h_file):
h_file = h_file.replace("\\","/")
idx = h_file.index("src/")
if idx == -1:
return h_file
return h_file[idx + 4:]
def mk_gparams_register_modules_internal(h_files_full_path, path):
"""
Generate a ``gparams_register_modules.cpp`` file in the directory ``path``.
@ -608,7 +616,7 @@ def mk_gparams_register_modules_internal(h_files_full_path, path):
fullname = os.path.join(path, 'gparams_register_modules.cpp')
fout = open(fullname, 'w')
fout.write('// Automatically generated file.\n')
fout.write('#include"gparams.h"\n')
fout.write('#include "util/gparams.h"\n')
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\(\'([^\']*)\', *\'([^\']*)\'\)')
@ -620,13 +628,13 @@ def mk_gparams_register_modules_internal(h_files_full_path, path):
if m:
if not added_include:
added_include = True
fout.write('#include"%s"\n' % os.path.basename(h_file))
fout.write('#include "%s"\n' % path_after_src(h_file))
cmds.append((m.group(1)))
m = reg_mod_pat.match(line)
if m:
if not added_include:
added_include = True
fout.write('#include"%s"\n' % os.path.basename(h_file))
fout.write('#include "%s"\n' % path_after_src(h_file))
mod_cmds.append((m.group(1), m.group(2)))
m = reg_mod_descr_pat.match(line)
if m:
@ -680,9 +688,9 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path):
fullname = os.path.join(path, 'install_tactic.cpp')
fout = open(fullname, 'w')
fout.write('// Automatically generated file.\n')
fout.write('#include"tactic.h"\n')
fout.write('#include"tactic_cmds.h"\n')
fout.write('#include"cmd_context.h"\n')
fout.write('#include "tactic/tactic.h"\n')
fout.write('#include "cmd_context/tactic_cmds.h"\n')
fout.write('#include "cmd_context/cmd_context.h"\n')
tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)')
probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)')
for h_file in sorted_headers_by_component(h_files_full_path):
@ -691,8 +699,8 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path):
for line in fin:
if tactic_pat.match(line):
if not added_include:
added_include = True
fout.write('#include"%s"\n' % os.path.basename(h_file))
added_include = True
fout.write('#include "%s"\n' % path_after_src(h_file))
try:
eval(line.strip('\n '), eval_globals, None)
except Exception as e:
@ -702,7 +710,7 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path):
if probe_pat.match(line):
if not added_include:
added_include = True
fout.write('#include"%s"\n' % os.path.basename(h_file))
fout.write('#include "%s"\n' % path_after_src(h_file))
try:
eval(line.strip('\n '), eval_globals, None)
except Exception as e:
@ -764,19 +772,19 @@ def mk_mem_initializer_cpp_internal(h_files_full_path, path):
if m:
if not added_include:
added_include = True
fout.write('#include"%s"\n' % os.path.basename(h_file))
fout.write('#include "%s"\n' % path_after_src(h_file))
initializer_cmds.append((m.group(1), 0))
m = initializer_prio_pat.match(line)
if m:
if not added_include:
added_include = True
fout.write('#include"%s"\n' % os.path.basename(h_file))
fout.write('#include "%s"\n' % path_after_src(h_file))
initializer_cmds.append((m.group(1), int(m.group(2))))
m = finalizer_pat.match(line)
if m:
if not added_include:
added_include = True
fout.write('#include"%s"\n' % os.path.basename(h_file))
fout.write('#include "%s"\n' % path_after_src(h_file))
finalizer_cmds.append(m.group(1))
initializer_cmds.sort(key=lambda tup: tup[1])
fout.write('void mem_initialize() {\n')
@ -881,9 +889,9 @@ def mk_hpp_from_pyg(pyg_file, output_dir):
out.write('// Automatically generated file\n')
out.write('#ifndef __%s_HPP_\n' % class_name.upper())
out.write('#define __%s_HPP_\n' % class_name.upper())
out.write('#include"params.h"\n')
out.write('#include "util/params.h"\n')
if export:
out.write('#include"gparams.h"\n')
out.write('#include "util/gparams.h"\n')
out.write('struct %s {\n' % class_name)
out.write(' params_ref const & p;\n')
if export:

2
scripts/update_include.py
View file

@ -45,7 +45,7 @@ def find_paths(dir):
for root, dirs, files in os.walk(dir):
root1 = root.replace("\\","/")[4:]
for f in files:
if f.endswith('.h'):
if f.endswith('.h') or f.endswith('.hpp') or f.endswith('.cpp'):
path = "%s/%s" % (root1, f)
paths[f] = path
if f.endswith('.pyg'):

2
src/ast/ast.cpp
View file

@ -2210,7 +2210,7 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
r = mk_app_core(decl, num_args, args);
}
SASSERT(r != 0);
TRACE("app_ground", tout << "ground: " << r->is_ground() << "\n" << mk_ll_pp(r, *this) << "\n";);
TRACE("app_ground", tout << "ground: " << r->is_ground() << " id: " << r->get_id() << "\n" << mk_ll_pp(r, *this) << "\n";);
return r;
}