- Generated on Tue Apr 12 2016 15:51:14 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 00034 #ifndef DEPENDENCY_GRAPH_HPP_INCLUDED__18102010 00035 #define DEPENDENCY_GRAPH_HPP_INCLUDED__18102010 00036 00037 #include "dlvhex2/PlatformDefinitions.h" 00038 #include "dlvhex2/fwd.h" 00039 #include "dlvhex2/Logger.h" 00040 #include "dlvhex2/ID.h" 00041 00042 #include <boost/graph/graph_traits.hpp> 00043 #include <boost/graph/adjacency_list.hpp> 00044 #include <boost/shared_ptr.hpp> 00045 00046 #include <boost/multi_index/member.hpp> 00047 #include <boost/multi_index/hashed_index.hpp> 00048 00049 //#include <cassert> 00050 00051 /* 00052 * TODO update paper/formal stuff: 00053 * definition of unifying dependency as in roman's thesis, not as in eswc paper 00054 * rule nodes added to graph 00055 * constraints have extra types of dependencies 00056 * negative dependencies unclear in roman's thesis: def 4.6.2 after second point 2: 00057 * "or b is a non-monotonic external atom" should imho be "or b \in B(r) and b a non-monotonic external atom" 00058 * (doesn't this give us fixed-point vs guess-and-check model generator choice for free?) 00059 * we will add those negative dependencies from rule to body atoms only 00060 * add external dependency if constant input has a variable created by output of other extatom (not covered by roman's thesis) 00061 * auxiliary rules do not take all body literals with the external atom's input variable, they only take positive literals! 00062 * (this is stated differently in the thesis. perhaps it would be more efficient to take the 00063 * transitive closure of dependencies over variables to make the body larger (and therefore reduce the grounding) 00064 * example: &foo[X](), bar(X,Y), not baz(X,Z), boo(Z) -> is it more efficient to take all body atoms instead of only bar(X,Y)?) 00065 * 00066 * for eval only: 00067 * create auxiliary input collecting predicates/rule before creating depedency graph 00068 * pos dependency from ext. atom to its auxiliary input collecting predicate 00069 */ 00070 00071 DLVHEX_NAMESPACE_BEGIN 00072 00074 class DependencyGraph 00075 { 00077 // types 00079 public: 00081 struct NodeInfo: 00082 public ostream_printable<NodeInfo> 00083 { 00084 // ID storage: 00085 // store rule as rule 00086 // store external atom body literal as atom (in non-naf-negated form) 00087 // store nothing else as node 00089 ID id; 00090 00093 NodeInfo(ID id=ID_FAIL): id(id) {} 00094 std::ostream& print(std::ostream& o) const; 00095 }; 00096 00128 struct DependencyInfo: 00129 public ostream_printable<DependencyInfo> 00130 { 00131 bool positiveRegularRule; 00132 bool positiveConstraint; 00133 bool negativeRule; 00134 bool unifyingHead; 00135 bool disjunctive; 00136 bool positiveExternal; 00137 bool negativeExternal; 00138 bool externalConstantInput; 00139 bool externalPredicateInput; 00140 bool externalNonmonotonicPredicateInput; 00141 00143 DependencyInfo(): 00144 positiveRegularRule(false), 00145 positiveConstraint(false), 00146 negativeRule(false), 00147 unifyingHead(false), 00148 disjunctive(false), 00149 positiveExternal(false), 00150 negativeExternal(false), 00151 externalConstantInput(false), 00152 externalPredicateInput(false), 00153 externalNonmonotonicPredicateInput(false) 00154 {} 00155 00161 const DependencyInfo& operator|=(const DependencyInfo& other); 00162 std::ostream& print(std::ostream& o) const; 00163 }; 00164 00165 // for out-edge list we use vecS so we may have duplicate edges which is not a 00166 // problem (at least not for the SCC algorithm, for drawing the graph we must take 00167 // care a bit, but drawing a graph need not be efficient) 00168 // 00169 // for vertices it is necesssary to use vecS because so many nice algorithms need 00170 // implicit vertex_index 00171 // 00172 // TODO: do we need bidirectional? (at the moment yes, to find roots and leaves) 00173 typedef boost::adjacency_list< 00174 boost::vecS, boost::vecS, boost::bidirectionalS, 00175 NodeInfo, DependencyInfo> Graph; 00176 typedef boost::graph_traits<Graph> Traits; 00177 00178 typedef Graph::vertex_descriptor Node; 00179 typedef Graph::edge_descriptor Dependency; 00180 typedef Traits::vertex_iterator NodeIterator; 00181 typedef Traits::edge_iterator DependencyIterator; 00182 typedef Traits::out_edge_iterator PredecessorIterator; 00183 typedef Traits::in_edge_iterator SuccessorIterator; 00184 00185 protected: 00186 // the node mapping maps IDs of external atoms and rules 00187 // to nodes of the dependency graph 00189 struct IDTag {}; 00191 struct NodeMappingInfo 00192 { 00193 ID id; 00194 Node node; 00195 NodeMappingInfo(): id(ID_FAIL) {} 00196 NodeMappingInfo(ID id, Node node): id(id), node(node) {} 00197 }; 00198 typedef boost::multi_index_container< 00199 NodeMappingInfo, 00200 boost::multi_index::indexed_by< 00201 boost::multi_index::hashed_unique< 00202 boost::multi_index::tag<IDTag>, 00203 BOOST_MULTI_INDEX_MEMBER(NodeMappingInfo,ID,id) 00204 > 00205 > 00206 > NodeMapping; 00207 typedef NodeMapping::index<IDTag>::type NodeIDIndex; 00208 00209 protected: 00210 typedef std::vector<Node> NodeList; 00212 struct HeadBodyInfo 00213 { 00215 ID id; 00217 bool inHead; 00219 bool inBody; 00221 NodeList inHeadOfNondisjunctiveRules; 00223 NodeList inHeadOfDisjunctiveRules; 00225 NodeList inPosBodyOfRegularRules; 00227 NodeList inPosBodyOfConstraints; 00229 NodeList inNegBodyOfRules; 00231 ID headPredicate; 00233 const OrdinaryAtom* oatom; 00234 00237 HeadBodyInfo(const OrdinaryAtom* oatom = NULL): 00238 id(ID_FAIL), inHead(false), inBody(false), 00239 headPredicate(ID_FAIL), oatom(oatom) {} 00240 }; 00241 00243 struct InHeadTag {}; 00245 struct InBodyTag {}; 00247 struct HeadPredicateTag {}; 00249 struct HeadBodyHelper 00250 { 00251 typedef boost::multi_index_container< 00252 HeadBodyInfo, 00253 boost::multi_index::indexed_by< 00254 boost::multi_index::hashed_unique< 00255 boost::multi_index::tag<IDTag>, 00256 BOOST_MULTI_INDEX_MEMBER(HeadBodyInfo,ID,id) 00257 >, 00258 boost::multi_index::hashed_non_unique< 00259 boost::multi_index::tag<InHeadTag>, 00260 BOOST_MULTI_INDEX_MEMBER(HeadBodyInfo,bool,inHead) 00261 >, 00262 boost::multi_index::hashed_non_unique< 00263 boost::multi_index::tag<InBodyTag>, 00264 BOOST_MULTI_INDEX_MEMBER(HeadBodyInfo,bool,inBody) 00265 >, 00266 boost::multi_index::hashed_non_unique< 00267 boost::multi_index::tag<HeadPredicateTag>, 00268 BOOST_MULTI_INDEX_MEMBER(HeadBodyInfo,ID,headPredicate) 00269 > 00270 > 00271 > HBInfos; 00272 typedef HBInfos::index<IDTag>::type IDIndex; 00273 typedef HBInfos::index<InHeadTag>::type InHeadIndex; 00274 typedef HBInfos::index<InBodyTag>::type InBodyIndex; 00275 typedef HBInfos::index<HeadPredicateTag>::type HeadPredicateIndex; 00276 00278 HBInfos infos; 00279 }; 00280 00282 // members 00284 protected: 00286 ProgramCtx& ctx; 00288 RegistryPtr registry; 00290 Graph dg; 00292 NodeMapping nm; 00293 00295 // methods 00297 private: 00302 DependencyGraph(const Dependency& other); 00303 public: 00307 DependencyGraph(ProgramCtx& ctx, RegistryPtr registry); 00309 virtual ~DependencyGraph(); 00310 00314 void createDependencies(const std::vector<ID>& idb, std::vector<ID>& createdAuxRules); 00315 00319 virtual void writeGraphViz(std::ostream& o, bool verbose) const; 00320 00323 const Graph& getInternalGraph() const 00324 { return dg; } 00325 00326 // get node given some object id 00327 inline Node getNode(ID id) const 00328 { 00329 const NodeIDIndex& idx = nm.get<IDTag>(); 00330 NodeIDIndex::const_iterator it = idx.find(id); 00331 assert(it != idx.end()); 00332 return it->node; 00333 } 00334 00338 inline std::pair<NodeIterator, NodeIterator> getNodes() const 00339 { return boost::vertices(dg); } 00340 00344 inline const NodeInfo& getNodeInfo(Node node) const 00345 { return dg[node]; } 00346 00350 inline const DependencyInfo& getDependencyInfo(Dependency dep) const 00351 { return dg[dep]; } 00352 00356 inline std::pair<PredecessorIterator, PredecessorIterator> 00357 getDependencies(Node node) const 00358 { return boost::out_edges(node, dg); } 00359 00363 inline std::pair<SuccessorIterator, SuccessorIterator> 00364 getProvides(Node node) const 00365 { return boost::in_edges(node, dg); } 00366 00370 inline Node sourceOf(Dependency d) const 00371 { return boost::source(d, dg); } 00372 00376 inline Node targetOf(Dependency d) const 00377 { return boost::target(d, dg); } 00378 00382 inline const NodeInfo& propsOf(Node n) const 00383 { return dg[n]; } 00387 inline NodeInfo& propsOf(Node n) 00388 { return dg[n]; } 00392 inline const DependencyInfo& propsOf(Dependency d) const 00393 { return dg[d]; } 00397 inline DependencyInfo& propsOf(Dependency d) 00398 { return dg[d]; } 00399 00400 // counting -> mainly for allocating and testing 00401 inline unsigned countNodes() const 00402 { return boost::num_vertices(dg); } 00403 inline unsigned countDependencies() const 00404 { return boost::num_edges(dg); } 00405 00406 protected: 00410 inline Node createNode(ID id); 00411 00412 protected: 00421 void createNodesAndIntraRuleDependencies( 00422 const std::vector<ID>& idb, 00423 std::vector<ID>& createdAuxRules, 00424 HeadBodyHelper& hbh); 00425 // helpers 00430 void createNodesAndIntraRuleDependenciesForRule( 00431 ID idrule, 00432 std::vector<ID>& createdAuxRules, 00433 HeadBodyHelper& hbh); 00439 void createNodesAndIntraRuleDependenciesForRuleAddHead( 00440 ID idat, const Rule& rule, Node nrule, HeadBodyHelper& hbh); 00449 void createNodesAndIntraRuleDependenciesForBody( 00450 ID idlit, ID idrule, const Tuple& body, Node nrule, 00451 HeadBodyHelper& hbh, std::vector<ID>& createdAuxRules, 00452 bool inAggregateBody = false); 00468 void createAuxiliaryRuleIfRequired( 00469 const Tuple& body, 00470 ID idlit, ID idat, Node neatom, const ExternalAtom& eatom, 00471 const PluginAtom* pluginAtom, 00472 std::vector<ID>& createdAuxRules, 00473 HeadBodyHelper& hbh); 00477 ID createAuxiliaryRuleHeadPredicate(ID forEAtom); 00482 ID createAuxiliaryRuleHead(ID idauxpred, const std::list<ID>& variables); 00487 ID createAuxiliaryRule(ID head, const std::list<ID>& body); 00488 00491 void createExternalPredicateInputDependencies(const HeadBodyHelper& hbh); 00492 // helpers 00498 void createExternalPredicateInputDependenciesForInput( 00499 bool nonmonotonic, const NodeMappingInfo& ni_eatom, ID predicate, const HeadBodyHelper& hbh); 00500 00503 void createUnifyingDependencies(const HeadBodyHelper& hbh); 00504 // helpers 00507 void createHeadHeadUnifyingDependencies(const HeadBodyHelper& hbh); 00510 void createHeadBodyUnifyingDependencies(const HeadBodyHelper& hbh); 00511 00512 protected: 00513 // helpers for writeGraphViz: extend for more output 00518 virtual void writeGraphVizNodeLabel(std::ostream& o, Node n, bool verbose) const; 00523 virtual void writeGraphVizDependencyLabel(std::ostream& o, Dependency dep, bool verbose) const; 00524 }; 00525 00526 DependencyGraph::Node DependencyGraph::createNode(ID id) 00527 { 00528 DBGLOG(DBG,"creating node for ID " << id); 00529 Node n = boost::add_vertex(NodeInfo(id), dg); 00530 { 00531 NodeIDIndex::const_iterator it; 00532 bool success; 00533 boost::tie(it, success) = nm.insert(NodeMappingInfo(id, n)); 00534 assert(success); 00535 } 00536 return n; 00537 } 00538 00539 00540 DLVHEX_NAMESPACE_END 00541 #endif // DEPENDENCY_GRAPH_HPP_INCLUDED__18102010 00542 00543 // vim:expandtab:ts=4:sw=4: 00544 // mode: C++ 00545 // End:
1.7.6.1