summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--math/Makefile1
-rw-r--r--math/lingeling/Makefile43
-rw-r--r--math/lingeling/distinfo3
-rw-r--r--math/lingeling/files/patch-configure.sh20
-rw-r--r--math/lingeling/files/patch-lglib.h10
-rw-r--r--math/lingeling/pkg-descr5
6 files changed, 82 insertions, 0 deletions
diff --git a/math/Makefile b/math/Makefile
index 39079c10d9e5..7493281fb77c 100644
--- a/math/Makefile
+++ b/math/Makefile
@@ -458,6 +458,7 @@
SUBDIR += libxsmm
SUBDIR += lidia
SUBDIR += linbox
+ SUBDIR += lingeling
SUBDIR += linpack
SUBDIR += lis
SUBDIR += lll_spect
diff --git a/math/lingeling/Makefile b/math/lingeling/Makefile
new file mode 100644
index 000000000000..c1439ee74d4b
--- /dev/null
+++ b/math/lingeling/Makefile
@@ -0,0 +1,43 @@
+PORTNAME= lingeling
+DISTVERSION= g20220515
+CATEGORIES= math
+
+MAINTAINER= yuri@FreeBSD.org
+COMMENT= Lingeling SAT Solver
+WWW= http://fmv.jku.at/lingeling/
+
+LICENSE= MIT
+LICENSE_FILE= ${WRKSRC}/COPYING
+
+USES= gmake
+
+USE_GITHUB= yes
+GH_ACCOUNT= arminbiere
+GH_TAGNAME= 72d2b13
+
+BINARY_ALIAS= gcc=${CC}
+
+EXECUTABLES= ilingeling lglddtrace lglmbt lgluntrace lingeling plingeling treengeling
+
+CFLAGS+= -fPIC
+
+PLIST_FILES= ${EXECUTABLES:S/^/bin\//} \
+ include/lglib.h \
+ lib/liblgl.a
+
+do-configure:
+ @cd ${WRKSRC} && \
+ ${SETENV} ${MAKE_ENV} ./configure.sh
+
+do-build:
+ @cd ${WRKSRC} && \
+ ${SETENV} ${MAKE_ENV} ${GMAKE} ${MAKE_ARGS} -j${MAKE_JOBS_NUMBER}
+
+do-install:
+.for e in ${EXECUTABLES}
+ ${INSTALL_PROGRAM} ${WRKSRC}/${e} ${STAGEDIR}${PREFIX}/bin
+.endfor
+ ${INSTALL_DATA} ${WRKSRC}/lglib.h ${STAGEDIR}${PREFIX}/include
+ ${INSTALL_DATA} ${WRKSRC}/liblgl.a ${STAGEDIR}${PREFIX}/lib
+
+.include <bsd.port.mk>
diff --git a/math/lingeling/distinfo b/math/lingeling/distinfo
new file mode 100644
index 000000000000..42c6b889da49
--- /dev/null
+++ b/math/lingeling/distinfo
@@ -0,0 +1,3 @@
+TIMESTAMP = 1672783599
+SHA256 (arminbiere-lingeling-g20220515-72d2b13_GH0.tar.gz) = ad6a7e9ed10e7c49f9c901365bee639508d999f32c0d59b8a43805e6d327c797
+SIZE (arminbiere-lingeling-g20220515-72d2b13_GH0.tar.gz) = 248128
diff --git a/math/lingeling/files/patch-configure.sh b/math/lingeling/files/patch-configure.sh
new file mode 100644
index 000000000000..bb5b86143b46
--- /dev/null
+++ b/math/lingeling/files/patch-configure.sh
@@ -0,0 +1,20 @@
+--- configure.sh.orig 2022-05-15 14:42:39 UTC
++++ configure.sh
+@@ -183,7 +183,7 @@ fi
+
+ [ x"$CC" = x ] && CC=gcc
+
+-CFLAGS="-W -Wall"
++CFLAGS="$CFLAGS -W -Wall"
+ if [ $debug = yes ]
+ then
+ CFLAGS="$CFLAGS -ggdb3"
+@@ -194,7 +194,7 @@ else
+ [ $lto = yes ] && CFLAGS="$CFLAGS -flto -fwhole-program"
+ fi
+
+-LIBS="-lm"
++LIBS="$LDFLAGS -lm"
+ HDEPS=""
+ LDEPS=""
+
diff --git a/math/lingeling/files/patch-lglib.h b/math/lingeling/files/patch-lglib.h
new file mode 100644
index 000000000000..feb638bf8f54
--- /dev/null
+++ b/math/lingeling/files/patch-lglib.h
@@ -0,0 +1,10 @@
+--- lglib.h.orig 2023-01-03 22:21:39 UTC
++++ lglib.h
+@@ -7,6 +7,7 @@
+
+ #include <stdio.h> // for 'FILE'
+ #include <stdlib.h> // for 'int64_t'
++#include <sys/types.h>
+
+ //--------------------------------------------------------------------------
+
diff --git a/math/lingeling/pkg-descr b/math/lingeling/pkg-descr
new file mode 100644
index 000000000000..ca90c4d970fa
--- /dev/null
+++ b/math/lingeling/pkg-descr
@@ -0,0 +1,5 @@
+Lingeling, Plingeling and Treengeling.
+
+The parallel portfolio front-end Plingeling was ranked on the first place on
+unsatisfiable instances in the parallel track of the SAT Competition 2020, and
+second place overall in the parallel track.