mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 03:32:28 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
Nikolaj Bjorner
commit
d73b8d8570
6 changed files with 383 additions and 90 deletions
|
|
@ -7,80 +7,13 @@
|
|||
# Author: Leonardo de Moura (leonardo)
|
||||
############################################
|
||||
from mk_util import *
|
||||
from mk_project import *
|
||||
|
||||
parse_options()
|
||||
check_eol()
|
||||
API_files = init_project_def()
|
||||
|
||||
add_lib('util', [])
|
||||
add_lib('polynomial', ['util'], 'math/polynomial')
|
||||
add_lib('sat', ['util'])
|
||||
add_lib('nlsat', ['polynomial', 'sat'])
|
||||
add_lib('subpaving', ['util'], 'math/subpaving')
|
||||
add_lib('ast', ['util', 'polynomial'])
|
||||
add_lib('rewriter', ['ast', 'polynomial'], 'ast/rewriter')
|
||||
# Simplifier module will be deleted in the future.
|
||||
# It has been replaced with rewriter module.
|
||||
add_lib('simplifier', ['rewriter'], 'ast/simplifier')
|
||||
# Model module should not depend on simplifier module.
|
||||
# We must replace all occurrences of simplifier with rewriter.
|
||||
add_lib('model', ['rewriter', 'simplifier'])
|
||||
add_lib('tactic', ['ast', 'model'])
|
||||
# Old (non-modular) parameter framework. It has been subsumed by util\params.h.
|
||||
# However, it is still used by many old components.
|
||||
add_lib('old_params', ['model', 'simplifier'])
|
||||
add_lib('cmd_context', ['tactic', 'rewriter', 'model', 'old_params', 'simplifier'])
|
||||
add_lib('substitution', ['ast'], 'ast/substitution')
|
||||
add_lib('normal_forms', ['rewriter', 'old_params'], 'ast/normal_forms')
|
||||
add_lib('parser_util', ['ast'], 'parsers/util')
|
||||
add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
|
||||
add_lib('pattern', ['normal_forms', 'smt2parser'], 'ast/pattern')
|
||||
add_lib('macros', ['simplifier', 'old_params'], 'ast/macros')
|
||||
add_lib('grobner', ['ast'], 'math/grobner')
|
||||
add_lib('euclid', ['util'], 'math/euclid')
|
||||
add_lib('proof_checker', ['rewriter', 'old_params'], 'ast/proof_checker')
|
||||
add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params'], 'ast/rewriter/bit_blaster')
|
||||
add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context',
|
||||
'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util'])
|
||||
add_lib('user_plugin', ['smt'], 'smt/user_plugin')
|
||||
add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core')
|
||||
add_lib('sat_tactic', ['tactic', 'sat'], 'tactic/sat')
|
||||
add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
|
||||
add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'tactic/nlsat')
|
||||
add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'tactic/subpaving')
|
||||
add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
|
||||
add_lib('fuzzing', ['ast'], 'test/fuzzing')
|
||||
add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
|
||||
add_lib('smt_tactic', ['smt'], 'tactic/smt')
|
||||
add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
|
||||
add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
|
||||
add_lib('aig', ['tactic'], 'tactic/aig')
|
||||
# TODO: split muz_qe into muz, qe. Perhaps, we should also consider breaking muz into muz and pdr.
|
||||
add_lib('muz_qe', ['smt', 'sat', 'smt2parser'])
|
||||
add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig', 'muz_qe'], 'tactic/smtlogics')
|
||||
add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
|
||||
add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
|
||||
# TODO: delete SMT 1.0 frontend
|
||||
add_lib('smtparser', ['portfolio'], 'parsers/smt')
|
||||
add_lib('api', ['portfolio', 'user_plugin', 'smtparser'],
|
||||
includes2install=['z3.h', 'z3_api.h', 'z3_v1.h', 'z3_macros.h'])
|
||||
add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
|
||||
add_exe('test', ['api', 'fuzzing'], exe_name='test-z3', install=False)
|
||||
API_files = ['z3_api.h']
|
||||
add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',
|
||||
reexports=['api'],
|
||||
dll_name='libz3',
|
||||
export_files=API_files)
|
||||
add_dot_net_dll('dotnet', ['api_dll'], 'bindings/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties')
|
||||
add_hlib('cpp', 'bindings/c++', includes2install=['z3++.h'])
|
||||
set_z3py_dir('bindings/python')
|
||||
# Examples
|
||||
add_cpp_example('cpp_example', 'c++')
|
||||
add_c_example('c_example', 'c')
|
||||
add_c_example('maxsat')
|
||||
add_dotnet_example('dotnet_example', 'dotnet')
|
||||
add_z3py_example('python')
|
||||
|
||||
update_version(4, 2, 0, 0)
|
||||
update_version()
|
||||
mk_auto_src()
|
||||
mk_bindings(API_files)
|
||||
mk_vs_proj('z3', ['shell'])
|
||||
|
|
|
|||
83
scripts/mk_project.py
Normal file
83
scripts/mk_project.py
Normal file
|
|
@ -0,0 +1,83 @@
|
|||
############################################
|
||||
# Copyright (c) 2012 Microsoft Corporation
|
||||
#
|
||||
# Z3 project configuration files
|
||||
#
|
||||
# Author: Leonardo de Moura (leonardo)
|
||||
############################################
|
||||
from mk_util import *
|
||||
|
||||
# Z3 Project definition
|
||||
def init_project_def():
|
||||
set_version(4, 2, 0, 0)
|
||||
add_lib('util', [])
|
||||
add_lib('polynomial', ['util'], 'math/polynomial')
|
||||
add_lib('sat', ['util'])
|
||||
add_lib('nlsat', ['polynomial', 'sat'])
|
||||
add_lib('subpaving', ['util'], 'math/subpaving')
|
||||
add_lib('ast', ['util', 'polynomial'])
|
||||
add_lib('rewriter', ['ast', 'polynomial'], 'ast/rewriter')
|
||||
# Simplifier module will be deleted in the future.
|
||||
# It has been replaced with rewriter module.
|
||||
add_lib('simplifier', ['rewriter'], 'ast/simplifier')
|
||||
# Model module should not depend on simplifier module.
|
||||
# We must replace all occurrences of simplifier with rewriter.
|
||||
add_lib('model', ['rewriter', 'simplifier'])
|
||||
add_lib('tactic', ['ast', 'model'])
|
||||
# Old (non-modular) parameter framework. It has been subsumed by util\params.h.
|
||||
# However, it is still used by many old components.
|
||||
add_lib('old_params', ['model', 'simplifier'])
|
||||
add_lib('cmd_context', ['tactic', 'rewriter', 'model', 'old_params', 'simplifier'])
|
||||
add_lib('substitution', ['ast'], 'ast/substitution')
|
||||
add_lib('normal_forms', ['rewriter', 'old_params'], 'ast/normal_forms')
|
||||
add_lib('parser_util', ['ast'], 'parsers/util')
|
||||
add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
|
||||
add_lib('pattern', ['normal_forms', 'smt2parser'], 'ast/pattern')
|
||||
add_lib('macros', ['simplifier', 'old_params'], 'ast/macros')
|
||||
add_lib('grobner', ['ast'], 'math/grobner')
|
||||
add_lib('euclid', ['util'], 'math/euclid')
|
||||
add_lib('proof_checker', ['rewriter', 'old_params'], 'ast/proof_checker')
|
||||
add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params'], 'ast/rewriter/bit_blaster')
|
||||
add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context',
|
||||
'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util'])
|
||||
add_lib('user_plugin', ['smt'], 'smt/user_plugin')
|
||||
add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core')
|
||||
add_lib('sat_tactic', ['tactic', 'sat'], 'tactic/sat')
|
||||
add_lib('arith_tactics', ['core_tactics', 'sat'], 'tactic/arith')
|
||||
add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'tactic/nlsat')
|
||||
add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'tactic/subpaving')
|
||||
add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
|
||||
add_lib('fuzzing', ['ast'], 'test/fuzzing')
|
||||
add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
|
||||
add_lib('smt_tactic', ['smt'], 'tactic/smt')
|
||||
add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
|
||||
add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
|
||||
add_lib('aig', ['tactic'], 'tactic/aig')
|
||||
# TODO: split muz_qe into muz, qe. Perhaps, we should also consider breaking muz into muz and pdr.
|
||||
add_lib('muz_qe', ['smt', 'sat', 'smt2parser'])
|
||||
add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig', 'muz_qe'], 'tactic/smtlogics')
|
||||
add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
|
||||
add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
|
||||
# TODO: delete SMT 1.0 frontend
|
||||
add_lib('smtparser', ['portfolio'], 'parsers/smt')
|
||||
add_lib('api', ['portfolio', 'user_plugin', 'smtparser'],
|
||||
includes2install=['z3.h', 'z3_api.h', 'z3_v1.h', 'z3_macros.h'])
|
||||
add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
|
||||
add_exe('test', ['api', 'fuzzing'], exe_name='test-z3', install=False)
|
||||
API_files = ['z3_api.h']
|
||||
add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',
|
||||
reexports=['api'],
|
||||
dll_name='libz3',
|
||||
export_files=API_files)
|
||||
add_dot_net_dll('dotnet', ['api_dll'], 'bindings/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties')
|
||||
add_hlib('cpp', 'bindings/c++', includes2install=['z3++.h'])
|
||||
set_z3py_dir('bindings/python')
|
||||
# Examples
|
||||
add_cpp_example('cpp_example', 'c++')
|
||||
add_c_example('c_example', 'c')
|
||||
add_c_example('maxsat')
|
||||
add_dotnet_example('dotnet_example', 'dotnet')
|
||||
add_z3py_example('py_example', 'python')
|
||||
return API_files
|
||||
|
||||
|
||||
|
|
@ -40,6 +40,21 @@ Z3PY_SRC_DIR=None
|
|||
VS_PROJ = False
|
||||
TRACE = False
|
||||
|
||||
VER_MAJOR=None
|
||||
VER_MINOR=None
|
||||
VER_BUILD=None
|
||||
VER_REVISION=None
|
||||
|
||||
def set_version(major, minor, build, revision):
|
||||
global VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION
|
||||
VER_MAJOR = major
|
||||
VER_MINOR = minor
|
||||
VER_BUILD = build
|
||||
VER_REVISION = revision
|
||||
|
||||
def get_version():
|
||||
return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION)
|
||||
|
||||
def is_cr_lf(fname):
|
||||
# Check whether text files use cr/lf
|
||||
f = open(fname, 'r')
|
||||
|
|
@ -191,14 +206,6 @@ def set_z3py_dir(p):
|
|||
if VERBOSE:
|
||||
print "Python bindinds directory was detected."
|
||||
|
||||
def add_z3py_example(p):
|
||||
mk_dir(BUILD_DIR)
|
||||
full = '%s/%s' % (EXAMPLE_DIR, p)
|
||||
for py in filter(lambda f: f.endswith('.py'), os.listdir(full)):
|
||||
shutil.copyfile('%s/%s' % (full, py), '%s/%s' % (BUILD_DIR, py))
|
||||
if is_verbose():
|
||||
print "Copied Z3Py example '%s' to '%s'" % (py, BUILD_DIR)
|
||||
|
||||
_UNIQ_ID = 0
|
||||
|
||||
def mk_fresh_name(prefix):
|
||||
|
|
@ -217,6 +224,9 @@ _Processed_Headers = set()
|
|||
def get_component(name):
|
||||
return _Name2Component[name]
|
||||
|
||||
def get_components():
|
||||
return _Components
|
||||
|
||||
# Return the directory where the python bindings are located.
|
||||
def get_z3py_dir():
|
||||
return Z3PY_SRC_DIR
|
||||
|
|
@ -362,6 +372,12 @@ class Component:
|
|||
def is_example(self):
|
||||
return False
|
||||
|
||||
# Invoked when creating a (windows) distribution package using components at build_path, and
|
||||
# storing them at dist_path
|
||||
def mk_win_dist(self, build_path, dist_path):
|
||||
return
|
||||
|
||||
|
||||
class LibComponent(Component):
|
||||
def __init__(self, name, path, deps, includes2install):
|
||||
Component.__init__(self, name, path, deps)
|
||||
|
|
@ -396,6 +412,12 @@ class LibComponent(Component):
|
|||
for include in self.includes2install:
|
||||
out.write('\t@rm -f $(PREFIX)/include/%s\n' % include)
|
||||
|
||||
def mk_win_dist(self, build_path, dist_path):
|
||||
mk_dir('%s/include' % dist_path)
|
||||
for include in self.includes2install:
|
||||
shutil.copy('%s/%s' % (self.src_dir, include),
|
||||
'%s/include/%s' % (dist_path, include))
|
||||
|
||||
# "Library" containing only .h files. This is just a placeholder for includes files to be installed.
|
||||
class HLibComponent(LibComponent):
|
||||
def __init__(self, name, path, includes2install):
|
||||
|
|
@ -467,6 +489,12 @@ class ExeComponent(Component):
|
|||
exefile = '%s$(EXE_EXT)' % self.exe_name
|
||||
out.write('\t@rm -f $(PREFIX)/bin/%s\n' % exefile)
|
||||
|
||||
def mk_win_dist(self, build_path, dist_path):
|
||||
if self.install:
|
||||
mk_dir('%s/bin' % dist_path)
|
||||
shutil.copy('%s/%s.exe' % (build_path, self.exe_name),
|
||||
'%s/bin/%s.exe' % (dist_path, self.exe_name))
|
||||
|
||||
|
||||
class DLLComponent(Component):
|
||||
def __init__(self, name, dll_name, path, deps, export_files, reexports, install):
|
||||
|
|
@ -538,6 +566,12 @@ class DLLComponent(Component):
|
|||
out.write('\t@rm -f $(PREFIX)/lib/%s\n' % dllfile)
|
||||
out.write('\t@rm -f %s/%s\n' % (PYTHON_PACKAGE_DIR, dllfile))
|
||||
|
||||
def mk_win_dist(self, build_path, dist_path):
|
||||
if self.install:
|
||||
mk_dir('%s/lib' % dist_path)
|
||||
shutil.copy('%s/%s.dll' % (build_path, self.dll_name),
|
||||
'%s/lib/%s.dll' % (dist_path, self.dll_name))
|
||||
|
||||
class DotNetDLLComponent(Component):
|
||||
def __init__(self, name, dll_name, path, deps, assembly_info_dir):
|
||||
Component.__init__(self, name, path, deps)
|
||||
|
|
@ -583,6 +617,12 @@ class DotNetDLLComponent(Component):
|
|||
def has_assembly_info(self):
|
||||
return True
|
||||
|
||||
def mk_win_dist(self, build_path, dist_path):
|
||||
# Assuming all DotNET dll should be in the distribution
|
||||
mk_dir('%s/lib' % dist_path)
|
||||
shutil.copy('%s/%s.dll' % (build_path, self.dll_name),
|
||||
'%s/lib/%s.dll' % (dist_path, self.dll_name))
|
||||
|
||||
class ExampleComponent(Component):
|
||||
def __init__(self, name, path):
|
||||
Component.__init__(self, name, path, [])
|
||||
|
|
@ -592,6 +632,7 @@ class ExampleComponent(Component):
|
|||
def is_example(self):
|
||||
return True
|
||||
|
||||
|
||||
class CppExampleComponent(ExampleComponent):
|
||||
def __init__(self, name, path):
|
||||
ExampleComponent.__init__(self, name, path)
|
||||
|
|
@ -666,6 +707,21 @@ class DotNetExampleComponent(ExampleComponent):
|
|||
out.write('\n')
|
||||
out.write('_ex_%s: %s\n\n' % (self.name, exefile))
|
||||
|
||||
class PythonExampleComponent(ExampleComponent):
|
||||
def __init__(self, name, path):
|
||||
ExampleComponent.__init__(self, name, path)
|
||||
|
||||
# Python examples are just placeholders, we just copy the *.py files when mk_makefile is invoked.
|
||||
# We don't need to include them in the :examples rule
|
||||
def mk_makefile(self, out):
|
||||
full = '%s/%s' % (EXAMPLE_DIR, self.path)
|
||||
for py in filter(lambda f: f.endswith('.py'), os.listdir(full)):
|
||||
shutil.copyfile('%s/%s' % (full, py), '%s/%s' % (BUILD_DIR, py))
|
||||
if is_verbose():
|
||||
print "Copied Z3Py example '%s' to '%s'" % (py, BUILD_DIR)
|
||||
out.write('_ex_%s: \n\n' % self.name)
|
||||
|
||||
|
||||
def reg_component(name, c):
|
||||
global _Id, _Components, _ComponentNames, _Name2Component
|
||||
c.id = _Id
|
||||
|
|
@ -708,6 +764,10 @@ def add_dotnet_example(name, path=None):
|
|||
c = DotNetExampleComponent(name, path)
|
||||
reg_component(name, c)
|
||||
|
||||
def add_z3py_example(name, path=None):
|
||||
c = PythonExampleComponent(name, path)
|
||||
reg_component(name, c)
|
||||
|
||||
# Copy configuration correct file to BUILD_DIR
|
||||
def cp_config_mk():
|
||||
if IS_WINDOW:
|
||||
|
|
@ -732,7 +792,7 @@ def mk_install(out):
|
|||
out.write('\t@mkdir -p $(PREFIX)/bin\n')
|
||||
out.write('\t@mkdir -p $(PREFIX)/include\n')
|
||||
out.write('\t@mkdir -p $(PREFIX)/lib\n')
|
||||
for c in _Components:
|
||||
for c in get_components():
|
||||
c.mk_install(out)
|
||||
out.write('\t@cp z3*.pyc %s\n' % PYTHON_PACKAGE_DIR)
|
||||
out.write('\t@echo Z3 was successfully installed.\n')
|
||||
|
|
@ -740,7 +800,7 @@ def mk_install(out):
|
|||
|
||||
def mk_uninstall(out):
|
||||
out.write('uninstall:\n')
|
||||
for c in _Components:
|
||||
for c in get_components():
|
||||
c.mk_uninstall(out)
|
||||
out.write('\t@rm -f %s/z3*.pyc\n' % PYTHON_PACKAGE_DIR)
|
||||
out.write('\t@echo Z3 was successfully uninstalled.\n')
|
||||
|
|
@ -757,7 +817,7 @@ def mk_makefile():
|
|||
out.write('include config.mk\n')
|
||||
# Generate :all rule
|
||||
out.write('all:')
|
||||
for c in _Components:
|
||||
for c in get_components():
|
||||
if c.main_component():
|
||||
out.write(' %s' % c.name)
|
||||
out.write('\n\t@echo Z3 was successfully built.\n')
|
||||
|
|
@ -766,12 +826,12 @@ def mk_makefile():
|
|||
out.write('\t@echo " sudo make install"\n')
|
||||
# Generate :examples rule
|
||||
out.write('examples:')
|
||||
for c in _Components:
|
||||
for c in get_components():
|
||||
if c.is_example():
|
||||
out.write(' _ex_%s' % c.name)
|
||||
out.write('\n\t@echo Z3 examples were successfully built.\n')
|
||||
# Generate components
|
||||
for c in _Components:
|
||||
for c in get_components():
|
||||
c.mk_makefile(out)
|
||||
# Generate install/uninstall rules if not WINDOWS
|
||||
if not IS_WINDOW:
|
||||
|
|
@ -818,7 +878,13 @@ def mk_pat_db():
|
|||
print "Generated '%s/database.h'" % c.src_dir
|
||||
|
||||
# Update version numbers
|
||||
def update_version(major, minor, build, revision):
|
||||
def update_version():
|
||||
major = VER_MAJOR
|
||||
minor = VER_MINOR
|
||||
build = VER_BUILD
|
||||
revision = VER_REVISION
|
||||
if major == None or minor == None or build == None or revision == None:
|
||||
raise MKException("set_version(major, minor, build, revision) must be used before invoking update_version()")
|
||||
if not ONLY_MAKEFILES:
|
||||
mk_version_dot_h(major, minor, build, revision)
|
||||
update_all_assembly_infos(major, minor, build, revision)
|
||||
|
|
@ -838,7 +904,7 @@ def mk_version_dot_h(major, minor, build, revision):
|
|||
|
||||
# Update version number in AssemblyInfo.cs files
|
||||
def update_all_assembly_infos(major, minor, build, revision):
|
||||
for c in _Components:
|
||||
for c in get_components():
|
||||
if c.has_assembly_info():
|
||||
assembly = '%s/%s/AssemblyInfo.cs' % (c.src_dir, c.assembly_info_dir)
|
||||
if os.path.exists(assembly):
|
||||
|
|
@ -962,7 +1028,7 @@ def mk_install_tactic_cpp(cnames, path):
|
|||
|
||||
def mk_all_install_tactic_cpps():
|
||||
if not ONLY_MAKEFILES:
|
||||
for c in _Components:
|
||||
for c in get_components():
|
||||
if c.require_install_tactics():
|
||||
cnames = []
|
||||
cnames.extend(c.deps)
|
||||
|
|
@ -995,7 +1061,7 @@ def mk_def_file(c):
|
|||
|
||||
def mk_def_files():
|
||||
if not ONLY_MAKEFILES:
|
||||
for c in _Components:
|
||||
for c in get_components():
|
||||
if c.require_def_file():
|
||||
mk_def_file(c)
|
||||
|
||||
|
|
@ -1273,3 +1339,11 @@ def mk_vs_proj(name, components):
|
|||
f.write('</Project>\n')
|
||||
if is_verbose():
|
||||
print "Generated '%s'" % proj_name
|
||||
|
||||
def mk_win_dist(build_path, dist_path):
|
||||
for c in get_components():
|
||||
c.mk_win_dist(build_path, dist_path)
|
||||
# Add Z3Py to lib directory
|
||||
for pyc in filter(lambda f: f.endswith('.pyc'), os.listdir(build_path)):
|
||||
shutil.copy('%s/%s' % (build_path, pyc),
|
||||
'%s/lib/%s' % (dist_path, pyc))
|
||||
|
|
|
|||
201
scripts/mk_win_dist.py
Normal file
201
scripts/mk_win_dist.py
Normal file
|
|
@ -0,0 +1,201 @@
|
|||
############################################
|
||||
# Copyright (c) 2012 Microsoft Corporation
|
||||
#
|
||||
# Scripts for automatically generating
|
||||
# Window distribution zip files.
|
||||
#
|
||||
# Author: Leonardo de Moura (leonardo)
|
||||
############################################
|
||||
import os
|
||||
import glob
|
||||
import re
|
||||
import getopt
|
||||
import sys
|
||||
import shutil
|
||||
import subprocess
|
||||
import zipfile
|
||||
from mk_exception import *
|
||||
from mk_project import *
|
||||
|
||||
BUILD_DIR='build-dist'
|
||||
BUILD_X64_DIR='build-dist/x64'
|
||||
BUILD_X86_DIR='build-dist/x86'
|
||||
VERBOSE=True
|
||||
DIST_DIR='dist'
|
||||
|
||||
def set_verbose(flag):
|
||||
global VERBOSE
|
||||
VERBOSE = flag
|
||||
|
||||
def is_verbose():
|
||||
return VERBOSE
|
||||
|
||||
def mk_dir(d):
|
||||
if not os.path.exists(d):
|
||||
os.makedirs(d)
|
||||
|
||||
def set_build_dir(path):
|
||||
global BUILD_DIR
|
||||
BUILD_DIR = path
|
||||
BUILD_X86_DIR = '%s/x86' % path
|
||||
BUILD_X64_DIR = '%s/x64' % path
|
||||
mk_dir(BUILD_X86_DIR)
|
||||
mk_dir(BUILD_X64_DIR)
|
||||
|
||||
def display_help():
|
||||
print "mk_win_dist.py: Z3 Windows distribution generator\n"
|
||||
print "This script generates the zip files containing executables, dlls, header files for Windows."
|
||||
print "It must be executed from the Z3 root directory."
|
||||
print "\nOptions:"
|
||||
print " -h, --help display this message."
|
||||
print " -s, --silent do not print verbose messages."
|
||||
print " -b <sudir>, --build=<subdir> subdirectory where x86 and x64 Z3 versions will be built (default: build-dist)."
|
||||
exit(0)
|
||||
|
||||
# Parse configuration option for mk_make script
|
||||
def parse_options():
|
||||
path = BUILD_DIR
|
||||
options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hs', ['build=',
|
||||
'help',
|
||||
'silent',
|
||||
])
|
||||
for opt, arg in options:
|
||||
if opt in ('-b', '--build'):
|
||||
if arg == 'src':
|
||||
raise MKException('The src directory should not be used to host the Makefile')
|
||||
path = arg
|
||||
elif opt in ('-s', '--silent'):
|
||||
set_verbose(False)
|
||||
elif opt in ('-h', '--help'):
|
||||
display_help()
|
||||
else:
|
||||
raise MKException("Invalid command line option '%s'" % opt)
|
||||
set_build_dir(path)
|
||||
|
||||
# Check whether build directory already exists or not
|
||||
def check_build_dir(path):
|
||||
return os.path.exists(path) and os.path.exists('%s/Makefile' % path)
|
||||
|
||||
# Create a build directory using mk_make.py
|
||||
def mk_build_dir(path, x64):
|
||||
if not check_build_dir(path):
|
||||
opts = ["python", "scripts/mk_make.py", "-b", path]
|
||||
if x64:
|
||||
opts.append('-x')
|
||||
if subprocess.call(opts) != 0:
|
||||
raise MKException("Failed to generate build directory at '%s'" % path)
|
||||
|
||||
# Create build directories
|
||||
def mk_build_dirs():
|
||||
mk_build_dir(BUILD_X86_DIR, False)
|
||||
mk_build_dir(BUILD_X64_DIR, True)
|
||||
|
||||
# Check if on Visual Studio command prompt
|
||||
def check_vc_cmd_prompt():
|
||||
try:
|
||||
subprocess.call(['cl'], stdin=subprocess.PIPE, stderr=subprocess.PIPE)
|
||||
except:
|
||||
raise MKException("You must execute the mk_win_dist.py script on a Visual Studio Command Prompt")
|
||||
|
||||
def exec_cmds(cmds):
|
||||
cmd_file = 'z3_tmp.cmd'
|
||||
f = open(cmd_file, 'w')
|
||||
for cmd in cmds:
|
||||
f.write(cmd)
|
||||
f.write('\n')
|
||||
f.close()
|
||||
res = 0
|
||||
try:
|
||||
res = subprocess.call(cmd_file, shell=True)
|
||||
except:
|
||||
res = 1
|
||||
try:
|
||||
os.erase(cmd_file)
|
||||
except:
|
||||
pass
|
||||
return res
|
||||
|
||||
# Compile Z3 (if x64 == True, then it builds it in x64 mode).
|
||||
def mk_z3_core(x64):
|
||||
cmds = []
|
||||
if x64:
|
||||
cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" amd64')
|
||||
cmds.append('cd %s' % BUILD_X64_DIR)
|
||||
else:
|
||||
cmds.append('"call %VCINSTALLDIR%vcvarsall.bat" x86')
|
||||
cmds.append('cd %s' % BUILD_X86_DIR)
|
||||
cmds.append('nmake')
|
||||
if exec_cmds(cmds) != 0:
|
||||
raise MKException("Failed to make z3, x64: %s" % x64)
|
||||
|
||||
def mk_z3():
|
||||
mk_z3_core(False)
|
||||
mk_z3_core(True)
|
||||
|
||||
def mk_dist_dir_core(x64):
|
||||
major, minor, build, revision = get_version()
|
||||
if x64:
|
||||
platform = "x64"
|
||||
build_path = BUILD_X64_DIR
|
||||
else:
|
||||
platform = "x86"
|
||||
build_path = BUILD_X86_DIR
|
||||
dist_path = '%s/z3-%s.%s.%s-%s' % (DIST_DIR, major, minor, build, platform)
|
||||
mk_dir(dist_path)
|
||||
mk_win_dist(build_path, dist_path)
|
||||
if is_verbose():
|
||||
print "Generated %s distribution folder at '%s'" % (platform, dist_path)
|
||||
|
||||
def mk_dist_dir():
|
||||
mk_dist_dir_core(False)
|
||||
mk_dist_dir_core(True)
|
||||
|
||||
ZIPOUT = None
|
||||
|
||||
def mk_zip_visitor(pattern, dir, files):
|
||||
for filename in files:
|
||||
if fnmatch(filename, pattern):
|
||||
fname = os.path.join(dir, filename)
|
||||
if not os.path.isdir(fname):
|
||||
ZIPOUT.write(fname)
|
||||
|
||||
def mk_zip_core(x64):
|
||||
global ZIPOUT
|
||||
major, minor, build, revision = get_version()
|
||||
if x64:
|
||||
platform = "x64"
|
||||
else:
|
||||
platform = "x86"
|
||||
dist_path = 'z3-%s.%s.%s-%s' % (major, minor, build, platform)
|
||||
old = os.getcwd()
|
||||
try:
|
||||
os.chdir(DIST_DIR)
|
||||
zfname = '%s.zip' % dist_path
|
||||
ZIPOUT = zipfile.ZipFile(zfname, 'w')
|
||||
os.path.walk(dist_path, mk_zip_visitor, '*')
|
||||
if is_verbose():
|
||||
print "Generated '%s'" % zfname
|
||||
except:
|
||||
pass
|
||||
ZIPOUT = None
|
||||
os.chdir(old)
|
||||
|
||||
# Create a zip file for each platform
|
||||
def mk_zip():
|
||||
mk_zip_core(False)
|
||||
mk_zip_core(True)
|
||||
|
||||
# Entry point
|
||||
def main():
|
||||
if os.name != 'nt':
|
||||
raise MKException("This script is for Windows only")
|
||||
parse_options()
|
||||
check_vc_cmd_prompt()
|
||||
mk_build_dirs()
|
||||
mk_z3()
|
||||
init_project_def()
|
||||
mk_dist_dir()
|
||||
mk_zip()
|
||||
|
||||
main()
|
||||
|
||||
|
|
@ -56,11 +56,13 @@ void error(const char * msg) {
|
|||
}
|
||||
|
||||
void display_usage() {
|
||||
std::cout << "Z3 [version " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << " - ";
|
||||
#ifdef _AMD64_
|
||||
std::cout << "Z3 [version " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << " - 64 bit]. (C) Copyright 2006 Microsoft Corp.\n";
|
||||
std::cout << "64";
|
||||
#else
|
||||
std::cout << "Z3 [version " << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << " - 32 bit]. (C) Copyright 2006 Microsoft Corp.\n";
|
||||
std::cout << "32";
|
||||
#endif
|
||||
std::cout << " bit]. (C) Copyright 2006 Microsoft Corp.\n";
|
||||
std::cout << "Usage: z3 [options] [" << OPT << "file:]file\n";
|
||||
std::cout << "\nInput format:\n";
|
||||
std::cout << " " << OPT << "smt use parser for SMT input format.\n";
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ Revision History:
|
|||
--*/
|
||||
#include"imdd.h"
|
||||
|
||||
#ifndef _AMD64_
|
||||
#if !defined(_AMD64_) && defined(Z3DEBUG)
|
||||
|
||||
static void tst0() {
|
||||
std::cout << "--------------------------------\n";
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue