Skip to content

Commit

Permalink
Issue #96: Fix LevelWeight comparison.
Browse files Browse the repository at this point in the history
* MinimizeBuilder::CmpWeight failed to handle missing levels correctly.
  In particular, if a tuple R with *negative* weight w at level p was
  compared to a tuple L with missing weight at p, RHS was incorrectly
  considered to be greater than L. Fix this so that now the weight at
  p is compared to 0 (no weight at p).
  • Loading branch information
BenKaufmann committed Oct 1, 2023
1 parent b08da9a commit 686973b
Show file tree
Hide file tree
Showing 2 changed files with 35 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/minimize_constraint.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -617,7 +617,9 @@ bool MinimizeBuilder::CmpWeight::operator()(const MLit& lhs, const MLit& rhs) co
const SharedData::LevelWeight* wLhs = &(*weights)[lhs.weight];
const SharedData::LevelWeight* wRhs = &(*weights)[rhs.weight];
for (;; ++wLhs, ++wRhs) {
if (wLhs->level != wRhs->level) { return wLhs->level < wRhs->level; }
if (wLhs->level != wRhs->level) {
return wLhs->level < wRhs->level ? wLhs->weight > 0 : 0 > wRhs->weight;
}
if (wLhs->weight != wRhs->weight){ return wLhs->weight > wRhs->weight; }
if (!wLhs->next) { return wRhs->next && (++wRhs)->weight < 0; }
if (!wRhs->next) { ++wLhs; break; }
Expand Down
32 changes: 32 additions & 0 deletions tests/minimize_test.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -247,6 +247,38 @@ TEST_CASE("Model-guided minimize", "[constraint][asp]") {
REQUIRE((newMin->shared()->weights[0].weight == 1));
REQUIRE((newMin->shared()->weights[1].weight == -5));
}
SECTION("testSparseCompare") {
mb.add(0, WeightLiteral(b, 1));
mb.add(1, WeightLiteral(a, 1));
mb.add(2, WeightLiteral(c, -1));
mb.add(2, WeightLiteral(b, -2));
mb.add(2, WeightLiteral(a, -2));

newMin = test.buildAndAttach(mb);
MinimizeConstraint::SharedDataP shared = newMin->shared();

#define CHECK_LEVEL_WEIGHT(idx, w, l, n) \
CHECK(shared->weights.at(idx).weight == w); \
CHECK(shared->weights.at(idx).level == l); \
CHECK(shared->weights.at(idx).next == n)

REQUIRE(test.countMinLits() == 3);

CHECK(shared->lits[0] == WeightLiteral(~b, 0));
CHECK_LEVEL_WEIGHT(0, 2, 0, 1);
CHECK_LEVEL_WEIGHT(1, -1, 2, 0);

CHECK(shared->lits[1] == WeightLiteral(~a, 2));
CHECK_LEVEL_WEIGHT(2, 2, 0, 1);
CHECK_LEVEL_WEIGHT(3, -1, 1, 0);

CHECK(shared->lits[2] == WeightLiteral(~c, 4));
CHECK_LEVEL_WEIGHT(4, 1, 0, 0);

CHECK(shared->adjust(0) == -5);
CHECK(shared->adjust(1) == 1);
CHECK(shared->adjust(2) == 1);
}
SECTION("testInitFromOther") {
min.push_back( WeightLiteral(~a, 2) );
min.push_back( WeightLiteral(~a, -3));
Expand Down

0 comments on commit 686973b

Please sign in to comment.