Add sci-mathematics/boolector

[shuber-gentoo-overlay.git] / sci-mathematics / boolector / files / pathfixes.patch

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
+