clasp: dlp_builder_test.cpp Source File

Go to the documentation of this file.
00001 // 
00002 // Copyright (c) 2012, 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/solver.h>
00022 #include <clasp/program_builder.h>
00023 #include <clasp/unfounded_check.h>
00024 #include <sstream>
00025 using namespace std;
00026 namespace Clasp { namespace Test {
00027 using namespace Clasp::Asp;
00028 class DlpBuilderTest : public CppUnit::TestFixture {
00029   CPPUNIT_TEST_SUITE(DlpBuilderTest);
00030         CPPUNIT_TEST(testSimpleChoice);
00031         CPPUNIT_TEST(testNotAChoice);
00032         CPPUNIT_TEST(testStillAChoice);
00033         CPPUNIT_TEST(testSubsumedChoice);
00034         CPPUNIT_TEST(testSubsumedByChoice);
00035         CPPUNIT_TEST(testChoiceDisjBug);
00036         CPPUNIT_TEST(testTautOverOne);
00037         CPPUNIT_TEST(testSimpleLoop);
00038         CPPUNIT_TEST(testComputeTrue);
00039         CPPUNIT_TEST(testComputeFalse);
00040         CPPUNIT_TEST(testIncremental);
00041         CPPUNIT_TEST_SUITE_END();       
00042 public:
00043         void tearDown(){
00044                 ctx.reset();
00045         }
00046         void testSimpleChoice() {
00047                 // a | b.
00048                 builder.start(ctx)
00049                         .setAtomName(1, "a").setAtomName(2, "b")
00050                         .startRule(DISJUNCTIVERULE).addHead(1).addHead(2).endRule()
00051                 ;
00052                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram() && ctx.endInit());
00053                 CPPUNIT_ASSERT(builder.stats.rules(DISJUNCTIVERULE).first == 1);
00054                 const SymbolTable& index = ctx.symbolTable();
00055                 CPPUNIT_ASSERT(index[1].lit != index[2].lit);
00056                 ctx.master()->assume(index[1].lit) && ctx.master()->propagate();
00057                 CPPUNIT_ASSERT(ctx.master()->isFalse(index[2].lit));
00058                 ctx.master()->undoUntil(0);
00059                 ctx.master()->assume(index[2].lit) && ctx.master()->propagate();
00060                 CPPUNIT_ASSERT(ctx.master()->isFalse(index[1].lit));
00061         }
00062         void testNotAChoice() {
00063                 // a | b.
00064                 // a :- not x.
00065                 builder.start(ctx)
00066                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "x")
00067                         .startRule(DISJUNCTIVERULE).addHead(1).addHead(2).endRule()
00068                         .startRule().addHead(1).addToBody(3, false).endRule()
00069                 ;
00070                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram() && ctx.endInit());
00071                 CPPUNIT_ASSERT(builder.stats.rules(DISJUNCTIVERULE).first == 1);
00072                 const SymbolTable& index = ctx.symbolTable();
00073                 CPPUNIT_ASSERT(index[2].lit == index[3].lit);
00074                 CPPUNIT_ASSERT(index[1].lit == posLit(0));
00075         }
00076 
00077         void testStillAChoice() {
00078                 // a | b.
00079                 // {b}.
00080                 builder.start(ctx)
00081                         .setAtomName(1, "a").setAtomName(2, "b")
00082                         .startRule(DISJUNCTIVERULE).addHead(1).addHead(2).endRule()
00083                         .startRule(CHOICERULE).addHead(2).endRule()
00084                 ;
00085                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram() && ctx.endInit());
00086                 CPPUNIT_ASSERT(builder.stats.rules(DISJUNCTIVERULE).first == 1);
00087                 const SymbolTable& index = ctx.symbolTable();
00088                 CPPUNIT_ASSERT(index[1].lit != index[2].lit);
00089                 ctx.master()->assume(index[1].lit) && ctx.master()->propagate();
00090                 CPPUNIT_ASSERT(ctx.master()->isFalse(index[2].lit));
00091                 ctx.master()->undoUntil(0);
00092                 ctx.master()->assume(index[2].lit) && ctx.master()->propagate();
00093                 CPPUNIT_ASSERT(ctx.master()->isFalse(index[1].lit));
00094         }
00095 
00096         void testSubsumedChoice() {
00097                 // a | b.
00098                 // a | b | c | d.
00099                 builder.start(ctx, LogicProgram::AspOptions().iterations(-1))
00100                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c").setAtomName(4, "d")
00101                         .startRule(DISJUNCTIVERULE).addHead(1).addHead(2).endRule()
00102                         .startRule(DISJUNCTIVERULE).addHead(1).addHead(2).addHead(3).addHead(4).endRule()
00103                 ;
00104                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram() && ctx.endInit());
00105                 CPPUNIT_ASSERT(builder.stats.rules(DISJUNCTIVERULE).first == 2);
00106                 const SymbolTable& index = ctx.symbolTable();
00107                 CPPUNIT_ASSERT(index[3].lit == negLit(0) || !(ctx.master()->assume(index[3].lit) && ctx.master()->propagate()));
00108                 ctx.master()->undoUntil(0);
00109                 CPPUNIT_ASSERT(index[4].lit == negLit(0) || !(ctx.master()->assume(index[4].lit) && ctx.master()->propagate()));
00110         }
00111         
00112         void testSubsumedByChoice() {
00113                 // a | b.
00114                 // {a,b}.
00115                 builder.start(ctx)
00116                         .setAtomName(1, "a").setAtomName(2, "b")
00117                         .startRule(DISJUNCTIVERULE).addHead(1).addHead(2).endRule()
00118                         .startRule(CHOICERULE).addHead(1).addHead(2).endRule()
00119                 ;
00120                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram() && ctx.endInit());
00121                 CPPUNIT_ASSERT(builder.stats.rules(DISJUNCTIVERULE).first == 1);
00122                 const SymbolTable& index = ctx.symbolTable();
00123                 ctx.master()->assume(~index[1].lit) && ctx.master()->propagate();
00124                 CPPUNIT_ASSERT(ctx.master()->isTrue(index[2].lit));
00125         }
00126         void testChoiceDisjBug() {
00127                 // a | b.
00128                 // {a,b,b}.
00129                 builder.start(ctx)
00130                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c")
00131                         .startRule(DISJUNCTIVERULE).addHead(1).addHead(2).endRule()
00132                         .startRule(CHOICERULE).addHead(1).addHead(2).addHead(3).endRule()
00133                 ;
00134                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram() && ctx.endInit());
00135                 CPPUNIT_ASSERT(builder.stats.rules(DISJUNCTIVERULE).first == 1);
00136                 const SymbolTable& index = ctx.symbolTable();
00137                 ctx.master()->assume(index[3].lit) && ctx.master()->propagate();
00138                 CPPUNIT_ASSERT(ctx.master()->value(index[1].lit.var()) == value_free);
00139                 CPPUNIT_ASSERT(ctx.master()->value(index[2].lit.var()) == value_free);
00140                 ctx.master()->assume(~index[1].lit) && ctx.master()->propagate();
00141                 CPPUNIT_ASSERT(ctx.master()->isTrue(index[2].lit));
00142                 ctx.master()->undoUntil(0);
00143                 ctx.master()->assume(index[1].lit) && ctx.master()->propagate();
00144                 ctx.master()->assume(index[2].lit) && ctx.master()->propagate();
00145                 ctx.master()->assume(index[3].lit) && ctx.master()->propagate();
00146                 CPPUNIT_ASSERT(!ctx.master()->hasConflict() && ctx.master()->numFreeVars() == 0);
00147         }
00148 
00149         void testTautOverOne() {
00150                 // {x}.
00151                 // y :- x.
00152                 // a | x :- y.
00153                 builder.start(ctx)
00154                         .setAtomName(1, "a").setAtomName(2, "x").setAtomName(3, "y")
00155                         .startRule(DISJUNCTIVERULE).addHead(1).addHead(2).addToBody(3, true).endRule()
00156                         .startRule(CHOICERULE).addHead(2).endRule()
00157                         .startRule().addHead(3).addToBody(2, true).endRule()
00158                 ;
00159                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram() && ctx.endInit());
00160                 CPPUNIT_ASSERT(builder.stats.rules(DISJUNCTIVERULE).first == 1);
00161                 const SymbolTable& index = ctx.symbolTable();
00162                 CPPUNIT_ASSERT(index[1].lit == negLit(0) && !(ctx.master()->assume(index[1].lit) && ctx.master()->propagate()));
00163         }
00164         
00165         void testSimpleLoop() {
00166                 // a | b.
00167                 // a :- b.
00168                 // b :- a.
00169                 builder.start(ctx)
00170                         .setAtomName(1, "a").setAtomName(2, "b")
00171                         .startRule(DISJUNCTIVERULE).addHead(1).addHead(2).endRule()
00172                         .startRule().addHead(1).addToBody(2, true).endRule()
00173                         .startRule().addHead(2).addToBody(1, true).endRule()
00174                 ;
00175                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00176                 CPPUNIT_ASSERT(builder.stats.rules(DISJUNCTIVERULE).first == 1);
00177                 ctx.master()->addPost(new DefaultUnfoundedCheck());
00178                 CPPUNIT_ASSERT_EQUAL(true, ctx.endInit());
00179                 const SymbolTable& index = ctx.symbolTable();
00180                 CPPUNIT_ASSERT(index[1].lit != index[2].lit);
00181                 CPPUNIT_ASSERT(ctx.master()->assume(index[1].lit) && ctx.master()->propagate());
00182                 CPPUNIT_ASSERT(!ctx.master()->isFalse(index[2].lit));
00183                 ctx.master()->undoUntil(0);
00184                 CPPUNIT_ASSERT(ctx.master()->assume(index[2].lit) && ctx.master()->propagate());
00185                 CPPUNIT_ASSERT(!ctx.master()->isFalse(index[1].lit));
00186         }
00187         void testComputeTrue() {
00188                 // a | x.
00189                 // :- not a.
00190                 // a :- x.
00191                 builder.start(ctx, LogicProgram::AspOptions().noScc())
00192                         .setAtomName(1, "a").setAtomName(2, "x")
00193                         .startRule(DISJUNCTIVERULE).addHead(1).addHead(2).endRule()
00194                         .startRule().addHead(1).addToBody(2, true).endRule()
00195                         .setCompute(1, true);
00196                 ;
00197                 CPPUNIT_ASSERT(builder.getAtom(1)->value() == value_true);
00198                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00199                 CPPUNIT_ASSERT(builder.stats.rules(DISJUNCTIVERULE).first == 1);
00200                 const SymbolTable& index = ctx.symbolTable();
00201                 CPPUNIT_ASSERT(ctx.master()->isTrue(index[1].lit));
00202                 CPPUNIT_ASSERT(ctx.master()->isFalse(index[2].lit));
00203         }
00204         void testComputeFalse() {
00205                 // a | b | x.
00206                 // :- a.
00207                 // a :- x.
00208                 builder.start(ctx)
00209                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "x")
00210                         .startRule(DISJUNCTIVERULE).addHead(1).addHead(2).addHead(3).endRule()
00211                         .startRule().addHead(1).addToBody(3, true).endRule()
00212                         .setCompute(1, false);
00213                 ;
00214                 CPPUNIT_ASSERT(builder.getAtom(1)->value() == value_false);
00215                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00216                 CPPUNIT_ASSERT(builder.stats.rules(DISJUNCTIVERULE).first == 1);
00217                 const SymbolTable& index = ctx.symbolTable();
00218                 CPPUNIT_ASSERT(ctx.master()->isFalse(index[1].lit));
00219                 CPPUNIT_ASSERT(ctx.master()->isFalse(index[3].lit));
00220                 CPPUNIT_ASSERT(ctx.master()->isTrue(index[2].lit));
00221         }
00222         void testIncremental() {
00223                 // Step 0:
00224                 // a | b :- x.
00225                 // a :- b.
00226                 // b :- a.
00227                 // freeze x.
00228                 builder.start(ctx);
00229                 builder.updateProgram();
00230                 builder.setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "x")
00231                         .startRule(DISJUNCTIVERULE).addHead(1).addHead(2).addToBody(3,true).endRule()
00232                         .startRule().addHead(1).addToBody(2, true).endRule()
00233                         .startRule().addHead(2).addToBody(1, true).endRule()
00234                         .freeze(3);
00235                 ;
00236                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00237                 CPPUNIT_ASSERT(builder.stats.rules(DISJUNCTIVERULE).first == 1);
00238                 CPPUNIT_ASSERT(builder.stats.sccs == 1);
00239                 CPPUNIT_ASSERT(builder.stats.nonHcfs == 1);
00240 
00241                 // Step 1:
00242                 // c | d :- a, y.
00243                 // c :- d, b.
00244                 // d :- c, a.
00245                 // freeze y.
00246                 builder.update();
00247                 builder.setAtomName(4, "c").setAtomName(5, "d").setAtomName(6, "y")
00248                         .startRule(DISJUNCTIVERULE).addHead(4).addHead(5).addToBody(1,true).addToBody(6,true).endRule()
00249                         .startRule().addHead(4).addToBody(5, true).addToBody(2, true).endRule()
00250                         .startRule().addHead(5).addToBody(4, true).addToBody(1, true).endRule()
00251                         .freeze(6);
00252                 ;
00253                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00254                 CPPUNIT_ASSERT(builder.stats.rules(DISJUNCTIVERULE).first == 1);
00255                 CPPUNIT_ASSERT(builder.stats.sccs == 1);
00256                 CPPUNIT_ASSERT(builder.stats.nonHcfs == 1);
00257         }
00258 private:
00259         typedef SharedDependencyGraph DG;
00260         SharedContext ctx;
00261         LogicProgram  builder;
00262         stringstream  str;
00263 };
00264 CPPUNIT_TEST_SUITE_REGISTRATION(DlpBuilderTest);
00265  } }