diff options
Diffstat (limited to 'academic/cvc4')
-rw-r--r-- | academic/cvc4/README | 11 | ||||
-rw-r--r-- | academic/cvc4/cvc4.SlackBuild | 115 | ||||
-rw-r--r-- | academic/cvc4/cvc4.info | 12 | ||||
-rw-r--r-- | academic/cvc4/run-antlr | 2 | ||||
-rw-r--r-- | academic/cvc4/slack-desc | 19 |
5 files changed, 159 insertions, 0 deletions
diff --git a/academic/cvc4/README b/academic/cvc4/README new file mode 100644 index 0000000000..ed00fa62b8 --- /dev/null +++ b/academic/cvc4/README @@ -0,0 +1,11 @@ +CVC4 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. CVC4 supports +arithmetic, reasoning about arrays, and several other built-in +theories. Input problems are written in SMT-LIB format. + +This package includes the cvc4 program, libraries, and Python 2 +bindings. + +Note that this SlackBuild builds CVC4 with readline support, which means +the resulting executable is licensed under the GPLv3. diff --git a/academic/cvc4/cvc4.SlackBuild b/academic/cvc4/cvc4.SlackBuild new file mode 100644 index 0000000000..d3a964cf03 --- /dev/null +++ b/academic/cvc4/cvc4.SlackBuild @@ -0,0 +1,115 @@ +#!/bin/sh + +# Slackware build script for cvc4 + +# Copyright 2019-2020 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. + +# TO DO: +# Add new Python bindings (requires a newer version of Cython?) +# Add Java bindings (requires a newer version of CMake?) + +PRGNAM=cvc4 +VERSION=${VERSION:-1.8} +BUILD=${BUILD:-1} +TAG=${TAG:-_SBo} +SRCNAM=CVC4 + +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 $SRCNAM-$VERSION +tar xvf $CWD/$SRCNAM-$VERSION.tar.gz +cd $SRCNAM-$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 {} \; + +sed -i "s/LIBRARY_INSTALL_DIR lib/&${LIBDIRSUFFIX}/" CMakeLists.txt +install -m 755 $CWD/run-antlr . +cp $CWD/antlr-3.4-complete.jar . + +cmake \ + -DCMAKE_C_FLAGS:STRING="$SLKCFLAGS" \ + -DCMAKE_CXX_FLAGS:STRING="$SLKCFLAGS" \ + -DCMAKE_INSTALL_PREFIX=/usr \ + -DCMAKE_BUILD_TYPE=Production \ + -DANTLR_INCLUDE_DIR=/usr/include/antlr3 \ + -DANTLR_BINARY="$TMP/$SRCNAM-$VERSION/run-antlr" \ + -DUSE_READLINE=OFF \ + -DBUILD_BINDINGS_PYTHON=OFF \ + -DBUILD_SWIG_BINDINGS_PYTHON=ON \ + -DBUILD_SWIG_BINDINGS_JAVA=OFF \ + . + +make +make install DESTDIR=$PKG + +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 + +mv $PKG/usr/share/man $PKG/usr/man + +find $PKG/usr/man -type f -exec gzip -9 {} \; +for i in $( find $PKG/usr/man -type l ) ; do ln -s $( readlink $i ).gz $i.gz ; rm $i ; done + +mkdir -p $PKG/usr/doc/$PRGNAM-$VERSION +cp -a \ + AUTHORS COPYING NEWS README.md THANKS \ + $PKG/usr/doc/$PRGNAM-$VERSION +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/cvc4/cvc4.info b/academic/cvc4/cvc4.info new file mode 100644 index 0000000000..4fc4ede8c6 --- /dev/null +++ b/academic/cvc4/cvc4.info @@ -0,0 +1,12 @@ +PRGNAM="cvc4" +VERSION="1.8" +HOMEPAGE="https://cvc4.cs.stanford.edu/" +DOWNLOAD="https://github.com/CVC4/CVC4/archive/1.8/CVC4-1.8.tar.gz \ + https://www.antlr3.org/download/antlr-3.4-complete.jar" +MD5SUM="9f7657e21fec3c4042225b0b8f513c34 \ + 1b91dea1c7d480b3223f7c8a9aa0e172" +DOWNLOAD_x86_64="" +MD5SUM_x86_64="" +REQUIRES="jdk libantlr3c python-toml" +MAINTAINER="Nick Smallbone" +EMAIL="nick@smallbone.se" diff --git a/academic/cvc4/run-antlr b/academic/cvc4/run-antlr new file mode 100644 index 0000000000..26f09c7cac --- /dev/null +++ b/academic/cvc4/run-antlr @@ -0,0 +1,2 @@ +#!/bin/bash +exec java -jar $(dirname $0)/antlr-3.4-complete.jar $* diff --git a/academic/cvc4/slack-desc b/academic/cvc4/slack-desc new file mode 100644 index 0000000000..7916878a78 --- /dev/null +++ b/academic/cvc4/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------------------------------------------------------| +cvc4: cvc4 (a first-order theorem prover and SMT solver) +cvc4: +cvc4: CVC4 is an automated theorem prover and satisfiability modulo +cvc4: theories (SMT) solver. Given a formula in first-order logic, it +cvc4: attempts to either prove the formula or find a counterexample. CVC4 +cvc4: supports arithmetic, reasoning about arrays, and several other +cvc4: built-in theories. Input problems are written in SMT-LIB format. +cvc4: +cvc4: This package includes the cvc4 program as well as libraries. +cvc4: +cvc4: Homepage: https://cvc4.cs.stanford.edu/ |