00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 #include "test.h"
00021 #include <clasp/solver.h>
00022 #include <clasp/clause.h>
00023 #include <clasp/clasp_facade.h>
00024 #include <clasp/minimize_constraint.h>
00025 #include <clasp/heuristics.h>
00026
00027 namespace Clasp { namespace Test {
00028 using namespace Clasp::mt;
00029
00030 class FacadeTest : public CppUnit::TestFixture {
00031 CPPUNIT_TEST_SUITE(FacadeTest);
00032 CPPUNIT_TEST(testIncrementalSolve);
00033 CPPUNIT_TEST(testIncrementalEnum);
00034 CPPUNIT_TEST(testIncrementalCons);
00035 CPPUNIT_TEST(testIncrementalMin);
00036 CPPUNIT_TEST(testUpdateConfig);
00037 CPPUNIT_TEST(testIncrementalProjectUpdate);
00038 CPPUNIT_TEST(testStats);
00039 #if WITH_THREADS
00040 CPPUNIT_TEST(testAsyncSolveTrivialUnsat);
00041 CPPUNIT_TEST(testInterruptBeforeSolve);
00042 CPPUNIT_TEST(testCancelAsyncOperation);
00043 CPPUNIT_TEST(testAsyncResultDtorCancelsOp);
00044 CPPUNIT_TEST(testDestroyAsyncResultNoFacade);
00045 CPPUNIT_TEST(testDestroyDanglingAsyncResult);
00046 CPPUNIT_TEST(testCancelDanglingAsyncOperation);
00047 #endif
00048 CPPUNIT_TEST_SUITE_END();
00049 public:
00050 typedef ClaspFacade::Result Result;
00051 void testRunIncremental(Result::Base stop, int maxStep, int minStep, Result::Base expectedRes, int expectedSteps) {
00052 ClaspConfig config;
00053 ClaspFacade f;
00054 f.ctx.enableStats(2);
00055 config.asp.noEq();
00056 Asp::LogicProgram& asp = f.startAsp(config, true);
00057 Result::Base res = Result::UNKNOWN;
00058 do {
00059 f.update();
00060 switch(f.step()) {
00061 default: break;
00062 case 0:
00063 asp.setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "x")
00064 .startRule().addHead(1).addToBody(2, true).endRule()
00065 .startRule().addHead(2).addToBody(1, true).endRule()
00066 .startRule().addHead(1).addToBody(3, true).endRule()
00067 .freeze(3)
00068 .setCompute(1, true);
00069 break;
00070 case 1:
00071 asp.setAtomName(4, "y").setAtomName(5, "z").endRule()
00072 .startRule().addHead(3).addToBody(4, true).endRule()
00073 .startRule().addHead(4).addToBody(3, true).endRule()
00074 .startRule().addHead(4).addToBody(5, true).endRule()
00075 .freeze(5);
00076 break;
00077 case 2:
00078 asp.setAtomName(6, "q").setAtomName(7, "r")
00079 .startRule().addHead(5).addToBody(6, true).addToBody(7, true).endRule()
00080 .startRule().addHead(6).addToBody(3, false).endRule()
00081 .startRule().addHead(7).addToBody(1, false).addToBody(2, false).endRule()
00082 .startRule(Asp::CHOICERULE).addHead(5).endRule();
00083 break;
00084 case 3:
00085 asp.setAtomName(8,"f").startRule(Asp::CHOICERULE).addHead(8).endRule();
00086 break;
00087 }
00088 if (!f.prepare()) { break; }
00089 res = f.solve();
00090 } while (--maxStep && ((minStep > 0 && --minStep) || res != stop));
00091 CPPUNIT_ASSERT_EQUAL(expectedRes, (Result::Base)f.result());
00092 CPPUNIT_ASSERT_EQUAL(expectedSteps, f.step());
00093 }
00094 void testIncrementalSolve() {
00095 testRunIncremental(Result::SAT , -1, -1, Result::SAT , 2);
00096 testRunIncremental(Result::UNSAT, -1, -1, Result::UNSAT, 0);
00097 testRunIncremental(Result::SAT , 2, -1, Result::UNSAT, 1);
00098 testRunIncremental(Result::SAT , -1, 4, Result::SAT , 3);
00099 }
00100 void testIncrementalEnum() {
00101 Clasp::ClaspFacade libclasp;
00102 Clasp::ClaspConfig config;
00103 config.enumerate.numModels = 0;
00104 config.enumerate.type = EnumOptions::enum_record;
00105 Clasp::Asp::LogicProgram& asp = libclasp.startAsp(config, true);
00106 asp.setAtomName(1, "a");
00107 asp.startRule(Clasp::Asp::CHOICERULE).addHead(1).endRule();
00108 libclasp.prepare(Clasp::ClaspFacade::enum_volatile);
00109 CPPUNIT_ASSERT(libclasp.solve().sat());
00110 CPPUNIT_ASSERT(libclasp.summary().numEnum == 2);
00111 CPPUNIT_ASSERT(libclasp.update().ok());
00112 asp.setAtomName(2, "b");
00113 asp.startRule(Clasp::Asp::CHOICERULE).addHead(2).endRule();
00114 libclasp.prepare();
00115 CPPUNIT_ASSERT(libclasp.solve().sat());
00116 CPPUNIT_ASSERT(libclasp.summary().numEnum == 4);
00117 }
00118 void testIncrementalCons() {
00119 Clasp::ClaspFacade libclasp;
00120 Clasp::ClaspConfig config;
00121 config.enumerate.numModels = 0;
00122 config.enumerate.type = EnumOptions::enum_cautious;
00123 Clasp::Asp::LogicProgram& asp = libclasp.startAsp(config, true);
00124 asp.setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c");
00125 asp.startRule(Clasp::Asp::CHOICERULE).addHead(1).addHead(2).addHead(3).endRule();
00126 libclasp.prepare();
00127 CPPUNIT_ASSERT(libclasp.solve().sat());
00128 config.enumerate.type = EnumOptions::enum_brave;
00129 libclasp.update(true);
00130 libclasp.prepare();
00131 CPPUNIT_ASSERT(libclasp.solve().sat());
00132 CPPUNIT_ASSERT(libclasp.summary().numEnum > 1);
00133 }
00134 void testIncrementalMin() {
00135 Clasp::ClaspFacade libclasp;
00136 Clasp::ClaspConfig config;
00137 config.enumerate.numModels = 0;
00138 config.enumerate.type = EnumOptions::enum_auto;
00139 Clasp::Asp::LogicProgram& asp = libclasp.startAsp(config, true);
00140 asp.setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c");
00141 asp.startRule(Clasp::Asp::CHOICERULE).addHead(1).addHead(2).addHead(3).endRule();
00142 asp.startRule(Clasp::Asp::OPTIMIZERULE).addToBody(1,true).addToBody(2, true).addToBody(3, true).endRule();
00143 libclasp.prepare();
00144 CPPUNIT_ASSERT(libclasp.solve().sat());
00145 CPPUNIT_ASSERT(libclasp.summary().numEnum < 8u);
00146 libclasp.update().disposeMinimizeConstraint();
00147 libclasp.prepare();
00148 CPPUNIT_ASSERT(libclasp.solve().sat());
00149 CPPUNIT_ASSERT(libclasp.summary().numEnum == 8);
00150 }
00151 void testUpdateConfig() {
00152 Clasp::ClaspFacade libclasp;
00153 Clasp::ClaspConfig config;
00154 config.enumerate.numModels = 0;
00155 config.enumerate.type = EnumOptions::enum_auto;
00156 config.addSolver(0).heuId = Heuristic_t::heu_berkmin;
00157 Clasp::Asp::LogicProgram& asp = libclasp.startAsp(config, true);
00158 asp.setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c");
00159 asp.startRule(Clasp::Asp::CHOICERULE).addHead(1).addHead(2).addHead(3).endRule();
00160 libclasp.prepare();
00161 CPPUNIT_ASSERT(libclasp.solve().sat());
00162 config.addSolver(0).heuId = Heuristic_t::heu_vsids;
00163 libclasp.update(true);
00164 libclasp.prepare();
00165 CPPUNIT_ASSERT(libclasp.solve().sat());
00166 CPPUNIT_ASSERT(dynamic_cast<ClaspVsids*>(libclasp.ctx.master()->heuristic().get()));
00167 }
00168 void testIncrementalProjectUpdate() {
00169 Clasp::ClaspFacade libclasp;
00170 Clasp::ClaspConfig config;
00171 config.enumerate.numModels = 0;
00172 config.enumerate.type = EnumOptions::enum_auto;
00173 config.enumerate.project = 1;
00174 Clasp::Asp::LogicProgram& asp = libclasp.startAsp(config, true);
00175 asp.setAtomName(1, "_a").setAtomName(2, "b");
00176 asp.startRule(Clasp::Asp::CHOICERULE).addHead(1).addHead(2).endRule();
00177 libclasp.prepare();
00178 CPPUNIT_ASSERT(libclasp.ctx.varInfo(libclasp.ctx.symbolTable()[2].lit.var()).project());
00179 CPPUNIT_ASSERT(libclasp.solve().sat());
00180 CPPUNIT_ASSERT(libclasp.summary().numEnum == 2);
00181 config.enumerate.project = 0;
00182 libclasp.update(true);
00183 libclasp.prepare();
00184 CPPUNIT_ASSERT(libclasp.solve().sat());
00185 CPPUNIT_ASSERT(libclasp.summary().numEnum == 4);
00186 config.enumerate.project = 1;
00187 libclasp.update(true);
00188 asp.setAtomName(3, "_x").setAtomName(4, "y");
00189 asp.startRule(Clasp::Asp::CHOICERULE).addHead(3).addHead(4).endRule();
00190 libclasp.prepare();
00191 CPPUNIT_ASSERT(libclasp.ctx.varInfo(libclasp.ctx.symbolTable()[2].lit.var()).project());
00192 CPPUNIT_ASSERT(libclasp.ctx.varInfo(libclasp.ctx.symbolTable()[4].lit.var()).project());
00193 CPPUNIT_ASSERT(libclasp.solve().sat());
00194 CPPUNIT_ASSERT_EQUAL(uint64(4), libclasp.summary().numEnum);
00195 }
00196 void testStats() {
00197 Clasp::ClaspFacade libclasp;
00198 Clasp::ClaspConfig config;
00199 Clasp::Asp::LogicProgram& asp = libclasp.startAsp(config, true);
00200 asp.setAtomName(1, "a").setAtomName(2, "b").setAtomName(3, "c");
00201 asp.startRule(Clasp::Asp::CHOICERULE).addHead(1).addHead(2).addHead(3).endRule();
00202 asp.startRule(Clasp::Asp::OPTIMIZERULE).addToBody(1, true).addToBody(2, true).endRule();
00203 libclasp.prepare();
00204 libclasp.solve();
00205 std::vector<std::string> keys;
00206 getKeys(libclasp, keys, "");
00207 CPPUNIT_ASSERT(!keys.empty());
00208 for (std::vector<std::string>::const_iterator it = keys.begin(), end = keys.end(); it != end; ++it) {
00209 CPPUNIT_ASSERT(libclasp.getStat(it->c_str()).valid());
00210 }
00211 CPPUNIT_ASSERT(libclasp.getStat("lp.rules") == double(asp.stats.rules()));
00212 CPPUNIT_ASSERT(libclasp.getStat("numEnum") == double(libclasp.summary().enumerated()));
00213 CPPUNIT_ASSERT(libclasp.getStat("solvers.choices") == double(libclasp.ctx.master()->stats.choices));
00214 CPPUNIT_ASSERT(libclasp.getStat("costs.0") == double(libclasp.summary().costs()->optimum(0)));
00215 CPPUNIT_ASSERT(libclasp.getStat("optimal") == double(libclasp.summary().optimal()));
00216 }
00217 void getKeys(const ClaspFacade& f, std::vector<std::string>& out, const std::string& p) {
00218 typedef std::pair<std::string, double> Stat;
00219 std::size_t len = 0;
00220 for (const char* k = f.getKeys(p.c_str()); (len = std::strlen(k)) != 0; k += len + 1) {
00221 if (k[len-1] != '.') {
00222 out.push_back(p+k);
00223 if (std::strcmp(k, "__len") == 0 && f.getStat(out.back().c_str()) > 0.0) {
00224 if (f.getKeys((p+"0").c_str())) { getKeys(f, out, p+"0."); }
00225 else { out.push_back(p+"0"); }
00226 }
00227 }
00228 else { getKeys(f, out, p+k); }
00229 }
00230 }
00231 #if WITH_THREADS
00232 typedef ClaspFacade::AsyncResult AsyncResult;
00233 void testAsyncSolveTrivialUnsat() {
00234 ClaspConfig config;
00235 ClaspFacade libclasp;
00236 config.enumerate.numModels = 0;
00237 Asp::LogicProgram& asp = libclasp.startAsp(config, true);
00238 asp.setAtomName(1, "a");
00239 asp.startRule().addHead(1).addToBody(1, false).endRule();
00240 libclasp.prepare(ClaspFacade::enum_volatile);
00241 AsyncResult it = libclasp.startSolveAsync();
00242 CPPUNIT_ASSERT(it.end());
00243 CPPUNIT_ASSERT(it.get().unsat());
00244 }
00245 void testInterruptBeforeSolve() {
00246 ClaspConfig config;
00247 ClaspFacade libclasp;
00248 config.enumerate.numModels = 0;
00249 Asp::LogicProgram& asp = libclasp.startAsp(config, true);
00250 asp.setAtomName(1, "a");
00251 asp.startRule(Asp::CHOICERULE).addHead(1).endRule();
00252 libclasp.prepare(ClaspFacade::enum_volatile);
00253 libclasp.terminate(2);
00254 AsyncResult it = libclasp.startSolveAsync();
00255 CPPUNIT_ASSERT(it.end());
00256 CPPUNIT_ASSERT(it.get().interrupted());
00257 }
00258 void testCancelAsyncOperation() {
00259 ClaspConfig config;
00260 ClaspFacade libclasp;
00261 config.enumerate.numModels = 0;
00262 Asp::LogicProgram& asp = libclasp.startAsp(config, true);
00263 asp.setAtomName(1, "a");
00264 asp.startRule(Asp::CHOICERULE).addHead(1).endRule();
00265 libclasp.prepare(ClaspFacade::enum_volatile);
00266 AsyncResult it = libclasp.startSolveAsync();
00267 while (!it.end()) {
00268 CPPUNIT_ASSERT(it.model().num == 1);
00269 if (it.cancel()){ break; }
00270 }
00271 CPPUNIT_ASSERT(it.end() && !libclasp.solving() && it.interrupted());
00272 libclasp.update();
00273 libclasp.prepare(ClaspFacade::enum_volatile);
00274 it = libclasp.startSolveAsync();
00275 int mod = 0;
00276 while (!it.end()) { ++mod; it.next(); }
00277 CPPUNIT_ASSERT(!libclasp.solving() && mod == 2);
00278 }
00279 void testAsyncResultDtorCancelsOp() {
00280 ClaspConfig config;
00281 ClaspFacade libclasp;
00282 Asp::LogicProgram& asp = libclasp.startAsp(config, true);
00283 asp.setAtomName(1, "a");
00284 asp.startRule(Asp::CHOICERULE).addHead(1).endRule();
00285 libclasp.prepare(ClaspFacade::enum_volatile);
00286 { AsyncResult it = libclasp.startSolveAsync(); }
00287 CPPUNIT_ASSERT(!libclasp.solving() && libclasp.result().interrupted());
00288 }
00289 void testDestroyAsyncResultNoFacade() {
00290 ClaspConfig config;
00291 AsyncResult* handle = 0;
00292 ClaspFacade* libclasp = new ClaspFacade();
00293 Asp::LogicProgram& asp= libclasp->startAsp(config, true);
00294 asp.setAtomName(1, "a");
00295 asp.startRule(Asp::CHOICERULE).addHead(1).endRule();
00296 libclasp->prepare(ClaspFacade::enum_volatile);
00297 handle = new AsyncResult( libclasp->startSolveAsync() );
00298 delete libclasp;
00299 CPPUNIT_ASSERT(handle->interrupted());
00300 CPPUNIT_ASSERT_NO_THROW(delete handle);
00301 }
00302 void testDestroyDanglingAsyncResult() {
00303 ClaspConfig config;
00304 ClaspFacade libclasp;
00305 AsyncResult* handle = 0;
00306 Asp::LogicProgram& asp = libclasp.startAsp(config, true);
00307 asp.setAtomName(1, "a");
00308 asp.startRule(Asp::CHOICERULE).addHead(1).endRule();
00309 libclasp.prepare(ClaspFacade::enum_volatile);
00310 handle = new AsyncResult( libclasp.solveAsync() );
00311 handle->wait();
00312 libclasp.update();
00313 libclasp.prepare(ClaspFacade::enum_volatile);
00314 AsyncResult* it = new AsyncResult(libclasp.startSolveAsync());
00315 delete handle;
00316 CPPUNIT_ASSERT(!it->interrupted() && libclasp.solving());
00317 CPPUNIT_ASSERT_NO_THROW(delete it);
00318 CPPUNIT_ASSERT(!libclasp.solving());
00319 }
00320 void testCancelDanglingAsyncOperation() {
00321 ClaspConfig config;
00322 ClaspFacade libclasp;
00323
00324 Asp::LogicProgram& asp = libclasp.startAsp(config, true);
00325 asp.setAtomName(1, "a");
00326 asp.startRule(Asp::CHOICERULE).addHead(1).endRule();
00327 libclasp.prepare(ClaspFacade::enum_volatile);
00328 AsyncResult step0 = libclasp.solveAsync();
00329 step0.wait();
00330 libclasp.update();
00331 libclasp.prepare(ClaspFacade::enum_volatile);
00332 AsyncResult step1 = libclasp.startSolveAsync();
00333
00334 CPPUNIT_ASSERT_EQUAL(false, step0.cancel());
00335 CPPUNIT_ASSERT(libclasp.solving());
00336 CPPUNIT_ASSERT_EQUAL(true, step1.cancel());
00337 CPPUNIT_ASSERT(!libclasp.solving());
00338 }
00339 #endif
00340 };
00341 CPPUNIT_TEST_SUITE_REGISTRATION(FacadeTest);
00342 } }
00343