Package: release.debian.org Severity: normal User: release.debian.org@packages.debian.org Usertags: unblock X-Debbugs-CC: siretart@tauware.de Hi, In order to fix #766273 properly, we had to make changes to both picosat and undertaker; the executive summary of #766273 is: undertaker, up to 1.6-1, used to ship its own copy of picosat as some fixes were required. These fixes make up the new upstream release 960 of picosat. With the uploads of picosat/960-1 and undertaker/1.6-2 thus both #766273 as well as embedded code copy problems are resolved. While I am aware that new upstream releases are not desirable at this point, I would ask to consider this update to picosat nevertheless as the upstream changes are bugfixes only and picosat has the science-logic meta package as sole rdepends, thus making this a low-risk step. Thanks a lot in advance, Michael unblock picosat/960-1 unblock undertaker/1.6-2
diff -Nru picosat-959/debian/changelog picosat-960/debian/changelog
--- picosat-959/debian/changelog 2014-06-28 17:37:35.000000000 +0100
+++ picosat-960/debian/changelog 2014-11-08 18:15:20.000000000 +0000
@@ -1,3 +1,9 @@
+picosat (960-1) unstable; urgency=low
+
+ * New upstream version
+
+ -- Michael Tautschnig <mt@debian.org> Sat, 08 Nov 2014 18:15:16 +0000
+
picosat (959-1) unstable; urgency=low
* New upstream version
diff -Nru picosat-959/LICENSE picosat-960/LICENSE
--- picosat-959/LICENSE 2014-02-07 06:23:28.000000000 +0000
+++ picosat-960/LICENSE 2014-10-26 10:03:30.000000000 +0000
@@ -1,4 +1,4 @@
-Copyright (c) 2006 - 2013, Armin Biere, Johannes Kepler University.
+Copyright (c) 2006 - 2014, Armin Biere, Johannes Kepler University.
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to
diff -Nru picosat-959/makefile.in picosat-960/makefile.in
--- picosat-959/makefile.in 2014-02-07 06:23:28.000000000 +0000
+++ picosat-960/makefile.in 2014-10-26 10:03:30.000000000 +0000
@@ -1,5 +1,5 @@
CC=@CC@
-CFLAGS=@CFLAGS@ -fno-strict-aliasing
+CFLAGS=@CFLAGS@
all: @TARGETS@
diff -Nru picosat-959/NEWS picosat-960/NEWS
--- picosat-959/NEWS 2014-02-07 06:23:28.000000000 +0000
+++ picosat-960/NEWS 2014-10-26 10:03:30.000000000 +0000
@@ -1,3 +1,13 @@
+news for release 960 since 959
+------------------------------
+
+* fixed various issues pointed out by Stefan Hengelein:
+ - fixed incremental usage of 'picosat_adjust'
+ - added CPP fixes (STATS, NO_BINARY_CLAUSE versus TRACE mix-ups)
+ - removed redundant explicit set to zero on reset
+* fixed various usage bugs with 'picomus' (thanks to Stefan Hengelein)
+* removed '-fno-strict-aliasing' (thanks to Jerry James)
+
news for release 959 since 953
------------------------------
diff -Nru picosat-959/picomus.c picosat-960/picomus.c
--- picosat-959/picomus.c 2014-02-07 06:23:28.000000000 +0000
+++ picosat-960/picomus.c 2014-10-26 10:03:30.000000000 +0000
@@ -1,5 +1,5 @@
/****************************************************************************
-Copyright (c) 2011-2012, Armin Biere, Johannes Kepler University.
+Copyright (c) 2011-2014, Armin Biere, Johannes Kepler University.
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to
@@ -34,7 +34,7 @@
typedef struct Cls { int lit, red, * lits; } Cls;
-static int verbose = 1, nowitness;
+static int verbose, nowitness;
static int fclose_input, pclose_input, close_output;
static FILE * input_file, * output_file;
static const char * input_name, * output_name;
@@ -66,6 +66,7 @@
static void warn (const char * fmt, ...) {
va_list ap;
+ if (verbose < 0) return;
fputs ("c [picomus] WARNING: ", stdout);
va_start (ap, fmt);
vfprintf (stdout, fmt, ap);
@@ -150,7 +151,7 @@
int remaining;
const int * p;
(void) dummy;
- if (!verbose) return;
+ if (verbose <= 0) return;
remaining = 0;
for (p = mus; *p; p++) remaining++;
assert (remaining <= nclauses);
@@ -161,6 +162,47 @@
picosat_time_stamp () - start);
}
+static const char * USAGE =
+"picomus [-h][-v][-q] [ <input> [ <output> ] ]\n"
+"\n"
+" -h print this command line option summary\n"
+" -v increase verbosity level (default 0 = no messages)\n"
+" -q be quiet (no warnings nor messages)\n"
+"\n"
+"This tool is a SAT solver that uses the PicoSAT library to\n"
+"generate a 'minimal unsatisfiable core' also known as 'minimal\n"
+"unsatisfiable set' (MUS) of a CNF in DIMACS format.\n"
+"\n"
+"Both file arguments can be \"-\" and then denote <stdin> and\n"
+"<stdout> respectively. If no input file is given <stdin> is used.\n"
+"If no output file is specified the MUS is computed and only printed\n"
+"to <stdout> in the format of the SAT competition 2011 MUS track.\n"
+"\n"
+"Note, that the 's ...' lines and in case the instance is satisfiable\n"
+"also the 'v ...' lines for the satisfying assignment are always\n"
+"printed to <stdout> (or not printed at all with '-q').\n"
+"\n"
+"If '-n' is specified satisfying assignment and MUS printing\n"
+"on <stdout> (using the 'v ...' format) is suppressed.\n"
+"The 's ...' line is still printed unless '-q' is specified.\n"
+"If <output> is specified an MUS is written to this file,\n"
+"even if '-n' or '-q' is used.\n"
+"\n"
+#ifndef TRACE
+"WARNING: PicosSAT is compiled without trace support.\n"
+"\n"
+"This typically slows down this MUS extractor, since\n"
+"it only relies on clause selector variables and\n"
+"can not make use of core extraction. To enable\n"
+"trace generation use './configure --trace' or\n"
+"'./configure -O --trace' when building PicoSAT.\n"
+#else
+"Since trace generation code is included, this binary\n"
+"uses also core extraction in addition to clause selector\n"
+"variables.\n"
+#endif
+;
+
int main (int argc, char ** argv) {
int i, * p, n, oldn, red, nonred, res, round, printed, len;
const char * err;
@@ -173,41 +215,17 @@
start = picosat_time_stamp ();
for (i = 1; i < argc; i++) {
if (!strcmp (argv[i], "-h")) {
- printf (
- "picomus [-v][-h][-a][<input>[<output>]]\n"
- "\n"
- "This tool is a SAT solver that uses the PicoSAT library to\n"
- "generate a 'minimal unsatisfiable core' also known as 'minimal\n"
- "unsatisfiable set' (MUS) of a CNF in DIMACS format.\n"
- "\n"
- "Both file arguments can be \"-\" and then denote <stdin> resp.\n"
- "<stdout>. If no input file is given <stdin> is used. If no\n"
- "output file is specified the MUS is computed and only printed\n"
- "to <stdout> in the format of the SAT competition 2011 MUS track.\n"
- "\n"
- "If '-n' is specified solution respectively MUS printing\n"
- "on <stdout> (using the 'v ...' format) is suppressed.\n"
- "If <output> is specified an MUS is written to this file,\n"
- "even if '-n' is used.\n"
- "\n"
-#ifndef TRACE
- "WARNING: PicosSAT is compiled without trace support.\n"
- "\n"
- "This typically slows down this MUS extractor, since\n"
- "it only relies on clause selector variables and\n"
- "can not make use of core extraction. To enable\n"
- "trace generation use './configure --trace' or\n"
- "'./configure -O --trace' when building PicoSAT.\n"
-#else
- "Since trace generation code is included, this binary\n"
- "uses also core extraction in addition to clause selector\n"
- "variables.\n"
-#endif
- );
+ fputs (USAGE, stdout);
exit (0);
- } else if (!strcmp (argv[i], "-v")) verbose++;
- else if (!strcmp (argv[i], "-n")) nowitness = 1;
- else if (argv[i][0] == '-')
+ } else if (!strcmp (argv[i], "-v")) {
+ if (verbose < 0) die ("'-v' option after '-q'");
+ verbose++;
+ } else if (!strcmp (argv[i], "-q")) {
+ if (verbose < 0) die ("two '-q' options");
+ if (verbose > 0) die ("'-q' option after '-v'");
+ verbose = -1;
+ } else if (!strcmp (argv[i], "-n")) nowitness = 1;
+ else if (argv[i][0] == '-' && argv[i][1])
die ("invalid command line option '%s'", argv[i]);
else if (output_name) die ("too many arguments");
else if (!input_name) input_name = argv[i];
@@ -268,8 +286,9 @@
if (!printed) {
assert (round == 1);
printed = 1;
- printf ("s UNSATISFIABLE\n");
- fflush (stdout);
+ if (verbose >= 0)
+ printf ("s UNSATISFIABLE\n"),
+ fflush (stdout);
}
for (i = 0; i < nclauses; i++) {
c = clauses + i;
@@ -327,7 +346,8 @@
}
res = picosat_sat (ps, -1);
if (res == 20) {
- if (!printed) printf ("s UNSATISFIABLE\n"), fflush (stdout);
+ if (!printed && verbose >= 0)
+ printf ("s UNSATISFIABLE\n"), fflush (stdout);
for (i = 0; i < nclauses; i++) clauses[i].red = 1;
q = picosat_mus_assumptions (ps, 0, callback, 1);
while ((i = *q++)) {
@@ -338,21 +358,23 @@
} else {
SAT:
assert (res == 10);
- printf ("s SATISFIABLE\n"); fflush (stdout);
- if (!nowitness) {
+ if (!printed && verbose >= 0)
+ printf ("s SATISFIABLE\n"), fflush (stdout);
+ if (!nowitness && verbose >= 0) {
for (i = 1; i <= nvars; i++)
printf ("v %d\n", ((picosat_deref (ps, i) < 0) ? -1 : 1) * i);
printf ("v 0\n");
}
}
- if (verbose) picosat_stats (ps);
+ if (verbose > 0) picosat_stats (ps);
picosat_reset (ps);
n = 0;
for (i = 0; i < nclauses; i++) if (!clauses[i].red) n++;
red = nclauses - n;
msg (1, "found %d redundant clauses %.0f%%", red, percent (red, nclauses));
- msg (0, "computed MUS of size %d out of %d (%.0f%%)",
- n, nclauses, percent (n, nclauses));
+ if (res == 20)
+ msg (0, "computed MUS of size %d out of %d (%.0f%%)",
+ n, nclauses, percent (n, nclauses));
if (output_name && strcmp (output_name, "-")) {
output_file = fopen (output_name, "w");
if (!output_file) die ("can not write '%s'", output_name);
@@ -368,7 +390,7 @@
if (close_output) fclose (output_file);
}
if (res == 20) {
- if (!nowitness) {
+ if (!nowitness && verbose >= 0) {
for (i = 0; i < nclauses; i++)
if (!clauses[i].red) printf ("v %d\n", i+1);
printf ("v 0\n");
diff -Nru picosat-959/picosat.c picosat-960/picosat.c
--- picosat-959/picosat.c 2014-02-07 06:23:28.000000000 +0000
+++ picosat-960/picosat.c 2014-10-26 10:03:30.000000000 +0000
@@ -1322,7 +1322,10 @@
#endif
if (learned && size > 2)
- *CLS2ACT (res) = ps->cinc;
+ {
+ Act * p = CLS2ACT (res);
+ *p = ps->cinc;
+ }
return res;
}
@@ -1456,8 +1459,6 @@
delete_zhains (ps);
#endif
#ifdef NO_BINARY_CLAUSES
- ps->implvalid = 0;
- ps->cimplvalid = 0;
{
unsigned i;
for (i = 2; i <= 2 * ps->max_var + 1; i++)
@@ -1469,7 +1470,6 @@
#endif
#ifndef NFL
DELETEN (ps->saved, ps->saved_size);
- ps->saved_size = 0;
#endif
DELETEN (ps->htps, 2 * ps->size_vars);
#ifndef NDSC
@@ -1480,204 +1480,33 @@
DELETEN (ps->jwh, 2 * ps->size_vars);
DELETEN (ps->vars, ps->size_vars);
DELETEN (ps->rnks, ps->size_vars);
-
DELETEN (ps->trail, ps->eot - ps->trail);
- ps->trail = ps->ttail = ps->ttail2 = ps->thead = ps->eot = 0;
-#ifndef NADC
- ps->ttailado = 0;
-#endif
-
DELETEN (ps->heap, ps->eoh - ps->heap);
- ps->heap = ps->hhead = ps->eoh = 0;
-
DELETEN (ps->als, ps->eoals - ps->als);
- ps->als = ps->eoals = ps->alshead = ps->alstail = 0;
- ps->extracted_all_failed_assumptions = 0;
- ps->failed_assumption = 0;
- ps->adecidelevel = 0;
DELETEN (ps->CLS, ps->eocls - ps->CLS);
- ps->CLS = ps->eocls = ps->clshead = 0;
DELETEN (ps->rils, ps->eorils - ps->rils);
- ps->rils = ps->eorils = ps->rilshead = 0;
DELETEN (ps->cils, ps->eocils - ps->cils);
- ps->cils = ps->eocils = ps->cilshead = 0;
DELETEN (ps->fals, ps->eofals - ps->fals);
- ps->fals = ps->eofals = ps->falshead = 0;
DELETEN (ps->mass, ps->szmass);
- ps->szmass = 0;
- ps->mass = 0;
DELETEN (ps->mssass, ps->szmssass);
- ps->szmssass = 0;
- ps->mssass = 0;
DELETEN (ps->mcsass, ps->szmcsass);
- ps->nmcsass = ps->szmcsass = 0;
- ps->mcsass = 0;
DELETEN (ps->humus, ps->szhumus);
- ps->szhumus = 0;
- ps->humus = 0;
-
- ps->size_vars = 0;
- ps->max_var = 0;
-
- ps->mtcls = 0;
-#ifdef TRACE
- ps->ocore = -1;
-#endif
- ps->conflict = 0;
-
DELETEN (ps->added, ps->eoa - ps->added);
- ps->eoa = ps->ahead = 0;
-
DELETEN (ps->marked, ps->eom - ps->marked);
- ps->eom = ps->mhead = 0;
-
DELETEN (ps->dfs, ps->eod - ps->dfs);
- ps->eod = ps->dhead = 0;
-
DELETEN (ps->resolved, ps->eor - ps->resolved);
- ps->eor = ps->rhead = 0;
-
DELETEN (ps->levels, ps->eolevels - ps->levels);
- ps->eolevels = ps->levelshead = 0;
-
DELETEN (ps->dused, ps->eodused - ps->dused);
- ps->eodused = ps->dusedhead = 0;
-
DELETEN (ps->buffer, ps->eob - ps->buffer);
- ps->eob = ps->bhead = 0;
-
DELETEN (ps->indices, ps->eoi - ps->indices);
- ps->eoi = ps->ihead = 0;
-
DELETEN (ps->soclauses, ps->eoso - ps->soclauses);
- ps->soclauses = ps->eoso = ps->sohead = 0;
- ps->saveorig = ps->partial = 0;
-
delete_prefix (ps);
-
delete (ps, ps->rline[0], ps->szrline);
delete (ps, ps->rline[1], ps->szrline);
- ps->rline[0] = ps->rline[1] = 0;
- ps->szrline = ps->RCOUNT = 0;
assert (getenv ("LEAK") || !ps->current_bytes); /* found leak if failing */
- ps->max_bytes = 0;
- ps->recycled = 0;
- ps->current_bytes = 0;
-
- ps->lrestart = 0;
- ps->lreduce = 0;
- ps->lastreduceconflicts = 0;
- ps->llocked = 0;
- ps->lsimplify = 0;
- ps->fsimplify = 0;
-
- ps->seconds = 0;
- ps->flseconds = 0;
- ps->entered = 0;
- ps->nentered = 0;
- ps->measurealltimeinlib = 0;
-
- ps->levelsum = 0.0;
- ps->calls = 0;
- ps->decisions = 0;
- ps->restarts = 0;
- ps->simps = 0;
- ps->iterations = 0;
- ps->reports = 0;
- ps->lastrheader = -2;
- ps->fixed = 0;
-#ifndef NFL
- ps->failedlits = 0;
- ps->simplifying = 0;
- ps->fllimit = 0;
-#ifdef STATS
- ps->efailedlits = ps->ifailedlits = 0;
- ps->fltried = ps->flskipped = ps->floopsed = 0;
- ps->flcalls = ps->flrounds = 0;
- ps->flprops = 0;
-#endif
-#endif
- ps->propagations = 0;
- ps->contexts = 0;
- ps->internals = 0;
- ps->conflicts = 0;
- ps->noclauses = 0;
- ps->oadded = 0;
- ps->lladded = 0;
- ps->loadded = 0;
- ps->olits = 0;
- ps->nlclauses = 0;
- ps->ladded = 0;
- ps->addedclauses = 0;
- ps->llits = 0;
- ps->out = 0;
-#ifdef TRACE
- ps->trace = 0;
-#endif
- ps->rup = 0;
- ps->rupstarted = 0;
- ps->rupclauses = 0;
- ps->rupvariables = 0;
- ps->LEVEL = 0;
-
- ps->reductions = 0;
-
- ps->vused = 0;
- ps->llitsadded = 0;
- ps->visits = 0;
-#ifdef STATS
- ps->loused = 0;
- ps->llused = 0;
- ps->bvisits = 0;
- ps->tvisits = 0;
- ps->lvisits = 0;
- ps->othertrue = 0;
- ps->othertrue2 = 0;
- ps->othertruel = 0;
- ps->othertrue2u = 0;
- ps->othertruelu = 0;
- ps->ltraversals = 0;
- ps->traversals = 0;
-#ifndef NO_BINARY_CLAUSES
- ps->antecedents = 0;
-#endif
- ps->znts = 0;
- ps->uips = 0;
- ps->assumptions = 0;
- ps->rdecisions = 0;
- ps->sdecisions = 0;
- ps->srecycled = 0;
- ps->rrecycled = 0;
-#endif
- ps->minimizedllits = 0;
- ps->nonminimizedllits = 0;
- ps->state = RESET;
- ps->srng = 0;
-
- ps->saved_flips = 0;
- ps->saved_max_var = 0;
- ps->min_flipped = UINT_MAX;
-
- ps->flips = 0;
-#ifdef STATS
- ps->FORCED = 0;
- ps->assignments = 0;
-#endif
-
- ps->sdflips = 0;
- ps->defaultphase = JWLPHASE;
-
-#ifdef STATS
- ps->staticphasedecisions = 0;
- ps->inclreduces = 0;
- ps->skippedrestarts = 0;
-#endif
-
#ifdef VISCORES
pclose (ps->fviscores);
- ps->fviscores = 0;
#endif
-
if (ps->edelete)
ps->edelete (ps->emgr, ps, sizeof *ps);
else
@@ -1954,11 +1783,9 @@
if (c == &ps->impl)
return;
-#else
-#ifdef STATS
+#elif defined(STATS) && defined(TRACE)
ps->antecedents++;
#endif
-#endif
if (ps->rhead == ps->eor)
ENLARGE (ps->resolved, ps->rhead, ps->eor);
@@ -2960,7 +2787,7 @@
Ltk * s;
Lit ** p;
- for (s = ps->impls + 2; s < ps->impls + 2 * ps->max_var; s++)
+ for (s = ps->impls + 2; s <= ps->impls + 2 * ps->max_var + 1; s++)
for (p = s->start; p < s->start + s->count; p++)
*p += delta;
}
@@ -3061,21 +2888,26 @@
RESIZEN (ps->vars, ps->size_vars, new_size_vars);
RESIZEN (ps->rnks, ps->size_vars, new_size_vars);
- lits_delta = ps->lits - old_lits;
- rnks_delta = ps->rnks - old_rnks;
-
- fix_trail_lits (ps, lits_delta);
- fix_clause_lits (ps, lits_delta);
- fix_added_lits (ps, lits_delta);
- fix_assumed_lits (ps, lits_delta);
- fix_cls_lits (ps, lits_delta);
+ if ((lits_delta = ps->lits - old_lits))
+ {
+ fix_trail_lits (ps, lits_delta);
+ fix_clause_lits (ps, lits_delta);
+ fix_added_lits (ps, lits_delta);
+ fix_assumed_lits (ps, lits_delta);
+ fix_cls_lits (ps, lits_delta);
#ifdef NO_BINARY_CLAUSES
- fix_impl_lits (ps, lits_delta);
+ fix_impl_lits (ps, lits_delta);
#endif
#ifndef NADC
- fix_ados (ps, lits_delta);
+ fix_ados (ps, lits_delta);
#endif
- fix_heap_rnks (ps, rnks_delta);
+ }
+
+ if ((rnks_delta = ps->rnks - old_rnks))
+ {
+ fix_heap_rnks (ps, rnks_delta);
+ }
+
assert (ps->mhead == ps->marked);
ps->size_vars = new_size_vars;
@@ -4616,11 +4448,11 @@
assert (ps->max_var < ps->size_vars);
- ps->max_var++; /* new index of variable */
- assert (ps->max_var); /* no unsigned overflow */
+ if (ps->max_var + 1 == ps->size_vars)
+ enlarge (ps, ps->size_vars + 2*(ps->size_vars + 3) / 4); /* +25% */
- if (ps->max_var == ps->size_vars)
- enlarge (ps, ps->size_vars + (ps->size_vars + 3) / 4); /* +25% */
+ ps->max_var++; /* new index of variable */
+ assert (ps->max_var); /* no unsigned overflow */
assert (ps->max_var < ps->size_vars);
@@ -4846,7 +4678,8 @@
{
Lit * other = *s;
Var *v = LIT2VAR (other);
- if (v->level || other->val != TRUE)
+ if (v->level ||
+ other->val != TRUE)
*r++ = other;
}
lstk->count = r - lstk->start;
@@ -5611,8 +5444,7 @@
static int
cmp_glue_activity_size (PS * ps, Cls * c, Cls * d)
{
- Act a;
- Act b;
+ Act a, b, * p, * q;
(void) ps;
@@ -5625,8 +5457,10 @@
if (c->glue > d->glue)
return -1;
- a = *CLS2ACT (c);
- b = *CLS2ACT (d);
+ p = CLS2ACT (c);
+ q = CLS2ACT (d);
+ a = *p;
+ b = *q;
if (a < b) // then higher activity
return -1;
@@ -7100,6 +6934,29 @@
}
static int
+tderef (PS * ps, int int_lit)
+{
+ Lit * lit;
+ Var * v;
+
+ assert (abs (int_lit) <= (int) ps->max_var);
+
+ lit = int2lit (ps, int_lit);
+
+ v = LIT2VAR (lit);
+ if (v->level > 0)
+ return 0;
+
+ if (lit->val == TRUE)
+ return 1;
+
+ if (lit->val == FALSE)
+ return -1;
+
+ return 0;
+}
+
+static int
pderef (PS * ps, int int_lit)
{
Lit * lit;
@@ -7127,6 +6984,9 @@
{
unsigned * occs, maxoccs, tmpoccs, npartial;
int * p, * c, lit, best, val;
+#ifdef LOGGING
+ int tl;
+#endif
assert (!ps->partial);
@@ -7141,10 +7001,25 @@
for (c = ps->soclauses; c < ps->sohead; c = p + 1)
{
+#ifdef LOGGING
+ tl = 0;
+#endif
best = 0;
maxoccs = 0;
for (p = c; (lit = *p); p++)
{
+ val = tderef (ps, lit);
+ if (val < 0)
+ continue;
+ if (val > 0)
+ {
+#ifdef LOGGING
+ tl = 1;
+#endif
+ best = lit;
+ maxoccs = occs[lit];
+ }
+
val = pderef (ps, lit);
if (val > 0)
break;
@@ -7163,8 +7038,8 @@
if (!lit)
{
assert (best);
- LOG ( fprintf (ps->out, "%sautark %d with %d occs\n",
- ps->prefix, best, maxoccs));
+ LOG ( fprintf (ps->out, "%sautark %d with %d occs%s\n",
+ ps->prefix, best, maxoccs, tl ? " (top)" : ""));
ps->vars[abs (best)].partial = 1;
npartial++;
}
@@ -7302,9 +7177,6 @@
int
picosat_deref_toplevel (PS * ps, int int_lit)
{
- Lit *lit;
- Var * v;
-
check_ready (ps);
ABORTIF (!int_lit, "API usage: can not deref zero literal");
@@ -7314,19 +7186,7 @@
if (abs (int_lit) > (int) ps->max_var)
return 0;
- lit = int2lit (ps, int_lit);
-
- v = LIT2VAR (lit);
- if (v->level > 0)
- return 0;
-
- if (lit->val == TRUE)
- return 1;
-
- if (lit->val == FALSE)
- return -1;
-
- return 0;
+ return tderef (ps, int_lit);
}
int
@@ -8160,16 +8020,12 @@
ps->prefix, PERCENT (redlits, ps->nonminimizedllits));
#ifdef STATS
-#ifndef NO_BINARY_CLAUSES
+#ifdef TRACE
fprintf (ps->out,
"%s%llu antecedents (%.1f antecedents per clause",
ps->prefix, ps->antecedents, AVERAGE (ps->antecedents, ps->conflicts));
-#endif
-#ifdef TRACE
if (ps->trace)
fprintf (ps->out, ", %.1f bytes/antecedent)", AVERAGE (ps->znts, ps->antecedents));
-#endif
-#if !defined(NO_BINARY_CLAUSES) || defined(TRACE)
fputs (")\n", ps->out);
#endif
diff -Nru picosat-959/VERSION picosat-960/VERSION
--- picosat-959/VERSION 2014-02-07 06:23:28.000000000 +0000
+++ picosat-960/VERSION 2014-10-26 10:03:30.000000000 +0000
@@ -1 +1 @@
-959
+960
diff -Nru undertaker-1.6/debian/changelog undertaker-1.6/debian/changelog
--- undertaker-1.6/debian/changelog 2014-10-19 21:04:57.000000000 +0100
+++ undertaker-1.6/debian/changelog 2014-11-12 04:07:57.000000000 +0000
@@ -1,3 +1,11 @@
+undertaker (1.6-2) unstable; urgency=medium
+
+ * Use system picsoat >= 960 (Closes: #766273)
+ * Apply logic bugfix from upstream for undertaker-checkpatch when
+ calucating statistics about Kconfig changes.
+
+ -- Reinhard Tartler <siretart@tauware.de> Tue, 11 Nov 2014 23:05:38 -0500
+
undertaker (1.6-1) unstable; urgency=medium
* New upstream release
diff -Nru undertaker-1.6/debian/control undertaker-1.6/debian/control
--- undertaker-1.6/debian/control 2014-10-19 19:08:54.000000000 +0100
+++ undertaker-1.6/debian/control 2014-11-12 04:00:27.000000000 +0000
@@ -15,6 +15,7 @@
libboost-wave-dev (>= 1.40),
libpstreams-dev,
libpuma-dev (>= 1:1.0-4~),
+ picosat (>= 960),
python-all (>= 2.6.6-3~)
Standards-Version: 3.9.5
Homepage: http://vamos.informatik.uni-erlangen.de/trac/undertaker
diff -Nru undertaker-1.6/debian/patches/series undertaker-1.6/debian/patches/series
--- undertaker-1.6/debian/patches/series 2014-10-19 21:04:57.000000000 +0100
+++ undertaker-1.6/debian/patches/series 2014-11-12 04:04:47.000000000 +0000
@@ -0,0 +1,2 @@
+update_picomus.patch
+undertaker-checkpatch-fix-Kconfig-parsing.patch
diff -Nru undertaker-1.6/debian/patches/undertaker-checkpatch-fix-Kconfig-parsing.patch undertaker-1.6/debian/patches/undertaker-checkpatch-fix-Kconfig-parsing.patch
--- undertaker-1.6/debian/patches/undertaker-checkpatch-fix-Kconfig-parsing.patch 1970-01-01 01:00:00.000000000 +0100
+++ undertaker-1.6/debian/patches/undertaker-checkpatch-fix-Kconfig-parsing.patch 2014-11-12 04:04:54.000000000 +0000
@@ -0,0 +1,27 @@
+From 69c153a00c3f4dc496ac55f3b44446b4217c9d9e Mon Sep 17 00:00:00 2001
+From: Valentin Rothberg <valentinrothberg@gmail.com>
+Date: Thu, 6 Nov 2014 18:37:00 +0100
+Subject: [PATCH] undertaker-checkpatch: fix Kconfig parsing
+
+This patch fixes the parsing of changes to Kconfig files. There is
+an internal dictionary which is meant to contain all added
+identifiers to Kconfig statements, such as 'if'/'depends on'/'select'.
+Accidentally, only removed statements have been checked which caused
+some false positives.
+
+Change-Id: I1cb950d5079a04e9a9bebf6b6c301c1c8d1be0bd
+---
+ python/undertaker-checkpatch | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+--- a/python/undertaker-checkpatch
++++ b/python/undertaker-checkpatch
+@@ -295,7 +295,7 @@ def parse_patch(patchfile):
+ removals[path] = removed
+
+ # added statements (if, select, depends on)
+- elif change[0] and not change[1] and \
++ elif not change[0] and change[1] and \
+ REGEX_KCONFIG_STMT.match(change[2]):
+ stmts = statements.get(path, set())
+ for feature in REGEX_FEATURE.findall(change[2]):
diff -Nru undertaker-1.6/debian/patches/update_picomus.patch undertaker-1.6/debian/patches/update_picomus.patch
--- undertaker-1.6/debian/patches/update_picomus.patch 1970-01-01 01:00:00.000000000 +0100
+++ undertaker-1.6/debian/patches/update_picomus.patch 2014-11-12 03:59:14.000000000 +0000
@@ -0,0 +1,45 @@
+From: Stefan Hengelein <stefan.hengelein@fau.de>
+Date: Mon, 10 Nov 2014 14:24:34 +0100
+Subject: [PATCH] undertaker: adjust picomus call for debian release
+
+This patches uses the new "quiet" mode of picomus 960. Earlier version
+of picomus did not support the "-q" option but produce slightly
+different diagnostic messages.
+
+---
+ Makefile | 2 --
+ undertaker/BlockDefectAnalyzer.cpp | 5 +----
+ 2 files changed, 1 insertion(+), 6 deletions(-)
+
+--- a/Makefile
++++ b/Makefile
+@@ -115,8 +115,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)
+--- a/undertaker/BlockDefectAnalyzer.cpp
++++ b/undertaker/BlockDefectAnalyzer.cpp
+@@ -247,7 +247,7 @@ void DeadBlockDefect::reportMUS(Configur
+ 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(Configur
+ 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
Attachment:
pgpVYwUdkPiLd.pgp
Description: PGP signature