sci-mathematics: remove boolector and lingeling

diff --git a/sci-mathematics/boolector/Manifest b/sci-mathematics/boolector/Manifest
deleted file mode 100644 (file)
index 1b33888..0000000
--- a/sci-mathematics/boolector/Manifest
+++ /dev/null
@@ -1,4 +0,0 @@
-AUX pathfixes.patch 1613 BLAKE2B 54d1c9723e33f58d77f0534918397b5257384b804242571099e94ce3e18b29460c2f8f15d841ca6b236064b3556166d29453185630f7ba6d0dc9aeed625cfcd0 SHA512 7efd68a0ab531a165727626c506f289b4181adca399c7f8dcf05ddbd1e41947df19eb48ef26bd7d9b0b6a0865a49711119caac53da9d4d0870572fdb4b0878fb
-DIST boolector-1.5.116-eeaf10b-121004.tar.gz 187600 BLAKE2B 613c23f63f07575900da3bd9522c12b9b55ffdb4b36ca9146d34ae0b06bf9b1a1f539682e6d362abd8b78a7800ae5d0e2a382252756a351c5f17c93f0261d993 SHA512 e38399280d2fa799b17f956adb21f53187e2a6e25ae09cc52403929e7cdc1ef7dce28b19eb27f5f3faaaba7e99c67c0ce0727979b467c04617da80d73a44c217
-EBUILD boolector-1.5.116.ebuild 728 BLAKE2B 9cde12f7f7ec0ddc1e0f02d362c4210fc3712665cd8635ffb2ed6d22639ac02329c38f401c574cfde230ad65e5eb5b36cd31526e23759721b62087f370323ab6 SHA512 d8df094d7de1bb3a75494a13bc18b7d59bde5e182883c28bb0a33bb10a68a80f25c1d0a940500ee7d8a64ce3dcdd4c1c8fc5ace5d3e12b880babb2781b0ea44a
-MISC metadata.xml 243 BLAKE2B 889d08efb220a9fb8457500f5f3c33c8c737616995e19fa8b621ced4bc9d380d016413d098d4d09925c679cd23f7fbd75e495424fe6ed809a9e873014caae682 SHA512 f9051a65d7e11d7abd1b9568dbbf8be84a6ae68eb994b0c22d57dff5620047d5ad5a324057a5cf4cec10837d16024e5f21a8cf5f1a6247807f62931839eb73bc

diff --git a/sci-mathematics/boolector/boolector-1.5.116.ebuild b/sci-mathematics/boolector/boolector-1.5.116.ebuild
deleted file mode 100644 (file)
index e361367..0000000
--- a/sci-mathematics/boolector/boolector-1.5.116.ebuild
+++ /dev/null
@@ -1,34 +0,0 @@
-# Copyright 1999-2013 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: $
-
-EAPI=8
-
-DESCRIPTION="Boolector is an SMT solver for bit-vectors and arrays"
-HOMEPAGE="http://fmv.jku.at/boolector/"
-SRC_URI="http://fmv.jku.at/boolector/boolector-1.5.116-eeaf10b-121004.tar.gz"
-S=${WORKDIR}/boolector-1.5.116-eeaf10b-121004
-
-LICENSE="boolector"
-SLOT="0"
-KEYWORDS="~x86 ~amd64"
-IUSE=""
-
-DEPEND="
-       sci-mathematics/lingeling"
-RDEPEND="${DEPEND}"
-
-src_prepare() {
-       epatch ${FILESDIR}/pathfixes.patch
-}
-
-src_configure() {
-       ./configure --lingeling --no-picosat --no-minisat
-}
-
-src_install() {
-       dodoc NEWS VERSION
-       dobin boolector synthebtor deltabtor
-       dolib libboolector.a
-       doheader boolector.h
-}

diff --git a/sci-mathematics/boolector/files/pathfixes.patch b/sci-mathematics/boolector/files/pathfixes.patch
deleted file mode 100644 (file)
index a378fd4..0000000
--- a/sci-mathematics/boolector/files/pathfixes.patch
+++ /dev/null
@@ -1,68 +0,0 @@
-diff --git a/btorexp.c b/btorexp.c
-index fe2bddf..0d9edd6 100644
---- a/btorexp.c
-+++ b/btorexp.c
-@@ -8267,7 +8267,7 @@ BTOR_SPLIT_SLICES_RESTART:
- #ifndef BTOR_DO_NOT_PROCESS_SKELETON
- /*------------------------------------------------------------------------*/
- 
--#include "../lingeling/lglib.h"
-+#include <lglib.h>
- 
- static int
- btor_fixed_exp (Btor * btor, BtorNode * exp)
-diff --git a/btorsat.c b/btorsat.c
-index 611c616..b54e4a6 100644
---- a/btorsat.c
-+++ b/btorsat.c
-@@ -14,7 +14,7 @@
- #endif
- 
- #ifdef BTOR_USE_LINGELING
--#include "../lingeling/lglib.h"
-+#include <lglib.h>
- #endif
- 
- #ifdef BTOR_USE_MINISAT
-diff --git a/configure b/configure
-index 13b1ffe..a6a1305 100755
---- a/configure
-+++ b/configure
-@@ -179,36 +179,13 @@ then
-   msg "not using Lingeling as requested by command line option"
- else
- 
--  if [ -d ../lingeling ]
--  then
--    for path in ../lingeling/lglib.h ../lingeling/liblgl.a allfound
--    do
--      [ -f $path ] || break
--    done
--  else
--    path=../lingeling
--  fi
--
--  if [ $path = allfound ]
--  then
--    msg "using Lingeling in '../lingeling'"
--    lingeling=yes
--  elif [ $lingeling = yes ]
--  then
--    die "impossible to use Lingeling: '$path' missing"
--  else
--    msg "disabling Lingeling: '$path' missing"
--    lingeling=no
--  fi
--
-   if [ $lingeling = yes ]
-   then
-     [ X"$CFLAGS" = X ] || CFLAGS="$CFLAGS "
-     [ X"$LDEPS" = X ] || LDEPS="$LDEPS "
-     [ X"$LIBS" = X ] || LIBS="$LIBS "
-     CFLAGS="${CFLAGS}-DBTOR_USE_LINGELING"
--    LIBS="${LIBS}-L../lingeling -llgl"
--    LDEPS="${LDEPS}../lingeling/liblgl.a"
-+    LIBS="${LIBS} -llgl"
-     LIBM=yes
-   fi
- 

