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/solver.h>
00022 #include <clasp/clause.h>
00023
00024 namespace Clasp { namespace Test {
00025 using namespace Clasp::mt;
00026 struct TestingConstraint : public LearntConstraint {
00027 TestingConstraint(bool* del = 0, ConstraintType t = Constraint_t::static_constraint)
00028 : type_(t), propagates(0), undos(0), sat(false), keepWatch(true), setConflict(false), deleted(del) {}
00029 Constraint* cloneAttach(Solver&) {
00030 return new TestingConstraint(0, type_);
00031 }
00032 PropResult propagate(Solver&, Literal, uint32&) {
00033 ++propagates;
00034 return PropResult(!setConflict, keepWatch);
00035 }
00036 void undoLevel(Solver&) {
00037 ++undos;
00038 }
00039 bool simplify(Solver&, bool) { return sat; }
00040 void reason(Solver&, Literal, LitVec& out) { out = ante; }
00041 void destroy(Solver* s, bool b) {
00042 if (deleted) *deleted = true;
00043 LearntConstraint::destroy(s, b);
00044 }
00045 bool locked(const Solver&) const { return false; }
00046 uint32 isOpen(const Solver&, const TypeSet&, LitVec&) { return 0; }
00047 static uint32 size() { return uint32(10); }
00048 ConstraintType type() const { return type_; }
00049 LitVec ante;
00050 ConstraintType type_;
00051 int propagates;
00052 int undos;
00053 bool sat;
00054 bool keepWatch;
00055 bool setConflict;
00056 bool* deleted;
00057 };
00058 struct TestingPostProp : public PostPropagator {
00059 explicit TestingPostProp(bool cfl, uint32 p = PostPropagator::priority_class_simple) : props(0), resets(0), inits(0), prio(p), conflict(cfl), deleteOnProp(false) {}
00060 bool propagateFixpoint(Solver& s, PostPropagator*) {
00061 ++props;
00062 bool ok = !conflict;
00063 if (deleteOnProp) {
00064 s.removePost(this);
00065 this->destroy();
00066 }
00067 return ok;
00068 }
00069 void reset() {
00070 ++resets;
00071 }
00072 bool init(Solver&) { ++inits; return true; }
00073 uint32 priority() const { return prio; }
00074 int props;
00075 int resets;
00076 int inits;
00077 uint32 prio;
00078 bool conflict;
00079 bool deleteOnProp;
00080 };
00081
00082 class SolverTest : public CppUnit::TestFixture {
00083 CPPUNIT_TEST_SUITE(SolverTest);
00084 CPPUNIT_TEST(testReasonStore);
00085 CPPUNIT_TEST(testSingleOwnerPtr);
00086 CPPUNIT_TEST(testDefaults);
00087 CPPUNIT_TEST(testVarNullIsSentinel);
00088 CPPUNIT_TEST(testSolverAlwaysContainsSentinelVar);
00089 CPPUNIT_TEST(testSolverOwnsConstraints);
00090 CPPUNIT_TEST(testAddVar);
00091 CPPUNIT_TEST(testEliminateVar);
00092 CPPUNIT_TEST(testResurrectVar);
00093 CPPUNIT_TEST(testCmpScores);
00094
00095 CPPUNIT_TEST(testValueSet);
00096 CPPUNIT_TEST(testPreferredLitByType);
00097 CPPUNIT_TEST(testInitSavedValue);
00098 CPPUNIT_TEST(testReset);
00099 CPPUNIT_TEST(testForce);
00100 CPPUNIT_TEST(testNoUpdateOnConsistentAssign);
00101 CPPUNIT_TEST(testAssume);
00102 CPPUNIT_TEST(testGetDecision);
00103 CPPUNIT_TEST(testAddWatch);
00104 CPPUNIT_TEST(testRemoveWatch);
00105 CPPUNIT_TEST(testNotifyWatch);
00106 CPPUNIT_TEST(testKeepWatchOnPropagate);
00107 CPPUNIT_TEST(testRemoveWatchOnPropagate);
00108 CPPUNIT_TEST(testWatchOrder);
00109 CPPUNIT_TEST(testUndoUntil);
00110 CPPUNIT_TEST(testUndoWatches);
00111 CPPUNIT_TEST(testPropBinary);
00112 CPPUNIT_TEST(testPropTernary);
00113 CPPUNIT_TEST(testRestartAfterUnitLitResolvedBug);
00114 CPPUNIT_TEST(testEstimateBCP);
00115 CPPUNIT_TEST(testEstimateBCPLoop);
00116 CPPUNIT_TEST(testAssertImmediate);
00117 CPPUNIT_TEST(testPreferShortBfs);
00118
00119 CPPUNIT_TEST(testPostPropInit);
00120 CPPUNIT_TEST(testPropagateCallsPostProp);
00121 CPPUNIT_TEST(testPropagateCallsResetOnConflict);
00122 CPPUNIT_TEST(testPostpropPriority);
00123 CPPUNIT_TEST(testPostpropPriorityExt);
00124 CPPUNIT_TEST(testPostpropRemove);
00125 CPPUNIT_TEST(testPostpropRemoveOnProp);
00126 CPPUNIT_TEST(testPostpropBug);
00127 CPPUNIT_TEST(testPostpropAddAfterInitBug);
00128
00129 CPPUNIT_TEST(testSimplifyRemovesSatBinClauses);
00130 CPPUNIT_TEST(testSimplifyRemovesSatTernClauses);
00131 CPPUNIT_TEST(testSimplifyRemovesSatConstraints);
00132 CPPUNIT_TEST(testRemoveConditional);
00133 CPPUNIT_TEST(testStrengthenConditional);
00134 CPPUNIT_TEST(testLearnConditional);
00135
00136
00137 CPPUNIT_TEST(testResolveUnary);
00138 CPPUNIT_TEST(testResolveConflict);
00139 CPPUNIT_TEST(testResolveConflictBounded);
00140
00141 CPPUNIT_TEST(testClearAssumptions);
00142 CPPUNIT_TEST(testStopConflict);
00143
00144 CPPUNIT_TEST(testSearchKeepsAssumptions);
00145 CPPUNIT_TEST(testSearchAddsLearntFacts);
00146 CPPUNIT_TEST(testSearchMaxConflicts);
00147
00148 CPPUNIT_TEST(testStats);
00149 #if WITH_THREADS
00150 CPPUNIT_TEST(testLearntShort);
00151 CPPUNIT_TEST(testLearntShortAreDistributed);
00152 CPPUNIT_TEST(testAuxAreNotDistributed);
00153 CPPUNIT_TEST(testAttachToDB);
00154 CPPUNIT_TEST(testAttachDeferred);
00155 #endif
00156
00157 CPPUNIT_TEST(testUnfortunateSplitSeq);
00158 CPPUNIT_TEST(testSplitInc);
00159 CPPUNIT_TEST(testSplitFlipped);
00160 CPPUNIT_TEST(testSplitFlipToNewRoot);
00161 CPPUNIT_TEST(testSplitImplied);
00162
00163 CPPUNIT_TEST(testAddShortIncremental);
00164 CPPUNIT_TEST(testSwitchToMtIncremental);
00165 #if TEST_ONCE
00166 CPPUNIT_TEST(testScheduleAdvance);
00167 CPPUNIT_TEST(testLubyAdvance);
00168 #endif
00169
00170 CPPUNIT_TEST(testPushAux);
00171 CPPUNIT_TEST(testPushAuxFact);
00172 CPPUNIT_TEST(testPopAuxRemovesConstraints);
00173 CPPUNIT_TEST(testPopAuxMaintainsQueue);
00174 CPPUNIT_TEST(testIncrementalAux);
00175
00176 CPPUNIT_TEST(testUnfreezeStepBug);
00177 CPPUNIT_TEST(testRemoveConstraint);
00178 CPPUNIT_TEST_SUITE_END();
00179 public:
00180 void setUp() {
00181 }
00182 template <class ST>
00183 void testReasonStore() {
00184 ST store;
00185 store.resize(1);
00186 store.dataResize(1);
00187 Constraint* x = new TestingConstraint(0, Constraint_t::learnt_conflict);
00188 store[0] = x;
00189 store.setData(0, 22);
00190 CPPUNIT_ASSERT(store[0] == x);
00191 CPPUNIT_ASSERT(store.data(0) == 22);
00192 Literal p(10,0), q(22, 0);
00193 store[0] = Antecedent(p, q);
00194 uint32 old = store.data(0);
00195 store.setData(0, 74);
00196 CPPUNIT_ASSERT(store.data(0) == 74);
00197 store.setData(0, old);
00198 CPPUNIT_ASSERT(store[0].firstLiteral() == p && store[0].secondLiteral() == q);
00199
00200 typedef typename ST::value_type ReasonWithData;
00201 ReasonWithData rwd(x, 169);
00202 store[0] = rwd.ante();
00203 if (rwd.data() != UINT32_MAX) {
00204 store.setData(0, rwd.data());
00205 }
00206 CPPUNIT_ASSERT(store[0] == x);
00207 CPPUNIT_ASSERT(store.data(0) == 169);
00208
00209 rwd = ReasonWithData(p, UINT32_MAX);
00210 store[0] = rwd.ante();
00211 if (rwd.data() != UINT32_MAX) {
00212 store.setData(0, rwd.data());
00213 }
00214 CPPUNIT_ASSERT(store[0].firstLiteral() == p);
00215 x->destroy();
00216 }
00217 void testReasonStore() {
00218 if (sizeof(void*) == sizeof(uint32)) {
00219 testReasonStore<ReasonStore32>();
00220 }
00221 testReasonStore<ReasonStore64>();
00222 }
00223
00224 void testSingleOwnerPtr() {
00225 bool conDel1 = false, conDel2 = false;
00226 TestingConstraint* f = new TestingConstraint(&conDel2);
00227 {
00228 SingleOwnerPtr<Constraint, DestroyObject> x(new TestingConstraint(&conDel1));
00229 SingleOwnerPtr<Constraint, DestroyObject> y(f);
00230 y.release();
00231 }
00232 CPPUNIT_ASSERT_EQUAL(true, conDel1);
00233 CPPUNIT_ASSERT_EQUAL(false, conDel2);
00234 {
00235 SingleOwnerPtr<Constraint, DestroyObject> y(f);
00236 y = f;
00237 CPPUNIT_ASSERT_EQUAL(true, y.is_owner());
00238 y.release();
00239 CPPUNIT_ASSERT_EQUAL(false, conDel2);
00240 y = f;
00241 CPPUNIT_ASSERT_EQUAL(true, !conDel2 && y.is_owner());
00242 }
00243 CPPUNIT_ASSERT_EQUAL(true, conDel2);
00244 }
00245 void testDefaults() {
00246 Solver& s = *ctx.master();
00247 const SolverParams& x = s.configuration();
00248 CPPUNIT_ASSERT(x.heuId == 0);
00249 CPPUNIT_ASSERT(x.ccMinRec == false);
00250 CPPUNIT_ASSERT(x.ccMinAntes == SolverStrategies::all_antes);
00251 CPPUNIT_ASSERT(x.search == SolverStrategies::use_learning);
00252 CPPUNIT_ASSERT(x.compress == 0);
00253 CPPUNIT_ASSERT(x.initWatches == SolverStrategies::watch_rand);
00254
00255 CPPUNIT_ASSERT_EQUAL(0u, s.numVars());
00256 CPPUNIT_ASSERT_EQUAL(0u, s.numAssignedVars());
00257 CPPUNIT_ASSERT_EQUAL(0u, s.numConstraints());
00258 CPPUNIT_ASSERT_EQUAL(0u, s.numLearntConstraints());
00259 CPPUNIT_ASSERT_EQUAL(0u, s.decisionLevel());
00260 CPPUNIT_ASSERT_EQUAL(0u, s.queueSize());
00261 ctx.setFrozen(0, true);
00262 CPPUNIT_ASSERT(ctx.stats().vars_frozen == 0);
00263 }
00264 void testVarNullIsSentinel() {
00265 Literal p = posLit(0);
00266 CPPUNIT_ASSERT_EQUAL(true, isSentinel(p));
00267 CPPUNIT_ASSERT_EQUAL(true, isSentinel(~p));
00268 }
00269 void testSolverAlwaysContainsSentinelVar() {
00270 Solver& s = *ctx.master();
00271 CPPUNIT_ASSERT_EQUAL(value_true, s.value(sentVar));
00272 CPPUNIT_ASSERT(s.isTrue(posLit(sentVar)));
00273 CPPUNIT_ASSERT(s.isFalse(negLit(sentVar)));
00274 CPPUNIT_ASSERT(s.seen(sentVar) == true);
00275 }
00276 void testSolverOwnsConstraints() {
00277 bool conDel = false;
00278 bool lconDel = false;
00279 {
00280 SharedContext ctx;
00281 Solver& s = ctx.startAddConstraints();
00282 ctx.add( new TestingConstraint(&conDel) );
00283 ctx.endInit();
00284 s.addLearnt( new TestingConstraint(&lconDel, Constraint_t::learnt_conflict), TestingConstraint::size());
00285 CPPUNIT_ASSERT_EQUAL(1u, s.numConstraints());
00286 CPPUNIT_ASSERT_EQUAL(1u, s.numLearntConstraints());
00287 }
00288 CPPUNIT_ASSERT_EQUAL(true, conDel);
00289 CPPUNIT_ASSERT_EQUAL(true, lconDel);
00290 }
00291
00292 void testAddVar() {
00293 Var v1 = ctx.addVar(Var_t::atom_var);
00294 Var v2 = ctx.addVar(Var_t::body_var);
00295 Solver& s = ctx.startAddConstraints();
00296 ctx.endInit();
00297 CPPUNIT_ASSERT_EQUAL(2u, s.numVars());
00298 CPPUNIT_ASSERT_EQUAL(0u, s.numAssignedVars());
00299 CPPUNIT_ASSERT_EQUAL(2u, s.numFreeVars());
00300 CPPUNIT_ASSERT_EQUAL(Var_t::atom_var, ctx.varInfo(v1).type());
00301 CPPUNIT_ASSERT_EQUAL(Var_t::body_var, ctx.varInfo(v2).type());
00302
00303 CPPUNIT_ASSERT_EQUAL( true, ctx.varInfo(v1).preferredSign() );
00304 CPPUNIT_ASSERT_EQUAL( false, ctx.varInfo(v2).preferredSign() );
00305 }
00306
00307 void testEliminateVar() {
00308 Var v1 = ctx.addVar(Var_t::atom_var);
00309 ctx.addVar(Var_t::body_var);
00310 Solver& s = ctx.startAddConstraints();
00311 ctx.eliminate(v1);
00312 CPPUNIT_ASSERT_EQUAL(uint32(2), s.numVars());
00313 CPPUNIT_ASSERT_EQUAL(uint32(1), ctx.numEliminatedVars());
00314 CPPUNIT_ASSERT_EQUAL(uint32(1), s.numFreeVars());
00315 CPPUNIT_ASSERT_EQUAL(uint32(0), s.numAssignedVars());
00316 CPPUNIT_ASSERT_EQUAL(true, ctx.eliminated(v1));
00317
00318 CPPUNIT_ASSERT(s.value(v1) != value_free);
00319
00320
00321 ctx.eliminate(v1);
00322 CPPUNIT_ASSERT_EQUAL(uint32(1), ctx.numEliminatedVars());
00323 ctx.endInit();
00324 }
00325 void testResurrectVar() {
00326
00327
00328
00329
00330
00331
00332
00333
00334
00335
00336
00337
00338
00339
00340
00341
00342
00343
00344
00345
00346
00347
00348
00349 CPPUNIT_FAIL("TODO - Resurrection of vars not yet supported\n");
00350 }
00351
00352 void testCmpScores() {
00353 ReduceStrategy rs;
00354 Activity a1(100, 5);
00355 Activity a2(90, 3);
00356 CPPUNIT_ASSERT(rs.compare(ReduceStrategy::score_act, a1, a2) > 0);
00357 CPPUNIT_ASSERT(rs.compare(ReduceStrategy::score_lbd, a1, a2) < 0);
00358 CPPUNIT_ASSERT(rs.compare(ReduceStrategy::score_both, a1, a2) > 0);
00359 }
00360
00361 void testValueSet() {
00362 ValueSet vs;
00363 CPPUNIT_ASSERT_EQUAL(vs.empty(), true);
00364 vs.set(ValueSet::pref_value, value_true);
00365 CPPUNIT_ASSERT_EQUAL(vs.empty(), false);
00366 CPPUNIT_ASSERT_EQUAL(vs.has(ValueSet::pref_value), true);
00367 CPPUNIT_ASSERT_EQUAL(vs.sign(), false);
00368 vs.set(ValueSet::saved_value, value_false);
00369 CPPUNIT_ASSERT_EQUAL(vs.has(ValueSet::saved_value), true);
00370 CPPUNIT_ASSERT_EQUAL(vs.sign(), true);
00371
00372 vs.set(ValueSet::user_value, value_true);
00373 CPPUNIT_ASSERT_EQUAL(vs.has(ValueSet::user_value), true);
00374 CPPUNIT_ASSERT_EQUAL(vs.sign(), false);
00375
00376 vs.set(ValueSet::user_value, value_free);
00377 CPPUNIT_ASSERT_EQUAL(vs.has(ValueSet::user_value), false);
00378 CPPUNIT_ASSERT_EQUAL(vs.sign(), true);
00379 }
00380 void testPreferredLitByType() {
00381 Var v1 = ctx.addVar(Var_t::atom_var);
00382 Var v2 = ctx.addVar(Var_t::body_var);
00383 Var v3 = ctx.addVar(Var_t::atom_var, true);
00384 Var v4 = ctx.addVar(Var_t::body_var, true);
00385 CPPUNIT_ASSERT_EQUAL( true, ctx.varInfo(v1).preferredSign() );
00386 CPPUNIT_ASSERT_EQUAL( false, ctx.varInfo(v2).preferredSign() );
00387 CPPUNIT_ASSERT_EQUAL( true, ctx.varInfo(v3).preferredSign() );
00388 CPPUNIT_ASSERT_EQUAL( false, ctx.varInfo(v4).preferredSign() );
00389 Solver& s = ctx.startAddConstraints();
00390 CPPUNIT_ASSERT_EQUAL( negLit(v1), DecisionHeuristic::selectLiteral(s, v1, 0) );
00391 CPPUNIT_ASSERT_EQUAL( posLit(v2), DecisionHeuristic::selectLiteral(s, v2, 0) );
00392 ctx.setInDisj(v1, true);
00393 ctx.master()->strategy.signDef = SolverStrategies::sign_disj;
00394 CPPUNIT_ASSERT_EQUAL( posLit(v1), DecisionHeuristic::selectLiteral(s, v1, 0) );
00395 }
00396
00397 void testInitSavedValue() {
00398 Var v1 = ctx.addVar(Var_t::atom_var);
00399 Var v2 = ctx.addVar(Var_t::body_var);
00400 Solver& s = ctx.startAddConstraints();
00401 ctx.endInit();
00402 CPPUNIT_ASSERT_EQUAL( value_free, s.pref(v1).get(ValueSet::saved_value) );
00403 CPPUNIT_ASSERT_EQUAL( value_free, s.pref(v2).get(ValueSet::saved_value) );
00404
00405 s.setPref(v1, ValueSet::saved_value, value_true);
00406 s.setPref(v2, ValueSet::saved_value, value_false);
00407
00408 CPPUNIT_ASSERT_EQUAL( value_true, s.pref(v1).get(ValueSet::saved_value) );
00409 CPPUNIT_ASSERT_EQUAL( value_false, s.pref(v2).get(ValueSet::saved_value));
00410 }
00411
00412 void testReset() {
00413 ctx.master()->strategy.initWatches = SolverStrategies::watch_rand;
00414 ctx.addVar(Var_t::atom_var); ctx.addVar(Var_t::body_var);
00415 Solver& s = ctx.startAddConstraints();
00416 s.add( new TestingConstraint(0) );
00417 ctx.endInit();
00418 s.addLearnt( new TestingConstraint(0, Constraint_t::learnt_conflict), TestingConstraint::size());
00419 s.assume( posLit(1) );
00420 ctx.reset();
00421 testDefaults();
00422 Var n = ctx.addVar(Var_t::body_var);
00423 ctx.startAddConstraints();
00424 ctx.endInit();
00425 CPPUNIT_ASSERT_EQUAL(Var_t::body_var, ctx.varInfo(n).type());
00426 }
00427
00428 void testForce() {
00429 Var v1 = ctx.addVar(Var_t::atom_var);
00430 Var v2 = ctx.addVar(Var_t::atom_var);
00431 Solver& s = ctx.startAddConstraints();
00432 ctx.endInit();
00433 CPPUNIT_ASSERT_EQUAL(true, s.force(posLit(v1), 0));
00434 CPPUNIT_ASSERT_EQUAL(true, s.force(negLit(v2), posLit(v1)));
00435 CPPUNIT_ASSERT_EQUAL(true, s.isTrue(posLit(v1)));
00436 CPPUNIT_ASSERT_EQUAL(true, s.isTrue(negLit(v2)));
00437 CPPUNIT_ASSERT(s.reason(negLit(v2)).type() == Antecedent::binary_constraint);
00438
00439 CPPUNIT_ASSERT_EQUAL(2u, s.queueSize());
00440 }
00441
00442 void testNoUpdateOnConsistentAssign() {
00443 Var v1 = ctx.addVar(Var_t::atom_var);
00444 Var v2 = ctx.addVar(Var_t::atom_var);
00445 Solver& s = ctx.startAddConstraints();
00446 s.force( posLit(v2), 0 );
00447 s.force( posLit(v1), 0 );
00448 uint32 oldA = s.numAssignedVars();
00449 CPPUNIT_ASSERT_EQUAL(true, s.force( posLit(v1), posLit(v2) ));
00450 CPPUNIT_ASSERT_EQUAL(oldA, s.numAssignedVars());
00451 CPPUNIT_ASSERT_EQUAL(2u, s.queueSize());
00452 }
00453
00454 void testAssume() {
00455 Literal p = posLit(ctx.addVar(Var_t::atom_var));
00456 Solver& s = ctx.startAddConstraints();
00457 CPPUNIT_ASSERT_EQUAL(true, s.assume(p));
00458 CPPUNIT_ASSERT_EQUAL(value_true, s.value(p.var()));
00459 CPPUNIT_ASSERT_EQUAL(1u, s.decisionLevel());
00460 CPPUNIT_ASSERT_EQUAL(1u, s.queueSize());
00461 }
00462
00463 void testGetDecision() {
00464 Literal p = posLit(ctx.addVar(Var_t::atom_var));
00465 Literal q = posLit(ctx.addVar(Var_t::atom_var));
00466 Literal r = posLit(ctx.addVar(Var_t::atom_var));
00467 Solver& s = ctx.startAddConstraints();
00468 s.assume(p);
00469 s.assume(q);
00470 s.assume(~r);
00471 CPPUNIT_ASSERT_EQUAL(p, s.decision(1));
00472 CPPUNIT_ASSERT_EQUAL(q, s.decision(2));
00473 CPPUNIT_ASSERT_EQUAL(~r, s.decision(3));
00474 CPPUNIT_ASSERT_EQUAL(~r, s.decision(s.decisionLevel()));
00475 }
00476 void testAddWatch() {
00477 Literal p = posLit(ctx.addVar(Var_t::atom_var));
00478 Solver& s = ctx.startAddConstraints();
00479 TestingConstraint c;
00480 CPPUNIT_ASSERT_EQUAL(false, s.hasWatch(p, &c));
00481 s.addWatch(p, &c);
00482 CPPUNIT_ASSERT_EQUAL(true, s.hasWatch(p, &c));
00483 CPPUNIT_ASSERT_EQUAL(1u, s.numWatches(p));
00484 }
00485
00486 void testRemoveWatch() {
00487 Literal p = posLit(ctx.addVar(Var_t::atom_var));
00488 Solver& s = ctx.startAddConstraints();
00489 TestingConstraint c;
00490 s.addWatch(p, &c);
00491 s.removeWatch(p, &c);
00492 CPPUNIT_ASSERT_EQUAL(false, s.hasWatch(p, &c));
00493 }
00494
00495 void testNotifyWatch() {
00496 Literal p = posLit(ctx.addVar(Var_t::atom_var)), q = posLit(ctx.addVar(Var_t::atom_var));
00497 TestingConstraint c;
00498 Solver& s = ctx.startAddConstraints();
00499 ctx.endInit();
00500 s.addWatch(p, &c);
00501 s.addWatch(q, &c);
00502 s.assume(p);
00503 s.propagate();
00504 CPPUNIT_ASSERT_EQUAL(1, c.propagates);
00505 s.assume(~q);
00506 s.propagate();
00507 CPPUNIT_ASSERT_EQUAL(1, c.propagates);
00508 }
00509
00510 void testKeepWatchOnPropagate() {
00511 Literal p = posLit(ctx.addVar(Var_t::atom_var));
00512 Solver& s = ctx.startAddConstraints();
00513 ctx.endInit();
00514 TestingConstraint c;
00515 s.addWatch(p, &c);
00516 s.assume(p);
00517 s.propagate();
00518 CPPUNIT_ASSERT_EQUAL(true, s.hasWatch(p, &c));
00519 }
00520
00521 void testRemoveWatchOnPropagate() {
00522 Literal p = posLit(ctx.addVar(Var_t::atom_var));
00523 Solver& s = ctx.startAddConstraints();
00524 ctx.endInit();
00525 TestingConstraint c;
00526 c.keepWatch = false;
00527 s.addWatch(p, &c);
00528 s.assume(p);
00529 s.propagate();
00530 CPPUNIT_ASSERT_EQUAL(false, s.hasWatch(p, &c));
00531 }
00532
00533 void testWatchOrder() {
00534 Literal p = posLit(ctx.addVar(Var_t::atom_var));
00535 Solver& s = ctx.startAddConstraints();
00536 ctx.endInit();
00537 TestingConstraint c1, c2, c3;
00538 c1.keepWatch = false;
00539 c2.setConflict = true;
00540 s.addWatch(p, &c1);
00541 s.addWatch(p, &c2);
00542 s.addWatch(p, &c3);
00543 s.assume(p);
00544 CPPUNIT_ASSERT_EQUAL(false, s.propagate());
00545 CPPUNIT_ASSERT_EQUAL(false, s.hasWatch(p, &c1));
00546 CPPUNIT_ASSERT_EQUAL(true, s.hasWatch(p, &c2));
00547 CPPUNIT_ASSERT_EQUAL(true, s.hasWatch(p, &c3));
00548 CPPUNIT_ASSERT_EQUAL(1, c1.propagates);
00549 CPPUNIT_ASSERT_EQUAL(1, c2.propagates);
00550 CPPUNIT_ASSERT_EQUAL(0, c3.propagates);
00551 }
00552
00553 void testUndoUntil() {
00554 Literal a = posLit(ctx.addVar(Var_t::atom_var)), b = posLit(ctx.addVar(Var_t::atom_var))
00555 , c = posLit(ctx.addVar(Var_t::atom_var)), d = posLit(ctx.addVar(Var_t::atom_var));
00556 Solver& s = ctx.startAddConstraints();
00557 s.assume(a);
00558 s.force(~b, a);
00559 s.force(~c, a);
00560 s.force(d, a);
00561 CPPUNIT_ASSERT_EQUAL(4u, s.queueSize());
00562 CPPUNIT_ASSERT_EQUAL(4u, s.numAssignedVars());
00563 s.undoUntil(0u);
00564 CPPUNIT_ASSERT_EQUAL(0u, s.numAssignedVars());
00565 for (Var i = a.var(); i != d.var()+1; ++i) {
00566 CPPUNIT_ASSERT_EQUAL(value_free, s.value(i));
00567 }
00568 }
00569
00570 void testUndoWatches() {
00571 Literal a = posLit(ctx.addVar(Var_t::atom_var)), b = posLit(ctx.addVar(Var_t::atom_var));
00572 TestingConstraint c;
00573 Solver& s = ctx.startAddConstraints();
00574 ctx.endInit();
00575 s.assume(a);
00576 s.addUndoWatch(1, &c);
00577 s.assume(b);
00578 s.undoUntil(1);
00579 CPPUNIT_ASSERT_EQUAL(0, c.undos);
00580 s.undoUntil(0);
00581 CPPUNIT_ASSERT_EQUAL(1, c.undos);
00582 }
00583
00584 void testPropBinary() {
00585 LitVec bin = addBinary();
00586 Solver& s = *ctx.master();
00587 for (int i = 0; i < 2; ++i) {
00588 s.assume(~bin[i]);
00589 CPPUNIT_ASSERT(s.propagate());
00590 int o = (i+1)%2;
00591 CPPUNIT_ASSERT_EQUAL(true, s.isTrue(bin[o]));
00592 CPPUNIT_ASSERT_EQUAL(Antecedent::binary_constraint, s.reason(bin[o]).type());
00593 LitVec r;
00594 s.reason(bin[o], r);
00595 CPPUNIT_ASSERT_EQUAL(1u, (uint32)r.size());
00596 CPPUNIT_ASSERT(~bin[i] == r[0]);
00597 s.undoUntil(0);
00598 }
00599 s.assume(~bin[0]);
00600 s.force(~bin[1], 0);
00601 CPPUNIT_ASSERT_EQUAL(false, s.propagate());
00602 const LitVec& r = s.conflict();
00603 CPPUNIT_ASSERT_EQUAL(2u, (uint32)r.size());
00604 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~bin[0]) != r.end());
00605 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~bin[1]) != r.end());
00606 }
00607
00608 void testPropTernary() {
00609 LitVec tern = addTernary();
00610 Solver& s = *ctx.master();
00611 for (int i = 0; i < 3; ++i) {
00612 s.assume(~tern[i]);
00613 s.assume(~tern[(i+1)%3]);
00614 CPPUNIT_ASSERT(s.propagate());
00615 int o = (i+2)%3;
00616 CPPUNIT_ASSERT_EQUAL(true, s.isTrue(tern[o]));
00617 CPPUNIT_ASSERT_EQUAL(Antecedent::ternary_constraint, s.reason(tern[o]).type());
00618 LitVec r;
00619 s.reason(tern[o], r);
00620 CPPUNIT_ASSERT_EQUAL(2u, (uint32)r.size());
00621 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~tern[i]) != r.end());
00622 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~tern[(i+1)%3]) != r.end());
00623 s.undoUntil(0);
00624 }
00625 s.assume(~tern[0]);
00626 s.force(~tern[1], 0);
00627 s.force(~tern[2], 0);
00628 CPPUNIT_ASSERT_EQUAL(false, s.propagate());
00629 const LitVec& r = s.conflict();
00630 CPPUNIT_ASSERT_EQUAL(3u, (uint32)r.size());
00631 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~tern[0]) != r.end());
00632 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~tern[1]) != r.end());
00633 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~tern[2]) != r.end());
00634 }
00635
00636 void testRestartAfterUnitLitResolvedBug() {
00637 LitVec bin = addBinary();
00638 Solver& s = *ctx.master();
00639 s.force(~bin[0], 0);
00640 s.undoUntil(0);
00641 s.propagate();
00642 CPPUNIT_ASSERT_EQUAL(true, s.isTrue(~bin[0]));
00643 CPPUNIT_ASSERT_EQUAL(true, s.isTrue(bin[1]));
00644 }
00645
00646 void testEstimateBCP() {
00647 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00648 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00649 Literal c = posLit(ctx.addVar(Var_t::atom_var));
00650 Literal d = posLit(ctx.addVar(Var_t::atom_var));
00651 Literal e = posLit(ctx.addVar(Var_t::atom_var));
00652 Solver& s = ctx.startAddConstraints();
00653 ctx.addBinary(a, b);
00654 ctx.addBinary(~b, c);
00655 ctx.addBinary(~c, d);
00656 ctx.addBinary(~d, e);
00657 ctx.endInit();
00658 for (int i = 0; i < 4; ++i) {
00659 uint32 est = s.estimateBCP(~a, i);
00660 CPPUNIT_ASSERT_EQUAL(uint32(i + 2), est);
00661 }
00662 }
00663
00664 void testEstimateBCPLoop() {
00665 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00666 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00667 Literal c = posLit(ctx.addVar(Var_t::atom_var));
00668 Solver& s = ctx.startAddConstraints();
00669 ctx.addBinary(a, b);
00670 ctx.addBinary(~b, c);
00671 ctx.addBinary(~c, ~a);
00672 ctx.endInit();
00673 CPPUNIT_ASSERT_EQUAL(uint32(3), s.estimateBCP(~a, -1));
00674 }
00675
00676 void testAssertImmediate() {
00677 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00678 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00679 Literal d = posLit(ctx.addVar(Var_t::atom_var));
00680 Literal q = posLit(ctx.addVar(Var_t::atom_var));
00681 Literal f = posLit(ctx.addVar(Var_t::atom_var));
00682 Literal x = posLit(ctx.addVar(Var_t::atom_var));
00683 Literal z = posLit(ctx.addVar(Var_t::atom_var));
00684 Solver& s = ctx.startAddConstraints();
00685 s.strategy.initWatches = SolverStrategies::watch_first;
00686
00687 ClauseCreator cl(&s);
00688 cl.start().add(~z).add(d).end();
00689 cl.start().add(a).add(b).end();
00690 cl.start().add(a).add(~b).add(z).end();
00691 cl.start().add(a).add(~b).add(~z).add(d).end();
00692 cl.start().add(~b).add(~z).add(~d).add(q).end();
00693 cl.start().add(~q).add(f).end();
00694 cl.start().add(~f).add(~z).add(x).end();
00695 s.assume( ~a );
00696 CPPUNIT_ASSERT_EQUAL( true, s.propagate() );
00697
00698 CPPUNIT_ASSERT_EQUAL( 7u, s.numAssignedVars());
00699
00700 Antecedent whyB = s.reason(b);
00701 Antecedent whyZ = s.reason(z);
00702 Antecedent whyD = s.reason(d);
00703 Antecedent whyQ = s.reason(q);
00704 Antecedent whyF = s.reason(f);
00705 Antecedent whyX = s.reason(x);
00706
00707 CPPUNIT_ASSERT(whyB.type() == Antecedent::binary_constraint && whyB.firstLiteral() == ~a);
00708 CPPUNIT_ASSERT(whyZ.type() == Antecedent::ternary_constraint && whyZ.firstLiteral() == ~a && whyZ.secondLiteral() == b);
00709 CPPUNIT_ASSERT(whyD.type() == Antecedent::generic_constraint);
00710 CPPUNIT_ASSERT(whyQ.type() == Antecedent::generic_constraint);
00711
00712 CPPUNIT_ASSERT(whyF.type() == Antecedent::binary_constraint && whyF.firstLiteral() == q);
00713 CPPUNIT_ASSERT(whyX.type() == Antecedent::ternary_constraint && whyX.firstLiteral() == f && whyX.secondLiteral() == z);
00714 }
00715
00716 void testPreferShortBfs() {
00717 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00718 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00719 Literal p = posLit(ctx.addVar(Var_t::atom_var));
00720 Literal q = posLit(ctx.addVar(Var_t::atom_var));
00721 Literal x = posLit(ctx.addVar(Var_t::atom_var));
00722 Literal y = posLit(ctx.addVar(Var_t::atom_var));
00723 Literal z = posLit(ctx.addVar(Var_t::atom_var));
00724 Solver& s = ctx.startAddConstraints();
00725 s.strategy.initWatches = SolverStrategies::watch_least;
00726 ClauseCreator cl(&s);
00727 cl.start().add(a).add(x).add(y).add(p).end();
00728 cl.start().add(a).add(x).add(y).add(z).end();
00729 cl.start().add(a).add(p).end();
00730 cl.start().add(a).add(~p).add(z).end();
00731 cl.start().add(~z).add(b).end();
00732 cl.start().add(a).add(x).add(q).add(~b).end();
00733 cl.start().add(a).add(~b).add(~p).add(~q).end();
00734
00735 CPPUNIT_ASSERT_EQUAL(7u, s.numConstraints());
00736 CPPUNIT_ASSERT_EQUAL(2u, ctx.numBinary());
00737 CPPUNIT_ASSERT_EQUAL(1u, ctx.numTernary());
00738
00739 s.assume( ~x );
00740 s.propagate();
00741 s.assume( ~y );
00742 s.propagate();
00743 CPPUNIT_ASSERT_EQUAL(2u, s.numAssignedVars());
00744 s.assume( ~a );
00745
00746 CPPUNIT_ASSERT_EQUAL(false, s.propagate());
00747
00748 CPPUNIT_ASSERT_EQUAL( 7u, s.numAssignedVars());
00749
00750 CPPUNIT_ASSERT( s.reason(b).type() == Antecedent::binary_constraint );
00751 CPPUNIT_ASSERT( s.reason(p).type() == Antecedent::binary_constraint );
00752 CPPUNIT_ASSERT( s.reason(z).type() == Antecedent::ternary_constraint );
00753 CPPUNIT_ASSERT( s.reason(q).type() == Antecedent::generic_constraint );
00754 }
00755 void testPostPropInit() {
00756 TestingPostProp* p = new TestingPostProp(false);
00757 Solver& s = ctx.startAddConstraints();
00758 s.addPost(p);
00759 CPPUNIT_ASSERT_EQUAL(0, p->inits);
00760 ctx.endInit();
00761 CPPUNIT_ASSERT_EQUAL(1, p->inits);
00762 ctx.startAddConstraints();
00763 ctx.endInit();
00764 CPPUNIT_ASSERT_EQUAL(2, p->inits);
00765 }
00766 void testPropagateCallsPostProp() {
00767 TestingPostProp* p = new TestingPostProp(false);
00768 Solver& s = ctx.startAddConstraints();
00769 s.addPost(p);
00770 s.propagate();
00771 CPPUNIT_ASSERT_EQUAL(0, p->props);
00772 ctx.endInit();
00773 CPPUNIT_ASSERT_EQUAL(1, p->props);
00774 CPPUNIT_ASSERT_EQUAL(0, p->resets);
00775 }
00776 void testPropagateCallsResetOnConflict() {
00777 TestingPostProp* p = new TestingPostProp(true);
00778 Solver& s = ctx.startAddConstraints();
00779 s.addPost(p);
00780 ctx.endInit();
00781 CPPUNIT_ASSERT_EQUAL(1, p->props);
00782 CPPUNIT_ASSERT_EQUAL(1, p->resets);
00783 }
00784
00785 void testPostpropPriority() {
00786 TestingPostProp* p1 = new TestingPostProp(false);
00787 p1->prio += 10;
00788 TestingPostProp* p2 = new TestingPostProp(false);
00789 p2->prio += 30;
00790 TestingPostProp* p3 = new TestingPostProp(false);
00791 p3->prio += 20;
00792 Solver& s = ctx.startAddConstraints();
00793 s.addPost(p2);
00794 s.addPost(p1);
00795 s.addPost(p3);
00796 CPPUNIT_ASSERT(p1->next == p3 && p3->next == p2);
00797 }
00798
00799 void testPostpropPriorityExt() {
00800 TestingPostProp* p1 = new TestingPostProp(false);
00801 TestingPostProp* p2 = new TestingPostProp(false);
00802 TestingPostProp* p3 = new TestingPostProp(false);
00803 TestingPostProp* p4 = new TestingPostProp(false);
00804 p1->prio = 10;
00805 p2->prio = 20;
00806 p3->prio = PostPropagator::priority_class_general;
00807 p4->prio = PostPropagator::priority_class_general;
00808 Solver& s = ctx.startAddConstraints();
00809 s.addPost(p3);
00810 s.addPost(p2);
00811 CPPUNIT_ASSERT(s.getPost(PostPropagator::priority_class_general));
00812 CPPUNIT_ASSERT(s.getPost(20));
00813 CPPUNIT_ASSERT(p2->next == p3);
00814 s.addPost(p4);
00815 CPPUNIT_ASSERT(p2->next == p4);
00816 CPPUNIT_ASSERT(p4->next == p3);
00817 ctx.endInit();
00818 CPPUNIT_ASSERT(p3->inits == 1);
00819 p3->props = 0;
00820 p2->props = 0;
00821 p4->props = 0;
00822 s.removePost(p2);
00823 s.removePost(p4);
00824 s.addPost(p4);
00825 s.propagate();
00826 CPPUNIT_ASSERT(p3->props == 1 && p4->props == 1);
00827 s.addPost(p1);
00828 CPPUNIT_ASSERT(p1->next == p4);
00829 s.addPost(p2);
00830 CPPUNIT_ASSERT(p1->next == p2 && p2->next == p4);
00831 s.removePost(p3);
00832 s.removePost(p4);
00833 s.propagate();
00834 CPPUNIT_ASSERT(p3->props == 1 && p4->props == 1 && p1->props == 1 && p2->props == 1);
00835 s.addPost(p4);
00836 s.addPost(p3);
00837 p3->conflict = true;
00838 s.propagate();
00839 CPPUNIT_ASSERT(p3->props == 2 && p1->props == 2 && p2->props == 2 && p4->props == 1);
00840 }
00841
00842 void testPostpropRemove() {
00843 SingleOwnerPtr<TestingPostProp> p1(new TestingPostProp(false, 1));
00844 SingleOwnerPtr<TestingPostProp> p2(new TestingPostProp(false, 2));
00845 SingleOwnerPtr<TestingPostProp> p3(new TestingPostProp(false, 3));
00846 Solver& s = ctx.startAddConstraints();
00847 s.addPost(p1.release());
00848 s.addPost(p2.release());
00849 s.addPost(p3.release());
00850 CPPUNIT_ASSERT(p1->next == p2.get() && p2->next == p3.get());
00851 s.removePost(p2.acquire());
00852 CPPUNIT_ASSERT(p1->next == p3.get() && p3->next == 0 && p2->next == 0);
00853 s.removePost(p2.acquire());
00854 s.removePost(p3.acquire());
00855 CPPUNIT_ASSERT(p1->next == 0);
00856 ctx.endInit();
00857 CPPUNIT_ASSERT(p1->props == 1);
00858 }
00859
00860 void testPostpropRemoveOnProp() {
00861 TestingPostProp* p1 = new TestingPostProp(false);
00862 TestingPostProp* p2 = new TestingPostProp(false);
00863 TestingPostProp* p3 = new TestingPostProp(false);
00864 Solver& s = ctx.startAddConstraints();
00865 s.addPost(p1);
00866 s.addPost(p2);
00867 s.addPost(p3);
00868 ctx.endInit();
00869 p2->deleteOnProp = true;
00870 s.propagate();
00871 CPPUNIT_ASSERT(p1->props == 2 && p3->props == 2);
00872 }
00873
00874 void testPostpropBug() {
00875 Solver& s = ctx.startAddConstraints();
00876 SingleOwnerPtr<TestingPostProp> p1(new TestingPostProp(false));
00877 s.addPost(p1.release());
00878 ctx.endInit();
00879
00880 ctx.startAddConstraints();
00881 s.removePost(p1.get());
00882 p1.acquire();
00883 ctx.endInit();
00884 s.removePost(p1.get());
00885 CPPUNIT_ASSERT(p1->inits == 1);
00886 }
00887
00888 void testPostpropAddAfterInitBug() {
00889 Solver& s = ctx.startAddConstraints();
00890 SingleOwnerPtr<TestingPostProp> p1(new TestingPostProp(false));
00891 ctx.endInit();
00892 s.addPost(p1.release());
00893 CPPUNIT_ASSERT(p1->inits == 1);
00894 s.propagate();
00895 CPPUNIT_ASSERT(p1->props == 1);
00896 }
00897
00898 void testSimplifyRemovesSatBinClauses() {
00899 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00900 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00901 Literal c = posLit(ctx.addVar(Var_t::atom_var));
00902 Literal d = posLit(ctx.addVar(Var_t::atom_var));
00903 Solver& s = ctx.startAddConstraints();
00904 ctx.addBinary(a, b);
00905 ctx.addBinary(a, c);
00906 ctx.addBinary(~a, d);
00907 s.force(a, 0);
00908 s.simplify();
00909 CPPUNIT_ASSERT_EQUAL(0u, ctx.numBinary());
00910 }
00911
00912 void testSimplifyRemovesSatTernClauses() {
00913 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00914 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00915 Literal c = posLit(ctx.addVar(Var_t::atom_var));
00916 Literal d = posLit(ctx.addVar(Var_t::atom_var));
00917 Solver& s = ctx.startAddConstraints();
00918 ctx.addTernary(a, b, d);
00919 ctx.addTernary(~a, b, c);
00920 s.force(a, 0);
00921 s.simplify();
00922 s.assume(~b);
00923 CPPUNIT_ASSERT_EQUAL(0u, ctx.numTernary());
00924
00925
00926
00927 CPPUNIT_ASSERT_EQUAL(1u, ctx.numBinary());
00928 s.propagate();
00929 CPPUNIT_ASSERT_EQUAL(true, s.isTrue(c));
00930 }
00931
00932 void testSimplifyRemovesSatConstraints() {
00933 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00934 Solver& s = ctx.startAddConstraints();
00935 TestingConstraint* t1;
00936 TestingConstraint* t2;
00937 TestingConstraint* t3;
00938 TestingConstraint* t4;
00939 bool t2Del = false, t3Del = false;
00940 s.add( t1 = new TestingConstraint );
00941 s.add( t2 = new TestingConstraint(&t2Del) );
00942 ctx.endInit();
00943 s.addLearnt( t3 = new TestingConstraint(&t3Del, Constraint_t::learnt_conflict), TestingConstraint::size() );
00944 s.addLearnt( t4 = new TestingConstraint(0, Constraint_t::learnt_conflict), TestingConstraint::size() );
00945 t1->sat = false;
00946 t2->sat = true;
00947 t3->sat = true;
00948 t4->sat = false;
00949 CPPUNIT_ASSERT_EQUAL(2u, s.numLearntConstraints());
00950 CPPUNIT_ASSERT_EQUAL(2u, s.numLearntConstraints());
00951 s.force( a, 0 );
00952 s.simplify();
00953 CPPUNIT_ASSERT_EQUAL(1u, s.numLearntConstraints());
00954 CPPUNIT_ASSERT_EQUAL(1u, s.numLearntConstraints());
00955 CPPUNIT_ASSERT_EQUAL(true, t2Del);
00956 CPPUNIT_ASSERT_EQUAL(true, t3Del);
00957 }
00958
00959 void testRemoveConditional() {
00960 Var a = ctx.addVar( Var_t::atom_var );
00961 Var b = ctx.addVar( Var_t::atom_var );
00962 Var c = ctx.addVar( Var_t::atom_var );
00963 Solver& s = ctx.startAddConstraints();
00964 ctx.endInit();
00965 Literal tag = posLit(s.pushTagVar(false));
00966 ClauseCreator cc(&s);
00967 cc.start(Constraint_t::learnt_conflict).add(posLit(a)).add(posLit(b)).add(posLit(c)).add(~tag).end();
00968 CPPUNIT_ASSERT(s.numLearntConstraints() == 1);
00969 s.removeConditional();
00970 CPPUNIT_ASSERT(s.numLearntConstraints() == 0);
00971 }
00972
00973 void testStrengthenConditional() {
00974 Var a = ctx.addVar( Var_t::atom_var );
00975 Var b = ctx.addVar( Var_t::atom_var );
00976 Var c = ctx.addVar( Var_t::atom_var );
00977 Solver& s = ctx.startAddConstraints();
00978 ctx.endInit();
00979 ClauseCreator cc(&s);
00980 Literal tag = posLit(s.pushTagVar(false));
00981 cc.start(Constraint_t::learnt_conflict).add(posLit(a)).add(posLit(b)).add(posLit(c)).add(~tag).end();
00982 CPPUNIT_ASSERT(s.numLearntConstraints() == 1);
00983 s.strengthenConditional();
00984 CPPUNIT_ASSERT(ctx.numLearntShort() == 1 || ctx.numTernary() == 1);
00985 }
00986
00987 void testLearnConditional() {
00988 Var b = ctx.addVar( Var_t::atom_var );
00989 Solver& s = ctx.startAddConstraints();
00990 ctx.endInit();
00991 Literal tag = posLit(s.pushTagVar(true));
00992 s.assume(posLit(b));
00993 s.propagate();
00994 TestingConstraint* cfl = new TestingConstraint;
00995 cfl->ante.push_back(tag);
00996 cfl->ante.push_back(posLit(b));
00997 s.force(negLit(0), cfl);
00998 cfl->destroy(&s, true);
00999 s.resolveConflict();
01000 CPPUNIT_ASSERT(ctx.numLearntShort() == 0 && ctx.numBinary() == 0);
01001 CPPUNIT_ASSERT(s.numLearntConstraints() == 1 && s.decisionLevel() == 1);
01002 s.strengthenConditional();
01003 s.clearAssumptions();
01004 CPPUNIT_ASSERT(s.isTrue(negLit(b)));
01005 }
01006
01007 void testResolveUnary() {
01008 ctx.enableStats(1);
01009 Var a = ctx.addVar( Var_t::atom_var );
01010 Var b = ctx.addVar( Var_t::atom_var );
01011 Var c = ctx.addVar( Var_t::atom_var );
01012 Solver& s = ctx.startAddConstraints();
01013 ctx.addBinary(posLit(a), posLit(b));
01014 ctx.addBinary(negLit(b), posLit(c));
01015 ctx.addBinary(negLit(a), posLit(c));
01016 s.assume( negLit(c) );
01017 CPPUNIT_ASSERT_EQUAL(false, s.propagate());
01018 CPPUNIT_ASSERT_EQUAL(true, s.resolveConflict());
01019 CPPUNIT_ASSERT_EQUAL(false, s.hasConflict());
01020 CPPUNIT_ASSERT_EQUAL(true, s.isTrue(posLit(c)));
01021 CPPUNIT_ASSERT_EQUAL(0u, s.decisionLevel());
01022 CPPUNIT_ASSERT(s.stats.extra->learnts[Constraint_t::learnt_conflict-1] == 1);
01023 }
01024
01025 void testResolveConflict() {
01026 Literal x1 = posLit(ctx.addVar( Var_t::atom_var )); Literal x2 = posLit(ctx.addVar( Var_t::atom_var ));
01027 Literal x3 = posLit(ctx.addVar( Var_t::atom_var )); Literal x4 = posLit(ctx.addVar( Var_t::atom_var ));
01028 Literal x5 = posLit(ctx.addVar( Var_t::atom_var )); Literal x6 = posLit(ctx.addVar( Var_t::atom_var ));
01029 Literal x7 = posLit(ctx.addVar( Var_t::atom_var )); Literal x8 = posLit(ctx.addVar( Var_t::atom_var ));
01030 Literal x9 = posLit(ctx.addVar( Var_t::atom_var )); Literal x10 = posLit(ctx.addVar( Var_t::atom_var ));
01031 Literal x11 = posLit(ctx.addVar( Var_t::atom_var )); Literal x12 = posLit(ctx.addVar( Var_t::atom_var ));
01032 Literal x13 = posLit(ctx.addVar( Var_t::atom_var )); Literal x14 = posLit(ctx.addVar( Var_t::atom_var ));
01033 Literal x15 = posLit(ctx.addVar( Var_t::atom_var )); Literal x16 = posLit(ctx.addVar( Var_t::atom_var ));
01034 Literal x17 = posLit(ctx.addVar( Var_t::atom_var ));
01035 Solver& s = ctx.startAddConstraints();
01036 ClauseCreator cl(&s);
01037 cl.start().add(~x11).add(x12).end();
01038 cl.start().add(x1).add(~x12).add(~x13).end();
01039 cl.start().add(~x4).add(~x12).add(x14).end();
01040 cl.start().add(x13).add(~x14).add(~x15).end();
01041 cl.start().add(~x2).add(x15).add(x16).end();
01042 cl.start().add(x3).add(x15).add(~x17).end();
01043 cl.start().add(~x6).add(~x16).add(x17).end();
01044 cl.start().add(~x2).add(x9).add(x10).end();
01045 cl.start().add(~x4).add(~x7).add(~x8).end();
01046 cl.start().add(x5).add(x6).end();
01047 CPPUNIT_ASSERT_EQUAL(true, ctx.endInit());
01048 CPPUNIT_ASSERT_EQUAL(0u, s.queueSize());
01049
01050 CPPUNIT_ASSERT_EQUAL(true, s.assume(~x1) && s.propagate());
01051 CPPUNIT_ASSERT_EQUAL(true, s.assume(x2) && s.propagate());
01052 CPPUNIT_ASSERT_EQUAL(true, s.assume(~x3) && s.propagate());
01053 CPPUNIT_ASSERT_EQUAL(true, s.assume(x4) && s.propagate());
01054 CPPUNIT_ASSERT_EQUAL(true, s.assume(~x5) && s.propagate());
01055 CPPUNIT_ASSERT_EQUAL(true, s.assume(x7) && s.propagate());
01056 CPPUNIT_ASSERT_EQUAL(true, s.assume(~x9) && s.propagate());
01057
01058 CPPUNIT_ASSERT_EQUAL(false, s.assume(x11) && s.propagate());
01059
01060 CPPUNIT_ASSERT_EQUAL(true, s.resolveConflict());
01061 CPPUNIT_ASSERT_EQUAL(s.trail().back(), x15);
01062 CPPUNIT_ASSERT_EQUAL(5u, s.decisionLevel());
01063 CPPUNIT_ASSERT_EQUAL(Antecedent::generic_constraint, s.reason(s.trail().back()).type());
01064
01065 LitVec cflClause;
01066 s.reason(s.trail().back(), cflClause);
01067 cflClause.push_back(s.trail().back());
01068 CPPUNIT_ASSERT(LitVec::size_type(4) == cflClause.size());
01069 CPPUNIT_ASSERT(std::find(cflClause.begin(), cflClause.end(), x2) != cflClause.end());
01070 CPPUNIT_ASSERT(std::find(cflClause.begin(), cflClause.end(), ~x3) != cflClause.end());
01071 CPPUNIT_ASSERT(std::find(cflClause.begin(), cflClause.end(), x6) != cflClause.end());
01072 CPPUNIT_ASSERT(std::find(cflClause.begin(), cflClause.end(), x15) != cflClause.end());
01073 }
01074
01075 void testResolveConflictBounded() {
01076 Literal x1 = posLit(ctx.addVar( Var_t::atom_var )); Literal x2 = posLit(ctx.addVar( Var_t::atom_var ));
01077 Literal x3 = posLit(ctx.addVar( Var_t::atom_var )); Literal x4 = posLit(ctx.addVar( Var_t::atom_var ));
01078 Literal x5 = posLit(ctx.addVar( Var_t::atom_var )); Literal x6 = posLit(ctx.addVar( Var_t::atom_var ));
01079 Literal x7 = posLit(ctx.addVar( Var_t::atom_var )); Literal x8 = posLit(ctx.addVar( Var_t::atom_var ));
01080 Literal x9 = posLit(ctx.addVar( Var_t::atom_var )); Literal x10 = posLit(ctx.addVar( Var_t::atom_var ));
01081 Literal x11 = posLit(ctx.addVar( Var_t::atom_var )); Literal x12 = posLit(ctx.addVar( Var_t::atom_var ));
01082 Literal x13 = posLit(ctx.addVar( Var_t::atom_var )); Literal x14 = posLit(ctx.addVar( Var_t::atom_var ));
01083 Literal x15 = posLit(ctx.addVar( Var_t::atom_var )); Literal x16 = posLit(ctx.addVar( Var_t::atom_var ));
01084 Literal x17 = posLit(ctx.addVar( Var_t::atom_var )); Literal x18 = posLit(ctx.addVar( Var_t::atom_var ));
01085 Solver& s = ctx.startAddConstraints();
01086 ClauseCreator cl(&s);
01087 cl.start().add(~x11).add(x12).end();
01088 cl.start().add(x1).add(~x12).add(~x13).end();
01089 cl.start().add(~x4).add(~x12).add(x14).end();
01090 cl.start().add(x13).add(~x14).add(~x15).end();
01091 cl.start().add(~x2).add(x15).add(x16).end();
01092 cl.start().add(x3).add(x15).add(~x17).end();
01093 cl.start().add(~x6).add(~x16).add(x17).end();
01094 cl.start().add(~x2).add(x9).add(x10).end();
01095 cl.start().add(~x4).add(~x7).add(~x8).end();
01096 cl.start().add(x5).add(x6).end();
01097 CPPUNIT_ASSERT_EQUAL(true, ctx.endInit());
01098 CPPUNIT_ASSERT_EQUAL(0u, s.queueSize());
01099
01100 CPPUNIT_ASSERT_EQUAL(true, s.assume(~x1) && s.propagate());
01101 CPPUNIT_ASSERT_EQUAL(true, s.assume(x2) && s.propagate());
01102 CPPUNIT_ASSERT_EQUAL(true, s.assume(~x3) && s.propagate());
01103 CPPUNIT_ASSERT_EQUAL(true, s.assume(x4) && s.propagate());
01104 CPPUNIT_ASSERT_EQUAL(true, s.assume(~x5) && s.propagate());
01105 CPPUNIT_ASSERT_EQUAL(true, s.assume(x7) && s.propagate());
01106
01107
01108 CPPUNIT_ASSERT_EQUAL(true, s.assume(x18) && s.propagate());
01109 CPPUNIT_ASSERT_EQUAL(true, s.backtrack());
01110
01111 CPPUNIT_ASSERT_EQUAL(true, s.assume(~x9) && s.propagate());
01112 CPPUNIT_ASSERT_EQUAL(false, s.assume(x11) && s.propagate());
01113
01114 CPPUNIT_ASSERT_EQUAL(true, s.resolveConflict());
01115 CPPUNIT_ASSERT_EQUAL(s.trail().back(), x15);
01116 CPPUNIT_ASSERT_EQUAL(6u, s.decisionLevel());
01117 Antecedent ante = s.reason(s.trail().back());
01118 CPPUNIT_ASSERT_EQUAL(Antecedent::generic_constraint, ante.type());
01119 ClauseHead* cflClause = (ClauseHead*)ante.constraint();
01120 LitVec r;
01121 cflClause->reason(s, s.trail().back(), r);
01122 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), x2) != r.end());
01123 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), ~x3) != r.end());
01124 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), x6) != r.end());
01125
01126 CPPUNIT_ASSERT_EQUAL(true, s.hasWatch(x6, cflClause));
01127
01128 CPPUNIT_ASSERT_EQUAL(true, s.backtrack());
01129 CPPUNIT_ASSERT_EQUAL(true, s.isTrue(x15));
01130 CPPUNIT_ASSERT_EQUAL(true, s.backtrack());
01131 CPPUNIT_ASSERT_EQUAL(value_free, s.value(x15.var()));
01132 }
01133
01134 void testSearchKeepsAssumptions() {
01135 Var a = ctx.addVar( Var_t::atom_var );
01136 Var b = ctx.addVar( Var_t::atom_var );
01137 Var c = ctx.addVar( Var_t::atom_var );
01138 Var d = ctx.addVar( Var_t::atom_var );
01139 Solver& s = ctx.startAddConstraints();
01140 ClauseCreator cl(&s);
01141 ctx.addBinary(posLit(a), posLit(b));
01142 ctx.addBinary(negLit(b), posLit(c));
01143 ctx.addBinary(negLit(a), posLit(c));
01144 ctx.addBinary(negLit(c), negLit(d));
01145 ctx.endInit();
01146 s.simplify();
01147 s.assume( posLit(d) );
01148 s.pushRootLevel();
01149 CPPUNIT_ASSERT_EQUAL(value_false, s.search(-1, -1, 0));
01150 CPPUNIT_ASSERT_EQUAL(1u, s.decisionLevel());
01151 }
01152 void testSearchAddsLearntFacts() {
01153 Var a = ctx.addVar( Var_t::atom_var );
01154 Var b = ctx.addVar( Var_t::atom_var );
01155 Var c = ctx.addVar( Var_t::atom_var );
01156 Var d = ctx.addVar( Var_t::atom_var );
01157 struct Dummy : public DecisionHeuristic {
01158 Dummy(Literal first, Literal second) {lit_[0] = first; lit_[1] = second;}
01159 void updateVar(const Solver&, Var, uint32) {}
01160 Literal doSelect(Solver& s) {
01161 for (uint32 i = 0; i < 2; ++i) {
01162 if (s.value(lit_[i].var()) == value_free) {
01163 return lit_[i];
01164 }
01165 }
01166 return Literal();
01167 }
01168 Literal lit_[2];
01169 }*h = new Dummy(negLit(c),negLit(a));
01170 ctx.master()->heuristic().reset(h);
01171 Solver& s = ctx.startAddConstraints();
01172 ClauseCreator cl(&s);
01173 ctx.addBinary(posLit(a), posLit(b));
01174 ctx.addBinary(negLit(b), posLit(c));
01175 ctx.addBinary(negLit(a), posLit(c));
01176 ctx.endInit();
01177 s.assume( posLit(d) );
01178 s.pushRootLevel();
01179 CPPUNIT_ASSERT_EQUAL(value_true, s.search(-1, -1, 0));
01180 s.clearAssumptions();
01181 CPPUNIT_ASSERT_EQUAL(0u, s.decisionLevel());
01182 CPPUNIT_ASSERT(s.isTrue(posLit(c)));
01183 }
01184
01185 void testSearchMaxConflicts() {
01186 Var a = ctx.addVar( Var_t::atom_var );
01187 Var b = ctx.addVar( Var_t::atom_var );
01188 Var c = ctx.addVar( Var_t::atom_var );
01189 ctx.addVar( Var_t::atom_var );
01190 Solver& s = ctx.startAddConstraints();
01191 ctx.addBinary(posLit(a), negLit(b));
01192 ctx.addBinary(negLit(a), posLit(b));
01193 ctx.addBinary(negLit(a), negLit(b));
01194 ctx.endInit();
01195 s.simplify();
01196 s.assume(posLit(c));
01197 s.pushRootLevel();
01198 s.assume(posLit(a));
01199 CPPUNIT_ASSERT_EQUAL(value_free, s.search(1, -1, 0));
01200 CPPUNIT_ASSERT_EQUAL(1u, s.decisionLevel());
01201 }
01202
01203 void testClearAssumptions() {
01204 Var a = ctx.addVar( Var_t::atom_var );
01205 Var b = ctx.addVar( Var_t::atom_var );
01206 ctx.addVar( Var_t::atom_var );
01207 Solver& s = ctx.startAddConstraints();
01208 ctx.addBinary(negLit(a), negLit(b));
01209 ctx.addBinary(negLit(a), posLit(b));
01210 ctx.endInit();
01211 s.assume(posLit(a));
01212 s.pushRootLevel();
01213 CPPUNIT_ASSERT_EQUAL(false, s.propagate());
01214 CPPUNIT_ASSERT_EQUAL(true, s.clearAssumptions());
01215 CPPUNIT_ASSERT_EQUAL(0u, s.decisionLevel());
01216
01217 s.force(posLit(a), 0);
01218 CPPUNIT_ASSERT_EQUAL(false, s.propagate());
01219 CPPUNIT_ASSERT_EQUAL(false, s.clearAssumptions());
01220 }
01221
01222 void testStopConflict() {
01223 Var a = ctx.addVar( Var_t::atom_var );
01224 Var b = ctx.addVar( Var_t::atom_var );
01225 Var c = ctx.addVar( Var_t::atom_var );
01226 Var d = ctx.addVar( Var_t::atom_var );
01227 Solver& s = ctx.startAddConstraints();
01228 ctx.addBinary(negLit(a), negLit(b));
01229 ctx.addBinary(negLit(a), posLit(b));
01230 ctx.endInit();
01231 s.assume(posLit(a)) && !s.propagate() && s.resolveConflict();
01232 CPPUNIT_ASSERT(s.decisionLevel() == 0 && s.queueSize() == 1 && !s.hasConflict());
01233 s.setStopConflict();
01234 CPPUNIT_ASSERT(s.hasConflict() && !s.resolveConflict());
01235 s.clearStopConflict();
01236 CPPUNIT_ASSERT(s.decisionLevel() == 0 && s.queueSize() == 1 && !s.hasConflict());
01237 s.propagate();
01238 s.assume(posLit(c)) && s.propagate();
01239 s.pushRootLevel(1);
01240 CPPUNIT_ASSERT(s.rootLevel() == 1);
01241 s.assume(posLit(d));
01242 s.setStopConflict();
01243 CPPUNIT_ASSERT(s.rootLevel() == 2);
01244 s.clearStopConflict();
01245 CPPUNIT_ASSERT(s.rootLevel() == 1 && s.queueSize() == 1);
01246 }
01247
01248 void testStats() {
01249 ProblemStats p1, p2;
01250 CPPUNIT_ASSERT_EQUAL(uint32(0), p1.vars);
01251 CPPUNIT_ASSERT_EQUAL(uint32(0), p2.vars_eliminated);
01252 CPPUNIT_ASSERT_EQUAL(uint32(0), p1.constraints);
01253 CPPUNIT_ASSERT_EQUAL(uint32(0), p2.constraints_binary);
01254 CPPUNIT_ASSERT_EQUAL(uint32(0), p2.constraints_ternary);
01255
01256 p1.vars = 100; p2.vars = 150;
01257 p1.vars_eliminated = 20; p2.vars_eliminated = 30;
01258 p1.constraints = 150; p2.constraints = 150;
01259 p1.constraints_binary = 0; p2.constraints_binary = 100;
01260 p1.constraints_ternary= 100; p2.constraints_ternary= 0;
01261 p1.diff(p2);
01262
01263 CPPUNIT_ASSERT_EQUAL(uint32(50), p1.vars);
01264 CPPUNIT_ASSERT_EQUAL(uint32(10), p1.vars_eliminated);
01265 CPPUNIT_ASSERT_EQUAL(uint32(0), p1.constraints);
01266 CPPUNIT_ASSERT_EQUAL(uint32(100),p1.constraints_binary);
01267 CPPUNIT_ASSERT_EQUAL(uint32(100),p1.constraints_ternary);
01268
01269 SolverStats st, st2;
01270 st.enableExtended();
01271 st2.enableExtended();
01272
01273 st.conflicts = 12; st2.conflicts = 3;
01274 st.choices = 100;st2.choices = 99;
01275 st.restarts = 7; st2.restarts = 8;
01276
01277 st.extra->models = 10; st2.extra->models = 2;
01278 st.extra->learnts[0] = 6; st2.extra->learnts[0] = 4;
01279 st.extra->learnts[1] = 5; st2.extra->learnts[1] = 4;
01280 st.extra->lits[0] = 15; st2.extra->lits[0] = 14;
01281 st.extra->lits[1] = 5; st2.extra->lits[1] = 4;
01282 st.extra->binary = 6; st2.extra->ternary = 5;
01283 st.extra->deleted = 10;
01284
01285 st.accu(st2);
01286
01287 CPPUNIT_ASSERT_EQUAL(uint64(15), st.conflicts);
01288 CPPUNIT_ASSERT_EQUAL(uint64(199),st.choices);
01289 CPPUNIT_ASSERT_EQUAL(uint64(15),st.restarts);
01290 CPPUNIT_ASSERT_EQUAL(uint64(12), st.extra->models);
01291 CPPUNIT_ASSERT_EQUAL(uint64(29),st.extra->lits[0]);
01292 CPPUNIT_ASSERT_EQUAL(uint64(9),st.extra->lits[1]);
01293 CPPUNIT_ASSERT_EQUAL(uint64(10),st.extra->learnts[0]);
01294 CPPUNIT_ASSERT_EQUAL(uint64(9),st.extra->learnts[1]);
01295 CPPUNIT_ASSERT_EQUAL(uint32(6),st.extra->binary);
01296 CPPUNIT_ASSERT_EQUAL(uint32(5),st.extra->ternary);
01297 CPPUNIT_ASSERT_EQUAL(uint64(10),st.extra->deleted);
01298 }
01299
01300
01301 void testLearntShort() {
01302 Literal a = posLit(ctx.addVar( Var_t::atom_var ));
01303 Literal b = posLit(ctx.addVar( Var_t::atom_var ));
01304 Literal c = posLit(ctx.addVar( Var_t::atom_var ));
01305 Literal d = posLit(ctx.addVar( Var_t::atom_var ));
01306 ctx.setShareMode(ContextParams::share_problem);
01307 ctx.setConcurrency(2);
01308 Solver& s = ctx.startAddConstraints();
01309 ctx.addBinary(c, d);
01310 ctx.endInit();
01311 ClauseCreator cc(&s);
01312 CPPUNIT_ASSERT(cc.start(Constraint_t::learnt_conflict).add(a).add(b).end());
01313 CPPUNIT_ASSERT(cc.start(Constraint_t::learnt_conflict).add(~a).add(~b).add(c).end());
01314 CPPUNIT_ASSERT(ctx.numLearntShort() == 2);
01315 CPPUNIT_ASSERT(ctx.numBinary() == 1);
01316 CPPUNIT_ASSERT(ctx.numTernary() == 0);
01317
01318 cc.start(Constraint_t::learnt_conflict).add(a).add(b).add(c).end();
01319
01320 CPPUNIT_ASSERT(ctx.numLearntShort() == 2);
01321
01322 s.assume(~b);
01323 s.propagate();
01324 CPPUNIT_ASSERT(s.isTrue(a) && s.reason(a).firstLiteral() == ~b);
01325 s.undoUntil(0);
01326 s.assume(a);
01327 s.propagate();
01328 s.assume(b);
01329 s.propagate();
01330 CPPUNIT_ASSERT(s.isTrue(c));
01331 LitVec res;
01332 s.reason(c, res);
01333 CPPUNIT_ASSERT(std::find(res.begin(), res.end(), a) != res.end());
01334 CPPUNIT_ASSERT(std::find(res.begin(), res.end(), b) != res.end());
01335 }
01336
01337 void testLearntShortAreDistributed() {
01338 Literal a = posLit(ctx.addVar( Var_t::atom_var ));
01339 Literal b = posLit(ctx.addVar( Var_t::atom_var ));
01340 Literal c = posLit(ctx.addVar( Var_t::atom_var ));
01341 Literal d = posLit(ctx.addVar( Var_t::atom_var ));
01342 struct Dummy : public Distributor {
01343 Dummy() : Distributor(Policy(UINT32_MAX, UINT32_MAX, UINT32_MAX)), unary(0), binary(0), ternary(0) {}
01344 void publish(const Solver&, SharedLiterals* lits) {
01345 uint32 size = lits->size();
01346 unary += size == 1;
01347 binary += size == 2;
01348 ternary += size == 3;
01349 shared.push_back(lits);
01350 }
01351 uint32 receive(const Solver&, SharedLiterals** out, uint32 num) {
01352 uint32 r = 0;
01353 while (!shared.empty() && num--) {
01354 out[r++] = shared.back();
01355 shared.pop_back();
01356 }
01357 return r;
01358 }
01359 uint32 unary;
01360 uint32 binary;
01361 uint32 ternary;
01362 PodVector<SharedLiterals*>::type shared;
01363 }* dummy;
01364 ctx.distributor.reset(dummy = new Dummy());
01365 ctx.setConcurrency(2);
01366 Solver& s = ctx.startAddConstraints();
01367 ctx.endInit();
01368 LitVec lits; lits.resize(2);
01369 lits[0] = a; lits[1] = b;
01370 ClauseCreator::create(s, lits, 0, ClauseInfo(Constraint_t::learnt_conflict));
01371 lits.resize(3);
01372 lits[0] = ~a; lits[1] = ~b; lits[2] = ~c;
01373 ClauseCreator::create(s, lits, 0, ClauseInfo(Constraint_t::learnt_loop));
01374 lits.resize(1);
01375 lits[0] = d;
01376 ClauseCreator::create(s, lits, 0, ClauseInfo(Constraint_t::learnt_conflict));
01377 CPPUNIT_ASSERT(dummy->unary == 1);
01378 CPPUNIT_ASSERT(dummy->binary == 1);
01379 CPPUNIT_ASSERT(dummy->ternary == 1);
01380 SharedLiterals* rec[3];
01381 CPPUNIT_ASSERT(dummy->receive(s, rec, 3) == 3);
01382 CPPUNIT_ASSERT(ClauseCreator::integrate(s, rec[0], 0).ok() == true);
01383 CPPUNIT_ASSERT(ClauseCreator::integrate(s, rec[1], 0).ok() == true);
01384 CPPUNIT_ASSERT(ClauseCreator::integrate(s, rec[2], 0).ok() == true);
01385 }
01386
01387 void testAuxAreNotDistributed() {
01388 Literal a = posLit(ctx.addVar( Var_t::atom_var ));
01389 Literal b = posLit(ctx.addVar( Var_t::atom_var ));
01390 Literal c = posLit(ctx.addVar( Var_t::atom_var ));
01391 Literal d = posLit(ctx.addVar( Var_t::atom_var ));
01392 struct Dummy : public Distributor {
01393 Dummy() : Distributor(Policy(UINT32_MAX, UINT32_MAX, UINT32_MAX)) {}
01394 void publish(const Solver&, SharedLiterals* lits) {
01395 shared.push_back(lits);
01396 }
01397 uint32 receive(const Solver&, SharedLiterals**, uint32) { return 0; }
01398 PodVector<SharedLiterals*>::type shared;
01399 }* dummy;
01400 ctx.distributor.reset(dummy = new Dummy());
01401 ctx.setConcurrency(2);
01402 Solver& s = ctx.startAddConstraints();
01403 ctx.endInit();
01404 Var aux = s.pushAuxVar();
01405
01406 LitVec lits; lits.resize(2);
01407 lits[0] = a; lits[1] = posLit(aux);
01408 ClauseCreator::create(s, lits, 0, ClauseInfo(Constraint_t::learnt_conflict));
01409 lits.resize(4);
01410 lits[0] = ~a; lits[1] = posLit(aux); lits[2] = b; lits[3] = c;
01411 ClauseCreator::create(s, lits, 0, ClauseInfo(Constraint_t::learnt_conflict));
01412 CPPUNIT_ASSERT(s.numLearntConstraints() == 2);
01413 CPPUNIT_ASSERT(dummy->shared.empty());
01414 CPPUNIT_ASSERT(s.getLearnt(0).simplify(s, false) == false);
01415 s.pushRoot(posLit(aux));
01416 s.pushRoot(a);
01417 lits.clear();
01418 s.copyGuidingPath(lits);
01419 CPPUNIT_ASSERT(lits.size() == 1 && lits[0] == a);
01420 s.clearAssumptions();
01421 lits.resize(4);
01422 lits[0] = ~a; lits[1] = posLit(aux); lits[2] = ~b; lits[3] = c;
01423 ClauseCreator::create(s, lits, 0, ClauseInfo(Constraint_t::learnt_conflict));
01424 s.assume(a) && s.propagate();
01425 s.assume(negLit(aux)) && s.propagate();
01426 s.assume(~c) && s.propagate();
01427 CPPUNIT_ASSERT(s.hasConflict());
01428 s.resolveConflict();
01429 CPPUNIT_ASSERT(s.numLearntConstraints() == 4);
01430 CPPUNIT_ASSERT(dummy->shared.empty());
01431 CPPUNIT_ASSERT(s.sharedContext()->numTernary() + s.sharedContext()->numBinary() == 0);
01432 }
01433
01434 void testAttachToDB() {
01435 Literal a = posLit(ctx.addVar( Var_t::atom_var ));
01436 Literal b = posLit(ctx.addVar( Var_t::atom_var ));
01437 Literal c = posLit(ctx.addVar( Var_t::atom_var ));
01438 Literal d = posLit(ctx.addVar( Var_t::atom_var ));
01439 ctx.setConcurrency(2);
01440 Solver& s = ctx.startAddConstraints();
01441 ClauseCreator cc(&s);
01442 cc.start().add(a).add(b).add(c).add(d).end();
01443 Solver& s2 = ctx.addSolver();
01444 ctx.endInit();
01445 ctx.attach(s2);
01446 CPPUNIT_ASSERT(s2.numConstraints() == 1);
01447 ctx.unfreeze();
01448 Literal e = posLit(ctx.addVar( Var_t::atom_var ));
01449 Literal f = posLit(ctx.addVar( Var_t::atom_var ));
01450 Literal g = posLit(ctx.addVar( Var_t::atom_var ));
01451 Literal h = posLit(ctx.addVar( Var_t::atom_var ));
01452 ctx.startAddConstraints();
01453 cc.start().add(e).add(f).add(g).add(h).end();
01454 cc.start().add(a).end();
01455 ctx.endInit();
01456 CPPUNIT_ASSERT(s.numConstraints() == 1);
01457 ctx.attach(s2);
01458 CPPUNIT_ASSERT(s2.numConstraints() == 1);
01459 s2.assume(~e) && s2.propagate();
01460 s2.assume(~f) && s2.propagate();
01461 s2.assume(~g) && s2.propagate();
01462 CPPUNIT_ASSERT(s2.isTrue(h));
01463 }
01464
01465 void testAttachDeferred() {
01466 Literal a = posLit(ctx.addVar( Var_t::atom_var ));
01467 Literal b = posLit(ctx.addVar( Var_t::atom_var ));
01468 Literal c = posLit(ctx.addVar( Var_t::atom_var ));
01469 Literal d = posLit(ctx.addVar( Var_t::atom_var ));
01470 ctx.setConcurrency(2);
01471 Solver& s = ctx.startAddConstraints();
01472 ClauseCreator cc(&s);
01473 cc.start().add(a).add(b).add(c).add(d).end();
01474 Solver& s2= ctx.addSolver();
01475 ctx.endInit(true);
01476 CPPUNIT_ASSERT(s2.numConstraints() == 1);
01477 ctx.unfreeze();
01478 ctx.startAddConstraints();
01479 cc.start().add(~a).add(~b).add(c).add(d).end();
01480 ctx.endInit(false);
01481 CPPUNIT_ASSERT(s.numConstraints() == 2);
01482 CPPUNIT_ASSERT(s2.numConstraints() == 1);
01483 ctx.unfreeze();
01484 ctx.startAddConstraints();
01485 cc.start().add(a).add(b).add(~c).add(~d).end();
01486 ctx.endInit(true);
01487 CPPUNIT_ASSERT(s.numConstraints() == 3);
01488 CPPUNIT_ASSERT(s2.numConstraints() == 3);
01489 }
01490
01491 void testUnfortunateSplitSeq() {
01492 Literal a = posLit(ctx.addVar( Var_t::atom_var ));
01493 Literal b = posLit(ctx.addVar( Var_t::atom_var ));
01494 Literal c = posLit(ctx.addVar( Var_t::atom_var ));
01495 Literal d = posLit(ctx.addVar( Var_t::atom_var ));
01496 ctx.setConcurrency(2);
01497 Solver& s = ctx.startAddConstraints();
01498 Solver& s2= ctx.addSolver();
01499 ctx.endInit(true);
01500
01501 s.assume(a) && s.propagate();
01502
01503 s.backtrack() && s.propagate();
01504
01505 s.assume(b) && s.propagate();
01506
01507 LitVec sGp;
01508 s.copyGuidingPath(sGp);
01509
01510 sGp.push_back(~b);
01511 s.pushRootLevel();
01512 integrateGp(s2, sGp);
01513 sGp.pop_back();
01514 s.clearAssumptions();
01515
01516 LitVec s2Gp;
01517
01518 s2.assume(c)&& s.propagate();
01519 s2.copyGuidingPath(s2Gp);
01520 s.pushRootLevel();
01521 s2Gp.push_back(~c);
01522 integrateGp(s, s2Gp);
01523 s2.clearAssumptions();
01524 s2Gp.clear();
01525
01526 s.assume(d)&& s.propagate();
01527 sGp.clear();
01528 s.copyGuidingPath(sGp);
01529
01530 integrateGp(s2, sGp);
01531 CPPUNIT_ASSERT(s2.isTrue(~a));
01532 }
01533
01534 void testSplitInc() {
01535 Literal a = posLit(ctx.addVar( Var_t::atom_var ));
01536 Literal b = posLit(ctx.addVar( Var_t::atom_var ));
01537 Literal c = posLit(ctx.addVar( Var_t::atom_var ));
01538 Literal d = posLit(ctx.addVar( Var_t::atom_var ));
01539 Solver& s = ctx.startAddConstraints();
01540 ctx.endInit();
01541 s.assume(a) && s.propagate();
01542 s.assume(b) && s.propagate();
01543 s.assume(c) && s.propagate();
01544 s.assume(d) && s.propagate();
01545 LitVec gp;
01546 s.copyGuidingPath(gp);
01547 s.pushRootLevel();
01548 gp.push_back(~a);
01549 CPPUNIT_ASSERT(gp.size() == 1 && gp[0] == ~a && s.rootLevel() == 1);
01550 gp.pop_back();
01551
01552 s.copyGuidingPath(gp);
01553 s.pushRootLevel();
01554 gp.push_back(~b);
01555 CPPUNIT_ASSERT(gp.size() == 2 && gp[1] == ~b && s.rootLevel() == 2);
01556 gp.pop_back();
01557
01558 s.copyGuidingPath(gp);
01559 s.pushRootLevel();
01560 gp.push_back(~c);
01561 CPPUNIT_ASSERT(gp.size() == 3 && gp[2] == ~c && s.rootLevel() == 3);
01562 gp.pop_back();
01563 }
01564
01565 void testSplitFlipped() {
01566 Literal a = posLit(ctx.addVar( Var_t::atom_var ));
01567 Literal b = posLit(ctx.addVar( Var_t::atom_var ));
01568 Literal c = posLit(ctx.addVar( Var_t::atom_var ));
01569 Literal d = posLit(ctx.addVar( Var_t::atom_var ));
01570 Solver& s = ctx.startAddConstraints();
01571 ctx.endInit();
01572
01573 LitVec gp;
01574
01575 s.assume(a) && s.propagate();
01576 s.pushRootLevel();
01577 s.assume(b) && s.propagate();
01578 s.backtrack();
01579
01580 s.assume(c) && s.propagate();
01581 s.backtrack();
01582
01583 s.assume(d) && s.propagate();
01584 s.copyGuidingPath(gp);
01585 CPPUNIT_ASSERT(std::find(gp.begin(), gp.end(), ~b) != gp.end());
01586 CPPUNIT_ASSERT(std::find(gp.begin(), gp.end(), ~c) != gp.end());
01587 }
01588
01589 void testSplitFlipToNewRoot() {
01590 Literal a = posLit(ctx.addVar( Var_t::atom_var ));
01591 Literal b = posLit(ctx.addVar( Var_t::atom_var ));
01592 Literal c = posLit(ctx.addVar( Var_t::atom_var ));
01593 Literal d = posLit(ctx.addVar( Var_t::atom_var ));
01594 Solver& s = ctx.startAddConstraints();
01595 ctx.endInit();
01596
01597 LitVec gp;
01598 s.assume(a) && s.propagate();
01599 s.copyGuidingPath(gp);
01600 s.pushRootLevel();
01601
01602 s.assume(b) && s.propagate();
01603 s.assume(c) && s.propagate();
01604
01605 s.backtrack();
01606
01607 s.copyGuidingPath(gp);
01608 s.pushRootLevel();
01609 CPPUNIT_ASSERT(s.rootLevel() == s.backtrackLevel());
01610 s.assume(d) && s.propagate();
01611 s.copyGuidingPath(gp);
01612 s.pushRootLevel();
01613 CPPUNIT_ASSERT(std::find(gp.begin(), gp.end(), ~c) != gp.end());
01614 }
01615
01616 void testSplitImplied() {
01617 Literal a = posLit(ctx.addVar( Var_t::atom_var ));
01618 Literal b = posLit(ctx.addVar( Var_t::atom_var ));
01619 Literal c = posLit(ctx.addVar( Var_t::atom_var ));
01620 Literal d = posLit(ctx.addVar( Var_t::atom_var ));
01621 Literal e = posLit(ctx.addVar( Var_t::atom_var ));
01622 Literal f = posLit(ctx.addVar( Var_t::atom_var ));
01623 Solver& s = ctx.startAddConstraints();
01624 ctx.endInit();
01625
01626 s.assume(a) && s.propagate();
01627 s.assume(b) && s.propagate();
01628 s.pushRootLevel(2);
01629
01630 s.assume(c);
01631 s.setBacktrackLevel(s.decisionLevel());
01632 SingleOwnerPtr<TestingConstraint> x( new TestingConstraint );
01633 s.force(~d, 2, x.get());
01634
01635 LitVec gp;
01636 s.copyGuidingPath(gp);
01637
01638 CPPUNIT_ASSERT(std::find(gp.begin(), gp.end(), ~d) != gp.end());
01639 s.pushRootLevel();
01640 s.assume(e);
01641 s.setBacktrackLevel(s.decisionLevel());
01642 s.force(~f, 2, x.get());
01643
01644 s.copyGuidingPath(gp);
01645 CPPUNIT_ASSERT(std::find(gp.begin(), gp.end(), ~f) != gp.end());
01646 }
01647
01648 void testAddShortIncremental() {
01649 Literal a = posLit(ctx.addVar( Var_t::atom_var ));
01650 Literal b = posLit(ctx.addVar( Var_t::atom_var ));
01651 ctx.setConcurrency(2);
01652 ctx.startAddConstraints();
01653 ctx.addBinary(a, b);
01654 ctx.endInit();
01655 CPPUNIT_ASSERT(ctx.numBinary() == 1);
01656 ctx.startAddConstraints();
01657 ctx.addBinary(~a, ~b);
01658 ctx.endInit();
01659 CPPUNIT_ASSERT(ctx.numBinary() == 2);
01660 }
01661
01662 void testSwitchToMtIncremental() {
01663 Literal a = posLit(ctx.addVar( Var_t::atom_var ));
01664 Literal b = posLit(ctx.addVar( Var_t::atom_var ));
01665 Literal c = posLit(ctx.addVar( Var_t::atom_var ));
01666 Literal d = posLit(ctx.addVar( Var_t::atom_var ));
01667 Solver& s = ctx.startAddConstraints();
01668 ClauseCreator cl(&s);
01669 cl.start().add(a).add(b).add(c).add(d).end();
01670 ctx.endInit(true);
01671 CPPUNIT_ASSERT(s.numVars() == 4 && s.numConstraints() == 1);
01672 ctx.unfreeze();
01673 Solver& s2 = ctx.addSolver();
01674 CPPUNIT_ASSERT(ctx.concurrency() == 2);
01675 ctx.startAddConstraints();
01676 cl.start().add(~a).add(~b).add(~c).add(~d).end();
01677 ctx.endInit(true);
01678 CPPUNIT_ASSERT(s.numVars() == 4 && s.numConstraints() == 2);
01679 CPPUNIT_ASSERT(s2.numVars() == 4 && s2.numConstraints() == 2);
01680 }
01681
01682 void testScheduleAdvance() {
01683 ScheduleStrategy r1 = ScheduleStrategy::geom(100,1.5,13);
01684 for (uint32 i = 0, m = (1u << 15)-1; i != m; ++i, r1.next()) {
01685 ScheduleStrategy r2 = ScheduleStrategy::geom(100,1.5,13);
01686 r2.advanceTo(i);
01687 CPPUNIT_ASSERT(r1.idx == r2.idx && r1.len == r2.len);
01688 }
01689 }
01690 void testLubyAdvance() {
01691 ScheduleStrategy r1 = ScheduleStrategy::luby(64,10);
01692 for (uint32 i = 0, m = (1u << 15)-1; i != m; ++i, r1.next()) {
01693 ScheduleStrategy r2 = ScheduleStrategy::luby(64,10);
01694 r2.advanceTo(i);
01695 CPPUNIT_ASSERT(r1.idx == r2.idx && r1.len == r2.len);
01696 }
01697 }
01698 void testPushAux() {
01699 Literal a = posLit(ctx.addVar(Var_t::atom_var));
01700 Literal b = posLit(ctx.addVar(Var_t::atom_var));
01701 Solver& s = ctx.startAddConstraints();
01702 ctx.endInit();
01703 CPPUNIT_ASSERT(s.numVars() == s.sharedContext()->numVars());
01704
01705 Var aux = s.pushAuxVar();
01706 CPPUNIT_ASSERT(s.numVars() > s.sharedContext()->numVars());
01707 CPPUNIT_ASSERT(s.validVar(aux) && !s.sharedContext()->validVar(aux));
01708 LitVec clause;
01709 clause.push_back(posLit(aux));
01710 clause.push_back(a);
01711 clause.push_back(b);
01712 ClauseCreator::create(s, clause, 0, Constraint_t::learnt_conflict);
01713 CPPUNIT_ASSERT(s.sharedContext()->numTernary() == 0);
01714 CPPUNIT_ASSERT(s.numLearntConstraints() == 1);
01715 s.assume(~a) && s.propagate();
01716 s.assume(~b) && s.propagate();
01717 CPPUNIT_ASSERT(s.isTrue(posLit(aux)));
01718 s.popAuxVar();
01719 CPPUNIT_ASSERT(s.decisionLevel() < 2u);
01720 CPPUNIT_ASSERT(s.numVars() == s.sharedContext()->numVars());
01721 }
01722 void testPushAuxFact() {
01723 Literal a = posLit(ctx.addVar(Var_t::atom_var));
01724 Literal b = posLit(ctx.addVar(Var_t::atom_var));
01725 Solver& s = ctx.startAddConstraints();
01726 ctx.endInit();
01727 Var aux = s.pushAuxVar();
01728 LitVec clause;
01729 clause.push_back(posLit(aux));
01730 clause.push_back(a);
01731 ClauseCreator::create(s, clause, 0, Constraint_t::learnt_conflict);
01732 s.force(~a) && s.propagate();
01733 s.force(b) && s.simplify();
01734 CPPUNIT_ASSERT(s.numFreeVars() == 0);
01735 s.popAuxVar();
01736 CPPUNIT_ASSERT(s.numFreeVars() == 0 && s.validVar(aux) == false);
01737 }
01738 void testPopAuxRemovesConstraints() {
01739 Literal a = posLit(ctx.addVar(Var_t::atom_var));
01740 Literal b = posLit(ctx.addVar(Var_t::atom_var));
01741 Literal c = posLit(ctx.addVar(Var_t::atom_var));
01742 Solver& s = ctx.startAddConstraints();
01743 ctx.endInit();
01744 Var aux = s.pushAuxVar();
01745 LitVec clause;
01746 clause.push_back(a);
01747 clause.push_back(b);
01748 clause.push_back(c);
01749 clause.push_back(posLit(aux));
01750 ClauseCreator::create(s, clause, 0, Constraint_t::learnt_conflict);
01751 clause.clear();
01752 clause.push_back(a);
01753 clause.push_back(b);
01754 clause.push_back(~c);
01755 clause.push_back(negLit(aux));
01756 ClauseCreator::create(s, clause, 0, Constraint_t::learnt_conflict);
01757 CPPUNIT_ASSERT(s.numLearntConstraints() == 2);
01758 s.popAuxVar();
01759 CPPUNIT_ASSERT(s.numLearntConstraints() == 0);
01760 }
01761 void testPopAuxMaintainsQueue() {
01762 Literal a = posLit(ctx.addVar(Var_t::atom_var));
01763 Literal b = posLit(ctx.addVar(Var_t::atom_var));
01764 Literal c = posLit(ctx.addVar(Var_t::atom_var));
01765 Solver& s = ctx.startAddConstraints();
01766 ctx.endInit();
01767 Var aux = s.pushAuxVar();
01768 s.force(a, 0); s.propagate();
01769 s.force(posLit(aux), 0);
01770 s.force(b, 0);
01771 s.popAuxVar();
01772 CPPUNIT_ASSERT(s.isTrue(a) && s.isTrue(b) && s.queueSize() == 1 && s.assignment().units() == 1);
01773 }
01774
01775 void testIncrementalAux() {
01776 Literal a = posLit(ctx.addVar(Var_t::atom_var));
01777 Literal b = posLit(ctx.addVar(Var_t::atom_var));
01778 Literal c = posLit(ctx.addVar(Var_t::atom_var));
01779 Solver& s = ctx.startAddConstraints();
01780 Solver& s2= ctx.addSolver();
01781 ctx.endInit(true);
01782 Var aux = s2.pushAuxVar();
01783 CPPUNIT_ASSERT(!ctx.validVar(aux) && !s.validVar(aux));
01784 LitVec clause;
01785 clause.push_back(a);
01786 clause.push_back(posLit(aux));
01787 ClauseCreator::create(s2, clause, 0, Constraint_t::learnt_conflict);
01788 ctx.unfreeze();
01789 Var n = ctx.addVar(Var_t::atom_var);
01790 ctx.startAddConstraints();
01791 ctx.endInit(true);
01792 s2.assume(negLit(n)) && s2.propagate();
01793 CPPUNIT_ASSERT(s2.value(a.var()) == value_free);
01794 }
01795
01796 void testUnfreezeStepBug() {
01797 Literal a = posLit(ctx.addVar(Var_t::atom_var));
01798 Literal b = posLit(ctx.addVar(Var_t::atom_var));
01799 ctx.requestStepVar();
01800 Solver& s = ctx.startAddConstraints();
01801 Solver& s2= ctx.addSolver();
01802 ctx.addBinary(~a, b);
01803 ctx.endInit(true);
01804 s2.force(b);
01805 ctx.unfreeze();
01806 ctx.endInit(true);
01807 CPPUNIT_ASSERT(s.force(a) && s.propagate());
01808 CPPUNIT_ASSERT(s.isTrue(b));
01809 }
01810 void testRemoveConstraint() {
01811 Literal a = posLit(ctx.addVar(Var_t::atom_var));
01812 Literal b = posLit(ctx.addVar(Var_t::atom_var));
01813 ctx.requestStepVar();
01814 Solver& s = ctx.startAddConstraints();
01815 Solver& s2= ctx.addSolver();
01816 ctx.add(new TestingConstraint());
01817 ctx.endInit(true);
01818 CPPUNIT_ASSERT(s2.numConstraints() == 1);
01819 ctx.removeConstraint(0, true);
01820 CPPUNIT_ASSERT(s.numConstraints() == 0);
01821 CPPUNIT_ASSERT(s2.numConstraints() == 1);
01822 ctx.unfreeze();
01823 ctx.startAddConstraints();
01824 ctx.add(new TestingConstraint());
01825 ctx.add(new TestingConstraint());
01826 ctx.endInit(true);
01827 CPPUNIT_ASSERT(s.numConstraints() == 2);
01828 CPPUNIT_ASSERT(s2.numConstraints() == 3);
01829 }
01830 private:
01831 SharedContext ctx;
01832 void integrateGp(Solver& s, LitVec& gp) {
01833 s.clearAssumptions();
01834 for (LitVec::size_type i = 0; i != gp.size(); ++i) {
01835 if (s.value(gp[i].var()) == value_free) {
01836 s.assume(gp[i]) && s.propagate();
01837 s.pushRootLevel();
01838 }
01839 }
01840 }
01841 LitVec addBinary() {
01842 LitVec r;
01843 r.push_back( posLit(ctx.addVar(Var_t::atom_var)) );
01844 r.push_back( posLit(ctx.addVar(Var_t::atom_var)) );
01845 ctx.startAddConstraints();
01846 ctx.addBinary(r[0], r[1]);
01847 ctx.endInit();
01848 return r;
01849 }
01850 LitVec addTernary() {
01851 LitVec r;
01852 r.push_back( posLit(ctx.addVar(Var_t::atom_var)) );
01853 r.push_back( posLit(ctx.addVar(Var_t::atom_var)) );
01854 r.push_back( posLit(ctx.addVar(Var_t::atom_var)) );
01855 ctx.startAddConstraints();
01856 ctx.addTernary(r[0], r[1],r[2]);
01857 ctx.endInit();
01858 return r;
01859 }
01860 };
01861 CPPUNIT_TEST_SUITE_REGISTRATION(SolverTest);
01862 } }
01863