diff options
author | alan_NaverOsa@lavSaPbiAtM.com <alan_NaverOsa@lavSaPbiAtM.com> | 2024-04-14 10:59:06 +0700 |
---|---|---|
committer | Willy Sudiarto Raharjo <willysr@slackbuilds.org> | 2024-04-14 12:05:18 +0700 |
commit | df4e060a184822c8b1c25f34c1f0ce2676f7453b (patch) | |
tree | 16edb9f013bf963655aeec0403a51c294aa42adb /academic/kissat | |
parent | 5118f7868b5d7c3bd3bdf22249912be8c630e995 (diff) |
academic/kissat: Added (SAT solver).
Signed-off-by: Willy Sudiarto Raharjo <willysr@slackbuilds.org>
Diffstat (limited to 'academic/kissat')
-rw-r--r-- | academic/kissat/README | 16 | ||||
-rw-r--r-- | academic/kissat/kissat.SlackBuild | 113 | ||||
-rw-r--r-- | academic/kissat/kissat.info | 10 | ||||
-rw-r--r-- | academic/kissat/slack-desc | 19 |
4 files changed, 158 insertions, 0 deletions
diff --git a/academic/kissat/README b/academic/kissat/README new file mode 100644 index 0000000000000..27b8882eb36bf --- /dev/null +++ b/academic/kissat/README @@ -0,0 +1,16 @@ +Kissat is a "keep it simple and clean bare metal SAT solver" written +in C. It is a port of CaDiCaL back to C with improved data +structures, better scheduling of inprocessing and optimized +algorithms and implementation. + +Coincidentally "kissat" also means "cats" in Finnish. + +You can get more information about Kissat in the last solver +description for the SAT Competition 2022: + +Armin Biere and Mathias Fleury. Gimsatul, IsaSAT and Kissat entering +the SAT Competition 2022. In Proc. of SAT Competition 2022 - Solver +and Benchmark Descriptions, Tomas Balyo, Marijn Heule, Markus Iser, +Matti Järvisalo, Martin Suda (editors), vol. B-2022-1 of Department +of Computer Science Report Series B, pages 10-11, University of +Helsinki, 2022. diff --git a/academic/kissat/kissat.SlackBuild b/academic/kissat/kissat.SlackBuild new file mode 100644 index 0000000000000..6fdda8acf6498 --- /dev/null +++ b/academic/kissat/kissat.SlackBuild @@ -0,0 +1,113 @@ +#!/bin/bash + +# Slackware build script for kissat + +# Copyright Caterino Tommaso, T.O.P. 2024 USA +# 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. + +cd $(dirname $0) ; CWD=$(pwd) + +PRGNAM=kissat +VERSION=${VERSION:-3.1.1} +BUILD=${BUILD:-1} +TAG=${TAG:-_SBo} +PKGTYPE=${PKGTYPE:-tgz} + +if [ -z "$ARCH" ]; then + case "$( uname -m )" in + i?86) ARCH=i586 ;; + arm*) ARCH=arm ;; + *) ARCH=$( uname -m ) ;; + esac +fi + +if [ ! -z "${PRINT_PACKAGE_NAME}" ]; then + echo "$PRGNAM-$VERSION-$ARCH-$BUILD$TAG.$PKGTYPE" + exit 0 +fi + +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" +elif [ "$ARCH" = "aarch64" ]; 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-rel-$VERSION +tar xvf $CWD/$PRGNAM-rel-$VERSION.tar.gz +cd $PRGNAM-rel-$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" \ +./configure + +cd build +make +cd .. + +mkdir -p $PKG/usr/bin $PKG/usr/lib${LIBDIRSUFFIX} +cp -a build/kissat $PKG/usr/bin/ +cp -a build/libkissat.a $PKG/usr/lib${LIBDIRSUFFIX}/ + +rm -f $PKG/{,usr/}lib${LIBDIRSUFFIX}/*.la + +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 + +rm -f $PKG/usr/info/dir + +find $PKG -name perllocal.pod -o -name ".packlist" -o -name "*.bs" | xargs rm -f || true + +mkdir -p $PKG/usr/doc/$PRGNAM-$VERSION +cp -a \ + CONTRIBUTING LICENSE NEWS.md README.md VERSION \ + $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 diff --git a/academic/kissat/kissat.info b/academic/kissat/kissat.info new file mode 100644 index 0000000000000..cefa036030705 --- /dev/null +++ b/academic/kissat/kissat.info @@ -0,0 +1,10 @@ +PRGNAM="kissat" +VERSION="3.1.1" +HOMEPAGE="https://github.com/arminbiere/kissat" +DOWNLOAD="https://github.com/arminbiere/kissat/archive/refs/tags/rel-3.1.1.tar.gz" +MD5SUM="601d796884d5e9efe2af78dfe77d73ba" +DOWNLOAD_x86_64="" +MD5SUM_x86_64="" +REQUIRES="" +MAINTAINER="Caterino Tommaso, T.O.P." +EMAIL="alan_NaverOsa@lavSaPbiAtM.com (remove capital letters)" diff --git a/academic/kissat/slack-desc b/academic/kissat/slack-desc new file mode 100644 index 0000000000000..02a27e4e5d243 --- /dev/null +++ b/academic/kissat/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------------------------------------------------------| +kissat: kissat (International SAT Competition award-winning SAT solver) +kissat: Kissat is a "keep it simple and clean bare metal SAT solver" written +kissat: in C. It is a port of CaDiCaL back to C with improved data +kissat: structures, better scheduling of inprocessing and optimized +kissat: algorithms and implementation. +kissat: Armin Biere and Mathias Fleury. Gimsatul, IsaSAT and Kissat entering +kissat: the SAT Competition 2022. In Proc. of SAT Competition 2022 - Solver +kissat: and Benchmark Descriptions, Tomas Balyo, Marijn Heule, Markus Iser, +kissat: Matti Jarvisalo, Martin Suda (editors), vol. B-2022-1 of Department +kissat: of Computer Science Report Series B, pages 10-11, University of +kissat: Helsinki, 2022 |