root
8 years ago
parent
50cf0d521f
commit
f88ec4f738
@ -1,11 +0,0 @@
|
||||
--- pyamg/gallery/stencil.py.orig 2011-08-06 20:26:36.000000000 +0100
|
||||
+++ pyamg/gallery/stencil.py 2011-08-06 20:27:12.000000000 +0100
|
||||
@@ -85,7 +85,7 @@
|
||||
|
||||
# compute index offset of each dof within the stencil
|
||||
strides = numpy.cumprod( [1] + list(reversed(grid)) )[:-1]
|
||||
- indices = S.nonzero()
|
||||
+ indices = tuple(i.copy() for i in S.nonzero())
|
||||
for i,s in zip(indices,S.shape):
|
||||
i -= s // 2
|
||||
for stride,coords in zip(strides, reversed(indices)):
|
||||
@ -1,16 +0,0 @@
|
||||
pyamg/amg_core/ruge_stuben.h | 2 ++
|
||||
1 files changed, 2 insertions(+), 0 deletions(-)
|
||||
|
||||
diff --git a/pyamg/amg_core/ruge_stuben.h b/pyamg/amg_core/ruge_stuben.h
|
||||
index 51cec80..d0ff9a9 100644
|
||||
--- a/pyamg/amg_core/ruge_stuben.h
|
||||
+++ b/pyamg/amg_core/ruge_stuben.h
|
||||
@@ -7,6 +7,8 @@
|
||||
#include <cassert>
|
||||
#include <limits>
|
||||
#include <algorithm>
|
||||
+#include "graph.h"
|
||||
+#include "linalg.h"
|
||||
|
||||
/*
|
||||
* Compute a strength of connection matrix using the classical strength
|
||||
@ -1,97 +0,0 @@
|
||||
--- pyfits-3.2.orig/setup.cfg 2014-02-05 14:11:01.244895447 -0800
|
||||
+++ pyfits-3.2/setup.cfg 2014-02-05 14:28:44.175030178 -0800
|
||||
@@ -36,91 +36,12 @@
|
||||
|
||||
[extension=pyfits.compression]
|
||||
sources =
|
||||
- cextern/cfitsio/adler32.c
|
||||
- cextern/cfitsio/buffers.c
|
||||
- cextern/cfitsio/cfileio.c
|
||||
- cextern/cfitsio/checksum.c
|
||||
- cextern/cfitsio/crc32.c
|
||||
- cextern/cfitsio/deflate.c
|
||||
- cextern/cfitsio/drvrfile.c
|
||||
- cextern/cfitsio/drvrgsiftp.c
|
||||
- cextern/cfitsio/drvrmem.c
|
||||
- cextern/cfitsio/drvrnet.c
|
||||
- cextern/cfitsio/drvrsmem.c
|
||||
- cextern/cfitsio/editcol.c
|
||||
- cextern/cfitsio/edithdu.c
|
||||
- cextern/cfitsio/eval_f.c
|
||||
- cextern/cfitsio/eval_l.c
|
||||
- cextern/cfitsio/eval_y.c
|
||||
- cextern/cfitsio/fitscore.c
|
||||
- cextern/cfitsio/fits_hcompress.c
|
||||
- cextern/cfitsio/fits_hdecompress.c
|
||||
- cextern/cfitsio/getcolb.c
|
||||
- cextern/cfitsio/getcol.c
|
||||
- cextern/cfitsio/getcold.c
|
||||
- cextern/cfitsio/getcole.c
|
||||
- cextern/cfitsio/getcoli.c
|
||||
- cextern/cfitsio/getcolj.c
|
||||
- cextern/cfitsio/getcolk.c
|
||||
- cextern/cfitsio/getcoll.c
|
||||
- cextern/cfitsio/getcolsb.c
|
||||
- cextern/cfitsio/getcols.c
|
||||
- cextern/cfitsio/getcolui.c
|
||||
- cextern/cfitsio/getcoluj.c
|
||||
- cextern/cfitsio/getcoluk.c
|
||||
- cextern/cfitsio/getkey.c
|
||||
- cextern/cfitsio/group.c
|
||||
- cextern/cfitsio/grparser.c
|
||||
- cextern/cfitsio/histo.c
|
||||
- cextern/cfitsio/imcompress.c
|
||||
- cextern/cfitsio/infback.c
|
||||
- cextern/cfitsio/inffast.c
|
||||
- cextern/cfitsio/inflate.c
|
||||
- cextern/cfitsio/inftrees.c
|
||||
- cextern/cfitsio/iraffits.c
|
||||
- cextern/cfitsio/modkey.c
|
||||
- cextern/cfitsio/pliocomp.c
|
||||
- cextern/cfitsio/putcolb.c
|
||||
- cextern/cfitsio/putcol.c
|
||||
- cextern/cfitsio/putcold.c
|
||||
- cextern/cfitsio/putcole.c
|
||||
- cextern/cfitsio/putcoli.c
|
||||
- cextern/cfitsio/putcolj.c
|
||||
- cextern/cfitsio/putcolk.c
|
||||
- cextern/cfitsio/putcoll.c
|
||||
- cextern/cfitsio/putcolsb.c
|
||||
- cextern/cfitsio/putcols.c
|
||||
- cextern/cfitsio/putcolu.c
|
||||
- cextern/cfitsio/putcolui.c
|
||||
- cextern/cfitsio/putcoluj.c
|
||||
- cextern/cfitsio/putcoluk.c
|
||||
- cextern/cfitsio/putkey.c
|
||||
- cextern/cfitsio/quantize.c
|
||||
- cextern/cfitsio/region.c
|
||||
- cextern/cfitsio/ricecomp.c
|
||||
- cextern/cfitsio/scalnull.c
|
||||
- cextern/cfitsio/swapproc.c
|
||||
- cextern/cfitsio/trees.c
|
||||
- cextern/cfitsio/uncompr.c
|
||||
- cextern/cfitsio/wcssub.c
|
||||
- cextern/cfitsio/wcsutil.c
|
||||
- cextern/cfitsio/zcompress.c
|
||||
- cextern/cfitsio/zuncompress.c
|
||||
- cextern/cfitsio/zutil.c
|
||||
src/compressionmodule.c
|
||||
include_dirs =
|
||||
numpy
|
||||
- cextern/cfitsio
|
||||
-extra_compile_args =
|
||||
- -Wno-unused-variable
|
||||
- -Wno-parentheses
|
||||
- -Wno-uninitialized
|
||||
- -Wno-format
|
||||
- -Wno-strict-prototypes
|
||||
- -Wno-unused
|
||||
- -Wno-comments
|
||||
- -Wno-switch
|
||||
-optional = True
|
||||
+libraries =
|
||||
+ cfitsio
|
||||
+optional = False
|
||||
fail_message =
|
||||
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
||||
Failed to build PyFITS tile compression support. PyFITS will still
|
||||
@ -1,45 +0,0 @@
|
||||
https://bitbucket.org/lgautier/rpy2/commits/bf38fa9960aa
|
||||
# HG changeset patch
|
||||
# User Laurent Gautier <lgautier@gmail.com>
|
||||
# Date 1415656651 18000
|
||||
# Node ID bf38fa9960aacf7ba24a20cfae631aa695fea986
|
||||
# Parent 9c1212066f5c980a211b21943f62fd69743ca4bd
|
||||
Should fix issue #234
|
||||
|
||||
diff --git a/setup.py b/setup.py
|
||||
--- a/setup.py
|
||||
+++ b/setup.py
|
||||
@@ -136,8 +136,6 @@
|
||||
return output
|
||||
|
||||
def getRinterface_ext():
|
||||
- #r_libs = [os.path.join(RHOME, 'lib'), os.path.join(RHOME, 'modules')]
|
||||
- r_libs = []
|
||||
extra_link_args = []
|
||||
extra_compile_args = []
|
||||
include_dirs = []
|
||||
@@ -250,9 +248,9 @@
|
||||
include_dirs = [os.path.join(package_prefix,
|
||||
'rpy', 'rinterface'),] + include_dirs,
|
||||
libraries = libraries,
|
||||
- library_dirs = r_libs,
|
||||
+ library_dirs = library_dirs,
|
||||
define_macros = define_macros,
|
||||
- runtime_library_dirs = r_libs,
|
||||
+ runtime_library_dirs = library_dirs,
|
||||
extra_compile_args=extra_compile_args,
|
||||
extra_link_args = extra_link_args
|
||||
)
|
||||
@@ -266,9 +264,9 @@
|
||||
include_dirs = include_dirs +
|
||||
[os.path.join('rpy', 'rinterface'), ],
|
||||
libraries = libraries,
|
||||
- library_dirs = r_libs,
|
||||
+ library_dirs = library_dirs,
|
||||
define_macros = define_macros,
|
||||
- runtime_library_dirs = r_libs,
|
||||
+ runtime_library_dirs = library_dirs,
|
||||
extra_compile_args=extra_compile_args,
|
||||
extra_link_args = extra_link_args
|
||||
)
|
||||
|
||||
@ -1,14 +0,0 @@
|
||||
Author: Ole Streicher <olebole@debian.org>
|
||||
Description: Remove the tests that require pytest-mpl
|
||||
Pytest_mpl is (still) not available in Debian.
|
||||
https://github.com/astrofrog/pytest-mpl
|
||||
--- a/setup.cfg
|
||||
+++ b/setup.cfg
|
||||
@@ -11,7 +11,6 @@
|
||||
minversion = 2.2
|
||||
norecursedirs = build docs/_build
|
||||
doctest_plus = enabled
|
||||
-addopts = --mpl --mpl-baseline-path=wcsaxes/tests/baseline_images
|
||||
|
||||
[ah_bootstrap]
|
||||
auto_use = False
|
||||
@ -1,16 +0,0 @@
|
||||
Author: Ole Streicher <olebole@debian.org>
|
||||
Description: Disable test_no_numpy_warnings
|
||||
This test may fails when numpy decides that it wants to put some important
|
||||
message as a warning; even if nothing goes wrong. This happens f.e. for
|
||||
numpy-1.11.0~b2.
|
||||
--- a/wcsaxes/tests/test_misc.py
|
||||
+++ b/wcsaxes/tests/test_misc.py
|
||||
@@ -51,6 +51,8 @@
|
||||
COORDSYS= 'icrs '
|
||||
""", sep='\n')
|
||||
|
||||
+# see https://github.com/astrofrog/wcsaxes/issues/187
|
||||
+@pytest.mark.xfail
|
||||
def test_no_numpy_warnings():
|
||||
|
||||
# Make sure that no warnings are raised if some pixels are outside WCS
|
||||
@ -0,0 +1,52 @@
|
||||
This patch fixes gentoo QA notices against the desktop file (see gentoo bug 460412#3)
|
||||
Based upon patch extracted from upstream git; original patch info:
|
||||
commit 04f73d125365d97fa6f72677ec5d220292690e56
|
||||
Author: Golubev Alexander <fatzer2@gmail.com>
|
||||
Date: Mon Jul 18 13:45:03 2016 +0400
|
||||
|
||||
Remove OnlyShowIn=Unity from clementine.desktop's action sections (#5444)
|
||||
|
||||
diff --git a/dist/clementine.desktop b/dist/clementine.desktop
|
||||
index 2fb9559..9ee881e 100644
|
||||
--- a/dist/clementine.desktop
|
||||
+++ b/dist/clementine.desktop
|
||||
@@ -38,7 +38,6 @@ Actions=Play;Pause;Stop;Previous;Next;
|
||||
[Desktop Action Play]
|
||||
Name=Play
|
||||
Exec=clementine --play
|
||||
-OnlyShowIn=Unity;
|
||||
Name[af]=Speel
|
||||
Name[be]=Прайграць
|
||||
Name[bg]=Възпроизвеждане
|
||||
@@ -89,7 +88,6 @@ Name[zh_TW]=播放
|
||||
[Desktop Action Pause]
|
||||
Name=Pause
|
||||
Exec=clementine --pause
|
||||
-OnlyShowIn=Unity;
|
||||
Name[be]=Прыпыніць
|
||||
Name[bg]=Пауза
|
||||
Name[br]=Ehan
|
||||
@@ -135,7 +133,6 @@ Name[zh_TW]=暫停
|
||||
[Desktop Action Stop]
|
||||
Name=Stop
|
||||
Exec=clementine --stop
|
||||
-OnlyShowIn=Unity;
|
||||
Name[be]=Спыніць
|
||||
Name[bg]=Спиране
|
||||
Name[br]=Paouez
|
||||
@@ -184,7 +181,6 @@ Name[zh_TW]=停止
|
||||
[Desktop Action Previous]
|
||||
Name=Previous
|
||||
Exec=clementine --previous
|
||||
-OnlyShowIn=Unity;
|
||||
Name[af]=Vorige
|
||||
Name[be]=Папярэдні
|
||||
Name[bg]=Предишна
|
||||
@@ -232,7 +228,6 @@ Name[zh_TW]=往前
|
||||
[Desktop Action Next]
|
||||
Name=Next
|
||||
Exec=clementine --next
|
||||
-OnlyShowIn=Unity;
|
||||
Name[af]=Volgende
|
||||
Name[be]=Далей
|
||||
Name[bg]=Следваща
|
||||
@ -0,0 +1,34 @@
|
||||
From 3771a139059cf248cc07cf8a735c0cd95ae3c6af Mon Sep 17 00:00:00 2001
|
||||
From: Mykyta Holubakha <hilobakho@gmail.com>
|
||||
Date: Fri, 9 Sep 2016 00:56:22 +0300
|
||||
Subject: [PATCH] Fix automagic pandoc dependency
|
||||
|
||||
---
|
||||
configure.ac | 11 ++++++++---
|
||||
1 file changed, 8 insertions(+), 3 deletions(-)
|
||||
|
||||
diff --git a/configure.ac b/configure.ac
|
||||
index 45e6d1a..aea9285 100644
|
||||
--- a/configure.ac
|
||||
+++ b/configure.ac
|
||||
@@ -25,9 +25,14 @@ PKG_CHECK_MODULES([glib], [glib-2.0 >= 2.0],, [AC_MSG_ERROR([glib 2.0 or newer i
|
||||
PKG_CHECK_MODULES([libmpdclient], [libmpdclient >= 2.5],, [AC_MSG_ERROR([libmpdclient 2.5 or newer is required])])
|
||||
|
||||
# Check for Pandoc
|
||||
-AC_PATH_PROG(PANDOC,pandoc,no)
|
||||
-if [[ "x$PANDOC" = xno ]]; then
|
||||
- AC_MSG_WARN([The manual page will not be built.])
|
||||
+AC_ARG_WITH([doc], AS_HELP_STRING([--with-doc],[Build the manpage (default: disabled)]))
|
||||
+if [test "x$with_doc" = "xyes"]; then
|
||||
+ AC_PATH_PROG(PANDOC,pandoc,no)
|
||||
+ if [[ "x$PANDOC" = xno ]]; then
|
||||
+ AC_MSG_WARN([The manual page will not be built.])
|
||||
+ fi
|
||||
+else
|
||||
+ PANDOC="no"
|
||||
fi
|
||||
AM_CONDITIONAL([PANDOC], [test "x$PANDOC" != xno])
|
||||
|
||||
--
|
||||
2.10.0
|
||||
|
||||
@ -1 +1 @@
|
||||
Tue, 13 Sep 2016 07:10:35 +0000
|
||||
Tue, 13 Sep 2016 10:40:35 +0000
|
||||
|
||||
@ -1 +1 @@
|
||||
Tue, 13 Sep 2016 07:10:35 +0000
|
||||
Tue, 13 Sep 2016 10:40:35 +0000
|
||||
|
||||
@ -1,13 +1,13 @@
|
||||
DEFINED_PHASES=configure prepare
|
||||
DEPEND=virtual/pkgconfig sys-libs/ncurses:= dev-libs/glib:2 regex? ( dev-libs/boost:= ) !<sys-devel/gettext-0.18.1.1-r3 || ( >=sys-devel/automake-1.15:1.15 ) >=sys-devel/autoconf-2.69 >=sys-devel/libtool-2.4
|
||||
DEPEND=virtual/pkgconfig sys-devel/gettext sys-libs/ncurses:0= dev-libs/glib:2 virtual/libintl regex? ( dev-libs/boost:= ) !<sys-devel/gettext-0.18.1.1-r3 || ( >=sys-devel/automake-1.15:1.15 ) >=sys-devel/autoconf-2.69 >=sys-devel/libtool-2.4
|
||||
DESCRIPTION=Practical Music Search: an open source ncurses client for mpd, written in C++
|
||||
EAPI=6
|
||||
HOMEPAGE=https://ambientsound.github.io/pms/
|
||||
IUSE=regex
|
||||
KEYWORDS=~amd64 ~x86
|
||||
LICENSE=GPL-3
|
||||
RDEPEND=sys-libs/ncurses:= dev-libs/glib:2 regex? ( dev-libs/boost:= )
|
||||
LICENSE=GPL-3+
|
||||
RDEPEND=sys-libs/ncurses:0= dev-libs/glib:2 virtual/libintl regex? ( dev-libs/boost:= )
|
||||
SLOT=0
|
||||
SRC_URI=https://github.com/ambientsound/pms/archive/0.42.tar.gz -> pms-0.42.tar.gz
|
||||
_eclasses_=autotools 07e71b3b5690738ef7e8bc097077e00c eutils b83a2420b796f7c6eff682679d08fe25 flag-o-matic 8632fcd33a047954f007dee9a137bdcc libtool 4890219c51da247200223277f993e054 multilib 165fc17c38d1b11dac2008280dab6e80 toolchain-funcs 6198c04daba0e1307bd844df7d37f423
|
||||
_md5_=e21f1aefa97d6f98073c1307db97c653
|
||||
_md5_=390f6fb7c16a329714655dc8af71d86a
|
||||
|
||||
@ -1,11 +1,11 @@
|
||||
DEFINED_PHASES=configure prepare unpack
|
||||
DEPEND=virtual/pkgconfig sys-libs/ncurses:=[unicode] dev-libs/glib:2 media-libs/libmpdclient !<sys-devel/gettext-0.18.1.1-r3 || ( >=sys-devel/automake-1.15:1.15 ) >=sys-devel/autoconf-2.69 >=sys-devel/libtool-2.4 >=dev-vcs/git-1.8.2.1
|
||||
DEFINED_PHASES=configure prepare pretend unpack
|
||||
DEPEND=virtual/pkgconfig dev-util/intltool sys-devel/gettext doc? ( app-text/pandoc ) sys-libs/ncurses:0=[unicode] dev-libs/glib:2 media-libs/libmpdclient virtual/libintl !<sys-devel/gettext-0.18.1.1-r3 || ( >=sys-devel/automake-1.15:1.15 ) >=sys-devel/autoconf-2.69 >=sys-devel/libtool-2.4 >=dev-vcs/git-1.8.2.1
|
||||
DESCRIPTION=Practical Music Search: an open source ncurses client for mpd, written in C++
|
||||
EAPI=6
|
||||
HOMEPAGE=https://ambientsound.github.io/pms
|
||||
IUSE=regex
|
||||
LICENSE=GPL-3
|
||||
RDEPEND=sys-libs/ncurses:=[unicode] dev-libs/glib:2 media-libs/libmpdclient
|
||||
IUSE=regex doc
|
||||
LICENSE=GPL-3+
|
||||
RDEPEND=sys-libs/ncurses:0=[unicode] dev-libs/glib:2 media-libs/libmpdclient virtual/libintl
|
||||
SLOT=0
|
||||
_eclasses_=autotools 07e71b3b5690738ef7e8bc097077e00c eutils b83a2420b796f7c6eff682679d08fe25 flag-o-matic 8632fcd33a047954f007dee9a137bdcc git-r3 00f60a84fc7b499c99edfe99caea9f95 libtool 4890219c51da247200223277f993e054 multilib 165fc17c38d1b11dac2008280dab6e80 toolchain-funcs 6198c04daba0e1307bd844df7d37f423
|
||||
_md5_=9655679997ceb7357a1de64ca93ef699
|
||||
_eclasses_=autotools 07e71b3b5690738ef7e8bc097077e00c eutils b83a2420b796f7c6eff682679d08fe25 flag-o-matic 8632fcd33a047954f007dee9a137bdcc git-r3 00f60a84fc7b499c99edfe99caea9f95 libtool 4890219c51da247200223277f993e054 multilib 165fc17c38d1b11dac2008280dab6e80 toolchain-funcs 6198c04daba0e1307bd844df7d37f423 versionator 99ae9d758cbe7cfed19170e7d48f5a9c
|
||||
_md5_=90cf6a941689798f93e8ebc95706ad61
|
||||
|
||||
@ -0,0 +1,13 @@
|
||||
DEFINED_PHASES=compile configure install prepare unpack
|
||||
DEPEND=sys-libs/zlib
|
||||
DESCRIPTION=Small yet efficient SAT solver with reference paper
|
||||
EAPI=6
|
||||
HOMEPAGE=http://minisat.se/Main.html
|
||||
IUSE=debug doc
|
||||
KEYWORDS=~amd64 ~x86 ~amd64-linux ~x86-linux
|
||||
LICENSE=MIT
|
||||
RDEPEND=sys-libs/zlib
|
||||
SLOT=0
|
||||
SRC_URI=https://github.com/niklasso/minisat/archive/37dc6c67e2af26379d88ce349eb9c4c6160e8543.tar.gz -> minisat-2.2.0_p20130925.tar.gz doc? ( http://minisat.se/downloads/MiniSat.pdf )
|
||||
_eclasses_=multilib 165fc17c38d1b11dac2008280dab6e80 toolchain-funcs 6198c04daba0e1307bd844df7d37f423 vcs-snapshot 2b65ecb2d0f91e4322c2ac8d673993bd
|
||||
_md5_=883902044873c9d3d76aa85c0683f9ce
|
||||
@ -1 +1 @@
|
||||
Tue, 13 Sep 2016 07:10:35 +0000
|
||||
Tue, 13 Sep 2016 10:40:35 +0000
|
||||
|
||||
@ -1 +1 @@
|
||||
Tue Sep 13 07:09:40 UTC 2016
|
||||
Tue Sep 13 10:39:40 UTC 2016
|
||||
|
||||
@ -1 +1 @@
|
||||
Tue, 13 Sep 2016 07:30:01 +0000
|
||||
Tue, 13 Sep 2016 11:00:01 +0000
|
||||
|
||||
@ -1 +1 @@
|
||||
1473750601 Tue 13 Sep 2016 07:10:01 AM UTC
|
||||
1473763201 Tue 13 Sep 2016 10:40:01 AM UTC
|
||||
|
||||
@ -1 +1 @@
|
||||
Tue, 13 Sep 2016 07:10:35 +0000
|
||||
Tue, 13 Sep 2016 10:40:35 +0000
|
||||
|
||||
@ -1,2 +1,3 @@
|
||||
DIST MiniSat.pdf 327416 SHA256 53197dbd783c924a2627d75e305706297988494265bd5e5ec873840e5d797ac4 SHA512 94e70c721740c0b7fd52621c7a5e43dd9207eed92e60a1c64ee63b541b9861d2580d14ba64c49c6c4f273ac028ded43bc944c71131e51693cdd7d1763af582f6 WHIRLPOOL a087d8929476fc33464d19432fc05a01797761f695b81c0aa6d35270731b00dabe2402ea2cfd705b49d5d6664a3cbd46bc60147d60934acdfc94a33066316185
|
||||
DIST minisat-2.2.0.tar.gz 43879 SHA256 92957d851cdc3baddfe07b5fc80ed5a0237c489d0c52ae72f62844b3b46d7808 SHA512 cf79b05d43ebdc8fd8081899a1f853370de051cafe6e5b143eaff9827efc542b58062782a3ce2a3d1a03561a9ffd780c9cdc645bb50036eb61e80fa729136e64 WHIRLPOOL a5117e7bc81aeecb6fa34d8e2dea70b379d9e3463957e7029c80957ff3bcdd3107a99fb0dabfe59b57bfdb16ed51a0a4781c8dbf8e3f6f225ebd5035c1a9ff79
|
||||
DIST minisat-2.2.0_p20130925.tar.gz 49544 SHA256 3db05b02f91c4b097b7962e523225aa5e6fa9a6c0d42704a170b01b069cdfcfe SHA512 37fc35cc4f3104d7f0e8ee9f7123fc34e175df578658266799d809d71d6cf081e811919f304a02f6cb9c3827d308e59408149d63d1d1e7c6d0b495350f93b3d9 WHIRLPOOL c976fabadb2149e15260025646e465d7422ffb9fd35e37263766002462de7b8d16db031aacb1458467acd9957eb370894d39ea3a7ddc5c98627f84b0a08b7820
|
||||
|
||||
@ -0,0 +1,527 @@
|
||||
--- a/Makefile
|
||||
+++ b/Makefile
|
||||
@@ -69,8 +89,8 @@
|
||||
VERB=
|
||||
endif
|
||||
|
||||
-SRCS = $(wildcard minisat/core/*.cc) $(wildcard minisat/simp/*.cc) $(wildcard minisat/utils/*.cc)
|
||||
-HDRS = $(wildcard minisat/mtl/*.h) $(wildcard minisat/core/*.h) $(wildcard minisat/simp/*.h) $(wildcard minisat/utils/*.h)
|
||||
+SRCS = $(wildcard minisat/core/*.cc) $(wildcard minisat/simp/*.cc) $(wildcard minisat/utils/*.cc) $(wildcard minisat/proof/*.cc)
|
||||
+HDRS = $(wildcard minisat/mtl/*.h) $(wildcard minisat/core/*.h) $(wildcard minisat/simp/*.h) $(wildcard minisat/utils/*.h) $(wildcard minisat/proof/*.h)
|
||||
OBJS = $(filter-out %Main.o, $(SRCS:.cc=.o))
|
||||
|
||||
r: $(BUILD_DIR)/release/bin/$(MINISAT)
|
||||
@@ -89,7 +109,7 @@
|
||||
lsh: $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)
|
||||
|
||||
## Build-type Compile-flags:
|
||||
-$(BUILD_DIR)/release/%.o: MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_RELSYM)
|
||||
+$(BUILD_DIR)/release/%.o: MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_RELSYM) $(MINISAT_FPIC)
|
||||
$(BUILD_DIR)/debug/%.o: MINISAT_CXXFLAGS +=$(MINISAT_DEB) -g
|
||||
$(BUILD_DIR)/profile/%.o: MINISAT_CXXFLAGS +=$(MINISAT_PRF) -pg
|
||||
$(BUILD_DIR)/dynamic/%.o: MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_FPIC)
|
||||
@@ -195,7 +215,7 @@
|
||||
$(INSTALL) -d $(DESTDIR)$(bindir)
|
||||
$(INSTALL) -m 755 $(BUILD_DIR)/dynamic/bin/$(MINISAT) $(DESTDIR)$(bindir)
|
||||
|
||||
-clean:
|
||||
+origclean:
|
||||
rm -f $(foreach t, release debug profile dynamic, $(foreach o, $(SRCS:.cc=.o), $(BUILD_DIR)/$t/$o)) \
|
||||
$(foreach t, release debug profile dynamic, $(foreach d, $(SRCS:.cc=.d), $(BUILD_DIR)/$t/$d)) \
|
||||
$(foreach t, release debug profile dynamic, $(BUILD_DIR)/$t/bin/$(MINISAT_CORE) $(BUILD_DIR)/$t/bin/$(MINISAT)) \
|
||||
@@ -203,6 +223,7 @@
|
||||
$(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\
|
||||
$(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)\
|
||||
$(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB)
|
||||
+ rm -f $(NUSMV_LIBNAME)
|
||||
|
||||
distclean: clean
|
||||
rm -f config.mk
|
||||
--- a/minisat/core/Solver.cc
|
||||
+++ b/minisat/core/Solver.cc
|
||||
@@ -101,7 +101,16 @@
|
||||
, conflict_budget (-1)
|
||||
, propagation_budget (-1)
|
||||
, asynch_interrupt (false)
|
||||
-{}
|
||||
+{
|
||||
+ // NuSMV: MOD BEGIN
|
||||
+ /* Disables "progress saving" which relies on last polarity
|
||||
+ assigned to a var when branching. Polarity for us is forced to
|
||||
+ be false. See http://reasoning.cs.ucla.edu/fetch.php?id=69&type=pdf
|
||||
+ */
|
||||
+ phase_saving = 0;
|
||||
+ default_polarity = l_Undef;
|
||||
+ // NuSMV: MOD END
|
||||
+}
|
||||
|
||||
|
||||
Solver::~Solver()
|
||||
@@ -250,8 +259,19 @@
|
||||
{
|
||||
Var next = var_Undef;
|
||||
|
||||
+ // NuSMV: PREF MOD
|
||||
+ // Selection from preferred list
|
||||
+ for (int i = 0; i < preferred.size(); i++) {
|
||||
+ if (value(preferred[i]) == l_Undef) {
|
||||
+ next = preferred[i];
|
||||
+ break;
|
||||
+ }
|
||||
+ }
|
||||
+ // NuSMV: PREF MOD END
|
||||
+
|
||||
// Random decision:
|
||||
- if (drand(random_seed) < random_var_freq && !order_heap.empty()){
|
||||
+ if (next == var_Undef && // NuSMV: PREF MOD
|
||||
+ drand(random_seed) < random_var_freq && !order_heap.empty()){
|
||||
next = order_heap[irand(random_seed,order_heap.size())];
|
||||
if (value(next) == l_Undef && decision[next])
|
||||
rnd_decisions++; }
|
||||
@@ -269,6 +289,8 @@
|
||||
return lit_Undef;
|
||||
else if (user_pol[next] != l_Undef)
|
||||
return mkLit(next, user_pol[next] == l_True);
|
||||
+ else if (default_polarity != l_Undef) // NuSMV
|
||||
+ return mkLit(next, default_polarity == l_True);
|
||||
else if (rnd_pol)
|
||||
return mkLit(next, drand(random_seed) < 0.5);
|
||||
else
|
||||
@@ -620,6 +642,19 @@
|
||||
}
|
||||
|
||||
|
||||
+// NuSMV: PREF MOD
|
||||
+void Solver::addPreferred(Var v)
|
||||
+{
|
||||
+ preferred.push(v);
|
||||
+}
|
||||
+
|
||||
+void Solver::clearPreferred()
|
||||
+{
|
||||
+ preferred.clear(0);
|
||||
+}
|
||||
+// NuSMV: PREF MOD END
|
||||
+
|
||||
+
|
||||
void Solver::rebuildOrderHeap()
|
||||
{
|
||||
vec<Var> vs;
|
||||
--- a/minisat/core/Solver.h
|
||||
+++ b/minisat/core/Solver.h
|
||||
@@ -90,6 +90,19 @@
|
||||
void setPolarity (Var v, lbool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
|
||||
void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
|
||||
|
||||
+ // NuSMV: PREF MOD
|
||||
+ /*
|
||||
+ * Add a variable at the end of the list of preferred variables
|
||||
+ * Does not remove the variable from the standard ordering.
|
||||
+ */
|
||||
+ void addPreferred(Var v);
|
||||
+
|
||||
+ /*
|
||||
+ * Clear vector of preferred variables.
|
||||
+ */
|
||||
+ void clearPreferred();
|
||||
+ // NuSMV: PREF MOD END
|
||||
+
|
||||
// Read state:
|
||||
//
|
||||
lbool value (Var x) const; // The current value of a variable.
|
||||
@@ -134,6 +147,8 @@
|
||||
int ccmin_mode; // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
|
||||
int phase_saving; // Controls the level of phase saving (0=none, 1=limited, 2=full).
|
||||
bool rnd_pol; // Use random polarities for branching heuristics.
|
||||
+ lbool default_polarity; // NuSMV: default polarity for vars
|
||||
+
|
||||
bool rnd_init_act; // Initialize variable activities with a small random value.
|
||||
double garbage_frac; // The fraction of wasted memory allowed before a garbage collection is triggered.
|
||||
int min_learnts_lim; // Minimum number to set the learnts limit to.
|
||||
@@ -215,6 +230,10 @@
|
||||
Var next_var; // Next variable to be created.
|
||||
ClauseAllocator ca;
|
||||
|
||||
+ // NuSMV: PREF MOD
|
||||
+ vec<Var> preferred;
|
||||
+ // NuSMV: PREF MOD END
|
||||
+
|
||||
vec<Var> released_vars;
|
||||
vec<Var> free_vars;
|
||||
|
||||
--- a/minisat/core/SolverTypes.h
|
||||
+++ b/minisat/core/SolverTypes.h
|
||||
@@ -52,7 +52,7 @@
|
||||
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; }
|
||||
@@ -61,6 +61,7 @@
|
||||
|
||||
|
||||
inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
|
||||
+inline Lit mkLit (Var var) { return mkLit(var, false); }
|
||||
inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; }
|
||||
inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; }
|
||||
inline bool sign (Lit p) { return p.x & 1; }
|
||||
@@ -120,6 +121,7 @@
|
||||
inline int toInt (lbool l) { return l.value; }
|
||||
inline lbool toLbool(int v) { return lbool((uint8_t)v); }
|
||||
|
||||
+#define MINISAT_CONSTANTS_AS_MACROS
|
||||
#if defined(MINISAT_CONSTANTS_AS_MACROS)
|
||||
#define l_True (lbool((uint8_t)0)) // gcc does not do constant propagation if these are real constants.
|
||||
#define l_False (lbool((uint8_t)1))
|
||||
--- a/minisat/simp/Solver_C.cc
|
||||
+++ b/minisat/simp/Solver_C.cc
|
||||
@@ -0,0 +1,246 @@
|
||||
+
|
||||
+/**************************************************************************************************
|
||||
+
|
||||
+Solver_C.C
|
||||
+
|
||||
+C-wrapper for Solver.C
|
||||
+
|
||||
+ This file is part of NuSMV version 2.
|
||||
+ Copyright (C) 2007 by FBK-irst.
|
||||
+ Author: Roberto Cavada <cavada@fbk.eu>
|
||||
+
|
||||
+ NuSMV version 2 is free software; you can redistribute it and/or
|
||||
+ modify it under the terms of the GNU Lesser General Public
|
||||
+ License as published by the Free Software Foundation; either
|
||||
+ version 2 of the License, or (at your option) any later version.
|
||||
+
|
||||
+ NuSMV version 2 is distributed in the hope that it will be useful,
|
||||
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
|
||||
+ Lesser General Public License for more details.
|
||||
+
|
||||
+ You should have received a copy of the GNU Lesser General Public
|
||||
+ License along with this library; if not, write to the Free Software
|
||||
+ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA.
|
||||
+
|
||||
+ For more information on NuSMV see <http://nusmv.fbk.eu>
|
||||
+ or email to <nusmv-users@fbk.eu>.
|
||||
+ Please report bugs to <nusmv-users@fbk.eu>.
|
||||
+
|
||||
+ To contact the NuSMV development board, email to <nusmv@fbk.eu>. ]
|
||||
+
|
||||
+**************************************************************************************************/
|
||||
+
|
||||
+
|
||||
+#include "SimpSolver.h"
|
||||
+extern "C" {
|
||||
+#include "Solver_C.h"
|
||||
+}
|
||||
+
|
||||
+namespace {
|
||||
+using Minisat::lbool;
|
||||
+} // namespace
|
||||
+
|
||||
+extern "C" MiniSat_ptr MiniSat_Create()
|
||||
+{
|
||||
+ Minisat::SimpSolver *s = new Minisat::SimpSolver();
|
||||
+ s->default_polarity = l_True;
|
||||
+ return (MiniSat_ptr)s;
|
||||
+}
|
||||
+
|
||||
+extern "C"void MiniSat_Delete(MiniSat_ptr ms)
|
||||
+{
|
||||
+ delete (Minisat::SimpSolver *)ms;
|
||||
+}
|
||||
+
|
||||
+extern "C" int MiniSat_Nof_Variables(MiniSat_ptr ms)
|
||||
+{
|
||||
+ return ((Minisat::SimpSolver *)ms)->nVars();
|
||||
+}
|
||||
+
|
||||
+extern "C" int MiniSat_Nof_Clauses(MiniSat_ptr ms)
|
||||
+{
|
||||
+ return ((Minisat::SimpSolver *)ms)->nClauses();
|
||||
+}
|
||||
+
|
||||
+/* variables are in the range 1...N */
|
||||
+extern "C" int MiniSat_New_Variable(MiniSat_ptr ms)
|
||||
+{
|
||||
+ /* Actually, minisat used variable range 0 .. N-1,
|
||||
+ so in all function below there is a convertion between
|
||||
+ input variable (1..N) and internal variables (0..N-1)
|
||||
+ */
|
||||
+ Minisat::Var var = ((Minisat::SimpSolver *)ms)->newVar();
|
||||
+ ((Minisat::SimpSolver *)ms)->setFrozen(var, true);
|
||||
+ return var+1;
|
||||
+}
|
||||
+
|
||||
+
|
||||
+/*
|
||||
+ * Here clauses are in dimacs form, variable indexing is 1...N
|
||||
+ */
|
||||
+extern "C" int MiniSat_Add_Clause(MiniSat_ptr ms,
|
||||
+ int *clause_lits, int num_lits)
|
||||
+{
|
||||
+ int i;
|
||||
+ Minisat::vec<Minisat::Lit> cl;
|
||||
+ for(i = 0; i < num_lits; ++i) {
|
||||
+ const int lit = clause_lits[i];
|
||||
+ assert(abs(lit) > 0);
|
||||
+ assert(abs(lit) <= MiniSat_Nof_Variables((Minisat::SimpSolver*)ms));
|
||||
+ int var = abs(lit) - 1;
|
||||
+ cl.push((lit > 0) ? Minisat::mkLit(var) : ~ Minisat::mkLit(var));
|
||||
+ }
|
||||
+ ((Minisat::SimpSolver *)ms)->addClause(cl);
|
||||
+
|
||||
+ if(((Minisat::SimpSolver *)ms)->okay()) return 1;
|
||||
+ return 0;
|
||||
+}
|
||||
+
|
||||
+extern "C" int MiniSat_Solve(MiniSat_ptr ms)
|
||||
+{
|
||||
+ bool ret = ((Minisat::SimpSolver *)ms)->solve();
|
||||
+ if(ret) return 1;
|
||||
+ return 0;
|
||||
+}
|
||||
+
|
||||
+/*
|
||||
+ * Here the assumption is in "dimacs form", variable indexing is 1...N
|
||||
+ */
|
||||
+extern "C" int MiniSat_Solve_Assume(MiniSat_ptr ms,
|
||||
+ int nof_assumed_lits,
|
||||
+ int *assumed_lits)
|
||||
+{
|
||||
+ int i;
|
||||
+ Minisat::vec<Minisat::Lit> cl;
|
||||
+ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
|
||||
+ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
|
||||
+
|
||||
+ solver.simplify();
|
||||
+ if(solver.okay() == false) return 0;
|
||||
+
|
||||
+ assert(nof_assumed_lits >= 0);
|
||||
+ for(i = 0; i < nof_assumed_lits; ++i) {
|
||||
+ const int lit = assumed_lits[i];
|
||||
+ assert(abs(lit) > 0);
|
||||
+ assert(abs(lit) <= MiniSat_Nof_Variables((Minisat::SimpSolver*)ms));
|
||||
+ int var = abs(lit) - 1;
|
||||
+ cl.push((lit > 0) ? Minisat::mkLit(var) : ~Minisat::mkLit(var));
|
||||
+ }
|
||||
+
|
||||
+ if (solver.solve(cl)) return 1;
|
||||
+ return 0;
|
||||
+}
|
||||
+
|
||||
+extern "C" int MiniSat_simplifyDB(MiniSat_ptr ms)
|
||||
+{
|
||||
+ ((Minisat::SimpSolver *)ms)->simplify();
|
||||
+ if(((Minisat::SimpSolver *)ms)->okay()) return 1;
|
||||
+ return 0;
|
||||
+}
|
||||
+
|
||||
+/*
|
||||
+ * Here variables are numbered 1...N
|
||||
+ */
|
||||
+extern "C" int MiniSat_Get_Value(MiniSat_ptr ms, int var_num)
|
||||
+{
|
||||
+ assert(var_num > 0);
|
||||
+ if(var_num > MiniSat_Nof_Variables(ms)) return -1;
|
||||
+ /* minisat assigns all variables. just check */
|
||||
+ assert(((Minisat::SimpSolver *)ms)->model[var_num-1] != l_Undef);
|
||||
+
|
||||
+ if(((Minisat::SimpSolver *)ms)->model[var_num-1] == l_True) return 1;
|
||||
+ return 0;
|
||||
+}
|
||||
+
|
||||
+extern "C" int MiniSat_Get_Nof_Conflict_Lits(MiniSat_ptr ms)
|
||||
+{
|
||||
+ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
|
||||
+ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
|
||||
+
|
||||
+ return solver.conflict.size();
|
||||
+}
|
||||
+
|
||||
+extern "C" void MiniSat_Get_Conflict_Lits(MiniSat_ptr ms, int* conflict_lits)
|
||||
+{
|
||||
+ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
|
||||
+ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
|
||||
+
|
||||
+ Minisat::LSet& cf = solver.conflict;
|
||||
+
|
||||
+ for (int i = 0; i < cf.size(); ++i) {
|
||||
+ int v = Minisat::var(~cf[i]);
|
||||
+ int s = Minisat::sign(~cf[i]);
|
||||
+ assert(v != Minisat::var_Undef);
|
||||
+ conflict_lits[i] = (s == 0) ? (v+1) : -(v+1);
|
||||
+ }
|
||||
+}
|
||||
+
|
||||
+/** mode can be polarity_user, polarity_rnd */
|
||||
+extern "C" void MiniSat_Set_Polarity_Mode(MiniSat_ptr ms, int mode)
|
||||
+{
|
||||
+ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
|
||||
+ assert(__polarity_unsupported != mode);
|
||||
+ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
|
||||
+ if (polarity_rnd == mode) {
|
||||
+ solver.rnd_pol = true;
|
||||
+ solver.default_polarity = l_Undef;
|
||||
+ }
|
||||
+ else {
|
||||
+ // assert(polarity_user == mode);
|
||||
+ solver.rnd_pol = false;
|
||||
+ switch (mode) {
|
||||
+ case polarity_false:
|
||||
+ solver.default_polarity = l_True;
|
||||
+ break;
|
||||
+ case polarity_true:
|
||||
+ solver.default_polarity = l_False;
|
||||
+ break;
|
||||
+ default: // polarity_user
|
||||
+ solver.default_polarity = l_Undef;
|
||||
+ break;
|
||||
+ }
|
||||
+ }
|
||||
+}
|
||||
+
|
||||
+extern "C" int MiniSat_Get_Polarity_Mode(MiniSat_ptr ms)
|
||||
+{
|
||||
+ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
|
||||
+ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
|
||||
+ //return solver.rnd_pol ? polarity_rnd : polarity_user;
|
||||
+ if (solver.rnd_pol) {
|
||||
+ return polarity_rnd;
|
||||
+ } else if (solver.default_polarity == l_True) {
|
||||
+ return polarity_false;
|
||||
+ } else if (solver.default_polarity == l_False) {
|
||||
+ return polarity_true;
|
||||
+ } else {
|
||||
+ return polarity_user;
|
||||
+ }
|
||||
+}
|
||||
+
|
||||
+extern "C" void MiniSat_Set_Random_Seed(MiniSat_ptr ms, double seed)
|
||||
+{
|
||||
+ assert(((Minisat::SimpSolver*)0) != ((Minisat::SimpSolver*)ms));
|
||||
+ Minisat::SimpSolver& solver = *((Minisat::SimpSolver*)ms);
|
||||
+ solver.random_seed = seed;
|
||||
+}
|
||||
+
|
||||
+
|
||||
+// NuSMV: PREF MOD
|
||||
+/* variables are in the range 1...N */
|
||||
+extern "C" void MiniSat_Set_Preferred_Variable(MiniSat_ptr ms, int x)
|
||||
+{
|
||||
+ /* Actually, minisat used variable range 0 .. N-1,
|
||||
+ so in all function below there is a convertion between
|
||||
+ input variable (1..N) and internal variables (0..N-1)
|
||||
+ */
|
||||
+ ((Minisat::SimpSolver *)ms)->addPreferred((Minisat::Var) x);
|
||||
+}
|
||||
+
|
||||
+extern "C" void MiniSat_Clear_Preferred_Variables(MiniSat_ptr ms)
|
||||
+{
|
||||
+
|
||||
+ ((Minisat::SimpSolver *)ms)->clearPreferred();
|
||||
+}
|
||||
+// NuSMV: PREF MOD END
|
||||
--- a/minisat/simp/Solver_C.h
|
||||
+++ b/minisat/simp/Solver_C.h
|
||||
@@ -0,0 +1,72 @@
|
||||
+/**************************************************************************************************
|
||||
+
|
||||
+Solver_C.h
|
||||
+
|
||||
+C-wrapper for Solver.h
|
||||
+
|
||||
+ This file is part of NuSMV version 2.
|
||||
+ Copyright (C) 2007 by FBK-irst.
|
||||
+ Author: Roberto Cavada <cavada@fbk.eu>
|
||||
+
|
||||
+ NuSMV version 2 is free software; you can redistribute it and/or
|
||||
+ modify it under the terms of the GNU Lesser General Public
|
||||
+ License as published by the Free Software Foundation; either
|
||||
+ version 2 of the License, or (at your option) any later version.
|
||||
+
|
||||
+ NuSMV version 2 is distributed in the hope that it will be useful,
|
||||
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
|
||||
+ Lesser General Public License for more details.
|
||||
+
|
||||
+ You should have received a copy of the GNU Lesser General Public
|
||||
+ License along with this library; if not, write to the Free Software
|
||||
+ Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA.
|
||||
+
|
||||
+ For more information on NuSMV see <http://nusmv.fbk.eu>
|
||||
+ or email to <nusmv-users@fbk.eu>.
|
||||
+ Please report bugs to <nusmv-users@fbk.eu>.
|
||||
+
|
||||
+ To contact the NuSMV development board, email to <nusmv@fbk.eu>. ]
|
||||
+
|
||||
+**************************************************************************************************/
|
||||
+
|
||||
+#ifndef SOLVER_C_h
|
||||
+#define SOLVER_C_h
|
||||
+
|
||||
+//=================================================================================================
|
||||
+// Solver -- the main class:
|
||||
+
|
||||
+#define MiniSat_ptr void *
|
||||
+
|
||||
+enum {
|
||||
+ __polarity_unsupported = -1,
|
||||
+ polarity_true = 0,
|
||||
+ polarity_false = 1,
|
||||
+ polarity_user = 2,
|
||||
+ polarity_rnd = 3,
|
||||
+};
|
||||
+
|
||||
+MiniSat_ptr MiniSat_Create();
|
||||
+void MiniSat_Delete(MiniSat_ptr);
|
||||
+int MiniSat_Nof_Variables(MiniSat_ptr);
|
||||
+int MiniSat_Nof_Clauses(MiniSat_ptr);
|
||||
+int MiniSat_New_Variable(MiniSat_ptr);
|
||||
+int MiniSat_Add_Clause(MiniSat_ptr, int *clause_lits, int num_lits);
|
||||
+int MiniSat_Solve(MiniSat_ptr);
|
||||
+int MiniSat_Solve_Assume(MiniSat_ptr, int nof_assumed_lits, int *assumed_lits);
|
||||
+int MiniSat_simplifyDB(MiniSat_ptr);
|
||||
+int MiniSat_Get_Value(MiniSat_ptr, int var_num);
|
||||
+int MiniSat_Get_Nof_Conflict_Lits(MiniSat_ptr ms);
|
||||
+void MiniSat_Get_Conflict_Lits(MiniSat_ptr ms, int* conflict_lits);
|
||||
+
|
||||
+void MiniSat_Set_Polarity_Mode(MiniSat_ptr ms, int mode);
|
||||
+int MiniSat_Get_Polarity_Mode(MiniSat_ptr ms);
|
||||
+void MiniSat_Set_Random_Seed(MiniSat_ptr ms, double seed);
|
||||
+
|
||||
+// NuSMV: PREF MOD
|
||||
+void MiniSat_Set_Preferred_Variable(MiniSat_ptr, int);
|
||||
+void MiniSat_Clear_Preferred_Variables(MiniSat_ptr);
|
||||
+// NuSMV: PREF MOD END
|
||||
+
|
||||
+//=================================================================================================
|
||||
+#endif
|
||||
--- a/minisat/utils/System.cc
|
||||
+++ b/minisat/utils/System.cc
|
||||
@@ -77,7 +77,7 @@
|
||||
struct rusage ru;
|
||||
getrusage(RUSAGE_SELF, &ru);
|
||||
return (double)ru.ru_maxrss / 1024; }
|
||||
-double Minisat::memUsedPeak() { return memUsed(); }
|
||||
+double Minisat::memUsedPeak(bool strictlyPeak) { return memUsed(); }
|
||||
|
||||
|
||||
#elif defined(__APPLE__)
|
||||
@@ -87,11 +87,11 @@
|
||||
malloc_statistics_t t;
|
||||
malloc_zone_statistics(NULL, &t);
|
||||
return (double)t.max_size_in_use / (1024*1024); }
|
||||
-double Minisat::memUsedPeak() { return memUsed(); }
|
||||
+double Minisat::memUsedPeak(bool strictlyPeak) { return memUsed(); }
|
||||
|
||||
#else
|
||||
double Minisat::memUsed() { return 0; }
|
||||
-double Minisat::memUsedPeak() { return 0; }
|
||||
+double Minisat::memUsedPeak(bool strictlyPeak) { return 0; }
|
||||
#endif
|
||||
|
||||
|
||||
@ -0,0 +1,58 @@
|
||||
# Copyright 1999-2016 Gentoo Foundation
|
||||
# Distributed under the terms of the GNU General Public License v2
|
||||
# $Id$
|
||||
|
||||
EAPI=6
|
||||
|
||||
inherit toolchain-funcs vcs-snapshot
|
||||
|
||||
DESCRIPTION="Small yet efficient SAT solver with reference paper"
|
||||
HOMEPAGE="http://minisat.se/Main.html"
|
||||
COMMIT=37dc6c67e2af26379d88ce349eb9c4c6160e8543
|
||||
SRC_URI="https://github.com/niklasso/minisat/archive/${COMMIT}.tar.gz -> ${P}.tar.gz
|
||||
doc? ( http://minisat.se/downloads/MiniSat.pdf )"
|
||||
|
||||
SLOT="0"
|
||||
KEYWORDS="~amd64 ~x86 ~amd64-linux ~x86-linux"
|
||||
LICENSE="MIT"
|
||||
|
||||
IUSE="debug doc"
|
||||
|
||||
DEPEND="sys-libs/zlib"
|
||||
RDEPEND="${DEPEND}"
|
||||
DOCS=( README doc/ReleaseNotes-${PV%_*}.txt )
|
||||
PATCHES=( "${FILESDIR}"/${P}-nusmv.patch )
|
||||
|
||||
src_prepare() {
|
||||
default
|
||||
# Remove makefile silencing and
|
||||
# Remove static linking by default
|
||||
sed -i -e "s/VERB=@/VERB=/" \
|
||||
-e "s/--static //g" \
|
||||
Makefile || die
|
||||
|
||||
sed -i -e "s:\$(exec_prefix)/lib:\$(exec_prefix)/$(get_libdir):" \
|
||||
Makefile || die
|
||||
|
||||
# Fix headers ( #include "minisat/..." -> #include <...> )
|
||||
while IFS="" read -d $'\0' -r file; do
|
||||
einfo Correcting header "$file"
|
||||
sed -i -e 's:#include "minisat/\([^"]*\)":#include <\1>:g' "${file}" || die
|
||||
done < <(find minisat -name "*.h" -print0)
|
||||
}
|
||||
|
||||
src_configure() {
|
||||
local minisat_cflags="${CFLAGS} -D NDEBUG -I${S}/minisat"
|
||||
emake config prefix="${EPREFIX}"/usr MINISAT_RELSYM="" MINISAT_REL="${minisat_cflags}" MINISAT_PRF="${minisat_cflags}" MINISAT_DEB="${CFLAGS} -D DEBUG -I${S}/minisat"
|
||||
}
|
||||
|
||||
src_compile() {
|
||||
emake all $(usex debug d "")
|
||||
}
|
||||
|
||||
src_install() {
|
||||
use doc && DOCS+=( "${DISTDIR}"/MiniSat.pdf )
|
||||
default
|
||||
|
||||
dosym libminisat.a /usr/$(get_libdir)/libMiniSat.a
|
||||
}
|
||||
Loading…
Reference in new issue