- 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 UNFOUNDEDSETCHECKER_H__ 00035 #define UNFOUNDEDSETCHECKER_H__ 00036 00037 #include "dlvhex2/PlatformDefinitions.h" 00038 #include "dlvhex2/fwd.h" 00039 #include "dlvhex2/BaseModelGenerator.h" 00040 #include "dlvhex2/AnnotatedGroundProgram.h" 00041 #include "dlvhex2/ExternalAtomVerificationTree.h" 00042 00043 #include <boost/unordered_map.hpp> 00044 00045 #include <boost/graph/graph_traits.hpp> 00046 #include <boost/graph/adjacency_list.hpp> 00047 #include <boost/shared_ptr.hpp> 00048 00049 DLVHEX_NAMESPACE_BEGIN 00050 00054 class UnfoundedSetChecker 00055 { 00056 protected: 00058 BaseModelGenerator* mg; 00059 00060 enum Mode 00061 { 00063 Ordinary, 00065 WithExt 00066 }; 00068 Mode mode; 00069 00071 ProgramCtx& ctx; 00073 RegistryPtr reg; 00074 00075 // problem specification 00077 const OrdinaryASPProgram& groundProgram; 00079 AnnotatedGroundProgram emptyagp; 00081 const AnnotatedGroundProgram& agp; 00083 InterpretationConstPtr componentAtoms; 00085 ExternalAtomVerificationTree eavTree; 00087 SimpleNogoodContainerPtr ngc; 00089 InterpretationPtr domain; 00090 00097 SATSolverPtr solver; 00098 00106 bool isUnfoundedSet(InterpretationConstPtr compatibleSet, InterpretationConstPtr compatibleSetWithoutAux, InterpretationConstPtr ufsCandidate); 00107 00115 virtual std::pair<bool, Nogood> nogoodTransformation(Nogood ng, InterpretationConstPtr compatibleSet) = 0; 00116 00117 private: 00118 00122 struct UnfoundedSetVerificationStatus 00123 { 00125 InterpretationPtr eaInput; 00126 00132 std::vector<IDAddress> auxiliariesToVerify; 00133 00139 std::vector<std::set<ID> > auxIndexToRemainingExternalAtoms; 00140 00146 std::vector<std::vector<int> > externalAtomAddressToAuxIndices; 00147 00155 UnfoundedSetVerificationStatus( 00156 const AnnotatedGroundProgram& agp, 00157 InterpretationConstPtr domain, InterpretationConstPtr ufsCandidate, InterpretationConstPtr compatibleSet, InterpretationConstPtr compatibleSetWithoutAux); 00158 }; 00159 00167 bool verifyExternalAtomByEvaluation( 00168 ID eaID, 00169 InterpretationConstPtr ufsCandidate, InterpretationConstPtr compatibleSet, 00170 UnfoundedSetVerificationStatus& ufsVerStatus); 00171 00172 public: 00179 UnfoundedSetChecker( 00180 ProgramCtx& ctx, 00181 const OrdinaryASPProgram& groundProgram, 00182 InterpretationConstPtr componentAtoms = InterpretationConstPtr(), 00183 SimpleNogoodContainerPtr ngc = SimpleNogoodContainerPtr()); 00184 00194 UnfoundedSetChecker( 00195 BaseModelGenerator* mg, 00196 ProgramCtx& ctx, 00197 const OrdinaryASPProgram& groundProgram, 00198 const AnnotatedGroundProgram& agp, 00199 InterpretationConstPtr componentAtoms = InterpretationConstPtr(), 00200 SimpleNogoodContainerPtr ngc = SimpleNogoodContainerPtr()); 00201 00202 virtual ~UnfoundedSetChecker() {} 00203 00219 virtual std::vector<IDAddress> getUnfoundedSet(InterpretationConstPtr compatibleSet, const std::set<ID>& skipProgram) = 0; 00220 00224 virtual void learnNogoodsFromMainSearch(bool reset) = 0; 00225 00232 Nogood getUFSNogood( 00233 const std::vector<IDAddress>& ufs, 00234 InterpretationConstPtr interpretation); 00235 00242 Nogood getUFSNogoodReductBased( 00243 const std::vector<IDAddress>& ufs, 00244 InterpretationConstPtr interpretation); 00245 00252 Nogood getUFSNogoodUFSBased( 00253 const std::vector<IDAddress>& ufs, 00254 InterpretationConstPtr interpretation); 00255 00256 typedef boost::shared_ptr<UnfoundedSetChecker> Ptr; 00257 typedef boost::shared_ptr<const UnfoundedSetChecker> ConstPtr; 00258 }; 00259 00260 typedef UnfoundedSetChecker::Ptr UnfoundedSetCheckerPtr; 00261 typedef UnfoundedSetChecker::ConstPtr UnfoundedSetCheckerConstPtr; 00262 00263 class EncodingBasedUnfoundedSetChecker : public UnfoundedSetChecker 00264 { 00265 private: 00277 void constructUFSDetectionProblem( 00278 NogoodSet& ufsDetectionProblem, 00279 InterpretationConstPtr compatibleSet, 00280 InterpretationConstPtr compatibleSetWithoutAux, 00281 const std::set<ID>& skipProgram, 00282 std::vector<ID>& ufsProgram); 00283 00295 void constructUFSDetectionProblemNecessaryPart( 00296 NogoodSet& ufsDetectionProblem, 00297 int& auxatomcnt, 00298 InterpretationConstPtr compatibleSet, 00299 InterpretationConstPtr compatibleSetWithoutAux, 00300 const std::set<ID>& skipProgram, 00301 std::vector<ID>& ufsProgram); 00302 00314 void constructUFSDetectionProblemOptimizationPart( 00315 NogoodSet& ufsDetectionProblem, 00316 int& auxatomcnt, 00317 InterpretationConstPtr compatibleSet, 00318 InterpretationConstPtr compatibleSetWithoutAux, 00319 const std::set<ID>& skipProgram, 00320 std::vector<ID>& ufsProgram); 00321 00334 void constructUFSDetectionProblemOptimizationPartRestrictToCompatibleSet( 00335 NogoodSet& ufsDetectionProblem, 00336 int& auxatomcnt, 00337 InterpretationConstPtr compatibleSet, 00338 InterpretationConstPtr compatibleSetWithoutAux, 00339 const std::set<ID>& skipProgram, 00340 std::vector<ID>& ufsProgram); 00341 00354 void constructUFSDetectionProblemOptimizationPartBasicEAKnowledge( 00355 NogoodSet& ufsDetectionProblem, 00356 int& auxatomcnt, 00357 InterpretationConstPtr compatibleSet, 00358 InterpretationConstPtr compatibleSetWithoutAux, 00359 const std::set<ID>& skipProgram, 00360 std::vector<ID>& ufsProgram); 00361 00374 void constructUFSDetectionProblemOptimizationPartLearnedFromMainSearch( 00375 NogoodSet& ufsDetectionProblem, 00376 int& auxatomcnt, 00377 InterpretationConstPtr compatibleSet, 00378 InterpretationConstPtr compatibleSetWithoutAux, 00379 const std::set<ID>& skipProgram, 00380 std::vector<ID>& ufsProgram); 00381 00394 void constructUFSDetectionProblemOptimizationPartEAEnforement( 00395 NogoodSet& ufsDetectionProblem, 00396 int& auxatomcnt, 00397 InterpretationConstPtr compatibleSet, 00398 InterpretationConstPtr compatibleSetWithoutAux, 00399 const std::set<ID>& skipProgram, 00400 std::vector<ID>& ufsProgram); 00401 00402 std::pair<bool, Nogood> nogoodTransformation(Nogood ng, InterpretationConstPtr compatibleSet); 00403 00404 public: 00412 EncodingBasedUnfoundedSetChecker( 00413 ProgramCtx& ctx, 00414 const OrdinaryASPProgram& groundProgram, 00415 InterpretationConstPtr componentAtoms = InterpretationConstPtr(), 00416 SimpleNogoodContainerPtr ngc = SimpleNogoodContainerPtr()); 00417 00429 EncodingBasedUnfoundedSetChecker( 00430 BaseModelGenerator& mg, 00431 ProgramCtx& ctx, 00432 const OrdinaryASPProgram& groundProgram, 00433 const AnnotatedGroundProgram& agp, 00434 InterpretationConstPtr componentAtoms = InterpretationConstPtr(), 00435 SimpleNogoodContainerPtr ngc = SimpleNogoodContainerPtr()); 00436 00441 void learnNogoodsFromMainSearch(bool reset); 00442 00449 std::vector<IDAddress> getUnfoundedSet( 00450 InterpretationConstPtr compatibleSet, 00451 const std::set<ID>& skipProgram); 00452 }; 00453 00454 class AssumptionBasedUnfoundedSetChecker : public UnfoundedSetChecker 00455 { 00456 private: 00458 boost::unordered_map<IDAddress, IDAddress> interpretationShadow; 00460 boost::unordered_map<IDAddress, IDAddress> residualShadow; 00462 boost::unordered_map<IDAddress, IDAddress> becomeFalse; 00464 boost::unordered_map<IDAddress, IDAddress> IandU; 00466 boost::unordered_map<IDAddress, IDAddress> nIorU; 00467 00469 int atomcnt; 00470 00472 int problemRuleCount; 00473 00475 ID hookAtom; 00476 00477 // stores how many nogoods in ngc we have already transformed and learned in the UFS search 00478 int learnedNogoodsFromMainSearch; 00479 00481 void constructDomain(); 00482 00486 void constructUFSDetectionProblemFacts(NogoodSet& ns); 00487 00491 void constructUFSDetectionProblemCreateAuxAtoms(); 00492 00497 void constructUFSDetectionProblemDefineAuxiliaries(NogoodSet& ns); 00498 00504 void constructUFSDetectionProblemRule(NogoodSet& ns, ID ruleID); 00505 00510 void constructUFSDetectionProblemNonempty(NogoodSet& ns); 00511 00516 void constructUFSDetectionProblemRestrictToSCC(NogoodSet& ns); 00517 00522 void constructUFSDetectionProblemBasicEABehavior(NogoodSet& ns); 00523 00527 void constructUFSDetectionProblemAndInstantiateSolver(); 00528 00532 void expandUFSDetectionProblemAndReinstantiateSolver(); 00533 00539 void setAssumptions(InterpretationConstPtr compatibleSet, const std::set<ID>& skipProgram); 00540 00541 std::pair<bool, Nogood> nogoodTransformation(Nogood ng, InterpretationConstPtr compatibleSet); 00542 00543 public: 00551 AssumptionBasedUnfoundedSetChecker( 00552 ProgramCtx& ctx, 00553 const OrdinaryASPProgram& groundProgram, 00554 InterpretationConstPtr componentAtoms = InterpretationConstPtr(), 00555 SimpleNogoodContainerPtr ngc = SimpleNogoodContainerPtr()); 00556 00568 AssumptionBasedUnfoundedSetChecker( 00569 BaseModelGenerator& mg, 00570 ProgramCtx& ctx, 00571 const OrdinaryASPProgram& groundProgram, 00572 const AnnotatedGroundProgram& agp, 00573 InterpretationConstPtr componentAtoms = InterpretationConstPtr(), 00574 SimpleNogoodContainerPtr ngc = SimpleNogoodContainerPtr()); 00575 00576 void learnNogoodsFromMainSearch(bool reset); 00577 00584 std::vector<IDAddress> getUnfoundedSet(InterpretationConstPtr compatibleSet, const std::set<ID>& skipProgram); 00585 }; 00586 00594 class DLVHEX_EXPORT UnfoundedSetCheckerManager 00595 { 00596 private: 00598 ProgramCtx& ctx; 00599 00601 BaseModelGenerator* mg; 00603 const AnnotatedGroundProgram& agp; 00605 int lastAGPComponentCount; 00607 Nogood ufsnogood; 00609 SimpleNogoodContainerPtr ngc; 00610 00612 std::map<int, UnfoundedSetCheckerPtr> preparedUnfoundedSetCheckers; 00613 00615 std::vector<bool> intersectsWithNonHCFDisjunctiveRules; 00616 00624 bool choiceRuleCompatible; 00625 00630 void computeChoiceRuleCompatibility(bool choiceRuleCompatible); 00631 00637 void computeChoiceRuleCompatibilityForComponent(bool choiceRuleCompatible, int comp); 00638 00646 UnfoundedSetCheckerPtr instantiateUnfoundedSetChecker( 00647 ProgramCtx& ctx, 00648 const OrdinaryASPProgram& groundProgram, 00649 InterpretationConstPtr componentAtoms = InterpretationConstPtr(), 00650 SimpleNogoodContainerPtr ngc = SimpleNogoodContainerPtr()); 00651 00663 UnfoundedSetCheckerPtr instantiateUnfoundedSetChecker( 00664 BaseModelGenerator& mg, 00665 ProgramCtx& ctx, 00666 const OrdinaryASPProgram& groundProgram, 00667 const AnnotatedGroundProgram& agp, 00668 InterpretationConstPtr componentAtoms = InterpretationConstPtr(), 00669 SimpleNogoodContainerPtr ngc = SimpleNogoodContainerPtr()); 00670 00671 public: 00682 UnfoundedSetCheckerManager( 00683 BaseModelGenerator& mg, 00684 ProgramCtx& ctx, 00685 const AnnotatedGroundProgram& agp, 00686 bool choiceRuleCompatible = false, 00687 SimpleNogoodContainerPtr ngc = SimpleNogoodContainerPtr()); 00688 00697 UnfoundedSetCheckerManager( 00698 ProgramCtx& ctx, 00699 const AnnotatedGroundProgram& agp, 00700 bool choiceRuleCompatible = false); 00701 00709 std::vector<IDAddress> getUnfoundedSet( 00710 InterpretationConstPtr interpretation, 00711 const std::set<ID>& skipProgram, 00712 SimpleNogoodContainerPtr ngc = SimpleNogoodContainerPtr()); 00713 00719 std::vector<IDAddress> getUnfoundedSet( 00720 InterpretationConstPtr interpretation); 00721 00725 void initializeUnfoundedSetCheckers(); 00726 00731 void learnNogoodsFromMainSearch(bool reset); 00732 00737 Nogood getLastUFSNogood() const; 00738 00739 typedef boost::shared_ptr<UnfoundedSetCheckerManager> Ptr; 00740 }; 00741 00742 typedef UnfoundedSetCheckerManager::Ptr UnfoundedSetCheckerManagerPtr; 00743 00744 DLVHEX_NAMESPACE_END 00745 #endif 00746 00747 // vim:expandtab:ts=4:sw=4: 00748 // mode: C++ 00749 // End:
1.7.6.1