Add sci-mathematics/boolector

diff --git a/licenses/boolector b/licenses/boolector
new file mode 100644 (file)
index 0000000..32c7a0d
--- /dev/null
+++ b/licenses/boolector
@@ -0,0 +1,41 @@
+Copyright (c) 2007 - 2013,
+Institute for Formal Models and Verification,
+Johannes Kepler University, Linz, Austria.
+
+Permission is hereby granted, free of charge, to use this software for
+evaluation and research purposes.
+
+This license does not allow this software to be used in a commercial context.
+
+It is further prohibited to use this software or a substantial portion of it
+in a competition or a similar competetive event, such as the SAT, SMT or QBF
+competitions or evaluations, without explicit written permission by the
+copyright holder.
+
+However, competition organizers are allowed to use this software as part of
+the evaluation process of a particular competition, evaluation or
+competetive event, if the copyright holder of this software submitted this
+software to this particular competition, evaluation or event explicitly.
+
+This permission of using the software as part of a submission by the
+copyright holder to a competition, evaluation or competive event is only
+granted for one year and only for one particular instance of the competition
+to which this software was submitted by the copyright holder.
+
+If a competition, evaluation or competetive event has multiple tracks,
+categories or sub-competitions, this license is only granted for the tracks
+respectively categories or sub-competitions, to which the software was
+explicitly submitted by the copyright holder.
+
+All other usage is reserved.
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
+FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
+IN THE SOFTWARE.

diff --git a/sci-mathematics/boolector/Manifest b/sci-mathematics/boolector/Manifest
new file mode 100644 (file)
index 0000000..1c69d4e
--- /dev/null
+++ b/sci-mathematics/boolector/Manifest
@@ -0,0 +1,3 @@
+AUX pathfixes.patch 1613 SHA256 532eb084341af629ba51b7fbfbee13d89e435f21082f82257d55572f4b609acd SHA512 7efd68a0ab531a165727626c506f289b4181adca399c7f8dcf05ddbd1e41947df19eb48ef26bd7d9b0b6a0865a49711119caac53da9d4d0870572fdb4b0878fb WHIRLPOOL d246934e41837a7b5d08d84b3f58e9dad21b8b428bd38e597fbc46b5c8dce2afc3bc06f5f6b1fd0a2160323fadb7e8fec7f9e0116271fe682dc6f649a8f915df
+DIST boolector-1.5.116-eeaf10b-121004.tar.gz 187600 SHA256 23dd6d44fe938e62548a9364863850cb87f920bd9f359d3985c7c8f7c26c808d SHA512 e38399280d2fa799b17f956adb21f53187e2a6e25ae09cc52403929e7cdc1ef7dce28b19eb27f5f3faaaba7e99c67c0ce0727979b467c04617da80d73a44c217 WHIRLPOOL 744fff8f381397d099827e3305594d461af827bbc4617a4cfda9b6cb7b7875d2285bd0210aa932bfa60df066e31b5694435654832ec1955da489f01f3f6cf3c0
+EBUILD boolector-1.5.116.ebuild 743 SHA256 2e0c0af46155e9677a7094be7db2f0a7f224334952c4ad8c72de28207b522c87 SHA512 4475d84b315c8b85f62678c9554252b378282b7ab228aaa7eed953d363b075971b7767bb8d2d55345d4dc6002ad66ac1f2e0f36aec95f9299aa3cec402d83e70 WHIRLPOOL ce659773698c2b73e3a1f50a776f20255df3914a80cef02a29dd199c60cb305e2006c91f02a0558cb7dda36d3fc18e14f4ac8c1a094873dc11dc17ed0de3bdf3

diff --git a/sci-mathematics/boolector/boolector-1.5.116.ebuild b/sci-mathematics/boolector/boolector-1.5.116.ebuild
new file mode 100644 (file)
index 0000000..aff2eae
--- /dev/null
+++ b/sci-mathematics/boolector/boolector-1.5.116.ebuild
@@ -0,0 +1,35 @@
+# Copyright 1999-2013 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: $
+
+EAPI=5
+inherit eutils
+
+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
new file mode 100644 (file)
index 0000000..a378fd4
--- /dev/null
+++ b/sci-mathematics/boolector/files/pathfixes.patch
@@ -0,0 +1,68 @@
+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
+