I've attached a patch that enables the undertaker to be run with a 960
picomus and removes the install of the intree picomus.
Best Regards,
Stefan
2014-11-10 11:25 GMT+01:00 Michael Tautschnig <m...@debian.org>:
> Hi,
>
> On Sat, Nov 08, 2014 at 12:52:13 -0500, Reinhard Tartler wrote:
>> That doesn't sound like a bad idea at all. I'm not sure if going via
>> unstable or experimental is best at this point, but either way, this would
>> allow us preparing a package that links against the system picosat again.
>>
> [...]
>
> So 960-1 is in unstable; please let me know whether this allows for
> adjustments
> to undertaker so that #766273 can eventually be closed. I'd suggest we file
> unblock requests once an updated version of undertaker has been uploaded (and
> assuming that it's actually going to be the undertaker upload that will close
> this bug).
>
> Best,
> Michael
>
From cf400f123f4b73f01954b014905b67393c095039 Mon Sep 17 00:00:00 2001
From: Stefan Hengelein <stefan.hengel...@fau.de>
Date: Mon, 10 Nov 2014 14:24:34 +0100
Subject: [PATCH] undertaker: adjust picomus call for debian release
Change-Id: I6241e49b938a84715a8c3486b6b01307d95b7dc1
---
Makefile | 2 --
undertaker/BlockDefectAnalyzer.cpp | 5 +----
2 files changed, 1 insertion(+), 6 deletions(-)
diff --git a/Makefile b/Makefile
index 2bc9b81..6640ec2 100644
--- a/Makefile
+++ b/Makefile
@@ -183,8 +183,6 @@ install: all $(MANPAGES)
@install -v undertaker/rsf2cnf $(DESTDIR)$(BINDIR)
@install -v undertaker/satyr $(DESTDIR)$(BINDIR)
- @install -v picosat/picomus $(DESTDIR)$(BINDIR)
-
@install -v ziz/zizler $(DESTDIR)$(BINDIR)
@install -v scripts/Makefile.list $(DESTDIR)$(LIBDIR)
diff --git a/undertaker/BlockDefectAnalyzer.cpp b/undertaker/BlockDefectAnalyzer.cpp
index 3ecfd10..bb73476 100644
--- a/undertaker/BlockDefectAnalyzer.cpp
+++ b/undertaker/BlockDefectAnalyzer.cpp
@@ -247,7 +247,7 @@ void DeadBlockDefect::reportMUS(ConfigurationModel *main_model) const {
sc(_musFormula);
const kconfig::PicosatCNF *cnf = sc.getCNF();
// call picosat in quiet mode with stdin as input and stdout as output
- redi::pstream cmd_process("picomus - -");
+ redi::pstream cmd_process("picomus -q - -");
// write to stdin of the process
cmd_process << "p cnf " << cnf->getVarCount() << " " << cnf->getClauseCount() << std::endl;
for (const int &clause : cnf->getClauses()) {
@@ -261,9 +261,6 @@ void DeadBlockDefect::reportMUS(ConfigurationModel *main_model) const {
std::stringstream ss;
ss << cmd_process.rdbuf();
cmd_process.close();
- // remove first line from ss (=UNSATISFIABLE)
- std::string garbage;
- std::getline(ss, garbage);
// create a string from DIMACs CNF Format (=picomus result) to a more readable CNF Format
// Note: The formula might be incomplete, since a lot operators create new CNF-IDs without
--
1.9.1
