Your message dated Thu, 20 Nov 2014 23:08:23 +0000 with message-id <20141120230823.GT6216@lupin.home.powdarrmonkey.net> and subject line Re: Bug#769634: unblock: picosat/960-1 and undertaker/1.6-2 has caused the Debian Bug report #769634, regarding unblock: picosat/960-1 and undertaker/1.6-2 to be marked as done. This means that you claim that the problem has been dealt with. If this is not the case it is now your responsibility to reopen the Bug report if necessary, and/or fix the problem forthwith. (NB: If you are a system administrator and have no idea what this message is talking about, this may indicate a serious mail system misconfiguration somewhere. Please contact owner@bugs.debian.org immediately.) -- 769634: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=769634 Debian Bug Tracking System Contact owner@bugs.debian.org with problems
--- Begin Message ---
- To: submit@bugs.debian.org
- Subject: unblock: picosat/960-1 and undertaker/1.6-2
- From: Michael Tautschnig <mt@debian.org>
- Date: Sat, 15 Nov 2014 08:23:03 +0000
- Message-id: <[🔎] 20141115082303.GB29386@l04.Home>
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-2diff -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 +960diff -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 withoutAttachment: pgpJxOHucQY44.pgp
Description: PGP signature
--- End Message ---
--- Begin Message ---
- To: Michael Tautschnig <mt@debian.org>, 769634-done@bugs.debian.org
- Subject: Re: Bug#769634: unblock: picosat/960-1 and undertaker/1.6-2
- From: Jonathan Wiltshire <jmw@debian.org>
- Date: Thu, 20 Nov 2014 23:08:23 +0000
- Message-id: <20141120230823.GT6216@lupin.home.powdarrmonkey.net>
- In-reply-to: <[🔎] 20141115082303.GB29386@l04.Home>
- References: <[🔎] 20141115082303.GB29386@l04.Home>
On Sat, Nov 15, 2014 at 08:23:03AM +0000, Michael Tautschnig wrote: > 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. It's not awesome, but not terrible. Unblocked. -- Jonathan Wiltshire jmw@debian.org Debian Developer http://people.debian.org/~jmw 4096R: 0xD3524C51 / 0A55 B7C5 1223 3942 86EC 74C3 5394 479D D352 4C51Attachment: signature.asc
Description: Digital signature
--- End Message ---