unfounded_check_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/unfounded_check.h>
00022 #include <clasp/program_builder.h>
00023 #include <clasp/clause.h>
00024 #include <memory>
00025 
00026 namespace Clasp { namespace Test {
00027         using namespace Clasp::Asp;
00028         class UnfoundedCheckTest : public CppUnit::TestFixture {
00029         CPPUNIT_TEST_SUITE(UnfoundedCheckTest);
00030         CPPUNIT_TEST(testAllUncoloredNoUnfounded);
00031         CPPUNIT_TEST(testAlternativeSourceNotUnfounded);
00032         CPPUNIT_TEST(testOnlyOneSourceUnfoundedIfMinus);
00033         
00034         CPPUNIT_TEST(testWithSimpleCardinalityConstraint);
00035         CPPUNIT_TEST(testWithSimpleWeightConstraint);
00036         
00037         CPPUNIT_TEST(testNtExtendedBug);
00038         CPPUNIT_TEST(testNtExtendedFalse);
00039         
00040         CPPUNIT_TEST(testDependentExtReason);
00041         CPPUNIT_TEST(testEqBodyDiffType);
00042         CPPUNIT_TEST(testChoiceCardInterplay);
00043         CPPUNIT_TEST(testCardInterplayOnBT);
00044 
00045         CPPUNIT_TEST(testInitNoSource);
00046 
00047         CPPUNIT_TEST(testIncrementalUfs);
00048         CPPUNIT_TEST(testInitialStopConflict);
00049         CPPUNIT_TEST(testIncrementalLearnFact);
00050 
00051         CPPUNIT_TEST(testApproxUfs);
00052         CPPUNIT_TEST_SUITE_END(); 
00053 public:
00054         class WrapDefaultUnfoundedCheck : public DefaultUnfoundedCheck {
00055         public:
00056                 bool propagate(Solver& s) { return DefaultUnfoundedCheck::propagateFixpoint(s, 0); }
00057         };
00058         UnfoundedCheckTest() : ufs(0) { }
00059         void setUp() { 
00060                 ufs   = new WrapDefaultUnfoundedCheck();
00061         }
00062         void tearDown() {
00063                 ufs   = 0;
00064         }
00065         Solver& solver() { return *ctx.master(); }
00066         void testAllUncoloredNoUnfounded() {
00067                 setupSimpleProgram();
00068                 uint32 x = solver().numAssignedVars();
00069                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()));
00070                 CPPUNIT_ASSERT_EQUAL(x, solver().numAssignedVars());
00071         }
00072         
00073         void testAlternativeSourceNotUnfounded() {
00074                 setupSimpleProgram();
00075                 solver().assume( ctx.symbolTable()[6].lit );
00076                 solver().propagateUntil(ufs.get());
00077                 uint32 old = solver().numAssignedVars();
00078                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()));
00079                 CPPUNIT_ASSERT_EQUAL(old, solver().numAssignedVars());
00080         }
00081         
00082         void testOnlyOneSourceUnfoundedIfMinus() {
00083                 setupSimpleProgram();
00084                 solver().assume( ctx.symbolTable()[6].lit );
00085                 solver().assume( ctx.symbolTable()[5].lit );
00086                 solver().propagateUntil(ufs.get());
00087                 uint32 old = solver().numAssignedVars();
00088                 uint32 oldC = ctx.numConstraints();
00089                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()));
00090                 CPPUNIT_ASSERT(old < solver().numAssignedVars());
00091                 CPPUNIT_ASSERT(solver().isFalse(ctx.symbolTable()[4].lit));
00092                 CPPUNIT_ASSERT(solver().isFalse(ctx.symbolTable()[1].lit));
00093                 CPPUNIT_ASSERT(!solver().isFalse(ctx.symbolTable()[2].lit));
00094                 CPPUNIT_ASSERT(oldC+1 == ctx.numConstraints() + ctx.numLearntShort());
00095         }
00096         
00097         void testWithSimpleCardinalityConstraint() {
00098                 builder.start(ctx)
00099                         .setAtomName(1, "a").setAtomName(2, "b")
00100                         .startRule(CHOICERULE).addHead(2).endRule()
00101                         .startRule(CONSTRAINTRULE, 1).addHead(1).addToBody(1, true).addToBody(2,true).endRule()
00102                 ;
00103                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00104                 attachUfs();
00105                 
00106                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00107                 CPPUNIT_ASSERT_EQUAL(2u, solver().numVars());
00108                 CPPUNIT_ASSERT_EQUAL(0u, solver().numAssignedVars());
00109                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()) );
00110                 CPPUNIT_ASSERT_EQUAL(0u, solver().numAssignedVars());
00111                 CPPUNIT_ASSERT_EQUAL(true, solver().assume(~ctx.symbolTable()[2].lit));
00112                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00113                 CPPUNIT_ASSERT_EQUAL(1u, solver().numAssignedVars());
00114                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()) );
00115                 CPPUNIT_ASSERT_EQUAL(2u, solver().numAssignedVars());
00116                 LitVec r;
00117                 solver().reason(~ctx.symbolTable()[1].lit, r);
00118                 CPPUNIT_ASSERT(1 == r.size());
00119                 CPPUNIT_ASSERT(r[0] == ~ctx.symbolTable()[2].lit);
00120         }
00121         void testWithSimpleWeightConstraint() {
00122                 builder.start(ctx)
00123                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c")
00124                         .startRule(CHOICERULE).addHead(2).addHead(3).endRule()
00125                         .startRule(WEIGHTRULE, 2).addHead(1).addToBody(1, true, 2).addToBody(2,true, 2).addToBody(3, true, 1).endRule()
00126                 ;
00127                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00128                 attachUfs();
00129                 
00130                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00131                 CPPUNIT_ASSERT_EQUAL(3u, solver().numVars());
00132                 CPPUNIT_ASSERT_EQUAL(0u, solver().numAssignedVars());
00133                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()) );
00134                 CPPUNIT_ASSERT_EQUAL(0u, solver().numAssignedVars());
00135                 CPPUNIT_ASSERT_EQUAL(true, solver().assume(~ctx.symbolTable()[3].lit));
00136                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00137                 CPPUNIT_ASSERT_EQUAL(1u, solver().numAssignedVars());
00138                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()) );
00139                 CPPUNIT_ASSERT_EQUAL(1u, solver().numAssignedVars());
00140 
00141                 CPPUNIT_ASSERT_EQUAL(true, solver().assume(~ctx.symbolTable()[2].lit));
00142                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00143                 CPPUNIT_ASSERT_EQUAL(2u, solver().numAssignedVars());
00144 
00145                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()) );
00146                 CPPUNIT_ASSERT_EQUAL(3u, solver().numAssignedVars());
00147                 
00148                 LitVec r;
00149                 solver().reason(~ctx.symbolTable()[1].lit, r);
00150                 CPPUNIT_ASSERT(2 == r.size());
00151                 CPPUNIT_ASSERT(r[0] == ~ctx.symbolTable()[2].lit);
00152                 CPPUNIT_ASSERT(r[1] == ~ctx.symbolTable()[3].lit);
00153 
00154                 solver().undoUntil(0);
00155                 CPPUNIT_ASSERT_EQUAL(true, solver().assume(~ctx.symbolTable()[2].lit));
00156                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00157                 CPPUNIT_ASSERT_EQUAL(1u, solver().numAssignedVars());
00158                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()) );
00159                 CPPUNIT_ASSERT_EQUAL(2u, solver().numAssignedVars());
00160                 r.clear();
00161                 solver().reason(~ctx.symbolTable()[1].lit, r);
00162                 CPPUNIT_ASSERT(1 == r.size());
00163                 CPPUNIT_ASSERT(r[0] == ~ctx.symbolTable()[2].lit);
00164         }
00165         
00166         void testNtExtendedBug() {
00167                 builder.start(ctx)
00168                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c").setAtomName(4, "t").setAtomName(5, "x")
00169                         .startRule(CHOICERULE).addHead(1).addHead(2).addHead(3).endRule() // {a,b,c}.
00170                         .startRule(CONSTRAINTRULE, 2).addHead(4).addToBody(2, true).addToBody(4, true).addToBody(5,true).endRule()
00171                         .startRule().addHead(5).addToBody(4,true).addToBody(3,true).endRule()
00172                         .startRule().addHead(5).addToBody(1,true).endRule()
00173                 ;
00174                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00175                 attachUfs();
00176                 
00177                 // T: {t,c}
00178                 solver().assume(Literal(6, false));
00179                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00180                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()));
00181                 solver().assume(~ctx.symbolTable()[1].lit);
00182                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00183                 CPPUNIT_ASSERT_EQUAL(false, ufs->propagate(solver()));  // {x, t} are unfounded!
00184                 
00185                 solver().undoUntil(0);
00186                 ufs->reset();
00187 
00188                 // F: {t,c}
00189                 solver().assume(Literal(6, true));
00190                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00191                 // F: a
00192                 solver().assume(~ctx.symbolTable()[1].lit);
00193                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00194                 // x is false because both of its bodies are false
00195                 CPPUNIT_ASSERT_EQUAL(true, solver().isFalse(ctx.symbolTable()[5].lit));
00196         
00197                 // t is now unfounded but its defining body is not
00198                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()));
00199                 CPPUNIT_ASSERT_EQUAL(true, solver().isFalse(ctx.symbolTable()[4].lit));
00200                 LitVec r;
00201                 solver().reason(~ctx.symbolTable()[4].lit, r);
00202                 CPPUNIT_ASSERT(r.size() == 1 && r[0] == ~ctx.symbolTable()[5].lit);
00203         }
00204         
00205         void testNtExtendedFalse() {
00206                 // {z}.
00207                 // r :- 2 {x, y, s}
00208                 // s :- r, z.
00209                 // r :- s, z.
00210                 // x :- not z.
00211                 // y :- not z.
00212                 builder.start(ctx, LogicProgram::AspOptions().noEq())
00213                         .setAtomName(1, "x").setAtomName(2, "y").setAtomName(3, "z").setAtomName(4, "r").setAtomName(5, "s")
00214                         .startRule(CHOICERULE).addHead(3).endRule() // {z}.
00215                         .startRule().addHead(1).addToBody(3,false).endRule()
00216                         .startRule().addHead(2).addToBody(3,false).endRule()
00217                         .startRule(CONSTRAINTRULE, 2).addHead(4).addToBody(1, true).addToBody(2, true).addToBody(5,true).endRule()
00218                         .startRule().addHead(5).addToBody(4,true).addToBody(3,true).endRule()
00219                         .startRule().addHead(4).addToBody(5,true).addToBody(3,true).endRule()
00220                 ;
00221                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00222                 attachUfs();
00223                 
00224                 solver().assume(ctx.symbolTable()[3].lit);
00225                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00226                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()));
00227                 CPPUNIT_ASSERT(solver().numVars() == solver().numAssignedVars());
00228                 CPPUNIT_ASSERT_EQUAL(true, solver().isFalse(ctx.symbolTable()[4].lit));
00229                 CPPUNIT_ASSERT_EQUAL(true, solver().isFalse(ctx.symbolTable()[5].lit));
00230 
00231                 solver().backtrack();
00232                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00233                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()));
00234                 CPPUNIT_ASSERT(solver().numVars() == solver().numAssignedVars());
00235                 CPPUNIT_ASSERT_EQUAL(true, solver().isTrue(ctx.symbolTable()[4].lit));
00236                 CPPUNIT_ASSERT_EQUAL(true, solver().isFalse(ctx.symbolTable()[5].lit));
00237         }
00238 
00239         void testDependentExtReason() {
00240                 // {z, q, r}.
00241                 // x :- not q.
00242                 // x :- 2 {x, y, z}.
00243                 // x :- y, z.
00244                 // y :- x, r.
00245                 builder.start(ctx, LogicProgram::AspOptions().noEq())
00246                         .setAtomName(1, "x").setAtomName(2, "y").setAtomName(3, "z").setAtomName(4, "q").setAtomName(5, "r")
00247                         .startRule(CHOICERULE).addHead(3).addHead(4).addHead(5).endRule()
00248                         .startRule().addHead(1).addToBody(4,false).endRule()
00249                         .startRule(CONSTRAINTRULE, 2).addHead(1).addToBody(1, true).addToBody(2, true).addToBody(3, true).endRule()
00250                         .startRule().addHead(1).addToBody(2,true).addToBody(3, true).endRule()
00251                         .startRule().addHead(2).addToBody(1,true).addToBody(5, true).endRule()
00252                 ;
00253                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00254                 attachUfs();
00255                 
00256                 // assume ~B1, where B1 = 2 {x, y, z}
00257                 const SharedDependencyGraph::AtomNode& a = ufs->graph()->getAtom(builder.getAtom(1)->id());
00258                 Literal x = ufs->graph()->getBody(a.body(1)).lit;
00259 
00260                 solver().assume(~x);
00261                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()) && ufs->propagate(solver()));
00262                 CPPUNIT_ASSERT_EQUAL(value_free, solver().value(ctx.symbolTable()[1].lit.var()));
00263                 CPPUNIT_ASSERT_EQUAL(value_free, solver().value(ctx.symbolTable()[2].lit.var()));
00264                 // B1
00265                 CPPUNIT_ASSERT_EQUAL(1u, solver().numAssignedVars());
00266                 
00267                 // assume q
00268                 solver().assume(ctx.symbolTable()[4].lit);
00269                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00270                 // B1 + q (hence {not q})
00271                 CPPUNIT_ASSERT_EQUAL(2u, solver().numAssignedVars());
00272 
00273                 // U = {x, y}.
00274                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()));
00275                 CPPUNIT_ASSERT_EQUAL(true, solver().isFalse(ctx.symbolTable()[1].lit));
00276                 CPPUNIT_ASSERT_EQUAL(true, solver().isFalse(ctx.symbolTable()[2].lit));
00277                 Literal extBody = ufs->graph()->getBody(a.body(0)).lit;
00278                 LitVec r;
00279                 solver().reason(~ctx.symbolTable()[1].lit, r);
00280                 CPPUNIT_ASSERT(r.size() == 1u && r[0] == ~extBody);
00281         }
00282 
00283         void testEqBodyDiffType() { 
00284                 builder.start(ctx)
00285                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c").setAtomName(4, "x").setAtomName(5,"y")
00286                         .startRule(CHOICERULE).addHead(1).addHead(4).addHead(5).endRule()
00287                         .startRule(CHOICERULE).addHead(2).addToBody(1,true).endRule()
00288                         .startRule().addHead(3).addToBody(1,true).endRule()
00289                         .startRule().addHead(2).addToBody(3,true).addToBody(4, true).endRule()
00290                         .startRule().addHead(3).addToBody(2,true).addToBody(5,true).endRule()
00291                 .endProgram();
00292                 CPPUNIT_ASSERT(builder.stats.sccs == 1);
00293                 attachUfs();
00294                 
00295                 solver().assume(~ctx.symbolTable()[1].lit);
00296                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00297                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()));
00298                 CPPUNIT_ASSERT_EQUAL(true, solver().isFalse(ctx.symbolTable()[2].lit));
00299                 CPPUNIT_ASSERT_EQUAL(true, solver().isFalse(ctx.symbolTable()[3].lit));
00300         }
00301 
00302         void testChoiceCardInterplay() {  
00303                 builder.start(ctx, LogicProgram::AspOptions().noEq())
00304                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c").setAtomName(4, "x")
00305                         .startRule(CHOICERULE).addHead(4).endRule() // {x}.
00306                         .startRule(CHOICERULE).addHead(1).addToBody(4, true).endRule()  // {a} :- x.
00307                         .startRule(CONSTRAINTRULE,1).addHead(2).addToBody(1, true).addToBody(3, true).endRule() // b :- 1{a,c}
00308                         .startRule().addHead(3).addToBody(2,true).endRule() // c :- b.
00309                         .startRule(CHOICERULE).addHead(1).addToBody(3,true).endRule() // {a} :- c.
00310                 .endProgram();
00311                 CPPUNIT_ASSERT(builder.stats.sccs == 1);
00312                 attachUfs();
00313                 
00314                 solver().assume(~ctx.symbolTable()[1].lit);
00315                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00316                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()));
00317                 CPPUNIT_ASSERT_EQUAL(true, solver().isFalse(ctx.symbolTable()[2].lit));
00318                 CPPUNIT_ASSERT_EQUAL(true, solver().isFalse(ctx.symbolTable()[3].lit));
00319         }
00320 
00321         void testCardInterplayOnBT() {  
00322                 builder.start(ctx, LogicProgram::AspOptions().noEq())
00323                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c").setAtomName(4, "d").setAtomName(5,"z")
00324                         .startRule(CHOICERULE).addHead(1).addHead(5).endRule()                                  // {a,z}.
00325                         .startRule(CONSTRAINTRULE,1).addHead(2).addToBody(1, true).addToBody(3, true).endRule() // b :- 1{a,c}
00326                         .startRule(BASICRULE).addHead(2).addToBody(4, true).endRule()                           // b :- d.
00327                         .startRule(BASICRULE).addHead(4).addToBody(2, true).endRule()                           // d :- b.
00328                         .startRule(BASICRULE).addHead(4).addToBody(5, true).endRule()                           // d :- z.
00329                         .startRule(BASICRULE).addHead(3).addToBody(2,true).addToBody(4,true).endRule()          // c :- b,d.      
00330                 .endProgram();
00331                 CPPUNIT_ASSERT(builder.stats.sccs == 1);
00332                 attachUfs();
00333                 
00334                 solver().assume(~ctx.symbolTable()[1].lit);
00335                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()) && ufs->propagate(solver()));
00336                 CPPUNIT_ASSERT_EQUAL(false, solver().isFalse(ctx.symbolTable()[2].lit));
00337                 CPPUNIT_ASSERT_EQUAL(false, solver().isFalse(ctx.symbolTable()[3].lit));
00338                 solver().undoUntil(0);
00339                 
00340                 solver().assume(~ctx.symbolTable()[5].lit);
00341                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()) && ufs->propagate(solver()));
00342                 CPPUNIT_ASSERT_EQUAL(false, solver().isFalse(ctx.symbolTable()[2].lit));
00343                 CPPUNIT_ASSERT_EQUAL(false, solver().isFalse(ctx.symbolTable()[3].lit));
00344         }
00345         
00346         void testInitNoSource() {
00347                 builder.start(ctx, LogicProgram::AspOptions().noEq())
00348                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "x")
00349                         .startRule(CHOICERULE).addHead(3).endRule()                                  // {x}.
00350                         .startRule(CHOICERULE).addHead(1).addHead(2).addToBody(3, true).endRule()    // {a,b} :- x.
00351                         .startRule(BASICRULE).addHead(1).addToBody(2, true).endRule()                // a :- b.
00352                         .startRule(BASICRULE).addHead(2).addToBody(1, true).endRule()                // b :- a.
00353                 .endProgram();
00354                 CPPUNIT_ASSERT(builder.stats.sccs == 1);
00355                 
00356                 solver().force(~ctx.symbolTable()[3].lit);
00357                 attachUfs();
00358                 CPPUNIT_ASSERT(solver().isFalse(ctx.symbolTable()[1].lit));
00359         }
00360 
00361         void testIncrementalUfs() {
00362                 builder.start(ctx, LogicProgram::AspOptions().noEq());
00363                 // I1:
00364                 // a :- not b.
00365                 // b :- not a.
00366                 // freeze(c).
00367                 builder.updateProgram();
00368                 builder.setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c")
00369                         .startRule().addHead(1).addToBody(2, false).endRule()
00370                         .startRule().addHead(2).addToBody(1, false).endRule()
00371                         .freeze(3)
00372                 ;
00373                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram() && ctx.endInit());
00374                 CPPUNIT_ASSERT(ctx.sccGraph.get() == 0);
00375                 
00376                 // I2:
00377                 // {c, z}
00378                 // x :- not c.
00379                 // x :- y, z.
00380                 // y :- x, z.
00381                 builder.updateProgram();
00382                 builder.setAtomName(4, "x").setAtomName(5, "y").setAtomName(6, "z")
00383                         .startRule(CHOICERULE).addHead(3).addHead(6).endRule()
00384                         .startRule().addHead(4).addToBody(3, false).endRule()
00385                         .startRule().addHead(4).addToBody(5, true).addToBody(6, true).endRule()
00386                         .startRule().addHead(5).addToBody(4, true).addToBody(6, true).endRule()
00387                         .unfreeze(3)
00388                 ;
00389                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00390                 CPPUNIT_ASSERT(6u == ctx.sccGraph.get()->nodes());
00391                 CPPUNIT_ASSERT(1 == builder.stats.sccs);
00392                 attachUfs();
00393                 CPPUNIT_ASSERT(6u == ufs->nodes());
00394 
00395                 // I3:
00396                 // a :- x, not r.
00397                 // r :- not a.
00398                 // a :- b.
00399                 // b :- a, not z.
00400                 builder.updateProgram();
00401                 builder.setAtomName(7, "a").setAtomName(8, "b").setAtomName(9, "r")
00402                         .startRule().addHead(7).addToBody(4, true).addToBody(9, false).endRule()
00403                         .startRule().addHead(9).addToBody(7, false).endRule()
00404                         .startRule().addHead(7).addToBody(8, true).endRule()
00405                         .startRule().addHead(8).addToBody(7, true).addToBody(6, false).endRule()
00406                 ;
00407                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00408                 CPPUNIT_ASSERT(11u == ctx.sccGraph.get()->nodes());
00409                 CPPUNIT_ASSERT(1 == builder.stats.sccs);
00410                 ctx.endInit();
00411                 CPPUNIT_ASSERT(11u == ufs->nodes());
00412                 CPPUNIT_ASSERT(builder.getAtom(7)->scc() != builder.getAtom(4)->scc());
00413         }
00414 
00415         void testInitialStopConflict() {
00416                 builder.start(ctx);
00417                 // I1:
00418                 // {x,y}.
00419                 // a :- {x, y}.
00420                 // a :- b,y.
00421                 // b :- a,y.
00422                 builder.setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "x").setAtomName(4, "y")
00423                         .startRule(CHOICERULE).addHead(3).addHead(4).endRule()
00424                         .startRule().addHead(1).addToBody(3, true).addToBody(4, true).endRule()
00425                         .startRule().addHead(1).addToBody(2, true).addToBody(4, true).endRule()
00426                         .startRule().addHead(2).addToBody(1, true).addToBody(4, true).endRule()
00427                 ;
00428                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00429                 CPPUNIT_ASSERT(builder.stats.sccs == 1);
00430                 struct M : PostPropagator {                     
00431                         uint32 priority() const { return priority_reserved_msg; }
00432                         bool propagateFixpoint(Solver& s, PostPropagator*) {
00433                                 s.setStopConflict();
00434                                 return false;
00435                         }
00436                 } m;
00437                 solver().addPost(&m);
00438                 ctx.addUnary(~builder.getAtom(3)->literal());
00439                 attachUfs();
00440                 CPPUNIT_ASSERT(solver().hasStopConflict());
00441                 solver().removePost(&m);
00442                 solver().popRootLevel();
00443                 solver().propagate();
00444                 CPPUNIT_ASSERT(solver().isFalse(builder.getAtom(3)->literal()));
00445                 CPPUNIT_ASSERT(solver().isFalse(builder.getAtom(1)->literal()) && solver().isFalse(builder.getAtom(2)->literal()));
00446         }
00447 
00448         void testIncrementalLearnFact() {
00449                 builder.start(ctx);
00450                 builder.update();
00451                 // I1:
00452                 // {x,y}.
00453                 // a :- {x, y}.
00454                 // a :- b,y.
00455                 // b :- a,y.
00456                 builder.setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "x").setAtomName(4, "y")
00457                         .startRule(CHOICERULE).addHead(3).addHead(4).endRule()
00458                         .startRule().addHead(1).addToBody(3, true).addToBody(4, true).endRule()
00459                         .startRule().addHead(1).addToBody(2, true).addToBody(4, true).endRule()
00460                         .startRule().addHead(2).addToBody(1, true).addToBody(4, true).endRule()
00461                 ;
00462                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00463                 attachUfs();
00464                 builder.update();
00465                 builder.endProgram();
00466                 ctx.addUnary(~builder.getAtom(3)->literal());
00467                 CPPUNIT_ASSERT(solver().propagate());
00468                 CPPUNIT_ASSERT(ctx.endInit());
00469                 CPPUNIT_ASSERT(solver().isFalse(builder.getAtom(3)->literal()));
00470                 CPPUNIT_ASSERT(solver().isFalse(builder.getAtom(1)->literal()) && solver().isFalse(builder.getAtom(2)->literal()));
00471         }
00472 
00473         void testApproxUfs() {
00474                 builder.start(ctx)
00475                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c").setAtomName(4, "d").setAtomName(5,"e")
00476                         .startRule(DISJUNCTIVERULE).addHead(1).addHead(2).endRule() // a | b.
00477                         .startRule(DISJUNCTIVERULE).addHead(3).addHead(4).endRule() // c | d.
00478                         .startRule(DISJUNCTIVERULE).addHead(3).addHead(5).addToBody(2, true).endRule() // c | e :- b.
00479                         .startRule(DISJUNCTIVERULE).addHead(2).addHead(4).addToBody(3, true).endRule() // b | d :- c.
00480                         .startRule().addHead(3).addToBody(4,true).addToBody(2, false).endRule() // c :- d, not b.
00481                         .startRule().addHead(3).addToBody(5,true).endRule()                     // c :- e.
00482                         .startRule().addHead(4).addToBody(5,true).addToBody(1, false).endRule() // d :- e, not a.
00483                         .startRule().addHead(5).addToBody(3,true).addToBody(4, true).endRule()  // e :- c, d.
00484                 .endProgram();
00485                 CPPUNIT_ASSERT(builder.stats.sccs == 1);
00486                 CPPUNIT_ASSERT(builder.getAtom(1)->scc() == PrgNode::noScc);
00487                 CPPUNIT_ASSERT(5u == ctx.sccGraph.get()->numAtoms());
00488                 CPPUNIT_ASSERT(8u == ctx.sccGraph.get()->numBodies());
00489                 attachUfs();
00490                 CPPUNIT_ASSERT_EQUAL(true, solver().assume(ctx.symbolTable()[2].lit) && solver().propagate());
00491                 solver().assume(ctx.symbolTable()[3].lit);
00492                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00493                 
00494                 CPPUNIT_ASSERT(solver().value(ctx.symbolTable()[4].lit.var()) == value_free);
00495                 CPPUNIT_ASSERT_EQUAL(true, ufs->propagate(solver()));
00496                 CPPUNIT_ASSERT_MESSAGE("TODO: Implement approx. ufs!", solver().isFalse(ctx.symbolTable()[4].lit));
00497                 
00498         }
00499 private:
00500         SharedContext ctx;
00501         SingleOwnerPtr<WrapDefaultUnfoundedCheck> ufs;
00502         LogicProgram builder;
00503         void attachUfs() {
00504                 solver().addPost(ufs.release());
00505                 ctx.endInit();
00506         }
00507         void setupSimpleProgram() {
00508                 builder.startProgram(ctx);
00509                 builder
00510                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c").setAtomName(4, "f")
00511                         .setAtomName(5, "x").setAtomName(6, "y").setAtomName(7, "z")
00512                         .startRule(CHOICERULE).addHead(5).addHead(6).addHead(7).addHead(3).endRule()
00513                         .startRule().addHead(2).addToBody(1, true).endRule()                    // b :- a.
00514                         .startRule().addHead(1).addToBody(2, true).addToBody(4, true).endRule() // a :- b,f.
00515                         .startRule().addHead(4).addToBody(1, true).addToBody(3, true).endRule() // f :- a,c.
00516                         .startRule().addHead(1).addToBody(5, false).endRule()                   // a :- not x.
00517                         .startRule().addHead(2).addToBody(7, false).endRule()                   // b :- not z.
00518                         .startRule().addHead(4).addToBody(6, false).endRule()                   // f :- not y.
00519                 ;
00520                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00521                 attachUfs();
00522                 CPPUNIT_ASSERT_EQUAL(true, solver().propagateUntil(ufs.get()));
00523         }
00524 };
00525 CPPUNIT_TEST_SUITE_REGISTRATION(UnfoundedCheckTest);
00526 } }

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