diff --git a/sci-mathematics/boolector/metadata.xml b/sci-mathematics/boolector/metadata.xml
deleted file mode 100644 (file)
index 9434230..0000000
--- a/sci-mathematics/boolector/metadata.xml
+++ /dev/null
@@ -1,8 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
-<pkgmetadata>
-       <maintainer type="person">
-               <email>shuber@sthu.org</email>
-               <name>Stefan Huber</name>
-       </maintainer>
-</pkgmetadata>

diff --git a/sci-mathematics/lingeling/Manifest b/sci-mathematics/lingeling/Manifest
deleted file mode 100644 (file)
index 1c1077c..0000000
--- a/sci-mathematics/lingeling/Manifest
+++ /dev/null
@@ -1,3 +0,0 @@
-DIST lingeling-ala-b02aa1a-121013.tar.gz 166291 BLAKE2B e9b824832559b16c50cea3d7857bced6d07432da9f16ac9e1128c6c40d69e2c0989d22aeb0cb27fad44ab815c6869094715fcbfb2dfbcb55e39cb23ea63532ef SHA512 b7ad6cedef5ebcd03d798ae6b379a10077c657172932a6124a6972d70e87be428148d0a47ba91a67a78a0d413a0de0a13fd3cd1687a04d98434160f27ae9089e
-EBUILD lingeling-1212013.ebuild 576 BLAKE2B ee3d8f4ff294e3ca006b7f1e9461dba200b74a1462d5fcb4d04df1c50070a23afc54e57849189a3646800bbce47c4626f8c9388fb03ad83f43285f16b2d6095c SHA512 74c187b7f253a78aa074c2b412605620f2774e2378cc3cd1af60784a09f15de1b76278270f8c8a3a28ae7d1c91d97a8dcc60ff6263230d2ff75535d6639b050d
-MISC metadata.xml 243 BLAKE2B 889d08efb220a9fb8457500f5f3c33c8c737616995e19fa8b621ced4bc9d380d016413d098d4d09925c679cd23f7fbd75e495424fe6ed809a9e873014caae682 SHA512 f9051a65d7e11d7abd1b9568dbbf8be84a6ae68eb994b0c22d57dff5620047d5ad5a324057a5cf4cec10837d16024e5f21a8cf5f1a6247807f62931839eb73bc

diff --git a/sci-mathematics/lingeling/lingeling-1212013.ebuild b/sci-mathematics/lingeling/lingeling-1212013.ebuild
deleted file mode 100644 (file)
index a46d955..0000000
--- a/sci-mathematics/lingeling/lingeling-1212013.ebuild
+++ /dev/null
@@ -1,29 +0,0 @@
-# Copyright 1999-2013 Gentoo Foundation
-# Distributed under the terms of the GNU General Public License v2
-# $Header: $
-
-EAPI=8
-
-DESCRIPTION="A SAT (boolean satisfiability) solver"
-HOMEPAGE="http://fmv.jku.at/lingeling/"
-SRC_URI="http://fmv.jku.at/lingeling/lingeling-ala-b02aa1a-121013.tar.gz"
-S=${WORKDIR}/lingeling-ala-b02aa1a-121013
-
-LICENSE="GPL"
-SLOT="0"
-KEYWORDS="~x86 ~amd64"
-IUSE=""
-
-DEPEND=""
-RDEPEND="${DEPEND}"
-
-src_configure() {
-       ./configure || die
-}
-
-src_install() {
-       dodoc NEWS VERSION
-       dobin lingeling ilingeling plingeling
-       dolib liblgl.a
-       doheader lglib.h
-}

diff --git a/sci-mathematics/lingeling/metadata.xml b/sci-mathematics/lingeling/metadata.xml
deleted file mode 100644 (file)
index 9434230..0000000
--- a/sci-mathematics/lingeling/metadata.xml
+++ /dev/null
@@ -1,8 +0,0 @@
-<?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE pkgmetadata SYSTEM "http://www.gentoo.org/dtd/metadata.dtd">
-<pkgmetadata>
-       <maintainer type="person">
-               <email>shuber@sthu.org</email>
-               <name>Stefan Huber</name>
-       </maintainer>
-</pkgmetadata>