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 00066 #ifdef HAVE_CONFIG_H 00067 #include "config.h" 00068 #endif // HAVE_CONFIG_H 00069 00070 #include "dlvhex2/EvalHeuristicASP.h" 00071 #include "dlvhex2/EvalHeuristicShared.h" 00072 #include "dlvhex2/Logger.h" 00073 #include "dlvhex2/Registry.h" 00074 #include "dlvhex2/ASPSolver.h" 00075 #include "dlvhex2/Printer.h" 00076 00077 #include <boost/lexical_cast.hpp> 00078 00079 #include <fstream> 00080 #include <sstream> 00081 00082 DLVHEX_NAMESPACE_BEGIN 00083 00084 using namespace evalheur; 00085 00086 EvalHeuristicASP::EvalHeuristicASP(const std::string& scriptname): 00087 Base(), 00088 scriptname(scriptname) 00089 { 00090 } 00091 00092 00093 EvalHeuristicASP::~EvalHeuristicASP() 00094 { 00095 } 00096 00097 00098 namespace 00099 { 00100 00101 typedef ComponentGraph::Component Component; 00102 typedef ComponentGraph::ComponentIterator ComponentIterator; 00103 typedef std::vector<Component> ComponentContainer; 00104 typedef std::set<Component> ComponentSet; 00105 00106 void transformComponentGraphIntoASPFacts( 00107 std::ostream& facts, 00108 std::map<unsigned, Component>& componentindices, 00109 const ComponentGraph& cg, 00110 RegistryPtr reg); 00111 00112 void buildEvalUnitsFromAnswerSet( 00113 EvalGraphBuilder& builder, 00114 AnswerSet::Ptr as, 00115 const std::map<unsigned, Component>& componentindices); 00116 00117 } 00118 00119 00120 // ASP strategy: 00121 // send component graph to ASP 00122 // get commands from first answer set 00123 void EvalHeuristicASP::build(EvalGraphBuilder& builder) 00124 { 00125 typedef ComponentGraph::Component Component; 00126 LOG(INFO,"using ASP evaluation heuristic '" << scriptname << "'"); 00127 00128 const ComponentGraph& compgraph = builder.getComponentGraph(); 00129 00130 // create inputprovider 00131 InputProviderPtr inp(new InputProvider); 00132 00133 std::map<unsigned, Component> componentindices; 00134 00135 std::ostringstream facts; 00136 transformComponentGraphIntoASPFacts(facts, componentindices, compgraph, builder.registry()); 00137 inp->addStringInput(facts.str(), "facts_from_EvalHeuristicASP.cpp"); 00138 00139 // put in program file 00140 inp->addFileInput(scriptname); 00141 00142 #ifdef HAVE_DLV 00143 // send it to DLV aspsolver 00144 WARNING("we could use the general solver used in dlvhex, but this means we need encodings for all heuristics for all solvers") { 00145 ASPSolver::DLVSoftware::Configuration dlvconfig; 00146 ASPSolverManager mgr; 00147 ASPSolverManager::ResultsPtr results = mgr.solve(dlvconfig, *inp, builder.registry()); 00148 // we use the first answer set 00149 // we warn if there are more only in debug mode 00150 AnswerSet::Ptr as = results->getNextAnswerSet(); 00151 if( !as ) 00152 throw std::runtime_error("ASP evaluation heuristic did not return any answer set!"); 00153 DBGLOG(DBG,"evaluation heuristic (first) answer set:"); 00154 DBGLOG(DBG,*as); 00155 00156 buildEvalUnitsFromAnswerSet(builder, as, componentindices); 00157 00158 #ifndef NDEBUG 00159 // display the rest of answer sets 00160 bool first = true; 00161 while( (as = results->getNextAnswerSet()) ) { 00162 if( first ) { 00163 LOG(WARNING,"ASP evaluation heuristic returned more than one answer set (use --verbose=255 to see them)"); 00164 first = false; 00165 } 00166 LOG(DBG,"got superfluous ASP evaluation heuristic answer set:"); 00167 LOG(DBG,*as); 00168 } 00169 #endif 00170 } 00171 #else 00172 throw std::runtime_error("no usable asp solver configured, please implement ASPSolverManager for gringo+clasp or use dlv or integrate libclingo"); 00173 #endif 00174 } 00175 00176 00177 namespace 00178 { 00179 00180 inline void printCommentedWithInfoIfNonempty(std::ostream& out, RawPrinter& pr, const Tuple& ids, const std::string& info) { 00181 if( !ids.empty() ) { 00182 // std::endl is not for cross-platform-line-endings! it is for flushing, and here we do not need flushing. 00183 out << "% " << info << ":\n"; 00184 out << "% "; 00185 pr.printmany(ids, "\n% "); 00186 out << "\n"; 00187 } 00188 } 00189 00190 struct EvalUnitInfo 00191 { 00192 bool gotUnit; 00193 std::list<Component> collapse; 00194 std::list<Component> share; 00195 00196 EvalUnitInfo(): 00197 gotUnit(false) {} 00198 }; 00199 00200 void buildEvalUnitsFromAnswerSet( 00201 EvalGraphBuilder& builder, 00202 AnswerSet::Ptr as, 00203 const std::map<unsigned, Component>& componentindices) { 00204 InterpretationPtr interpretation = as->interpretation; 00205 RegistryPtr reg = interpretation->getRegistry(); 00206 00207 // get ids for interesting preds 00208 Term termunit(ID::MAINKIND_TERM | ID::SUBKIND_TERM_CONSTANT, "unit"); 00209 Term termuse(ID::MAINKIND_TERM | ID::SUBKIND_TERM_CONSTANT, "use"); 00210 Term termshare(ID::MAINKIND_TERM | ID::SUBKIND_TERM_CONSTANT, "share"); 00211 ID idunit = reg->storeConstOrVarTerm(termunit); 00212 ID iduse = reg->storeConstOrVarTerm(termuse); 00213 ID idshare = reg->storeConstOrVarTerm(termshare); 00214 00215 // create answer set projection mask 00216 PredicateMask interestingPreds; 00217 interestingPreds.setRegistry(reg); 00218 interestingPreds.addPredicate(idunit); 00219 interestingPreds.addPredicate(iduse); 00220 interestingPreds.addPredicate(idshare); 00221 interestingPreds.updateMask(); 00222 00223 // project 00224 InterpretationPtr projected(new Interpretation(*interpretation)); 00225 projected->bit_and(*interestingPreds.mask()); 00226 00227 typedef std::map<ID, EvalUnitInfo> UnitMap; 00228 UnitMap um; 00229 00230 // * build um 00231 // * verify all components were used 00232 std::vector<bool> componentsused(componentindices.size(), false); 00233 Interpretation::TrueBitIterator bit, bit_end; 00234 for(boost::tie(bit, bit_end) = projected->trueBits(); 00235 bit != bit_end; ++bit) { 00236 const OrdinaryAtom& gatom = reg->ogatoms.getByAddress(*bit); 00237 00238 assert((gatom.tuple.size() == 2 || gatom.tuple.size() == 3) && 00239 "expecting unit(U), use(U,C), share(U,C) here"); 00240 00241 // lookup or create unit info 00242 EvalUnitInfo& thisunitinfo = um[gatom.tuple[1]]; 00243 00244 if( gatom.tuple.size() == 2 ) { 00245 assert(gatom.tuple[0] == idunit); 00246 thisunitinfo.gotUnit = true; 00247 } 00248 else if( gatom.tuple[0] == iduse ) { 00249 assert(gatom.tuple[2].isIntegerTerm()); 00250 unsigned index = gatom.tuple[2].address; 00251 // implicit assert in next line's -> 00252 thisunitinfo.collapse.push_back(componentindices.find(index)->second); 00253 00254 // verify that all components have been used not more than once 00255 if( componentsused[index] == true ) { 00256 std::ostringstream os; 00257 os << "asp evaluation heuristic uses component " << index << 00258 " exclusively in more than one unit, which is not allowed"; 00259 throw GeneralError(os.str()); 00260 } 00261 componentsused[index] = true; 00262 } 00263 else { 00264 assert(gatom.tuple[0] == idshare); 00265 assert(gatom.tuple[2].isIntegerTerm()); 00266 unsigned index = gatom.tuple[2].address; 00267 // implicit assert in next line's -> 00268 thisunitinfo.share.push_back(componentindices.find(index)->second); 00269 } 00270 } 00271 00272 // verify that all components have been used 00273 for(unsigned idx = 0; idx < componentsused.size(); ++idx) { 00274 if( componentsused[idx] == false ) { 00275 std::ostringstream os; 00276 os << "asp evaluation heuristic did not use component " << idx << 00277 ", which is not allowed"; 00278 throw GeneralError(os.str()); 00279 } 00280 } 00281 00282 // next loop: 00283 // * verify that all units in use/2 and share/2 were received as unit/1 00284 // * create commands from um 00285 // initialize all indices to false 00286 CommandVector cv; 00287 for(UnitMap::const_iterator umit = um.begin(); 00288 umit != um.end(); ++umit) { 00289 const EvalUnitInfo& uinfos = umit->second; 00290 if( !uinfos.gotUnit ) { 00291 LOG(WARNING,"EvalHeuristicASP: did not get unit(" << 00292 printToString<RawPrinter>(umit->first, reg) << 00293 ") while getting commands for that unit"); 00294 } 00295 00296 BuildCommand bc; 00297 bc.collapse.insert(bc.collapse.end(), uinfos.collapse.begin(), uinfos.collapse.end()); 00298 bc.share.insert(bc.share.end(), uinfos.share.begin(), uinfos.share.end()); 00299 cv.push_back(bc); 00300 } 00301 00302 WARNING("maybe we need to sort the build commands here, in topological order of units to be created") 00303 00304 executeBuildCommands(cv, builder); 00305 } 00306 00307 // see documentation at top of file 00308 void transformComponentGraphIntoASPFacts(std::ostream& facts, std::map<unsigned, Component>& componentindices, const ComponentGraph& cg, RegistryPtr reg) { 00309 // put in facts as string 00310 ComponentIterator it, end; 00311 unsigned idx = 0; 00312 std::map<ComponentGraph::Component, std::string> componentidentifier; 00313 #ifndef NDEBUG 00314 RawPrinter pr(facts, reg); 00315 #endif NDEBUG 00316 for(boost::tie(it, end) = cg.getComponents(); it != end; ++it, ++idx) { 00317 const ComponentGraph::ComponentInfo& ci = cg.getComponentInfo(*it); 00318 std::string c(boost::lexical_cast<std::string>(idx)); 00319 componentidentifier[*it] = c; 00320 componentindices[idx] = *it; 00321 00322 // output component debug information 00323 #ifndef NDEBUG 00324 if( Logger::Instance().shallPrint(Logger::DBG) ) { 00325 facts << "% component " << c << ":" << std::endl; 00326 printCommentedWithInfoIfNonempty(facts, pr, ci.outerEatoms, "outerEatoms"); 00327 printCommentedWithInfoIfNonempty(facts, pr, ci.innerRules, "innerRules"); 00328 printCommentedWithInfoIfNonempty(facts, pr, ci.innerEatoms, "innerEatoms"); 00329 printCommentedWithInfoIfNonempty(facts, pr, ci.innerConstraints, "innerConstraints"); 00330 } 00331 #endif 00332 00333 // output the component facts 00334 std::string arg("(" + c + ").\n"); 00335 facts << "component" << arg; 00336 if( !ci.innerRules.empty() ) 00337 facts << "rules" << arg; 00338 if( !ci.innerConstraints.empty() ) 00339 facts << "constraints" << arg; 00340 if( !ci.innerEatoms.empty() ) 00341 facts << "innerext" << arg; 00342 if( !ci.outerEatoms.empty() ) 00343 facts << "outerext" << arg; 00344 if( !ci.disjunctiveHeads ) 00345 facts << "disjheads" << arg; 00346 if( !ci.negativeDependencyBetweenRules ) 00347 facts << "negcycles" << arg; 00348 if( !ci.innerEatomsNonmonotonic ) 00349 facts << "innerextnonmon" << arg; 00350 if( !ci.outerEatomsNonmonotonic ) 00351 facts << "outerextnonmon" << arg; 00352 } 00353 ComponentGraph::DependencyIterator dit, dend; 00354 for(boost::tie(dit, dend) = cg.getDependencies(); dit != dend; ++dit) { 00355 const ComponentGraph::DependencyInfo& di = cg.getDependencyInfo(*dit); 00356 const std::string& src = componentidentifier.find(cg.sourceOf(*dit))->second; 00357 const std::string& tgt = componentidentifier.find(cg.targetOf(*dit))->second; 00358 00359 // output dependency debug information 00360 #ifndef NDEBUG 00361 if( Logger::Instance().shallPrint(Logger::DBG) ) { 00362 facts << "% dependency from " << src << " to " << tgt << "." << std::endl; 00363 } 00364 #endif 00365 00366 // output dependency facts 00367 std::string arg("(" + src + "," + tgt + ").\n"); 00368 facts << "dep" << arg; 00369 if( di.positiveRegularRule ) 00370 facts << "posrule" << arg; 00371 if( di.positiveConstraint ) 00372 facts << "posconstraint" << arg; 00373 if( di.negativeRule ) 00374 facts << "neg" << arg; 00375 assert(!di.unifyingHead); 00376 assert(!di.disjunctive); 00377 if( di.positiveExternal ) 00378 facts << "posext" << arg; 00379 if( di.negativeExternal ) 00380 facts << "negext" << arg; 00381 if( di.externalConstantInput ) 00382 facts << "extconst" << arg; 00383 if( di.externalPredicateInput ) 00384 facts << "extpred" << arg; 00385 } 00386 } 00387 00388 } 00389 00390 00391 DLVHEX_NAMESPACE_END 00392 00393 00394 // vim:expandtab:ts=4:sw=4: 00395 // mode: C++ 00396 // End: