- Generated on Tue Apr 12 2016 15:51:15 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 00128 #ifdef HAVE_CONFIG_H 00129 #include "config.h" 00130 #endif // HAVE_CONFIG_H 00131 00132 #include "dlvhex2/Error.h" 00133 #include "dlvhex2/Benchmarking.h" 00134 #include "dlvhex2/ProgramCtx.h" 00135 #include "dlvhex2/Registry.h" 00136 #include "dlvhex2/PluginContainer.h" 00137 #include "dlvhex2/ASPSolverManager.h" 00138 #include "dlvhex2/ASPSolver.h" 00139 #include "dlvhex2/AnswerSetPrinterCallback.h" 00140 #include "dlvhex2/State.h" 00141 #include "dlvhex2/EvalGraphBuilder.h" 00142 #include "dlvhex2/EvalHeuristicBase.h" 00143 #include "dlvhex2/EvalHeuristicASP.h" 00144 #include "dlvhex2/EvalHeuristicOldDlvhex.h" 00145 #include "dlvhex2/EvalHeuristicTrivial.h" 00146 #include "dlvhex2/EvalHeuristicEasy.h" 00147 #include "dlvhex2/EvalHeuristicGreedy.h" 00148 #include "dlvhex2/EvalHeuristicMonolithic.h" 00149 #include "dlvhex2/EvalHeuristicFromFile.h" 00150 #include "dlvhex2/ExternalAtomEvaluationHeuristics.h" 00151 #include "dlvhex2/UnfoundedSetCheckHeuristics.h" 00152 #include "dlvhex2/OnlineModelBuilder.h" 00153 #include "dlvhex2/OfflineModelBuilder.h" 00154 00155 // internal plugins 00156 #include "dlvhex2/QueryPlugin.h" 00157 #include "dlvhex2/AggregatePlugin.h" 00158 #include "dlvhex2/ChoicePlugin.h" 00159 #include "dlvhex2/ConditionalLiteralPlugin.h" 00160 #include "dlvhex2/StrongNegationPlugin.h" 00161 #include "dlvhex2/HigherOrderPlugin.h" 00162 #include "dlvhex2/WeakConstraintPlugin.h" 00163 #include "dlvhex2/ManualEvalHeuristicsPlugin.h" 00164 #include "dlvhex2/FunctionPlugin.h" 00165 #ifdef HAVE_PYTHON 00166 #include "dlvhex2/PythonPlugin.h" 00167 #endif 00168 00169 #include <getopt.h> 00170 #include <signal.h> 00171 #include <sys/types.h> 00172 #ifdef WIN32 00173 #include <windows.h> 00174 #undef ERROR // there is a clash with a Windows definition 00175 #elif POSIX 00176 #include <pwd.h> 00177 #else 00178 #error Either POSIX or WIN32 must be defined 00179 #endif 00180 00181 #include <boost/tokenizer.hpp> 00182 #include <boost/foreach.hpp> 00183 #include <boost/lexical_cast.hpp> 00184 00185 #include <iostream> 00186 #include <fstream> 00187 #include <sstream> 00188 #include <cstring> 00189 00190 DLVHEX_NAMESPACE_USE 00191 00195 void 00196 printLogo() 00197 { 00198 std::cout 00199 << "DLVHEX " 00200 #ifdef HAVE_CONFIG_H 00201 << VERSION << " " 00202 #endif // HAVE_CONFIG_H 00203 << "[build " 00204 << __DATE__ 00205 #ifdef __GNUC__ 00206 << " gcc " << __VERSION__ 00207 #endif 00208 << "]" << std::endl 00209 << std::endl; 00210 } 00211 00212 00216 void 00217 printUsage(std::ostream &out, const char* whoAmI, bool full) 00218 { 00219 // 123456789-123456789-123456789-123456789-123456789-123456789-123456789-123456789- 00220 out << "Usage: " << whoAmI 00221 << " [OPTION] FILENAME [FILENAME ...]" << std::endl 00222 << std::endl; 00223 00224 out << " or: " << whoAmI 00225 << " [OPTION] --" << std::endl 00226 << std::endl; 00227 00228 if (!full) { 00229 out << "Specify -h or --help for more detailed usage information." << std::endl 00230 << std::endl; 00231 00232 return; 00233 } 00234 00235 // 00236 // As soos as we have more options, we can introduce sections here! 00237 // 00238 // 123456789-123456789-123456789-123456789-123456789-123456789-123456789-123456789- 00239 out << "Input, Output and Reasoning Options (influence the results):" << std::endl 00240 << " -- Parse from stdin." << std::endl 00241 << " -s, --silent Do not display anything than the actual result." << std::endl 00242 << " -f, --filter=foo[,bar[,...]]" << std::endl 00243 << " Only display instances of the specified predicate(s)." << std::endl 00244 << " --nofacts Do not output EDB facts." << std::endl 00245 << " -n, --number=<num> Limit number of displayed models to <num>, 0 (default) means all." << std::endl 00246 << " -N, --maxint=<num> Set maximum integer (#maxint in the program takes precedence over the parameter)." << std::endl 00247 << " --weaksafety Skip strong safety check." << std::endl 00248 << " --strongsafety Applies traditional strong safety criteria." << std::endl 00249 << " --liberalsafety Uses more liberal safety conditions than strong safety (default)." << std::endl 00250 << " --mlp Use dlvhex+mlp solver (modular nonmonotonic logic programs)." << std::endl 00251 << " --forget Forget previous instantiations that are not involved in current computation (mlp setting)." << std::endl 00252 << " --split Use instantiation splitting techniques." << std::endl 00253 << " --noeval Just parse the program, don't evaluate it (only useful with --verbose)." << std::endl 00254 << " --keepnsprefix Keep specified namespace-prefixes in the result." << std::endl 00255 << " --keepauxpreds Keep auxiliary predicates in answer sets." << std::endl 00256 << " --csvinput=PREDICATE,FILENAME" << std::endl 00257 << " Read from the given file in CSV format and add each line as fact" << std::endl 00258 << " in over the specified predicate (the original line number is added as first argument)." << std::endl 00259 << " --cvsoutput=PREDICATE" << std::endl 00260 << " Print the extension of the specified predicate in CSV format." << std::endl 00261 << " They are sorted by their first argument (should be numeric)." << std::endl 00262 << " Answer Sets are separated by empty lines." << std::endl 00263 << " --waitonmodel Wait for newline from stdin after each model." << std::endl 00264 00265 << std::endl << "Plugin Options:" << std::endl 00266 << " -p, --plugindir=DIR Specify additional directory where to look for plugin" << std::endl 00267 << " libraries (additionally to the installation plugin-dir" << std::endl 00268 << " and $HOME/.dlvhex/plugins). Start with ! to reset the" << std::endl 00269 << " preset plugin paths, e.g., '!:/lib' will use only /lib/." << std::endl 00270 00271 << std::endl << "Performance Tuning Options:" << std::endl 00272 << " --extlearn[=none,iobehavior,monotonicity,functionality,linearity,neg,user,generalize]" << std::endl 00273 << " Learn nogoods from external atom evaluation (only useful with --solver=genuineii or --solver=genuinegi)." << std::endl 00274 << " none : Deactivate external learning" << std::endl 00275 << " iobehavior : Apply generic rules to learn input-output behavior" << std::endl 00276 << " monotonicity : Apply special rules for monotonic and antimonotonic external atoms" << std::endl 00277 << " (only useful with iobehavior)" << std::endl 00278 << " functionality : Apply special rules for functional external atoms" << std::endl 00279 << " linearity : Apply special rules for external atoms which are linear in all(!) predicate parameters" << std::endl 00280 << " neg : Learn negative information" << std::endl 00281 << " user : Apply user-defined rules for nogood learning" << std::endl 00282 << " generalize : Generalize learned ground nogoods to nonground nogoods" << std::endl 00283 << " By default, all options except \"generalize\" are enabled." << std::endl 00284 << " --supportsets Exploits support sets for evaluation." << std::endl 00285 << " --extinlining Inlines external sources (based on support sets)" << std::endl 00286 << " --evalall Evaluate all external atoms in every compatibility check, even if previous external atoms already failed." << std::endl 00287 << " This makes nogood learning more independent of the sequence of external atom checks." << std::endl 00288 << " Only useful with --extlearn." << std::endl 00289 << " --nongroundnogoods" << std::endl 00290 << " Automatically instantiate learned nonground nogoods." << std::endl 00291 << " --flpcheck=[explicit,ufs,ufsm,aufs,aufsm,none]" << std::endl 00292 << " Sets the strategy used to check if a candidate is a subset-minimal model of the reduct." << std::endl 00293 << " explicit : Compute the reduct and compare its models with the candidate" << std::endl 00294 << " ufs : Use unfounded sets for minimality checking" << std::endl 00295 << " ufsm : Use unfounded sets for minimality checking;" << std::endl 00296 << " do not decompose the program for UFS checking" << std::endl 00297 << " aufs (default) : Use unfounded sets for minimality checking by exploiting assumptions" << std::endl 00298 << " aufsm : Use unfounded sets for minimality checking by exploiting assumptions;" << std::endl 00299 << " do not decompose the program for UFS checking" << std::endl 00300 << " none : Disable the check" << std::endl 00301 << " --flpcriterion=[all,head,e,em,emi,none]" << std::endl 00302 << " Defines the kind of cycles whose absence is exploited for skipping minimality checks." << std::endl 00303 << " all (default) : Exploit head- and e-cycles for skipping minimality checks" << std::endl 00304 << " head : Exploit head-cycles for skipping minimality checks" << std::endl 00305 << " e : Exploit e-cycles for skipping minimality checks" << std::endl 00306 << " em : Exploit e-cycles and (anti)monotonicity of predicate parameters for skipping minimality checks" << std::endl 00307 << " emi : Exploit e-cycles, (anti)monotonicity of predicate parameters and current interpretation for skipping minimality checks" << std::endl 00308 << " none : Do not exploit head- or e-cycles for skipping minimality checks" << std::endl 00309 << " --noflpcriterion Do no apply decision criterion to skip the FLP check." << std::endl 00310 << " (equivalent to --flpcriterion=none)" << std::endl 00311 << " --ufslearn=[none,reduct,ufs]" << std::endl 00312 << " Enable learning from UFS checks (only useful with --flpcheck=[a]ufs[m])." << std::endl 00313 << " none : No learning" << std::endl 00314 << " reduct : Learning is based on the FLP-reduct" << std::endl 00315 << " ufs (default) : Learning is based on the unfounded set" << std::endl 00316 << " --eaevalheuristics=[always,periodic,inputcomplete,eacomplete,post,never]" << std::endl 00317 << " Selects the heuristic for external atom evaluation." << std::endl 00318 << " always : Evaluate whenever possible" << std::endl 00319 << " periodic : Evaluate in regular intervals" << std::endl 00320 << " inputcomplete : Evaluate whenever the input to the external atom is complete" << std::endl 00321 << " eacomplete : Evaluate whenever all atoms relevant for the external atom are assigned" << std::endl 00322 << " post (default) : Only evaluate at the end" << std::endl 00323 << " never : Only evaluate at the end and also ignore custom heuristics provided by plugins" << std::endl 00324 << " Except for heuristics \"never\", custom heuristics provided by external atoms overrule the" << std::endl 00325 << " global heuristics for the particular external atom." << std::endl 00326 << " --ngminimization=[always,alwaysopt,onconflict,onconflictopt]" << std::endl 00327 << " Minimize positive and negative nogoods generated by external learning." << std::endl 00328 << " always : Try to minimize every learned nogood" << std::endl 00329 << " alwaysopt : Like always, but use cache for answers of external atom queries" << std::endl 00330 << " onconflict : Only minimize nogoods that are violated by the current assignment" << std::endl 00331 << " onconflictopt : Like onconflict, but use cache for answers of external atom queries" << std::endl 00332 << " --ngminimizationlimit=N" << std::endl 00333 << " Maximum size of nogoods that will be minimized" << std::endl 00334 << " (only useful with ngminimization)" << std::endl 00335 << " --ufscheckheuristic=[post,max,periodic]" << std::endl 00336 << " Specifies the frequency of unfounded set checks (only useful with --flpcheck=[a]ufs[m])." << std::endl 00337 << " post (default) : Do UFS check only over complete interpretations" << std::endl 00338 << " max : Do UFS check as frequent as possible and over maximal subprograms" << std::endl 00339 << " periodic : Do UFS check in periodic intervals" << std::endl 00340 << " --modelqueuesize=N" << std::endl 00341 << " Size of the model queue, i.e. number of models which can be computed in parallel." << std::endl 00342 << " Default value is 5. The option is only useful for clasp solver." << std::endl 00343 << " --solver=S Use S as ASP engine, where S is one of dlv, dlvdb, libdlv, libclingo, genuineii, genuinegi, genuineic, genuinegc" << std::endl 00344 << " (genuineii=(i)nternal grounder and (i)nternal solver; genuinegi=(g)ringo grounder and (i)nternal solver" << std::endl 00345 << " genuineic=(i)nternal grounder and (c)lasp solver; genuinegc=(g)ringo grounder and (c)lasp solver)." << std::endl 00346 << " --claspconfig=C If clasp is used, configure it with C where C is parsed by clasp config parser, or " << std::endl 00347 << " C is one of the predefined strings frumpy, jumpy, handy, crafty, or trendy." << std::endl 00348 << " -e, --heuristics=H Use H as evaluation heuristics, where H is one of" << std::endl 00349 << " old : Old dlvhex behavior" << std::endl 00350 << " trivial : Use component graph as eval graph (much overhead)" << std::endl 00351 << " easy : Simple heuristics, used for LPNMR2011" << std::endl 00352 << " greedy (default) : Heuristics with advantages for external behavior learning" << std::endl 00353 << " monolithic : Put entire program into one unit" << std::endl 00354 << " manual:<file> : Read 'collapse <idxs> share <idxs>' commands from <file>" << std::endl 00355 << " where component indices <idx> are from '--graphviz=comp'" << std::endl 00356 << " asp:<script> : Use asp program <script> as eval heuristic" << std::endl 00357 << " --forcegc Always use the guess and check model generator." << std::endl 00358 << " -m, --modelbuilder=M Use M as model builder, where M is one of (online,offline)." << std::endl 00359 << " --nocache Do not cache queries to and answers from external atoms." << std::endl 00360 << " --iauxinaux Keep auxiliary input predicates in auxiliary external atom predicates (can increase or decrease efficiency)." << std::endl 00361 << " --constspace Free partial models immediately after using them. This may cause some models." << std::endl 00362 << " to be computed multiple times. (Not with monolithic.)" << std::endl 00363 00364 << std::endl << "Debugging and General Options:" << std::endl 00365 << " --dumpevalplan=F Dump evaluation plan (usable as manual heuristics) to file F." << std::endl 00366 << " --dumpeanogoods=F" << std::endl 00367 << " Dump learned EA nogoods to file F." << std::endl 00368 << " -v, --verbose[=N] Specify verbose category (if option is used without [=N] then default is 1):" << std::endl 00369 << " 1 : Program analysis information (including dot-file)" << std::endl 00370 << " 2 : Program modifications by plugins" << std::endl 00371 << " 4 : Intermediate model generation info" << std::endl 00372 << " 8 : Timing information" << std::endl 00373 << " (only if configured with --enable-benchmark)" << std::endl 00374 << " add values for multiple categories." << std::endl 00375 << " --dumpstats Dump certain benchmarking results and statistics in CSV format." << std::endl 00376 << " (Only if configured with --enable-benchmark.)" << std::endl 00377 << " --graphviz=G Specify comma separated list of graph types to export as .dot files." << std::endl 00378 << " Default is none, graph types are:" << std::endl 00379 << " dep : Dependency Graph (once per program)" << std::endl 00380 << " cycinp : Graph for analysis cyclic predicate inputs (once per G&C-eval unit)" << std::endl 00381 << " comp : Component Graph (once per program)" << std::endl 00382 << " eval : Evaluation Graph (once per program)" << std::endl 00383 << " model : Model Graph (once per program, after end of computation)" << std::endl 00384 << " imodel : Individual Model Graph (once per model)" << std::endl 00385 << " attr : Attribute dependency graph (once per program)" << std::endl 00386 << " --version Show version information." << std::endl; 00387 } 00388 00389 00390 void 00391 printVersion() 00392 { 00393 std::cout << PACKAGE_TARNAME << " " << VERSION << std::endl; 00394 00395 std::cout << "Copyright (C) 2005-2015 Roman Schindlauer, Thomas Krennwallner, Peter Sch\303\274ller, Christoph Redl" << std::endl 00396 << "License LGPLv2+: GNU GPL version 2 or later <http://gnu.org/licenses/lgpl.html>" << std::endl 00397 << "This is free software: you are free to change and redistribute it." << std::endl 00398 << "There is NO WARRANTY, to the extent permitted by law." << std::endl; 00399 00400 std::cout << std::endl; 00401 00402 std::cout << "Homepage: http://www.kr.tuwien.ac.at/research/systems/dlvhex/" << std::endl 00403 << "Support: [email protected]" << std::endl 00404 << "Bug reports: http://github.com/hexhex/core/issues/" << std::endl; 00405 00406 exit(0); 00407 } 00408 00409 00413 void 00414 InternalError (const char *msg) 00415 { 00416 std::cerr << std::endl 00417 << "An internal error occurred (" << msg << ")." 00418 << std::endl 00419 << "Please contact <" PACKAGE_BUGREPORT ">." << std::endl; 00420 exit (99); 00421 } 00422 00423 00424 // config and defaults of dlvhex main 00425 struct Config 00426 { 00427 bool optionNoEval; 00428 bool helpRequested; 00429 std::string optionPlugindir; 00430 #if defined(HAVE_DLVDB) 00431 // dlvdb speciality 00432 std::string typFile; 00433 #endif 00434 // those options unhandled by dlvhex main 00435 std::list<const char*> pluginOptions; 00436 00437 Config(): 00438 optionNoEval(false), 00439 helpRequested(false), 00440 optionPlugindir(""), 00441 #if defined(HAVE_DLVDB) 00442 typFile(), 00443 #endif 00444 pluginOptions() {} 00445 }; 00446 00447 void processOptionsPrePlugin(int argc, char** argv, Config& config, ProgramCtx& pctx); 00448 00449 namespace 00450 { 00451 ProgramCtx* exeCtx = NULL; 00452 } 00453 00454 00455 void signal_handler(int signum) 00456 { 00457 // perform benchmarking shutdown to obtain benchmark output 00458 #ifdef WIN32 00459 LOG(ERROR,"dlvhex2 with pid " << GetCurrentProcessId() << " got termination signal" << signum << "!"); 00460 #else 00461 LOG(ERROR,"dlvhex2 with pid " << getpid() << " got termination signal " << signum << "!"); 00462 #endif 00463 00464 benchmark::BenchmarkController::finish(); 00465 00466 // hard exit 00467 // (otherwise ctrl+c does not work for many situations, which is annoying!) 00468 exit(2); 00469 } 00470 00471 00472 int main(int argc, char *argv[]) 00473 { 00474 const char* whoAmI = argv[0]; 00475 00476 // pre-init logger 00477 // (we use more than 4 bits -> two digit loglevel) 00478 Logger::Instance().setPrintLevelWidth(2); 00479 00480 // program context 00481 ProgramCtx pctx; 00482 exeCtx = &pctx; 00483 { 00484 RegistryPtr registry(new Registry); 00485 PluginContainerPtr pcp(new PluginContainer); 00486 pctx.setupRegistry(registry); 00487 pctx.setupPluginContainer(pcp); 00488 } 00489 00490 // default external asp solver to first one that has been configured 00491 #if HAVE_DLV 00492 pctx.setASPSoftware( 00493 ASPSolverManager::SoftwareConfigurationPtr(new ASPSolver::DLVSoftware::Configuration)); 00494 #else 00495 #if HAVE_DLVDB 00496 #error reactivate dlvdb 00497 //pctx.setASPSoftware( 00498 // ASPSolverManager::SoftwareConfigurationPtr(new ASPSolver::DLVDBSoftware::Configuration)); 00499 #else 00500 #if HAVE_LIBDLV 00501 pctx.setASPSoftware( 00502 ASPSolverManager::SoftwareConfigurationPtr(new ASPSolver::DLVLibSoftware::Configuration)); 00503 #else 00504 #if HAVE_LIBCLINGO 00505 pctx.setASPSoftware( 00506 ASPSolverManager::SoftwareConfigurationPtr(new ASPSolver::ClingoSoftware::Configuration)); 00507 #else 00508 #if defined(HAVE_LIBGRINGO) && defined(HAVE_LIBCLASP) 00509 #else 00510 #ifndef WIN32 00511 #error no asp software configured! configure.ac should not allow this to happen! 00512 #endif 00513 #endif 00514 #endif 00515 #endif 00516 #endif 00517 #endif 00518 00519 // default eval heuristic = "greedy" heuristic 00520 pctx.evalHeuristic.reset(new EvalHeuristicGreedy); 00521 // default model builder = "online" model builder 00522 pctx.modelBuilderFactory = boost::factory<OnlineModelBuilder<FinalEvalGraph>*>(); 00523 00524 // defaults of main 00525 Config config; 00526 00527 // if we throw UsageError inside this, error and usage will be displayed, otherwise only error 00528 int returnCode = 1; 00529 try 00530 { 00531 // default logging priority = errors + warnings 00532 Logger::Instance().setPrintLevels(Logger::ERROR | Logger::WARNING); 00533 00534 // manage options we can already manage 00535 // TODO use boost::program_options 00536 processOptionsPrePlugin(argc, argv, config, pctx); 00537 00538 #ifdef HAVE_PYTHON 00539 PythonPlugin* pythonPlugin = new PythonPlugin(); 00540 #endif 00541 00542 // initialize internal plugins 00543 { 00544 PluginInterfacePtr manualEvalHeuristicsPlugin(new ManualEvalHeuristicsPlugin); 00545 pctx.pluginContainer()->addInternalPlugin(manualEvalHeuristicsPlugin); 00546 PluginInterfacePtr queryPlugin(new QueryPlugin); 00547 pctx.pluginContainer()->addInternalPlugin(queryPlugin); 00548 PluginInterfacePtr aggregatePlugin(new AggregatePlugin); 00549 pctx.pluginContainer()->addInternalPlugin(aggregatePlugin); 00550 PluginInterfacePtr strongNegationPlugin(new StrongNegationPlugin); 00551 pctx.pluginContainer()->addInternalPlugin(strongNegationPlugin); 00552 PluginInterfacePtr higherOrderPlugin(new HigherOrderPlugin); 00553 pctx.pluginContainer()->addInternalPlugin(higherOrderPlugin); 00554 PluginInterfacePtr weakConstraintPlugin(new WeakConstraintPlugin); 00555 pctx.pluginContainer()->addInternalPlugin(weakConstraintPlugin); 00556 PluginInterfacePtr functionPlugin(new FunctionPlugin); 00557 pctx.pluginContainer()->addInternalPlugin(functionPlugin); 00558 PluginInterfacePtr choicePlugin(new ChoicePlugin); 00559 pctx.pluginContainer()->addInternalPlugin(choicePlugin); 00560 PluginInterfacePtr conditionalLiteralPlugin(new ConditionalLiteralPlugin); 00561 pctx.pluginContainer()->addInternalPlugin(conditionalLiteralPlugin); 00562 #ifdef HAVE_PYTHON 00563 PluginInterfacePtr _pythonPlugin(pythonPlugin); 00564 pctx.pluginContainer()->addInternalPlugin(_pythonPlugin); 00565 #endif 00566 } 00567 00568 // before anything else we dump the logo 00569 if( !pctx.config.getOption("Silent") ) 00570 printLogo(); 00571 00572 // initialize benchmarking (--verbose=8) with scope exit 00573 // (this cannot be outsourced due to the scope) 00574 benchmark::BenchmarkController& ctr = 00575 benchmark::BenchmarkController::Instance(); 00576 if( pctx.config.doVerbose(dlvhex::Configuration::PROFILING) ) { 00577 LOG(INFO,"initializing benchmarking output"); 00578 ctr.setOutput(&Logger::Instance().stream()); 00579 // for continuous statistics output, display every 1000'th output 00580 ctr.setPrintInterval(999); 00581 } 00582 else 00583 ctr.setOutput(0); 00584 00585 // also deconstruct & output at SIGTERM/SIGINT 00586 { 00587 if( SIG_ERR == signal(SIGTERM, signal_handler) ) 00588 LOG(WARNING,"setting SIGTERM handler terminated with error '" << strerror(errno)); 00589 if( SIG_ERR == signal(SIGINT, signal_handler) ) 00590 LOG(WARNING,"setting SIINT handler terminated with error '" << strerror(errno)); 00591 } 00592 00593 // startup statemachine 00594 pctx.changeState(StatePtr(new ShowPluginsState)); 00595 00596 // load plugins 00597 { 00598 DLVHEX_BENCHMARK_REGISTER_AND_SCOPE(sid,"loading plugins"); 00599 pctx.pluginContainer()->loadPlugins(config.optionPlugindir); 00600 pctx.showPlugins(); 00601 } 00602 00603 // now we may offer help, including plugin help 00604 if( config.helpRequested ) { 00605 printUsage(std::cerr, whoAmI, true); 00606 pctx.pluginContainer()->printUsage(std::cerr); 00607 return 1; 00608 } 00609 00610 // process plugin options using plugins 00611 // (this deletes processed options from config.pluginOptions) 00612 // TODO use boost::program_options 00613 pctx.processPluginOptions(config.pluginOptions); 00614 if( pctx.terminationRequest ) return 1; 00615 00616 // handle options not recognized by dlvhex and not by plugins 00617 if( !config.pluginOptions.empty() ) { 00618 std::stringstream bad; 00619 bad << "Unknown option(s):"; 00620 BOOST_FOREACH(const char* opt, config.pluginOptions) { 00621 bad << " " << opt; 00622 } 00623 throw UsageError(bad.str()); 00624 } 00625 // use configured plugins to obtain plugin atoms 00626 pctx.addPluginAtomsFromPluginContainer(); 00627 00628 // check if this plugin provides a custom model generator 00629 BOOST_FOREACH(PluginInterfacePtr plugin, pctx.pluginContainer()->getPlugins()) { 00630 if (plugin->providesCustomModelGeneratorFactory(pctx)) { 00631 if (pctx.customModelGeneratorProvider == 0) { 00632 LOG(DBG, "Plugin provides custom model generator factory"); 00633 pctx.customModelGeneratorProvider = plugin; 00634 } 00635 else { 00636 throw PluginError("Multiple plugins prove alternative model generator factories. Do not know which one to use. Please change command-line options."); 00637 } 00638 } 00639 } 00640 00641 #ifdef HAVE_PYTHON 00642 if (pctx.config.getOption("HavePythonMain")) { 00643 pythonPlugin->runPythonMain(pctx.config.getStringOption("PythonMain")); 00644 // display benchmark output 00645 benchmark::BenchmarkController::finish(); 00646 return 1; 00647 } 00648 #endif 00649 00650 // now we check if we got input 00651 if( !pctx.inputProvider || !pctx.inputProvider->hasContent() ) 00652 throw UsageError("no input specified!"); 00653 00654 // convert input (only done if at least one plugin provides a converter) 00655 pctx.convert(); 00656 if( pctx.terminationRequest ) return 1; 00657 00658 // parse input (coming directly from inputprovider or from inputprovider provided by the convert() step) 00659 pctx.parse(); 00660 if( pctx.terminationRequest ) return 1; 00661 00662 // check if in mlp mode 00663 if( pctx.config.getOption("MLP") ) { 00664 // syntax check for mlp 00665 pctx.moduleSyntaxCheck(); 00666 if( pctx.terminationRequest ) return 1; 00667 00668 // solve mlp 00669 pctx.mlpSolver(); 00670 if( pctx.terminationRequest ) return 1; 00671 } 00672 00673 else { 00674 00675 // associate PluginAtom instances with 00676 // ExternalAtom instances (in the IDB) 00677 pctx.associateExtAtomsWithPluginAtoms(pctx.idb, true); 00678 if( pctx.terminationRequest ) return 1; 00679 00680 // rewrite program (plugins might want to do this, e.g., for partial grounding) 00681 pctx.rewriteEDBIDB(); 00682 if( pctx.terminationRequest ) return 1; 00683 00684 // associate PluginAtom instances with 00685 // ExternalAtom instances (in the IDB) 00686 // (again, rewrite might add external atoms) 00687 pctx.associateExtAtomsWithPluginAtoms(pctx.idb, true); 00688 00689 // check weak safety 00690 pctx.safetyCheck(); 00691 if( pctx.terminationRequest ) return 1; 00692 00693 // check liberal safety 00694 pctx.liberalSafetyCheck(); 00695 if( pctx.terminationRequest ) return 1; 00696 00697 // create dependency graph (we need the previous step for this) 00698 pctx.createDependencyGraph(); 00699 if( pctx.terminationRequest ) return 1; 00700 00701 // optimize dependency graph (plugins might want to do this, e.g. by using domain information) 00702 pctx.optimizeEDBDependencyGraph(); 00703 if( pctx.terminationRequest ) return 1; 00704 // everything in the following will be done using the dependency graph and EDB 00705 WARNING("IDB and dependencygraph could get out of sync! should we lock or empty the IDB to ensure that it is not directly used anymore after this step?") 00706 00707 // create graph of strongly connected components of dependency graph 00708 pctx.createComponentGraph(); 00709 if( pctx.terminationRequest ) return 1; 00710 00711 // use SCCs to do strong safety check 00712 if( !pctx.config.getOption("SkipStrongSafetyCheck") ) { 00713 pctx.strongSafetyCheck(); 00714 if( pctx.terminationRequest ) return 1; 00715 } 00716 00717 // select heuristics and create eval graph 00718 pctx.createEvalGraph(); 00719 if( pctx.terminationRequest ) return 1; 00720 00721 // stop here if no evaluation was requested 00722 if( config.optionNoEval ) 00723 return 0; 00724 00725 // setup model builder and configure plugin/dlvhex model processing hooks 00726 pctx.setupProgramCtx(); 00727 if( pctx.terminationRequest ) return 1; 00728 00729 // evaluate (generally done in streaming mode, may exit early if indicated by hooks) 00730 // (individual model output should happen here) 00731 pctx.evaluate(); 00732 if( pctx.terminationRequest ) return 1; 00733 00734 } // end if (mlp) else ... 00735 00736 // finalization plugin/dlvhex hooks (for accumulating model processing) 00737 // (accumulated model output/query answering should happen here) 00738 pctx.postProcess(); 00739 00740 // no error 00741 returnCode = 0; 00742 } 00743 catch(const UsageError &ue) { 00744 std::cerr << "UsageError: " << ue.getErrorMsg() << std::endl << std::endl; 00745 printUsage(std::cerr, whoAmI, true); 00746 if( !!pctx.pluginContainer() ) 00747 pctx.pluginContainer()->printUsage(std::cerr); 00748 } 00749 catch(const GeneralError &ge) { 00750 pctx.modelBuilder.reset(); 00751 std::cerr << "GeneralError: " << ge.getErrorMsg() << std::endl << std::endl; 00752 } 00753 catch(const std::exception& e) { 00754 std::cerr << "Exception: " << e.what() << std::endl << std::endl; 00755 } 00756 00757 // display benchmark output 00758 benchmark::BenchmarkController::finish(); 00759 00760 // regular exit 00761 return returnCode; 00762 } 00763 00764 00765 void configurePluginPath(std::string& userPlugindir); 00766 00767 // process whole commandline: 00768 // * recognized arguments are stored into some config 00769 // * non-option arguments are interpreted as input files 00770 // and used to configure config.inputProvider (exception: .typ files) 00771 // * non-recognized option arguments are stored into config.pluginOptions 00772 void processOptionsPrePlugin( 00773 int argc, char** argv, 00774 Config& config, ProgramCtx& pctx) 00775 { 00776 extern char* optarg; 00777 extern int optind; 00778 extern int opterr; 00779 00780 // 00781 // prevent error message for unknown options - they might be known to 00782 // plugins later! 00783 // 00784 opterr = 0; 00785 00786 int ch; 00787 int longid; 00788 00789 static const char* shortopts = "hsvf:p:are:m:n:N:"; 00790 static struct option longopts[] = { 00791 { "help", no_argument, 0, 'h' }, 00792 { "silent", no_argument, 0, 's' }, 00793 { "verbose", optional_argument, 0, 'v' }, 00794 { "filter", required_argument, 0, 'f' }, 00795 { "plugindir", required_argument, 0, 'p' }, 00796 { "reverse", no_argument, 0, 'r' }, 00797 { "heuristics", required_argument, 0, 'e' }, 00798 { "modelbuilder", required_argument, 0, 'm' }, 00799 { "number", required_argument, 0, 'n' }, 00800 { "maxint", required_argument, 0, 'N' }, 00801 { "weaksafety", no_argument, &longid, 2 }, 00802 { "noeval", no_argument, &longid, 5 }, 00803 { "keepnsprefix", no_argument, &longid, 6 }, 00804 { "solver", required_argument, &longid, 7 }, 00805 { "nocache", no_argument, &longid, 8 }, 00806 { "version", no_argument, &longid, 9 }, 00807 { "graphviz", required_argument, &longid, 10 }, 00808 { "keepauxpreds", no_argument, &longid, 11 }, 00809 { "nofacts", no_argument, &longid, 12 }, 00810 { "mlp", no_argument, &longid, 13 }, 00811 { "forget", no_argument, &longid, 15 }, 00812 { "split", no_argument, &longid, 16 }, 00813 { "dumpevalplan", required_argument, &longid, 17 }, 00814 { "extlearn", optional_argument, 0, 18 }, 00815 { "evalall", no_argument, 0, 19 }, 00816 { "flpcheck", required_argument, 0, 20 }, 00817 { "ufslearn", optional_argument, 0, 23 }, 00818 { "noflpcriterion", no_argument, 0, 35 }, 00819 { "flpcriterion", optional_argument, 0, 42 }, 00820 { "eaevalheuristic", required_argument, 0, 26 }, 00821 { // compatibility 00822 "eaevalheuristics", required_argument, 0, 26 00823 }, 00824 { "ufscheckheuristic", required_argument, 0, 27 }, 00825 { // compatibility 00826 "ufscheckheuristics", required_argument, 0, 27 00827 }, 00828 { // perhaps only temporary 00829 "benchmarkeastderr", no_argument, 0, 28 00830 }, 00831 { // perhaps only temporary 00832 "explicitflpunshift", no_argument, 0, 29 00833 }, 00834 { // perhaps only temporary 00835 "printlearnednogoodsstderr", no_argument, 0, 30 00836 }, 00837 { "nongroundnogoods", no_argument, 0, 31 }, 00838 { "modelqueuesize", required_argument, 0, 32 }, 00839 { "liberalsafety", no_argument, 0, 33 }, 00840 { // perhaps only temporary 00841 "claspconfig", required_argument, 0, 36 00842 }, 00843 { "noclaspincremental", no_argument, 0, 43 }, 00844 { "claspsingletonloopnogoods", no_argument, 0, 44 }, 00845 { "claspinverseliterals", no_argument, 0, 45 }, 00846 { "dumpstats", no_argument, 0, 37 }, 00847 { "iauxinaux", optional_argument, 0, 38 }, 00848 { "legacyecycledetection", no_argument, 0, 46 }, 00849 { "constspace", no_argument, 0, 39 }, 00850 { "forcesinglethreading", no_argument, 0, 40 }, 00851 { "lazyufscheckerinitialization", no_argument, 0, 47 }, 00852 { "supportsets", no_argument, 0, 48 }, 00853 { "forcegc", no_argument, 0, 49 }, 00854 { "incremental", no_argument, 0, 50 }, 00855 { "strongsafety", no_argument, 0, 52 }, 00856 { "optmode", required_argument, 0, 54 }, 00857 { "claspdefernprop", required_argument, 0, 55 }, 00858 { "claspdefermsec", required_argument, 0, 56 }, 00859 { "dumpeanogoods", required_argument, 0, 57 }, 00860 { "ngminimization", required_argument, 0, 58 }, 00861 { "ngminimizationlimit", required_argument, 0, 59 }, 00862 { "csvinput", required_argument, 0, 60 }, 00863 { "csvoutput", required_argument, 0, 61 }, 00864 { "noouterexternalatoms", no_argument, 0, 62 }, 00865 { "transunitlearning", no_argument, 0, 64 }, 00866 { "verifyfromlearned", no_argument, 0, 65 }, 00867 { "waitonmodel", no_argument, 0, 66 }, 00868 { "extinlining", no_argument, 0, 67 }, 00869 { NULL, 0, NULL, 0 } 00870 }; 00871 00872 // default settings 00873 pctx.config.setOption("NoPropagator", 0); 00874 pctx.defaultExternalAtomEvaluationHeuristicsFactory.reset(new ExternalAtomEvaluationHeuristicsNeverFactory()); 00875 pctx.unfoundedSetCheckHeuristicsFactory.reset(new UnfoundedSetCheckHeuristicsPostFactory()); 00876 00877 // start with new input provider 00878 pctx.inputProvider.reset(new InputProvider); 00879 00880 bool specifiedModelQueueSize = false; 00881 bool defiaux = false; 00882 bool iaux = false; 00883 bool heuristicChosen = false; 00884 bool heuristicMonolithic = false; 00885 bool solverSet = false; 00886 bool forceoptmode = false; 00887 while ((ch = getopt_long(argc, argv, shortopts, longopts, NULL)) != -1) { 00888 switch (ch) { 00889 case 'h': 00890 config.helpRequested = 1; 00891 break; 00892 00893 case 's': 00894 pctx.config.setOption("Silent", 1); 00895 break; 00896 00897 case 'v': 00898 if (optarg) { 00899 int level = 1; 00900 try 00901 { 00902 level = boost::lexical_cast<int>(optarg); 00903 } 00904 catch(const boost::bad_lexical_cast&) { 00905 LOG(ERROR,"could not parse verbosity level '" << optarg << "' - using default=" << level << "!"); 00906 } 00907 pctx.config.setOption("Verbose", level); 00908 Logger::Instance().setPrintLevels(level); 00909 } 00910 else { 00911 pctx.config.setOption("Verbose", 1); 00912 Logger::Instance().setPrintLevels(Logger::ERROR | Logger::WARNING | Logger::INFO); 00913 } 00914 break; 00915 00916 case 'f': 00917 { 00918 boost::char_separator<char> sep(","); 00919 // g++ 3.3 is unable to pass that at the ctor line below 00920 std::string oa(optarg); 00921 boost::tokenizer<boost::char_separator<char> > tok(oa, sep); 00922 00923 for(boost::tokenizer<boost::char_separator<char> >::const_iterator f = tok.begin(); 00924 f != tok.end(); ++f) 00925 pctx.config.addFilter(*f); 00926 } 00927 break; 00928 00929 case 'p': 00930 config.optionPlugindir = std::string(optarg); 00931 pctx.config.setStringOption("PluginDirs", std::string(optarg)); 00932 break; 00933 00934 case 'r': 00935 pctx.config.setOption("ReverseOrder", 1); 00936 break; 00937 00938 case 'e': 00939 // heuristics={old,trivial,easy,manual:>filename>} 00940 { 00941 heuristicChosen = true; 00942 std::string heuri(optarg); 00943 if( heuri == "old" ) { 00944 pctx.evalHeuristic.reset(new EvalHeuristicOldDlvhex); 00945 } 00946 else if( heuri == "trivial" ) { 00947 pctx.evalHeuristic.reset(new EvalHeuristicTrivial); 00948 } 00949 else if( heuri == "easy" ) { 00950 pctx.evalHeuristic.reset(new EvalHeuristicEasy); 00951 } 00952 else if( heuri == "greedy" ) { 00953 pctx.evalHeuristic.reset(new EvalHeuristicGreedy); 00954 } 00955 else if( heuri == "monolithic" ) { 00956 pctx.evalHeuristic.reset(new EvalHeuristicMonolithic); 00957 heuristicMonolithic = true; 00958 } 00959 else if( heuri.substr(0,7) == "manual:" ) { 00960 pctx.evalHeuristic.reset(new EvalHeuristicFromFile(heuri.substr(7))); 00961 } 00962 else if( heuri.substr(0,4) == "asp:" ) { 00963 pctx.evalHeuristic.reset(new EvalHeuristicASP(heuri.substr(4))); 00964 } 00965 else { 00966 throw UsageError("unknown evaluation heuristic '" + heuri +"' specified!"); 00967 } 00968 LOG(INFO,"selected '" << heuri << "' evaluation heuristics"); 00969 } 00970 break; 00971 00972 case 'm': 00973 // modelbuilder={offline,online} 00974 { 00975 std::string modelbuilder(optarg); 00976 if( modelbuilder == "offline" ) { 00977 pctx.modelBuilderFactory = 00978 boost::factory<OfflineModelBuilder<FinalEvalGraph>*>(); 00979 } 00980 else if( modelbuilder == "online" ) { 00981 pctx.modelBuilderFactory = 00982 boost::factory<OnlineModelBuilder<FinalEvalGraph>*>(); 00983 } 00984 else { 00985 throw UsageError("unknown model builder '" + modelbuilder +"' specified!"); 00986 } 00987 LOG(INFO,"selected '" << modelbuilder << "' model builder"); 00988 } 00989 break; 00990 00991 case 'n': 00992 { 00993 int models = 0; 00994 try 00995 { 00996 if( optarg[0] == '=' ) 00997 models = boost::lexical_cast<unsigned>(&optarg[1]); 00998 else 00999 models = boost::lexical_cast<unsigned>(optarg); 01000 } 01001 catch(const boost::bad_lexical_cast&) { 01002 LOG(ERROR,"could not parse model count '" << optarg << "' - using default=" << models << "!"); 01003 } 01004 pctx.config.setOption("NumberOfModels", models); 01005 } 01006 break; 01007 01008 case 'N': 01009 { 01010 int maxint = 0; 01011 try 01012 { 01013 if( optarg[0] == '=' ) 01014 maxint = boost::lexical_cast<unsigned>(&optarg[1]); 01015 else 01016 maxint = boost::lexical_cast<unsigned>(optarg); 01017 } 01018 catch(const boost::bad_lexical_cast&) { 01019 LOG(ERROR,"could not parse maxint '" << optarg << "' - using default=" << maxint << "!"); 01020 } 01021 pctx.maxint = maxint; 01022 } 01023 break; 01024 01025 case 0: 01026 switch (longid) { 01027 case 2: 01028 pctx.config.setOption("SkipStrongSafetyCheck",1); 01029 break; 01030 01031 //case 3: 01032 // pctx.setOutputBuilder(new RuleMLOutputBuilder); 01033 // XML output makes only sense with silent: 01034 // pctx.config.setOption("Silent", 1); 01035 // break; 01036 01037 //case 4: 01038 // optiondlt = true; 01039 // break; 01040 01041 case 5: 01042 config.optionNoEval = true; 01043 break; 01044 01045 case 6: 01046 pctx.config.setOption("KeepNamespacePrefix",1); 01047 break; 01048 01049 case 7: 01050 { 01051 std::string solver(optarg); 01052 if( solver == "dlv" ) { 01053 #if defined(HAVE_DLV) 01054 pctx.setASPSoftware( 01055 ASPSolverManager::SoftwareConfigurationPtr(new ASPSolver::DLVSoftware::Configuration)); 01056 pctx.config.setOption("GenuineSolver", 0); 01057 #else 01058 throw GeneralError("sorry, no support for solver backend '"+solver+"' compiled into this binary"); 01059 #endif 01060 } 01061 else if( solver == "dlvdb" ) { 01062 #if defined(HAVE_DLVDB) 01063 WARNING("reactivate dlvhdb") 01064 //pctx.setASPSoftware( 01065 // ASPSolverManager::SoftwareConfigurationPtr(new ASPSolver::DLVDBSoftware::Configuration)); 01066 pctx.config.setOption("GenuineSolver", 0); 01067 #else 01068 throw GeneralError("sorry, no support for solver backend '"+solver+"' compiled into this binary"); 01069 #endif 01070 } 01071 else if( solver == "libdlv" ) { 01072 #if defined(HAVE_LIBDLV) 01073 pctx.setASPSoftware( 01074 ASPSolverManager::SoftwareConfigurationPtr(new ASPSolver::DLVLibSoftware::Configuration)); 01075 pctx.config.setOption("GenuineSolver", 0); 01076 #else 01077 throw GeneralError("sorry, no support for solver backend '"+solver+"' compiled into this binary"); 01078 #endif 01079 } 01080 else if( solver == "libclingo" ) { 01081 #if defined(HAVE_LIBCLINGO) 01082 pctx.setASPSoftware( 01083 ASPSolverManager::SoftwareConfigurationPtr(new ASPSolver::ClingoSoftware::Configuration)); 01084 pctx.config.setOption("GenuineSolver", 0); 01085 #else 01086 throw GeneralError("sorry, no support for solver backend '"+solver+"' compiled into this binary"); 01087 #endif 01088 } 01089 else if( solver == "genuineii" ) { 01090 pctx.config.setOption("GenuineSolver", 1); 01091 } 01092 else if( solver == "genuinegi" ) { 01093 #if defined(HAVE_LIBGRINGO) 01094 pctx.config.setOption("GenuineSolver", 2); 01095 #else 01096 throw GeneralError("sorry, no support for solver backend '"+solver+"' compiled into this binary"); 01097 #endif 01098 } 01099 else if( solver == "genuineic" ) { 01100 #if defined(HAVE_LIBCLASP) 01101 pctx.config.setOption("GenuineSolver", 3); 01102 #else 01103 throw GeneralError("sorry, no support for solver backend '"+solver+"' compiled into this binary"); 01104 #endif 01105 } 01106 else if( solver == "genuinegc" ) { 01107 #if defined(HAVE_LIBGRINGO) && defined(HAVE_LIBCLASP) 01108 pctx.config.setOption("GenuineSolver", 4); 01109 #else 01110 throw GeneralError("sorry, no support for solver backend '"+solver+"' compiled into this binary"); 01111 #endif 01112 } 01113 else { 01114 throw UsageError("unknown solver backend '" + solver +"' specified!"); 01115 } 01116 LOG(INFO,"selected '" << solver << "' solver backend"); 01117 solverSet = true; 01118 } 01119 break; 01120 01121 case 8: 01122 pctx.config.setOption("UseExtAtomCache",0); 01123 break; 01124 01125 case 9: 01126 printVersion(); 01127 break; 01128 01129 case 10: 01130 { 01131 boost::char_separator<char> sep(","); 01132 // g++ 3.3 is unable to pass that at the ctor line below 01133 std::string oa(optarg); 01134 boost::tokenizer<boost::char_separator<char> > tok(oa, sep); 01135 01136 for(boost::tokenizer<boost::char_separator<char> >::const_iterator f = tok.begin(); 01137 f != tok.end(); ++f) { 01138 const std::string& token = *f; 01139 if( token == "dep" ) { 01140 pctx.config.setOption("DumpDepGraph",1); 01141 } 01142 else if( token == "cycinp" ) { 01143 pctx.config.setOption("DumpCyclicPredicateInputAnalysisGraph",1); 01144 } 01145 else if( token == "comp" ) { 01146 pctx.config.setOption("DumpCompGraph",1); 01147 } 01148 else if( token == "eval" ) { 01149 pctx.config.setOption("DumpEvalGraph",1); 01150 } 01151 else if( token == "model" ) { 01152 pctx.config.setOption("DumpModelGraph",1); 01153 throw std::runtime_error("DumpModelGraph not implemented!"); 01154 } 01155 else if( token == "imodel" ) { 01156 pctx.config.setOption("DumpIModelGraph",1); 01157 throw std::runtime_error("DumpIModelGraph not implemented!"); 01158 } 01159 else if( token == "attr" ) { 01160 pctx.config.setOption("DumpAttrGraph",1); 01161 } 01162 else 01163 throw UsageError("unknown graphviz graph type '"+token+"'"); 01164 } 01165 } 01166 break; 01167 case 11: 01168 pctx.config.setOption("KeepAuxiliaryPredicates",1); 01169 break; 01170 case 12: 01171 pctx.config.setOption("NoFacts",1); 01172 break; 01173 case 13: 01174 pctx.config.setOption("MLP",1); 01175 break; 01176 // unused case 14: 01177 case 15: 01178 pctx.config.setOption("Forget",1); 01179 break; 01180 case 16: 01181 pctx.config.setOption("Split",1); 01182 break; 01183 case 17: 01184 { 01185 std::string fname(optarg); 01186 pctx.config.setOption("DumpEvaluationPlan",1); 01187 pctx.config.setStringOption("DumpEvaluationPlanFile",fname); 01188 } 01189 break; 01190 } 01191 break; 01192 01193 case 18: 01194 { 01195 // overwrite default settings: assume that nothing is enabled 01196 pctx.config.setOption("ExternalLearningIOBehavior", 0); 01197 pctx.config.setOption("ExternalLearningMonotonicity", 0); 01198 pctx.config.setOption("ExternalLearningFunctionality", 0); 01199 pctx.config.setOption("ExternalLearningLinearity", 0); 01200 pctx.config.setOption("ExternalLearningNeg", 0); 01201 pctx.config.setOption("ExternalLearningUser", 0); 01202 01203 bool noneToken = false; 01204 bool enableToken = false; 01205 if (optarg) { 01206 boost::char_separator<char> sep(","); 01207 // g++ 3.3 is unable to pass that at the ctor line below 01208 std::string oa(optarg); 01209 boost::tokenizer<boost::char_separator<char> > tok(oa, sep); 01210 01211 for(boost::tokenizer<boost::char_separator<char> >::const_iterator f = tok.begin(); 01212 f != tok.end(); ++f) { 01213 const std::string& token = *f; 01214 if (token == "none" ) { 01215 noneToken = true; 01216 } 01217 else if (token == "iobehavior" ) { 01218 pctx.config.setOption("ExternalLearningIOBehavior", 1); 01219 enableToken = true; 01220 } 01221 else if( token == "monotonicity" ) { 01222 pctx.config.setOption("ExternalLearningMonotonicity", 1); 01223 enableToken = true; 01224 } 01225 else if( token == "functionality" ) { 01226 pctx.config.setOption("ExternalLearningFunctionality", 1); 01227 enableToken = true; 01228 } 01229 else if( token == "linearity" ) { 01230 pctx.config.setOption("ExternalLearningLinearity", 1); 01231 enableToken = true; 01232 } 01233 else if( token == "neg" ) { 01234 pctx.config.setOption("ExternalLearningNeg", 1); 01235 enableToken = true; 01236 } 01237 else if( token == "user" ) { 01238 pctx.config.setOption("ExternalLearningUser", 1); 01239 enableToken = true; 01240 } 01241 else if( token == "generalize" ) { 01242 pctx.config.setOption("ExternalLearningGeneralize", 1); 01243 enableToken = true; 01244 } 01245 else { 01246 throw GeneralError("Unknown learning option: \"" + token + "\""); 01247 } 01248 } 01249 } 01250 else { 01251 // by default, turn on all external learning rules 01252 pctx.config.setOption("ExternalLearningIOBehavior", 1); 01253 pctx.config.setOption("ExternalLearningMonotonicity", 1); 01254 pctx.config.setOption("ExternalLearningFunctionality", 1); 01255 pctx.config.setOption("ExternalLearningLinearity", 1); 01256 pctx.config.setOption("ExternalLearningNeg", 1); 01257 pctx.config.setOption("ExternalLearningUser", 1); 01258 //pctx.config.setOption("ExternalLearningGeneralize", 1); // do not activate by default (it is mostly counterproductive) 01259 } 01260 if (noneToken && enableToken) { 01261 throw GeneralError("--extlearn: Value \"none\" cannot be used simultanously with other options"); 01262 } 01263 01264 pctx.config.setOption("ExternalLearning", noneToken ? 0 : 1); 01265 } 01266 01267 LOG(DBG, "External learning: " << pctx.config.getOption("ExternalLearning") << " [iobehavior: " << pctx.config.getOption("ExternalLearningIOBehavior") << " [monotonicity: " << pctx.config.getOption("ExternalLearningMonotonicity") << ", functionlity: " << pctx.config.getOption("ExternalLearningFunctionality") << ", linearity: " << pctx.config.getOption("ExternalLearningLinearity") << ", user-defined: " << pctx.config.getOption("ExternalLearningUser") << "]"); 01268 break; 01269 01270 case 19: 01271 01272 { 01273 pctx.config.setOption("AlwaysEvaluateAllExternalAtoms", 1); 01274 break; 01275 } 01276 01277 case 20: 01278 { 01279 std::string check(optarg); 01280 if( check == "explicit" ) { 01281 pctx.config.setOption("FLPCheck", 1); 01282 pctx.config.setOption("UFSCheck", 0); 01283 }else if( check == "ufs" ) 01284 { 01285 pctx.config.setOption("FLPCheck", 0); 01286 pctx.config.setOption("UFSCheck", 1); 01287 pctx.config.setOption("UFSCheckMonolithic", 0); 01288 pctx.config.setOption("UFSCheckAssumptionBased", 0); 01289 }else if( check == "ufsm" ) 01290 { 01291 pctx.config.setOption("FLPCheck", 0); 01292 pctx.config.setOption("UFSCheck", 1); 01293 pctx.config.setOption("UFSCheckMonolithic", 1); 01294 pctx.config.setOption("UFSCheckAssumptionBased", 0); 01295 01296 }else if( check == "aufs" ) 01297 { 01298 pctx.config.setOption("FLPCheck", 0); 01299 pctx.config.setOption("UFSCheck", 1); 01300 pctx.config.setOption("UFSCheckMonolithic", 0); 01301 pctx.config.setOption("UFSCheckAssumptionBased", 1); 01302 }else if( check == "aufsm" ) 01303 { 01304 pctx.config.setOption("FLPCheck", 0); 01305 pctx.config.setOption("UFSCheck", 1); 01306 pctx.config.setOption("UFSCheckMonolithic", 1); 01307 pctx.config.setOption("UFSCheckAssumptionBased", 1); 01308 }else if( check == "none" ) 01309 { 01310 pctx.config.setOption("FLPCheck", 0); 01311 pctx.config.setOption("UFSCheck", 0); 01312 } 01313 else { 01314 throw GeneralError("Invalid FLP check option: \"" + check + "\""); 01315 } 01316 01317 LOG(INFO,"FLP Check: " << pctx.config.getOption("FLPCheck") << "; UFS Check: " << pctx.config.getOption("UFSCheck")); 01318 } 01319 01320 break; 01321 01322 case 23: 01323 if (!optarg) { 01324 // use UFS-based learning 01325 pctx.config.setOption("UFSLearning", 1); 01326 pctx.config.setOption("UFSLearnStrategy", 2); 01327 } 01328 else { 01329 std::string learn(optarg); 01330 if (learn == "none") { 01331 pctx.config.setOption("UFSLearning", 0); 01332 } 01333 else if (learn == "reduct") { 01334 pctx.config.setOption("UFSLearning", 1); 01335 pctx.config.setOption("UFSLearnStrategy", 1); 01336 } 01337 else if (learn == "ufs") { 01338 pctx.config.setOption("UFSLearning", 1); 01339 pctx.config.setOption("UFSLearnStrategy", 2); 01340 } 01341 else { 01342 throw GeneralError("Unknown UFS Learning option: \"" + learn + "\""); 01343 } 01344 } 01345 break; 01346 01347 case 26: 01348 { 01349 std::string heur(optarg); 01350 if (heur == "always") { 01351 pctx.defaultExternalAtomEvaluationHeuristicsFactory.reset(new ExternalAtomEvaluationHeuristicsAlwaysFactory()); 01352 pctx.config.setOption("NoPropagator", 0); 01353 } 01354 else if (heur == "periodic") { 01355 pctx.defaultExternalAtomEvaluationHeuristicsFactory.reset(new ExternalAtomEvaluationHeuristicsPeriodicFactory()); 01356 pctx.config.setOption("NoPropagator", 0); 01357 } 01358 else if (heur == "inputcomplete") { 01359 pctx.defaultExternalAtomEvaluationHeuristicsFactory.reset(new ExternalAtomEvaluationHeuristicsInputCompleteFactory()); 01360 pctx.config.setOption("NoPropagator", 0); 01361 } 01362 else if (heur == "eacomplete") { 01363 pctx.defaultExternalAtomEvaluationHeuristicsFactory.reset(new ExternalAtomEvaluationHeuristicsEACompleteFactory()); 01364 pctx.config.setOption("NoPropagator", 0); 01365 } 01366 else if (heur == "post") { 01367 // here we evaluate only after the model candidate has been completed 01368 pctx.defaultExternalAtomEvaluationHeuristicsFactory.reset(new ExternalAtomEvaluationHeuristicsNeverFactory()); 01369 pctx.config.setOption("NoPropagator", 0); 01370 } 01371 else if (heur == "never") { 01372 // here we evaluate only after the model candidate has been completed 01373 // differently from post, even the propagator is diabled, thus also custom heuristics provided by external atoms cannot overwrite this behavior 01374 pctx.defaultExternalAtomEvaluationHeuristicsFactory.reset(new ExternalAtomEvaluationHeuristicsNeverFactory()); 01375 pctx.config.setOption("NoPropagator", 1); 01376 } 01377 else { 01378 throw GeneralError(std::string("Unknown external atom evaluation heuristic: \"") + heur + std::string("\"")); 01379 } 01380 } 01381 break; 01382 01383 case 27: 01384 { 01385 std::string heur(optarg); 01386 if (heur == "post") { 01387 pctx.unfoundedSetCheckHeuristicsFactory.reset(new UnfoundedSetCheckHeuristicsPostFactory()); 01388 pctx.config.setOption("UFSCheckHeuristics", 0); 01389 } 01390 else if (heur == "max") { 01391 pctx.unfoundedSetCheckHeuristicsFactory.reset(new UnfoundedSetCheckHeuristicsMaxFactory()); 01392 pctx.config.setOption("UFSCheckHeuristics", 1); 01393 } 01394 else if (heur == "periodic") { 01395 pctx.unfoundedSetCheckHeuristicsFactory.reset(new UnfoundedSetCheckHeuristicsPeriodicFactory()); 01396 pctx.config.setOption("UFSCheckHeuristics", 2); 01397 } 01398 else { 01399 throw GeneralError(std::string("Unknown UFS check heuristic: \"") + heur + std::string("\"")); 01400 } 01401 } 01402 break; 01403 01404 case 28: pctx.config.setOption("BenchmarkEAstderr",1); break; 01405 case 29: pctx.config.setOption("ExplicitFLPUnshift",1); break; 01406 01407 case 30: pctx.config.setOption("PrintLearnedNogoods",1); break; 01408 01409 case 31: pctx.config.setOption("NongroundNogoodInstantiation", 1); break; 01410 01411 case 32: 01412 { 01413 int queuesize = 5; 01414 try 01415 { 01416 if( optarg[0] == '=' ) 01417 queuesize = boost::lexical_cast<unsigned>(&optarg[1]); 01418 else 01419 queuesize = boost::lexical_cast<unsigned>(optarg); 01420 } 01421 catch(const boost::bad_lexical_cast&) { 01422 LOG(ERROR,"could not parse size of model queue '" << optarg << "' - using default=" << queuesize << "!"); 01423 } 01424 if (queuesize < 1) { 01425 throw GeneralError(std::string("Model queue size must be > 0")); 01426 } 01427 pctx.config.setOption("ModelQueueSize", queuesize); break; 01428 specifiedModelQueueSize = true; 01429 } 01430 break; 01431 01432 case 33: 01433 pctx.config.setOption("LiberalSafety", 1); 01434 break; 01435 01436 case 35: 01437 pctx.config.setOption("FLPDecisionCriterionHead", 0); 01438 pctx.config.setOption("FLPDecisionCriterionE", 0); 01439 break; 01440 01441 case 36: pctx.config.setStringOption("ClaspConfiguration",std::string(optarg)); break; 01442 01443 case 37: 01444 pctx.config.setOption("DumpStats",1); 01445 #if !defined(DLVHEX_BENCHMARK) 01446 throw std::runtime_error("you can only use --dumpstats if you configured with --enable-benchmark"); 01447 #endif 01448 break; 01449 01450 case 38: 01451 defiaux = true; 01452 01453 if (!optarg) { 01454 iaux = true; 01455 } 01456 else { 01457 if (std::string(optarg) == "true") iaux = true; 01458 else if (std::string(optarg) == "false") iaux = false; 01459 else throw GeneralError("Unknown option \"" + std::string(optarg) + "\" for iauxinaux"); 01460 } 01461 break; 01462 01463 case 39: 01464 pctx.config.setOption("UseConstantSpace",1); 01465 break; 01466 01467 case '?': 01468 config.pluginOptions.push_back(argv[optind - 1]); 01469 break; 01470 case 40: 01471 pctx.config.setOption("ClaspForceSingleThreaded", 1); 01472 break; 01473 01474 case 42: 01475 if (optarg) { 01476 std::string cycle(optarg); 01477 if (cycle == "all") { 01478 pctx.config.setOption("FLPDecisionCriterionE", 1); 01479 pctx.config.setOption("FLPDecisionCriterionEM", 1); 01480 pctx.config.setOption("FLPDecisionCriterionEMI", 1); 01481 pctx.config.setOption("FLPDecisionCriterionHead", 1); 01482 } 01483 else if (cycle == "head") { 01484 pctx.config.setOption("FLPDecisionCriterionE", 0); 01485 pctx.config.setOption("FLPDecisionCriterionEM", 0); 01486 pctx.config.setOption("FLPDecisionCriterionEMI", 0); 01487 pctx.config.setOption("FLPDecisionCriterionHead", 1); 01488 } 01489 else if (cycle == "e") { 01490 pctx.config.setOption("FLPDecisionCriterionE", 1); 01491 pctx.config.setOption("FLPDecisionCriterionEM", 0); 01492 pctx.config.setOption("FLPDecisionCriterionEMI", 0); 01493 pctx.config.setOption("FLPDecisionCriterionHead", 0); 01494 } 01495 else if (cycle == "em") { 01496 pctx.config.setOption("FLPDecisionCriterionE", 1); 01497 pctx.config.setOption("FLPDecisionCriterionEM", 1); 01498 pctx.config.setOption("FLPDecisionCriterionEMI", 0); 01499 pctx.config.setOption("FLPDecisionCriterionHead", 0); 01500 } 01501 else if (cycle == "emi") { 01502 pctx.config.setOption("FLPDecisionCriterionE", 1); 01503 pctx.config.setOption("FLPDecisionCriterionEM", 1); 01504 pctx.config.setOption("FLPDecisionCriterionEMI", 1); 01505 pctx.config.setOption("FLPDecisionCriterionHead", 0); 01506 } 01507 else if (cycle == "none") { 01508 pctx.config.setOption("FLPDecisionCriterionE", 0); 01509 pctx.config.setOption("FLPDecisionCriterionEM", 0); 01510 pctx.config.setOption("FLPDecisionCriterionEMI", 0); 01511 pctx.config.setOption("FLPDecisionCriterionHead", 0); 01512 } 01513 else { 01514 throw GeneralError(std::string("Unknown cycle type: \"" + cycle + "\"")); 01515 } 01516 } 01517 else { 01518 pctx.config.setOption("FLPDecisionCriterionE", 1); 01519 pctx.config.setOption("FLPDecisionCriterionHead", 1); 01520 } 01521 break; 01522 case 43: 01523 pctx.config.setOption("ClaspIncrementalInterpretationExtraction", 0); 01524 break; 01525 case 44: 01526 pctx.config.setOption("ClaspSingletonLoopNogoods", 0); 01527 break; 01528 case 45: 01529 pctx.config.setOption("ClaspInverseLiterals", 1); 01530 break; 01531 case 46: 01532 pctx.config.setOption("LegacyECycleDetection", 1); 01533 break; 01534 case 47: 01535 pctx.config.setOption("LazyUFSCheckerInitialization", 1); 01536 break; 01537 case 48: 01538 pctx.config.setOption("SupportSets", 1); 01539 pctx.config.setOption("ExternalLearningUser", 1); 01540 pctx.config.setOption("ExternalLearning", 1); 01541 // pctx.config.setOption("ForceGC", 1); 01542 pctx.config.setOption("LiberalSafety", 1); 01543 break; 01544 case 49: 01545 pctx.config.setOption("ForceGC", 1); 01546 pctx.config.setOption("LiberalSafety", 1); 01547 break; 01548 case 50: 01549 pctx.config.setOption("IncrementalGrounding", 1); 01550 break; 01551 case 52: 01552 pctx.config.setOption("LiberalSafety", 0); 01553 break; 01554 case 54: 01555 { 01556 int optmode = 0; 01557 try 01558 { 01559 if( optarg[0] == '=' ) 01560 optmode = boost::lexical_cast<unsigned>(&optarg[1]); 01561 else 01562 optmode = boost::lexical_cast<unsigned>(optarg); 01563 } 01564 catch(const boost::bad_lexical_cast&) { 01565 LOG(ERROR,"could not parse optmode '" << optarg << "' - using default"); 01566 } 01567 pctx.config.setOption("OptimizationTwoStep", optmode); 01568 forceoptmode = true; 01569 } 01570 break; 01571 case 55: 01572 { 01573 int deferval = 0; 01574 try 01575 { 01576 if( optarg[0] == '=' ) 01577 deferval = boost::lexical_cast<unsigned>(&optarg[1]); 01578 else 01579 deferval = boost::lexical_cast<unsigned>(optarg); 01580 } 01581 catch(const boost::bad_lexical_cast&) { 01582 LOG(ERROR,"claspdefernprop '" << optarg << "' does not specify an integer value"); 01583 } 01584 pctx.config.setOption("ClaspDeferNPropagations", deferval); 01585 } 01586 break; 01587 case 56: 01588 { 01589 int deferval = 0; 01590 try 01591 { 01592 if( optarg[0] == '=' ) 01593 deferval = boost::lexical_cast<unsigned>(&optarg[1]); 01594 else 01595 deferval = boost::lexical_cast<unsigned>(optarg); 01596 } 01597 catch(const boost::bad_lexical_cast&) { 01598 LOG(ERROR,"claspdefermsec '" << optarg << "' does not specify an integer value"); 01599 } 01600 pctx.config.setOption("ClaspDeferMaxTMilliseconds", deferval); 01601 } 01602 break; 01603 case 57: 01604 { 01605 pctx.config.setStringOption("DumpEANogoods", optarg); 01606 std::ofstream filev(pctx.config.getStringOption("DumpEANogoods").c_str(), std::ios_base::out); 01607 } 01608 break; 01609 case 58: 01610 { 01611 std::string heur(optarg); 01612 if (heur == "always") { 01613 pctx.config.setOption("MinimizeNogoods", 1); 01614 } 01615 else if (heur == "onconflict") { 01616 pctx.config.setOption("MinimizeNogoods", 1); 01617 pctx.config.setOption("MinimizeNogoodsOnConflict", 1); 01618 } 01619 else if (heur == "alwaysopt") { 01620 pctx.config.setOption("MinimizeNogoods", 1); 01621 pctx.config.setOption("MinimizeNogoodsOpt", 1); 01622 } 01623 else if (heur == "onconflictopt") { 01624 pctx.config.setOption("MinimizeNogoods", 1); 01625 pctx.config.setOption("MinimizeNogoodsOpt", 1); 01626 pctx.config.setOption("MinimizeNogoodsOnConflict", 1); 01627 } 01628 else { 01629 throw GeneralError(std::string("Unknown value for nogood minimization: \"") + heur + std::string("\"")); 01630 } 01631 } 01632 break; 01633 case 59: 01634 { 01635 int minval = 0; 01636 try 01637 { 01638 if( optarg[0] == '=' ) 01639 minval = boost::lexical_cast<unsigned>(&optarg[1]); 01640 else 01641 minval = boost::lexical_cast<unsigned>(optarg); 01642 } 01643 catch(const boost::bad_lexical_cast&) { 01644 LOG(ERROR,"minimizesize '" << optarg << "' does not specify an integer value"); 01645 } 01646 pctx.config.setOption("MinimizationSize", minval); 01647 } 01648 break; 01649 case 60: 01650 { 01651 std::string arg(optarg); 01652 if (arg.find(',', 0) == std::string::npos) throw GeneralError(std::string("Argument of \"--csvinput\" must be of type \"PREDICATE,FILENAME\"")); 01653 std::string pred = arg.substr(0, arg.find(',', 0)); 01654 std::string filename = arg.substr(arg.find(',', 0) + 1); 01655 pctx.inputProvider->addCSVFileInput(pred, filename); 01656 } 01657 break; 01658 case 61: 01659 { 01660 std::string pred(optarg); 01661 pctx.modelCallbacks.push_back(ModelCallbackPtr(new CSVAnswerSetPrinterCallback(pctx, pred))); 01662 } 01663 break; 01664 case 62: 01665 { 01666 pctx.config.setOption("NoOuterExternalAtoms", 1); 01667 } 01668 break; 01669 case 64: 01670 { 01671 pctx.config.setOption("UnitInconsistencyAnalysis", 1); 01672 pctx.config.setOption("TransUnitLearning", 1); 01673 pctx.config.setOption("ForceGC", 1); 01674 pctx.config.setOption("LiberalSafety", 1); 01675 pctx.config.setOption("NoOuterExternalAtoms", 1); 01676 } 01677 break; 01678 case 65: 01679 { 01680 pctx.config.setOption("ExternalAtomVerificationFromLearnedNogoods", 1); 01681 } 01682 break; 01683 case 66: 01684 { 01685 pctx.config.setOption("WaitOnModel", 1); 01686 } 01687 break; 01688 case 67: 01689 { 01690 pctx.config.setOption("SupportSets", 1); 01691 pctx.config.setOption("ExternalSourceInlining", 1); 01692 } 01693 } 01694 } 01695 01696 // global constraints 01697 if (pctx.config.getOption("UFSCheck") && !pctx.config.getOption("GenuineSolver")) { 01698 // if solver was not set by user, disable it silently, otherwise print a warning 01699 if (!solverSet) { 01700 DBGLOG(WARNING, "Unfounded Set Check is only supported for genuine solvers; will behave like flpcheck=explicit"); 01701 } 01702 else { 01703 LOG(WARNING, "Unfounded Set Check is only supported for genuine solvers; will behave like flpcheck=explicit"); 01704 } 01705 pctx.config.setOption("FLPCheck", 1); 01706 pctx.config.setOption("UFSCheck", 0); 01707 } 01708 if (pctx.config.getOption("LiberalSafety") && !pctx.config.getOption("GenuineSolver")) { 01709 // if solver was not set by user, disable it silently, otherwise print a warning 01710 if (!solverSet) { 01711 DBGLOG(WARNING, "Liberal safety is only supported for genuine solvers, will disable it"); 01712 } 01713 else { 01714 LOG(WARNING, "Liberal safety is only supported for genuine solvers, will disable it"); 01715 } 01716 pctx.config.setOption("LiberalSafety", 0); 01717 } 01718 if (specifiedModelQueueSize && pctx.config.getOption("GenuineSolver") <= 2) { 01719 LOG(WARNING, "Model caching (modelqueuesize) is only compatible with clasp backend"); 01720 } 01721 if (pctx.config.getOption("GenuineSolver") || pctx.config.getOption("LiberalSafety") || heuristicMonolithic) { 01722 pctx.config.setOption("IncludeAuxInputInAuxiliaries", 1); 01723 } 01724 if (defiaux) { 01725 pctx.config.setOption("IncludeAuxInputInAuxiliaries", iaux); 01726 } 01727 if (!pctx.config.getOption("GenuineSolver") && pctx.config.getOption("ExternalLearning")) { 01728 // if solver was not set by user, disable it silently, otherwise print a warning 01729 if (!solverSet) { 01730 DBGLOG(WARNING, "Cannot use external learning with non-genuine solver, will disable it"); 01731 } 01732 else { 01733 LOG(WARNING, "Cannot use external learning with non-genuine solver, will disable it"); 01734 } 01735 pctx.config.setOption("ExternalLearning", 0); 01736 01737 } 01738 bool usingClaspBackend = (pctx.config.getOption("GenuineSolver") == 3 || pctx.config.getOption("GenuineSolver") == 4); 01739 if( !forceoptmode && heuristicMonolithic && usingClaspBackend ) { 01740 // we can use this in a safe way if we use a monolithic evaluation unit 01741 // we can use this with the clasp backend (the other solver does not honor setOptimum() calls) 01742 // TODO we can also use this if we have all weight constraints in one evaluation unit, this can be detected automatically 01743 pctx.config.setOption("OptimizationTwoStep", 1); 01744 } 01745 // We cannot use strong safety if we treat all outer external atoms as inner ones. 01746 // We support two types of safety (strong and liberal) and two grounding approaches (decomposition-based and fixpoint-based). The two dimensions are related as follows: 01747 // - decomposition-based grounding is made for strong safety (it cannot handle liberally safe programs) 01748 // - fixpoint-based grounding is made for liberal safety (but can also handle strongly safe programs which are a special case of liberally safe ones) 01749 // Currently there are no separate options for the two dimensions: --strongsafety and --liberalsafety switch both the safety concept and the grounding approach (fixpoint-based with --liberalsafety and decomposition-based for --strongsafety). 01750 // Treating outer external atoms as inner ones does not destroy strong safety (because the structure of the program does not change) but destroys correctness of the decomposition-based grounder even for strongly safe programs, 01751 // while the fixpoint-based grounding approach is still correct (both for strongly and for liberally safe programs). 01752 // Thus, we can only handle outer external atoms as inner ones if --liberalsafety is used since then also the fixpoint-based grounding approach is used 01753 // (in principle, switching only the grounding approach to fixpoint-based but still using strong safety is possible but not implemented). 01754 if (!pctx.config.getOption("LiberalSafety") && pctx.config.getOption("NoOuterExternalAtoms")){ 01755 throw GeneralError("Option --noouterexternalatoms can only be used with --liberalsafety"); 01756 } 01757 01758 // configure plugin path 01759 configurePluginPath(config.optionPlugindir); 01760 01761 // check input files (stdin, file, or URI) 01762 01763 // stdin requested, append it first 01764 if( std::string(argv[optind - 1]) == "--" ) 01765 pctx.inputProvider->addStreamInput(std::cin, "<stdin>"); 01766 01767 // collect further filenames/URIs 01768 // if we use dlvdb, manage .typ files 01769 for (int i = optind; i < argc; ++i) { 01770 std::string arg(argv[i]); 01771 if( arg.size() > 4 && arg.substr(arg.size()-4) == ".typ" ) { 01772 #if defined(HAVE_DLVDB) 01773 boost::shared_ptr<ASPSolver::DLVDBSoftware::Configuration> ptr = 01774 boost::dynamic_pointer_cast<ASPSolver::DLVDBSoftware::Configuration>(pctx.getASPSoftware()); 01775 if( ptr == 0 ) 01776 throw GeneralError(".typ files can only be used if dlvdb backend is used"); 01777 01778 if( !ptr->options.typFile.empty() ) 01779 throw GeneralError("cannot use more than one .typ file with dlvdb"); 01780 01781 ptr->options.typFile = arg; 01782 #endif 01783 } 01784 #ifdef HAEV_LIBCURL 01785 else if( arg.find("http://") == 0 ) { 01786 pctx.inputProvider->addURLInput(arg); 01787 } 01788 #endif 01789 else { 01790 pctx.inputProvider->addFileInput(arg); 01791 } 01792 } 01793 } 01794 01795 01796 void configurePluginPath(std::string& userPlugindir) 01797 { 01798 #ifdef WIN32 01799 bool reset = false; 01800 if( !userPlugindir.empty() && userPlugindir[0] == '!' ) { 01801 reset = true; 01802 if( userPlugindir.size() > 2 && userPlugindir[1] == ';' ) 01803 userPlugindir.erase(0,2); 01804 else 01805 userPlugindir.erase(0,1); 01806 } 01807 01808 std::stringstream searchpath; 01809 01810 if( !userPlugindir.empty() ) 01811 searchpath << userPlugindir << ';'; 01812 01813 #ifdef LOCAL_PLUGIN_DIR 01814 reset = true; 01815 searchpath << LOCAL_PLUGIN_DIR << ';'; 01816 #endif 01817 01818 if( !reset ) { 01819 // add LD_LIBRARY_PATH 01820 const char *envld = ::getenv("LD_LIBRARY_PATH"); 01821 if( envld ) { 01822 searchpath << envld << ";"; 01823 } 01824 01825 #ifdef USER_PLUGIN_DIR 01826 const char* homedir = ::getenv("USERPROFILE"); 01827 if (!!homedir) searchpath << homedir << "/" USER_PLUGIN_DIR << ';'; 01828 #endif 01829 #ifdef SYS_PLUGIN_DIR 01830 searchpath << SYS_PLUGIN_DIR; 01831 #endif 01832 } 01833 userPlugindir = searchpath.str(); 01834 #elif POSIX 01835 bool reset = false; 01836 if( !userPlugindir.empty() && userPlugindir[0] == '!' ) { 01837 reset = true; 01838 if( userPlugindir.size() > 2 && userPlugindir[1] == ':' ) 01839 userPlugindir.erase(0,2); 01840 else 01841 userPlugindir.erase(0,1); 01842 } 01843 01844 std::stringstream searchpath; 01845 01846 if( !userPlugindir.empty() ) 01847 searchpath << userPlugindir << ':'; 01848 01849 #ifdef LOCAL_PLUGIN_DIR 01850 reset = true; 01851 searchpath << LOCAL_PLUGIN_DIR << ':'; 01852 #endif 01853 01854 if( !reset ) { 01855 // add LD_LIBRARY_PATH 01856 const char *envld = ::getenv("LD_LIBRARY_PATH"); 01857 if( envld ) { 01858 searchpath << envld << ":"; 01859 } 01860 01861 const char* homedir = ::getpwuid(::geteuid())->pw_dir; 01862 searchpath << homedir << "/" USER_PLUGIN_DIR << ':' << SYS_PLUGIN_DIR; 01863 } 01864 userPlugindir = searchpath.str(); 01865 #else 01866 #error Either POSIX or WIN32 must be defined 01867 #endif 01868 } 01869 01870 01871 // vim:expandtab:ts=4:sw=4: 01872 // mode: C++ 01873 // End: 01874
1.7.6.1