# $FreeBSD$

PORTNAME=	z3

PORTVERSION=	4.4.0

CATEGORIES=	math

MAINTAINER=     6yearold@gmail.com

COMMENT=        Z3 Theorem Prover

LICENSE=	MIT

USE_GITHUB=	yes

GH_ACCOUNT=	Z3Prover

GH_TAGNAME=	z3-${PORTVERSION}

OPTIONS_DEFINE=		STATIC \

#GMP

#there is some problem on C++ side when compiling with GMP

OPTIONS_DEFAULT=	STATIC

OPTIONS_SUB=		yes

STATIC_DESC=		Build static z3 library

STATIC_CONFIGURE_ON=	--staticlib

GMP_DESC=		Use GMP library for AP arithmetic

GMP_CONFIGURE_ON=	--gmp

GMP_CXXFLAGS=		-I${LOCALBASE}include

GMP_LDFLAGS=		-L${LOCALBASE}/lib

GMP_LIB_DEPENDS=	libgmp.so:${PORTSDIR}/math/gmp

HAS_CONFIGURE=		yes

BUILD_WRKSRC=		${WRKSRC}/build

INSTALL_WRKSRC=		${WRKSRC}/build

.if defined(WITH_DEBUG)

CONFIGURE_ARGS+=	--debug

.endif

USES=		python

pre-build:

	${MKDIR} ${STAGEDIR}/${PYTHON_SITELIBDIR}

.include <bsd.port.mk>

SHA256 (Z3Prover-z3-4.4.0-z3-4.4.0_GH0.tar.gz) = 65b72f9eb0af50949e504b47080fb3fc95f11c435633041d9a534473f3142cba

SIZE (Z3Prover-z3-4.4.0-z3-4.4.0_GH0.tar.gz) = 3060731

--- scripts/mk_util.py.orig	2015-04-29 14:40:46 UTC

+++ scripts/mk_util.py

@@ -948,7 +948,7 @@ class LibComponent(Component):

     def mk_install(self, out):

         for include in self.includes2install:

-            out.write('\t@cp %s %s\n' % (os.path.join(self.to_src_dir, include), os.path.join('$(PREFIX)', 'include', include)))

+            out.write('\t@cp %s %s\n' % (os.path.join(self.to_src_dir, include), os.path.join('$(DESTDIR)/$(PREFIX)', 'include', include)))

     def mk_uninstall(self, out):

         for include in self.includes2install:

@@ -1034,7 +1034,7 @@ class ExeComponent(Component):

     def mk_install(self, out):

         if self.install:

             exefile = '%s$(EXE_EXT)' % self.exe_name

-            out.write('\t@cp %s %s\n' % (exefile, os.path.join('$(PREFIX)', 'bin', exefile)))

+            out.write('\t@cp %s %s\n' % (exefile, os.path.join('$(DESTDIR)/$(PREFIX)', 'bin', exefile)))

     def mk_uninstall(self, out):

         exefile = '%s$(EXE_EXT)' % self.exe_name

@@ -1180,11 +1180,11 @@ class DLLComponent(Component):

     def mk_install(self, out):

         if 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 %s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))

+            out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(DESTDIR)/$(PREFIX)', 'lib', dllfile)))

+            out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(DESTDIR)' + PYTHON_PACKAGE_DIR, dllfile)))

             if self.static:

                 libfile = '%s$(LIB_EXT)' % self.dll_name

-                out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(PREFIX)', 'lib', libfile)))

+                out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(DESTDIR)/$(PREFIX)', 'lib', libfile)))

     def mk_uninstall(self, out):

@@ -1359,8 +1359,8 @@ class JavaDLLComponent(Component):

     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)))

+            out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(DESTDIR)/$(PREFIX)', 'lib', dllfile)))

+            out.write('\t@cp %s.jar %s.jar\n' % (self.package_name, os.path.join('$(DESTDIR)/$(PREFIX)', 'lib', self.package_name)))

     def mk_uninstall(self, out):

         if is_java_enabled() and self.install:

@@ -1873,6 +1873,7 @@ def mk_config():

             CPPFLAGS     = '%s -D_TRACE' % CPPFLAGS

         CXXFLAGS         = '%s -msse -msse2' % CXXFLAGS

         config.write('PREFIX=%s\n' % PREFIX)

+        config.write('DESTDIR?=\n')

         config.write('CC=%s\n' % CC)

         config.write('CXX=%s\n' % CXX)

         config.write('CXXFLAGS=%s %s\n' % (CPPFLAGS, CXXFLAGS))

@@ -1926,12 +1927,12 @@ def mk_install(out):

     out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'lib'))

     for c in get_components():

         c.mk_install(out)

-    out.write('\t@cp z3*.py %s\n' % PYTHON_PACKAGE_DIR)

+    out.write('\t@cp z3*.py %s\n' % ('$(DESTDIR)/' + PYTHON_PACKAGE_DIR))

     if sys.version >= "3":

         out.write('\t@cp %s*.pyc %s\n' % (os.path.join('__pycache__', 'z3'),

-                                          os.path.join(PYTHON_PACKAGE_DIR, '__pycache__')))

+                                          os.path.join('$(DESTDIR)/' + PYTHON_PACKAGE_DIR, '__pycache__')))

     else:

-        out.write('\t@cp z3*.pyc %s\n' % PYTHON_PACKAGE_DIR)

+        out.write('\t@cp z3*.pyc %s\n' % ('$(DESTDIR)/' + PYTHON_PACKAGE_DIR))

     out.write('\t@echo Z3 was successfully installed.\n')

     if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():

         if os.uname()[0] == 'Darwin':

Z3 is a high-performance theorem prover developed

at Microsoft Research.

WWW: https://github.com/Z3Prover/z3

bin/z3

include/z3++.h

include/z3.h

include/z3_algebraic.h

include/z3_api.h

include/z3_fpa.h

include/z3_interp.h

include/z3_macros.h

include/z3_polynomial.h

include/z3_rcf.h

include/z3_v1.h

%%STATIC%%lib/libz3.a

lib/libz3.so

%%PYTHON_SITELIBDIR%%/libz3.so

%%PYTHON_SITELIBDIR%%/z3.py

%%PYTHON_SITELIBDIR%%/z3.pyc

%%PYTHON_SITELIBDIR%%/z3consts.py

%%PYTHON_SITELIBDIR%%/z3consts.pyc

%%PYTHON_SITELIBDIR%%/z3core.py

%%PYTHON_SITELIBDIR%%/z3core.pyc

%%PYTHON_SITELIBDIR%%/z3num.py

%%PYTHON_SITELIBDIR%%/z3num.pyc

%%PYTHON_SITELIBDIR%%/z3poly.py

%%PYTHON_SITELIBDIR%%/z3poly.pyc

%%PYTHON_SITELIBDIR%%/z3printer.py

%%PYTHON_SITELIBDIR%%/z3printer.pyc

%%PYTHON_SITELIBDIR%%/z3rcf.py

%%PYTHON_SITELIBDIR%%/z3rcf.pyc

%%PYTHON_SITELIBDIR%%/z3test.py

%%PYTHON_SITELIBDIR%%/z3test.pyc

%%PYTHON_SITELIBDIR%%/z3types.py

%%PYTHON_SITELIBDIR%%/z3types.pyc

%%PYTHON_SITELIBDIR%%/z3util.py

%%PYTHON_SITELIBDIR%%/z3util.pyc