clause_creator_test.cpp
Go to the documentation of this file.
00001 // 
00002 // Copyright (c) 2006, Benjamin Kaufmann
00003 // 
00004 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 
00005 // 
00006 // Clasp is free software; you can redistribute it and/or modify
00007 // it under the terms of the GNU General Public License as published by
00008 // the Free Software Foundation; either version 2 of the License, or
00009 // (at your option) any later version.
00010 // 
00011 // Clasp is distributed in the hope that it will be useful,
00012 // but WITHOUT ANY WARRANTY; without even the implied warranty of
00013 // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
00014 // GNU General Public License for more details.
00015 // 
00016 // You should have received a copy of the GNU General Public License
00017 // along with Clasp; if not, write to the Free Software
00018 // Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
00019 //
00020 #include "test.h"
00021 #include <algorithm>
00022 #include <clasp/clause.h>
00023 #include <clasp/solver.h>
00024 namespace Clasp { namespace Test {
00025 using namespace Clasp::mt;
00026 class ClauseCreatorTest : public CppUnit::TestFixture {
00027 
00028   CPPUNIT_TEST_SUITE(ClauseCreatorTest);
00029         CPPUNIT_TEST(testEmptyClauseIsFalse);   
00030         CPPUNIT_TEST(testFactsAreAsserted);
00031         CPPUNIT_TEST(testTopLevelSATClausesAreNotAdded);
00032         CPPUNIT_TEST(testTopLevelFalseLitsAreRemoved);
00033         CPPUNIT_TEST(testAddBinaryClause);
00034         CPPUNIT_TEST(testAddTernaryClause);
00035         CPPUNIT_TEST(testAddGenericClause);
00036         CPPUNIT_TEST(testCreatorAssertsFirstLit);
00037         CPPUNIT_TEST(testCreatorInitsWatches);
00038         CPPUNIT_TEST(testCreatorNotifiesHeuristic);
00039         CPPUNIT_TEST(testCreatorAddLitBug);
00040 
00041         CPPUNIT_TEST(testCreatorSimplifyRemovesDuplicates);
00042         CPPUNIT_TEST(testCreatorSimplifyFindsTauts);
00043         CPPUNIT_TEST(testCreatorSimplifyMovesWatch);
00044         CPPUNIT_TEST(testCreatorSimplifyBug);
00045 
00046         CPPUNIT_TEST(testCreateNonAssertingLearntClause);
00047         CPPUNIT_TEST(testCreateLearntClauseConflict);
00048         CPPUNIT_TEST(testCreateNonAssertingLearntClauseAsserting);
00049         CPPUNIT_TEST(testCreateBogusUnit);
00050         
00051         CPPUNIT_TEST(testInitWatches);
00052         CPPUNIT_TEST(testIntegrateEmpty);
00053         CPPUNIT_TEST(testIntegrateUnit);
00054         CPPUNIT_TEST(testIntegrateUnitSAT);
00055         CPPUNIT_TEST(testIntegrateConflict);
00056         CPPUNIT_TEST(testIntegrateAssertingConflict);
00057         CPPUNIT_TEST(testIntegrateAssertingConflictBelowRoot);
00058         CPPUNIT_TEST(testIntegrateConflictBelowRoot);
00059         CPPUNIT_TEST(testIntegrateSATBug1);
00060         CPPUNIT_TEST(testIntegrateSATBug2);
00061         CPPUNIT_TEST(testIntegrateSATBug3);
00062         CPPUNIT_TEST(testIntegrateSATBug4);
00063         CPPUNIT_TEST(testIntegrateKnownOrderBug);
00064         CPPUNIT_TEST(testIntegrateNotConflictingBug);
00065         CPPUNIT_TEST(testIntegrateSimplify);
00066         CPPUNIT_TEST(testIntegrateSAT);
00067         CPPUNIT_TEST(testIntegrateUnsat);
00068         CPPUNIT_TEST(testIntegrateAssertingBelowBT);
00069         CPPUNIT_TEST(testIntegrateConflictBelowBT);
00070         
00071         CPPUNIT_TEST(testFactsAreRemovedFromLearnt);
00072         CPPUNIT_TEST_SUITE_END();       
00073 public:
00074         ClauseCreatorTest() {
00075                 a = posLit(ctx.addVar(Var_t::atom_var));
00076                 b = posLit(ctx.addVar(Var_t::atom_var));
00077                 c = posLit(ctx.addVar(Var_t::atom_var));
00078                 d = posLit(ctx.addVar(Var_t::atom_var));
00079                 e = posLit(ctx.addVar(Var_t::atom_var));
00080                 f = posLit(ctx.addVar(Var_t::atom_var));
00081                 creator.setSolver(*ctx.master());
00082                 ctx.startAddConstraints(1);
00083         }
00084         void testEmptyClauseIsFalse() {
00085                 CPPUNIT_ASSERT_EQUAL(false, (bool)creator.start().end());
00086         }
00087         
00088         void testFactsAreAsserted() {
00089                 CPPUNIT_ASSERT_EQUAL(true, (bool)creator.start().add(a).end());
00090                 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(a));
00091         }
00092         void testTopLevelSATClausesAreNotAdded() {
00093                 solver().force(a, 0);
00094                 CPPUNIT_ASSERT_EQUAL(true, (bool)creator.start().add(a).add(b).end());
00095                 CPPUNIT_ASSERT_EQUAL(0u, ctx.numConstraints());
00096         }
00097         void testTopLevelFalseLitsAreRemoved() {
00098                 solver().force(~a, 0);
00099                 CPPUNIT_ASSERT_EQUAL(true, (bool)creator.start().add(a).add(b).end());
00100                 CPPUNIT_ASSERT_EQUAL(0u, ctx.numConstraints());
00101                 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(b));
00102         }
00103         void testAddBinaryClause() {
00104                 CPPUNIT_ASSERT_EQUAL(true, (bool)creator.start().add(a).add(b).end());
00105                 CPPUNIT_ASSERT_EQUAL(1u, ctx.numConstraints());
00106                 CPPUNIT_ASSERT_EQUAL(1u, ctx.numBinary());
00107         }
00108         void testAddTernaryClause() {
00109                 CPPUNIT_ASSERT_EQUAL(true, (bool)creator.start().add(a).add(b).add(c).end());
00110                 CPPUNIT_ASSERT_EQUAL(1u, ctx.numConstraints());
00111                 CPPUNIT_ASSERT_EQUAL(1u, ctx.numTernary());
00112         }
00113         void testAddGenericClause() {
00114                 CPPUNIT_ASSERT_EQUAL(true, (bool)creator.start().add(a).add(b).add(c).add(d).end());            
00115                 CPPUNIT_ASSERT_EQUAL(1u, ctx.numConstraints());
00116         }
00117 
00118         void testCreatorAssertsFirstLit() {
00119                 ctx.endInit();
00120                 solver().assume(~b);
00121                 solver().assume(~c);
00122                 solver().assume(~d);
00123                 solver().propagate();
00124                 CPPUNIT_ASSERT_EQUAL(true, (bool)creator.start(Constraint_t::learnt_conflict).add(a)
00125                         .add(b).add(c).add(d).end());
00126 
00127                 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(a));
00128                 CPPUNIT_ASSERT_EQUAL(false, solver().hasConflict());
00129                 CPPUNIT_ASSERT_EQUAL(1u, solver().numLearntConstraints());
00130         }
00131 
00132         void testCreatorInitsWatches() {
00133                 ctx.endInit();
00134                 solver().assume(~b);
00135                 solver().assume(~c);
00136                 solver().assume(~d);
00137                 
00138                 creator.start(Constraint_t::learnt_conflict).add(a).add(b).add(d).add(c);
00139                 CPPUNIT_ASSERT_EQUAL(true, (bool)creator.end());        // asserts a
00140                 solver().undoUntil(2);  // clear a and d
00141                 solver().assume(~d);            // hopefully d was watched.
00142                 solver().propagate();
00143                 CPPUNIT_ASSERT_EQUAL( value_true, solver().value(a.var()) );
00144         }
00145         void testCreatorNotifiesHeuristic() {
00146                 struct FakeHeu : public SelectFirst {
00147                         void newConstraint(const Solver&, const Literal*, LitVec::size_type size, ConstraintType t) {
00148                                 clSizes_.push_back(size);
00149                                 clTypes_.push_back(t);
00150                         }
00151                         std::vector<LitVec::size_type> clSizes_;
00152                         std::vector<ConstraintType> clTypes_;
00153                 }*heu = new FakeHeu;
00154                 solver().heuristic().reset(heu);
00155                 CPPUNIT_ASSERT_EQUAL(true, (bool)creator.start().add(a).add(b).add(c).add(d).end());
00156                 ctx.endInit();
00157                 solver().assume(a);
00158                 solver().assume(b);
00159                 solver().propagate();
00160 
00161                 CPPUNIT_ASSERT_EQUAL(true, (bool)creator.start(Constraint_t::learnt_conflict).add(c)
00162                         .add(~a).add(~b).end());
00163 
00164                 CPPUNIT_ASSERT_EQUAL(true, (bool)creator.start(Constraint_t::learnt_loop).add(c)
00165                         .add(~a).add(~b).end(0));
00166 
00167                 CPPUNIT_ASSERT_EQUAL(uint32(3), (uint32)heu->clSizes_.size());
00168                 CPPUNIT_ASSERT_EQUAL(uint32(4), (uint32)heu->clSizes_[0]);
00169                 CPPUNIT_ASSERT_EQUAL(uint32(3), (uint32)heu->clSizes_[1]);
00170                 CPPUNIT_ASSERT_EQUAL(uint32(3), (uint32)heu->clSizes_[2]);
00171 
00172                 CPPUNIT_ASSERT_EQUAL(Constraint_t::static_constraint, heu->clTypes_[0]);
00173                 CPPUNIT_ASSERT_EQUAL(Constraint_t::learnt_conflict, heu->clTypes_[1]);
00174                 CPPUNIT_ASSERT_EQUAL(Constraint_t::learnt_loop, heu->clTypes_[2]);
00175         }
00176 
00177         void testCreatorAddLitBug() {
00178                 creator.start(Constraint_t::learnt_conflict).add(a);
00179                 solver().assume(b) && solver().propagate();
00180                 creator.add(~b);
00181                 solver().assume(c) && solver().propagate();
00182                 creator.add(~c);
00183                 solver().assume(d) && solver().propagate();
00184                 creator.add(~d);
00185                 creator.end();
00186                 CPPUNIT_ASSERT_MESSAGE("TODO: Fix me!", creator[0] == a);
00187         }
00188 
00189         void testCreatorSimplifyRemovesDuplicates() {
00190                 creator.start().add(a).add(b).add(c).add(a).add(b).add(d).prepare(true);
00191                 CPPUNIT_ASSERT(creator.size() == 4);
00192                 CPPUNIT_ASSERT(creator[0] == a);
00193                 CPPUNIT_ASSERT(creator[1] == b);
00194                 CPPUNIT_ASSERT(creator[2] == c);
00195                 CPPUNIT_ASSERT(creator[3] == d);
00196         }
00197         void testCreatorSimplifyFindsTauts() {
00198                 creator.start().add(a).add(b).add(c).add(a).add(b).add(~a).end(ClauseCreator::clause_force_simplify);
00199                 CPPUNIT_ASSERT(0 == ctx.numConstraints());
00200         }
00201         void testCreatorSimplifyMovesWatch() {
00202                 ctx.endInit();
00203                 solver().assume(a); solver().propagate();
00204                 solver().assume(b); solver().propagate();
00205                 creator.start(Constraint_t::learnt_loop);
00206                 creator.add(~a).add(~b).add(~b).add(~a).add(c).add(d).prepare(true);
00207                 CPPUNIT_ASSERT(creator.size() == 4);
00208                 CPPUNIT_ASSERT_EQUAL(c, creator[0]);
00209                 CPPUNIT_ASSERT_EQUAL(d, creator[1]);
00210         }
00211 
00212         void testCreatorSimplifyBug() {
00213                 LitVec clause;
00214                 clause.push_back(negLit(0));
00215                 clause.push_back(a);
00216                 clause.push_back(b);
00217                 ClauseCreator::prepare(*ctx.master(), clause, ClauseCreator::clause_force_simplify);
00218                 CPPUNIT_ASSERT(clause.size() == 2);
00219         }
00220 
00221         void testCreateNonAssertingLearntClause() {
00222                 ctx.endInit();
00223                 solver().assume(a); solver().propagate();
00224                 solver().assume(b); solver().propagate();
00225                 creator.start(Constraint_t::learnt_loop);
00226                 creator.add(~a).add(~b).add(c).add(d);
00227                 CPPUNIT_ASSERT(creator.end());
00228                 CPPUNIT_ASSERT_EQUAL(c, creator[0]);
00229                 CPPUNIT_ASSERT_EQUAL(d, creator[1]);
00230                 CPPUNIT_ASSERT(solver().numLearntConstraints() == 1);
00231 
00232                 solver().undoUntil(0);
00233                 // test with a short clause
00234                 solver().assume(a); solver().propagate();
00235                 creator.start(Constraint_t::learnt_loop);
00236                 creator.add(~a).add(b).add(c);
00237                 CPPUNIT_ASSERT(creator.end());
00238                 CPPUNIT_ASSERT_EQUAL(b, creator[0]);
00239                 CPPUNIT_ASSERT_EQUAL(c, creator[1]);
00240                 CPPUNIT_ASSERT(ctx.numLearntShort() == 1);
00241         }
00242         void testCreateLearntClauseConflict() {
00243                 ctx.endInit();
00244                 solver().assume(a); solver().force(b,0); solver().propagate();// level 1
00245                 solver().assume(c); solver().propagate();                     // level 2
00246                 solver().assume(d); solver().propagate();                     // level 3
00247                 solver().assume(f); solver().propagate();                     // level 4
00248 
00249                 creator.start(Constraint_t::learnt_loop);
00250                 creator.add(~c).add(~a).add(~d).add(~b); // 2 1 3 1
00251                 CPPUNIT_ASSERT_EQUAL(false, (bool)creator.end());
00252                 // make sure we watch highest levels, i.e. 3 and 2
00253                 CPPUNIT_ASSERT_EQUAL(~d, creator[0]);
00254                 CPPUNIT_ASSERT_EQUAL(~c, creator[1]);
00255                 CPPUNIT_ASSERT(solver().numLearntConstraints() == 0);
00256 
00257                 
00258                 solver().undoUntil(0);
00259                 // test with a short clause
00260                 solver().assume(a); solver().propagate();// level 1
00261                 solver().assume(c); solver().propagate();// level 2
00262                 creator.start(Constraint_t::learnt_loop);
00263                 creator.add(~a).add(~c);
00264                 CPPUNIT_ASSERT_EQUAL(false, (bool)creator.end());
00265                 CPPUNIT_ASSERT_EQUAL(~c, creator[0]);
00266                 CPPUNIT_ASSERT_EQUAL(~a, creator[1]);
00267                 CPPUNIT_ASSERT(ctx.numBinary() == 0);
00268         }
00269 
00270         void testCreateNonAssertingLearntClauseAsserting() {
00271                 ctx.endInit();
00272                 solver().assume(a); solver().force(b,0); solver().propagate();// level 1
00273                 solver().assume(c); solver().propagate();                     // level 2
00274                 creator.start(Constraint_t::learnt_loop);
00275                 creator.add(~c).add(~a).add(d).add(~b);                       // 2 1 Free 1
00276                 CPPUNIT_ASSERT_EQUAL(true, (bool)creator.end());
00277                 // make sure we watch the right lits, i.e. d (free) and ~c (highest DL)
00278                 CPPUNIT_ASSERT_EQUAL(d, creator[0]);
00279                 CPPUNIT_ASSERT_EQUAL(~c, creator[1]);
00280                 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(d));
00281                 CPPUNIT_ASSERT(solver().numLearntConstraints() == 1);
00282                 // test with a short clause
00283                 solver().undoUntil(0);
00284                 solver().reduceLearnts(1.0f);
00285                 solver().assume(a); solver().force(b,0); solver().propagate();// level 1
00286                 solver().assume(c); solver().propagate();                     // level 2
00287                 creator.start(Constraint_t::learnt_loop);
00288                 creator.add(~c).add(~a).add(d);                               // 2 1 Free
00289                 CPPUNIT_ASSERT_EQUAL(true, (bool)creator.end());
00290                 // make sure we watch the right lits, i.e. d (free) and ~c (highest DL)
00291                 CPPUNIT_ASSERT_EQUAL(d, creator[0]);
00292                 CPPUNIT_ASSERT_EQUAL(~c, creator[1]);
00293                 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(d));
00294         }
00295 
00296         void testCreateBogusUnit() {
00297                 solver().assume(a) && solver().propagate();
00298                 solver().assume(~b) && solver().propagate();
00299                 solver().force(~d,0) && solver().propagate();
00300                 solver().assume(~c) && solver().propagate();
00301                 CPPUNIT_ASSERT(solver().decisionLevel() == 3);
00302                 
00303                 creator.start(Constraint_t::learnt_other).add(d).add(b).add(c).add(a);
00304                 CPPUNIT_ASSERT(ClauseCreator::status(solver(), &creator.lits()[0], &creator.lits()[0] + creator.size()) == ClauseCreator::status_sat);
00305 
00306                 ClauseCreator::Result r = creator.end();
00307                 CPPUNIT_ASSERT_EQUAL(true, r.ok());
00308                 CPPUNIT_ASSERT(solver().decisionLevel() == 3);
00309         }
00310 
00311         void testInitWatches() {
00312                 LitVec cl;
00313                 cl.push_back(a);
00314                 cl.push_back(b);
00315                 cl.push_back(c);
00316                 cl.push_back(d);
00317                 solver().assume(~b)   && solver().propagate();
00318                 solver().force(~c, 0) && solver().propagate();
00319                 solver().assume(~a)   && solver().propagate();
00320                 solver().assume(d)    && solver().propagate();
00321                 // aF@2 bF@1 cF@1 dT@3 -> dT@3 aF@2 cF@1 bF@1
00322                 LitVec temp = cl;
00323                 ClauseCreator::prepare(solver(), temp, 0);
00324                 CPPUNIT_ASSERT(temp[0] == d);
00325                 CPPUNIT_ASSERT(temp[1] == a);
00326                 
00327                 SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00328                 ClauseCreator::Result r = ClauseCreator::integrate(solver(), p, ClauseCreator::clause_no_add);
00329                 temp.clear();
00330                 r.local->clause()->toLits(temp);
00331                 CPPUNIT_ASSERT(temp[0] == d);
00332                 CPPUNIT_ASSERT(temp[1] == a);
00333                 r.local->destroy(&solver(), true);
00334         }
00335 
00336         void testIntegrateEmpty() {
00337                 LitVec cl;
00338                 solver().assume(~a) && solver().propagate();
00339                 solver().pushRootLevel(solver().decisionLevel());
00340                 SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00341                 ClauseCreator::Result r = ClauseCreator::integrate(solver(), p, 0);
00342                 CPPUNIT_ASSERT_EQUAL(false, r.ok());
00343                 CPPUNIT_ASSERT_EQUAL(true, solver().hasConflict());
00344                 CPPUNIT_ASSERT_EQUAL(false, solver().clearAssumptions());
00345         }
00346         void testIntegrateUnit() {
00347                 solver().assume(a) && solver().propagate();
00348                 solver().assume(b) && solver().propagate();
00349                 solver().assume(c) && solver().propagate();
00350                 solver().assume(d) && solver().propagate();
00351                 solver().pushRootLevel(solver().decisionLevel());
00352                 solver().assume(e) && solver().propagate();
00353 
00354                 LitVec cl; 
00355                 // ~a ~b ~c f -> Unit: f@3
00356                 cl.push_back(~a); cl.push_back(f);
00357                 cl.push_back(~c); cl.push_back(~b);
00358                 SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00359                 ClauseCreator::integrate(solver(), p, 0);
00360                 CPPUNIT_ASSERT(solver().isTrue(f));
00361                 CPPUNIT_ASSERT(solver().decisionLevel() == solver().rootLevel());
00362                 solver().popRootLevel();
00363                 solver().backtrack() && solver().propagate();
00364                 CPPUNIT_ASSERT(solver().isTrue(f));
00365                 CPPUNIT_ASSERT(solver().decisionLevel() == solver().rootLevel());
00366                 solver().popRootLevel();
00367                 solver().backtrack() && solver().propagate();
00368                 CPPUNIT_ASSERT_EQUAL(false, solver().isTrue(f));
00369                 CPPUNIT_ASSERT(solver().value(c.var()) == value_free);
00370         }
00371 
00372         void testIntegrateUnitSAT() {
00373                 solver().assume(a) && solver().propagate();
00374                 LitVec cl; 
00375                 cl.push_back(a);
00376                 SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00377                 ClauseCreator::integrate(solver(), p, 0);
00378                 CPPUNIT_ASSERT(solver().isTrue(a));
00379                 CPPUNIT_ASSERT(solver().decisionLevel() == 0);
00380         }
00381 
00382         void testIntegrateConflict() {
00383                 solver().assume(a) && solver().propagate();
00384                 solver().assume(b) && solver().propagate();
00385                 solver().assume(c) && solver().propagate();
00386                 solver().force(d, 0) && solver().propagate();
00387                 
00388                 // ~a ~b ~c ~d -> conflicting@3
00389                 LitVec cl;
00390                 cl.push_back(~a); cl.push_back(~c); cl.push_back(~b); cl.push_back(~d);
00391                 SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00392                 ClauseCreator::Result r = ClauseCreator::integrate(solver(), p, 0);
00393                 CPPUNIT_ASSERT(!r.ok());
00394                 CPPUNIT_ASSERT(r.local != 0);
00395                 CPPUNIT_ASSERT(solver().hasConflict());
00396         }
00397 
00398         void testIntegrateAssertingConflict() {
00399                 solver().assume(a) && solver().propagate();
00400                 solver().assume(b) && solver().propagate();
00401                 solver().assume(c) && solver().propagate();
00402                 solver().assume(d) && solver().propagate();
00403                 
00404                 // ~a ~b ~c -> Conflict @3
00405                 LitVec cl;
00406                 cl.push_back(~a); cl.push_back(~c); cl.push_back(~b);
00407                 SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00408                 ClauseCreator::integrate(solver(), p, 0);
00409                 CPPUNIT_ASSERT(solver().decisionLevel() == uint32(2));
00410         }
00411 
00412         void testIntegrateAssertingConflictBelowRoot() {
00413                 solver().assume(a) && solver().propagate();
00414                 solver().assume(b) && solver().propagate();
00415                 solver().assume(d) && solver().propagate();
00416                 solver().pushRootLevel(solver().decisionLevel());
00417                 solver().assume(c) && solver().propagate();
00418                 // ~a ~b ~c -> Conflict @3, Asserting @2
00419                 LitVec cl;
00420                 cl.push_back(~a); cl.push_back(~c); cl.push_back(~b);
00421                 SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00422                 ClauseCreator::integrate(solver(), p, 0);
00423                 CPPUNIT_ASSERT(solver().decisionLevel() == uint32(3));
00424                 solver().popRootLevel();
00425                 solver().backtrack() && solver().propagate();
00426                 CPPUNIT_ASSERT(solver().isTrue(~c));
00427         }
00428         void testIntegrateConflictBelowRoot() {
00429                 LitVec cl;
00430                 cl.push_back(a); cl.push_back(b); cl.push_back(c);
00431                 solver().assume(~a) && solver().propagate();
00432                 solver().assume(~b) && solver().propagate();
00433                 solver().assume(~c) && solver().propagate();
00434                 solver().assume(~d) && solver().propagate();
00435                 solver().pushRootLevel(solver().decisionLevel());
00436                 SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00437                 ClauseCreator::Result r = ClauseCreator::integrate(solver(), p, ClauseCreator::clause_explicit);
00438                 CPPUNIT_ASSERT_EQUAL(false, r.ok());
00439                 CPPUNIT_ASSERT_EQUAL(uint32(1), solver().numLearntConstraints());
00440         }
00441         
00442         void testIntegrateSATBug1() {
00443                 LitVec cl;
00444                 cl.push_back(d); cl.push_back(b); cl.push_back(a); cl.push_back(c);
00445                 solver().assume(~a) && solver().propagate();
00446                 solver().assume(b) && solver().propagate();
00447                 solver().assume(~d) && solver().propagate();
00448                 SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00449                 ClauseCreator::Result r = ClauseCreator::integrate(solver(), p, 0);
00450                 CPPUNIT_ASSERT_EQUAL(true, r.ok());
00451                 CPPUNIT_ASSERT(3u == solver().numAssignedVars());
00452         }
00453         void testIntegrateSATBug2() {
00454                 LitVec cl;
00455                 cl.push_back(d); cl.push_back(b); cl.push_back(c); cl.push_back(a);
00456                 solver().assume(~a) && solver().propagate();
00457                 solver().assume(b) && solver().propagate();
00458                 solver().assume(~d) && solver().propagate();
00459                 solver().force(c,0) && solver().propagate();
00460                 SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00461                 ClauseCreator::Result r = ClauseCreator::integrate(solver(), p, 0);
00462                 CPPUNIT_ASSERT_EQUAL(true, r.ok());
00463         }
00464 
00465         void testIntegrateSATBug3() {
00466                 LitVec cl;
00467                 cl.push_back(d); cl.push_back(b); cl.push_back(c); cl.push_back(a);
00468                 solver().assume(~a) && solver().propagate();
00469                 solver().assume(~b) && solver().propagate();
00470                 solver().force(~d,0) && solver().propagate();
00471                 solver().assume(c) && solver().propagate();
00472                 CPPUNIT_ASSERT(solver().decisionLevel() == 3);
00473                 SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00474                 ClauseCreator::Result r = ClauseCreator::integrate(solver(), p, ClauseCreator::clause_not_sat);
00475                 
00476                 CPPUNIT_ASSERT_EQUAL(true, r.ok());
00477                 CPPUNIT_ASSERT(solver().decisionLevel() == 2);
00478                 CPPUNIT_ASSERT(solver().isTrue(c));
00479         }
00480 
00481         void testIntegrateSATBug4() {
00482                 LitVec cl;
00483                 cl.push_back(a); cl.push_back(b);
00484                 solver().force(~a, 0);
00485                 solver().assume(b);
00486                 SharedLiterals* p(SharedLiterals::newShareable(cl,Constraint_t::learnt_other));
00487                 CPPUNIT_ASSERT((ClauseCreator::status(solver(), p->begin(), p->end()) & ClauseCreator::status_unit) != 0);
00488                 ClauseCreator::integrate(solver(), p, ClauseCreator::clause_explicit);
00489         }
00490 
00491         void testIntegrateKnownOrderBug() {
00492                 LitVec cl;
00493                 cl.push_back(a);
00494                 SharedLiterals* p(SharedLiterals::newShareable(cl,Constraint_t::learnt_other));
00495                 CPPUNIT_ASSERT((ClauseCreator::status(solver(), p->begin(), p->end()) & ClauseCreator::status_unit) != 0);
00496                 ClauseCreator::integrate(solver(), p, ClauseCreator::clause_no_prepare);
00497                 CPPUNIT_ASSERT(solver().isTrue(a));
00498         }
00499 
00500         void testIntegrateNotConflictingBug() {
00501                 LitVec cl;
00502                 cl.push_back(a); cl.push_back(b);
00503                 SharedLiterals* p(SharedLiterals::newShareable(cl,Constraint_t::learnt_other));
00504                 solver().assume(~a) && solver().propagate();
00505                 solver().force(~b,0)&& solver().propagate();
00506                 CPPUNIT_ASSERT((ClauseCreator::status(solver(), p->begin(), p->end()) & ClauseCreator::status_unsat) != 0);
00507                 ClauseCreator::Result r = ClauseCreator::integrate(solver(), p, ClauseCreator::clause_not_conflict);
00508                 CPPUNIT_ASSERT(r.ok() == false);
00509                 CPPUNIT_ASSERT(r.local == 0);
00510         }
00511         void testIntegrateSimplify() {
00512                 LitVec cl;
00513                 cl.push_back(a); cl.push_back(b); cl.push_back(c);
00514                 cl.push_back(d); cl.push_back(e); cl.push_back(f);
00515                 SharedLiterals* p(SharedLiterals::newShareable(cl,Constraint_t::learnt_other));
00516                 solver().force(~d, 0) && solver().propagate();
00517                 solver().assume(~a)   && solver().propagate();
00518                 ClauseCreator::Result r = ClauseCreator::integrate(solver(), p, ClauseCreator::clause_no_add);
00519                 CPPUNIT_ASSERT(r.ok());
00520                 CPPUNIT_ASSERT(r.local != 0);
00521                 cl.clear();
00522                 r.local->toLits(cl);
00523                 CPPUNIT_ASSERT(cl.size() == 5 && std::find(cl.begin(), cl.end(), d) == cl.end());
00524         }
00525         void testIntegrateSAT() {
00526                 LitVec cl;
00527                 cl.push_back(a); cl.push_back(b); cl.push_back(c); cl.push_back(d);
00528                 solver().assume(~a) && solver().propagate();
00529                 solver().assume(b) && solver().propagate();
00530                 solver().assume(~d) && solver().propagate();
00531                 do {
00532                         SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00533                         ClauseCreator::Result r = ClauseCreator::integrate(solver(), p, ClauseCreator::clause_not_sat);
00534                         CPPUNIT_ASSERT_EQUAL(true, r.ok());
00535                         CPPUNIT_ASSERT(solver().numAssignedVars() == 3);
00536                 } while (std::next_permutation(cl.begin(), cl.end()));
00537                 CPPUNIT_ASSERT(solver().numLearntConstraints() == 0);
00538         }
00539 
00540         void testIntegrateUnsat() {
00541                 solver().force(~a,0) && solver().propagate();
00542                 solver().assume(b);
00543                 LitVec cl;
00544                 cl.push_back(a);
00545                 SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00546                 ClauseCreator::Result r = ClauseCreator::integrate(solver(), p, 0);
00547                 CPPUNIT_ASSERT_EQUAL(false, r.ok());
00548                 CPPUNIT_ASSERT(0 == r.local);
00549                 CPPUNIT_ASSERT_EQUAL(uint32(0), solver().decisionLevel());
00550         }
00551 
00552         void testIntegrateAssertingBelowBT() {
00553                 solver().assume(a) && solver().propagate();
00554                 solver().assume(b) && solver().propagate();
00555                 solver().assume(c) && solver().propagate();
00556                 solver().assume(d) && solver().propagate();
00557                 solver().setBacktrackLevel(solver().decisionLevel());
00558                 // ~a ~b ~c -> Conflict @3, Asserting @2
00559                 LitVec cl;
00560                 cl.push_back(~a); cl.push_back(~c); cl.push_back(~b);
00561                 SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00562                 ClauseCreator::Result r = ClauseCreator::integrate(solver(), p, 0);
00563                 CPPUNIT_ASSERT_EQUAL(false, r.ok());
00564                 solver().backtrack();
00565                 CPPUNIT_ASSERT(solver().isTrue(~c));
00566                 CPPUNIT_ASSERT_EQUAL(uint32(2), solver().decisionLevel());
00567                 solver().backtrack();
00568                 CPPUNIT_ASSERT(!solver().isTrue(~c));
00569         }
00570 
00571         void testIntegrateConflictBelowBT() {
00572                 solver().assume(a) && solver().propagate();
00573                 solver().assume(b) && solver().force(c, 0) && solver().propagate();
00574                 solver().assume(d) && solver().propagate();
00575                 solver().assume(e) && solver().propagate();
00576                 solver().setBacktrackLevel(solver().decisionLevel());
00577                 // ~a ~b ~c -> Conflict @2
00578                 LitVec cl;
00579                 cl.push_back(~a); cl.push_back(~c); cl.push_back(~b);
00580                 SharedLiterals* p(SharedLiterals::newShareable(cl, Constraint_t::learnt_other));
00581                 ClauseCreator::Result r = ClauseCreator::integrate(solver(), p, 0);
00582                 CPPUNIT_ASSERT_EQUAL(false, r.ok());
00583                 CPPUNIT_ASSERT_EQUAL(true, solver().resolveConflict());
00584                 CPPUNIT_ASSERT_EQUAL(uint32(1), solver().decisionLevel());
00585         }
00586 
00587 
00588         void testFactsAreRemovedFromLearnt() {
00589                 ctx.enableStats(1);
00590                 ctx.addUnary(a);
00591                 ctx.endInit();
00592                 solver().assume(~b) && solver().propagate();
00593                 creator.start(Constraint_t::learnt_conflict);
00594                 creator.add(b).add(c).add(~a).end();
00595 
00596                 CPPUNIT_ASSERT(1u == ctx.numLearntShort());
00597                 CPPUNIT_ASSERT(ctx.master()->stats.extra->lits[0] == 2);
00598         }
00599 private:
00600         const Solver& solver() const { return *ctx.master(); }
00601         Solver&       solver()       { return *ctx.master(); }
00602         SharedContext ctx;
00603         ClauseCreator creator;
00604         Literal a,b,c,d,e,f;
00605 };
00606 CPPUNIT_TEST_SUITE_REGISTRATION(ClauseCreatorTest);
00607 } }

clasp
Author(s): Benjamin Kaufmann
autogenerated on Thu Aug 27 2015 12:41:38