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 #if !defined(_DLVHEX_PROGRAMCTX_H) 00036 #define _DLVHEX_PROGRAMCTX_H 00037 00038 #include "dlvhex2/PlatformDefinitions.h" 00039 #include "dlvhex2/fwd.h" 00040 #include "dlvhex2/Configuration.h" 00041 #include "dlvhex2/ASPSolverManager.h" 00042 #include "dlvhex2/Interpretation.h" 00043 #include "dlvhex2/PluginContainer.h" 00044 #include "dlvhex2/InputProvider.h" 00045 #include "dlvhex2/FinalEvalGraph.h" 00046 #include "dlvhex2/EvalHeuristicBase.h" 00047 #include "dlvhex2/EvalGraphBuilder.h" 00048 #include "dlvhex2/ExternalAtomEvaluationHeuristicsInterface.h" 00049 #include "dlvhex2/UnfoundedSetCheckHeuristics.h" 00050 #include "dlvhex2/ModelBuilder.h" 00051 #include "dlvhex2/Registry.h" 00052 #include "dlvhex2/Nogood.h" 00053 00054 #include <boost/shared_ptr.hpp> 00055 #include <boost/functional/factory.hpp> 00056 00057 #include <typeinfo> 00058 #include <vector> 00059 #include <string> 00060 #include <iosfwd> 00061 00062 DLVHEX_NAMESPACE_BEGIN 00063 00064 typedef boost::shared_ptr<EvalHeuristicBase<EvalGraphBuilder> > 00065 EvalHeuristicPtr; 00066 00067 typedef boost::shared_ptr<ModelBuilder<FinalEvalGraph> > 00068 ModelBuilderPtr; 00069 00070 typedef boost::function<ModelBuilder<FinalEvalGraph>*(ModelBuilderConfig<FinalEvalGraph>&)> 00071 ModelBuilderFactory; 00072 00073 typedef std::map<std::string, PluginAtomPtr> 00074 PluginAtomMap; 00075 00081 class DLVHEX_EXPORT ProgramCtx 00082 { 00083 public: 00085 Configuration config; 00086 00089 const RegistryPtr& registry() const 00090 { return _registry; } 00091 00094 const PluginContainerPtr& pluginContainer() const 00095 { return _pluginContainer; } 00096 00099 PluginAtomMap& pluginAtomMap() 00100 { return pluginAtoms; } 00101 00106 void setupRegistry(RegistryPtr registry); 00107 00113 void changeRegistry(RegistryPtr registry); 00114 00117 void setupPluginContainer(PluginContainerPtr pluginContainer); 00118 00120 EvalHeuristicPtr evalHeuristic; 00122 ModelBuilderFactory modelBuilderFactory; 00124 ExternalAtomEvaluationHeuristicsFactoryPtr defaultExternalAtomEvaluationHeuristicsFactory; 00126 UnfoundedSetCheckHeuristicsFactoryPtr unfoundedSetCheckHeuristicsFactory; 00127 00129 ASPSolverManager::SoftwareConfigurationPtr aspsoftware; 00130 00132 InputProviderPtr inputProvider; 00133 00135 HexParserPtr parser; 00136 00138 std::vector<ID> idb; 00139 std::vector<std::vector<ID> > idbList; 00140 00142 Interpretation::Ptr edb; 00144 std::vector<InterpretationPtr> edbList; 00145 00147 uint32_t maxint; 00148 00152 PluginInterfacePtr customModelGeneratorProvider; 00153 00158 std::vector<int> currentOptimum; 00164 unsigned currentOptimumRelevantLevels; 00165 00166 // used by plugins to store specific plugin data in ProgramCtx 00167 // default constructs PluginT::CtxData if it is not yet stored in ProgramCtx 00168 template<typename PluginT> 00169 typename PluginT::CtxData& getPluginData(); 00170 00174 template<typename PluginT> 00175 typename PluginT::Environment& getPluginEnvironment(); 00176 template<typename PluginT> 00177 const typename PluginT::Environment& getPluginEnvironment() const; 00178 00179 // TODO: add visibility policy (as in clasp) 00181 DependencyGraphPtr depgraph; 00183 ComponentGraphPtr compgraph; 00185 std::vector<LiberalSafetyPluginFactoryPtr> liberalSafetyPlugins; 00187 LiberalSafetyCheckerPtr liberalSafetyChecker; 00189 FinalEvalGraphPtr evalgraph; 00191 FinalEvalGraph::EvalUnit ufinal; 00193 std::list<ModelCallbackPtr> modelCallbacks; 00195 std::list<FinalCallbackPtr> finalCallbacks; 00197 ModelBuilderPtr modelBuilder; 00198 // model graph is only accessible via modelbuilder->getModelGraph()! 00199 // (model graph is part of the model builder) TODO think about that 00200 00202 std::map<std::string, std::string> benchmarksToSnapshotAtFirstModel; 00203 00205 StatePtr state; 00206 00213 bool terminationRequest; 00214 00217 void 00218 changeState(const boost::shared_ptr<State>& s); 00219 00220 public: 00222 ProgramCtx(); 00226 ~ProgramCtx(); 00227 00230 ASPSolverManager::SoftwareConfigurationPtr 00231 getASPSoftware() const; 00232 00235 void 00236 setASPSoftware(ASPSolverManager::SoftwareConfigurationPtr c); 00237 00238 // 00239 // plugin helpers 00240 // 00241 00246 void processPluginOptions(std::list<const char*>& pluginOptions); 00247 00249 void addPluginAtomsFromPluginContainer(); 00250 00253 void addPluginAtom(PluginAtomPtr atom); 00254 00260 void associateExtAtomsWithPluginAtoms(const Tuple& idb, bool failOnUnknownAtom=true); 00261 00263 void setupByPlugins(); 00264 00269 void resetCacheOfPlugins(bool resetOnlyIfUsesEnvironment=true); 00270 00271 // 00272 // state processing 00273 // the following functions are given in intended order of calling 00274 // optional functions may be omitted 00275 // 00276 00280 void showPlugins(); 00284 void convert(); 00286 void parse(); 00288 void moduleSyntaxCheck(); 00290 void mlpSolver(); 00294 void rewriteEDBIDB(); 00298 void safetyCheck(); 00300 void createDependencyGraph(); 00302 void liberalSafetyCheck(); 00306 void optimizeEDBDependencyGraph(); 00308 void createComponentGraph(); 00312 void strongSafetyCheck(); 00314 void createEvalGraph(); 00316 void setupProgramCtx(); 00318 void evaluate(); 00320 void postProcess(); 00321 00323 class SubprogramAnswerSetCallback : public ModelCallback 00324 { 00325 public: 00327 std::vector<InterpretationPtr> answersets; 00330 virtual bool operator()(AnswerSetPtr model); 00332 virtual ~SubprogramAnswerSetCallback(); 00333 }; 00338 std::vector<InterpretationPtr> evaluateSubprogram(InterpretationConstPtr edb, std::vector<ID>& idb); 00343 std::vector<InterpretationPtr> evaluateSubprogram(InputProviderPtr& ip, InterpretationConstPtr addFacts); 00347 std::vector<InterpretationPtr> evaluateSubprogram(ProgramCtx& pc, bool parse); 00348 00349 protected: 00354 RegistryPtr _registry; 00355 00357 PluginContainerPtr _pluginContainer; 00358 00359 typedef std::map<std::string, boost::shared_ptr<PluginData> > PluginDataContainer; 00363 PluginDataContainer pluginData; 00364 00365 typedef std::map<std::string, boost::shared_ptr<PluginEnvironment> > PluginEnvironmentContainer; 00369 PluginEnvironmentContainer pluginEnvironment; 00370 00372 PluginAtomMap pluginAtoms; 00373 }; 00374 00375 // used by plugins to store specific plugin data in ProgramCtx 00376 // default constructs PluginT::CtxData if it is not yet stored in ProgramCtx 00377 template<typename PluginT> 00378 typename PluginT::CtxData& ProgramCtx::getPluginData() 00379 { 00380 const std::string pluginTypeName(typeid(PluginT).name()); 00381 PluginDataContainer::const_iterator it = 00382 pluginData.find(pluginTypeName); 00383 if( it == pluginData.end() ) { 00384 it = pluginData.insert(std::make_pair( 00385 pluginTypeName, 00386 boost::shared_ptr<PluginData>(new typename PluginT::CtxData)) 00387 ).first; 00388 } 00389 typename PluginT::CtxData* pret = 00390 dynamic_cast<typename PluginT::CtxData*>(it->second.get()); 00391 assert(!!pret); 00392 return *pret; 00393 } 00394 00395 00396 // used by plugins to store specific plugin data in ProgramCtx 00397 // default constructs PluginT::Environment if it is not yet stored in ProgramCtx 00398 template<typename PluginT> 00399 typename PluginT::Environment& ProgramCtx::getPluginEnvironment() 00400 { 00401 const std::string pluginTypeName(typeid(PluginT).name()); 00402 PluginEnvironmentContainer::const_iterator it = 00403 pluginEnvironment.find(pluginTypeName); 00404 if( it == pluginEnvironment.end() ) { 00405 it = pluginEnvironment.insert(std::make_pair( 00406 pluginTypeName, 00407 boost::shared_ptr<PluginEnvironment>(new typename PluginT::Environment)) 00408 ).first; 00409 } 00410 typename PluginT::Environment* pret = 00411 dynamic_cast<typename PluginT::Environment*>(it->second.get()); 00412 assert(!!pret); 00413 return *pret; 00414 } 00415 00416 00417 template<typename PluginT> 00418 const typename PluginT::Environment& ProgramCtx::getPluginEnvironment() const 00419 { 00420 const std::string pluginTypeName(typeid(PluginT).name()); 00421 PluginEnvironmentContainer::const_iterator it = 00422 pluginEnvironment.find(pluginTypeName); 00423 if( it == pluginEnvironment.end() ) { 00424 throw std::runtime_error("Cannot use getPluginEnvironment const before using not const"); 00425 } 00426 const typename PluginT::Environment* pret = 00427 dynamic_cast<const typename PluginT::Environment*>(it->second.get()); 00428 assert(!!pret); 00429 return *pret; 00430 } 00431 00432 00433 DLVHEX_NAMESPACE_END 00434 #endif /* _DLVHEX_PROGRAMCTX_H */ 00435 00436 00437 00438 // vim:expandtab:ts=4:sw=4: 00439 // mode: C++ 00440 // End: