Z3 is a high-performance theorem prover developed

at Microsoft Research.

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

PR:		202136
Submitted by:	6yearold@gmail.com

6 files changed, 155 insertions, 0 deletions

diff --git a/math/Makefile b/math/Makefile
index 4f3944706854..4ec2f0f4f9e8 100644
--- a/math/Makefile
+++ b/math/Makefile
@@ -688,5 +688,6 @@
     SUBDIR += xppaut
     SUBDIR += xspread
     SUBDIR += yacas
+    SUBDIR += z3
 
 .include <bsd.port.subdir.mk>
diff --git a/math/z3/Makefile b/math/z3/Makefile
new file mode 100644
index 000000000000..8612fd6f88d4
--- /dev/null
+++ b/math/z3/Makefile
@@ -0,0 +1,44 @@
+# $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
+
+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
+USE_LDCONFIG=		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>
diff --git a/math/z3/distinfo b/math/z3/distinfo
new file mode 100644
index 000000000000..9748d69f04bc
--- /dev/null
+++ b/math/z3/distinfo
@@ -0,0 +1,2 @@
+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
diff --git a/math/z3/files/patch-scripts_mk__util.py b/math/z3/files/patch-scripts_mk__util.py
new file mode 100644
index 000000000000..87fea5e606c9
--- /dev/null
+++ b/math/z3/files/patch-scripts_mk__util.py
@@ -0,0 +1,70 @@
+--- 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':
diff --git a/math/z3/pkg-descr b/math/z3/pkg-descr
new file mode 100644
index 000000000000..18ec9996b873
--- /dev/null
+++ b/math/z3/pkg-descr
@@ -0,0 +1,4 @@
+Z3 is a high-performance theorem prover developed
+at Microsoft Research.
+
+WWW: https://github.com/Z3Prover/z3
diff --git a/math/z3/pkg-plist b/math/z3/pkg-plist
new file mode 100644
index 000000000000..0a77495b98ad
--- /dev/null
+++ b/math/z3/pkg-plist
@@ -0,0 +1,34 @@
+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