Package the Z3 theorem prover / SMT solver from Microsoft Research.

6 files changed, 112 insertions, 0 deletions

diff --git a/math/z3/DESCR b/math/z3/DESCR
new file mode 100644
index 00000000000..a15f33fa4ed
--- /dev/null
+++ b/math/z3/DESCR
@@ -0,0 +1,3 @@
+z3 is an open source theorem prover / SMT solver from Microsoft Research.
+
+(SMT stands for "satisfiability modulo theories".)
diff --git a/math/z3/Makefile b/math/z3/Makefile
new file mode 100644
index 00000000000..e1017a4ccd3
--- /dev/null
+++ b/math/z3/Makefile
@@ -0,0 +1,29 @@
+# $NetBSD: Makefile,v 1.1 2015/11/24 05:45:58 dholland Exp $
+
+DISTNAME=	z3-4.4.1
+GITHUB_TAG=	${DISTNAME}
+CATEGORIES=	math
+MASTER_SITES=	${MASTER_SITE_GITHUB:=Z3Prover/}
+PATCHFILES+=	z3-jumbo-patch-20151123.gz
+SITES.z3-jumbo-patch-20151123.gz=\
+			http://www.NetBSD.org/~dholland/patchkits/z3/
+PATCH_DIST_STRIP=	-p1
+
+MAINTAINER=	dholland@NetBSD.org
+HOMEPAGE=	https://github.com/Z3Prover/z3/
+COMMENT=	The Z3 theorem prover / SMT solver
+LICENSE=	mit
+
+WRKSRC=		${WRKDIR}/z3-${DISTNAME}
+HAS_CONFIGURE=	yes
+USE_LANGUAGES=	c c++
+BUILD_DIRS=	build
+PY_PATCHPLIST=	yes
+
+CONFIGURE_ENV+=		PYTHON=${PYTHONBIN}
+CONFIGURE_ARGS+=	--destdir=${DESTDIR} --prefix=${PREFIX}
+
+.include "options.mk"
+
+.include "../../lang/python/extension.mk"
+.include "../../mk/bsd.pkg.mk"
diff --git a/math/z3/PLIST b/math/z3/PLIST
new file mode 100644
index 00000000000..866184fe592
--- /dev/null
+++ b/math/z3/PLIST
@@ -0,0 +1,34 @@
+@comment $NetBSD: PLIST,v 1.1 2015/11/24 05:45:58 dholland Exp $
+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
+lib/libz3.so
+${PYSITELIB}/libz3.so
+${PYSITELIB}/z3.py
+${PYSITELIB}/z3.pyc
+${PYSITELIB}/z3consts.py
+${PYSITELIB}/z3consts.pyc
+${PYSITELIB}/z3core.py
+${PYSITELIB}/z3core.pyc
+${PYSITELIB}/z3num.py
+${PYSITELIB}/z3num.pyc
+${PYSITELIB}/z3poly.py
+${PYSITELIB}/z3poly.pyc
+${PYSITELIB}/z3printer.py
+${PYSITELIB}/z3printer.pyc
+${PYSITELIB}/z3rcf.py
+${PYSITELIB}/z3rcf.pyc
+${PYSITELIB}/z3test.py
+${PYSITELIB}/z3test.pyc
+${PYSITELIB}/z3types.py
+${PYSITELIB}/z3types.pyc
+${PYSITELIB}/z3util.py
+${PYSITELIB}/z3util.pyc
diff --git a/math/z3/distinfo b/math/z3/distinfo
new file mode 100644
index 00000000000..e88bad37193
--- /dev/null
+++ b/math/z3/distinfo
@@ -0,0 +1,11 @@
+$NetBSD: distinfo,v 1.1 2015/11/24 05:45:58 dholland Exp $
+
+SHA1 (z3-4.4.1.tar.gz) = 60094acaa53459ec694899aca9f17aa830875610
+RMD160 (z3-4.4.1.tar.gz) = 2c891e115a5d097dbbda53c1b322c65bc5b679f7
+SHA512 (z3-4.4.1.tar.gz) = 76991a24f47f2b53ceb8d7a9a6be19913c57994ffb6cf6acfe30f61b2e73959cf02a99f656053594fccb5aaf4d1f44b3ae7e51f1c8953b213d738ceeeaea74f8
+Size (z3-4.4.1.tar.gz) = 3347371 bytes
+SHA1 (z3-jumbo-patch-20151123.gz) = d31b8840575536104680bb624b15cc1c2084a7fb
+RMD160 (z3-jumbo-patch-20151123.gz) = eb74bd41125e1b07a7f873774a2c354e3c8ca378
+SHA512 (z3-jumbo-patch-20151123.gz) = c23d363bf53b40c3ccbfc10d03ef3621d6abfa9cf86375e7e853e85a0971db70992173df04df1a895e16d4a9b533e955953455a7533889963d2920a4b48d0056
+Size (z3-jumbo-patch-20151123.gz) = 4395 bytes
+SHA1 (patch-scripts_mk__util.py) = 1ab32d86649c5b3e83e9b20632d21018a1e22617
diff --git a/math/z3/options.mk b/math/z3/options.mk
new file mode 100644
index 00000000000..56fc3630cec
--- /dev/null
+++ b/math/z3/options.mk
@@ -0,0 +1,19 @@
+# $NetBSD: options.mk,v 1.1 2015/11/24 05:45:58 dholland Exp $
+
+PKG_OPTIONS_VAR=	PKG_OPTIONS.z3
+PKG_SUPPORTED_OPTIONS=	ocaml java
+PKG_SUGGESTED_OPTIONS=	ocaml
+
+.include "../../mk/bsd.options.mk"
+
+.if !empty(PKG_OPTIONS:Mocaml)
+CONFIGURE_ARGS+=	--ml
+.include "../../lang/ocaml/buildlink3.mk"
+.endif
+
+.if !empty(PKG_OPTIONS:Mjava)
+# XXX untested
+USE_JAVA=	yes
+CONFIGURE_ARGS+=	--java
+.include "../../mk/java-vm.mk"
+.endif
diff --git a/math/z3/patches/patch-scripts_mk__util.py b/math/z3/patches/patch-scripts_mk__util.py
new file mode 100644
index 00000000000..be3815ced2c
--- /dev/null
+++ b/math/z3/patches/patch-scripts_mk__util.py
@@ -0,0 +1,16 @@
+$NetBSD: patch-scripts_mk__util.py,v 1.1 2015/11/24 05:45:58 dholland Exp $
+
+For pkgsrc, use site-packages rather than dist-packages.
+
+diff -r 59247c69b92d scripts/mk_util.py
+--- scripts/mk_util.py	Mon Nov 23 19:08:36 2015 -0500
++++ scripts/mk_util.py	Mon Nov 23 19:50:45 2015 -0500
+@@ -637,7 +637,7 @@
+             SLOW_OPTIMIZE = True
+         elif not IS_WINDOWS and opt in ('-p', '--prefix'):
+             PREFIX = arg
+-            PYTHON_PACKAGE_DIR = os.path.join(PREFIX, 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'dist-packages')
++            PYTHON_PACKAGE_DIR = os.path.join(PREFIX, 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'site-packages')
+             mk_dir(DESTDIR + PYTHON_PACKAGE_DIR)
+             if sys.version >= "3":
+                 mk_dir(os.path.join(DESTDIR + PYTHON_PACKAGE_DIR, '__pycache__'))