diff -Nru clasp-3.1.3/CHANGES clasp-3.1.4/CHANGES --- clasp-3.1.3/CHANGES 2015-07-31 13:49:44.000000000 +0000 +++ clasp-3.1.4/CHANGES 2015-12-10 12:14:58.000000000 +0000 @@ -1,3 +1,13 @@ +clasp 3.1.4: Thursday, 10th December 2015 + * fixed: "--pre" failed to handle choice/disjunctive heads defined by extended bodies + * fixed: "--backprop" failed to backpropagte certain constraints when used with "--eq=0" + * fixed: potential deadlock during shutdown/join() in async solving + * fixed: DomainHeuristic failed to handle nested heuristic predicates + * fixed: invalid delete in DomainHeuristic destructor + * fixed: configuration sometimes failed to initialize solver id + * rewrote Clause::updateWatch() loop to workaround bug #67892 in gcc 5 + (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=67892) + clasp 3.1.3: Friday, 31th July 2015 * fixed: possible livelock in multi-threaded enumeration of optimal models * fixed: parser for _heuristic atoms failed to handle atoms containing strings diff -Nru clasp-3.1.3/debian/changelog clasp-3.1.4/debian/changelog --- clasp-3.1.3/debian/changelog 2015-10-05 05:44:19.000000000 +0000 +++ clasp-3.1.4/debian/changelog 2015-12-20 11:06:49.000000000 +0000 @@ -1,3 +1,11 @@ +clasp (3.1.4-1) unstable; urgency=medium + + * Imported Upstream version 3.1.4 + * Remove g++5 patch introduced in clasp 3.1.3-2 + * Fix dep5-copyright-license-name-not-unique + + -- Thomas Krennwallner Sun, 20 Dec 2015 12:06:30 +0100 + clasp (3.1.3-2) unstable; urgency=medium * Circumvent g++-5 loop code generation bug. diff -Nru clasp-3.1.3/debian/copyright clasp-3.1.4/debian/copyright --- clasp-3.1.3/debian/copyright 2015-10-05 05:44:19.000000000 +0000 +++ clasp-3.1.4/debian/copyright 2015-12-20 11:06:49.000000000 +0000 @@ -7,36 +7,11 @@ Files: * Copyright: 2006-2014, Benjamin Kaufmann License: GPL-2+ - This program is free software; you can redistribute it - and/or modify it under the terms of the GNU General Public - License as published by the Free Software Foundation; either - version 2 of the License, or (at your option) any later - version. - . - This program 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 General Public License for more - details. - . - You should have received a copy of the GNU General Public - License along with this package; if not, write to the Free - Software Foundation, Inc., 51 Franklin St, Fifth Floor, - Boston, MA 02110-1301 USA - . - On Debian systems, the full text of the GNU General Public - License version 2 can be found in the file - `/usr/share/common-licenses/GPL-2'. Files: debian/* Copyright: 2010-2015, Thomas Krennwallner License: GPL-2+ - This package was debianized by Thomas Krennwallner - on Thu, 04 Mar 2010 19:31:51 +0100 - . - On Debian systems, the complete text of the GNU General - Public License version 2 can be found in `/usr/share/common-licenses/GPL-2'. Files: libclasp/clasp/satelite.h @@ -67,6 +42,9 @@ Files: libprogram_opts/* Copyright: 2004, 2006-2007, 2010 Benjamin Kaufmann License: GPL-2+ + + +License: GPL-2+ This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either diff -Nru clasp-3.1.3/debian/patches/clasp-g++5.patch clasp-3.1.4/debian/patches/clasp-g++5.patch --- clasp-3.1.3/debian/patches/clasp-g++5.patch 2015-10-05 05:44:19.000000000 +0000 +++ clasp-3.1.4/debian/patches/clasp-g++5.patch 1970-01-01 00:00:00.000000000 +0000 @@ -1,21 +0,0 @@ -Author: Roland Kaminski -Description: Circumvent g++-5 loop code generation bug. -Origin: upstream, http://sourceforge.net/p/potassco/mailman/message/34512643/ -Forwarded: not-needed -Bug: http://sourceforge.net/p/potassco/mailman/message/34487825/ -Bug-Debian: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=800526 -Index: clasp-git-gbp/libclasp/src/clause.cpp -=================================================================== ---- clasp-git-gbp.orig/libclasp/src/clause.cpp -+++ clasp-git-gbp/libclasp/src/clause.cpp -@@ -472,7 +472,9 @@ uint32 Clause::computeAllocSize() const - bool Clause::updateWatch(Solver& s, uint32 pos) { - uint32 idx = data_.local.idx; - if (!isSmall()) { -- for (Literal* tailS = head_ + ClauseHead::HEAD_LITS, *end = longEnd();;) { -+ while (true) { -+ Literal* tailS = head_ + ClauseHead::HEAD_LITS; -+ Literal* end = longEnd(); - for (Literal* it = tailS + idx; it < end; ++it) { - if (!s.isFalse(*it)) { - std::swap(*it, head_[pos]); diff -Nru clasp-3.1.3/debian/patches/series clasp-3.1.4/debian/patches/series --- clasp-3.1.3/debian/patches/series 2015-10-05 05:44:19.000000000 +0000 +++ clasp-3.1.4/debian/patches/series 2015-12-20 11:06:49.000000000 +0000 @@ -1,2 +1 @@ -clasp-g++5.patch clasp-manpage.patch diff -Nru clasp-3.1.3/libclasp/clasp/clasp_facade.h clasp-3.1.4/libclasp/clasp/clasp_facade.h --- clasp-3.1.3/libclasp/clasp/clasp_facade.h 2015-07-27 16:02:11.000000000 +0000 +++ clasp-3.1.4/libclasp/clasp/clasp_facade.h 2015-12-10 12:14:58.000000000 +0000 @@ -26,7 +26,7 @@ #endif #if !defined(CLASP_VERSION) -#define CLASP_VERSION "3.1.3" +#define CLASP_VERSION "3.1.4" #endif #if !defined(CLASP_LEGAL) #define CLASP_LEGAL \ diff -Nru clasp-3.1.3/libclasp/src/asp_preprocessor.cpp clasp-3.1.4/libclasp/src/asp_preprocessor.cpp --- clasp-3.1.3/libclasp/src/asp_preprocessor.cpp 2015-07-27 16:02:11.000000000 +0000 +++ clasp-3.1.4/libclasp/src/asp_preprocessor.cpp 2015-12-10 12:14:58.000000000 +0000 @@ -37,8 +37,11 @@ // set up body if (!b->simplify(*prg_, false)) { return false; } if (b->var() < startVar) { b->assignVar(*prg_); } - // add all heads of b to the "upper"-closure - if (!addHeadsToUpper(b)) { return false; } + // add all heads of b to the "upper"-closure and + // remove any false/removed atoms from head + if (!addHeadsToUpper(b) || !b->simplifyHeads(*prg_, true)) { + return false; + } } return prg_->propagate(); } diff -Nru clasp-3.1.3/libclasp/src/clasp_facade.cpp clasp-3.1.4/libclasp/src/clasp_facade.cpp --- clasp-3.1.3/libclasp/src/clasp_facade.cpp 2015-07-27 16:02:11.000000000 +0000 +++ clasp-3.1.4/libclasp/src/clasp_facade.cpp 2015-12-10 12:14:58.000000000 +0000 @@ -182,7 +182,12 @@ Clasp::thread(std::mem_fun(&AsyncSolve::threadMain), this, &f).swap(task); } virtual bool cancel(int sig) { - return SolveStrategy::cancel(sig) && (sig != SIGCANCEL || wait()); + if (!SolveStrategy::cancel(sig)) return false; + if (sig == SIGCANCEL) { + wait(); + join(); + } + return true; } void threadMain(ClaspFacade* f) { try { runAlgo(*f, state_running); } @@ -202,6 +207,7 @@ bool next() { if (state != state_model) { return false; } unique_lock lock(mqMutex); + if (state != state_model) { return false; } state = state_running; mqCond.notify_one(); return true; diff -Nru clasp-3.1.3/libclasp/src/clause.cpp clasp-3.1.4/libclasp/src/clause.cpp --- clasp-3.1.3/libclasp/src/clause.cpp 2015-07-27 16:02:11.000000000 +0000 +++ clasp-3.1.4/libclasp/src/clause.cpp 2015-12-10 12:14:58.000000000 +0000 @@ -470,23 +470,23 @@ } bool Clause::updateWatch(Solver& s, uint32 pos) { - uint32 idx = data_.local.idx; + uint32* n; if (!isSmall()) { - for (Literal* tailS = head_ + ClauseHead::HEAD_LITS, *end = longEnd();;) { - for (Literal* it = tailS + idx; it < end; ++it) { + for (Literal* begin = head_ + ClauseHead::HEAD_LITS, *end = longEnd(), *first = begin + data_.local.idx;;) { + for (Literal* it = first; it < end; ++it) { if (!s.isFalse(*it)) { std::swap(*it, head_[pos]); - data_.local.idx = static_cast(++it - tailS); + data_.local.idx = static_cast(++it - begin); return true; } } - if (idx == 0) { break; } - end = tailS + idx; - idx = 0; + if (first == begin) { break; } + end = first; + first = begin; } } - else if (!s.isFalse(Literal::fromRep(data_.lits[idx=0])) || !s.isFalse(Literal::fromRep(data_.lits[idx=1]))) { - std::swap(head_[pos].asUint(), data_.lits[idx]); + else if (!s.isFalse(Literal::fromRep(*(n = data_.lits))) || !s.isFalse(Literal::fromRep(*++n))) { + std::swap(head_[pos].asUint(), *n); return true; } return false; diff -Nru clasp-3.1.3/libclasp/src/heuristics.cpp clasp-3.1.4/libclasp/src/heuristics.cpp --- clasp-3.1.3/libclasp/src/heuristics.cpp 2015-07-27 16:02:11.000000000 +0000 +++ clasp-3.1.4/libclasp/src/heuristics.cpp 2015-12-10 12:14:58.000000000 +0000 @@ -689,7 +689,6 @@ frames_.push_back(Frame(0,UINT32_MAX)); } DomainHeuristic::~DomainHeuristic() { - delete domMin_; } void DomainHeuristic::setDefaultMod(GlobalModifier mod, uint32 prefSet) { defMod_ = (uint16)mod; @@ -733,8 +732,10 @@ uint32 nKey = (uint32)prios_.size(), uKey = nKey; uint32 nRules = (uint32)domTab.size(); if (&s == s.sharedContext()->master()) { domMin_ = &s.sharedContext()->symbolTable().domLits; } + typedef PodVector >::type InitVec; + InitVec initVals; for (SymbolTable::const_iterator sIt = s.symbolTable().begin(), end = s.symbolTable().end(); sIt != end && nRules; ++sIt) { - if (sIt->second.name.empty() || DomEntry::isDomEntry(sIt->second) || s.topValue(sIt->second.lit.var()) != value_free) { continue; } + if (sIt->second.name.empty() || s.topValue(sIt->second.lit.var()) != value_free) { continue; } const char* head = sIt->second.name.c_str(); Var ev = 0; int16 init = 0; @@ -765,9 +766,18 @@ } } if (ev && init) { - score_[ev].value += init; + initVals.push_back(std::make_pair(ev, uint32(init))); } } + std::sort(initVals.begin(), initVals.end()); + for (InitVec::const_iterator it = initVals.begin(), end = initVals.end(); it != end; ++it) { + uint32 val = it->second; + for (InitVec::const_iterator j = it + 1; j != end && j->first == it->first; it = j++) { + if (j->second > val) { val = j->second; } + } + score_[it->first].value += val; + } + InitVec().swap(initVals); DomTable().swap(domTab); if (s.symbolTable().incremental()) { uKey = nKey; } if (uKey != nKey) { diff -Nru clasp-3.1.3/libclasp/src/logic_program.cpp clasp-3.1.4/libclasp/src/logic_program.cpp --- clasp-3.1.3/libclasp/src/logic_program.cpp 2015-07-27 16:02:11.000000000 +0000 +++ clasp-3.1.4/libclasp/src/logic_program.cpp 2015-12-10 12:14:58.000000000 +0000 @@ -325,27 +325,43 @@ os << activeBody_.ruleType() << " " << falseAtom << " " << activeBody_ << "\n"; } else { - activeHead_.clear(); + activeHead_.clear(); uint32 nDisj = 0; for (PrgBody::head_iterator hIt = b->heads_begin(); hIt != b->heads_end(); ++hIt) { if (!getHead(*hIt)->hasVar() || hIt->isGamma()) { continue; } if (hIt->isAtom()) { - if (hIt->isNormal()) { os << activeBody_.ruleType() << " " << hIt->node() << " " << activeBody_ << "\n"; } - else if (hIt->isChoice()) { activeHead_.push_back(hIt->node()); } - } - else if (hIt->isDisj()) { - PrgDisj* d = getDisj(hIt->node()); - os << DISJUNCTIVERULE << " " << d->size() << " "; - for (PrgDisj::atom_iterator a = d->begin(), aEnd = d->end(); a != aEnd; ++a) { - os << a->node() << " "; + if (hIt->isNormal()) { + os << activeBody_.ruleType() << " " << hIt->node() << " " << activeBody_ << "\n"; + if (activeBody_.type() != BodyInfo::NORMAL_BODY && getHead(*hIt)->literal() == b->literal()) { + activeBody_.reset(); + Literal lit = posLit(hIt->node()); + activeBody_.init(BodyInfo::NORMAL_BODY, 1, hashLit(lit), 1); + activeBody_.lits.push_back(WeightLiteral(lit, 1)); + } } - os << activeBody_ << "\n"; + else if (hIt->isChoice()) { activeHead_.push_back(hIt->node()); } } + else if (hIt->isDisj()) { ++nDisj; } } if (!activeHead_.empty()) { os << CHOICERULE << " " << activeHead_.size() << " "; std::copy(activeHead_.begin(), activeHead_.end(), std::ostream_iterator(os, " ")); + assert(activeBody_.type() == BodyInfo::NORMAL_BODY); os << activeBody_ << "\n"; } + if (nDisj) { + assert(activeBody_.type() == BodyInfo::NORMAL_BODY); + for (PrgBody::head_iterator hIt = b->heads_begin(); hIt != b->heads_end(); ++hIt) { + if (hIt->isDisj()) { + PrgDisj* d = getDisj(hIt->node()); + os << DISJUNCTIVERULE << " " << d->size() << " "; + for (PrgDisj::atom_iterator a = d->begin(), aEnd = d->end(); a != aEnd; ++a) { + os << a->node() << " "; + } + os << activeBody_ << "\n"; + if (--nDisj == 0) break; + } + } + } } } } diff -Nru clasp-3.1.3/libclasp/src/model_enumerators.cpp clasp-3.1.4/libclasp/src/model_enumerators.cpp --- clasp-3.1.3/libclasp/src/model_enumerators.cpp 2015-07-27 16:02:11.000000000 +0000 +++ clasp-3.1.4/libclasp/src/model_enumerators.cpp 2015-12-10 12:14:58.000000000 +0000 @@ -244,7 +244,7 @@ void ModelEnumerator::setStrategy(Strategy st, uint32 projection) { options_ = uint32(st) | ((projection & 15u) << 4u); project_ = 0; - if ((projection & 7u) != 0) { + if ((projection & 15u) != 0) { options_ |= uint32(project_enable_simple) << 4u; project_ = new VarVec(); } diff -Nru clasp-3.1.3/libclasp/src/solver_strategies.cpp clasp-3.1.4/libclasp/src/solver_strategies.cpp --- clasp-3.1.3/libclasp/src/solver_strategies.cpp 2015-07-27 16:02:11.000000000 +0000 +++ clasp-3.1.4/libclasp/src/solver_strategies.cpp 2015-12-10 12:14:58.000000000 +0000 @@ -260,7 +260,10 @@ return Heuristic_t::create(BasicSatConfig::solver(i)); } SolverParams& BasicSatConfig::addSolver(uint32 i) { - if (i >= solver_.size()) { solver_.resize(i+1); solver_[i].id = i;} + while (i >= solver_.size()) { + solver_.push_back(SolverParams()); + solver_.back().id = static_cast(solver_.size()) - 1; + } return solver_[i]; } SolveParams& BasicSatConfig::addSearch(uint32 i) { diff -Nru clasp-3.1.3/libclasp/tests/cli_test.cpp clasp-3.1.4/libclasp/tests/cli_test.cpp --- clasp-3.1.3/libclasp/tests/cli_test.cpp 2015-07-27 16:02:11.000000000 +0000 +++ clasp-3.1.4/libclasp/tests/cli_test.cpp 2015-12-10 12:14:58.000000000 +0000 @@ -114,8 +114,16 @@ void testConfigImplicitCreateSolver() { ClaspCliConfig config; CPPUNIT_ASSERT(config.numSolver() == 1); - CPPUNIT_ASSERT(config.setValue("solver.1.heuristic", "berkmin") && config.solver(1).heuId == Heuristic_t::heu_berkmin); + // solver option + CPPUNIT_ASSERT(config.setValue("solver.1.heuristic", "berkmin")); CPPUNIT_ASSERT(config.numSolver() == 2); + CPPUNIT_ASSERT(config.solver(1).heuId == Heuristic_t::heu_berkmin); + + CPPUNIT_ASSERT(config.setValue("solver.17.heuristic", "unit")); + CPPUNIT_ASSERT(config.numSolver() == 18); + for (uint32 i = 0; i != config.numSolver(); ++i) { + CPPUNIT_ASSERT_EQUAL_MESSAGE("solver id not set", i, config.solver(i).id); + } } void testConfigImplicitCreateTester() { ClaspCliConfig config; diff -Nru clasp-3.1.3/libclasp/tests/program_builder_test.cpp clasp-3.1.4/libclasp/tests/program_builder_test.cpp --- clasp-3.1.3/libclasp/tests/program_builder_test.cpp 2015-07-31 09:26:05.000000000 +0000 +++ clasp-3.1.4/libclasp/tests/program_builder_test.cpp 2015-12-10 12:14:58.000000000 +0000 @@ -77,6 +77,7 @@ CPPUNIT_TEST(testRegressionR1); CPPUNIT_TEST(testRegressionR2); CPPUNIT_TEST(testFuzzBug); + CPPUNIT_TEST(testBackpropNoEqBug); CPPUNIT_TEST(testCloneShare); CPPUNIT_TEST(testCloneShareSymbols); @@ -629,6 +630,24 @@ ; CPPUNIT_ASSERT_EQUAL(false, builder.endProgram() && ctx.endInit()); } + void testBackpropNoEqBug() { + builder.start(ctx, LogicProgram::AspOptions().noEq().backpropagate()); + Var x[9]; + for (Var i = 1; i != 9; ++i) { + x[i] = builder.newAtom(); + } + builder.startRule(CHOICERULE).addHead(x[2]).addHead(x[3]).addHead(x[4]).addToBody(x[5], true).endRule(); + builder.startRule().addHead(x[1]).addToBody(x[7], true).addToBody(x[5], true).endRule(); + builder.startRule().addHead(x[5]).endRule(); + builder.startRule().addHead(x[7]).addToBody(x[2], true).addToBody(x[3], true).endRule(); + builder.startRule().addHead(x[7]).addToBody(x[6], true).endRule(); + builder.startRule().addHead(x[6]).addToBody(x[8], true).endRule(); + builder.startRule().addHead(x[8]).addToBody(x[4], true).endRule(); + builder.setCompute(x[1], false); + CPPUNIT_ASSERT_EQUAL(true, builder.endProgram() && ctx.endInit()); + CPPUNIT_ASSERT_EQUAL(true, ctx.master()->isFalse(builder.getLiteral(x[6]))); + } + void testCloneShare() { // {a, b, c}. // d :- a, b, c.