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 <algorithm>
00022 #include <clasp/clause.h>
00023 #include <clasp/solver.h>
00024
00025 #ifdef _MSC_VER
00026 #pragma warning (disable : 4267) // conversion from 'size_t' to unsigned int
00027 #pragma once
00028 #endif
00029
00030
00031 namespace Clasp { namespace Test {
00032
00033 class ClauseTest : public CppUnit::TestFixture {
00034 CPPUNIT_TEST_SUITE(ClauseTest);
00035 CPPUNIT_TEST(testClauseCtorAddsWatches);
00036 CPPUNIT_TEST(testClauseTypes);
00037 CPPUNIT_TEST(testClauseActivity);
00038
00039 CPPUNIT_TEST(testPropGenericClause);
00040 CPPUNIT_TEST(testPropGenericClauseConflict);
00041 CPPUNIT_TEST(testPropAlreadySatisfied);
00042 CPPUNIT_TEST(testPropRandomClauses);
00043
00044 CPPUNIT_TEST(testReasonBumpsActivityIfLearnt);
00045
00046 CPPUNIT_TEST(testSimplifySAT);
00047
00048 CPPUNIT_TEST(testSimplifyUnitButNotLocked);
00049 CPPUNIT_TEST(testSimplifyRemovesFalseLitsBeg);
00050 CPPUNIT_TEST(testSimplifyRemovesFalseLitsMid);
00051 CPPUNIT_TEST(testSimplifyRemovesFalseLitsEnd);
00052 CPPUNIT_TEST(testSimplifyShortRemovesFalseLitsBeg);
00053 CPPUNIT_TEST(testSimplifyShortRemovesFalseLitsMid);
00054 CPPUNIT_TEST(testSimplifyShortRemovesFalseLitsEnd);
00055
00056 CPPUNIT_TEST(testStrengthen);
00057 CPPUNIT_TEST(testStrengthenToUnary);
00058 CPPUNIT_TEST(testStrengthenContracted);
00059 CPPUNIT_TEST(testStrengthenBug);
00060 CPPUNIT_TEST(testStrengthenContractedNoExtend);
00061 CPPUNIT_TEST(testStrengthenLocked);
00062 CPPUNIT_TEST(testStrengthenLockedEarly);
00063 CPPUNIT_TEST(testSimplifyTagged);
00064
00065 CPPUNIT_TEST(testClauseSatisfied);
00066 CPPUNIT_TEST(testContraction);
00067 CPPUNIT_TEST(testNewContractedClause);
00068
00069 CPPUNIT_TEST(testClone);
00070
00071 CPPUNIT_TEST(testBug);
00072
00073 CPPUNIT_TEST(testLoopFormulaInitialWatches);
00074 CPPUNIT_TEST(testSimplifyLFIfOneBodyTrue);
00075 CPPUNIT_TEST(testSimplifyLFIfAllAtomsFalse);
00076 CPPUNIT_TEST(testSimplifyLFRemovesFalseBodies);
00077 CPPUNIT_TEST(testSimplifyLFRemovesFalseAtoms);
00078 CPPUNIT_TEST(testSimplifyLFRemovesTrueAtoms);
00079
00080 CPPUNIT_TEST(testLoopFormulaPropagateBody);
00081 CPPUNIT_TEST(testLoopFormulaPropagateBody2);
00082 CPPUNIT_TEST(testLoopFormulaPropagateAtoms);
00083 CPPUNIT_TEST(testLoopFormulaPropagateAtoms2);
00084 CPPUNIT_TEST(testLoopFormulaBodyConflict);
00085 CPPUNIT_TEST(testLoopFormulaAtomConflict);
00086 CPPUNIT_TEST(testLoopFormulaDontChangeSat);
00087 CPPUNIT_TEST(testLoopFormulaPropTrueAtomInSatClause);
00088
00089 CPPUNIT_TEST(testLoopFormulaSatisfied);
00090
00091 CPPUNIT_TEST(testLoopFormulaBugEq);
00092
00093 CPPUNIT_TEST_SUITE_END();
00094 public:
00095 ClauseTest() {
00096 a1 = posLit(ctx.addVar(Var_t::atom_var));
00097 a2 = posLit(ctx.addVar(Var_t::atom_var));
00098 a3 = posLit(ctx.addVar(Var_t::atom_var));
00099 b1 = posLit(ctx.addVar(Var_t::body_var));
00100 b2 = posLit(ctx.addVar(Var_t::body_var));
00101 b3 = posLit(ctx.addVar(Var_t::body_var));
00102
00103 for (int i = 6; i < 15; ++i) {
00104 ctx.addVar(Var_t::atom_var);
00105 }
00106 ctx.startAddConstraints(10);
00107 solver = ctx.master();
00108 }
00109 void testClauseCtorAddsWatches() {
00110 ClauseHead* cl1;
00111 solver->add(cl1 = createClause(2,2));
00112 CPPUNIT_ASSERT_EQUAL(2, countWatches(*solver, cl1, clLits) );
00113 ClauseHead* cl2 = createClause(clLits, Constraint_t::learnt_conflict);
00114 solver->add(cl2);
00115 CPPUNIT_ASSERT_EQUAL(2, countWatches(*solver, cl2, clLits));
00116 }
00117
00118 void testClauseTypes() {
00119 Clause* cl1 = createClause(2, 2);
00120 LearntConstraint* cl2 = createClause(clLits, ClauseInfo(Constraint_t::learnt_conflict));
00121 LearntConstraint* cl3 = createClause(clLits, ClauseInfo(Constraint_t::learnt_loop));
00122 CPPUNIT_ASSERT_EQUAL(Constraint_t::static_constraint, cl1->type());
00123 CPPUNIT_ASSERT_EQUAL(Constraint_t::learnt_conflict, cl2->type());
00124 CPPUNIT_ASSERT_EQUAL(Constraint_t::learnt_loop, cl3->type());
00125 cl1->destroy();
00126 cl2->destroy();
00127 cl3->destroy();
00128 }
00129
00130 void testClauseActivity() {
00131 LitVec lit;
00132 lit.push_back(posLit(1));
00133 lit.push_back(posLit(2));
00134 lit.push_back(posLit(3));
00135 lit.push_back(posLit(4));
00136 uint32 exp = 258;
00137 ClauseHead* cl1 = createClause(lit, ClauseInfo(Constraint_t::learnt_conflict).setActivity(exp));
00138 ClauseHead* cl2 = createClause(lit, ClauseInfo(Constraint_t::learnt_loop).setActivity(exp));
00139 solver->add(cl1);
00140 solver->add(cl2);
00141 while ( exp != 0 ) {
00142 CPPUNIT_ASSERT(cl1->activity().activity() == cl2->activity().activity() && cl1->activity().activity() == exp);
00143 exp >>= 1;
00144 cl1->decreaseActivity();
00145 cl2->decreaseActivity();
00146 }
00147 CPPUNIT_ASSERT(cl1->activity().activity() == cl2->activity().activity() && cl1->activity().activity() == exp);
00148 }
00149
00150 void testPropGenericClause() {
00151 Clause* c;
00152 solver->add(c = createClause(2, 2));
00153 solver->assume(~clLits[0]);
00154 solver->propagate();
00155 solver->assume( ~clLits.back() );
00156 solver->propagate();
00157
00158 solver->assume(~clLits[1]);
00159 solver->propagate();
00160
00161 CPPUNIT_ASSERT_EQUAL(true, solver->isTrue( clLits[2] ) );
00162 CPPUNIT_ASSERT_EQUAL(true, c->locked(*solver));
00163 Antecedent reason = solver->reason(clLits[2]);
00164 CPPUNIT_ASSERT(reason == c);
00165
00166 LitVec r;
00167 reason.reason(*solver, clLits[2], r);
00168 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~clLits[0]) != r.end());
00169 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~clLits[1]) != r.end());
00170 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~clLits[3]) != r.end());
00171 }
00172
00173 void testPropGenericClauseConflict() {
00174 Clause* c;
00175 solver->add(c = createClause(2, 2));
00176 solver->assume( ~clLits[0] );
00177 solver->force( ~clLits[1], 0 );
00178 solver->force( ~clLits[2], 0 );
00179 solver->force( ~clLits[3], 0 );
00180
00181 CPPUNIT_ASSERT_EQUAL(false, solver->propagate());
00182 const LitVec& r = solver->conflict();
00183 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~clLits[0]) != r.end());
00184 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~clLits[1]) != r.end());
00185 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~clLits[2]) != r.end());
00186 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~clLits[3]) != r.end());
00187 }
00188
00189 void testPropAlreadySatisfied() {
00190 Clause* c;
00191 solver->add(c = createClause(2, 2));
00192
00193
00194 solver->force(clLits[2], 0);
00195 solver->propagate();
00196
00197
00198 solver->force(~clLits[0], 0);
00199 solver->force(~clLits[1], 0);
00200 solver->propagate();
00201
00202
00203 CPPUNIT_ASSERT(value_free == solver->value(clLits[3].var()));
00204 }
00205 void testPropRandomClauses() {
00206 for (int i = 0; i != 100; ++i) {
00207 SharedContext cc;
00208 solver = cc.master();
00209 solver->strategy.initWatches = SolverStrategies::watch_rand;
00210 for (int j = 0; j < 12; ++j) { cc.addVar(Var_t::atom_var); }
00211 cc.startAddConstraints(1);
00212 Clause* c;
00213 solver->add( c = createRandomClause( (rand() % 10) + 2 ) );
00214 check(*c);
00215 }
00216 }
00217
00218 void testReasonBumpsActivityIfLearnt() {
00219 clLits.push_back(posLit(1));
00220 clLits.push_back(posLit(2));
00221 clLits.push_back(posLit(3));
00222 clLits.push_back(posLit(4));
00223 ctx.endInit();
00224 ClauseHead* cl1 = createClause(clLits, ClauseInfo(Constraint_t::learnt_conflict));
00225 solver->addLearnt(cl1, (uint32)clLits.size());
00226 solver->assume(~clLits[0]);
00227 solver->propagate();
00228 solver->assume(~clLits[1]);
00229 solver->propagate();
00230 solver->assume(~clLits[2]);
00231 solver->propagate();
00232
00233 CPPUNIT_ASSERT_EQUAL(true, solver->isTrue( clLits[3] ) );
00234 uint32 a = cl1->activity().activity();
00235 LitVec r;
00236 solver->reason(clLits[3], r);
00237 CPPUNIT_ASSERT_EQUAL(a+1, cl1->activity().activity());
00238 }
00239
00240 void testSimplifySAT() {
00241 Clause* c;
00242 solver->add(c = createClause(3, 2));
00243 solver->force( ~clLits[1], 0);
00244 solver->force( clLits[2], 0 );
00245 solver->propagate();
00246
00247 CPPUNIT_ASSERT_EQUAL(true, c->simplify(*solver, false));
00248 }
00249 void testSimplifyUnitButNotLocked() {
00250 Clause* c;
00251 solver->add(c = createClause(2, 2));
00252 solver->force( clLits[0], 0);
00253 solver->force( ~clLits[1], 0 );
00254 solver->force( ~clLits[2], 0 );
00255 solver->force( ~clLits[3], 0 );
00256 solver->propagate();
00257 CPPUNIT_ASSERT_EQUAL(true, c->simplify(*solver, false));
00258 }
00259
00260 void testSimplifyRemovesFalseLitsBeg() {
00261 Clause* c;
00262
00263 solver->add(c = createClause(3, 3));
00264 CPPUNIT_ASSERT(6 == c->size());
00265
00266 solver->force(~clLits[0], 0);
00267 solver->force(~clLits[1], 0);
00268 solver->propagate();
00269
00270 CPPUNIT_ASSERT_EQUAL(false, c->simplify(*solver));
00271 CPPUNIT_ASSERT(4 == c->size());
00272
00273 CPPUNIT_ASSERT_EQUAL(2, countWatches(*solver, c, clLits));
00274 }
00275
00276 void testSimplifyRemovesFalseLitsMid() {
00277 Clause* c;
00278
00279 solver->add(c = createClause(3, 3));
00280 CPPUNIT_ASSERT(6 == c->size());
00281
00282 solver->force(~clLits[1], 0);
00283 solver->force(~clLits[2], 0);
00284 solver->propagate();
00285
00286 CPPUNIT_ASSERT_EQUAL(false, c->simplify(*solver));
00287 CPPUNIT_ASSERT(4 == c->size());
00288
00289 CPPUNIT_ASSERT_EQUAL(2, countWatches(*solver, c, clLits));
00290 }
00291
00292 void testSimplifyShortRemovesFalseLitsBeg() {
00293 ClauseHead* c = createClause(2, 3);
00294 solver->add(c);
00295
00296 solver->force(~clLits[0], 0);
00297 solver->propagate();
00298
00299 CPPUNIT_ASSERT_EQUAL(false, c->simplify(*solver));
00300 CPPUNIT_ASSERT(4 == c->size());
00301
00302 CPPUNIT_ASSERT_EQUAL(2, countWatches(*solver, c, clLits));
00303 }
00304
00305 void testSimplifyShortRemovesFalseLitsMid() {
00306 ClauseHead* c = createClause(2, 3);
00307 solver->add(c);
00308
00309 solver->force(~clLits[2], 0);
00310 solver->propagate();
00311
00312 CPPUNIT_ASSERT_EQUAL(false, c->simplify(*solver));
00313 CPPUNIT_ASSERT(4 == c->size());
00314
00315 CPPUNIT_ASSERT_EQUAL(2, countWatches(*solver, c, clLits));
00316 }
00317
00318 void testSimplifyShortRemovesFalseLitsEnd() {
00319 ClauseHead* c = createClause(2, 3);
00320 solver->add(c);
00321
00322 solver->force(~clLits[4], 0);
00323 solver->propagate();
00324
00325 CPPUNIT_ASSERT_EQUAL(false, c->simplify(*solver));
00326 CPPUNIT_ASSERT(4 == c->size());
00327
00328 CPPUNIT_ASSERT_EQUAL(2, countWatches(*solver, c, clLits));
00329 }
00330
00331 void testStrengthen() {
00332 ClauseHead* c;
00333 clLits.push_back(a1);
00334 clLits.push_back(a2);
00335 clLits.push_back(a3);
00336 clLits.push_back(b1);
00337 clLits.push_back(b2);
00338 clLits.push_back(b3);
00339 c = createClause(clLits, ClauseInfo());
00340 CPPUNIT_ASSERT_EQUAL(false, c->strengthen(*solver, b2).second);
00341 CPPUNIT_ASSERT(c->size() == 5);
00342 CPPUNIT_ASSERT_EQUAL(false, c->strengthen(*solver, a3).second);
00343 CPPUNIT_ASSERT(c->size() == 4);
00344
00345 CPPUNIT_ASSERT_EQUAL(true, c->strengthen(*solver, a1).second);
00346 CPPUNIT_ASSERT(c->size() == 3);
00347 c->destroy(solver, true);
00348 }
00349
00350 void testStrengthenToUnary() {
00351 Literal b = posLit(ctx.addVar( Var_t::atom_var ));
00352 Literal x = posLit(ctx.addVar( Var_t::atom_var ));
00353 Literal y = posLit(ctx.addVar( Var_t::atom_var ));
00354 ctx.startAddConstraints();
00355 ctx.endInit();
00356 Literal a = posLit(solver->pushTagVar(true));
00357 solver->assume(x) && solver->propagate();
00358 solver->assume(y) && solver->propagate();
00359 solver->setBacktrackLevel(solver->decisionLevel());
00360 clLits.clear();
00361 clLits.push_back(b);
00362 clLits.push_back(~a);
00363 ClauseInfo extra(Constraint_t::learnt_conflict); extra.setTagged(true);
00364 ClauseHead* c = ClauseCreator::create(*solver, clLits, 0, extra).local;
00365 CPPUNIT_ASSERT(c->size() == 2);
00366 CPPUNIT_ASSERT(solver->isTrue(b) && solver->reason(b).constraint() == c);
00367 solver->backtrack() && solver->propagate();
00368 CPPUNIT_ASSERT(solver->isTrue(b) && solver->reason(b).constraint() == c);
00369 c->strengthen(*solver, ~a);
00370 solver->backtrack();
00371 CPPUNIT_ASSERT(solver->isTrue(b));
00372 LitVec out;
00373 solver->reason(b, out);
00374 CPPUNIT_ASSERT(out.size() == 1 && out[0] == posLit(0));
00375 solver->clearAssumptions();
00376 CPPUNIT_ASSERT(solver->isTrue(b));
00377 }
00378
00379 void testStrengthenContracted() {
00380 solver->strategy.compress = 4;
00381 ctx.endInit();
00382 LitVec lits;
00383 lits.push_back(a1);
00384 for (uint32 i = 2; i <= 12; ++i) {
00385 solver->assume(negLit(i));
00386 lits.push_back(posLit(i));
00387 }
00388 ClauseHead* c = ClauseCreator::create(*solver, lits, 0, Constraint_t::learnt_conflict).local;
00389 uint32 si = c->size();
00390 c->strengthen(*solver, posLit(12));
00391 solver->undoUntil(solver->decisionLevel()-1);
00392 CPPUNIT_ASSERT(solver->value(posLit(12).var()) == value_free && si == c->size());
00393 solver->undoUntil(solver->level(posLit(9).var())-1);
00394
00395 CPPUNIT_ASSERT(si+1 <= c->size());
00396 si = c->size();
00397
00398 c->strengthen(*solver, posLit(2));
00399 c->strengthen(*solver, posLit(6));
00400 CPPUNIT_ASSERT(si == c->size());
00401 c->strengthen(*solver, posLit(9));
00402
00403 c->strengthen(*solver, posLit(8));
00404 c->strengthen(*solver, posLit(5));
00405 c->strengthen(*solver, posLit(4));
00406 c->strengthen(*solver, posLit(3));
00407
00408 CPPUNIT_ASSERT_EQUAL(false, c->strengthen(*solver, posLit(7), false).second);
00409 CPPUNIT_ASSERT_EQUAL(uint32(3), c->size());
00410 CPPUNIT_ASSERT_EQUAL(true, c->strengthen(*solver, posLit(11)).second);
00411 CPPUNIT_ASSERT_EQUAL(uint32(sizeof(Clause) + (9*sizeof(Literal))), ((Clause*)c)->computeAllocSize());
00412 }
00413
00414 void testStrengthenBug() {
00415 solver->strategy.compress = 6;
00416 ctx.endInit();
00417 LitVec clause;
00418 clause.push_back(a1);
00419 for (uint32 i = 2; i <= 6; ++i) {
00420 solver->assume(negLit(8-i)) && solver->propagate();
00421 clause.push_back(posLit(i));
00422 }
00423 ClauseHead* c = Clause::newContractedClause(*solver, ClauseRep::create(&clause[0], (uint32)clause.size(), ClauseInfo(Constraint_t::learnt_conflict)) , 5, true);
00424 solver->addLearnt(c, 5);
00425 uint32 si = c->size();
00426 CPPUNIT_ASSERT(si == 5);
00427 c->strengthen(*solver, posLit(4));
00428 LitVec clause2;
00429 c->toLits(clause2);
00430 CPPUNIT_ASSERT(clause2.size() == 5);
00431 for (uint32 i = 0; i != clause.size(); ++i) {
00432 CPPUNIT_ASSERT(std::find(clause2.begin(), clause2.end(), clause[i]) != clause2.end() || clause[i] == posLit(4));
00433 }
00434 }
00435
00436 void testStrengthenContractedNoExtend() {
00437 solver->strategy.compress = 4;
00438 ctx.endInit();
00439 LitVec clause;
00440 clause.push_back(a1);
00441 for (uint32 i = 2; i <= 6; ++i) {
00442 solver->assume(negLit(8-i)) && solver->propagate();
00443 clause.push_back(posLit(i));
00444 }
00445 ClauseRep x = ClauseRep::create(&clause[0], (uint32)clause.size(), ClauseInfo(Constraint_t::learnt_conflict));
00446 ClauseHead* c = Clause::newContractedClause(*solver, x, 4, false);
00447 solver->addLearnt(c, 4);
00448 CPPUNIT_ASSERT(c->size() == 4);
00449 c->strengthen(*solver, posLit(2));
00450 CPPUNIT_ASSERT(c->size() == 4);
00451 solver->undoUntil(0);
00452 CPPUNIT_ASSERT(c->size() == 4);
00453 }
00454
00455 void testStrengthenLocked() {
00456 Var a = ctx.addVar( Var_t::atom_var );
00457 Var b = ctx.addVar( Var_t::atom_var );
00458 Var c = ctx.addVar( Var_t::atom_var );
00459 ctx.startAddConstraints();
00460 ctx.endInit();
00461 Literal tag = posLit(solver->pushTagVar(true));
00462 solver->assume(posLit(a)) && solver->propagate();
00463 solver->assume(posLit(b)) && solver->propagate();
00464 ClauseCreator cc(solver);
00465 cc.start(Constraint_t::learnt_conflict).add(negLit(a)).add(negLit(b)).add(negLit(c)).add(~tag);
00466 ClauseHead* clause = cc.end().local;
00467 CPPUNIT_ASSERT(clause->locked(*solver));
00468 CPPUNIT_ASSERT(!clause->strengthen(*solver, ~tag).second);
00469 CPPUNIT_ASSERT(clause->locked(*solver));
00470 LitVec r;
00471 solver->reason(negLit(c), r);
00472 CPPUNIT_ASSERT(r.size() == 2);
00473 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), posLit(a)) != r.end());
00474 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), posLit(b)) != r.end());
00475 }
00476
00477 void testStrengthenLockedEarly() {
00478 Literal b = posLit(ctx.addVar( Var_t::atom_var ));
00479 Literal c = posLit(ctx.addVar( Var_t::atom_var ));
00480 Literal d = posLit(ctx.addVar( Var_t::atom_var ));
00481 Literal x = posLit(ctx.addVar( Var_t::atom_var ));
00482 ctx.startAddConstraints();
00483 ctx.endInit();
00484 Literal a = posLit(solver->pushTagVar(true));
00485 solver->assume(b) && solver->propagate();
00486 solver->force(c, 0) && solver->propagate();
00487 solver->assume(x) && solver->propagate();
00488 solver->setBacktrackLevel(solver->decisionLevel());
00489
00490 ClauseCreator cc(solver);
00491 cc.start(Constraint_t::learnt_conflict).add(~a).add(~b).add(~c).add(d);
00492 ClauseHead* clause = cc.end().local;
00493 CPPUNIT_ASSERT(clause->locked(*solver));
00494 bool remove = clause->strengthen(*solver, ~a).second;
00495 solver->backtrack();
00496 CPPUNIT_ASSERT(solver->isTrue(d));
00497 CPPUNIT_ASSERT(!remove || solver->reason(d).type() != Antecedent::generic_constraint || solver->reason(d).constraint() != clause);
00498 }
00499
00500 void testSimplifyTagged() {
00501 Var a = ctx.addVar( Var_t::atom_var );
00502 Var b = ctx.addVar( Var_t::atom_var );
00503 Var c = ctx.addVar( Var_t::atom_var );
00504 ctx.startAddConstraints();
00505 ctx.endInit();
00506 Literal tag = posLit(solver->pushTagVar(true));
00507 ClauseCreator cc(solver);
00508
00509 cc.start(Constraint_t::learnt_conflict).add(negLit(a)).add(negLit(b)).add(negLit(c)).add(~tag);
00510 ClauseHead* clause = cc.end().local;
00511
00512 solver->force(posLit(c));
00513 CPPUNIT_ASSERT_EQUAL(false, clause->strengthen(*solver, negLit(c)).second);
00514 }
00515
00516 void testSimplifyRemovesFalseLitsEnd() {
00517 Clause* c;
00518 solver->add(c = createClause(3, 3));
00519 CPPUNIT_ASSERT(6 == c->size());
00520
00521 solver->force(~clLits[4], 0);
00522 solver->force(~clLits[5], 0);
00523 solver->propagate();
00524
00525 CPPUNIT_ASSERT_EQUAL(false, c->simplify(*solver));
00526 CPPUNIT_ASSERT(4 == c->size());
00527
00528 CPPUNIT_ASSERT_EQUAL(2, countWatches(*solver, c, clLits));
00529 }
00530
00531 void testClauseSatisfied() {
00532 ConstraintType t = Constraint_t::learnt_conflict;
00533 TypeSet ts; ts.addSet(t);
00534 Clause* c;
00535 solver->addLearnt(c = createClause(2, 2, t), 4);
00536 LitVec free;
00537 CPPUNIT_ASSERT_EQUAL(uint32(t), c->isOpen(*solver, ts, free));
00538 CPPUNIT_ASSERT_EQUAL(LitVec::size_type(4), free.size());
00539
00540 solver->assume( clLits[2] );
00541 solver->propagate();
00542 free.clear();
00543 CPPUNIT_ASSERT_EQUAL(uint32(0), c->isOpen(*solver, ts, free));
00544 solver->undoUntil(0);
00545 solver->assume( ~clLits[1] );
00546 solver->assume( ~clLits[2] );
00547 solver->propagate();
00548 free.clear();
00549 CPPUNIT_ASSERT_EQUAL(uint32(t), c->isOpen(*solver, ts, free));
00550 CPPUNIT_ASSERT_EQUAL(LitVec::size_type(2), free.size());
00551 ts.m = 0; ts.addSet(Constraint_t::learnt_loop);
00552 CPPUNIT_ASSERT_EQUAL(uint32(0), c->isOpen(*solver, ts, free));
00553 }
00554
00555 void testContraction() {
00556 solver->strategy.compress = 6;
00557 ctx.endInit();
00558 LitVec lits(1, a1);
00559 for (uint32 i = 2; i <= 12; ++i) {
00560 solver->assume(negLit(i));
00561 lits.push_back(posLit(i));
00562 }
00563 ClauseHead* cl = ClauseCreator::create(*solver, lits, 0, Constraint_t::learnt_conflict).local;
00564 uint32 s1 = cl->size();
00565 CPPUNIT_ASSERT(s1 < lits.size());
00566 LitVec r;
00567 solver->reason(a1, r);
00568 CPPUNIT_ASSERT( r.size() == lits.size()-1 );
00569
00570 solver->undoUntil(0);
00571 CPPUNIT_ASSERT(cl->size() == lits.size());
00572 }
00573
00574 void testNewContractedClause() {
00575 ctx.endInit();
00576
00577 clLits.push_back(a1);
00578 clLits.push_back(a2);
00579 clLits.push_back(a3);
00580 for (uint32 i = 4; i <= 12; ++i) {
00581 solver->assume(negLit(i));
00582
00583 clLits.push_back(posLit(i));
00584 }
00585 ClauseRep x = ClauseRep::create(&clLits[0], (uint32)clLits.size(), ClauseInfo(Constraint_t::learnt_conflict));
00586 ClauseHead* c = Clause::newContractedClause(*solver, x, 3, false);
00587 solver->addLearnt(c, static_cast<uint32>(clLits.size()));
00588 CPPUNIT_ASSERT(c->size() < clLits.size());
00589
00590 solver->assume(~a1) && solver->propagate();
00591 solver->assume(~a3) && solver->propagate();
00592 CPPUNIT_ASSERT(solver->isTrue(a2));
00593 LitVec r;
00594 solver->reason(a2, r);
00595 CPPUNIT_ASSERT(r.size() == clLits.size()-1);
00596 }
00597 void testBug() {
00598 Clause* c;
00599 solver->add(c = createClause(3, 3));
00600 solver->assume(~clLits[1]);
00601 solver->propagate();
00602 solver->assume(~clLits[2]);
00603 solver->propagate();
00604 solver->assume(~clLits[3]);
00605 solver->propagate();
00606 solver->assume(~clLits[0]);
00607 solver->propagate();
00608 uint32 exp = solver->numAssignedVars();
00609 solver->undoUntil(0);
00610 solver->assume(~clLits[1]);
00611 solver->propagate();
00612 solver->assume(~clLits[2]);
00613 solver->propagate();
00614 solver->assume(~clLits[3]);
00615 solver->propagate();
00616 solver->assume(~clLits[4]);
00617 solver->propagate();
00618
00619 CPPUNIT_ASSERT(exp == solver->numAssignedVars());
00620 CPPUNIT_ASSERT_EQUAL(true, solver->hasWatch(~clLits[0], c));
00621 CPPUNIT_ASSERT_EQUAL(true, solver->hasWatch(~clLits[5], c));
00622 }
00623
00624 void testClone() {
00625 ctx.setConcurrency(2);
00626 Solver& solver2 = ctx.addSolver();
00627 ctx.endInit(true);
00628 ClauseHead* c = createClause(3, 3);
00629 ClauseHead* clone = (ClauseHead*)c->cloneAttach(solver2);
00630 LitVec lits;
00631 clone->toLits(lits);
00632 CPPUNIT_ASSERT(lits == clLits);
00633 CPPUNIT_ASSERT(countWatches(solver2, clone, lits) == 2);
00634 clone->destroy(&solver2, true);
00635
00636 solver->force(~clLits[0], 0);
00637 solver->force(~clLits[2], 0);
00638 solver->propagate();
00639 c->simplify(*solver);
00640 clone = (ClauseHead*)c->cloneAttach(solver2);
00641 lits.clear();
00642 clone->toLits(lits);
00643 CPPUNIT_ASSERT(lits.size() == 4);
00644 CPPUNIT_ASSERT(countWatches(solver2, clone, lits) == 2);
00645 clone->destroy(&solver2, true);
00646 c->destroy(solver, true);
00647
00648 }
00649
00650 void testLoopFormulaInitialWatches() {
00651 LoopFormula* lf = lfTestInit();
00652 CPPUNIT_ASSERT_EQUAL(true, solver->hasWatch(a1, lf));
00653 CPPUNIT_ASSERT_EQUAL(true, solver->hasWatch(a2, lf));
00654 CPPUNIT_ASSERT_EQUAL(true, solver->hasWatch(a3, lf));
00655 CPPUNIT_ASSERT_EQUAL(true, solver->hasWatch(~b3, lf));
00656 }
00657
00658 void testSimplifyLFIfOneBodyTrue() {
00659 LoopFormula* lf = lfTestInit();
00660 solver->undoUntil(0);
00661 solver->force( b2, 0 );
00662 solver->propagate();
00663
00664 CPPUNIT_ASSERT_EQUAL(true, lf->simplify(*solver));
00665 CPPUNIT_ASSERT_EQUAL(false, solver->hasWatch(a1, lf));
00666 CPPUNIT_ASSERT_EQUAL(false, solver->hasWatch(~b3, lf));
00667 }
00668
00669 void testSimplifyLFIfAllAtomsFalse() {
00670 LoopFormula* lf = lfTestInit();
00671 solver->undoUntil(0);
00672 solver->force( ~a1, 0 );
00673 solver->force( ~a2, 0 );
00674 solver->propagate();
00675 CPPUNIT_ASSERT_EQUAL(false, lf->simplify(*solver));
00676 solver->force( ~a3, 0 );
00677 solver->propagate();
00678 CPPUNIT_ASSERT_EQUAL(true, lf->simplify(*solver));
00679 CPPUNIT_ASSERT_EQUAL(false, solver->hasWatch(~b3, lf));
00680 solver->reduceLearnts(1.0f);
00681 }
00682
00683 void testSimplifyLFRemovesFalseBodies() {
00684 LoopFormula* lf = lfTestInit();
00685 solver->undoUntil(0);
00686
00687 solver->force( ~b1, 0 );
00688 solver->propagate();
00689 CPPUNIT_ASSERT_EQUAL(true, lf->simplify(*solver));
00690 CPPUNIT_ASSERT(3u == solver->sharedContext()->numLearntShort());
00691 }
00692
00693 void testSimplifyLFRemovesFalseAtoms() {
00694 LoopFormula* lf = lfTestInit();
00695 solver->undoUntil(0);
00696 solver->force( ~a1,0 );
00697 solver->propagate();
00698 CPPUNIT_ASSERT_EQUAL(false, lf->simplify(*solver));
00699 CPPUNIT_ASSERT(5 == lf->size());
00700
00701 solver->force( ~a3,0 );
00702 solver->propagate();
00703 CPPUNIT_ASSERT_EQUAL(false, lf->simplify(*solver));
00704 CPPUNIT_ASSERT(4 == lf->size());
00705
00706 solver->force( ~a2,0 );
00707 solver->propagate();
00708 CPPUNIT_ASSERT_EQUAL(true, lf->simplify(*solver));
00709 }
00710
00711 void testSimplifyLFRemovesTrueAtoms() {
00712 LoopFormula* lf = lfTestInit();
00713 solver->undoUntil(0);
00714 solver->force( a1,0 );
00715 solver->propagate();
00716 CPPUNIT_ASSERT_EQUAL(false, lf->simplify(*solver));
00717 CPPUNIT_ASSERT(5 == lf->size());
00718
00719 solver->force( a3,0 );
00720 solver->propagate();
00721 CPPUNIT_ASSERT_EQUAL(false, lf->simplify(*solver));
00722 CPPUNIT_ASSERT(4 == lf->size());
00723
00724 solver->force( a2,0 );
00725 solver->propagate();
00726 CPPUNIT_ASSERT_EQUAL(true, lf->simplify(*solver));
00727 }
00728
00729 void testLoopFormulaPropagateBody() {
00730 LoopFormula* lf = lfTestInit();
00731 solver->undoUntil(0);
00732 solver->assume( ~b1 );
00733 solver->propagate();
00734 solver->assume( ~b3 );
00735 solver->propagate();
00736 solver->assume( a3 );
00737 solver->propagate();
00738
00739 CPPUNIT_ASSERT_EQUAL( true, solver->isTrue(b2) );
00740 CPPUNIT_ASSERT_EQUAL( Antecedent::generic_constraint, solver->reason(b2).type() );
00741 LitVec r;
00742 solver->reason(b2, r);
00743 CPPUNIT_ASSERT_EQUAL( LitVec::size_type(3), r.size() );
00744 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), a3) != r.end());
00745 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b3) != r.end());
00746 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b1) != r.end());
00747
00748 CPPUNIT_ASSERT_EQUAL(true, lf->locked(*solver));
00749 }
00750
00751 void testLoopFormulaPropagateBody2() {
00752 LoopFormula* lf = lfTestInit();
00753 solver->undoUntil(0);
00754 solver->assume( a1 );
00755 solver->propagate();
00756 solver->undoUntil(0);
00757
00758 solver->assume( ~b1 );
00759 solver->propagate();
00760 solver->assume( a2 );
00761 solver->propagate();
00762 solver->assume( ~b2 );
00763 solver->propagate();
00764
00765 CPPUNIT_ASSERT_EQUAL( true, solver->isTrue(b3) );
00766
00767 CPPUNIT_ASSERT_EQUAL( Antecedent::generic_constraint, solver->reason(b3).type() );
00768 LitVec r;
00769 solver->reason(b3, r);
00770 CPPUNIT_ASSERT_EQUAL( LitVec::size_type(3), r.size() );
00771 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b1) != r.end());
00772 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b2) != r.end());
00773 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), a2) != r.end());
00774
00775 CPPUNIT_ASSERT_EQUAL(true, lf->locked(*solver));
00776 }
00777
00778 void testLoopFormulaPropagateAtoms() {
00779 LoopFormula* lf = lfTestInit();
00780 solver->undoUntil(0);
00781 solver->assume( ~b3 );
00782 solver->propagate();
00783 solver->assume( ~b1 );
00784 solver->propagate();
00785 solver->assume( ~b2 );
00786 solver->propagate();
00787
00788 CPPUNIT_ASSERT_EQUAL( true, solver->isTrue(~a1) );
00789 CPPUNIT_ASSERT_EQUAL( true, solver->isTrue(~a2) );
00790 CPPUNIT_ASSERT_EQUAL( true, solver->isTrue(~a3) );
00791
00792 CPPUNIT_ASSERT_EQUAL( Antecedent::generic_constraint, solver->reason(~a1).type() );
00793 LitVec r;
00794 solver->reason(~a1, r);
00795 CPPUNIT_ASSERT_EQUAL( LitVec::size_type(3), r.size() );
00796 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b1) != r.end());
00797 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b2) != r.end());
00798 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b3) != r.end());
00799
00800 CPPUNIT_ASSERT_EQUAL(true, lf->locked(*solver));
00801 }
00802
00803 void testLoopFormulaPropagateAtoms2() {
00804 LoopFormula* lf = lfTestInit();
00805 solver->undoUntil(0);
00806 solver->assume( a1 );
00807 solver->force( a2, 0 );
00808 solver->propagate();
00809 solver->undoUntil(0);
00810
00811 solver->assume( ~b3 );
00812 solver->propagate();
00813 solver->assume( ~b1 );
00814 solver->propagate();
00815 solver->assume( ~b2 );
00816 solver->propagate();
00817
00818 CPPUNIT_ASSERT_EQUAL( true, solver->isTrue(~a1) );
00819 CPPUNIT_ASSERT_EQUAL( true, solver->isTrue(~a2) );
00820 CPPUNIT_ASSERT_EQUAL( true, solver->isTrue(~a3) );
00821
00822
00823 CPPUNIT_ASSERT_EQUAL( Antecedent::generic_constraint, solver->reason(~a1).type() );
00824 LitVec r;
00825 solver->reason(~a1, r);
00826 CPPUNIT_ASSERT_EQUAL( LitVec::size_type(3), r.size() );
00827 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b1) != r.end());
00828 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b2) != r.end());
00829 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b3) != r.end());
00830
00831 CPPUNIT_ASSERT_EQUAL(true, lf->locked(*solver));
00832 }
00833
00834 void testLoopFormulaBodyConflict() {
00835 lfTestInit();
00836 solver->undoUntil(0);
00837
00838 solver->assume( ~b3 );
00839 solver->propagate();
00840 solver->assume( ~b2 );
00841 solver->propagate();
00842 solver->force(a3, 0);
00843 solver->force(~b1, 0);
00844
00845 CPPUNIT_ASSERT_EQUAL( false, solver->propagate() );
00846 const LitVec& r = solver->conflict();
00847
00848 CPPUNIT_ASSERT_EQUAL( LitVec::size_type(4), r.size() );
00849 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), a3) != r.end());
00850 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b3) != r.end());
00851 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b1) != r.end());
00852 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b2) != r.end());
00853 }
00854 void testLoopFormulaAtomConflict() {
00855 lfTestInit();
00856 solver->undoUntil(0);
00857 solver->assume( ~b3 );
00858 solver->propagate();
00859 solver->assume(~b1);
00860 solver->propagate();
00861 solver->force(~b2, 0);
00862 solver->force(a2, 0);
00863 CPPUNIT_ASSERT_EQUAL( false, solver->propagate() );
00864
00865
00866 LitVec r = solver->conflict();
00867
00868 CPPUNIT_ASSERT_EQUAL( LitVec::size_type(4), r.size() );
00869 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), a2) != r.end());
00870 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b3) != r.end());
00871 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b1) != r.end());
00872 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b2) != r.end());
00873
00874 CPPUNIT_ASSERT_EQUAL( true, solver->isTrue(~a1));
00875 solver->reason(~a1, r);
00876 CPPUNIT_ASSERT_EQUAL( LitVec::size_type(3), r.size() );
00877 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b3) != r.end());
00878 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b1) != r.end());
00879 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~b2) != r.end());
00880 }
00881
00882 void testLoopFormulaDontChangeSat() {
00883 lfTestInit();
00884 solver->undoUntil(0);
00885 CPPUNIT_ASSERT_EQUAL(true, solver->assume( ~b1 ) && solver->propagate());
00886 CPPUNIT_ASSERT_EQUAL(true, solver->assume( ~b3 ) && solver->propagate());
00887 CPPUNIT_ASSERT_EQUAL(true, solver->assume( a2 ) && solver->propagate());
00888
00889 CPPUNIT_ASSERT_EQUAL(true, solver->isTrue( b2 ));
00890 LitVec rold;
00891 solver->reason(b2, rold);
00892
00893 CPPUNIT_ASSERT_EQUAL(true, solver->assume( a1 ) && solver->propagate());
00894 CPPUNIT_ASSERT_EQUAL(true, solver->isTrue( b2 ));
00895 LitVec rnew;
00896 solver->reason(b2, rnew);
00897 CPPUNIT_ASSERT(rold == rnew);
00898 }
00899
00900 void testLoopFormulaSatisfied() {
00901 LoopFormula* lf = lfTestInit();
00902 ConstraintType t= Constraint_t::learnt_loop;
00903 TypeSet ts, other; ts.addSet(t); other.addSet(Constraint_t::learnt_conflict);
00904 LitVec free;
00905 CPPUNIT_ASSERT_EQUAL(uint32(0), lf->isOpen(*solver, ts, free));
00906 solver->undoUntil(0);
00907 free.clear();
00908 CPPUNIT_ASSERT_EQUAL(uint32(lf->type()), lf->isOpen(*solver, ts, free));
00909 CPPUNIT_ASSERT_EQUAL(LitVec::size_type(6), free.size());
00910 CPPUNIT_ASSERT_EQUAL(uint32(0), lf->isOpen(*solver, other, free));
00911 solver->assume( a1 );
00912 solver->assume( ~b2 );
00913 solver->propagate();
00914 free.clear();
00915 CPPUNIT_ASSERT_EQUAL(uint32(lf->type()), lf->isOpen(*solver, ts, free));
00916 CPPUNIT_ASSERT_EQUAL(LitVec::size_type(4), free.size());
00917 solver->assume( ~b1 );
00918 solver->propagate();
00919 CPPUNIT_ASSERT_EQUAL(uint32(0), lf->isOpen(*solver, ts, free));
00920 }
00921
00922 void testLoopFormulaBugEq() {
00923 ctx.endInit();
00924 Literal body1 = b1;
00925 Literal body2 = b2;
00926 Literal body3 = ~b3;
00927 solver->assume(~body1);
00928 solver->assume(~body2);
00929 solver->assume(~body3);
00930 solver->propagate();
00931 Literal bodies[3] = {body1, body2, body3 };
00932 LoopFormula* lf = LoopFormula::newLoopFormula(*solver, &bodies[0], 3, 2, 1, Activity(0,10));
00933 solver->addLearnt(lf, lf->size());
00934 solver->force(~a1, lf);
00935 lf->addAtom(~a1, *solver);
00936 solver->propagate();
00937 solver->undoUntil(solver->decisionLevel()-2);
00938 CPPUNIT_ASSERT_EQUAL(true, solver->assume(~body3) && solver->propagate());
00939 CPPUNIT_ASSERT_EQUAL(true, solver->assume(a1) && solver->propagate());
00940 CPPUNIT_ASSERT_EQUAL(true, solver->isTrue(body2));
00941 }
00942
00943 void testLoopFormulaPropTrueAtomInSatClause() {
00944 lfTestInit();
00945 solver->undoUntil(0);
00946 solver->assume( ~a1 );
00947 solver->propagate();
00948
00949 solver->assume( a2 );
00950 solver->force( ~b3, 0 );
00951 solver->force( ~b2, 0 );
00952 solver->propagate();
00953
00954 CPPUNIT_ASSERT_EQUAL( true, solver->isTrue(b1) );
00955 }
00956 private:
00957 SharedContext ctx;
00958 Solver* solver;
00959 int countWatches(const Solver& s, ClauseHead* c, const LitVec& lits) {
00960 int w = 0;
00961 for (LitVec::size_type i = 0; i != lits.size(); ++i) {
00962 w += s.hasWatch(~lits[i], c);
00963 }
00964 return w;
00965 }
00966 void check(Clause& c) {
00967 std::string s = toString(clLits);
00968 std::random_shuffle(clLits.begin(), clLits.end());
00969 CPPUNIT_ASSERT( value_free == solver->value(clLits.back().var()) );
00970 for (LitVec::size_type i = 0; i != clLits.size() - 1; ++i) {
00971 CPPUNIT_ASSERT( value_free == solver->value(clLits[i].var()) );
00972 solver->force(~clLits[i], 0);
00973 solver->propagate();
00974 }
00975 CPPUNIT_ASSERT_EQUAL_MESSAGE(s.c_str(), true, solver->isTrue(clLits.back()));
00976
00977 Antecedent reason = solver->reason(clLits.back());
00978 CPPUNIT_ASSERT(reason == &c);
00979 LitVec r;
00980 c.reason(*solver, clLits.back(), r);
00981 for (LitVec::size_type i = 0; i != clLits.size() - 1; ++i) {
00982 LitVec::iterator it = std::find(r.begin(), r.end(), ~clLits[i]);
00983 CPPUNIT_ASSERT_MESSAGE(s.c_str(), it != r.end());
00984 r.erase(it);
00985 }
00986 while (!r.empty() && isSentinel(r.back())) r.pop_back();
00987 CPPUNIT_ASSERT(r.empty());
00988 }
00989 std::string toString(const LitVec& c) {
00990 std::string res="[";
00991 for (uint32 i = 0; i != c.size(); ++i) {
00992 if (c[i].sign()) {
00993 res += '~';
00994 }
00995 res += ('a' + i);
00996 res += ' ';
00997 }
00998 res+="]";
00999 return res;
01000 }
01001 Clause* createClause(LitVec& lits, const ClauseInfo& info) {
01002 uint32 flags = ClauseCreator::clause_explicit | ClauseCreator::clause_no_add | ClauseCreator::clause_no_prepare;
01003 return (Clause*)ClauseCreator::create(*solver, lits, flags, info).local;
01004 }
01005 Clause* createClause(int pos, int neg, ConstraintType t = Constraint_t::static_constraint) {
01006 clLits.clear();
01007 int size = pos + neg;
01008 LitVec lit(size);
01009 for (int i = 0; i < pos; ++i) {
01010 lit[i] = posLit(i+1);
01011 clLits.push_back(lit[i]);
01012 }
01013 for (int i = pos; i < pos + neg; ++i) {
01014 lit[i] = negLit(i+1);
01015 clLits.push_back(lit[i]);
01016 }
01017 return createClause(clLits, ClauseInfo(t));
01018 }
01019
01020 Clause* createRandomClause(int size) {
01021 int pos = rand() % size + 1;
01022 return createClause( pos, size - pos );
01023 }
01024
01025 LoopFormula* lfTestInit() {
01026 ctx.endInit();
01027 solver->assume(~b1);
01028 solver->assume(~b2);
01029 solver->assume(~b3);
01030 solver->propagate();
01031 Literal bodies[3] = {b1, b2, b3 };
01032 LoopFormula* lf = LoopFormula::newLoopFormula(*solver, &bodies[0], 3, 2, 3, Activity(0,10));
01033 solver->addLearnt(lf, lf->size());
01034 solver->force(~a1, lf);
01035 solver->force(~a2, lf);
01036 solver->force(~a3, lf);
01037 lf->addAtom(~a1, *solver);
01038 lf->addAtom(~a2, *solver);
01039 lf->addAtom(~a3, *solver);
01040 solver->propagate();
01041 return lf;
01042 }
01043 Literal a1, a2, a3, b1, b2, b3;
01044 LitVec clLits;
01045 };
01046 CPPUNIT_TEST_SUITE_REGISTRATION(ClauseTest);
01047 } }