decision_heuristic_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 <clasp/heuristics.h>
00022 #include <clasp/lookahead.h>
00023 #include <clasp/logic_program.h>
00024 #include <clasp/clause.h>
00025 #include <clasp/solver.h>
00026 namespace Clasp { namespace Test {
00027 using namespace Clasp::Asp;
00028 class DecisionHeuristicTest : public CppUnit::TestFixture {
00029   CPPUNIT_TEST_SUITE(DecisionHeuristicTest);
00030         CPPUNIT_TEST(testTrivial);
00031         CPPUNIT_TEST(testBodyLookahead);
00032         CPPUNIT_TEST(testAtomLookahead);
00033         CPPUNIT_TEST(testLookaheadBugNoSimplify);
00034         CPPUNIT_TEST(testLookaheadBugDepsNotCleared);
00035         CPPUNIT_TEST(testLookaheadBugNoDeps);
00036         CPPUNIT_TEST(testLookaheadBugNoNant);
00037         CPPUNIT_TEST(testLookaheadStopConflict);
00038 
00039         CPPUNIT_TEST(testBerkmin);
00040         CPPUNIT_TEST(testVmtf);
00041         CPPUNIT_TEST(testVsids);
00042         CPPUNIT_TEST(testVsidsAux);
00043         CPPUNIT_TEST(testResurrect);
00044         CPPUNIT_TEST(testStrangeLookSeq);
00045         CPPUNIT_TEST(testStrangeLookSeq2);
00046 
00047         CPPUNIT_TEST(testDomSignPos);
00048         CPPUNIT_TEST(testDomSignNeg);
00049         CPPUNIT_TEST(testDomLevel);
00050         CPPUNIT_TEST(testDomDynamic);
00051         CPPUNIT_TEST(testDomPrio);
00052         CPPUNIT_TEST(testDomPrio2);
00053         CPPUNIT_TEST(testDomInit);
00054         CPPUNIT_TEST(testDomInc);
00055         CPPUNIT_TEST_SUITE_END();
00056 public:
00057         void testTrivial() {
00058                 SharedContext ctx;
00059                 ctx.master()->heuristic().reset(new UnitHeuristic(Lookahead::hybrid_lookahead));
00060                 ctx.startAddConstraints();
00061                 CPPUNIT_ASSERT_EQUAL(true, ctx.endInit());
00062         }
00063         void testBodyLookahead() {
00064                 SharedContext ctx;
00065                 ctx.setConcurrency(2);
00066                 Solver& s = ctx.addSolver();
00067                 LogicProgram api;
00068                 api.start(ctx, LogicProgram::AspOptions().noEq().noScc())
00069                         .setAtomName(1, "x").setAtomName(2, "a1").setAtomName(3, "a2").setAtomName(4, "a3")
00070                         .setAtomName(5, "b1").setAtomName(6, "b2").setAtomName(7, "b3")
00071                         .startRule().addHead(1).addToBody(1, false).endRule()
00072                         .startRule().addHead(1).addToBody(2, false).addToBody(5, false).endRule()
00073                         .startRule().addHead(2).addToBody(5, false).endRule()
00074                         .startRule().addHead(5).addToBody(2, false).endRule()
00075                         .startRule().addHead(1).addToBody(3, false).addToBody(6, false).endRule()
00076                         .startRule().addHead(3).addToBody(6, false).endRule()
00077                         .startRule().addHead(6).addToBody(3, false).endRule()
00078                         .startRule().addHead(1).addToBody(4, false).addToBody(7, false).endRule()
00079                         .startRule().addHead(4).addToBody(7, false).endRule()
00080                         .startRule().addHead(7).addToBody(4, false).endRule()
00081                 ;
00082                 CPPUNIT_ASSERT_EQUAL(true, api.endProgram() && ctx.endInit());
00083                 s.addPost(new Lookahead(Lookahead::Params(Lookahead::body_lookahead).addImps(false)));
00084                 CPPUNIT_ASSERT_EQUAL(false, ctx.attach(s));
00085                 ctx.detach(s, true);
00086                 s.addPost(new Lookahead(Lookahead::Params(Lookahead::atom_lookahead).addImps(false)));
00087                 CPPUNIT_ASSERT_EQUAL(true, ctx.attach(s));
00088                 ctx.detach(s, true);
00089                 s.addPost(new Lookahead(Lookahead::Params(Lookahead::hybrid_lookahead).addImps(false)));
00090                 CPPUNIT_ASSERT_EQUAL(false, ctx.attach(s));
00091         }
00092         void testAtomLookahead() {
00093                 SharedContext ctx;
00094                 ctx.setConcurrency(2);
00095                 Solver& s = ctx.addSolver();
00096                 LogicProgram api;
00097                 api.start(ctx, LogicProgram::AspOptions().noEq().noScc())
00098                         .setAtomName(1, "x").setAtomName(2, "c1").setAtomName(3, "c2").setAtomName(4, "c3")
00099                         .setAtomName(5, "a1").setAtomName(6, "a2").setAtomName(7, "a3")
00100                         .setAtomName(8, "b1").setAtomName(9, "b2").setAtomName(10, "b3")
00101                         .startRule().addHead(1).addToBody(2, true).addToBody(3, true).addToBody(4, true).addToBody(1, false).endRule()
00102                         .startRule().addHead(2).addToBody(5, false).endRule()
00103                         .startRule().addHead(2).addToBody(8, false).endRule()
00104                         .startRule().addHead(5).addToBody(8, false).endRule()
00105                         .startRule().addHead(8).addToBody(5, false).endRule()
00106                         .startRule().addHead(3).addToBody(6, false).endRule()
00107                         .startRule().addHead(3).addToBody(9, false).endRule()
00108                         .startRule().addHead(6).addToBody(9, false).endRule()
00109                         .startRule().addHead(9).addToBody(6, false).endRule()
00110                         .startRule().addHead(4).addToBody(7, false).endRule()
00111                         .startRule().addHead(4).addToBody(10, false).endRule()
00112                         .startRule().addHead(7).addToBody(10, false).endRule()
00113                         .startRule().addHead(10).addToBody(7, false).endRule()
00114                 ;
00115                 CPPUNIT_ASSERT_EQUAL(true, api.endProgram() && ctx.endInit());
00116                 Lookahead::Params p; p.addImps(false);
00117                 s.addPost(new Lookahead(p.lookahead(Lookahead::body_lookahead)));
00118                 CPPUNIT_ASSERT_EQUAL(true, ctx.attach(s));
00119                 ctx.detach(s, true);
00120                 s.addPost(new Lookahead(p.lookahead(Lookahead::atom_lookahead)));
00121                 CPPUNIT_ASSERT_EQUAL(false, ctx.attach(s));
00122                 ctx.detach(s, true);
00123                 s.addPost(new Lookahead(p.lookahead(Lookahead::hybrid_lookahead)));
00124                 CPPUNIT_ASSERT_EQUAL(false, ctx.attach(s));
00125         }
00126 
00127         void testLookaheadBugNoSimplify() {
00128                 DecisionHeuristic* lookAtom = new UnitHeuristic(Lookahead::atom_lookahead);
00129                 SharedContext ctx;
00130                 ctx.master()->heuristic().reset(lookAtom);
00131                 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00132                 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00133                 Literal e = posLit(ctx.addVar(Var_t::atom_var));
00134                 Solver& s = ctx.startAddConstraints(10);
00135                 ctx.addBinary(a,  b);
00136                 ctx.endInit();
00137                 ctx.addBinary(a, ~b);
00138                 s.assume(e) && s.propagate();
00139                 CPPUNIT_ASSERT(lookAtom->select(s));
00140                 CPPUNIT_ASSERT(s.isTrue(a));    
00141                 CPPUNIT_ASSERT(s.seen(a.var()));
00142                 CPPUNIT_ASSERT(s.decisionLevel() == 1);
00143         }
00144         void testLookaheadBugDepsNotCleared() {
00145                 DecisionHeuristic* lookAtom = new UnitHeuristic(Lookahead::atom_lookahead);
00146                 SharedContext ctx;
00147                 ctx.master()->heuristic().reset(lookAtom);
00148                 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00149                 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00150                 Literal c = posLit(ctx.addVar(Var_t::atom_var));
00151                 Literal e = posLit(ctx.addVar(Var_t::atom_var));
00152                 Literal f = posLit(ctx.addVar(Var_t::atom_var));
00153                 Solver& s = ctx.startAddConstraints();
00154                 ctx.addBinary(a, b);
00155                 ctx.addBinary(b, c);
00156                 ctx.addBinary(c, f);
00157                 ctx.addUnary(e);
00158                 ctx.endInit();
00159                 // Assume without using lookahead (e.g. a random choice)
00160                 s.assume(b);
00161                 s.propagate();
00162                 // Deps not cleared
00163                 CPPUNIT_ASSERT(lookAtom->select(s));
00164                 CPPUNIT_ASSERT(s.isFalse(c) || s.isFalse(f));
00165         }
00166         void testLookaheadBugNoDeps() {
00167                 DecisionHeuristic* lookAtom = new UnitHeuristic(Lookahead::atom_lookahead);
00168                 SharedContext ctx;
00169                 ctx.master()->heuristic().reset(lookAtom);
00170                 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00171                 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00172                 Literal c = posLit(ctx.addVar(Var_t::atom_var));
00173                 Literal e = posLit(ctx.addVar(Var_t::atom_var));
00174                 Solver& s = ctx.startAddConstraints();
00175                 ctx.addBinary(a, b);
00176                 ctx.addBinary(b, c);
00177                 ctx.addUnary(e);
00178                 ctx.endInit();
00179                 CPPUNIT_ASSERT(lookAtom->select(s));
00180                 CPPUNIT_ASSERT(s.isFalse(b));
00181                 s.undoUntil(0);
00182                 s.simplify();
00183                 CPPUNIT_ASSERT(lookAtom->select(s));
00184                 CPPUNIT_ASSERT(s.isFalse(b));
00185         }
00186         void testLookaheadBugNoNant() {
00187                 Clasp::Lookahead::Params p(Lookahead::atom_lookahead);
00188                 p.restrictNant = true;
00189                 DecisionHeuristic* lookAtom = new UnitHeuristic(p);
00190                 SharedContext ctx;
00191                 ctx.master()->heuristic().reset(lookAtom);
00192                 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00193                 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00194                 Literal c = posLit(ctx.addVar(Var_t::atom_var));
00195                 Solver& s = ctx.startAddConstraints();
00196                 ctx.addBinary(a, b);
00197                 ctx.addBinary(b, c);
00198                 ctx.addBinary(~a, ~b);
00199                 ctx.addBinary(~b, ~c);
00200                 ctx.endInit();
00201                 uint32 n = s.numFreeVars();
00202                 CPPUNIT_ASSERT(lookAtom->select(s) && s.numFreeVars() != n);
00203         }
00204         
00205         void testLookaheadStopConflict() {
00206                 DecisionHeuristic* lookAtom = new UnitHeuristic(Lookahead::atom_lookahead);
00207                 SharedContext ctx;
00208                 ctx.master()->heuristic().reset(lookAtom);
00209                 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00210                 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00211                 Solver& s = ctx.startAddConstraints();
00212                 ctx.addBinary(a, b);
00213                 ctx.endInit();
00214                 struct StopConflict : public PostPropagator {
00215                         bool propagateFixpoint(Solver& s, PostPropagator*) { s.setStopConflict(); return false; }
00216                         uint32 priority() const   { return PostPropagator::priority_class_simple; }
00217                 }* x = new StopConflict;
00218                 s.addPost(x);
00219                 CPPUNIT_ASSERT(!lookAtom->select(s) && s.hasConflict());
00220                 CPPUNIT_ASSERT(s.search(0,0) == value_false);
00221         }
00222 
00223         void testBerkmin() {
00224                 ClaspBerkmin* berkmin = new ClaspBerkmin(0, HeuParams().other(3).init(1));
00225                 SharedContext ctx;
00226                 ctx.master()->heuristic().reset(berkmin);
00227                 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00228                 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00229                 Literal c = posLit(ctx.addVar(Var_t::atom_var));
00230                 Literal d = posLit(ctx.addVar(Var_t::atom_var));
00231                 Literal e = posLit(ctx.addVar(Var_t::atom_var));
00232                 Literal f = posLit(ctx.addVar(Var_t::atom_var));
00233                 Literal g = posLit(ctx.addVar(Var_t::atom_var));
00234                 Solver& s = ctx.startAddConstraints();
00235                 ctx.endInit();
00236                 s.stats.conflicts = 1;
00237                 LitVec up;
00238                 berkmin->updateReason(s, up, Literal() );
00239                 up.push_back(a);
00240                 berkmin->updateReason( s,up,a );
00241                 up.clear();
00242                 up.push_back(b);
00243                 up.push_back(b);
00244                 berkmin->updateReason( s,up,b );
00245                 up.clear();
00246                 berkmin->updateReason( s,up,e );
00247                 s.assume( ~b );
00248                 s.assume( ~c );
00249                 s.assume( ~d );
00250                 ClauseCreator cc(&s);
00251                 cc.start(Constraint_t::learnt_conflict).add(a).add(b).add(c).add(d).end();
00252                 s.undoUntil(0);
00253                 s.assume( ~e );
00254                 s.assume( ~f );
00255                 s.assume( ~g );
00256                 cc.start(Constraint_t::learnt_loop).add(d).add(e).add(f).add(g).end();
00257                 s.undoUntil(0);
00258                 CPPUNIT_ASSERT_EQUAL(0u, s.numAssignedVars());
00259                 CPPUNIT_ASSERT_EQUAL(true, berkmin->select(s));
00260                 CPPUNIT_ASSERT_EQUAL(b, s.trail().back());      // from conflict clause
00261                 s.propagate();
00262                 CPPUNIT_ASSERT_EQUAL(true, berkmin->select(s));
00263                 CPPUNIT_ASSERT_EQUAL(e, s.trail().back());      // from loop clause
00264                 s.propagate();
00265                 CPPUNIT_ASSERT_EQUAL(true, berkmin->select(s));
00266                 CPPUNIT_ASSERT_EQUAL(a.var(), s.trail().back().var());  // highest activity
00267         }
00268         void testVmtf() {
00269                 ClaspVmtf* vmtf = new ClaspVmtf;
00270                 SharedContext ctx;
00271                 ctx.master()->heuristic().reset(vmtf);
00272                 ctx.addVar(Var_t::atom_var);
00273                 ctx.addVar(Var_t::atom_var);
00274                 Solver& s = ctx.startAddConstraints();
00275                 ctx.endInit();
00276                 CPPUNIT_ASSERT_EQUAL(true, vmtf->select(s));
00277                 s.propagate();
00278                 CPPUNIT_ASSERT_EQUAL(true, vmtf->select(s));
00279                 s.propagate(); 
00280                 CPPUNIT_ASSERT_EQUAL(false, vmtf->select(s));
00281         }
00282 
00283         void testVsids() {
00284                 ClaspVsids* vsids = new ClaspVsids;
00285                 SharedContext ctx;
00286                 ctx.master()->heuristic().reset(vsids);
00287                 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00288                 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00289                 Solver& s = ctx.startAddConstraints();
00290                 ctx.endInit();
00291                 LitVec up;
00292                 up.push_back(a);
00293                 vsids->updateReason( s,up,a );
00294                 CPPUNIT_ASSERT_EQUAL(true, vsids->select(s));
00295                 CPPUNIT_ASSERT_EQUAL(true, s.trail().back() == ~a && s.propagate());
00296                 CPPUNIT_ASSERT_EQUAL(true, vsids->select(s));
00297                 CPPUNIT_ASSERT_EQUAL(true, s.trail().back() == ~b && s.propagate());
00298                 CPPUNIT_ASSERT_EQUAL(false, vsids->select(s));
00299         }
00300         void testVsidsAux() {
00301                 ClaspVsids* vsids = new ClaspVsids;
00302                 SharedContext ctx;
00303                 ctx.master()->heuristic().reset(vsids);
00304                 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00305                 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00306                 Solver& s = ctx.startAddConstraints();
00307                 ctx.endInit();
00308                 Var v = s.pushAuxVar();
00309                 LitVec up;
00310                 vsids->updateReason(s,up,posLit(v));
00311                 CPPUNIT_ASSERT_EQUAL(true, vsids->select(s));
00312                 CPPUNIT_ASSERT(s.value(v) != value_free);
00313                 s.popAuxVar(1);
00314                 CPPUNIT_ASSERT_EQUAL(true, vsids->select(s));
00315                 CPPUNIT_ASSERT(s.trail().back().var() != v);
00316         }
00317 
00318         void testStrangeLookSeq() {
00319                 SharedContext ctx;
00320                 Literal a = posLit(ctx.addVar(Var_t::body_var));
00321                 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00322                 Solver& s = ctx.startAddConstraints();
00323                 s.heuristic().reset(UnitHeuristic::restricted(Lookahead::body_lookahead, 3, s.heuristic().release()));
00324                 ctx.endInit();
00325                 s.force(a);
00326                 s.simplify();
00327                 bool x = s.decideNextBranch();
00328                 CPPUNIT_ASSERT(x == true && s.value(b.var()) != value_free);
00329         }
00330 
00331         void testStrangeLookSeq2() {
00332                 SharedContext ctx;
00333                 ctx.master()->heuristic().reset(UnitHeuristic::restricted(Lookahead::atom_lookahead, 2, new SelectFirst));
00334                 Literal a = posLit(ctx.addVar(Var_t::atom_var));
00335                 Literal b = posLit(ctx.addVar(Var_t::atom_var));
00336                 Solver& s = ctx.startAddConstraints();
00337                 ctx.addBinary(a, b);
00338                 ctx.addBinary(a, ~b);
00339                 ctx.addBinary(~a, b);
00340                 ctx.endInit();
00341                 bool x = ctx.master()->decideNextBranch();
00342                 CPPUNIT_ASSERT(x == false && s.decisionLevel() == 0 && s.numFreeVars() == 0);
00343         }
00344 
00345         void testResurrect() {
00346                 /*
00347                 typedef std::pair<const char*, DecisionHeuristic*> Heu;
00348                 Heu heus[3] = {
00349                         Heu("Berkmin", new ClaspBerkmin()),
00350                         Heu("Vmtf", new ClaspVmtf()),
00351                         Heu("Vsids", new ClaspVsids())
00352                 };
00353                 for (uint32 i = 0; i != 3; ++i) {
00354                         SharedContext ctx;
00355                         ctx.master()->strategy.heuristic.reset(heus[i].second);
00356                         Var v1 = ctx.addVar(Var_t::atom_var);
00357                         Var v2 = ctx.addVar(Var_t::atom_var);
00358                         Var v3 = ctx.addVar(Var_t::atom_var);
00359                         ctx.startAddConstraints();
00360                         ctx.endInit();
00361                         Solver& s = *ctx.master();
00362                         s.eliminate(v1, true);
00363                         while (s.strategy.heuristic->select(s) && s.propagate()) { ; }
00364                         CPPUNIT_ASSERT(2u == s.stats.choices);
00365                         CPPUNIT_ASSERT_EQUAL_MESSAGE(heus[i].first, 0u, s.numFreeVars());
00366                         s.eliminate(v1, false);
00367                         CPPUNIT_ASSERT_EQUAL(value_free, s.value(v1));
00368                         CPPUNIT_ASSERT_EQUAL_MESSAGE(heus[i].first, true, s.strategy.heuristic->select(s));
00369                         CPPUNIT_ASSERT_MESSAGE(heus[i].first, value_free != s.value(v1));
00370                 }
00371                 */
00372                 CPPUNIT_FAIL("TODO - Resurrection not yet supported!");
00373         }
00374 
00375         void testDomSignPos() {
00376                 DomainHeuristic* dom = new DomainHeuristic;
00377                 SharedContext ctx;
00378                 ctx.master()->heuristic().reset(dom);
00379                 Solver& s = *ctx.master();
00380                 LogicProgram api;
00381                 api.start(ctx).setAtomName(1, "a").startRule(Asp::CHOICERULE).addHead(1).endRule();
00382                 addDomRule(api, "_heuristic(a,sign,1)");
00383                 CPPUNIT_ASSERT_EQUAL(true, api.endProgram() && ctx.endInit());
00384                 
00385                 CPPUNIT_ASSERT(dom->select(s));
00386                 CPPUNIT_ASSERT(s.trail().back() == api.getAtom(1)->literal());
00387         }
00388         void testDomSignNeg() {
00389                 DomainHeuristic* dom = new DomainHeuristic;
00390                 SharedContext ctx;
00391                 ctx.master()->heuristic().reset(dom);
00392                 Solver& s = *ctx.master();
00393                 LogicProgram api;
00394                 api.start(ctx).setAtomName(1, "a").startRule(Asp::CHOICERULE).addHead(1).endRule();
00395                 addDomRule(api, "_heuristic(a,sign,-1)");
00396                 CPPUNIT_ASSERT_EQUAL(true, api.endProgram() && ctx.endInit());
00397                 
00398                 CPPUNIT_ASSERT(dom->select(s));
00399                 CPPUNIT_ASSERT(s.trail().back() == ~api.getAtom(1)->literal());
00400         }
00401         void testDomLevel() {
00402                 DomainHeuristic* dom = new DomainHeuristic;
00403                 SharedContext ctx;
00404                 ctx.master()->heuristic().reset(dom);
00405                 Solver& s = *ctx.master();
00406                 LogicProgram api;
00407                 api.start(ctx).setAtomName(1, "a").setAtomName(2,"b").startRule(Asp::CHOICERULE).addHead(1).addHead(2).endRule();
00408                 addDomRule(api, "_heuristic(a,sign,1)");
00409                 addDomRule(api, "_heuristic(b,sign,1)");
00410                 addDomRule(api, "_heuristic(a,level,10)");
00411                 CPPUNIT_ASSERT_EQUAL(true, api.endProgram() && ctx.endInit());
00412                 
00413                 CPPUNIT_ASSERT(dom->select(s));
00414                 CPPUNIT_ASSERT(s.trail().back() == api.getAtom(1)->literal());
00415         }
00416 
00417         void testDomDynamic() {
00418                 DomainHeuristic* dom = new DomainHeuristic;
00419                 SharedContext ctx;
00420                 ctx.master()->heuristic().reset(dom);
00421                 Solver& s = *ctx.master();
00422                 LogicProgram api;
00423                 api.start(ctx)
00424                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c")
00425                         .startRule(Asp::CHOICERULE).addHead(1).addHead(2).addHead(3).endRule()
00426                         .startRule().addHead(4).addToBody(1, true).addToBody(2,true).endRule()
00427                         .setCompute(4, false);
00428                 addDomRule(api, "_heuristic(a,sign,1)");
00429                 addDomRule(api, "_heuristic(b,sign,1)");
00430                 addDomRule(api, "_heuristic(a,level,10)");
00431                 addDomRule(api, "_heuristic(c,sign,1)", posLit(2));
00432                 addDomRule(api, "_heuristic(c,sign,-1)", negLit(2));
00433                 CPPUNIT_ASSERT_EQUAL(true, api.endProgram() && ctx.endInit());
00434                 CPPUNIT_ASSERT(dom->select(s));
00435                 CPPUNIT_ASSERT(s.trail().back() == api.getAtom(1)->literal());
00436                 s.propagate();
00437                 CPPUNIT_ASSERT(s.isFalse(api.getAtom(2)->literal()));
00438                 CPPUNIT_ASSERT(dom->select(s));
00439                 CPPUNIT_ASSERT(s.trail().back() == ~api.getAtom(3)->literal());
00440                 s.clearAssumptions();
00441                 uint32 n = s.numWatches(posLit(2));
00442                 // test removal of watches
00443                 ctx.master()->heuristic().reset(new SelectFirst());
00444                 CPPUNIT_ASSERT_MESSAGE("Heuristic not detached", s.numWatches(posLit(2)) != n);
00445         }
00446 
00447         void testDomPrio() {
00448                 DomainHeuristic* dom = new DomainHeuristic;
00449                 SharedContext ctx;
00450                 ctx.master()->heuristic().reset(dom);
00451                 Solver& s = *ctx.master();
00452                 LogicProgram api;
00453                 api.start(ctx)
00454                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c")
00455                         .startRule(Asp::CHOICERULE).addHead(1).addHead(2).addHead(3).endRule()
00456                         .startRule().addHead(4).addToBody(1, true).addToBody(2,true).endRule()
00457                         .setCompute(4, false);
00458                 addDomRule(api, "_heuristic(b,sign,1)");
00459                 addDomRule(api, "_heuristic(a,true,10)");
00460                 addDomRule(api, "_heuristic(c,sign,1,10)");
00461                 addDomRule(api, "_heuristic(c,sign,-1,20)", negLit(2));
00462                 CPPUNIT_ASSERT_EQUAL(true, api.endProgram() && ctx.endInit());
00463                 CPPUNIT_ASSERT(dom->select(s));
00464                 CPPUNIT_ASSERT(s.trail().back() == api.getAtom(1)->literal());
00465                 s.propagate();
00466                 CPPUNIT_ASSERT(s.isFalse(api.getAtom(2)->literal()));
00467                 CPPUNIT_ASSERT(dom->select(s));
00468                 CPPUNIT_ASSERT(s.trail().back() == ~api.getAtom(3)->literal());
00469         }
00470         void testDomPrio2() {
00471                 DomainHeuristic* dom = new DomainHeuristic;
00472                 SharedContext ctx;
00473                 ctx.master()->heuristic().reset(dom);
00474                 Solver& s = *ctx.master();
00475                 LogicProgram api;
00476                 api.start(ctx)
00477                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c")
00478                         .startRule(Asp::CHOICERULE).addHead(1).addHead(2).addHead(3).endRule()
00479                         .startRule().addHead(4).addToBody(1, true).addToBody(2,true).endRule()
00480                         .setCompute(4, false);
00481                 addDomRule(api, "_heuristic(b,sign,1)");
00482                 addDomRule(api, "_heuristic(a,true,10)");
00483                 addDomRule(api, "_heuristic(c,sign,1,30)");
00484                 addDomRule(api, "_heuristic(c,sign,-1,20)", negLit(2));
00485                 CPPUNIT_ASSERT_EQUAL(true, api.endProgram() && ctx.endInit());
00486                 CPPUNIT_ASSERT(dom->select(s));
00487                 CPPUNIT_ASSERT(s.trail().back() == api.getAtom(1)->literal());
00488                 s.propagate();
00489                 CPPUNIT_ASSERT(s.isFalse(api.getAtom(2)->literal()));
00490                 CPPUNIT_ASSERT(dom->select(s));
00491                 CPPUNIT_ASSERT(s.trail().back() == api.getAtom(3)->literal());
00492         }
00493         void testDomInit() {
00494                 DomainHeuristic* dom = new DomainHeuristic;
00495                 SharedContext ctx;
00496                 ctx.master()->heuristic().reset(dom);
00497                 Solver& s = *ctx.master();
00498                 LogicProgram api;
00499                 api.start(ctx)
00500                         .setAtomName(1, "a").setAtomName(2, "b")
00501                         .startRule(Asp::CHOICERULE).addHead(1).addHead(2).endRule();
00502                 addDomRule(api, "_heuristic(a,init,10,20)");
00503                 addDomRule(api, "_heuristic(a,init,50,10)");
00504                 addDomRule(api, "_heuristic(b,init,10,10)");
00505                 addDomRule(api, "_heuristic(b,init,30,20)");
00506                 CPPUNIT_ASSERT_EQUAL(true, api.endProgram() && ctx.endInit());
00507                 CPPUNIT_ASSERT(dom->select(s));
00508                 CPPUNIT_ASSERT(s.trail().back().var() == api.getAtom(2)->var());
00509         }
00510         void testDomInc() {
00511                 SharedContext ctx;
00512                 Solver& s = *ctx.master();
00513                 LogicProgram api;
00514                 api.start(ctx).updateProgram();
00515                 api.setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "x").setAtomName(4, "y")
00516                         .startRule(Asp::CHOICERULE).addHead(1).addHead(2).addHead(3).addHead(4).endRule();
00517                 addDomRule(api, "_heuristic(a,level,1)", posLit(3));
00518                 addDomRule(api, "_heuristic(b,level,1)", posLit(4));
00519                 CPPUNIT_ASSERT_EQUAL(true, api.endProgram() && ctx.endInit());
00520                 uint32 n = s.numWatches(posLit(3));
00521                 DomainHeuristic* dom = new DomainHeuristic;
00522                 dom->startInit(s);
00523                 dom->endInit(s);
00524                 CPPUNIT_ASSERT(s.numWatches(posLit(3)) > n);
00525                 CPPUNIT_ASSERT(api.updateProgram());
00526                 Var c = api.newAtom();
00527                 api.setAtomName(c, "c").startRule(Asp::CHOICERULE).addHead(c).endRule();
00528                 addDomRule(api, "_heuristic(c,level,1)", posLit(3));
00529                 CPPUNIT_ASSERT_EQUAL(true, api.endProgram() && ctx.endInit());
00530                 dom->startInit(s);
00531                 dom->endInit(s);
00532                 delete dom;
00533                 CPPUNIT_ASSERT_MESSAGE("Heuristic not detached", s.numWatches(posLit(3)) == n);
00534         }
00535         void addDomRule(LogicProgram& prg, const char* heu, Literal pre = posLit(0)) {
00536                 Var h = prg.newAtom();
00537                 prg.setAtomName(h, heu);
00538                 prg.startRule().addHead(h);
00539                 if (pre != posLit(0)) prg.addToBody(pre.var(), pre.sign() == false);
00540                 prg.endRule();
00541         }
00542 };
00543 
00544 CPPUNIT_TEST_SUITE_REGISTRATION(DecisionHeuristicTest);
00545 
00546 } }

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