1 // 2 // Copyright (c) 2006-2017 Benjamin Kaufmann 3 // 4 // This file is part of Clasp. See http://www.cs.uni-potsdam.de/clasp/ 5 // 6 // Permission is hereby granted, free of charge, to any person obtaining a copy 7 // of this software and associated documentation files (the "Software"), to 8 // deal in the Software without restriction, including without limitation the 9 // rights to use, copy, modify, merge, publish, distribute, sublicense, and/or 10 // sell copies of the Software, and to permit persons to whom the Software is 11 // furnished to do so, subject to the following conditions: 12 // 13 // The above copyright notice and this permission notice shall be included in 14 // all copies or substantial portions of the Software. 15 // 16 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 17 // IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 18 // FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 19 // AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 20 // LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING 21 // FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS 22 // IN THE SOFTWARE. 23 // 24 #ifndef CLASP_CLASP_APP_H_INCLUDED 25 #define CLASP_CLASP_APP_H_INCLUDED 26 27 #ifdef _MSC_VER 28 #pragma once 29 #endif 30 #include <potassco/program_opts/typed_value.h> 31 #include <potassco/application.h> 32 #include <clasp/util/timer.h> 33 #include <clasp/cli/clasp_options.h> 34 #include <clasp/cli/clasp_output.h> 35 #include <string> 36 #include <vector> 37 #include <iosfwd> 38 #include <memory> 39 namespace Potassco { class StringBuilder; } 40 namespace Clasp { namespace Cli { 41 ///////////////////////////////////////////////////////////////////////////////////////// 42 // clasp exit codes 43 ///////////////////////////////////////////////////////////////////////////////////////// 44 enum ExitCode { 45 E_UNKNOWN = 0, /*!< Satisfiablity of problem not knwon; search not started. */ 46 E_INTERRUPT = 1, /*!< Run was interrupted. */ 47 E_SAT = 10, /*!< At least one model was found. */ 48 E_EXHAUST = 20, /*!< Search-space was completely examined. */ 49 E_MEMORY = 33, /*!< Run was interrupted by out of memory exception. */ 50 E_ERROR = 65, /*!< Run was interrupted by internal error. */ 51 E_NO_RUN = 128 /*!< Search not started because of syntax or command line error.*/ 52 }; 53 ///////////////////////////////////////////////////////////////////////////////////////// 54 // clasp app helpers 55 ///////////////////////////////////////////////////////////////////////////////////////// 56 class WriteCnf { 57 public: 58 WriteCnf(const std::string& outFile); 59 ~WriteCnf(); 60 void writeHeader(uint32 numVars, uint32 numCons); 61 void write(Var maxVar, const ShortImplicationsGraph& g); 62 void write(ClauseHead* h); 63 void write(Literal unit); 64 void close(); 65 bool unary(Literal, Literal) const; 66 bool binary(Literal, Literal, Literal) const; 67 private: 68 WriteCnf(const WriteCnf&); 69 WriteCnf& operator=(const WriteCnf&); 70 FILE* str_; 71 LitVec lits_; 72 }; 73 class LemmaLogger { 74 public: 75 struct Options { OptionsOptions76 Options() : logMax(UINT32_MAX), lbdMax(UINT32_MAX), domOut(false), logText(false) {} 77 uint32 logMax; // log at most logMax lemmas 78 uint32 lbdMax; // only log lemmas with lbd <= lbdMax 79 bool domOut; // only log lemmas that can be expressed over out variables 80 bool logText; // log lemmas in ground lp format 81 }; 82 LemmaLogger(const std::string& outFile, const Options& opts); 83 ~LemmaLogger(); 84 void startStep(ProgramBuilder& prg, bool inc); 85 void add(const Solver& s, const LitVec& cc, const ConstraintInfo& info); 86 void close(); 87 private: 88 typedef PodVector<uint32>::type Var2Idx; 89 typedef Atomic_t<uint32>::type Counter; 90 LemmaLogger(const LemmaLogger&); 91 LemmaLogger& operator=(const LemmaLogger&); 92 void formatAspif(const LitVec& cc, uint32 lbd, Potassco::StringBuilder& out) const; 93 void formatText(const LitVec& cc, const OutputTable& tab, uint32 lbd, Potassco::StringBuilder& out) const; 94 FILE* str_; 95 Potassco::LitVec solver2asp_; 96 Var2Idx solver2NameIdx_; 97 ProblemType inputType_; 98 Options options_; 99 int step_; 100 Counter logged_; 101 }; 102 ///////////////////////////////////////////////////////////////////////////////////////// 103 // clasp specific application options 104 ///////////////////////////////////////////////////////////////////////////////////////// 105 struct ClaspAppOptions { 106 typedef LemmaLogger::Options LogOptions; 107 ClaspAppOptions(); 108 typedef std::vector<std::string> StringSeq; 109 static bool mappedOpts(ClaspAppOptions*, const std::string&, const std::string&); 110 void initOptions(Potassco::ProgramOptions::OptionContext& root); 111 bool validateOptions(const Potassco::ProgramOptions::ParsedOptions& parsed); 112 StringSeq input; // list of input files - only first used! 113 std::string lemmaLog; // optional file name for writing learnt lemmas 114 std::string lemmaIn; // optional file name for reading learnt lemmas 115 std::string hccOut; // optional file name for writing scc programs 116 std::string outAtom; // optional format string for atoms 117 uint32 outf; // output format 118 int compute; // force literal compute to true 119 LogOptions lemma; // options for lemma logging 120 char ifs; // output field separator 121 bool hideAux; // output aux atoms? 122 uint8 quiet[3]; // configure printing of models, optimization values, and call steps 123 int8 onlyPre; // run preprocessor and exit 124 bool printPort; // print portfolio and exit 125 enum OutputFormat { out_def = 0, out_comp = 1, out_json = 2, out_none = 3 }; 126 }; 127 ///////////////////////////////////////////////////////////////////////////////////////// 128 // clasp application base 129 ///////////////////////////////////////////////////////////////////////////////////////// 130 // Base class for applications using the clasp library. 131 class ClaspAppBase : public Potassco::Application, public Clasp::EventHandler { 132 public: 133 typedef ClaspFacade::Summary RunSummary; 134 typedef Potassco::ProgramOptions::PosOption PosOption; 135 protected: 136 using Potassco::Application::run; 137 ClaspAppBase(); 138 ~ClaspAppBase(); 139 // ------------------------------------------------------------------------------------------- 140 // Functions to be implemented by subclasses 141 virtual ProblemType getProblemType() = 0; 142 virtual void run(ClaspFacade& clasp) = 0; 143 virtual Output* createOutput(ProblemType f); 144 virtual void storeCommandArgs(const Potassco::ProgramOptions::ParsedValues& values); 145 // ------------------------------------------------------------------------------------------- 146 // Helper functions that subclasses might call during run 147 void handleStartOptions(ClaspFacade& clasp); 148 bool handlePostGroundOptions(ProgramBuilder& prg); 149 bool handlePreSolveOptions(ClaspFacade& clasp); 150 // ------------------------------------------------------------------------------------------- 151 // Application functions 152 virtual const int* getSignals() const; getHelpOption()153 virtual HelpOpt getHelpOption() const { return HelpOpt("Print {1=basic|2=more|3=full} help and exit", 3); } getPositional()154 virtual PosOption getPositional() const { return parsePositional; } 155 virtual void initOptions(Potassco::ProgramOptions::OptionContext& root); 156 virtual void validateOptions(const Potassco::ProgramOptions::OptionContext& root, const Potassco::ProgramOptions::ParsedOptions& parsed, const Potassco::ProgramOptions::ParsedValues& values); 157 virtual void setup(); 158 virtual void run(); 159 virtual void shutdown(); 160 virtual bool onSignal(int); 161 virtual void printHelp(const Potassco::ProgramOptions::OptionContext& root); 162 virtual void printVersion(); 163 static bool parsePositional(const std::string& s, std::string& out); 164 // ------------------------------------------------------------------------------------------- 165 // Event handler 166 virtual void onEvent(const Event& ev); 167 virtual bool onModel(const Solver& s, const Model& m); 168 virtual bool onUnsat(const Solver& s, const Model& m); 169 // ------------------------------------------------------------------------------------------- 170 // Status information & output 171 int exitCode(const RunSummary& sol) const; 172 void printTemplate() const; 173 void printDefaultConfigs() const; 174 void printConfig(ConfigKey k) const; 175 void printLibClaspVersion() const; 176 void printLicense() const; 177 std::istream& getStream(bool reopen = false) const; 178 // ------------------------------------------------------------------------------------------- 179 // Functions called in handlePreSolveOptions() 180 void writeNonHcfs(const PrgDepGraph& graph) const; 181 typedef Potassco::ProgramReader LemmaReader; 182 typedef SingleOwnerPtr<Output> OutPtr; 183 typedef SingleOwnerPtr<ClaspFacade> ClaspPtr; 184 typedef SingleOwnerPtr<LemmaLogger> LogPtr; 185 typedef SingleOwnerPtr<LemmaReader> LemmaPtr; 186 ClaspCliConfig claspConfig_; 187 ClaspAppOptions claspAppOpts_; 188 ClaspPtr clasp_; 189 OutPtr out_; 190 LogPtr logger_; 191 LemmaPtr lemmaIn_; 192 unsigned fpuMode_; 193 }; 194 ///////////////////////////////////////////////////////////////////////////////////////// 195 // clasp application 196 ///////////////////////////////////////////////////////////////////////////////////////// 197 // Standalone clasp application. 198 class ClaspApp : public ClaspAppBase { 199 public: 200 ClaspApp(); getName()201 const char* getName() const { return "clasp"; } getVersion()202 const char* getVersion() const { return CLASP_VERSION; } getUsage()203 const char* getUsage() const { 204 return 205 "[number] [options] [file]\n" 206 "Compute at most <number> models (0=all) of the instance given in <file>"; 207 } 208 protected: 209 virtual ProblemType getProblemType(); 210 virtual void run(ClaspFacade& clasp); 211 virtual void printHelp(const Potassco::ProgramOptions::OptionContext& root); 212 private: 213 ClaspApp(const ClaspApp&); 214 ClaspApp& operator=(const ClaspApp&); 215 }; 216 }} 217 #endif 218