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 INTERNALGROUNDASPSOLVER_HPP_INCLUDED__09122011 00035 #define INTERNALGROUNDASPSOLVER_HPP_INCLUDED__09122011 00036 00037 #include "dlvhex2/ID.h" 00038 #include "dlvhex2/Interpretation.h" 00039 #include "dlvhex2/ProgramCtx.h" 00040 #include <vector> 00041 #include <set> 00042 #include <map> 00043 #include <boost/foreach.hpp> 00044 #include "dlvhex2/Printhelpers.h" 00045 #include "CDNLSolver.h" 00046 #include "dlvhex2/OrdinaryASPProgram.h" 00047 #include "dlvhex2/AnnotatedGroundProgram.h" 00048 #include "dlvhex2/GenuineSolver.h" 00049 //#include <bm/bm.h> 00050 #include <boost/graph/graph_traits.hpp> 00051 #include <boost/graph/adjacency_list.hpp> 00052 #include <boost/shared_ptr.hpp> 00053 00054 DLVHEX_NAMESPACE_BEGIN 00055 00056 #ifdef _MSC_VER 00057 // suppresses warning C4250: 'dlvhex::InternalGroundASPSolver' : inherits 'dlvhex::CDNLSolver::dlvhex::CDNLSolver::addNogood' via dominance 00058 // (there is a compiler bug in MSVC; the call of addNogood is actually _not_ ambigious because the method is pure virtual in GenuineGroundSolver) 00059 #pragma warning (disable: 4250) 00060 #endif 00061 00062 class InternalGroundASPSolver : public CDNLSolver, public GenuineGroundSolver 00063 { 00064 private: 00066 std::string bodyAtomPrefix; 00068 int bodyAtomNumber; 00069 00070 protected: 00072 bool firstmodel; 00074 int modelCount; 00075 00076 protected: 00077 // structural program information 00079 AnnotatedGroundProgram program; 00081 RegistryPtr reg; 00082 00084 Set<IDAddress> ordinaryFacts; 00086 InterpretationPtr ordinaryFactsInt; 00088 Set<IDAddress> nonSingularFacts; 00089 00090 // dependency graph 00091 typedef boost::adjacency_list<boost::vecS, boost::vecS, boost::bidirectionalS, IDAddress> Graph; 00092 typedef Graph::vertex_descriptor Node; 00094 boost::unordered_map<IDAddress, Node, SimpleHashIDAddress> depNodes; 00096 Graph depGraph; 00097 00099 std::vector<Set<IDAddress> > depSCC; 00101 boost::unordered_map<IDAddress, int, SimpleHashIDAddress> componentOfAtom; 00103 boost::unordered_map<IDAddress, IDAddress, SimpleHashIDAddress> bodyAtomOfRule; 00104 00105 // data structures for unfounded set computation 00107 Set<IDAddress> unfoundedAtoms; 00109 boost::unordered_map<IDAddress, Set<ID>, SimpleHashIDAddress > rulesWithPosBodyLiteral; 00111 boost::unordered_map<IDAddress, Set<ID>, SimpleHashIDAddress > rulesWithNegBodyLiteral; 00113 boost::unordered_map<IDAddress, Set<ID>, SimpleHashIDAddress > rulesWithPosHeadLiteral; 00115 boost::unordered_map<IDAddress, Set<IDAddress>, SimpleHashIDAddress > foundedAtomsOfBodyAtom; 00117 boost::unordered_map<IDAddress, ID, SimpleHashIDAddress> sourceRule; 00118 00119 // statistics 00121 long cntDetectedUnfoundedSets; 00122 00123 // initialization members 00127 void createNogoodsForRule(ID ruleBodyAtomID, ID ruleID); 00131 void createNogoodsForRuleBody(ID ruleBodyAtomID, const Tuple& ruleBody); 00137 Set<std::pair<ID, ID> > createShiftedProgram(); 00139 void computeClarkCompletion(); 00143 void createSingularLoopNogoods(InterpretationConstPtr frozen); 00144 virtual void resizeVectors(); 00146 void setEDB(); 00148 void computeDepGraph(); 00150 void computeStronglyConnectedComponents(); 00152 void initSourcePointers(); 00156 void initializeLists(InterpretationConstPtr frozen); 00157 00158 // unfounded set members 00159 virtual void setFact(ID fact, int dl, int cause); 00160 virtual void clearFact(IDAddress litadr); 00163 void removeSourceFromAtom(IDAddress litadr); 00167 void addSourceToAtom(IDAddress litadr, ID rule); 00171 Set<IDAddress> getDependingAtoms(IDAddress litadr); 00175 void getInitialNewlyUnfoundedAtomsAfterSetFact(ID fact, Set<IDAddress>& newlyUnfoundedAtoms); 00178 void updateUnfoundedSetStructuresAfterSetFact(ID fact); 00181 void updateUnfoundedSetStructuresAfterClearFact(IDAddress litadr); 00182 ID getPossibleSourceRule(const Set<ID>& ufs); 00187 bool useAsNewSourceForHeadAtom(IDAddress headAtom, ID sourceRule); 00190 Set<ID> getUnfoundedSet(); 00191 00192 // helper members 00202 bool doesRuleExternallySupportLiteral(ID ruleID, ID lit, const Set<ID>& s); 00206 Set<ID> getExternalSupport(const Set<ID>& s); 00214 Set<ID> satisfiesIndependently(ID ruleID, const Set<ID>& y); 00218 Nogood getLoopNogood(const Set<ID>& ufs); 00222 ID createNewAtom(ID predID); 00225 ID createNewBodyAtom(); 00229 std::string toString(const Set<ID>& lits); 00233 std::string toString(const Set<IDAddress>& lits); 00237 std::string toString(const std::vector<IDAddress>& lits); 00238 00243 template <typename T> 00244 inline std::vector<T> intersect(const Set<T>& a, const std::vector<T>& b) { 00245 std::vector<T> i; 00246 BOOST_FOREACH (T el, a) { 00247 if (contains(b, el)) i.push_back(el); 00248 } 00249 return i; 00250 } 00251 00256 template <typename T> 00257 inline Set<T> intersect(const Set<T>& a, const Set<T>& b) { 00258 Set<T> out; 00259 std::set_intersection(a.begin(), a.end(), b.begin(), b.end(), insert_set_iterator<T>(out)); 00260 return out; 00261 } 00262 00266 InterpretationPtr outputProjection(InterpretationConstPtr intr); 00267 public: 00276 InternalGroundASPSolver(ProgramCtx& ctx, const AnnotatedGroundProgram& p, InterpretationConstPtr frozen = InterpretationConstPtr()); 00277 virtual void addProgram(const AnnotatedGroundProgram& p, InterpretationConstPtr frozen = InterpretationConstPtr()); 00278 virtual Nogood getInconsistencyCause(InterpretationConstPtr explanationAtoms); 00279 virtual void addNogoodSet(const NogoodSet& ns, InterpretationConstPtr frozen = InterpretationConstPtr()); 00280 00281 virtual void restartWithAssumptions(const std::vector<ID>& assumptions); 00282 virtual void addPropagator(PropagatorCallback* pb); 00283 virtual void removePropagator(PropagatorCallback* pb); 00284 virtual void setOptimum(std::vector<int>& optimum); 00285 virtual InterpretationPtr getNextModel(); 00286 virtual int getModelCount(); 00287 virtual std::string getStatistics(); 00288 00293 std::string getImplicationGraphAsDotString(); 00294 00295 typedef boost::shared_ptr<InternalGroundASPSolver> Ptr; 00296 typedef boost::shared_ptr<const InternalGroundASPSolver> ConstPtr; 00297 }; 00298 #ifdef _MSC_VER 00299 #pragma warning (default: 4250) 00300 #endif 00301 00302 typedef InternalGroundASPSolver::Ptr InternalGroundASPSolverPtr; 00303 typedef InternalGroundASPSolver::ConstPtr InternalGroundASPSolverConstPtr; 00304 00305 DLVHEX_NAMESPACE_END 00306 #endif 00307 00308 // vim:expandtab:ts=4:sw=4: 00309 // mode: C++ 00310 // End: