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

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-07-30 09:56:30 -07:00
parent fdcedee887 95845bbb01
commit 6d36e4277a
1 changed files with 31 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/api/python/setup.py
View file

@ -6,6 +6,7 @@ import subprocess
import multiprocessing
import re
from setuptools import setup
from distutils.util import get_platform
from distutils.errors import LibError
from distutils.command.build import build as _build
from distutils.command.sdist import sdist as _sdist
@ -45,13 +46,14 @@ def _clean_bins():
shutil.rmtree(HEADERS_DIR, ignore_errors=True)
def _z3_version():
post = os.getenv('Z3_VERSION_SUFFIX', '')
fn = os.path.join(SRC_DIR, 'scripts', 'mk_project.py')
if os.path.exists(fn):
if os.path.exists(fn):
with open(fn) as f:
for line in f:
n = re.match(".*set_version\((.*), (.*), (.*), (.*)\).*", line)
if not n is None:
return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4)
return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4) + post
return "?.?.?.?"
def _configure_z3():
@ -97,7 +99,10 @@ def _copy_bins():
os.mkdir(os.path.join(HEADERS_DIR, 'c++'))
shutil.copy(os.path.join(BUILD_DIR, LIBRARY_FILE), LIBS_DIR)
shutil.copy(os.path.join(BUILD_DIR, EXECUTABLE_FILE), BINS_DIR)
for fname in ('z3.h', 'z3_v1.h', 'z3_macros.h', 'z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h', 'z3_interp.h', 'z3_fpa.h', os.path.join('c++', 'z3++.h')):
header_files = [x for x in os.listdir(os.path.join(SRC_DIR, 'src', 'api')) if x.endswith('.h')]
header_files += [os.path.join('c++', x) for x in os.listdir(os.path.join(SRC_DIR, 'src', 'api', 'c++')) if x.endswith('.h')]
for fname in header_files:
shutil.copy(os.path.join(SRC_DIR, 'src', 'api', fname), os.path.join(HEADERS_DIR, fname))
def _copy_sources():
@ -118,6 +123,7 @@ def _copy_sources():
os.mkdir(os.path.join(SRC_DIR_LOCAL, 'src', 'api', 'python'))
os.mkdir(os.path.join(SRC_DIR_LOCAL, 'src', 'api', 'python', 'z3'))
open(os.path.join(SRC_DIR_LOCAL, 'src', 'api', 'python', 'z3', '.placeholder'), 'w').close()
open(os.path.join(SRC_DIR_LOCAL, 'src', 'api', 'python', 'z3test.py'), 'w').close()
class build(_build):
def run(self):
@ -148,14 +154,34 @@ class sdist(_sdist):
#try: os.makedirs(os.path.join(ROOT_DIR, 'build'))
#except OSError: pass
if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv:
idx = sys.argv.index('bdist_wheel') + 1
sys.argv.insert(idx, '--plat-name')
name = get_platform()
if 'linux' in name:
# linux_* platform tags are disallowed because the python ecosystem is fubar
# linux builds should be built in the centos 5 vm for maximum compatibility
# see https://github.com/pypa/manylinux
# see also https://github.com/angr/angr-dev/blob/master/admin/bdist.py
sys.argv.insert(idx + 1, 'manylinux1_' + platform.machine())
elif 'mingw' in name:
if platform.architecture()[0] == '64bit':
sys.argv.insert(idx + 1, 'win_amd64')
else:
sys.argv.insert(idx + 1, 'win32')
else:
# https://www.python.org/dev/peps/pep-0425/
sys.argv.insert(idx + 1, name.replace('.', '_').replace('-', '_'))
setup(
name='z3-solver',
version=_z3_version(),
description='an efficient SMT solver library',
long_description='Z3 is a theorem prover from Microsoft Research with support for bitvectors, booleans, arrays, floating point numbers, strings, and other data types.\n\nFor documentation, please read http://z3prover.github.io/api/html/z3.html\n\nIn the event of technical difficulties related to configuration, compiliation, or installation, please submit issues to https://github.com/angr/angr-z3',
author="The Z3 Theorem Prover Project",
maintainer="Andrew Dutcher",
maintainer_email="andrew@andrewdutcher.com",
maintainer="Audrey Dutcher",
maintainer_email="audrey@rhelmot.io",
url='https://github.com/Z3Prover/z3',
license='MIT License',
keywords=['z3', 'smt', 'sat', 'prover', 'theorem'],