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_FACADE_H_INCLUDED 25 #define CLASP_CLASP_FACADE_H_INCLUDED 26 #ifdef _MSC_VER 27 #pragma once 28 #endif 29 30 #include <clasp/config.h> 31 #include <clasp/program_builder.h> 32 #include <clasp/parser.h> 33 #include <clasp/logic_program.h> 34 #include <clasp/shared_context.h> 35 #include <clasp/enumerator.h> 36 #include <clasp/solver_types.h> 37 #include <clasp/solve_algorithms.h> 38 #if CLASP_HAS_THREADS 39 #include <clasp/mt/parallel_solve.h> 40 namespace Clasp { 41 //! Options for controlling enumeration and solving. 42 struct SolveOptions : Clasp::mt::ParallelSolveOptions, EnumOptions {}; 43 } 44 #else 45 namespace Clasp { 46 struct SolveOptions : Clasp::BasicSolveOptions, EnumOptions {}; 47 } 48 #endif 49 50 /*! 51 * \file 52 * \brief High-level API 53 * 54 * This file provides a facade around the clasp library. 55 * I.e. a simplified interface for (multishot) solving a problem using 56 * some configuration (set of parameters). 57 * \ingroup facade 58 */ 59 namespace Clasp { 60 ///////////////////////////////////////////////////////////////////////////////////////// 61 // Configuration 62 ///////////////////////////////////////////////////////////////////////////////////////// 63 /*! 64 * \defgroup facade Facade 65 * \brief Simplified interface for (multishot) solving. 66 * 67 * @{ 68 */ 69 //! Configuration object for configuring solving via the ClaspFacade. 70 class ClaspConfig : public BasicSatConfig { 71 public: 72 //! Interface for injecting user-provided configurations. 73 class Configurator { 74 public: 75 virtual ~Configurator(); 76 virtual void prepare(SharedContext&); 77 virtual bool applyConfig(Solver& s) = 0; 78 virtual void unfreeze(SharedContext&); 79 }; 80 typedef BasicSatConfig UserConfig; 81 typedef Solver** SolverIt; 82 typedef Asp::LogicProgram::AspOptions AspOptions; 83 ClaspConfig(); 84 ~ClaspConfig(); 85 // Base interface 86 void prepare(SharedContext&); 87 void reset(); 88 Configuration* config(const char*); 89 //! Adds an unfounded set checker to the given solver if necessary. 90 /*! 91 * If asp.suppMod is false and the problem in s is a non-tight asp-problem, 92 * the function adds an unfounded set checker to s. 93 */ 94 bool addPost(Solver& s) const; 95 // own interface testerConfig()96 UserConfig* testerConfig() const { return tester_; } 97 UserConfig* addTesterConfig(); 98 //! Registers c as additional callback for when addPost() is called. 99 /*! 100 * \param c Additional configuration to apply. 101 * \param ownership If Ownership_t::Acquire, ownership of c is transferred to the configuration object. 102 * \param once Whether c should be called once in the first step or also in each subsequent step. 103 */ 104 void addConfigurator(Configurator* c, Ownership_t::Type ownership = Ownership_t::Retain, bool once = true); 105 void unfreeze(SharedContext&); 106 SolveOptions solve; /*!< Options for solve algorithm and enumerator. */ 107 AspOptions asp; /*!< Options for asp preprocessing. */ 108 ParserOptions parse; /*!< Options for input parser. */ 109 private: 110 struct Impl; 111 ClaspConfig(const ClaspConfig&); 112 ClaspConfig& operator=(const ClaspConfig&); 113 UserConfig* tester_; 114 Impl* impl_; 115 }; 116 ///////////////////////////////////////////////////////////////////////////////////////// 117 // ClaspFacade 118 ///////////////////////////////////////////////////////////////////////////////////////// 119 //! Result of a solving step. 120 struct SolveResult { 121 //! Possible solving results. 122 enum Base { 123 UNKNOWN = 0, //!< Satisfiability unknown - a given solve limit was hit. 124 SAT = 1, //!< Problem is satisfiable (a model was found). 125 UNSAT = 2, //!< Problem is unsatisfiable. 126 }; 127 //! Additional flags applicable to a solve result. 128 enum Ext { 129 EXT_EXHAUST = 4, //!< Search space is exhausted. 130 EXT_INTERRUPT= 8, //!< The run was interrupted from outside. 131 }; satSolveResult132 bool sat() const { return *this == SAT; } unsatSolveResult133 bool unsat() const { return *this == UNSAT; } unknownSolveResult134 bool unknown() const { return *this == UNKNOWN; } exhaustedSolveResult135 bool exhausted() const { return (flags & EXT_EXHAUST) != 0; } interruptedSolveResult136 bool interrupted()const { return (flags & EXT_INTERRUPT) != 0; } BaseSolveResult137 operator Base() const { return static_cast<Base>(flags & 3u);} 138 uint8 flags; //!< Set of Base and Ext flags. 139 uint8 signal; //!< Term signal or 0. 140 }; 141 142 //! A bitmask type for representing supported solve modes. 143 struct SolveMode_t { 144 //! Named constants. 145 POTASSCO_ENUM_CONSTANTS(SolveMode_t, 146 Default = 0, /**< Solve synchronously in current thread. */ 147 Async = 1, /**< Solve asynchronously in worker thread. */ 148 Yield = 2, /**< Yield models one by one via handle. */ 149 AsyncYield); 150 friend inline SolveMode_t operator|(SolveMode_t::E x, SolveMode_t::E y) { return SolveMode_t(static_cast<uint32>(x)|static_cast<uint32>(y)); } 151 friend inline SolveMode_t operator|(SolveMode_t x, SolveMode_t::E y) { return SolveMode_t(static_cast<uint32>(x)|static_cast<uint32>(y)); } 152 friend inline SolveMode_t operator|(SolveMode_t::E x, SolveMode_t y) { return SolveMode_t(static_cast<uint32>(x)|static_cast<uint32>(y)); } 153 }; 154 //! Provides a simplified interface to the services of the clasp library. 155 class ClaspFacade : public ModelHandler { 156 struct SolveData; 157 struct SolveStrategy; 158 public: 159 //! A handle to a possibly asynchronously computed SolveResult. 160 class SolveHandle { 161 public: 162 typedef SolveResult Result; 163 typedef const Model* ModelRef; 164 typedef const LitVec* CoreRef; 165 explicit SolveHandle(SolveStrategy*); 166 SolveHandle(const SolveHandle&); 167 ~SolveHandle(); 168 SolveHandle& operator=(SolveHandle temp) { swap(*this, temp); return *this; } swap(SolveHandle & lhs,SolveHandle & rhs)169 friend void swap(SolveHandle& lhs, SolveHandle& rhs) { std::swap(lhs.strat_, rhs.strat_); } 170 /*! 171 * \name Blocking functions 172 * @{ */ 173 //! Waits until a result is ready and returns it. 174 Result get() const; 175 //! Returns an unsat core if get() returned unsat under assumptions. 176 CoreRef unsatCore() const; 177 //! Waits until a result is ready and returns it if it is a model. 178 /*! 179 * \note If the corresponding solve operation was not started with 180 * SolveMode_t::Yield, the function always returns 0. 181 * \note A call to resume() invalidates the returned model and starts 182 * the search for the next model. 183 */ 184 ModelRef model() const; 185 //! Waits until a result is ready. 186 void wait() const; 187 //! Waits for a result but for at most sec seconds. 188 bool waitFor(double sec)const; 189 //! Tries to cancel the active operation. 190 void cancel() const; 191 //! Behaves like resume() followed by return model() != 0. 192 bool next() const; 193 //@} 194 /*! 195 * \name Non-blocking functions 196 * @{ */ 197 //! Tests whether a result is ready. 198 bool ready() const; 199 //! Tests whether the operation was interrupted and if so returns the interruption signal. 200 int interrupted() const; 201 //! Tests whether a result is ready and has a stored exception. 202 bool error() const; 203 //! Tests whether the operation is still active. 204 bool running() const; 205 //! Releases ownership of the active model and schedules search for the next model. 206 void resume() const; 207 //@} 208 private: 209 SolveStrategy* strat_; 210 }; 211 typedef SolveResult Result; 212 typedef Potassco::AbstractStatistics AbstractStatistics; 213 //! Type summarizing one or more solving steps. 214 struct Summary { 215 typedef const ClaspFacade* FacadePtr; 216 void init(ClaspFacade& f); 217 //! Logic program elements added in the current step or 0 if not an asp problem. 218 const Asp::LpStats* lpStep() const; 219 //! Logic program stats or 0 if not an asp problem. 220 const Asp::LpStats* lpStats() const; 221 //! Active problem. ctxSummary222 const SharedContext& ctx() const { return facade->ctx; } 223 /*! 224 * \name Result functions 225 * Solve and enumeration result - not accumulated. 226 * @{ 227 */ satSummary228 bool sat() const { return result.sat(); } unsatSummary229 bool unsat() const { return result.unsat(); } completeSummary230 bool complete() const { return result.exhausted(); } optimumSummary231 bool optimum() const { return costs() && (complete() || model()->opt); } 232 const Model* model() const; 233 const LitVec* unsatCore() const; 234 const char* consequences() const; /**< Cautious/brave reasoning active? */ 235 bool optimize() const; /**< Optimization active? */ 236 const SumVec* costs() const; /**< Models have associated costs? */ 237 uint64 optimal() const; /**< Number of optimal models found. */ 238 bool hasLower() const; 239 SumVec lower() const; 240 //@} 241 //! Visits this summary object. 242 void accept(StatsVisitor& out) const; 243 FacadePtr facade; //!< Facade object of this run. 244 double totalTime; //!< Total wall clock time. 245 double cpuTime; //!< Total cpu time. 246 double solveTime; //!< Wall clock time for solving. 247 double unsatTime; //!< Wall clock time to prove unsat. 248 double satTime; //!< Wall clock time to first model. 249 uint64 numEnum; //!< Total models enumerated. 250 uint64 numOptimal;//!< Optimal models enumerated. 251 uint32 step; //!< Step number (multishot solving). 252 Result result; //!< Result of step. 253 }; 254 ClaspFacade(); 255 ~ClaspFacade(); 256 257 /*! 258 * \name Query functions 259 * Functions for checking the state of this object. 260 * @{ */ 261 //! Returns whether the problem is still valid. ok()262 bool ok() const { return program() ? program()->ok() : ctx.ok(); } 263 //! Returns whether the active step is ready for solving. 264 bool prepared() const; 265 //! Returns whether the active step is currently being solved. 266 bool solving() const; 267 //! Returns whether the active step has been solved, i.e., has a result. 268 bool solved() const; 269 //! Returns whether solving of the active step was interrupted. 270 bool interrupted() const; 271 //! Returns the summary of the active step. summary()272 const Summary& summary() const { return step_; } 273 //! Returns the summary of the active (accu = false) or all steps. 274 const Summary& summary(bool accu) const; 275 //! Returns solving statistics or throws std::logic_error if solving() is true. 276 AbstractStatistics*getStats() const; 277 //! Returns the active configuration. config()278 const ClaspConfig* config() const { return config_;} 279 //! Returns the current solving step (starts at 0). step()280 int step() const { return (int)step_.step;} 281 //! Returns the result of the active step (unknown if run is not yet completed). result()282 Result result() const { return step_.result; } 283 //! Returns the active program or 0 if it was already released. program()284 ProgramBuilder* program() const { return builder_.get(); } 285 //! Returns whether program updates are enabled. 286 bool incremental() const; 287 //! Returns the active enumerator or 0 if there is none. 288 Enumerator* enumerator() const; 289 //@} 290 291 //! Event type used to signal that a new step has started. 292 struct StepStart : Event_t<StepStart> { StepStartStepStart293 explicit StepStart(const ClaspFacade& f) : Event_t<StepStart>(subsystem_facade, verbosity_quiet), facade(&f) {} 294 const ClaspFacade* facade; 295 }; 296 //! Event type used to signal that a solve step has terminated. 297 struct StepReady : Event_t<StepReady> { StepReadyStepReady298 explicit StepReady(const Summary& x) : Event_t<StepReady>(subsystem_facade, verbosity_quiet), summary(&x) {} 299 const Summary* summary; 300 }; 301 302 SharedContext ctx; //!< Context-object used to store problem. 303 304 /*! 305 * \name Start functions 306 * Functions for defining a problem. 307 * Calling one of the start functions discards any previous problem 308 * and emits a StepStart event. 309 * @{ */ 310 //! Starts definition of an ASP-problem. 311 Asp::LogicProgram& startAsp(ClaspConfig& config, bool enableProgramUpdates = false); 312 //! Starts definition of a SAT-problem. 313 SatBuilder& startSat(ClaspConfig& config); 314 //! Starts definition of a PB-problem. 315 PBBuilder& startPB(ClaspConfig& config); 316 //! Starts definition of a problem of type t. 317 ProgramBuilder& start(ClaspConfig& config, ProblemType t); 318 //! Starts definition of a problem given in stream. 319 ProgramBuilder& start(ClaspConfig& config, std::istream& stream); 320 //! Enables support for program updates if supported by the program. 321 /*! 322 * \pre program() != 0 and not prepared(). 323 * \return true if program updates are supported. Otherwise, false. 324 */ 325 bool enableProgramUpdates(); 326 //! Enables support for (asynchronous) solve interrupts. 327 void enableSolveInterrupts(); 328 //! Disables program disposal in non-incremental mode after problem has been prepared for solving. 329 /*! 330 * \pre program() != 0 and not prepared(). 331 */ 332 void keepProgram(); 333 //! Tries to detect the problem type from the given input stream. 334 static ProblemType detectProblemType(std::istream& str); 335 //! Tries to read the next program part from the stream passed to start(). 336 /*! 337 * \return false if nothing was read because the stream is exhausted, solving was interrupted, 338 * or the problem is unconditionally unsat. 339 */ 340 bool read(); 341 342 //@} 343 344 /*! 345 * \name Solve functions 346 * Functions for solving a problem. 347 * @{ */ 348 349 enum EnumMode { enum_volatile, enum_static }; 350 351 //! Finishes the definition of a problem and prepares it for solving. 352 /*! 353 * \pre !solving() 354 * \post prepared() || !ok() 355 * \param m Mode to be used for handling enumeration-related knowledge. 356 * If m is enum_volatile, enumeration knowledge is learnt under an 357 * assumption that is retracted on program update. Otherwise, 358 * no special assumption is used and enumeration-related knowledge 359 * might become unretractable. 360 * \note If solved() is true, prepare() first starts a new solving step. 361 */ 362 void prepare(EnumMode m = enum_volatile); 363 364 //! Solves the current problem. 365 /*! 366 * If prepared() is false, the function first calls prepare() to prepare the problem for solving. 367 * \pre !solving() 368 * \post solved() 369 * \param a A list of unit-assumptions under which solving should operate. 370 * \param eh An optional event handler that is notified on each model and 371 * once the solve operation has completed. 372 */ 373 Result solve(const LitVec& a = LitVec(), EventHandler* eh = 0); solve(EventHandler * eh)374 Result solve(EventHandler* eh) { return solve(LitVec(), eh); } 375 376 //! Solves the current problem using the given solve mode. 377 /*! 378 * If prepared() is false, the function first calls prepare() to prepare the problem for solving. 379 * \pre !solving() 380 * \param mode The solve mode to use. 381 * \param a A list of unit-assumptions under which solving should operate. 382 * \param eh An optional event handler that is notified on each model and 383 * once the solve operation has completed. 384 * \throws std::logic_error if mode contains SolveMode_t::Async but thread support is disabled. 385 * \throws std::runtime_error if mode contains SolveMode_t::Async but solve is unable to start a thread. 386 * 387 * \note If mode contains SolveMode_t::Async, the optional event handler is notified in the 388 * context of the asynchronous thread. 389 * 390 * \note If mode contains SolveMode_t::Yield, models are signaled one by one via the 391 * returned handle object. 392 * It is the caller's responsibility to finish the solve operation, 393 * either by extracting models until SolveHandle::model() returns 0, or 394 * by calling SolveHandle::cancel(). 395 * 396 * To iterate over models one by one use a loop like: 397 * \code 398 * SolveMode_t p = ... 399 * for (auto it = facade.solve(p|SolveMode_t::Yield); it.model(); it.resume()) { 400 * printModel(*it.model()); 401 * } 402 * \endcode 403 */ 404 SolveHandle solve(SolveMode_t mode, const LitVec& a = LitVec(), EventHandler* eh = 0); 405 406 //! Tries to interrupt the active solve operation. 407 /*! 408 * The function sends the given signal to the active solve operation. 409 * If no solve operation is active (i.e. solving() is false), the signal 410 * is queued and applied to the next solve operation. 411 * 412 * \param sig The signal to raise or 0, to re-raises a previously queued signal. 413 * \return false if no operation was interrupted, because 414 * there is no active solve operation, 415 * or the operation does not support interrupts, 416 * or sig was 0 and there was no queued signal. 417 * 418 * \see enableSolveInterrupts() 419 */ 420 bool interrupt(int sig); 421 422 //! Forces termination of the current solving step. 423 /*! 424 * \post solved() 425 * \return summary(true) 426 */ 427 const Summary& shutdown(); 428 429 //! Starts update of the active problem. 430 /*! 431 * \pre solving() is false and program updates are enabled (incremental() is true). 432 * \post !solved() 433 * \param updateConfig If true, the function applies any configuration changes. 434 * \param sigQ An action to be performed for any queued signal. 435 * The default is to apply the signal to the next solve operation, while 436 * SIGN_IGN can be used to discard queued signals. 437 */ 438 ProgramBuilder& update(bool updateConfig, void (*sigQ)(int)); 439 ProgramBuilder& update(bool updateConfig = false); 440 //@} 441 private: 442 struct Statistics; 443 typedef SingleOwnerPtr<ProgramBuilder> BuilderPtr; 444 typedef SingleOwnerPtr<SolveData> SolvePtr; 445 typedef SingleOwnerPtr<Summary> SummaryPtr; 446 typedef SingleOwnerPtr<Statistics> StatsPtr; 447 void init(ClaspConfig& cfg, bool discardProblem); 448 void initBuilder(ProgramBuilder* in); isAsp()449 bool isAsp() const { return program() && type_ == Problem_t::Asp; } 450 void discardProblem(); 451 void startStep(uint32 num); 452 Result stopStep(int signal, bool complete); 453 void updateStats(); 454 bool onModel(const Solver& s, const Model& m); 455 void doUpdate(ProgramBuilder* p, bool updateConfig, void (*sig)(int)); 456 ProblemType type_; 457 Summary step_; 458 LitVec assume_; 459 ClaspConfig* config_; 460 BuilderPtr builder_; 461 SummaryPtr accu_; 462 StatsPtr stats_; // statistics: only if requested 463 SolvePtr solve_; // NOTE: last so that it is destroyed first; 464 }; 465 466 /** 467 * \example example2.cpp 468 * This is an example of how to use the ClaspFacade class for basic solving. 469 * 470 * \example example3.cpp 471 * This is an example of how to use the ClaspFacade class for generator-based solving. 472 */ 473 474 //!@} 475 476 } 477 #endif 478