- Generated on Tue Apr 12 2016 15:51:15 for dlvhex by
1.7.6.1
|
dlvhex
2.5.0
|
00001 /* dlvhex -- Answer-Set Programming with external interfaces. 00002 * Copyright (C) 2005-2007 Roman Schindlauer 00003 * Copyright (C) 2006-2015 Thomas Krennwallner 00004 * Copyright (C) 2009-2016 Peter Schüller 00005 * Copyright (C) 2011-2016 Christoph Redl 00006 * Copyright (C) 2015-2016 Tobias Kaminski 00007 * Copyright (C) 2015-2016 Antonius Weinzierl 00008 * 00009 * This file is part of dlvhex. 00010 * 00011 * dlvhex is free software; you can redistribute it and/or modify it 00012 * under the terms of the GNU Lesser General Public License as 00013 * published by the Free Software Foundation; either version 2.1 of 00014 * the License, or (at your option) any later version. 00015 * 00016 * dlvhex is distributed in the hope that it will be useful, but 00017 * WITHOUT ANY WARRANTY; without even the implied warranty of 00018 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU 00019 * Lesser General Public License for more details. 00020 * 00021 * You should have received a copy of the GNU Lesser General Public 00022 * License along with dlvhex; if not, write to the Free Software 00023 * Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA 00024 * 02110-1301 USA. 00025 */ 00026 00035 #ifdef HAVE_CONFIG_H 00036 #include "config.h" 00037 #endif // HAVE_CONFIG_H 00038 00039 #include "dlvhex2/FLPModelGeneratorBase.h" 00040 #include "dlvhex2/Printer.h" 00041 #include "dlvhex2/ProgramCtx.h" 00042 #include "dlvhex2/LiberalSafetyChecker.h" 00043 00044 #include "dlvhex2/CDNLSolver.h" 00045 #include "dlvhex2/ClaspSolver.h" 00046 #include "dlvhex2/SATSolver.h" 00047 #include "dlvhex2/Printer.h" 00048 00049 #include <boost/graph/graph_traits.hpp> 00050 #include <boost/graph/adjacency_list.hpp> 00051 #include <boost/graph/breadth_first_search.hpp> 00052 #include <boost/graph/visitors.hpp> 00053 00054 #include <fstream> 00055 00056 DLVHEX_NAMESPACE_BEGIN 00057 00058 FLPModelGeneratorFactoryBase::FLPModelGeneratorFactoryBase( 00059 ProgramCtx& ctx): 00060 ctx(ctx), reg(ctx.registry()) 00061 { 00062 gpMask.setRegistry(reg); 00063 gnMask.setRegistry(reg); 00064 fMask.setRegistry(reg); 00065 } 00066 00067 00076 void FLPModelGeneratorFactoryBase::createEatomGuessingRules(const ProgramCtx& ctx) 00077 { 00078 std::set<ID> innerEatomsSet(innerEatoms.begin(), innerEatoms.end()); 00079 assert((innerEatomsSet.empty() || 00080 (!innerEatomsSet.begin()->isLiteral() && innerEatomsSet.begin()->isExternalAtom())) && 00081 "we don't want literals here, we want external atoms"); 00082 00083 DBGLOG_SCOPE(DBG,"cEAGR",false); 00084 BOOST_FOREACH(ID rid, idb) { 00085 // skip rules without external atoms 00086 if( !rid.doesRuleContainExtatoms() ) 00087 continue; 00088 00089 // do not guess external atoms in auxiliary input rules 00090 // because those rules may not contain all relevant body atoms which provide grounding 00091 // if ( rid.isExternalInputAuxiliary() ) 00092 // continue; 00093 00094 const Rule& r = reg->rules.getByID(rid); 00095 DBGLOG(DBG,"processing rule with external atom(s): " << printToString<RawPrinter>(rid, reg) << 00096 " (rid " << rid << "r " << r << ")"); 00097 00098 BOOST_FOREACH(ID lit, r.body) { 00099 // skip atoms that are not external atoms 00100 if( !lit.isExternalAtom() ) 00101 continue; 00102 00103 if( innerEatomsSet.count(ID::atomFromLiteral(lit)) == 0 ) 00104 continue; 00105 00106 gidb.push_back(createEatomGuessingRule(ctx, rid, lit)); 00107 } 00108 } 00109 } 00110 00111 00112 ID FLPModelGeneratorFactoryBase::createEatomGuessingRule(const ProgramCtx& ctx, ID rid, ID lit) 00113 { 00114 const Rule& r = reg->rules.getByID(rid); 00115 const ExternalAtom& eatom = reg->eatoms.getByID(lit); 00116 DBGLOG(DBG,"processing external atom " << printToString<RawPrinter>(lit, reg) << 00117 " (lit " << lit << " eatom " << eatom << ")"); 00118 DBGLOG_INDENT(DBG); 00119 00120 // prepare replacement atom 00121 OrdinaryAtom replacement( 00122 ID::MAINKIND_ATOM | ID::PROPERTY_AUX | ID::PROPERTY_EXTERNALAUX); 00123 00124 // tuple: (replacement_predicate, inputs_as_in_inputtuple*, outputs*) 00125 // (build up incrementally) 00126 ID pospredicate = reg->getAuxiliaryConstantSymbol('r', eatom.predicate); 00127 ID negpredicate = reg->getAuxiliaryConstantSymbol('n', eatom.predicate); 00128 00129 replacement.tuple.push_back(pospredicate); 00130 gpMask.addPredicate(pospredicate); 00131 gnMask.addPredicate(negpredicate); 00132 00133 if (ctx.config.getOption("IncludeAuxInputInAuxiliaries") && eatom.auxInputPredicate != ID_FAIL) 00134 replacement.tuple.push_back(eatom.auxInputPredicate); 00135 00136 // build (nonground) replacement and harvest all variables 00137 std::set<ID> variables; 00138 BOOST_FOREACH(ID inp, eatom.inputs) { 00139 replacement.tuple.push_back(inp); 00140 if( inp.isVariableTerm() ) 00141 variables.insert(inp); 00142 } 00143 BOOST_FOREACH(ID outp, eatom.tuple) { 00144 replacement.tuple.push_back(outp); 00145 if( outp.isVariableTerm() ) 00146 variables.insert(outp); 00147 } 00148 DBGLOG(DBG,"found set of variables: " << printManyToString<RawPrinter>(Tuple(variables.begin(), variables.end()), ",", reg)); 00149 00150 // groundness of replacement predicate 00151 ID posreplacement; 00152 ID negreplacement; 00153 if( variables.empty() ) { 00154 replacement.kind |= ID::SUBKIND_ATOM_ORDINARYG; 00155 posreplacement = reg->storeOrdinaryGAtom(replacement); 00156 replacement.tuple[0] = negpredicate; 00157 negreplacement = reg->storeOrdinaryGAtom(replacement); 00158 } 00159 else { 00160 replacement.kind |= ID::SUBKIND_ATOM_ORDINARYN; 00161 posreplacement = reg->storeOrdinaryNAtom(replacement); 00162 replacement.tuple[0] = negpredicate; 00163 negreplacement = reg->storeOrdinaryNAtom(replacement); 00164 } 00165 DBGLOG(DBG,"registered posreplacement " << printToString<RawPrinter>(posreplacement, reg) << 00166 " and negreplacement " << printToString<RawPrinter>(negreplacement, reg)); 00167 00168 // create rule head 00169 Rule guessingrule(ID::MAINKIND_RULE | ID::SUBKIND_RULE_REGULAR | 00170 ID::PROPERTY_AUX | ID::PROPERTY_RULE_DISJ); 00171 guessingrule.head.push_back(posreplacement); 00172 guessingrule.head.push_back(negreplacement); 00173 00174 // create rule body (if there are variables that need to be grounded) 00175 if( !variables.empty() ) { 00176 // harvest all positive ordinary nonground atoms 00177 // "grounding the variables" (i.e., those that contain them) 00178 BOOST_FOREACH(ID lit, r.body) { 00179 if( lit.isNaf() || 00180 lit.isExternalAtom() ) 00181 continue; 00182 00183 bool use = false; 00184 if( lit.isOrdinaryNongroundAtom() ) { 00185 const OrdinaryAtom& oatom = reg->onatoms.getByID(lit); 00186 // look if this atom grounds any variables we need 00187 BOOST_FOREACH(ID term, oatom.tuple) { 00188 if( term.isVariableTerm() && 00189 (variables.find(term) != variables.end()) ) { 00190 use = true; 00191 break; 00192 } 00193 } 00194 } 00195 else if( lit.isBuiltinAtom() ) { 00196 const BuiltinAtom& biatom = reg->batoms.getByID(lit); 00197 // !=, <, >, <= and >= cannot provide grounding 00198 if (biatom.tuple[0].address == ID::TERM_BUILTIN_NE || biatom.tuple[0].address == ID::TERM_BUILTIN_LT || biatom.tuple[0].address == ID::TERM_BUILTIN_LE || 00199 biatom.tuple[0].address == ID::TERM_BUILTIN_GT || biatom.tuple[0].address == ID::TERM_BUILTIN_GE) continue; 00200 00201 // look if this atom grounds any variables we need 00202 BOOST_FOREACH(ID term, biatom.tuple) { 00203 if( term.isVariableTerm() && 00204 (variables.find(term) != variables.end()) ) { 00205 use = true; 00206 break; 00207 } 00208 } 00209 } 00210 else if (lit.isAggregateAtom()) { 00211 // take the aggregate iff it defines a variable to be grounded 00212 const AggregateAtom& aatom = reg->aatoms.getByID(lit); 00213 DBGLOG(DBG, "Checking if aggregate is included in guessing rule"); 00214 if ( (aatom.tuple[1].address == ID::TERM_BUILTIN_EQ && aatom.tuple[0].isVariableTerm() && variables.find(aatom.tuple[0]) != variables.end()) || (aatom.tuple[3].address == ID::TERM_BUILTIN_EQ && aatom.tuple[4].isVariableTerm() && variables.find(aatom.tuple[4]) != variables.end())) { 00215 DBGLOG(DBG, "Aggregate is included in guessing rule"); 00216 use = true; 00217 } 00218 } 00219 00220 if( use ) { 00221 guessingrule.body.push_back(lit); 00222 } 00223 } 00224 } 00225 00226 // the auxiliary input also provides grounding (potentially) 00227 if (eatom.auxInputPredicate != ID_FAIL) { 00228 DBGLOG(DBG, "Adding auxiliary input predicate " << printToString<RawPrinter>(eatom.auxInputPredicate,reg) << " to guessing rule"); 00229 OrdinaryAtom auxinput(ID::MAINKIND_ATOM | ID::SUBKIND_ATOM_ORDINARYN | ID::PROPERTY_AUX | ID::PROPERTY_EXTERNALINPUTAUX); 00230 auxinput.tuple.push_back(eatom.auxInputPredicate); 00231 // resize to hold input predicate and all aux input variables 00232 auxinput.tuple.resize(eatom.auxInputMapping.size()+1,ID_FAIL); 00233 // now assign correct variables from inputs to aux inputs 00234 unsigned at = 1; 00235 for(ExternalAtom::AuxInputMapping::const_iterator itaim = eatom.auxInputMapping.begin(); 00236 itaim != eatom.auxInputMapping.end(); ++itaim, ++at) { 00237 typedef std::list<unsigned> UList; 00238 const UList& varplaces = *itaim; 00239 ID current = ID_FAIL; 00240 assert(!varplaces.empty() && "cannot have empty variable mapping"); 00241 for(UList::const_iterator it = varplaces.begin(); 00242 it != varplaces.end(); ++it) { 00243 if( it == varplaces.begin() ) { 00244 // set the variable 00245 current = eatom.inputs[*it]; 00246 } 00247 else { 00248 // verify the variable 00249 assert(current == eatom.inputs[*it] && "something went wrong with auxInputMapping!"); 00250 } 00251 } 00252 auxinput.tuple[at] = current; 00253 } 00254 ID aiid = reg->storeOrdinaryNAtom(auxinput); 00255 DBGLOG(DBG,"created auxiliary grounding predicate " << printToString<RawPrinter>(aiid,reg) << " which got id " << aiid); 00256 guessingrule.body.push_back(ID::posLiteralFromAtom(aiid)); 00257 } 00258 00259 // store rule 00260 ID gid = reg->storeRule(guessingrule); 00261 DBGLOG(DBG,"stored guessingrule " << printToString<RawPrinter>(gid, reg) << " which got id " << gid); 00262 return gid; 00263 } 00264 00265 00277 void FLPModelGeneratorFactoryBase::createFLPRules() 00278 { 00279 DBGLOG_SCOPE(DBG,"cFLPR",false); 00280 BOOST_FOREACH(ID rid, xidb) { 00281 const Rule& r = reg->rules.getByID(rid); 00282 DBGLOG(DBG,"processing rule " << rid << " " << r); 00283 if( r.body.empty() ) { 00284 // keep disjunctive facts as they are 00285 xidbflphead.push_back(rid); 00286 xidbflpbody.push_back(rid); 00287 } 00288 else if( rid.isConstraint() || rid.isRegularRule() ) { 00289 // collect all variables 00290 std::set<ID> variables; 00291 BOOST_FOREACH(ID lit, r.body) { 00292 assert(!lit.isExternalAtom() && "in xidb there must not be external atoms left"); 00293 WARNING("TODO factorize get all (free) variables from entity") 00294 // from ground literals we don't need variables 00295 if( lit.isOrdinaryGroundAtom() ) 00296 continue; 00297 00298 if( lit.isOrdinaryNongroundAtom() ) { 00299 const OrdinaryAtom& onatom = reg->onatoms.getByID(lit); 00300 BOOST_FOREACH(ID idt, onatom.tuple) { 00301 if( idt.isVariableTerm() ) 00302 variables.insert(idt); 00303 } 00304 } 00305 else if( lit.isBuiltinAtom() ) { 00306 const BuiltinAtom& batom = reg->batoms.getByID(lit); 00307 BOOST_FOREACH(ID idt, batom.tuple) { 00308 if( idt.isVariableTerm() ) 00309 variables.insert(idt); 00310 } 00311 } 00312 else if( lit.isAggregateAtom() ) { 00313 // use boundaries as variables, variables in aggregate are free or (automatically) bound by context in rule 00314 const AggregateAtom& aatom = reg->aatoms.getByID(lit); 00315 if( aatom.tuple[0] != ID_FAIL && aatom.tuple[0].isVariableTerm() ) 00316 variables.insert(aatom.tuple[0]); 00317 if( aatom.tuple[4] != ID_FAIL && aatom.tuple[4].isVariableTerm() ) 00318 variables.insert(aatom.tuple[4]); 00319 } 00320 else { 00321 LOG(ERROR,"encountered literal " << lit << " in FLP check, don't know what to do about it"); 00322 throw FatalError("TODO: think about how to treat other types of atoms in FLP check"); 00323 } 00324 } 00325 DBGLOG(DBG,"collected variables " << printset(variables)); 00326 00327 // prepare replacement atom 00328 OrdinaryAtom replacement( 00329 ID::MAINKIND_ATOM | ID::PROPERTY_AUX | ID::PROPERTY_FLPAUX); 00330 00331 // tuple: (replacement_predicate, variables*) 00332 ID flppredicate = reg->getAuxiliaryConstantSymbol('f', rid); 00333 replacement.tuple.push_back(flppredicate); 00334 fMask.addPredicate(flppredicate); 00335 00336 // groundness of replacement predicate 00337 ID fid; 00338 if( variables.empty() ) { 00339 replacement.kind |= ID::SUBKIND_ATOM_ORDINARYG; 00340 fid = reg->storeOrdinaryGAtom(replacement); 00341 } 00342 else { 00343 replacement.kind |= ID::SUBKIND_ATOM_ORDINARYN; 00344 replacement.tuple.insert(replacement.tuple.end(), 00345 variables.begin(), variables.end()); 00346 fid = reg->storeOrdinaryNAtom(replacement); 00347 } 00348 DBGLOG(DBG,"registered flp replacement " << replacement << 00349 " with fid " << fid); 00350 00351 // create rules 00352 Rule rflphead( 00353 ID::MAINKIND_RULE | ID::SUBKIND_RULE_REGULAR | ID::PROPERTY_AUX); 00354 rflphead.head.push_back(fid); 00355 rflphead.body = r.body; 00356 00357 // kind will be overwritten 00358 Rule rflpbody(ID::MAINKIND_RULE | ID::SUBKIND_RULE_REGULAR); 00359 00360 // Note: EA-aux input rules MUST NOT be shifted! This could eliminate models of the reduct 00361 if( r.isEAAuxInputRule() || ctx.config.getOption("ExplicitFLPUnshift") == 1 ) { 00362 // original set of rules 00363 IDKind kind = ID::MAINKIND_RULE | ID::PROPERTY_AUX; 00364 if (r.head.size() == 0) { 00365 kind |= ID::SUBKIND_RULE_CONSTRAINT; 00366 } 00367 else { 00368 kind |= ID::SUBKIND_RULE_REGULAR; 00369 } 00370 rflpbody.kind = kind; 00371 rflpbody.head = r.head; 00372 if( rflpbody.head.size() > 1 ) 00373 rflpbody.kind |= ID::PROPERTY_RULE_DISJ; 00374 rflpbody.body = r.body; 00375 rflpbody.body.push_back(fid); 00376 } 00377 else { 00378 // optimized set of rules 00379 // another encoding which is more efficient on some examples: 00380 IDKind kind = ID::MAINKIND_RULE | ID::SUBKIND_RULE_CONSTRAINT | ID::PROPERTY_AUX; 00381 rflpbody.kind = kind | ID::SUBKIND_RULE_CONSTRAINT; 00382 rflpbody.body = r.body; 00383 rflpbody.body.push_back(fid); 00384 BOOST_FOREACH (ID h, r.head) { 00385 rflpbody.body.push_back(ID::literalFromAtom(h, true)); 00386 } 00387 } 00388 00389 // store rules 00390 ID fheadrid = reg->storeRule(rflphead); 00391 xidbflphead.push_back(fheadrid); 00392 ID fbodyrid = reg->storeRule(rflpbody); 00393 xidbflpbody.push_back(fbodyrid); 00394 00395 #ifndef NDEBUG 00396 { 00397 std::stringstream s; 00398 RawPrinter p(s, reg); 00399 p.print(fheadrid); 00400 s << " and "; 00401 p.print(fbodyrid); 00402 DBGLOG(DBG,"stored flphead rule " << rflphead << " which got id " << fheadrid); 00403 DBGLOG(DBG,"stored flpbody rule " << rflpbody << " which got id " << fbodyrid); 00404 DBGLOG(DBG,"rules are " << s.str()); 00405 } 00406 #endif 00407 } 00408 else { 00409 LOG(ERROR,"got weak rule " << r << " in guess and check model generator, don't know what to do about it"); 00410 throw FatalError("TODO: think about weak rules in G&C MG"); 00411 } 00412 } 00413 } 00414 00415 00416 // 00417 // FLPModelGeneratorBase 00418 // 00419 00420 FLPModelGeneratorBase::FLPModelGeneratorBase( 00421 FLPModelGeneratorFactoryBase& _factory, InterpretationConstPtr input): 00422 BaseModelGenerator(input), 00423 factory(_factory), 00424 annotatedGroundProgram(_factory.ctx, _factory.innerEatoms) 00425 { 00426 } 00427 00428 00429 bool FLPModelGeneratorBase::isCompatibleSet( 00430 InterpretationConstPtr candidateCompatibleSet, 00431 InterpretationConstPtr postprocessedInput, 00432 ProgramCtx& ctx, 00433 SimpleNogoodContainerPtr nc) 00434 { 00435 RegistryPtr& reg = factory.reg; 00436 PredicateMask& gpMask = factory.gpMask; 00437 PredicateMask& gnMask = factory.gnMask; 00438 00439 // project to pos and neg eatom replacements for validation 00440 InterpretationPtr projint(new Interpretation(reg)); 00441 projint->getStorage() = candidateCompatibleSet->getStorage() - postprocessedInput->getStorage(); 00442 00443 gpMask.updateMask(); 00444 InterpretationPtr projectedModelCandidate_pos(new Interpretation(reg)); 00445 projectedModelCandidate_pos->getStorage() = projint->getStorage() & gpMask.mask()->getStorage(); 00446 InterpretationPtr projectedModelCandidate_pos_val(new Interpretation(reg)); 00447 projectedModelCandidate_pos_val->getStorage() = projectedModelCandidate_pos->getStorage(); 00448 DBGLOG(DBG,"projected positive guess: " << *projectedModelCandidate_pos); 00449 00450 gnMask.updateMask(); 00451 InterpretationPtr projectedModelCandidate_neg(new Interpretation(reg)); 00452 projectedModelCandidate_neg->getStorage() = projint->getStorage() & gnMask.mask()->getStorage(); 00453 DBGLOG(DBG,"projected negative guess: " << *projectedModelCandidate_neg); 00454 00455 // verify whether correct eatoms where guessed true 00456 // this callback checks if a positive eatom result was guessed as negative 00457 // -> in this case it aborts 00458 // this callback resets all positive bits it encounters 00459 // -> if the positive interpretation is all-zeroes at the end, 00460 // the guess was correct 00461 VerifyExternalAnswerAgainstPosNegGuessInterpretationCB cb( 00462 projectedModelCandidate_pos_val, projectedModelCandidate_neg); 00463 00464 // we might need edb facts here 00465 // (dependencies to edb are not modelled in the dependency graph) 00466 // therefore we did not mask the guess program before 00467 if( !evaluateExternalAtoms( 00468 ctx, factory.innerEatoms, 00469 candidateCompatibleSet, cb, 00470 ctx.config.getOption("ExternalLearning") ? nc : SimpleNogoodContainerPtr())) { 00471 return false; 00472 } 00473 00474 // check if we guessed too many true atoms 00475 if (projectedModelCandidate_pos_val->getStorage().count() > 0) { 00476 return false; 00477 } 00478 return true; 00479 } 00480 00481 00482 Nogood FLPModelGeneratorBase::getFLPNogood( 00483 ProgramCtx& ctx, 00484 const OrdinaryASPProgram& groundProgram, 00485 InterpretationConstPtr compatibleSet, 00486 InterpretationConstPtr projectedCompatibleSet, 00487 InterpretationConstPtr smallerFLPModel 00488 ) 00489 { 00490 00491 RegistryPtr reg = factory.reg; 00492 00493 Nogood ng; 00494 00495 // for each rule with unsatisfied body 00496 BOOST_FOREACH (ID ruleId, groundProgram.idb) { 00497 const Rule& rule = reg->rules.getByID(ruleId); 00498 BOOST_FOREACH (ID b, rule.body) { 00499 if (compatibleSet->getFact(b.address) != !b.isNaf()) { 00500 // take an unsatisfied body literal 00501 ng.insert(NogoodContainer::createLiteral(b.address, compatibleSet->getFact(b.address))); 00502 break; 00503 } 00504 } 00505 } 00506 00507 // add the smaller FLP model 00508 bm::bvector<>::enumerator en = smallerFLPModel->getStorage().first(); 00509 bm::bvector<>::enumerator en_end = smallerFLPModel->getStorage().end(); 00510 while (en < en_end) { 00511 ng.insert(NogoodContainer::createLiteral(*en)); 00512 en++; 00513 } 00514 00515 // add one atom which is in the compatible set but not in the flp model 00516 en = projectedCompatibleSet->getStorage().first(); 00517 en_end = projectedCompatibleSet->getStorage().end(); 00518 while (en < en_end) { 00519 if (!smallerFLPModel->getFact(*en)) { 00520 ng.insert(NogoodContainer::createLiteral(*en)); 00521 break; 00522 } 00523 en++; 00524 } 00525 00526 DBGLOG(DBG, "Constructed FLP nogood " << ng); 00527 00528 return ng; 00529 } 00530 00531 00532 WARNING("TODO could we move shadow predicates and mappings and rules to factory?") 00533 void FLPModelGeneratorBase::computeShadowAndUnfoundedPredicates( 00534 RegistryPtr reg, 00535 InterpretationConstPtr edb, 00536 const std::vector<ID>& idb, 00537 std::map<ID, std::pair<int, ID> >& shadowPredicates, 00538 std::map<ID, std::pair<int, ID> >& unfoundedPredicates, 00539 std::string& shadowPostfix, 00540 std::string& unfoundedPostfix) 00541 { 00542 00543 // collect predicates 00544 std::set<std::pair<int, ID> > preds; 00545 00546 // edb 00547 bm::bvector<>::enumerator en = edb->getStorage().first(); 00548 bm::bvector<>::enumerator en_end = edb->getStorage().end(); 00549 while (en < en_end) { 00550 if (!reg->ogatoms.getIDByAddress(*en).isExternalAuxiliary() && !reg->ogatoms.getIDByAddress(*en).isFLPAuxiliary()) { 00551 const OrdinaryAtom& atom = reg->ogatoms.getByAddress(*en); 00552 preds.insert(std::pair<int, ID>(atom.tuple.size() - 1, atom.tuple.front())); 00553 } 00554 en++; 00555 } 00556 00557 // idb 00558 BOOST_FOREACH (ID rid, idb) { 00559 const Rule& r = reg->rules.getByID(rid); 00560 BOOST_FOREACH (ID h, r.head) { 00561 if (!h.isExternalAuxiliary() && !h.isFLPAuxiliary()) { 00562 const OrdinaryAtom& atom = h.isOrdinaryGroundAtom() ? reg->ogatoms.getByID(h) : reg->onatoms.getByID(h); 00563 preds.insert(std::pair<int, ID>(atom.tuple.size() - 1, atom.tuple.front())); 00564 } 00565 } 00566 BOOST_FOREACH (ID b, r.body) { 00567 if (b.isOrdinaryAtom() && !b.isExternalAuxiliary() && !b.isFLPAuxiliary()) { 00568 const OrdinaryAtom& atom = b.isOrdinaryGroundAtom() ? reg->ogatoms.getByID(b) : reg->onatoms.getByID(b); 00569 preds.insert(std::pair<int, ID>(atom.tuple.size() - 1, atom.tuple.front())); 00570 } 00571 } 00572 } 00573 00574 // create unique predicate suffix for shadow predicates 00575 // (must not start with _ as it will be used by itself and 00576 // constants starting with _ are forbidden in dlv as they are not c-identifiers) 00577 shadowPostfix = "shadow"; 00578 int idx = 0; 00579 bool clash; 00580 do { 00581 clash = false; 00582 00583 // check if the current postfix clashes with any of the predicates 00584 typedef std::pair<int, ID> Pair; 00585 BOOST_FOREACH (Pair p, preds) { 00586 std::string currentPred = reg->terms.getByID(p.second).getUnquotedString(); 00587 // currentPred is at least as long as shadowPostfix 00588 if (shadowPostfix.length() <= currentPred.length() && 00589 // postfixes coincide 00590 currentPred.substr(currentPred.length() - shadowPostfix.length()) == shadowPostfix) { 00591 clash = true; 00592 break; 00593 } 00594 } 00595 std::stringstream ss; 00596 ss << "shadow" << idx++; 00597 }while(clash); 00598 00599 // create shadow predicates 00600 typedef std::pair<int, ID> Pair; 00601 BOOST_FOREACH (Pair p, preds) { 00602 Term shadowTerm(ID::MAINKIND_TERM | ID::SUBKIND_TERM_CONSTANT, reg->terms.getByID(p.second).getUnquotedString() + shadowPostfix); 00603 ID shadowID = reg->storeTerm(shadowTerm); 00604 shadowPredicates[p.second] = Pair(p.first, shadowID); 00605 DBGLOG(DBG, "Predicate " << reg->terms.getByID(p.second).getUnquotedString() << " [" << p.second << "] has shadow predicate " << 00606 reg->terms.getByID(p.second).getUnquotedString() + shadowPostfix << " [" << shadowID << "]"); 00607 } 00608 00609 // create unfounded predicate suffix for shadow predicates 00610 unfoundedPostfix = "_unfounded"; 00611 idx = 0; 00612 do { 00613 clash = false; 00614 00615 // check if the current postfix clashes with any of the predicates 00616 typedef std::pair<int, ID> Pair; 00617 BOOST_FOREACH (Pair p, preds) { 00618 std::string currentPred = reg->terms.getByID(p.second).getUnquotedString(); 00619 // currentPred is at least as long as shadowPostfix 00620 if (unfoundedPostfix.length() <= currentPred.length() && 00621 // postfixes coincide 00622 currentPred.substr(currentPred.length() - unfoundedPostfix.length()) == unfoundedPostfix) { 00623 clash = true; 00624 break; 00625 } 00626 } 00627 std::stringstream ss; 00628 ss << "unfounded" << idx++; 00629 }while(clash); 00630 00631 // create unfounded predicates 00632 BOOST_FOREACH (Pair p, preds) { 00633 Term unfoundedTerm(ID::MAINKIND_TERM | ID::SUBKIND_TERM_CONSTANT, reg->terms.getByID(p.second).getUnquotedString() + unfoundedPostfix); 00634 ID unfoundedID = reg->storeTerm(unfoundedTerm); 00635 unfoundedPredicates[p.second] = Pair(p.first, unfoundedID); 00636 DBGLOG(DBG, "Predicate " << reg->terms.getByID(p.second).getUnquotedString() << " [" << p.second << "] has unfounded predicate " << 00637 reg->terms.getByID(p.second).getUnquotedString() + unfoundedPostfix << " [" << unfoundedID << "]"); 00638 } 00639 } 00640 00641 00642 void FLPModelGeneratorBase::addShadowInterpretation( 00643 RegistryPtr reg, 00644 std::map<ID, std::pair<int, ID> >& shadowPredicates, 00645 InterpretationConstPtr input, 00646 InterpretationPtr output) 00647 { 00648 00649 bm::bvector<>::enumerator en = input->getStorage().first(); 00650 bm::bvector<>::enumerator en_end = input->getStorage().end(); 00651 while (en < en_end) { 00652 OrdinaryAtom atom = reg->ogatoms.getByID(ID(ID::MAINKIND_ATOM | ID::SUBKIND_ATOM_ORDINARYG, *en)); 00653 if (shadowPredicates.find(atom.tuple[0]) != shadowPredicates.end()) { 00654 atom.tuple[0] = shadowPredicates[atom.tuple[0]].second; 00655 output->setFact(reg->storeOrdinaryGAtom(atom).address); 00656 } 00657 en++; 00658 } 00659 } 00660 00661 00662 void FLPModelGeneratorBase::createMinimalityRules( 00663 RegistryPtr reg, 00664 std::map<ID, std::pair<int, ID> >& shadowPredicates, 00665 std::string& shadowPostfix, 00666 std::vector<ID>& idb) 00667 { 00668 00669 // construct a propositional atom which does neither occur in the input program nor as a shadow predicate 00670 // for this purpose we use the shadowPostfix alone: 00671 // - it cannot be used by the input program (otherwise it would not be a postfix) 00672 // - it cannot be used by the shadow atoms (otherwise an input atom would be the empty string, which is not possible) 00673 Term smallerTerm(ID::MAINKIND_TERM | ID::SUBKIND_TERM_CONSTANT, shadowPostfix); 00674 OrdinaryAtom smallerAtom(ID::MAINKIND_ATOM | ID::SUBKIND_ATOM_ORDINARYG); 00675 smallerAtom.tuple.push_back(reg->storeTerm(smallerTerm)); 00676 ID smallerAtomID = reg->storeOrdinaryGAtom(smallerAtom); 00677 00678 typedef std::pair<ID, std::pair<int, ID> > Pair; 00679 BOOST_FOREACH (Pair p, shadowPredicates) { 00680 OrdinaryAtom atom(ID::MAINKIND_ATOM); 00681 if (p.second.first == 0) atom.kind |= ID::SUBKIND_ATOM_ORDINARYG; else atom.kind |= ID::SUBKIND_ATOM_ORDINARYN; 00682 if (p.first.isAuxiliary()) atom.kind |= ID::PROPERTY_AUX; 00683 atom.tuple.push_back(p.first); 00684 for (int i = 0; i < p.second.first; ++i) { 00685 std::stringstream var; 00686 var << "X" << i; 00687 atom.tuple.push_back(reg->storeVariableTerm(var.str())); 00688 } 00689 00690 // store original atom 00691 ID origID; 00692 if (p.second.first == 0) { 00693 origID = reg->storeOrdinaryGAtom(atom); 00694 } 00695 else { 00696 origID = reg->storeOrdinaryNAtom(atom); 00697 } 00698 00699 // store shadow atom 00700 atom.kind = ID::MAINKIND_ATOM; 00701 if (p.second.first == 0) atom.kind |= ID::SUBKIND_ATOM_ORDINARYG; else atom.kind |= ID::SUBKIND_ATOM_ORDINARYN; 00702 atom.tuple[0] = p.second.second; 00703 ID shadowID; 00704 if (p.second.first == 0) { 00705 shadowID = reg->storeOrdinaryGAtom(atom); 00706 } 00707 else { 00708 shadowID = reg->storeOrdinaryNAtom(atom); 00709 } 00710 DBGLOG(DBG, "Using shadow predicate for " << p.first << " which is " << p.second.second); 00711 00712 // an atom must not be true if the shadow atom is false because the computed interpretation must be a subset of the shadow interpretation 00713 { 00714 // construct rule :- a, not a_shadow to ensure that the models are (not necessarily proper) subsets of the shadow model 00715 Rule r(ID::MAINKIND_RULE | ID::SUBKIND_RULE_CONSTRAINT); 00716 ID id = origID; 00717 r.body.push_back(id); 00718 id = ID(ID::MAINKIND_LITERAL | ID::NAF_MASK | (shadowID.kind & ID::SUBKIND_MASK), shadowID.address); 00719 r.body.push_back(id); 00720 idb.push_back(reg->storeRule(r)); 00721 } 00722 00723 // but we want a proper subset, so add a rule smaller :- a_shadow, not a 00724 // an atom must not be true if the shadow atom is false because the computed interpretation must be a subset of the shadow interpretation 00725 { 00726 // construct rule :- a, not a_shadow to ensure that the models are (not necessarily proper) subsets of the shadow model 00727 Rule r(ID::MAINKIND_RULE | ID::SUBKIND_RULE_REGULAR); 00728 ID id = smallerAtomID; 00729 r.head.push_back(id); 00730 id = ID(ID::MAINKIND_LITERAL | ID::NAF_MASK | (origID.kind & ID::SUBKIND_MASK), origID.address); 00731 r.body.push_back(id); 00732 r.body.push_back(shadowID); 00733 idb.push_back(reg->storeRule(r)); 00734 } 00735 } 00736 00737 // construct a rule :- not smaller to restrict the search space to proper submodels of the shadow model 00738 Rule r(ID::MAINKIND_RULE | ID::SUBKIND_RULE_CONSTRAINT); 00739 r.body.push_back(ID(ID::MAINKIND_LITERAL | ID::SUBKIND_ATOM_ORDINARYG | ID::NAF_MASK, smallerAtomID.address)); 00740 idb.push_back(reg->storeRule(r)); 00741 } 00742 00743 00744 void FLPModelGeneratorBase::createFoundingRules( 00745 RegistryPtr reg, 00746 std::map<ID, std::pair<int, ID> >& shadowPredicates, 00747 std::map<ID, std::pair<int, ID> >& unfoundedPredicates, 00748 std::vector<ID>& idb) 00749 { 00750 00751 // We want to compute a _model_ of the reduct rather than an _answer set_, 00752 // i.e., atoms are allowed to be _not_ founded. 00753 // For this we introduce for each n-ary shadow predicate 00754 // ps(X1, ..., Xn) 00755 // a rule 00756 // p(X1, ..., Xn) v p_unfounded(X1, ..., Xn) :- ps(X1, ..., Xn) 00757 // which can be used to found an atom. 00758 // (p_unfounded(X1, ..., Xn) encodes that the atom is not artificially founded) 00759 00760 typedef std::pair<ID, std::pair<int, ID> > Pair; 00761 BOOST_FOREACH (Pair p, shadowPredicates) { 00762 OrdinaryAtom atom(ID::MAINKIND_ATOM); 00763 if (p.second.first == 0) atom.kind |= ID::SUBKIND_ATOM_ORDINARYG; else atom.kind |= ID::SUBKIND_ATOM_ORDINARYN; 00764 if (p.first.isAuxiliary()) atom.kind |= ID::PROPERTY_AUX; 00765 atom.tuple.push_back(p.first); 00766 for (int i = 0; i < p.second.first; ++i) { 00767 std::stringstream var; 00768 var << "X" << i; 00769 atom.tuple.push_back(reg->storeVariableTerm(var.str())); 00770 } 00771 00772 // store original atom 00773 ID origID; 00774 if (p.second.first == 0) { 00775 origID = reg->storeOrdinaryGAtom(atom); 00776 } 00777 else { 00778 origID = reg->storeOrdinaryNAtom(atom); 00779 } 00780 00781 // store unfounded atom 00782 atom.kind = ID::MAINKIND_ATOM; 00783 if (p.second.first == 0) atom.kind |= ID::SUBKIND_ATOM_ORDINARYG; else atom.kind |= ID::SUBKIND_ATOM_ORDINARYN; 00784 atom.tuple[0] = unfoundedPredicates[p.first].second; 00785 ID unfoundedID; 00786 if (p.second.first == 0) { 00787 unfoundedID = reg->storeOrdinaryGAtom(atom); 00788 } 00789 else { 00790 unfoundedID = reg->storeOrdinaryNAtom(atom); 00791 } 00792 00793 // store shadow atom 00794 atom.kind = ID::MAINKIND_ATOM; 00795 if (p.second.first == 0) atom.kind |= ID::SUBKIND_ATOM_ORDINARYG; else atom.kind |= ID::SUBKIND_ATOM_ORDINARYN; 00796 atom.tuple[0] = p.second.second; 00797 ID shadowID; 00798 if (p.second.first == 0) { 00799 shadowID = reg->storeOrdinaryGAtom(atom); 00800 } 00801 else { 00802 shadowID = reg->storeOrdinaryNAtom(atom); 00803 } 00804 DBGLOG(DBG, "Using shadow predicate for " << p.first << " which is " << p.second.second << " and unfounded predicate which is " << unfoundedPredicates[p.first].second); 00805 00806 // for each shadow atom, either the original atom or the notfounded atom is derived 00807 { 00808 Rule r(ID::MAINKIND_RULE | ID::SUBKIND_RULE_REGULAR | ID::PROPERTY_RULE_DISJ); 00809 r.head.push_back(origID); 00810 r.head.push_back(unfoundedID); 00811 r.body.push_back(shadowID); 00812 idb.push_back(reg->storeRule(r)); 00813 } 00814 } 00815 } 00816 00817 00818 DLVHEX_NAMESPACE_END 00819 00820 // vim:expandtab:ts=4:sw=4: 00821 // mode: C++ 00822 // End:
1.7.6.1