From a2e13bb161cb7663a1f2ecf371e4e2c6a5fc6cf2 Mon Sep 17 00:00:00 2001 From: Nick Smallbone Date: Sat, 23 Mar 2019 07:25:53 +0700 Subject: academic/z3: Added (theorem solver). Signed-off-by: Willy Sudiarto Raharjo --- academic/z3/README | 12 +++++ academic/z3/slack-desc | 19 ++++++++ academic/z3/z3.SlackBuild | 116 ++++++++++++++++++++++++++++++++++++++++++++++ academic/z3/z3.info | 10 ++++ 4 files changed, 157 insertions(+) create mode 100644 academic/z3/README create mode 100644 academic/z3/slack-desc create mode 100644 academic/z3/z3.SlackBuild create mode 100644 academic/z3/z3.info (limited to 'academic/z3') diff --git a/academic/z3/README b/academic/z3/README new file mode 100644 index 0000000000..a1f132277a --- /dev/null +++ b/academic/z3/README @@ -0,0 +1,12 @@ +Z3 is an automated theorem prover and satisfiability modulo theories +(SMT) solver. Given a formula in first-order logic, it attempts to +either prove the formula or find a counterexample. Z3 supports +arithmetic, reasoning about arrays, and several other built-in +theories. Input problems are written in SMT-LIB format. + +This package includes the z3 program as well as the C++ and +Python APIs. By default the Python 2 version of the API is built; +if you also want the Python 3 version, run the SlackBuild with +PYTHON3=yes, like so: + + PYTHON3=yes ./z3.SlackBuild diff --git a/academic/z3/slack-desc b/academic/z3/slack-desc new file mode 100644 index 0000000000..c8a8e4c2c2 --- /dev/null +++ b/academic/z3/slack-desc @@ -0,0 +1,19 @@ +# HOW TO EDIT THIS FILE: +# The "handy ruler" below makes it easier to edit a package description. +# Line up the first '|' above the ':' following the base package name, and +# the '|' on the right side marks the last column you can put a character in. +# You must make exactly 11 lines for the formatting to be correct. It's also +# customary to leave one space after the ':' except on otherwise blank lines. + + |-----handy-ruler------------------------------------------------------| +z3: z3 (a first-order theorem prover and SMT solver) +z3: +z3: Z3 is an automated theorem prover and satisfiability modulo theories +z3: (SMT) solver. Given a formula in first-order logic, it attempts to +z3: either prove the formula or find a counterexample. Z3 supports +z3: arithmetic, reasoning about arrays, and several other built-in +z3: theories. Input problems are written in SMT-LIB format. +z3: +z3: This package includes the z3 program as well as C++ and Python APIs. +z3: +z3: Homepage: https://github.com/Z3Prover/z3/wiki diff --git a/academic/z3/z3.SlackBuild b/academic/z3/z3.SlackBuild new file mode 100644 index 0000000000..bc6dd426f0 --- /dev/null +++ b/academic/z3/z3.SlackBuild @@ -0,0 +1,116 @@ +#!/bin/sh + +# Slackware build script for z3 + +# Copyright 2019 Nick Smallbone, Gothenburg, Sweden +# All rights reserved. +# +# Redistribution and use of this script, with or without modification, is +# permitted provided that the following conditions are met: +# +# 1. Redistributions of this script must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# +# THIS SOFTWARE IS PROVIDED BY THE AUTHOR "AS IS" AND ANY EXPRESS OR IMPLIED +# WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF +# MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO +# EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +# SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; +# OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, +# WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR +# OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF +# ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +PRGNAM=z3 +VERSION=${VERSION:-4.8.4} +BUILD=${BUILD:-1} +TAG=${TAG:-_SBo} + +if [ -z "$ARCH" ]; then + case "$( uname -m )" in + i?86) ARCH=i586 ;; + arm*) ARCH=arm ;; + *) ARCH=$( uname -m ) ;; + esac +fi + +CWD=$(pwd) +TMP=${TMP:-/tmp/SBo} +PKG=$TMP/package-$PRGNAM +OUTPUT=${OUTPUT:-/tmp} + +if [ "$ARCH" = "i586" ]; then + SLKCFLAGS="-O2 -march=i586 -mtune=i686" + LIBDIRSUFFIX="" +elif [ "$ARCH" = "i686" ]; then + SLKCFLAGS="-O2 -march=i686 -mtune=i686" + LIBDIRSUFFIX="" +elif [ "$ARCH" = "x86_64" ]; then + SLKCFLAGS="-O2 -fPIC" + LIBDIRSUFFIX="64" +else + SLKCFLAGS="-O2" + LIBDIRSUFFIX="" +fi + +set -e + +rm -rf $PKG +mkdir -p $TMP $PKG $OUTPUT +cd $TMP +rm -rf $PRGNAM-$PRGNAM-$VERSION +tar xvf $CWD/$PRGNAM-$VERSION.tar.gz +cd $PRGNAM-$PRGNAM-$VERSION +chown -R root:root . +find -L . \ + \( -perm 777 -o -perm 775 -o -perm 750 -o -perm 711 -o -perm 555 \ + -o -perm 511 \) -exec chmod 755 {} \; -o \ + \( -perm 666 -o -perm 664 -o -perm 640 -o -perm 600 -o -perm 444 \ + -o -perm 440 -o -perm 400 \) -exec chmod 644 {} \; + +CFLAGS="$SLKCFLAGS" \ +CXXFLAGS="$SLKCFLAGS" \ +Z3_INSTALL_LIB_DIR=lib${LIBDIRSUFFIX} \ +./configure \ + --prefix=/usr \ + --python + +cd build +make +make install DESTDIR=$PKG +cd ../doc +python mk_api_doc.py +cd .. + +if [ z$PYTHON3 = zyes ]; then + # Copy the Python bindings to python3.X/site-packages. + PYTHON_VERSION=$(python3 -c 'import sys; print("%d.%d" % sys.version_info[:2])') + PYLIB=$PKG/usr/lib${LIBDIRSUFFIX}/python${PYTHON_VERSION}/site-packages + mkdir -p $PYLIB + cp -a build/python/z3 $PYLIB/z3 + find $PYLIB/z3 -name '*.pyc' -delete +fi + +find $PKG -print0 | xargs -0 file | grep -e "executable" -e "shared object" | grep ELF \ + | cut -f 1 -d : | xargs strip --strip-unneeded 2> /dev/null || true + +mkdir -p $PKG/usr/doc/$PRGNAM-$VERSION +cp -a \ + README.md RELEASE_NOTES LICENSE.txt \ + $PKG/usr/doc/$PRGNAM-$VERSION +mkdir -p $PKG/usr/doc/$PRGNAM-$VERSION/examples +cp -a \ + examples/c examples/c++ examples/maxsat examples/python examples/tptp \ + $PKG/usr/doc/$PRGNAM-$VERSION/examples +find $PKG/usr/doc/$PRGNAM-$VERSION/examples -name CMakeLists.txt -delete +cp -a \ + doc/api/html \ + $PKG/usr/doc/$PRGNAM-$VERSION/api +cat $CWD/$PRGNAM.SlackBuild > $PKG/usr/doc/$PRGNAM-$VERSION/$PRGNAM.SlackBuild + +mkdir -p $PKG/install +cat $CWD/slack-desc > $PKG/install/slack-desc + +cd $PKG +/sbin/makepkg -l y -c n $OUTPUT/$PRGNAM-$VERSION-$ARCH-$BUILD$TAG.${PKGTYPE:-tgz} diff --git a/academic/z3/z3.info b/academic/z3/z3.info new file mode 100644 index 0000000000..b193eeb6d8 --- /dev/null +++ b/academic/z3/z3.info @@ -0,0 +1,10 @@ +PRGNAM="z3" +VERSION="4.8.4" +HOMEPAGE="https://github.com/Z3Prover/z3/wiki" +DOWNLOAD="https://github.com/Z3Prover/z3/archive/z3-4.8.4.tar.gz" +MD5SUM="b74bbb04e90c034125fe9e01988add95" +DOWNLOAD_x86_64="" +MD5SUM_x86_64="" +REQUIRES="" +MAINTAINER="Nick Smallbone" +EMAIL="nick@smallbone.se" -- cgit v1.2.3