clasp: enumerator_test.cpp Source File

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/solver.h>
00022 #include <clasp/program_builder.h>
00023 #include <clasp/unfounded_check.h>
00024 #include <clasp/minimize_constraint.h>
00025 #include <clasp/model_enumerators.h>
00026 #include <sstream>
00027 using namespace std;
00028 namespace Clasp { namespace Test {
00029 using namespace Clasp::Asp;
00030 class EnumeratorTest : public CppUnit::TestFixture {
00031   CPPUNIT_TEST_SUITE(EnumeratorTest);
00032         CPPUNIT_TEST(testMiniProject);
00033         CPPUNIT_TEST(testProjectBug);
00034         CPPUNIT_TEST(testProjectRestart);
00035         CPPUNIT_TEST(testTerminateRemovesWatches);
00036         CPPUNIT_TEST(testParallelRecord);
00037         CPPUNIT_TEST(testParallelUpdate);
00038         CPPUNIT_TEST(testTagLiteral);
00039         CPPUNIT_TEST(testIgnoreTagLiteralInPath);
00040         CPPUNIT_TEST(testSplittable);
00041         CPPUNIT_TEST(testLearnStepLiteral);
00042         CPPUNIT_TEST_SUITE_END();       
00043 public:
00044         void testMiniProject() {
00045                 SharedContext ctx;
00046                 Solver& solver = *ctx.master();
00047                 builder.start(ctx, LogicProgram::AspOptions().noEq().noScc())
00048                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "_x")
00049                         .startRule(CHOICERULE).addHead(1).addHead(2).addHead(3).endRule()
00050                         .startRule().addHead(3).addToBody(1, false).endRule()
00051                         .startRule().addHead(3).addToBody(2, false).endRule()
00052                         .startRule(OPTIMIZERULE).addToBody(3, true).endRule()
00053                 ;
00054                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00055                 ModelEnumerator e;
00056                 e.setStrategy(ModelEnumerator::strategy_backtrack, ModelEnumerator::project_enable_simple);
00057                 e.init(ctx, builder.getMinimizeConstraint()->share());
00058                 ctx.endInit();
00059                 SymbolTable& index = ctx.symbolTable();
00060                 solver.assume(index[1].lit);
00061                 solver.propagate();
00062                 solver.assume(index[2].lit);
00063                 solver.propagate();
00064                 solver.assume(index[3].lit);
00065                 solver.propagate();
00066                 CPPUNIT_ASSERT(solver.numVars() == solver.numAssignedVars());
00067                 e.commitModel(solver);
00068                 bool ok = e.update(solver) && solver.propagate();
00069                 CPPUNIT_ASSERT(!ok);
00070                 solver.backtrack();
00071                 CPPUNIT_ASSERT(false == solver.propagate() && !solver.resolveConflict());
00072         }
00073 
00074         void testProjectBug() {
00075                 SharedContext ctx;
00076                 Solver& solver = *ctx.master();
00077                 builder.start(ctx, LogicProgram::AspOptions().noEq().noScc())
00078                         .setAtomName(1, "x").setAtomName(2, "y").setAtomName(3, "z").setAtomName(4, "_p").setAtomName(5, "_q").setAtomName(6, "_r")
00079                         .startRule(CHOICERULE).addHead(1).addHead(2).addHead(4).endRule() // {x,y,_p}
00080                         .startRule().addHead(5).addToBody(1, true).addToBody(4, true).endRule() // _q :- x,_p.
00081                         .startRule().addHead(6).addToBody(2, true).addToBody(4, true).endRule() // _r :- y,_p.
00082                         .startRule().addHead(3).addToBody(5, true).addToBody(6, true).endRule() // z :- _q,_r.
00083                 ;
00084                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00085                 ModelEnumerator e;
00086                 e.setStrategy(ModelEnumerator::strategy_backtrack, ModelEnumerator::project_enable_full);
00087                 e.init(ctx, 0);
00088                 ctx.endInit();
00089                 SymbolTable& index = ctx.symbolTable();
00090                 solver.assume(index[1].lit);
00091                 solver.propagate();
00092                 solver.assume(index[2].lit);
00093                 solver.propagate();
00094                 solver.assume(index[4].lit);
00095                 solver.propagate();
00096                 CPPUNIT_ASSERT(solver.numVars() == solver.numAssignedVars());
00097                 CPPUNIT_ASSERT_EQUAL(true, e.commitModel(solver) && e.update(solver));
00098 
00099                 solver.undoUntil(0);
00100                 uint32 numT = 0;
00101                 if (solver.value(index[1].lit.var()) == value_free) {
00102                         solver.assume(index[1].lit) && solver.propagate();
00103                         ++numT;
00104                 }
00105                 else if (solver.isTrue(index[1].lit)) {
00106                         ++numT;
00107                 }
00108                 if (solver.value(index[2].lit.var()) == value_free) {
00109                         solver.assume(index[2].lit) && solver.propagate();
00110                         ++numT;
00111                 }
00112                 else if (solver.isTrue(index[2].lit)) {
00113                         ++numT;
00114                 }
00115                 if (solver.value(index[4].lit.var()) == value_free) {
00116                         solver.assume(index[4].lit) && solver.propagate();
00117                 }
00118                 if (solver.isTrue(index[3].lit)) {
00119                         ++numT;
00120                 }
00121                 CPPUNIT_ASSERT(numT < 3);
00122         }
00123         
00124         void testProjectRestart() {
00125                 SharedContext ctx;
00126                 Solver& solver = *ctx.master();
00127                 builder.start(ctx, LogicProgram::AspOptions().noEq().noScc())
00128                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "_c")
00129                         .startRule(CHOICERULE).addHead(1).addHead(2).addHead(3).endRule() // {a,b,_c}
00130                 ;
00131                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00132                 ModelEnumerator e;
00133                 e.setStrategy(ModelEnumerator::strategy_backtrack, ModelEnumerator::project_enable_full);
00134                 e.init(ctx, 0);
00135                 ctx.endInit();
00136                 
00137                 SymbolTable& index = ctx.symbolTable();
00138                 solver.assume(index[1].lit);
00139                 solver.propagate();
00140                 solver.assume(index[2].lit);
00141                 solver.propagate();
00142                 solver.assume(index[3].lit);
00143                 solver.propagate();
00144                 solver.strategy.restartOnModel = 1;
00145                 CPPUNIT_ASSERT(solver.numVars() == solver.numAssignedVars());
00146                 CPPUNIT_ASSERT_EQUAL(true, e.commitModel(solver));
00147                 CPPUNIT_ASSERT_EQUAL(true, e.update(solver));
00148                 CPPUNIT_ASSERT(solver.isFalse(index[2].lit));
00149         }
00150 
00151         void testTerminateRemovesWatches() {
00152                 SharedContext ctx; Solver& solver = *ctx.master();
00153                 builder.start(ctx, LogicProgram::AspOptions().noEq().noScc())
00154                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c").setAtomName(4, "d")
00155                         .startRule(CHOICERULE).addHead(1).addHead(2).addHead(3).addHead(4).endRule()
00156                 ;
00157                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00158                 ModelEnumerator e(ModelEnumerator::strategy_record);
00159                 e.init(ctx, 0);
00160                 CPPUNIT_ASSERT_EQUAL(true, ctx.endInit());
00161                 
00162                 SymbolTable& index = ctx.symbolTable();
00163                 solver.assume(index[1].lit) && solver.propagate();
00164                 solver.assume(index[2].lit) && solver.propagate();
00165                 solver.assume(index[3].lit) && solver.propagate();
00166                 solver.assume(index[4].lit) && solver.propagate();
00167                 CPPUNIT_ASSERT_EQUAL(uint32(0), solver.numFreeVars());
00168                 e.commitModel(solver) && e.update(solver);
00169                 uint32 numW = solver.numWatches(index[1].lit) + solver.numWatches(index[2].lit) + solver.numWatches(index[3].lit) + solver.numWatches(index[4].lit);
00170                 CPPUNIT_ASSERT(numW > 0);
00171                 ctx.detach(solver);
00172                 numW = solver.numWatches(index[1].lit) + solver.numWatches(index[2].lit) + solver.numWatches(index[3].lit) + solver.numWatches(index[4].lit);
00173                 CPPUNIT_ASSERT(numW == 0);
00174         }
00175 
00176         void testParallelRecord() {
00177                 SharedContext ctx; Solver& solver = *ctx.master();
00178                 builder.start(ctx, LogicProgram::AspOptions().noEq().noScc())
00179                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c").setAtomName(4, "d")
00180                         .startRule(CHOICERULE).addHead(1).addHead(2).addHead(3).addHead(4).endRule()
00181                 ;
00182                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00183                 ctx.setConcurrency(2);
00184                 ModelEnumerator e(ModelEnumerator::strategy_record);
00185                 e.init(ctx, 0);
00186                 Solver& solver2 = ctx.addSolver();
00187                 ctx.endInit(true);
00188                 SymbolTable& index = ctx.symbolTable();
00189                 solver.assume(index[1].lit) && solver.propagate();
00190                 solver.assume(index[2].lit) && solver.propagate();
00191                 solver.assume(index[3].lit) && solver.propagate();
00192                 solver.assume(index[4].lit) && solver.propagate();
00193                 CPPUNIT_ASSERT_EQUAL(uint32(0), solver.numFreeVars());
00194                 e.commitModel(solver) && e.update(solver);
00195                 solver.undoUntil(0);
00196                 
00197                 CPPUNIT_ASSERT_EQUAL(true, e.update(solver2));
00198 
00199                 solver2.assume(index[1].lit) && solver2.propagate();
00200                 solver2.assume(index[2].lit) && solver2.propagate();
00201                 solver2.assume(index[3].lit) && solver2.propagate();
00202                 CPPUNIT_ASSERT(solver2.isFalse(index[4].lit) && solver2.propagate());
00203                 CPPUNIT_ASSERT_EQUAL(uint32(0), solver2.numFreeVars());
00204                 e.commitModel(solver2) && e.update(solver2);
00205                 solver.undoUntil(0);
00206 
00207                 CPPUNIT_ASSERT_EQUAL(true, e.update(solver));
00208 
00209                 solver.assume(index[1].lit) && solver.propagate();
00210                 solver.assume(index[2].lit) && solver.propagate();
00211                 CPPUNIT_ASSERT(solver.isFalse(index[3].lit));
00212 
00213                 ctx.detach(solver2);
00214                 ctx.detach(solver);
00215                 solver2.undoUntil(0);
00216                 ctx.attach(solver2);
00217                 solver2.assume(index[1].lit) && solver2.propagate();
00218                 solver2.assume(index[2].lit) && solver2.propagate();
00219                 solver2.assume(index[3].lit) && solver2.propagate();
00220                 CPPUNIT_ASSERT(solver2.value(index[4].lit.var()) == value_free);
00221         }
00222 
00223         void testParallelUpdate() {
00224                 SharedContext ctx; Solver& solver = *ctx.master();
00225                 builder.start(ctx, LogicProgram::AspOptions().noEq().noScc())
00226                         .setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c")
00227                         .startRule(CHOICERULE).addHead(1).addHead(2).addHead(3).endRule()
00228                         .startRule(OPTIMIZERULE).addToBody(2, true).endRule()
00229                 ;
00230                 CPPUNIT_ASSERT_EQUAL(true, builder.endProgram());
00231                 ctx.setConcurrency(2);
00232                 ModelEnumerator e(ModelEnumerator::strategy_record);
00233                 e.init(ctx, builder.getMinimizeConstraint()->share());
00234                 
00235                 Solver& solver2 = ctx.addSolver();
00236                 ctx.endInit(true);
00237                 SymbolTable& index = ctx.symbolTable();
00238 
00239                 // a
00240                 solver.assume(index[1].lit);
00241                 solver.pushRootLevel(1);
00242                 solver.propagate();
00243                 // ~a
00244                 solver2.assume(~index[1].lit);
00245                 solver2.pushRootLevel(1);
00246                 solver2.propagate();
00247 
00248                 // M1: ~b, c
00249                 solver.assume(~index[2].lit);
00250                 solver.propagate();
00251                 solver.assume(index[3].lit);
00252                 solver.propagate();     
00253                 CPPUNIT_ASSERT_EQUAL(uint32(0), solver.numFreeVars());
00254                 e.commitModel(solver);
00255                 solver.undoUntil(0);
00256                 e.update(solver);
00257                 
00258                 // M2: ~b, ~c 
00259                 solver2.assume(~index[2].lit);
00260                 solver2.propagate();
00261                 solver2.assume(~index[3].lit);
00262                 solver2.propagate();    
00263                 // M2 is NOT VALID!
00264                 CPPUNIT_ASSERT_EQUAL(false, e.update(solver2));
00265         }
00266 
00267         void testTagLiteral() {
00268                 ModelEnumerator e;
00269                 SharedContext ctx;
00270                 Var a = ctx.addVar(Var_t::atom_var);
00271                 Var b = ctx.addVar(Var_t::atom_var);
00272                 ctx.startAddConstraints();
00273                 e.init(ctx);
00274                 ctx.endInit();
00275                 CPPUNIT_ASSERT(2 == ctx.numVars());
00276                 e.start(*ctx.master());
00277                 ctx.master()->pushTagVar(true);
00278                 CPPUNIT_ASSERT(2 == ctx.numVars());
00279                 CPPUNIT_ASSERT(3 == ctx.master()->numVars());
00280                 CPPUNIT_ASSERT(ctx.master()->isTrue(ctx.master()->tagLiteral()));
00281         }
00282         void testIgnoreTagLiteralInPath() {
00283                 SharedContext ctx;
00284                 Var a = ctx.addVar(Var_t::atom_var);
00285                 Var b = ctx.addVar(Var_t::atom_var);
00286                 Solver& s1 = ctx.startAddConstraints();
00287                 Solver& s2 = ctx.addSolver();
00288                 ctx.endInit();
00289                 ctx.attach(s2);
00290                 s1.pushRoot(posLit(a));
00291                 s1.pushTagVar(true);
00292                 CPPUNIT_ASSERT(s1.rootLevel() == 2 && s1.isTrue(s1.tagLiteral()));
00293                 LitVec path;
00294                 s1.copyGuidingPath(path);
00295                 CPPUNIT_ASSERT(path.size() == 1 && path.back() == posLit(a));
00296         }
00297         void testSplittable() {
00298                 SharedContext ctx;
00299                 Var a = ctx.addVar(Var_t::atom_var);
00300                 Var b = ctx.addVar(Var_t::atom_var);
00301                 Var c = ctx.addVar(Var_t::atom_var);
00302                 Solver& s = ctx.startAddConstraints();
00303                 ctx.endInit();
00304                 s.pushRoot(posLit(a));
00305                 CPPUNIT_ASSERT(!s.splittable());
00306                 s.assume(posLit(b)) && s.propagate();
00307                 CPPUNIT_ASSERT(s.splittable());
00308                 s.pushTagVar(true);
00309                 CPPUNIT_ASSERT(!s.splittable());
00310                 s.assume(posLit(c)) && s.propagate();
00311                 CPPUNIT_ASSERT(s.splittable());
00312                 s.pushRootLevel();
00313                 Var aux = s.pushAuxVar();
00314                 s.assume(posLit(aux)) && s.propagate();
00315                 CPPUNIT_ASSERT(!s.splittable());
00316         }
00317         void testLearnStepLiteral() {
00318                 SharedContext ctx;
00319                 ctx.requestStepVar();
00320                 Var a = ctx.addVar(Var_t::atom_var);
00321                 Var b = ctx.addVar(Var_t::atom_var);
00322                 Solver& s1 = ctx.startAddConstraints();
00323                 Solver& s2 = ctx.addSolver();
00324                 ctx.endInit(true);
00325                 ClauseCreator cc(&s1);
00326                 cc.start(Constraint_t::learnt_conflict).add(posLit(a)).add(~ctx.stepLiteral()).end();
00327                 ctx.unfreeze();
00328                 ctx.endInit(true);
00329                 s1.pushRoot(negLit(a));
00330                 CPPUNIT_ASSERT(s1.value(ctx.stepLiteral().var()) == value_free);
00331         }
00332 private:
00333         LogicProgram builder;
00334         stringstream str;
00335         Model model;
00336 };
00337 CPPUNIT_TEST_SUITE_REGISTRATION(EnumeratorTest);
00338  } }