00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 #include "test.h"
00021 #include <clasp/weight_constraint.h>
00022 #include <clasp/solver.h>
00023 #include <algorithm>
00024 using namespace std;
00025
00026 namespace Clasp { namespace Test {
00027 class WeightConstraintTest : public CppUnit::TestFixture {
00028 CPPUNIT_TEST_SUITE(WeightConstraintTest);
00029 CPPUNIT_TEST(testAssertTriviallySat);
00030 CPPUNIT_TEST(testAssertTriviallyUnSat);
00031 CPPUNIT_TEST(testAssertNotSoTriviallySat);
00032 CPPUNIT_TEST(testAssertNotSoTriviallyUnSat);
00033
00034 CPPUNIT_TEST(testTrivialBackpropTrue);
00035 CPPUNIT_TEST(testTrivialBackpropFalse);
00036 CPPUNIT_TEST(testTrivialBackpropFalseWeight);
00037
00038 CPPUNIT_TEST(testForwardTrue);
00039 CPPUNIT_TEST(testForwardFalse);
00040 CPPUNIT_TEST(testBackwardTrue);
00041 CPPUNIT_TEST(testBackwardFalse);
00042
00043 CPPUNIT_TEST(testForwardTrueConflict);
00044 CPPUNIT_TEST(testForwardFalseConflict);
00045 CPPUNIT_TEST(testBackwardTrueConflict);
00046 CPPUNIT_TEST(testBackwardFalseConflict);
00047
00048 CPPUNIT_TEST(testReasonBug);
00049 CPPUNIT_TEST(testWeightReasonAfterBackprop);
00050 CPPUNIT_TEST(testOrderBug);
00051 CPPUNIT_TEST(testBackwardAfterForward);
00052
00053 CPPUNIT_TEST(testSimplify);
00054 CPPUNIT_TEST(testSimplifyCardinality);
00055 CPPUNIT_TEST(testSimplifyWeight);
00056
00057 CPPUNIT_TEST(testAssertWeightTriviallySat);
00058 CPPUNIT_TEST(testAssertWeightTriviallyUnSat);
00059 CPPUNIT_TEST(testAssertWeightNotSoTriviallySat);
00060 CPPUNIT_TEST(testAssertWeightNotSoTriviallyUnSat);
00061 CPPUNIT_TEST(testWeightForwardTrue);
00062 CPPUNIT_TEST(testWeightForwardFalse);
00063 CPPUNIT_TEST(testWeightBackwardTrue);
00064 CPPUNIT_TEST(testWeightBackwardFalse);
00065 CPPUNIT_TEST(testWeightConflict);
00066
00067 CPPUNIT_TEST(testCloneWeight);
00068 CPPUNIT_TEST(testCloneWeightShared);
00069
00070 CPPUNIT_TEST(testAddOnLevel);
00071 CPPUNIT_TEST(testCreateSat);
00072 CPPUNIT_TEST(testCreateSatOnRoot);
00073 CPPUNIT_TEST(testCreateSatOnRootNoProp);
00074
00075 CPPUNIT_TEST(testMergeNegativeWeight);
00076 CPPUNIT_TEST_SUITE_END();
00077 public:
00078 WeightConstraintTest() {
00079 body = posLit(ctx.addVar(Var_t::body_var));
00080 a = posLit(ctx.addVar(Var_t::atom_var));
00081 b = posLit(ctx.addVar(Var_t::atom_var));
00082 c = posLit(ctx.addVar(Var_t::atom_var));
00083 d = posLit(ctx.addVar(Var_t::atom_var));
00084 e = posLit(ctx.addVar(Var_t::atom_var));
00085 f = posLit(ctx.addVar(Var_t::atom_var));
00086 ctx.startAddConstraints(10);
00087 }
00088 Solver& solver() { return *ctx.master(); }
00089 void testAssertTriviallySat() {
00090 LitVec lits;
00091 lits.push_back(body);
00092 lits.push_back(a);
00093 CPPUNIT_ASSERT_EQUAL(true, newCardinalityConstraint(ctx, lits, 0));
00094 CPPUNIT_ASSERT(solver().isTrue(body));
00095 CPPUNIT_ASSERT(ctx.numConstraints() == 0);
00096 }
00097 void testAssertTriviallyUnSat() {
00098 LitVec lits;
00099 lits.push_back(body);
00100 lits.push_back(a);
00101 CPPUNIT_ASSERT_EQUAL(true, newCardinalityConstraint(ctx, lits, 2));
00102 CPPUNIT_ASSERT(solver().isFalse(body));
00103 CPPUNIT_ASSERT(ctx.numConstraints() == 0);
00104 }
00105
00106 void testAssertNotSoTriviallySat() {
00107 LitVec lits = makeLits();
00108 solver().force(lits[1], 0);
00109 solver().force(lits[2], 0);
00110 CPPUNIT_ASSERT_EQUAL(true, newCardinalityConstraint(ctx, lits, 2));
00111 CPPUNIT_ASSERT(solver().isTrue(body));
00112 CPPUNIT_ASSERT(ctx.numConstraints() == 0);
00113 }
00114
00115 void testAssertNotSoTriviallyUnSat() {
00116 LitVec lits = makeLits();
00117 solver().force(~lits[1], 0);
00118 solver().force(~lits[3], 0);
00119 CPPUNIT_ASSERT_EQUAL(true, newCardinalityConstraint(ctx, lits, 3));
00120 CPPUNIT_ASSERT(solver().isTrue(~body));
00121 CPPUNIT_ASSERT(ctx.numConstraints() == 0);
00122 }
00123
00124 void testTrivialBackpropTrue() {
00125 WeightLitVec lits = makeWeightLits();
00126 solver().force(body, 0);
00127 CPPUNIT_ASSERT_EQUAL(true, newWeightConstraint(ctx, body, lits, 7));
00128 CPPUNIT_ASSERT(ctx.numConstraints() == 1);
00129 CPPUNIT_ASSERT(solver().isTrue(a));
00130 CPPUNIT_ASSERT(solver().isTrue(~b));
00131 solver().propagate();
00132 solver().assume(~lits[0].first) && solver().propagate();
00133 CPPUNIT_ASSERT(solver().isTrue(lits[1].first));
00134 }
00135
00136 void testTrivialBackpropFalse() {
00137 LitVec lits = makeLits();
00138 solver().force(~body, 0);
00139 CPPUNIT_ASSERT_EQUAL(true, newCardinalityConstraint(ctx, lits, 1));
00140 CPPUNIT_ASSERT(ctx.numConstraints() == 0);
00141 CPPUNIT_ASSERT(solver().isFalse(lits[1]));
00142 CPPUNIT_ASSERT(solver().isFalse(lits[2]));
00143 CPPUNIT_ASSERT(solver().isFalse(lits[3]));
00144 CPPUNIT_ASSERT(solver().isFalse(lits[4]));
00145 }
00146
00147 void testTrivialBackpropFalseWeight() {
00148 WeightLitVec lits = makeWeightLits();
00149 solver().force(~body, 0);
00150 CPPUNIT_ASSERT_EQUAL(true, newWeightConstraint(ctx, body, lits, 2));
00151 CPPUNIT_ASSERT(ctx.numConstraints() == 1);
00152 CPPUNIT_ASSERT(solver().isFalse(a));
00153 CPPUNIT_ASSERT(solver().isFalse(~b));
00154 }
00155
00156 void testForwardTrue() {
00157 LitVec assume, expected;
00158 assume.push_back(a);
00159 assume.push_back(~c);
00160 expected.push_back(body);
00161 propCard(assume, expected);
00162 }
00163
00164 void testForwardFalse() {
00165 LitVec assume;
00166 assume.push_back(~a);
00167 assume.push_back(c);
00168 assume.push_back(~d);
00169
00170 LitVec expect;
00171 expect.push_back(~body);
00172
00173 propCard(assume, expect);
00174 }
00175
00176 void testBackwardTrue() {
00177 LitVec assume, expect;
00178 assume.push_back(body);
00179 assume.push_back(c);
00180 assume.push_back(~d);
00181 expect.push_back(a);
00182 expect.push_back(~b);
00183 propCard(assume, expect);
00184
00185 }
00186
00187 void testBackwardFalse() {
00188 LitVec assume, expect;
00189 assume.push_back(~body);
00190 assume.push_back(d);
00191 expect.push_back( ~a );
00192 expect.push_back( b );
00193 expect.push_back( c );
00194 propCard(assume, expect);
00195 }
00196
00197 void testForwardTrueConflict() {
00198 LitVec assume;
00199 assume.push_back(a);
00200 assume.push_back(~c);
00201 propConflictTest(assume, ~body);
00202 }
00203
00204 void testForwardFalseConflict() {
00205 LitVec assume;
00206 assume.push_back(~a);
00207 assume.push_back(c);
00208 assume.push_back(~d);
00209 propConflictTest(assume, body);
00210
00211 }
00212
00213 void testBackwardTrueConflict() {
00214 LitVec assume;
00215 assume.push_back(body);
00216 assume.push_back(c);
00217 assume.push_back(~d);
00218 propConflictTest(assume, b);
00219 }
00220
00221 void testBackwardFalseConflict() {
00222 LitVec assume, expect;
00223 assume.push_back(~body);
00224 assume.push_back(d);
00225 propConflictTest(assume, ~b);
00226 }
00227
00228 void testReasonBug() {
00229 LitVec lits = makeLits();
00230 lits.push_back(~e);
00231 CPPUNIT_ASSERT_EQUAL(true, newCardinalityConstraint(ctx, lits, 3));
00232 LitVec assume, reason;
00233 assume.push_back(a);
00234 assume.push_back(~b);
00235 assume.push_back(~d);
00236 assume.push_back(e);
00237 for (uint32 i = 0; i < assume.size(); ++i) {
00238 CPPUNIT_ASSERT_EQUAL(true, solver().assume(assume[i]));
00239 CPPUNIT_ASSERT_EQUAL(true, solver().propagate());
00240 }
00241 CPPUNIT_ASSERT(assume.size() == solver().numAssignedVars());
00242
00243
00244 CPPUNIT_ASSERT_EQUAL(true, solver().assume(body));
00245 CPPUNIT_ASSERT_EQUAL(true, solver().propagate());
00246 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(~c));
00247
00248 solver().reason(~c, reason);
00249 CPPUNIT_ASSERT_EQUAL(LitVec::size_type(3), reason.size());
00250 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), ~d) != reason.end());
00251 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), e) != reason.end());
00252 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), body) != reason.end());
00253 solver().undoUntil(solver().decisionLevel()-1);
00254 reason.clear();
00255
00256
00257 CPPUNIT_ASSERT_EQUAL(true, solver().assume(~body));
00258 CPPUNIT_ASSERT_EQUAL(true, solver().propagate());
00259 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(c));
00260
00261 solver().reason(c, reason);
00262 CPPUNIT_ASSERT_EQUAL(LitVec::size_type(3), reason.size());
00263 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), a) != reason.end());
00264 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), ~b) != reason.end());
00265 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), ~body) != reason.end());
00266 solver().undoUntil(solver().decisionLevel()-1);
00267 reason.clear();
00268
00269
00270 CPPUNIT_ASSERT_EQUAL(true, solver().assume(~c));
00271 CPPUNIT_ASSERT_EQUAL(true, solver().propagate());
00272 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(body));
00273
00274 solver().reason(body, reason);
00275 CPPUNIT_ASSERT_EQUAL(LitVec::size_type(3), reason.size());
00276 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), a) != reason.end());
00277 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), ~b) != reason.end());
00278 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), ~c) != reason.end());
00279 solver().undoUntil(solver().decisionLevel()-1);
00280
00281
00282 CPPUNIT_ASSERT_EQUAL(true, solver().assume(c));
00283 CPPUNIT_ASSERT_EQUAL(true, solver().propagate());
00284 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(~body));
00285
00286 solver().reason(~body, reason);
00287 CPPUNIT_ASSERT_EQUAL(LitVec::size_type(3), reason.size());
00288 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), ~d) != reason.end());
00289 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), e) != reason.end());
00290 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), c) != reason.end());
00291 solver().undoUntil(solver().decisionLevel()-1);
00292 reason.clear();
00293 }
00294
00295 void testWeightReasonAfterBackprop() {
00296 WeightLitVec lits = makeWeightLits();
00297 CPPUNIT_ASSERT_EQUAL(true, newWeightConstraint(ctx, body, lits, 3));
00298 solver().assume(~body) && solver().propagate();
00299 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(~a));
00300 solver().assume(d) && solver().propagate();
00301 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(b));
00302 LitVec r;
00303 solver().reason(~a, r);
00304 CPPUNIT_ASSERT(r.size() == 1 && r[0] == ~body);
00305 solver().reason(b, r);
00306 CPPUNIT_ASSERT(r.size() == 2 && r[0] == ~body && r[1] == d);
00307 solver().undoUntil(solver().decisionLevel()-1);
00308 solver().reason(~a, r);
00309 CPPUNIT_ASSERT(r.size() == 1 && r[0] == ~body);
00310 solver().undoUntil(solver().decisionLevel()-1);
00311 }
00312
00313 void testOrderBug() {
00314 LitVec lits;
00315 lits.push_back(body);
00316 lits.push_back(a);
00317 lits.push_back(b);
00318 CPPUNIT_ASSERT_EQUAL(true, newCardinalityConstraint(ctx, lits, 1));
00319 solver().assume(e) && solver().propagate();
00320
00321 solver().force(~a, 0);
00322 solver().force(body, 0);
00323 CPPUNIT_ASSERT_EQUAL(true, solver().propagate());
00324 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(b));
00325 LitVec reason;
00326 solver().reason(b, reason);
00327 CPPUNIT_ASSERT(LitVec::size_type(2) == reason.size());
00328 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), body) != reason.end());
00329 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), ~a) != reason.end());
00330
00331 }
00332
00333 void testBackwardAfterForward() {
00334 LitVec lits;
00335 lits.push_back(body);
00336 lits.push_back(a);
00337 lits.push_back(b);
00338 CPPUNIT_ASSERT_EQUAL(true, newCardinalityConstraint(ctx, lits, 1));
00339 solver().assume(a);
00340 CPPUNIT_ASSERT_EQUAL(true, solver().propagate());
00341 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(body));
00342 LitVec reason;
00343 solver().reason(body, reason);
00344 CPPUNIT_ASSERT(LitVec::size_type(1) == reason.size());
00345 CPPUNIT_ASSERT(std::find(reason.begin(), reason.end(), a) != reason.end());
00346
00347 solver().assume(~b);
00348 CPPUNIT_ASSERT_EQUAL(true, solver().propagate());
00349 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(body));
00350 }
00351
00352 void testSimplify() {
00353 LitVec lits = makeLits();
00354 CPPUNIT_ASSERT_EQUAL(true, newCardinalityConstraint(ctx, lits, 2));
00355 CPPUNIT_ASSERT_EQUAL(true, solver().simplify());
00356 CPPUNIT_ASSERT_EQUAL(1u, ctx.numConstraints());
00357 solver().force(a, 0);
00358 solver().simplify();
00359 CPPUNIT_ASSERT_EQUAL(1u, ctx.numConstraints());
00360 solver().force(~c, 0);
00361 solver().simplify();
00362 CPPUNIT_ASSERT_EQUAL(0u, ctx.numConstraints());
00363 }
00364
00365 void testSimplifyCardinality() {
00366 LitVec lits = makeLits();
00367 CPPUNIT_ASSERT_EQUAL(true, newCardinalityConstraint(ctx, lits, 2));
00368 ctx.addUnary(~a);
00369 ctx.addUnary(~d);
00370 ctx.addUnary(~b);
00371 solver().simplify();
00372 solver().assume(~c);
00373 solver().propagate();
00374 CPPUNIT_ASSERT(solver().isTrue(body));
00375 LitVec out;
00376 solver().reason(body, out);
00377
00378 CPPUNIT_ASSERT(out.size() == 1 && out[0] == ~c);
00379 }
00380 void testSimplifyWeight() {
00381 WeightLitVec lits = makeWeightLits();
00382 lits[2].second = 2;
00383 lits.push_back(WeightLiteral(e, 1));
00384 lits.push_back(WeightLiteral(f, 1));
00385 CPPUNIT_ASSERT_EQUAL(true, newWeightConstraint(ctx, body, lits, 2));
00386 ctx.addUnary(body);
00387 ctx.addUnary(~a);
00388 ctx.addUnary(~d);
00389 ctx.addUnary(~e);
00390 ctx.addUnary(~f);
00391 solver().simplify();
00392 CPPUNIT_ASSERT(solver().value(b.var()) == value_free);
00393 solver().assume(c);
00394 solver().propagate();
00395 CPPUNIT_ASSERT(solver().isTrue(~b));
00396 LitVec out;
00397 solver().reason(~b, out);
00398 CPPUNIT_ASSERT(out.size() == 1 && out[0] == c);
00399 }
00400
00401 void testAssertWeightTriviallySat() {
00402 WeightLitVec lits;
00403 lits.push_back(WeightLiteral(a, 2));
00404 CPPUNIT_ASSERT_EQUAL(true, newWeightConstraint(ctx, body, lits, 0));
00405 CPPUNIT_ASSERT(solver().isTrue(body));
00406 }
00407 void testAssertWeightTriviallyUnSat() {
00408 WeightLitVec lits;
00409 lits.push_back(WeightLiteral(a, 2));
00410 CPPUNIT_ASSERT_EQUAL(true, newWeightConstraint(ctx, body, lits, 3));
00411 CPPUNIT_ASSERT(solver().isFalse(body));
00412 }
00413
00414 void testAssertWeightNotSoTriviallySat() {
00415 WeightLitVec lits = makeWeightLits();
00416 solver().force(lits[1].first, 0);
00417 CPPUNIT_ASSERT_EQUAL(true, newWeightConstraint(ctx, body,lits, 2));
00418 CPPUNIT_ASSERT(solver().isTrue(body));
00419 }
00420
00421 void testAssertWeightNotSoTriviallyUnSat() {
00422 WeightLitVec lits = makeWeightLits();
00423 solver().force(~lits[0].first, 0);
00424 solver().force(~lits[2].first, 0);
00425 CPPUNIT_ASSERT_EQUAL(true, newWeightConstraint(ctx, body, lits, 4));
00426 CPPUNIT_ASSERT(solver().isTrue(~body));
00427 }
00428
00429 void testWeightForwardTrue() {
00430 LitVec assume, expect;
00431 assume.push_back(a);
00432 expect.push_back(body);
00433 propWeight(assume, expect);
00434
00435 assume.clear();
00436 assume.push_back(~b);
00437 assume.push_back(~c);
00438 propImpl(assume, expect);
00439
00440 assume.clear();
00441 assume.push_back(~b);
00442 assume.push_back(d);
00443 propImpl(assume, expect);
00444 }
00445
00446 void testWeightForwardFalse() {
00447 LitVec assume, expect;
00448 assume.push_back(~a);
00449 assume.push_back(b);
00450 expect.push_back(~body);
00451 propWeight(assume, expect);
00452 }
00453
00454 void testWeightBackwardTrue() {
00455 WeightLitVec lits = makeWeightLits();
00456 CPPUNIT_ASSERT_EQUAL(true, newWeightConstraint(ctx, body, lits, 3));
00457 solver().assume(~a);
00458 solver().force(body, 0);
00459 CPPUNIT_ASSERT_EQUAL(true, solver().propagate());
00460 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(~b));
00461 CPPUNIT_ASSERT_EQUAL(value_free, solver().value(c.var()));
00462 LitVec r;
00463 solver().reason(~b, r);
00464 CPPUNIT_ASSERT(r.size() == 2);
00465 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~a) != r.end());
00466 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), body) != r.end());
00467
00468 solver().assume(~d);
00469 CPPUNIT_ASSERT_EQUAL(true, solver().propagate());
00470 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(~c));
00471
00472 solver().reason(~c, r);
00473 CPPUNIT_ASSERT(r.size() == 3);
00474 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~a) != r.end());
00475 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), body) != r.end());
00476 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~d) != r.end());
00477
00478 solver().undoUntil(solver().decisionLevel()-1);
00479 solver().reason(~b, r);
00480 CPPUNIT_ASSERT(r.size() == 2);
00481 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~a) != r.end());
00482 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), body) != r.end());
00483 }
00484
00485 void testWeightBackwardFalse() {
00486 WeightLitVec lits = makeWeightLits();
00487 CPPUNIT_ASSERT_EQUAL(true, newWeightConstraint(ctx, body, lits, 3));
00488 solver().assume(~body);
00489 CPPUNIT_ASSERT_EQUAL(true, solver().propagate());
00490 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(~a));
00491 LitVec r;
00492 solver().reason(~a, r);
00493 CPPUNIT_ASSERT(r.size() == 1);
00494 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~body) != r.end());
00495
00496 solver().force(~b, 0);
00497 CPPUNIT_ASSERT_EQUAL(true, solver().propagate());
00498 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(c));
00499 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(~d));
00500
00501 LitVec r2;
00502 solver().reason(c, r);
00503 solver().reason(~d, r2);
00504 CPPUNIT_ASSERT(r == r2);
00505 CPPUNIT_ASSERT(r.size() == 2);
00506 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~body) != r.end());
00507 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b) != r.end());
00508 }
00509
00510 void testWeightConflict() {
00511 WeightLitVec lits = makeWeightLits();
00512 CPPUNIT_ASSERT_EQUAL(true, newWeightConstraint(ctx, body, lits, 3));
00513 LitVec assume;
00514 assume.push_back(body);
00515 assume.push_back(~a);
00516 assume.push_back(b);
00517 std::sort(assume.begin(), assume.end());
00518 do {
00519 CPPUNIT_ASSERT_EQUAL(true, solver().assume(assume[0]));
00520 for (uint32 i = 1; i < assume.size(); ++i) {
00521 CPPUNIT_ASSERT_EQUAL(true, solver().force(assume[i],0));
00522 }
00523 CPPUNIT_ASSERT_EQUAL(false, solver().propagate());
00524 solver().undoUntil(0);
00525 } while (std::next_permutation(assume.begin(), assume.end()));
00526 }
00527
00528 void testCloneWeight() {
00529 ctx.setConcurrency(2);
00530 WeightLitVec lits = makeWeightLits();
00531 CPPUNIT_ASSERT_EQUAL(true, newWeightConstraint(ctx, body, lits, 3));
00532 solver().force(~a, 0);
00533 Solver& solver2 = ctx.addSolver();
00534 ctx.endInit(true);
00535
00536 CPPUNIT_ASSERT(solver2.numConstraints() == 1);
00537
00538 CPPUNIT_ASSERT(solver2.numWatches(a) == 0 && solver2.numWatches(~a) == 0);
00539 solver2.assume(body);
00540 solver2.propagate();
00541 solver2.assume(~d);
00542 solver2.propagate();
00543 CPPUNIT_ASSERT(solver2.isTrue(~b));
00544 CPPUNIT_ASSERT(solver2.isTrue(~c));
00545 LitVec out;
00546 solver2.reason(~b, out);
00547 CPPUNIT_ASSERT(std::find(out.begin(), out.end(), body) != out.end());
00548 CPPUNIT_ASSERT(std::find(out.begin(), out.end(), ~a) != out.end());
00549 CPPUNIT_ASSERT(std::find(out.begin(), out.end(), ~d) == out.end());
00550 out.clear();
00551 solver2.reason(~c, out);
00552 CPPUNIT_ASSERT(std::find(out.begin(), out.end(), ~d) != out.end());
00553 }
00554
00555 void testCloneWeightShared() {
00556 ctx.setConcurrency(2);
00557 ctx.setShareMode(ContextParams::share_problem);
00558 WeightLitVec lits = makeWeightLits();
00559 CPPUNIT_ASSERT_EQUAL(true, newWeightConstraint(ctx, body, lits, 3));
00560 solver().force(~a, 0);
00561 Solver& solver2 = ctx.addSolver();
00562 ctx.endInit(true);
00563
00564 CPPUNIT_ASSERT(solver2.numConstraints() == 1);
00565
00566 CPPUNIT_ASSERT(solver2.numWatches(a) == 0 && solver2.numWatches(~a) == 0);
00567 solver2.assume(body);
00568 solver2.propagate();
00569 solver2.assume(~d);
00570 solver2.propagate();
00571 CPPUNIT_ASSERT(solver2.isTrue(~b));
00572 CPPUNIT_ASSERT(solver2.isTrue(~c));
00573 LitVec out;
00574 solver2.reason(~b, out);
00575 CPPUNIT_ASSERT(std::find(out.begin(), out.end(), body) != out.end());
00576 CPPUNIT_ASSERT(std::find(out.begin(), out.end(), ~a) != out.end());
00577 CPPUNIT_ASSERT(std::find(out.begin(), out.end(), ~d) == out.end());
00578 out.clear();
00579 solver2.reason(~c, out);
00580 CPPUNIT_ASSERT(std::find(out.begin(), out.end(), ~d) != out.end());
00581 }
00582
00583 void testAddOnLevel() {
00584 ctx.endInit(true);
00585 WeightLitVec lits = makeWeightLits();
00586 uint32 sz = lits.size() + 1;
00587 Solver& s = *ctx.master();
00588 s.pushRoot(f);
00589 WeightConstraint::CPair res = WeightConstraint::create(s, body, lits, 2, WeightConstraint::create_no_add);
00590 CPPUNIT_ASSERT(res.ok() && res.first() != 0);
00591 CPPUNIT_ASSERT(res.first()->size() == sz && lits.size() == sz-1);
00592 s.force(body);
00593 s.force(~lits[0].first);
00594 s.force(~lits[1].first,0);
00595 s.propagate();
00596 CPPUNIT_ASSERT(s.isTrue(lits[2].first) && s.isTrue(lits[3].first));
00597 res.first()->destroy(&s, true);
00598 }
00599 void testCreateSat() {
00600 ctx.endInit(true);
00601 WeightLitVec lits = makeWeightLits();
00602 uint32 sz = lits.size() + 1;
00603 Solver& s = *ctx.master();
00604
00605 s.force(lits[0].first);
00606 s.force(lits[1].first);
00607 WeightConstraint::CPair res = WeightConstraint::create(s, body, lits, 2, WeightConstraint::create_no_add|WeightConstraint::create_sat);
00608 CPPUNIT_ASSERT(res.ok() && res.first() != 0);
00609 CPPUNIT_ASSERT(s.isTrue(body));
00610 s.propagate();
00611 CPPUNIT_ASSERT(s.isTrue(body));
00612 while (!lits.empty()) {
00613 CPPUNIT_ASSERT(s.force(~lits.back().first) && s.propagate());
00614 lits.pop_back();
00615 }
00616 res.first()->destroy(&s, true);
00617 }
00618 void testCreateSatOnRoot() {
00619 ctx.endInit(true);
00620 Solver& s = *ctx.master();
00621 s.pushRoot(f);
00622 CPPUNIT_ASSERT(s.rootLevel() == 1);
00623 s.force(a, 0);
00624 s.force(b, 0);
00625 s.propagate();
00626 WeightLitVec lits;
00627 lits.push_back(WeightLiteral(a, 1));
00628 lits.push_back(WeightLiteral(b, 1));
00629 lits.push_back(WeightLiteral(c, 1));
00630 lits.push_back(WeightLiteral(d, 1));
00631 WeightLitsRep rep = WeightLitsRep::create(s, lits, 2);
00632 WeightConstraint::CPair res = WeightConstraint::create(s, body, rep, WeightConstraint::create_no_add|WeightConstraint::create_sat);
00633 CPPUNIT_ASSERT(res.ok() && res.first());
00634 CPPUNIT_ASSERT(s.isTrue(body));
00635 CPPUNIT_ASSERT(s.reason(body) == res.first());
00636 s.popRootLevel(1);
00637 CPPUNIT_ASSERT(s.value(body.var()) == value_free);
00638 res.first()->destroy(&s, true);
00639 }
00640 void testCreateSatOnRootNoProp() {
00641 ctx.endInit(true);
00642 Solver& s = *ctx.master();
00643 s.pushRoot(f);
00644 CPPUNIT_ASSERT(s.rootLevel() == 1);
00645 s.force(a, 0);
00646 s.force(b, 0);
00647 WeightLitVec lits;
00648 lits.push_back(WeightLiteral(a, 1));
00649 lits.push_back(WeightLiteral(b, 1));
00650 lits.push_back(WeightLiteral(c, 1));
00651 lits.push_back(WeightLiteral(d, 1));
00652 WeightLitsRep rep = WeightLitsRep::create(s, lits, 2);
00653 WeightConstraint::CPair res = WeightConstraint::create(s, body, rep, WeightConstraint::create_no_add|WeightConstraint::create_sat);
00654 CPPUNIT_ASSERT(res.ok() && res.first());
00655 CPPUNIT_ASSERT(!s.isTrue(body));
00656 CPPUNIT_ASSERT(s.propagate());
00657 CPPUNIT_ASSERT(s.isTrue(body));
00658 CPPUNIT_ASSERT(s.reason(body) == res.first());
00659 s.popRootLevel(1);
00660 CPPUNIT_ASSERT(s.value(body.var()) == value_free);
00661 res.first()->destroy(&s, true);
00662 }
00663 void testMergeNegativeWeight() {
00664 WeightLitVec lits;
00665 lits.push_back(WeightLiteral(a, -1));
00666 lits.push_back(WeightLiteral(a, -1));
00667 lits.push_back(WeightLiteral(b, -2));
00668 WeightLitsRep rep = WeightLitsRep::create(*ctx.master(), lits, -2);
00669 CPPUNIT_ASSERT(rep.size == 2);
00670 CPPUNIT_ASSERT(rep.bound == 1);
00671 CPPUNIT_ASSERT(rep.reach == 2);
00672 CPPUNIT_ASSERT(rep.lits[0].second == 1);
00673 CPPUNIT_ASSERT(rep.lits[1].second == 1);
00674 }
00675 private:
00676 static bool newCardinalityConstraint(SharedContext& ctx, const LitVec& lits, int bound) {
00677 CPPUNIT_ASSERT(lits.size() > 1);
00678 WeightLitVec wlits;
00679 for (LitVec::size_type i = 1; i < lits.size(); ++i) {
00680 wlits.push_back(WeightLiteral(lits[i], 1));
00681 }
00682 return newWeightConstraint(ctx, lits[0], wlits, bound);
00683 }
00684 static bool newWeightConstraint(SharedContext& ctx, Literal W, WeightLitVec& lits, weight_t bound) {
00685 return WeightConstraint::create(*ctx.master(), W, lits, bound).ok();
00686 }
00687 void propCard(LitVec& assumptions, const LitVec& expected) {
00688 LitVec lits = makeLits();
00689 CPPUNIT_ASSERT_EQUAL(true, newCardinalityConstraint(ctx, lits, 2));
00690 propImpl(assumptions, expected);
00691 }
00692 void propWeight(LitVec& assume, LitVec& expect) {
00693 WeightLitVec lits = makeWeightLits();
00694 CPPUNIT_ASSERT_EQUAL(true, newWeightConstraint(ctx, body, lits, 3));
00695 propImpl(assume, expect);
00696 }
00697 void propImpl(LitVec& assumptions, const LitVec& expected) {
00698 std::sort(assumptions.begin(), assumptions.end());
00699 do {
00700 for (uint32 i = 0; i < assumptions.size(); ++i) {
00701 CPPUNIT_ASSERT_EQUAL(true, solver().assume(assumptions[i]));
00702 CPPUNIT_ASSERT_EQUAL(true, solver().propagate());
00703 }
00704 for (uint32 i = 0; i < expected.size(); ++i) {
00705 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(expected[i]));
00706 LitVec reason;
00707 solver().reason(expected[i], reason);
00708 CPPUNIT_ASSERT_EQUAL(assumptions.size(), reason.size());
00709 for (uint32 j = 0; j < assumptions.size(); ++j) {
00710 CPPUNIT_ASSERT(find(reason.begin(), reason.end(), assumptions[j]) != reason.end());
00711 }
00712
00713 }
00714 solver().undoUntil(0);
00715 } while (std::next_permutation(assumptions.begin(), assumptions.end()));
00716 }
00717 void propConflictTest(LitVec& assumptions, Literal cflLit) {
00718 LitVec lits = makeLits();
00719 CPPUNIT_ASSERT_EQUAL(true, newCardinalityConstraint(ctx, lits, 2));
00720 do {
00721 for (uint32 i = 0; i < assumptions.size()-1; ++i) {
00722 CPPUNIT_ASSERT_EQUAL(true, solver().assume(assumptions[i]));
00723 CPPUNIT_ASSERT_EQUAL(true, solver().propagate());
00724 }
00725 CPPUNIT_ASSERT_EQUAL(true, solver().assume(assumptions.back()));
00726 CPPUNIT_ASSERT_EQUAL(true, solver().force(cflLit, 0));
00727 CPPUNIT_ASSERT_EQUAL(false, solver().propagate());
00728 LitVec cfl = solver().conflict();
00729 CPPUNIT_ASSERT_EQUAL(assumptions.size() + 1, cfl.size());
00730 for (uint32 i = 0; i < assumptions.size(); ++i) {
00731 CPPUNIT_ASSERT(std::find(cfl.begin(), cfl.end(), assumptions[i]) != cfl.end());
00732 }
00733 CPPUNIT_ASSERT(std::find(cfl.begin(), cfl.end(), cflLit) != cfl.end());
00734 solver().undoUntil(0);
00735 }while (std::next_permutation(assumptions.begin(), assumptions.end()));
00736 }
00737
00738 LitVec makeLits() {
00739 LitVec res;
00740 res.push_back(body);
00741 res.push_back(a);
00742 res.push_back(~b);
00743 res.push_back(~c);
00744 res.push_back(d);
00745 return res;
00746 }
00747 WeightLitVec makeWeightLits() {
00748 WeightLitVec res;
00749 res.push_back(WeightLiteral(a, 4));
00750 res.push_back(WeightLiteral(~b, 2));
00751 res.push_back(WeightLiteral(~c, 1));
00752 res.push_back(WeightLiteral(d, 1));
00753 return res;
00754 }
00755 SharedContext ctx;
00756 Literal body;
00757 Literal a, b, c, d, e, f;
00758 };
00759 CPPUNIT_TEST_SUITE_REGISTRATION(WeightConstraintTest);
00760 } }