clasp: dependency_graph_test.cpp Source File

Go to the documentation of this file.
00001 // 
00002 // Copyright (c) 2009, 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/dependency_graph.h>
00022 #include <clasp/solver.h>
00023 namespace Clasp { namespace Test {
00024 using namespace Clasp::Asp;
00025 class DependencyGraphTest : public CppUnit::TestFixture {
00026         CPPUNIT_TEST_SUITE(DependencyGraphTest);
00027         CPPUNIT_TEST(testTightProgram);
00028         CPPUNIT_TEST(testInitOrder);
00029         CPPUNIT_TEST(testProgramWithLoops);
00030         CPPUNIT_TEST(testWithSimpleCardinalityConstraint);
00031         CPPUNIT_TEST(testWithSimpleWeightConstraint);
00032         CPPUNIT_TEST_SUITE_END(); 
00033 public:
00034         DependencyGraphTest() {
00035         }
00036         void setUp() {
00037                 ctx   = new SharedContext();
00038         }
00039         void tearDown() {
00040                 delete ctx;
00041         }
00042         void testTightProgram() { 
00043                 builder.start(*ctx)
00044                         .setAtomName(1, "a").setAtomName(2, "b")
00045                         .startRule().addHead(1).addToBody(2, false).endRule()
00046                 .endProgram();
00047                 CPPUNIT_ASSERT_EQUAL(true, builder.stats.sccs == 0);
00048                 CPPUNIT_ASSERT(ctx->sccGraph.get() == 0);
00049         }
00050         
00051         void testInitOrder() {
00052                 builder.start(*ctx, LogicProgram::AspOptions().noEq())
00053                         .setAtomName(1,"a").setAtomName(2,"b").setAtomName(3,"x").setAtomName(4,"y")
00054                         .startRule().addHead(4).addToBody(3, true).endRule()  // y :- x.
00055                         .startRule().addHead(3).addToBody(4, true).endRule()  // x :- y.
00056                         .startRule().addHead(2).addToBody(3, true).endRule()  // b :- x.
00057                         .startRule().addHead(2).addToBody(1, true).endRule()  // b :- a.
00058                         .startRule().addHead(1).addToBody(2, true).endRule()  // a :- b.
00059                         .startRule().addHead(3).addToBody(1, false).endRule() // x :- not a.
00060                 .endProgram();
00061                 
00062                 CPPUNIT_ASSERT_EQUAL(true, builder.stats.sccs == 2);
00063                 
00064                 DG* graph = ctx->sccGraph.get();
00065 
00066                 CPPUNIT_ASSERT_EQUAL(uint32(10), graph->nodes());
00067                 
00068                 const DG::AtomNode& b = graph->getAtom(builder.getAtom(2)->id());
00069                 const DG::AtomNode& x = graph->getAtom(builder.getAtom(3)->id());
00070                 
00071                 CPPUNIT_ASSERT(graph->getBody(b.body(0)).scc != b.scc);
00072                 CPPUNIT_ASSERT(graph->getBody(b.body(1)).scc == b.scc);
00073                 CPPUNIT_ASSERT(b.bodies_begin()+2 == b.bodies_end());
00074 
00075                 CPPUNIT_ASSERT(graph->getBody(x.body(0)).scc != x.scc);
00076                 CPPUNIT_ASSERT(graph->getBody(x.body(1)).scc == x.scc);
00077                 CPPUNIT_ASSERT(x.bodies_begin()+2 == x.bodies_end());
00078 
00079                 const DG::BodyNode& xBody = graph->getBody(b.body(0));
00080                 CPPUNIT_ASSERT(graph->getAtom(xBody.heads_begin()[0]).scc == xBody.scc);
00081                 CPPUNIT_ASSERT(graph->getAtom(xBody.heads_begin()[1]).scc != xBody.scc);
00082                 CPPUNIT_ASSERT(xBody.heads_begin()+2 == xBody.heads_end());
00083         }
00084 
00085         void testProgramWithLoops() {
00086                 builder.start(*ctx)
00087                 .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c")
00088                 .setAtomName(4, "d").setAtomName(5, "g").setAtomName(6, "x").setAtomName(7, "y")
00089                 .startRule().addHead(1).addToBody(6, false).endRule() // a :- not x.
00090                 .startRule().addHead(2).addToBody(1, true).endRule()  // b :- a.
00091                 .startRule().addHead(1).addToBody(2, true).addToBody(4, true).endRule() // a :- b, d.
00092                 .startRule().addHead(2).addToBody(5, false).endRule() // b :- not g.
00093                 .startRule().addHead(3).addToBody(6, true).endRule()  // c :- x.
00094                 .startRule().addHead(4).addToBody(3, true).endRule()  // d :- c.
00095                 .startRule().addHead(3).addToBody(4, true).endRule()  // c :- d.
00096                 .startRule().addHead(4).addToBody(5, false).endRule() // d :- not g.
00097                 .startRule().addHead(7).addToBody(5, false).endRule() // y :- not g.
00098                 .startRule().addHead(6).addToBody(7, true).endRule()  // x :- y.
00099                 .startRule().addHead(5).addToBody(7, false).endRule() // g :- not y.
00100                 .endProgram();
00101                 
00102                 SymbolTable& index = ctx->symbolTable();
00103                 DG* graph          = ctx->sccGraph.get();
00104                 CPPUNIT_ASSERT_EQUAL(index[6].lit, index[7].lit);
00105                 CPPUNIT_ASSERT_EQUAL(~index[6].lit, index[5].lit);
00106                 
00107                 CPPUNIT_ASSERT( graph->getAtom(builder.getAtom(1)->id()).scc == 0 );
00108                 CPPUNIT_ASSERT( graph->getAtom(builder.getAtom(2)->id()).scc == 0 );
00109                 CPPUNIT_ASSERT( graph->getAtom(builder.getAtom(3)->id()).scc == 1 );
00110                 CPPUNIT_ASSERT( graph->getAtom(builder.getAtom(4)->id()).scc == 1 );
00111                 CPPUNIT_ASSERT( builder.getAtom(5)->id() == PrgNode::maxVertex );
00112                 CPPUNIT_ASSERT( builder.getAtom(6)->eq() || builder.getAtom(6)->id() == PrgNode::maxVertex );
00113                 CPPUNIT_ASSERT( builder.getAtom(7)->id() == PrgNode::maxVertex );
00114                 
00115                 CPPUNIT_ASSERT(uint32(11) == graph->nodes());
00116                 // check that lists are partitioned by component number
00117                 const DG::AtomNode& a =  graph->getAtom(builder.getAtom(1)->id());
00118                 CPPUNIT_ASSERT(graph->getBody(a.body(0)).scc == PrgNode::noScc);
00119                 CPPUNIT_ASSERT(graph->getBody(a.body(1)).scc == a.scc);
00120                 CPPUNIT_ASSERT(a.bodies_begin()+2 == a.bodies_end());
00121                 CPPUNIT_ASSERT_EQUAL(true, ctx->varInfo(a.lit.var()).frozen());
00122 
00123                 const DG::BodyNode& bd = graph->getBody(a.body(1));
00124                 CPPUNIT_ASSERT_EQUAL(true, ctx->varInfo(bd.lit.var()).frozen());
00125                 CPPUNIT_ASSERT(graph->getAtom(bd.preds()[0]).lit == index[2].lit);
00126                 CPPUNIT_ASSERT(bd.preds()[1]== idMax);
00127                 CPPUNIT_ASSERT(bd.heads_begin()[0] == graph->id(a));
00128                 CPPUNIT_ASSERT(bd.heads_begin()+1 == bd.heads_end());
00129         }
00130 
00131         void testWithSimpleCardinalityConstraint() {
00132                 builder.start(*ctx)
00133                         .setAtomName(1, "a").setAtomName(2, "b")
00134                         .startRule(CHOICERULE).addHead(2).endRule()
00135                         .startRule(CONSTRAINTRULE, 1).addHead(1).addToBody(1, true).addToBody(2,true).endRule()
00136                 ;
00137                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00138                 DG* graph = ctx->sccGraph.get();
00139                 CPPUNIT_ASSERT( uint32(3) == graph->nodes() );
00140                 SymbolTable& index = ctx->symbolTable();
00141                 const DG::AtomNode& a    = graph->getAtom(builder.getAtom(1)->id());
00142                 const DG::BodyNode& body = graph->getBody(a.body(0));
00143 
00144                 CPPUNIT_ASSERT(body.num_preds() == 2);
00145                 CPPUNIT_ASSERT(body.extended());
00146                 CPPUNIT_ASSERT(body.ext_bound() == 1);
00147                 CPPUNIT_ASSERT(body.pred_inc() == 1);
00148                 CPPUNIT_ASSERT(body.preds()[0] == graph->id(a));
00149                 CPPUNIT_ASSERT(body.preds()[1] == idMax);
00150                 CPPUNIT_ASSERT(body.preds()[2] == index[2].lit.asUint());
00151                 CPPUNIT_ASSERT(body.preds()[3] == idMax);
00152                 CPPUNIT_ASSERT(body.pred_weight(0,false) == 1);
00153                 CPPUNIT_ASSERT(body.pred_weight(1,true) == 1);
00154 
00155                 CPPUNIT_ASSERT(a.inExtended());
00156                 CPPUNIT_ASSERT(a.succs()[0] == idMax);
00157                 CPPUNIT_ASSERT(a.succs()[1] == a.body(0));
00158                 CPPUNIT_ASSERT(a.succs()[2] == 0);
00159                 CPPUNIT_ASSERT(a.succs()[3] == idMax);
00160         }
00161 
00162         void testWithSimpleWeightConstraint() {
00163                 builder.start(*ctx)
00164                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c")
00165                         .startRule(CHOICERULE).addHead(2).addHead(3).endRule()
00166                         .startRule(WEIGHTRULE, 2).addHead(1).addToBody(1, true, 2).addToBody(2,true, 2).addToBody(3, true, 1).endRule()
00167                 ;
00168                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00169                 DG* graph = ctx->sccGraph.get();
00170                 CPPUNIT_ASSERT( uint32(3) == graph->nodes() );
00171                 
00172                 SymbolTable& index = ctx->symbolTable();
00173                 const DG::AtomNode& a    = graph->getAtom(builder.getAtom(1)->id());
00174                 const DG::BodyNode& body = graph->getBody(a.body(0));
00175 
00176                 CPPUNIT_ASSERT(body.num_preds() == 3);
00177                 CPPUNIT_ASSERT(body.extended());
00178                 CPPUNIT_ASSERT(body.ext_bound() == 2);
00179                 CPPUNIT_ASSERT(body.pred_inc() == 2);
00180                 CPPUNIT_ASSERT(body.preds()[0] == graph->id(a));
00181                 CPPUNIT_ASSERT(body.preds()[2] == idMax);
00182                 CPPUNIT_ASSERT(body.preds()[3] == index[2].lit.asUint());
00183                 CPPUNIT_ASSERT(body.preds()[5] == index[3].lit.asUint());
00184                 CPPUNIT_ASSERT(body.preds()[7] == idMax);
00185                 CPPUNIT_ASSERT(body.pred_weight(0, false) == 2);
00186                 CPPUNIT_ASSERT(body.pred_weight(1, true) == 2);
00187                 CPPUNIT_ASSERT(body.pred_weight(2, true) == 1);
00188                 
00189                 CPPUNIT_ASSERT(a.inExtended());
00190                 CPPUNIT_ASSERT(a.succs()[0] == idMax);
00191                 CPPUNIT_ASSERT(a.succs()[1] == a.body(0));
00192                 CPPUNIT_ASSERT(a.succs()[2] == 0);
00193                 CPPUNIT_ASSERT(a.succs()[3] == idMax);
00194         }
00195 private:
00196         typedef SharedDependencyGraph DG;
00197         SharedContext* ctx;
00198         LogicProgram   builder;
00199 };
00200 CPPUNIT_TEST_SUITE_REGISTRATION(DependencyGraphTest);
00201 } }