mirror of
https://github.com/Z3Prover/z3
synced 2025-06-06 14:13:23 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
zach shipko
commit
9cc4fc919d
396 changed files with 46229 additions and 69540 deletions
|
|
@ -32,6 +32,10 @@ CXXFLAGS=getenv("CXXFLAGS", "")
|
|||
EXAMP_DEBUG_FLAG=''
|
||||
LDFLAGS=getenv("LDFLAGS", "")
|
||||
JNI_HOME=getenv("JNI_HOME", None)
|
||||
OCAMLC=getenv("OCAMLC", "ocamlc")
|
||||
OCAMLOPT=getenv("OCAMLOPT", "ocamlopt")
|
||||
OCAML_LIB=getenv("OCAML_LIB", None)
|
||||
OCAMLFIND=getenv("OCAMLFIND", "ocamlfind")
|
||||
|
||||
CXX_COMPILERS=['g++', 'clang++']
|
||||
C_COMPILERS=['gcc', 'clang']
|
||||
|
|
@ -49,6 +53,7 @@ UTIL_COMPONENT='util'
|
|||
API_COMPONENT='api'
|
||||
DOTNET_COMPONENT='dotnet'
|
||||
JAVA_COMPONENT='java'
|
||||
ML_COMPONENT='ml'
|
||||
CPP_COMPONENT='cpp'
|
||||
#####################
|
||||
IS_WINDOWS=False
|
||||
|
|
@ -59,12 +64,14 @@ VERBOSE=True
|
|||
DEBUG_MODE=False
|
||||
SHOW_CPPS = True
|
||||
VS_X64 = False
|
||||
LINUX_X64 = True
|
||||
ONLY_MAKEFILES = False
|
||||
Z3PY_SRC_DIR=None
|
||||
VS_PROJ = False
|
||||
TRACE = False
|
||||
DOTNET_ENABLED=False
|
||||
JAVA_ENABLED=False
|
||||
ML_ENABLED=False
|
||||
STATIC_LIB=False
|
||||
VER_MAJOR=None
|
||||
VER_MINOR=None
|
||||
|
|
@ -219,7 +226,16 @@ def test_openmp(cc):
|
|||
t = TempFile('tstomp.cpp')
|
||||
t.add('#include<omp.h>\nint main() { return omp_in_parallel() ? 1 : 0; }\n')
|
||||
t.commit()
|
||||
return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '-fopenmp']) == 0
|
||||
if IS_WINDOWS:
|
||||
r = exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '/openmp']) == 0
|
||||
try:
|
||||
rmf('tstomp.obj')
|
||||
rmf('tstomp.exe')
|
||||
except:
|
||||
pass
|
||||
return r
|
||||
else:
|
||||
return exec_compiler_cmd([cc, CPPFLAGS, 'tstomp.cpp', LDFLAGS, '-fopenmp']) == 0
|
||||
|
||||
def find_jni_h(path):
|
||||
for root, dirs, files in os.walk(path):
|
||||
|
|
@ -333,8 +349,62 @@ def check_java():
|
|||
if JNI_HOME == None:
|
||||
raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.")
|
||||
|
||||
def check_ml():
|
||||
t = TempFile('hello.ml')
|
||||
t.add('print_string "Hello world!\n";;')
|
||||
t.commit()
|
||||
if is_verbose():
|
||||
print ('Testing %s...' % OCAMLC)
|
||||
r = exec_cmd([OCAMLC, '-o', 'a.out', 'hello.ml'])
|
||||
if r != 0:
|
||||
raise MKException('Failed testing ocamlc compiler. Set environment variable OCAMLC with the path to the Ocaml compiler')
|
||||
if is_verbose():
|
||||
print ('Testing %s...' % OCAMLOPT)
|
||||
r = exec_cmd([OCAMLOPT, '-o', 'a.out', 'hello.ml'])
|
||||
if r != 0:
|
||||
raise MKException('Failed testing ocamlopt compiler. Set environment variable OCAMLOPT with the path to the Ocaml native compiler. Note that ocamlopt may require flexlink to be in your path.')
|
||||
try:
|
||||
rmf('hello.cmi')
|
||||
rmf('hello.cmo')
|
||||
rmf('hello.cmx')
|
||||
rmf('a.out')
|
||||
rmf('hello.o')
|
||||
except:
|
||||
pass
|
||||
find_ml_lib()
|
||||
find_ocaml_find()
|
||||
|
||||
def find_ocaml_find():
|
||||
global OCAMLFIND
|
||||
if is_verbose():
|
||||
print ("Testing %s..." % OCAMLFIND)
|
||||
r = exec_cmd([OCAMLFIND, 'printconf'])
|
||||
if r != 0:
|
||||
OCAMLFIND=''
|
||||
|
||||
def find_ml_lib():
|
||||
global OCAML_LIB
|
||||
if is_verbose():
|
||||
print ('Finding OCAML_LIB...')
|
||||
t = TempFile('output')
|
||||
null = open(os.devnull, 'wb')
|
||||
try:
|
||||
subprocess.call([OCAMLC, '-where'], stdout=t.fname, stderr=null)
|
||||
t.commit()
|
||||
except:
|
||||
raise MKException('Failed to find Ocaml library; please set OCAML_LIB')
|
||||
t = open('output', 'r')
|
||||
for line in t:
|
||||
OCAML_LIB = line[:-1]
|
||||
if is_verbose():
|
||||
print ('OCAML_LIB=%s' % OCAML_LIB)
|
||||
t.close()
|
||||
rmf('output')
|
||||
return
|
||||
|
||||
def is64():
|
||||
return sys.maxsize >= 2**32
|
||||
global LINUX_X64
|
||||
return LINUX_X64 and sys.maxsize >= 2**32
|
||||
|
||||
def check_ar():
|
||||
if is_verbose():
|
||||
|
|
@ -450,13 +520,16 @@ def display_help(exit_code):
|
|||
print(" -t, --trace enable tracing in release mode.")
|
||||
if IS_WINDOWS:
|
||||
print(" -x, --x64 create 64 binary when using Visual Studio.")
|
||||
else:
|
||||
print(" --x86 force 32-bit x86 build on x64 systems.")
|
||||
print(" -m, --makefiles generate only makefiles.")
|
||||
if IS_WINDOWS:
|
||||
print(" -v, --vsproj generate Visual Studio Project Files.")
|
||||
if IS_WINDOWS:
|
||||
print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.")
|
||||
print(" -j, --java generate Java bindings.")
|
||||
print(" --staticlib build Z3 static library.")
|
||||
print(" --ml generate OCaml bindings.")
|
||||
print(" --staticlib build Z3 static library.")
|
||||
if not IS_WINDOWS:
|
||||
print(" -g, --gmp use GMP.")
|
||||
print(" --gprof enable gprof")
|
||||
|
|
@ -471,18 +544,22 @@ def display_help(exit_code):
|
|||
print(" CXXFLAGS C++ compiler flags")
|
||||
print(" JDK_HOME JDK installation directory (only relevant if -j or --java option is provided)")
|
||||
print(" JNI_HOME JNI bindings directory (only relevant if -j or --java option is provided)")
|
||||
print(" OCAMLC Ocaml byte-code compiler (only relevant with --ml)")
|
||||
print(" OCAMLOPT Ocaml native compiler (only relevant with --ml)")
|
||||
print(" OCAML_LIB Ocaml library directory (only relevant with --ml)")
|
||||
exit(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_ENABLED, JAVA_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
|
||||
global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
|
||||
global LINUX_X64
|
||||
try:
|
||||
options, remainder = getopt.gnu_getopt(sys.argv[1:],
|
||||
'b:df:sxhmcvtnp:gj',
|
||||
['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
|
||||
'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
|
||||
'githash='])
|
||||
'githash=', 'x86', 'ml'])
|
||||
except:
|
||||
print("ERROR: Invalid command line option")
|
||||
display_help(1)
|
||||
|
|
@ -501,9 +578,11 @@ def parse_options():
|
|||
if not IS_WINDOWS:
|
||||
raise MKException('x64 compilation mode can only be specified when using Visual Studio')
|
||||
VS_X64 = True
|
||||
elif opt in ('--x86'):
|
||||
LINUX_X64=False
|
||||
elif opt in ('-h', '--help'):
|
||||
display_help(0)
|
||||
elif opt in ('-m', '--onlymakefiles'):
|
||||
elif opt in ('-m', '--makefiles'):
|
||||
ONLY_MAKEFILES = True
|
||||
elif opt in ('-c', '--showcpp'):
|
||||
SHOW_CPPS = True
|
||||
|
|
@ -535,6 +614,8 @@ def parse_options():
|
|||
GPROF = True
|
||||
elif opt == '--githash':
|
||||
GIT_HASH=arg
|
||||
elif opt in ('', '--ml'):
|
||||
ML_ENABLED = True
|
||||
else:
|
||||
print("ERROR: Invalid command line option '%s'" % opt)
|
||||
display_help(1)
|
||||
|
|
@ -621,6 +702,9 @@ def is_verbose():
|
|||
def is_java_enabled():
|
||||
return JAVA_ENABLED
|
||||
|
||||
def is_ml_enabled():
|
||||
return ML_ENABLED
|
||||
|
||||
def is_compiler(given, expected):
|
||||
"""
|
||||
Return True if the 'given' compiler is the expected one.
|
||||
|
|
@ -665,6 +749,9 @@ def get_cs_files(path):
|
|||
def get_java_files(path):
|
||||
return filter(lambda f: f.endswith('.java'), os.listdir(path))
|
||||
|
||||
def get_ml_files(path):
|
||||
return filter(lambda f: f.endswith('.ml'), os.listdir(path))
|
||||
|
||||
def find_all_deps(name, deps):
|
||||
new_deps = []
|
||||
for dep in deps:
|
||||
|
|
@ -1198,6 +1285,7 @@ class JavaDLLComponent(Component):
|
|||
self.dll_name = dll_name
|
||||
self.package_name = package_name
|
||||
self.manifest_file = manifest_file
|
||||
self.install = not is_windows()
|
||||
|
||||
def mk_makefile(self, out):
|
||||
global JAVAC
|
||||
|
|
@ -1268,6 +1356,137 @@ class JavaDLLComponent(Component):
|
|||
shutil.copy(os.path.join(build_path, 'libz3java.%s' % so),
|
||||
os.path.join(dist_path, 'bin', 'libz3java.%s' % so))
|
||||
|
||||
def mk_install(self, out):
|
||||
if is_java_enabled() and self.install:
|
||||
dllfile = '%s$(SO_EXT)' % self.dll_name
|
||||
out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(PREFIX)', 'lib', dllfile)))
|
||||
out.write('\t@cp %s.jar %s.jar\n' % (self.package_name, os.path.join('$(PREFIX)', 'lib', self.package_name)))
|
||||
|
||||
def mk_uninstall(self, out):
|
||||
if is_java_enabled() and self.install:
|
||||
dllfile = '%s$(SO_EXT)' % self.dll_name
|
||||
out.write('\t@rm %s\n' % (os.path.join('$(PREFIX)', 'lib', dllfile)))
|
||||
out.write('\t@rm %s.jar\n' % (os.path.join('$(PREFIX)', 'lib', self.package_name)))
|
||||
|
||||
class MLComponent(Component):
|
||||
def __init__(self, name, lib_name, path, deps):
|
||||
Component.__init__(self, name, path, deps)
|
||||
if lib_name == None:
|
||||
lib_name = name
|
||||
self.lib_name = lib_name
|
||||
|
||||
def mk_ml_meta(self, ml_meta_in, ml_meta_out, major, minor, build, revision):
|
||||
ver_pat = re.compile('version = "VERSION"*')
|
||||
fin = open(ml_meta_in, 'r')
|
||||
fout = open(ml_meta_out, 'w')
|
||||
num_updates = 0
|
||||
for line in fin:
|
||||
if ver_pat.match(line):
|
||||
fout.write('version = "%s.%s.%s.%s"\n' % (major, minor, build, revision))
|
||||
num_updates = num_updates + 1
|
||||
else:
|
||||
fout.write(line)
|
||||
assert num_updates == 1, "unexpected number of version number updates"
|
||||
fin.close()
|
||||
fout.close()
|
||||
if VERBOSE:
|
||||
print("Updated '%s'" % ml_meta_out)
|
||||
|
||||
|
||||
def mk_makefile(self, out):
|
||||
if is_ml_enabled():
|
||||
CP_CMD = "cp"
|
||||
if IS_WINDOWS:
|
||||
CP_CMD = "copy"
|
||||
src_dir = self.to_src_dir
|
||||
sub_dir = os.path.join('api', 'ml')
|
||||
mk_dir(os.path.join(BUILD_DIR, sub_dir))
|
||||
api_src = get_component(API_COMPONENT).to_src_dir
|
||||
out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n') # remove /GL; the ocaml tools don't like it.
|
||||
for f in filter(lambda f: f.endswith('.ml'), os.listdir(self.src_dir)):
|
||||
out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f)))
|
||||
str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f))
|
||||
out.write(str)
|
||||
for f in filter(lambda f: f.endswith('.mli'), os.listdir(self.src_dir)):
|
||||
out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f)))
|
||||
str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f))
|
||||
out.write(str)
|
||||
for f in filter(lambda f: f.endswith('.c'), os.listdir(self.src_dir)):
|
||||
out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f)))
|
||||
str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f))
|
||||
out.write(str)
|
||||
modules = ["z3enums", "z3native", "z3"] # dependencies in this order!
|
||||
mls = ''
|
||||
mlis = ''
|
||||
cmis = ''
|
||||
archives = ''
|
||||
|
||||
for m in modules:
|
||||
fn = os.path.join(self.src_dir, ('%s.mli' % m))
|
||||
if not os.path.exists(fn):
|
||||
out.write('%s.mli: %s.ml%s\n' % (os.path.join(sub_dir,m),os.path.join(sub_dir,m),mlis))
|
||||
out.write('\t%s -I %s -i -c %s.ml > %s.mli\n' % (OCAMLC,sub_dir,os.path.join(sub_dir, m),os.path.join(sub_dir, m)))
|
||||
out.write('%s.cmi: %s.mli%s\n' % (os.path.join(sub_dir,m),os.path.join(sub_dir,m), cmis))
|
||||
out.write('\t%s -I %s -c %s.mli\n' % (OCAMLC,sub_dir,os.path.join(sub_dir,m)))
|
||||
out.write('%s.cma: %s.ml %s.cmi%s\n' % (os.path.join(sub_dir,m),os.path.join(sub_dir,m),os.path.join(sub_dir,m), archives))
|
||||
out.write('\t%s -a -o %s.ml -o %s.cma\n' % (OCAMLC,os.path.join(sub_dir,m), os.path.join(sub_dir,m)))
|
||||
mlis = mlis + ' ' + os.path.join(sub_dir, m) + '.mli'
|
||||
cmis = cmis + ' ' + os.path.join(sub_dir,m) + '.cmi'
|
||||
archives = archives + ' ' + os.path.join(sub_dir,m) + '.cma'
|
||||
mls = mls + ' ' + os.path.join(sub_dir, m) + '.ml'
|
||||
|
||||
out.write('%s: %s %s\n' %
|
||||
(os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)'),
|
||||
os.path.join(sub_dir, 'z3native_stubs.c'),
|
||||
get_component(Z3_DLL_COMPONENT).dll_name+'$(SO_EXT)'));
|
||||
out.write('\t$(CC) $(CXXFLAGS_OCAML) -I %s -I %s %s $(CXX_OUT_FLAG)%s$(OBJ_EXT)\n' %
|
||||
(OCAML_LIB, api_src, os.path.join(sub_dir, 'z3native_stubs.c'), os.path.join(sub_dir, 'z3native_stubs')))
|
||||
|
||||
out.write('%s: %s %s %s$(SO_EXT)' % (
|
||||
os.path.join(sub_dir, "z3ml.cmxa"),
|
||||
cmis,
|
||||
archives,
|
||||
get_component(Z3_DLL_COMPONENT).dll_name))
|
||||
out.write(' %s\n' % (os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)')))
|
||||
out.write('\tocamlmklib -o %s -I %s -ldopt \"-L. -lz3\" ' % (os.path.join(sub_dir, 'z3ml'), sub_dir))
|
||||
for m in modules:
|
||||
out.write(' %s' % (os.path.join(sub_dir, m+'.ml')))
|
||||
out.write(' %s\n' % (os.path.join(sub_dir, 'z3native_stubs$(OBJ_EXT)')))
|
||||
out.write('ml: %s\n' % (os.path.join(sub_dir, 'z3ml.cmxa')))
|
||||
self.mk_ml_meta(os.path.join('src/api/ml/META'), os.path.join(BUILD_DIR, sub_dir, 'META'), VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION)
|
||||
if OCAMLFIND != '':
|
||||
out.write('\nocamlfind_install: %s %s %s\n' % (
|
||||
get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT)',
|
||||
os.path.join(sub_dir, 'z3ml.cmxa'),
|
||||
os.path.join(sub_dir, 'META')))
|
||||
out.write('\t%s remove Z3\n' % (OCAMLFIND))
|
||||
out.write('\t%s install Z3 %s' % (OCAMLFIND, (os.path.join(sub_dir, 'META'))))
|
||||
for m in modules:
|
||||
out.write(' %s.cma' % (os.path.join(sub_dir, m)))
|
||||
out.write(' %s.cmx' % (os.path.join(sub_dir, m)))
|
||||
out.write(' %s.cmi' % (os.path.join(sub_dir, m)))
|
||||
out.write(' %s.cmo' % (os.path.join(sub_dir, m)))
|
||||
out.write(' %s.ml' % (os.path.join(sub_dir, m)))
|
||||
out.write(' %s.mli' % (os.path.join(sub_dir, m)))
|
||||
out.write(' %s$(OBJ_EXT)' % (os.path.join(sub_dir, m)))
|
||||
out.write(' %s' % ((os.path.join(sub_dir, 'z3ml$(LIB_EXT)'))))
|
||||
out.write(' %s' % ((os.path.join(sub_dir, 'z3ml.cma'))))
|
||||
out.write(' %s' % ((os.path.join(sub_dir, 'z3ml.cmxa'))))
|
||||
out.write(' %s' % ((os.path.join(sub_dir, 'libz3ml$(LIB_EXT)'))))
|
||||
out.write(' %s' % ((os.path.join(sub_dir, 'dllz3ml'))))
|
||||
if IS_WINDOWS:
|
||||
out.write('.dll')
|
||||
else:
|
||||
out.write('.so') # .so also on OSX!
|
||||
out.write(' ' + get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT)')
|
||||
if IS_WINDOWS:
|
||||
out.write(' ' + get_component(Z3_DLL_COMPONENT).dll_name + '$(LIB_EXT)')
|
||||
out.write('\n\n')
|
||||
|
||||
|
||||
def main_component(self):
|
||||
return is_ml_enabled()
|
||||
|
||||
class ExampleComponent(Component):
|
||||
def __init__(self, name, path):
|
||||
Component.__init__(self, name, path, [])
|
||||
|
|
@ -1377,6 +1596,39 @@ class JavaExampleComponent(ExampleComponent):
|
|||
out.write(' -d .\n')
|
||||
out.write('_ex_%s: JavaExample.class\n\n' % (self.name))
|
||||
|
||||
class MLExampleComponent(ExampleComponent):
|
||||
def __init__(self, name, path):
|
||||
ExampleComponent.__init__(self, name, path)
|
||||
|
||||
def is_example(self):
|
||||
return ML_ENABLED
|
||||
|
||||
def mk_makefile(self, out):
|
||||
if ML_ENABLED:
|
||||
out.write('ml_example.byte: api/ml/z3ml.cmxa ')
|
||||
for mlfile in get_ml_files(self.ex_dir):
|
||||
out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
|
||||
out.write('\n')
|
||||
out.write('\t%s ' % OCAMLC)
|
||||
if DEBUG_MODE:
|
||||
out.write('-g ')
|
||||
out.write('-custom -o ml_example.byte -I api/ml -cclib "-L. -lz3" nums.cma z3ml.cma')
|
||||
for mlfile in get_ml_files(self.ex_dir):
|
||||
out.write(' %s/%s' % (self.to_ex_dir, mlfile))
|
||||
out.write('\n')
|
||||
out.write('ml_example$(EXE_EXT): api/ml/z3ml.cmxa ml_example.byte')
|
||||
for mlfile in get_ml_files(self.ex_dir):
|
||||
out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
|
||||
out.write('\n')
|
||||
out.write('\t%s ' % OCAMLOPT)
|
||||
if DEBUG_MODE:
|
||||
out.write('-g ')
|
||||
out.write('-o ml_example$(EXE_EXT) -I api/ml -cclib "-L. -lz3" nums.cmxa z3ml.cmxa')
|
||||
for mlfile in get_ml_files(self.ex_dir):
|
||||
out.write(' %s/%s' % (self.to_ex_dir, mlfile))
|
||||
out.write('\n')
|
||||
out.write('_ex_%s: ml_example.byte ml_example$(EXE_EXT)\n\n' % self.name)
|
||||
|
||||
class PythonExampleComponent(ExampleComponent):
|
||||
def __init__(self, name, path):
|
||||
ExampleComponent.__init__(self, name, path)
|
||||
|
|
@ -1430,6 +1682,10 @@ def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, man
|
|||
c = JavaDLLComponent(name, dll_name, package_name, manifest_file, path, deps)
|
||||
reg_component(name, c)
|
||||
|
||||
def add_ml_lib(name, deps=[], path=None, lib_name=None):
|
||||
c = MLComponent(name, lib_name, path, deps)
|
||||
reg_component(name, c)
|
||||
|
||||
def add_cpp_example(name, path=None):
|
||||
c = CppExampleComponent(name, path)
|
||||
reg_component(name, c)
|
||||
|
|
@ -1446,6 +1702,10 @@ def add_java_example(name, path=None):
|
|||
c = JavaExampleComponent(name, path)
|
||||
reg_component(name, c)
|
||||
|
||||
def add_ml_example(name, path=None):
|
||||
c = MLExampleComponent(name, path)
|
||||
reg_component(name, c)
|
||||
|
||||
def add_z3py_example(name, path=None):
|
||||
c = PythonExampleComponent(name, path)
|
||||
reg_component(name, c)
|
||||
|
|
@ -1462,7 +1722,7 @@ def mk_config():
|
|||
'OBJ_EXT=.obj\n'
|
||||
'LIB_EXT=.lib\n'
|
||||
'AR=lib\n'
|
||||
'AR_FLAGS=/nologo\n'
|
||||
'AR_FLAGS=/nologo /LTCG\n'
|
||||
'AR_OUTFLAG=/OUT:\n'
|
||||
'EXE_EXT=.exe\n'
|
||||
'LINK=cl\n'
|
||||
|
|
@ -1472,50 +1732,60 @@ def mk_config():
|
|||
'SLINK_OUT_FLAG=/Fe\n'
|
||||
'OS_DEFINES=/D _WINDOWS\n')
|
||||
extra_opt = ''
|
||||
HAS_OMP = test_openmp('cl')
|
||||
if HAS_OMP:
|
||||
extra_opt = ' /openmp'
|
||||
else:
|
||||
extra_opt = ' -D_NO_OMP_'
|
||||
if GIT_HASH:
|
||||
extra_opt = '%s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH)
|
||||
extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH)
|
||||
if DEBUG_MODE:
|
||||
config.write(
|
||||
'LINK_FLAGS=/nologo /MDd\n'
|
||||
'SLINK_FLAGS=/nologo /LDd\n')
|
||||
if not VS_X64:
|
||||
config.write(
|
||||
'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt)
|
||||
'CXXFLAGS=/c /GL /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt)
|
||||
config.write(
|
||||
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
|
||||
'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
|
||||
'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
|
||||
'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
|
||||
else:
|
||||
config.write(
|
||||
'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt)
|
||||
'CXXFLAGS=/c /GL /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt)
|
||||
config.write(
|
||||
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
|
||||
'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
|
||||
'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
|
||||
'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
|
||||
else:
|
||||
# Windows Release mode
|
||||
config.write(
|
||||
'LINK_FLAGS=/nologo /MD\n'
|
||||
'SLINK_FLAGS=/nologo /LD\n')
|
||||
if TRACE:
|
||||
extra_opt = '%s /D _TRACE' % extra_opt
|
||||
extra_opt = '%s /D _TRACE ' % extra_opt
|
||||
if not VS_X64:
|
||||
config.write(
|
||||
'CXXFLAGS=/nologo /c /Zi /openmp /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt)
|
||||
'CXXFLAGS=/nologo /c /GL /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt)
|
||||
config.write(
|
||||
'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
|
||||
'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
|
||||
'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
|
||||
'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
|
||||
else:
|
||||
config.write(
|
||||
'CXXFLAGS=/c /Zi /nologo /openmp /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % extra_opt)
|
||||
'CXXFLAGS=/c /GL /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG %s /D _LIB /D _WINDOWS /D _AMD64_ /D _UNICODE /D UNICODE /Gm- /EHsc /MD /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP\n' % extra_opt)
|
||||
config.write(
|
||||
'LINK_EXTRA_FLAGS=/link /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n'
|
||||
'SLINK_EXTRA_FLAGS=/link /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n')
|
||||
'LINK_EXTRA_FLAGS=/link /LTCG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608\n'
|
||||
'SLINK_EXTRA_FLAGS=/link /LTCG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n')
|
||||
|
||||
# End of Windows VS config.mk
|
||||
if is_verbose():
|
||||
print('64-bit: %s' % is64())
|
||||
if is_java_enabled():
|
||||
print('OpenMP: %s' % HAS_OMP)
|
||||
if is_java_enabled():
|
||||
print('JNI Bindings: %s' % JNI_HOME)
|
||||
print('Java Compiler: %s' % JAVAC)
|
||||
if is_ml_enabled():
|
||||
print('OCaml Compiler: %s' % OCAMLC)
|
||||
print('OCaml Native: %s' % OCAMLOPT)
|
||||
print('OCaml Library: %s' % OCAML_LIB)
|
||||
else:
|
||||
global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG
|
||||
OS_DEFINES = ""
|
||||
|
|
@ -1545,7 +1815,7 @@ def mk_config():
|
|||
FOCI2 = False
|
||||
if GIT_HASH:
|
||||
CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
|
||||
CXXFLAGS = '%s -c' % CXXFLAGS
|
||||
CXXFLAGS = '%s -fvisibility=hidden -c' % CXXFLAGS
|
||||
HAS_OMP = test_openmp(CXX)
|
||||
if HAS_OMP:
|
||||
CXXFLAGS = '%s -fopenmp -mfpmath=sse' % CXXFLAGS
|
||||
|
|
@ -1598,6 +1868,10 @@ def mk_config():
|
|||
CPPFLAGS = '%s -D_AMD64_' % CPPFLAGS
|
||||
if sysname == 'Linux':
|
||||
CPPFLAGS = '%s -D_USE_THREAD_LOCAL' % CPPFLAGS
|
||||
elif not LINUX_X64:
|
||||
CXXFLAGS = '%s -m32' % CXXFLAGS
|
||||
LDFLAGS = '%s -m32' % LDFLAGS
|
||||
SLIBFLAGS = '%s -m32' % SLIBFLAGS
|
||||
if DEBUG_MODE:
|
||||
CPPFLAGS = '%s -DZ3DEBUG' % CPPFLAGS
|
||||
if TRACE or DEBUG_MODE:
|
||||
|
|
@ -1635,16 +1909,22 @@ def mk_config():
|
|||
print('64-bit: %s' % is64())
|
||||
if GPROF:
|
||||
print('gprof: enabled')
|
||||
print('Python version: %s' % distutils.sysconfig.get_python_version())
|
||||
print('Python version: %s' % distutils.sysconfig.get_python_version())
|
||||
if is_java_enabled():
|
||||
print('JNI Bindings: %s' % JNI_HOME)
|
||||
print('Java Compiler: %s' % JAVAC)
|
||||
if is_ml_enabled():
|
||||
print('OCaml Compiler: %s' % OCAMLC)
|
||||
print('OCaml Native: %s' % OCAMLOPT)
|
||||
print('OCaml Library: %s' % OCAML_LIB)
|
||||
|
||||
def mk_install(out):
|
||||
out.write('install: ')
|
||||
for c in get_components():
|
||||
c.mk_install_deps(out)
|
||||
out.write(' ')
|
||||
if is_ml_enabled() and OCAMLFIND != '':
|
||||
out.write('ocamlfind_install')
|
||||
out.write('\n')
|
||||
out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'bin'))
|
||||
out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'include'))
|
||||
|
|
@ -1862,7 +2142,7 @@ 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('char const * g_pattern_database =\n')
|
||||
fout.write('static char const g_pattern_database[] =\n')
|
||||
for line in fin:
|
||||
fout.write('"%s\\n"\n' % line.strip('\n'))
|
||||
fout.write(';\n')
|
||||
|
|
@ -2205,6 +2485,9 @@ def mk_bindings(api_files):
|
|||
mk_z3consts_java(api_files)
|
||||
_execfile(os.path.join('scripts', 'update_api.py'), g) # HACK
|
||||
cp_z3py_to_build()
|
||||
if is_ml_enabled():
|
||||
check_ml()
|
||||
mk_z3consts_ml(api_files)
|
||||
|
||||
# Extract enumeration types from API files, and add python definitions.
|
||||
def mk_z3consts_py(api_files):
|
||||
|
|
@ -2476,6 +2759,171 @@ def mk_z3consts_java(api_files):
|
|||
if VERBOSE:
|
||||
print("Generated '%s'" % ('%s' % gendir))
|
||||
|
||||
# Extract enumeration types from z3_api.h, and add ML definitions
|
||||
def mk_z3consts_ml(api_files):
|
||||
blank_pat = re.compile("^ *$")
|
||||
comment_pat = re.compile("^ *//.*$")
|
||||
typedef_pat = re.compile("typedef enum *")
|
||||
typedef2_pat = re.compile("typedef enum { *")
|
||||
openbrace_pat = re.compile("{ *")
|
||||
closebrace_pat = re.compile("}.*;")
|
||||
|
||||
ml = get_component(ML_COMPONENT)
|
||||
|
||||
DeprecatedEnums = [ 'Z3_search_failure' ]
|
||||
gendir = ml.src_dir
|
||||
if not os.path.exists(gendir):
|
||||
os.mkdir(gendir)
|
||||
|
||||
efile = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w')
|
||||
efile.write('(* Automatically generated file *)\n\n')
|
||||
efile.write('(** The enumeration types of Z3. *)\n\n')
|
||||
for api_file in api_files:
|
||||
api_file_c = ml.find_file(api_file, ml.name)
|
||||
api_file = os.path.join(api_file_c.src_dir, api_file)
|
||||
|
||||
api = open(api_file, 'r')
|
||||
|
||||
SEARCHING = 0
|
||||
FOUND_ENUM = 1
|
||||
IN_ENUM = 2
|
||||
|
||||
mode = SEARCHING
|
||||
decls = {}
|
||||
idx = 0
|
||||
|
||||
linenum = 1
|
||||
for line in api:
|
||||
m1 = blank_pat.match(line)
|
||||
m2 = comment_pat.match(line)
|
||||
if m1 or m2:
|
||||
# skip blank lines and comments
|
||||
linenum = linenum + 1
|
||||
elif mode == SEARCHING:
|
||||
m = typedef_pat.match(line)
|
||||
if m:
|
||||
mode = FOUND_ENUM
|
||||
m = typedef2_pat.match(line)
|
||||
if m:
|
||||
mode = IN_ENUM
|
||||
decls = {}
|
||||
idx = 0
|
||||
elif mode == FOUND_ENUM:
|
||||
m = openbrace_pat.match(line)
|
||||
if m:
|
||||
mode = IN_ENUM
|
||||
decls = {}
|
||||
idx = 0
|
||||
else:
|
||||
assert False, "Invalid %s, line: %s" % (api_file, linenum)
|
||||
else:
|
||||
assert mode == IN_ENUM
|
||||
words = re.split('[^\-a-zA-Z0-9_]+', line)
|
||||
m = closebrace_pat.match(line)
|
||||
if m:
|
||||
name = words[1]
|
||||
if name not in DeprecatedEnums:
|
||||
efile.write('(** %s *)\n' % name[3:])
|
||||
efile.write('type %s =\n' % name[3:]) # strip Z3_
|
||||
for k, i in decls.items():
|
||||
efile.write(' | %s \n' % k[3:]) # strip Z3_
|
||||
efile.write('\n')
|
||||
efile.write('(** Convert %s to int*)\n' % name[3:])
|
||||
efile.write('let int_of_%s x : int =\n' % (name[3:])) # strip Z3_
|
||||
efile.write(' match x with\n')
|
||||
for k, i in decls.items():
|
||||
efile.write(' | %s -> %d\n' % (k[3:], i))
|
||||
efile.write('\n')
|
||||
efile.write('(** Convert int to %s*)\n' % name[3:])
|
||||
efile.write('let %s_of_int x : %s =\n' % (name[3:],name[3:])) # strip Z3_
|
||||
efile.write(' match x with\n')
|
||||
for k, i in decls.items():
|
||||
efile.write(' | %d -> %s\n' % (i, k[3:]))
|
||||
# use Z3.Exception?
|
||||
efile.write(' | _ -> raise (Failure "undefined enum value")\n\n')
|
||||
mode = SEARCHING
|
||||
else:
|
||||
if words[2] != '':
|
||||
if len(words[2]) > 1 and words[2][1] == 'x':
|
||||
idx = int(words[2], 16)
|
||||
else:
|
||||
idx = int(words[2])
|
||||
decls[words[1]] = idx
|
||||
idx = idx + 1
|
||||
linenum = linenum + 1
|
||||
if VERBOSE:
|
||||
print ('Generated "%s/z3enums.ml"' % ('%s' % gendir))
|
||||
efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w')
|
||||
efile.write('(* Automatically generated file *)\n\n')
|
||||
efile.write('(** The enumeration types of Z3. *)\n\n')
|
||||
for api_file in api_files:
|
||||
api_file_c = ml.find_file(api_file, ml.name)
|
||||
api_file = os.path.join(api_file_c.src_dir, api_file)
|
||||
|
||||
api = open(api_file, 'r')
|
||||
|
||||
SEARCHING = 0
|
||||
FOUND_ENUM = 1
|
||||
IN_ENUM = 2
|
||||
|
||||
mode = SEARCHING
|
||||
decls = {}
|
||||
idx = 0
|
||||
|
||||
linenum = 1
|
||||
for line in api:
|
||||
m1 = blank_pat.match(line)
|
||||
m2 = comment_pat.match(line)
|
||||
if m1 or m2:
|
||||
# skip blank lines and comments
|
||||
linenum = linenum + 1
|
||||
elif mode == SEARCHING:
|
||||
m = typedef_pat.match(line)
|
||||
if m:
|
||||
mode = FOUND_ENUM
|
||||
m = typedef2_pat.match(line)
|
||||
if m:
|
||||
mode = IN_ENUM
|
||||
decls = {}
|
||||
idx = 0
|
||||
elif mode == FOUND_ENUM:
|
||||
m = openbrace_pat.match(line)
|
||||
if m:
|
||||
mode = IN_ENUM
|
||||
decls = {}
|
||||
idx = 0
|
||||
else:
|
||||
assert False, "Invalid %s, line: %s" % (api_file, linenum)
|
||||
else:
|
||||
assert mode == IN_ENUM
|
||||
words = re.split('[^\-a-zA-Z0-9_]+', line)
|
||||
m = closebrace_pat.match(line)
|
||||
if m:
|
||||
name = words[1]
|
||||
if name not in DeprecatedEnums:
|
||||
efile.write('(** %s *)\n' % name[3:])
|
||||
efile.write('type %s =\n' % name[3:]) # strip Z3_
|
||||
for k, i in decls.items():
|
||||
efile.write(' | %s \n' % k[3:]) # strip Z3_
|
||||
efile.write('\n')
|
||||
efile.write('(** Convert %s to int*)\n' % name[3:])
|
||||
efile.write('val int_of_%s : %s -> int\n' % (name[3:], name[3:])) # strip Z3_
|
||||
efile.write('(** Convert int to %s*)\n' % name[3:])
|
||||
efile.write('val %s_of_int : int -> %s\n' % (name[3:],name[3:])) # strip Z3_
|
||||
efile.write('\n')
|
||||
mode = SEARCHING
|
||||
else:
|
||||
if words[2] != '':
|
||||
if len(words[2]) > 1 and words[2][1] == 'x':
|
||||
idx = int(words[2], 16)
|
||||
else:
|
||||
idx = int(words[2])
|
||||
decls[words[1]] = idx
|
||||
idx = idx + 1
|
||||
linenum = linenum + 1
|
||||
if VERBOSE:
|
||||
print ('Generated "%s/z3enums.mli"' % ('%s' % gendir))
|
||||
|
||||
def mk_gui_str(id):
|
||||
return '4D2F40D8-E5F9-473B-B548-%012d' % id
|
||||
|
||||
|
|
@ -2633,3 +3081,5 @@ def mk_unix_dist(build_path, dist_path):
|
|||
if __name__ == '__main__':
|
||||
import doctest
|
||||
doctest.testmod()
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue