Import of pkgsrc-2014Q1
This commit is contained in:
2
math/minisat/DESCR
Normal file
2
math/minisat/DESCR
Normal file
@@ -0,0 +1,2 @@
|
||||
MiniSat is a minimalistic, industrial strength, open-source SAT solver,
|
||||
developed to help researchers and developers alike to get started on SAT.
|
||||
27
math/minisat/Makefile
Normal file
27
math/minisat/Makefile
Normal file
@@ -0,0 +1,27 @@
|
||||
# $NetBSD: Makefile,v 1.2 2014/01/09 14:38:33 jperkin Exp $
|
||||
|
||||
DISTNAME= minisat-2.2.0
|
||||
CATEGORIES= math
|
||||
MASTER_SITES= http://minisat.se/downloads/
|
||||
|
||||
MAINTAINER= pkgsrc-users@NetBSD.org
|
||||
HOMEPAGE= http://minisat.se/
|
||||
COMMENT= Minimalistic yet highly efficient SAT solver
|
||||
LICENSE= mit
|
||||
|
||||
WRKSRC= $(WRKDIR)/minisat
|
||||
USE_LANGUAGES= c++
|
||||
USE_TOOLS+= gmake
|
||||
#BUILD_DIRS= core simp
|
||||
BUILD_DIRS= simp
|
||||
MAKE_ENV= MROOT=$(WRKSRC)
|
||||
BUILD_TARGET= # empty
|
||||
|
||||
INSTALLATION_DIRS+= bin
|
||||
|
||||
do-install:
|
||||
$(INSTALL_PROGRAM) $(WRKSRC)/simp/minisat \
|
||||
$(DESTDIR)$(PREFIX)/bin/minisat
|
||||
|
||||
.include "../../devel/zlib/buildlink3.mk"
|
||||
.include "../../mk/bsd.pkg.mk"
|
||||
2
math/minisat/PLIST
Normal file
2
math/minisat/PLIST
Normal file
@@ -0,0 +1,2 @@
|
||||
@comment $NetBSD: PLIST,v 1.1.1.1 2013/10/28 04:15:11 asau Exp $
|
||||
bin/minisat
|
||||
7
math/minisat/distinfo
Normal file
7
math/minisat/distinfo
Normal file
@@ -0,0 +1,7 @@
|
||||
$NetBSD: distinfo,v 1.3 2014/01/09 14:38:33 jperkin Exp $
|
||||
|
||||
SHA1 (minisat-2.2.0.tar.gz) = dfc25898bf40e00cf04252a42176e0c0600fbc90
|
||||
RMD160 (minisat-2.2.0.tar.gz) = 169ec9116befa9067db9076d26309f7e9ab408dd
|
||||
Size (minisat-2.2.0.tar.gz) = 43879 bytes
|
||||
SHA1 (patch-core_SolverTypes.h) = 969937eaaaac60b5e2b415ce3282797daacc4890
|
||||
SHA1 (patch-utils_System.cc) = b24990458c2abb9fca014ddccd27220a49ea7799
|
||||
25
math/minisat/patches/patch-core_SolverTypes.h
Normal file
25
math/minisat/patches/patch-core_SolverTypes.h
Normal file
@@ -0,0 +1,25 @@
|
||||
$NetBSD: patch-core_SolverTypes.h,v 1.1 2013/11/08 21:15:02 joerg Exp $
|
||||
|
||||
--- core/SolverTypes.h.orig 2013-11-08 20:45:57.000000000 +0000
|
||||
+++ core/SolverTypes.h
|
||||
@@ -42,18 +42,18 @@ namespace Minisat {
|
||||
typedef int Var;
|
||||
#define var_Undef (-1)
|
||||
|
||||
-
|
||||
struct Lit {
|
||||
int x;
|
||||
|
||||
// Use this as a constructor:
|
||||
- friend Lit mkLit(Var var, bool sign = false);
|
||||
+ friend Lit mkLit(Var var, bool sign);
|
||||
|
||||
bool operator == (Lit p) const { return x == p.x; }
|
||||
bool operator != (Lit p) const { return x != p.x; }
|
||||
bool operator < (Lit p) const { return x < p.x; } // '<' makes p, ~p adjacent in the ordering.
|
||||
};
|
||||
|
||||
+Lit mkLit(Var var, bool sign = false);
|
||||
|
||||
inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
|
||||
inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
|
||||
29
math/minisat/patches/patch-utils_System.cc
Normal file
29
math/minisat/patches/patch-utils_System.cc
Normal file
@@ -0,0 +1,29 @@
|
||||
$NetBSD: patch-utils_System.cc,v 1.2 2014/01/09 14:38:33 jperkin Exp $
|
||||
|
||||
Support NetBSD.
|
||||
|
||||
--- utils/System.cc.orig 2010-07-10 16:07:36.000000000 +0000
|
||||
+++ utils/System.cc
|
||||
@@ -72,13 +72,13 @@ double Minisat::memUsedPeak() {
|
||||
double peak = memReadPeak() / 1024;
|
||||
return peak == 0 ? memUsed() : peak; }
|
||||
|
||||
-#elif defined(__FreeBSD__)
|
||||
+#elif defined(__NetBSD__) || defined(__FreeBSD__)
|
||||
|
||||
double Minisat::memUsed(void) {
|
||||
struct rusage ru;
|
||||
getrusage(RUSAGE_SELF, &ru);
|
||||
return (double)ru.ru_maxrss / 1024; }
|
||||
-double MiniSat::memUsedPeak(void) { return memUsed(); }
|
||||
+double Minisat::memUsedPeak(void) { return memUsed(); }
|
||||
|
||||
|
||||
#elif defined(__APPLE__)
|
||||
@@ -92,4 +92,6 @@ double Minisat::memUsed(void) {
|
||||
#else
|
||||
double Minisat::memUsed() {
|
||||
return 0; }
|
||||
+double Minisat::memUsedPeak() {
|
||||
+ return 0; }
|
||||
#endif
|
||||
Reference in New Issue
Block a user