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 #ifdef HAVE_CONFIG_H 00036 # include "config.h" 00037 #endif 00038 00039 #ifdef HAVE_DLV 00040 00041 #include "dlvhex2/ASPSolver.h" 00042 #include "dlvhex2/PlatformDefinitions.h" 00043 #include "dlvhex2/Benchmarking.h" 00044 #include "dlvhex2/DLVProcess.h" 00045 #include "dlvhex2/DLVresultParserDriver.h" 00046 #include "dlvhex2/Printer.h" 00047 #include "dlvhex2/Registry.h" 00048 #include "dlvhex2/ProgramCtx.h" 00049 #include "dlvhex2/AnswerSet.h" 00050 00051 #include <boost/thread.hpp> 00052 #include <boost/shared_ptr.hpp> 00053 #include <boost/foreach.hpp> 00054 #include <list> 00055 00056 DLVHEX_NAMESPACE_BEGIN 00057 00058 namespace 00059 { 00060 00061 struct MaskedResultAdder 00062 { 00063 ConcurrentQueueResults& queue; 00064 InterpretationConstPtr mask; 00065 00066 MaskedResultAdder(ConcurrentQueueResults& queue, InterpretationConstPtr mask): 00067 queue(queue), mask(mask) { 00068 } 00069 00070 void operator()(AnswerSetPtr as) { 00071 if( mask ) 00072 as->interpretation->getStorage() -= mask->getStorage(); 00073 queue.enqueueAnswerset(as); 00074 boost::this_thread::interruption_point(); 00075 } 00076 }; 00077 00078 } // anonymous namespace 00079 00080 00081 namespace ASPSolver 00082 { 00083 00084 // 00085 // DLVSoftware 00086 // 00087 00088 DLVSoftware::Options::Options(): 00089 ASPSolverManager::GenericOptions(), 00090 arguments() { 00091 arguments.push_back("-silent"); 00092 } 00093 00094 DLVSoftware::Options::~Options() { 00095 } 00096 00097 // 00098 // ConcurrentQueueResultsImpl 00099 // 00100 00101 // Delegate::Impl is used to prepare the result 00102 // this object would be destroyed long before the result will be destroyed 00103 // therefore its ownership is passed to the results 00104 struct DLVSoftware::Delegate::ConcurrentQueueResultsImpl: 00105 public ConcurrentQueueResults 00106 { 00107 public: 00108 Options options; 00109 DLVProcess proc; 00110 RegistryPtr reg; 00111 InterpretationConstPtr mask; 00112 bool shouldTerminate; 00113 boost::thread answerSetProcessingThread; 00114 00115 public: 00116 ConcurrentQueueResultsImpl(const Options& options): 00117 ConcurrentQueueResults(), 00118 options(options), 00119 shouldTerminate(false) { 00120 DBGLOG(DBG,"DLVSoftware::Delegate::ConcurrentQueueResultsImpl()" << this); 00121 } 00122 00123 virtual ~ConcurrentQueueResultsImpl() { 00124 DBGLOG(DBG,"DLVSoftware::Delegate::~ConcurrentQueueResultsImpl()" << this); 00125 DBGLOG(DBG,"setting termination bool, emptying queue, and joining thread"); 00126 shouldTerminate = true; 00127 queue->flush(); 00128 DBGLOG(DBG,"joining thread"); 00129 answerSetProcessingThread.join(); 00130 DBGLOG(DBG,"closing (probably killing) process"); 00131 proc.close(true); 00132 DBGLOG(DBG,"done"); 00133 } 00134 00135 void setupProcess() { 00136 proc.setPath(DLVPATH); 00137 if( options.includeFacts ) 00138 proc.addOption("-facts"); 00139 else 00140 proc.addOption("-nofacts"); 00141 BOOST_FOREACH(const std::string& arg, options.arguments) { 00142 proc.addOption(arg); 00143 } 00144 } 00145 00146 void answerSetProcessingThreadFunc(); 00147 00148 void startThread() { 00149 DBGLOG(DBG,"starting dlv answer set processing thread"); 00150 answerSetProcessingThread = boost::thread( 00151 boost::bind( 00152 &ConcurrentQueueResultsImpl::answerSetProcessingThreadFunc, 00153 boost::ref(*this))); 00154 DBGLOG(DBG,"started dlv answer set processing thread"); 00155 } 00156 00157 void closeAndCheck() { 00158 int retcode = proc.close(); 00159 00160 // check for errors 00161 if (retcode == 127) { 00162 throw FatalError("LP solver command `" + proc.path() + "\302\264 not found!"); 00163 } 00164 // other problem 00165 else if (retcode != 0) { 00166 std::stringstream errstr; 00167 00168 errstr << 00169 "LP solver `" << proc.path() << "\302\264 " 00170 "bailed out with exitcode " << retcode << ": " 00171 "re-run dlvhex with `strace -f\302\264."; 00172 00173 throw FatalError(errstr.str()); 00174 } 00175 } 00176 }; 00177 00178 void DLVSoftware::Delegate::ConcurrentQueueResultsImpl::answerSetProcessingThreadFunc() { 00179 WARNING("create multithreaded logger by using thread-local storage for logger indent") 00180 DBGLOG(DBG,"[" << this << "]" " starting dlv answerSetProcessingThreadFunc"); 00181 try 00182 { 00183 // parse results and store them into the queue 00184 00185 // parse result 00186 assert(!!reg); 00187 DLVResultParser parser(reg); 00188 MaskedResultAdder adder(*this, mask); 00189 std::istream& is = proc.getInput(); 00190 do { 00191 // get next input line 00192 DBGLOG(DBG,"[" << this << "]" "getting input from stream"); 00193 std::string input; 00194 std::getline(is, input); 00195 DBGLOG(DBG,"[" << this << "]" "obtained " << input.size() << 00196 " characters from input stream via getline"); 00197 if( input.empty() || is.bad() ) { 00198 DBGLOG(DBG,"[" << this << "]" "leaving loop because got input size " << input.size() << 00199 ", stream bits fail " << is.fail() << ", bad " << is.bad() << ", eof " << is.eof()); 00200 break; 00201 } 00202 00203 // discard weak answer set cost lines 00204 if( 0 == input.compare(0, 22, "Cost ([Weight:Level]):") ) { 00205 DBGLOG(DBG,"[" << this << "]" "discarding weak answer set cost line"); 00206 } 00207 else { 00208 // parse line 00209 DBGLOG(DBG,"[" << this << "]" "parsing"); 00210 //std::cout << this << "DLV MODEL" << std::endl << input << std::endl; 00211 std::istringstream iss(input); 00212 parser.parse(iss, adder); 00213 } 00214 } 00215 while(!shouldTerminate); 00216 DBGLOG(DBG,"[" << this << "]" "after loop " << shouldTerminate); 00217 00218 // do clean shutdown if we were not terminated from outside 00219 if( !shouldTerminate ) { 00220 // closes process and throws on errors 00221 // (all results have been parsed above) 00222 closeAndCheck(); 00223 enqueueEnd(); 00224 } 00225 } 00226 catch(const GeneralError& e) { 00227 int retcode = proc.close(); 00228 std::stringstream s; 00229 s << proc.path() << " (exitcode = " << retcode << "): " << e.getErrorMsg(); 00230 LOG(ERROR, "[" << this << "]" + s.str()); 00231 enqueueException(s.str()); 00232 } 00233 catch(const std::exception& e) { 00234 std::stringstream s; 00235 s << proc.path() + ": " + e.what(); 00236 LOG(ERROR, "[" << this << "]" + s.str()); 00237 enqueueException(s.str()); 00238 } 00239 catch(...) { 00240 std::stringstream s; 00241 s << proc.path() + " other exception"; 00242 LOG(ERROR, "[" << this << "]" + s.str()); 00243 enqueueException(s.str()); 00244 } 00245 DBGLOG(DBG,"[" << this << "]" "exiting answerSetProcessingThreadFunc"); 00246 } 00247 00249 // DLVSoftware::Delegate::Delegate // 00251 DLVSoftware::Delegate::Delegate(const Options& options): 00252 results(new ConcurrentQueueResultsImpl(options)) { 00253 } 00254 00255 DLVSoftware::Delegate::~Delegate() { 00256 } 00257 00258 void 00259 DLVSoftware::Delegate::useInputProviderInput(InputProvider& inp, RegistryPtr reg) { 00260 DLVHEX_BENCHMARK_REGISTER_AND_SCOPE(sid,"DLVSoftw:Delegate:useInputProvInp"); 00261 00262 DLVProcess& proc = results->proc; 00263 results->reg = reg; 00264 assert(results->reg); 00265 WARNING("TODO set results->mask?") 00266 00267 try 00268 { 00269 results->setupProcess(); 00270 // request stdin as last parameter 00271 proc.addOption("--"); 00272 LOG(DBG,"external process was setup with path '" << proc.path() << "'"); 00273 00274 // fork dlv process 00275 proc.spawn(); 00276 00277 std::ostream& programStream = proc.getOutput(); 00278 00279 // copy stream 00280 programStream << inp.getAsStream().rdbuf(); 00281 programStream.flush(); 00282 00283 proc.endoffile(); 00284 00285 // start thread 00286 results->startThread(); 00287 } 00288 catch(const GeneralError& e) { 00289 std::stringstream errstr; 00290 int retcode = results->proc.close(); 00291 errstr << results->proc.path() << " (exitcode = " << retcode << 00292 "): " << e.getErrorMsg(); 00293 throw FatalError(errstr.str()); 00294 } 00295 catch(const std::exception& e) { 00296 throw FatalError(results->proc.path() + ": " + e.what()); 00297 } 00298 } 00299 00300 void 00301 DLVSoftware::Delegate::useASTInput(const OrdinaryASPProgram& program) { 00302 DLVHEX_BENCHMARK_REGISTER_AND_SCOPE(sid,"DLVSoftw:Delegate:useASTInput"); 00303 00304 DLVProcess& proc = results->proc; 00305 results->reg = program.registry; 00306 assert(results->reg); 00307 results->mask = program.mask; 00308 00309 try 00310 { 00311 results->setupProcess(); 00312 // handle maxint 00313 if( program.maxint > 0 ) { 00314 std::ostringstream os; 00315 os << "-N=" << program.maxint; 00316 proc.addOption(os.str()); 00317 } 00318 // request stdin as last parameter 00319 proc.addOption("--"); 00320 LOG(DBG,"external process was setup with path '" << proc.path() << "'"); 00321 00322 // fork dlv process 00323 proc.spawn(); 00324 00325 std::ostream& programStream = proc.getOutput(); 00326 00327 // output program 00328 RawPrinter printer(programStream, program.registry); 00329 00330 if( program.edb != 0 ) { 00331 // print edb interpretation as facts 00332 program.edb->printAsFacts(programStream); 00333 programStream << "\n"; 00334 programStream.flush(); 00335 } 00336 00337 printer.printmany(program.idb, "\n"); 00338 programStream << "\n"; 00339 programStream.flush(); 00340 00341 proc.endoffile(); 00342 00343 #if 0 00344 { 00345 std::ostringstream oss; 00346 RawPrinter printer(oss, program.registry); 00347 if( program.edb != 0 ) { 00348 // print edb interpretation as facts 00349 program.edb->printAsFacts(oss); 00350 } 00351 00352 printer.printmany(program.idb, "\n"); 00353 std::cout << this << "DLV PROGRAM" << std::endl << oss.str() << std::endl; 00354 } 00355 #endif 00356 00357 // start thread 00358 results->startThread(); 00359 } 00360 catch(const GeneralError& e) { 00361 std::stringstream errstr; 00362 int retcode = results->proc.close(); 00363 errstr << results->proc.path() << " (exitcode = " << retcode << 00364 "): " << e.getErrorMsg(); 00365 throw FatalError(errstr.str()); 00366 } 00367 catch(const std::exception& e) { 00368 throw FatalError(results->proc.path() + ": " + e.what()); 00369 } 00370 } 00371 00372 ASPSolverManager::ResultsPtr 00373 DLVSoftware::Delegate::getResults() { 00374 DBGLOG(DBG,"DLVSoftware::Delegate::getResults"); 00375 return results; 00376 } 00377 00378 } // namespace ASPSolver 00379 00380 00381 DLVHEX_NAMESPACE_END 00382 #endif // HAVE_DLV 00383 00384 00385 // vim:expandtab:ts=4:sw=4: 00386 // mode: C++ 00387 // End: