Fawkes API  Fawkes Development Version
clingo_access.cpp
1 /***************************************************************************
2  * clingo_access.cpp - Clingo access wrapper for the aspects
3  *
4  * Created: Mon Oct 31 13:41:07 2016
5  * Copyright 2016 Björn Schäpers
6  * 2018 Tim Niemueller [www.niemueller.org]
7  ****************************************************************************/
8 
9 /* This program is free software; you can redistribute it and/or modify
10  * it under the terms of the GNU General Public License as published by
11  * the Free Software Foundation; either version 2 of the License, or
12  * (at your option) any later version. A runtime exception applies to
13  * this software (see LICENSE.GPL_WRE file mentioned below for details).
14  *
15  * This program is distributed in the hope that it will be useful,
16  * but WITHOUT ANY WARRANTY; without even the implied warranty of
17  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
18  * GNU Library General Public License for more details.
19  *
20  * Read the full text in the LICENSE.GPL_WRE file in the doc directory.
21  */
22 
23 #include "clingo_access.h"
24 
25 #include <core/threading/mutex_locker.h>
26 #include <logging/logger.h>
27 
28 #include <algorithm>
29 #include <sstream>
30 #include <thread>
31 
32 namespace fawkes {
33 
34 /** Helper class to incorporate bool into mutex locker with RAII */
36 {
37 public:
38  /** Constructor.
39  * @param mutex mutex to lock
40  * @param associated_bool associated bool value
41  */
42  BoolMutexLocker(Mutex *mutex, bool &associated_bool)
43  : mutex_(mutex), bool_(associated_bool), initial_locked_(associated_bool)
44  {
45  if (!initial_locked_) {
46  mutex_->lock();
47  bool_ = true;
48  }
49  }
50 
51  /** Destructor. */
53  {
54  if (initial_locked_ != bool_) {
55  if (initial_locked_) {
56  relock();
57  } else {
58  unlock();
59  }
60  }
61  }
62 
63  /** Unlock mutex. */
64  void
65  unlock(void)
66  {
67  bool_ = false;
68  mutex_->unlock();
69  }
70 
71  /** Relock mutex after unlock. */
72  void
73  relock(void)
74  {
75  mutex_->lock();
76  bool_ = true;
77  }
78 
79 private:
80  Mutex *const mutex_;
81  bool & bool_;
82  const bool initial_locked_;
83 };
84 
85 /**
86  * @class ClingoAccess
87  * @brief A wrapper around the clingo control, to control the solving process.
88  * This class provides access to the Clingo solver. Callbacks can be used for
89  * automated notification on specific events, such if a model has been found.
90  * It provides a high-level interface to the solver, i.e., to configure, start,
91  * or cancel the solving process. It also supports assigning and releasing
92  * externals.
93  * @author Björn Schäpers
94  *
95  * @property ClingoAccess::logger_
96  * @brief The used logger.
97  *
98  * @property ClingoAccess::log_comp_
99  * @brief The log component.
100  *
101  * @property ClingoAccess::num_threads_
102  * @brief How many threads Clingo should use for solving.
103  *
104  * @property ClingoAccess::thread_mode_splitting_
105  * @brief Wether splitting should be used.
106  *
107  * @fn bool ClingoAccess::assign_external(const Clingo::Symbol& atom, const bool value)
108  * @brief Assign external value.
109  * @param atom external atom
110  * @param value value to assign
111  * @return true if external was assigned, false otherwise.
112  *
113  * @fn bool ClingoAccess::free_external(const Clingo::Symbol& atom)
114  * @brief Release external value.
115  * @param atom external atom
116  * @return true if external was released, false otherwise.
117  */
118 
119 /**
120  * @property ClingoAccess::control_mutex_
121  * @brief The mutex to protect the clingo control.
122  *
123  * @property ClingoAccess::control_is_locked_
124  * @brief Mark if control_mutex_ is locked. (Because we can not ask the
125  * mutex and need this information for blocked solving.)
126  *
127  * @property ClingoAccess::control_
128  * @brief The clingo control.
129  */
130 
131 /**
132  * @property ClingoAccess::model_mutex_
133  * @brief The mutex for the model symbols.
134  *
135  * @property ClingoAccess::model_symbols_
136  * @brief The symbols found in the last model.
137  *
138  * @property ClingoAccess::old_symbols_
139  * @brief The symbols found in the before last model.
140  *
141  * @property ClingoAccess::model_counter_
142  * @brief Counts how many models we have computed for one solving process.
143  */
144 
145 /**
146  * @property ClingoAccess::solving_
147  * @brief Whether the control is in the solving process.
148  *
149  * @property ClingoAccess::callback_mutex_
150  * @brief The mutex to protect the callback vectors.
151  *
152  * @property ClingoAccess::model_callbacks_
153  * @brief The functions to call on a new model.
154  *
155  * @property ClingoAccess::finish_callbacks_
156  * @brief The functions to call, when the solving process finished.
157  *
158  * @property ClingoAccess::ground_callback_
159  * @brief The callback for the grounding.
160  *
161  * @property ClingoAccess::async_handle_
162  * @brief The handle for the async solving.
163  *
164  * @property ClingoAccess::debug_level_
165  * @brief Which debug outputs should be printed.
166  */
167 
168 /**
169  * @brief Extracts the symbols from the new model and calls the registered functions.
170  * @param[in] model The new model.
171  * @return If the solving process should compute more models (if there are any).
172  */
173 bool
174 ClingoAccess::on_model(Clingo::Model &model)
175 {
176  MutexLocker locker1(&model_mutex_);
177  model_symbols_ = model.symbols(
178  debug_level_ >= ASP_DBG_ALL_MODEL_SYMBOLS ? Clingo::ShowType::All : Clingo::ShowType::Shown);
179 
180  if (debug_level_ >= ASP_DBG_TIME) {
181  logger_->log_info(log_comp_.c_str(),
182  "New %smodel found: #%d",
183  model.optimality_proven() ? "optimal " : "",
184  ++model_counter_);
185 
186  if (debug_level_ >= ASP_DBG_MODELS) {
187  /* To save (de-)allocations just move found symbols at the end
188  * of the vector and move the end iterator to the front. After
189  * this everything in [begin, end) is in oldSymbols but not in
190  * symbols. */
191  auto begin = old_symbols_.begin(), end = old_symbols_.end();
192 
193  for (const Clingo::Symbol &symbol : model_symbols_) {
194  auto iter = std::find(begin, end, symbol);
195  if (iter == end) {
196  logger_->log_info(log_comp_.c_str(), "New Symbol: %s", symbol.to_string().c_str());
197  } else {
198  std::swap(*iter, *--end);
199  }
200  }
201 
202  for (; begin != end; ++begin) {
203  logger_->log_info(log_comp_.c_str(), "Symbol removed: %s", begin->to_string().c_str());
204  }
205  }
206  }
207 
208  old_symbols_ = model_symbols_;
209 
210  bool ret = false;
211 
212  MutexLocker locker2(&callback_mutex_);
213  for (const auto &cb : model_callbacks_) {
214  ret |= (*cb)();
215  }
216 
217  return ret;
218 }
219 
220 /**
221  * @brief Calls the callbacks for the end of the solving.
222  * @param[in] result The result of the solving process.
223  */
224 void
225 ClingoAccess::on_finish(Clingo::SolveResult result)
226 {
227  if (debug_level_ >= ASP_DBG_TIME) {
228  logger_->log_info(log_comp_.c_str(), "Solving nearly done.");
229  }
230 
231  BoolMutexLocker locker1(&control_mutex_, control_is_locked_);
232  MutexLocker locker2(&callback_mutex_);
233  for (const auto &cb : finish_callbacks_) {
234  (*cb)(result);
235  }
236 
237  std::thread blocking_thread([this](void) {
238  async_handle_.wait();
239  if (debug_level_ >= ASP_DBG_TIME) {
240  logger_->log_info(log_comp_.c_str(), "Solving done.");
241  }
242  solving_ = false;
243  return;
244  });
245  blocking_thread.detach();
246  return;
247 }
248 
249 /**
250  * @brief Allocates the control object and initializes the logger.
251  */
252 void
253 ClingoAccess::alloc_control()
254 {
255  assert(!control_);
256 
257  /* The arguments to Clingo::Control are given as a Span of const char*, because we need to compose some strings we
258  * save them as std::string, so we have not to take care about memory leaks. The arguments given to Clingo are saved
259  * in another vector, where the c_str() pointers of the strings are saved. */
260 
261  std::vector<std::string> argumentsString;
262  std::vector<const char *> argumentsChar;
263 
264  if (debug_level_ >= ASP_DBG_EVEN_CLINGO) {
265  argumentsChar.push_back("--output-debug=text");
266  }
267 
268  if (num_threads_ != 1) {
269  std::stringstream s("-t ", std::ios_base::ate | std::ios_base::out);
270  s << num_threads_ << "," << (thread_mode_splitting_ ? "split" : "compete");
271  argumentsString.push_back(s.str());
272  argumentsChar.push_back(argumentsString.back().c_str());
273  }
274 
275  control_ = new Clingo::Control(
276  argumentsChar,
277  [this](const Clingo::WarningCode code, char const *msg) {
279  switch (code) {
280  case Clingo::WarningCode::AtomUndefined:
281  case Clingo::WarningCode::OperationUndefined:
282  case Clingo::WarningCode::RuntimeError: level = fawkes::Logger::LL_ERROR; break;
283  case Clingo::WarningCode::Other:
284  case Clingo::WarningCode::VariableUnbounded: level = fawkes::Logger::LL_WARN; break;
285  case Clingo::WarningCode::FileIncluded:
286  case Clingo::WarningCode::GlobalVariable: level = fawkes::Logger::LL_INFO; break;
287  }
288  logger_->log(level, log_comp_.c_str(), msg);
289  return;
290  },
291  100);
292  return;
293 }
294 
295 /** Constructor.
296  * @param[in] logger The used logger.
297  * @param[in] log_component The logging component.
298  */
299 ClingoAccess::ClingoAccess(Logger *logger, const std::string &log_component)
300 : logger_(logger),
301  log_comp_(log_component.empty() ? "Clingo" : log_component),
302  debug_level_(ASP_DBG_NONE),
303  num_threads_(1),
304  thread_mode_splitting_(false),
305  control_is_locked_(false),
306  control_(nullptr),
307  model_mutex_(Mutex::RECURSIVE),
308  solving_(false)
309 {
310  alloc_control();
311 }
312 
313 /** Destructor. */
315 {
316  delete control_;
317 }
318 
319 /**
320  * @brief Registers a callback for the event of a new model. The callback can control with it's return value if the
321  * search for models should continue. If one of the callbacks says yes the search is continued.
322  * @param[in] callback The callback to register.
323  */
324 void
325 ClingoAccess::register_model_callback(std::shared_ptr<std::function<bool(void)>> callback)
326 {
327  MutexLocker locker(&callback_mutex_);
328  model_callbacks_.emplace_back(callback);
329 }
330 
331 /**
332  * @brief Unregisters a callback for the event of a new model.
333  * @param[in] callback The callback to unregister.
334  */
335 void
336 ClingoAccess::unregister_model_callback(std::shared_ptr<std::function<bool(void)>> callback)
337 {
338  MutexLocker locker(&callback_mutex_);
339  model_callbacks_.erase(std::find(model_callbacks_.begin(), model_callbacks_.end(), callback));
340 }
341 
342 /**
343  * @brief Registers a callback for the event of finishing the solving process.
344  * @param[in] callback The callback to register.
345  */
346 void
348  std::shared_ptr<std::function<void(Clingo::SolveResult)>> callback)
349 {
350  MutexLocker locker(&callback_mutex_);
351  finish_callbacks_.emplace_back(callback);
352 }
353 
354 /**
355  * @brief Unregisters a callback for the event of finishing the solving process.
356  * @param[in] callback The callback to unregister.
357  */
358 void
360  std::shared_ptr<std::function<void(Clingo::SolveResult)>> callback)
361 {
362  MutexLocker locker(&callback_mutex_);
363  finish_callbacks_.erase(std::find(finish_callbacks_.begin(), finish_callbacks_.end(), callback));
364 }
365 
366 /**
367  * @brief Sets the ground callback, to implement custom functions.
368  * @param[in, out] callback The callback, will be moved.
369  */
370 void
371 ClingoAccess::set_ground_callback(Clingo::GroundCallback &&callback)
372 {
373  MutexLocker locker(&callback_mutex_);
374  ground_callback_ = std::move(callback);
375 }
376 
377 /** Returns whether the solving process is running.
378  * @return true if currently solving, false otherwise
379  */
380 bool
381 ClingoAccess::solving(void) const noexcept
382 {
383  return solving_;
384 }
385 
386 /**
387  * @brief Starts the solving process, if it isn't already running.
388  * @return If the process is started.
389  */
390 bool
392 {
393  BoolMutexLocker locker(&control_mutex_, control_is_locked_);
394  if (solving_) {
395  return false;
396  }
397  if (debug_level_ >= ASP_DBG_TIME) {
398  logger_->log_info(log_comp_.c_str(), "Start async solving.");
399  }
400 
401  solving_ = true;
402  model_mutex_.lock();
403  model_counter_ = 0;
404  model_mutex_.unlock();
405  async_handle_ = control_->solve(Clingo::SymbolicLiteralSpan{}, this, true, true);
406  return true;
407 }
408 
409 /** Starts the solving process.
410  * If it isn't already running, in a blocking manner, that means it
411  * does not start the computation in an asynchronous way.
412  * @return true, if the process was started
413  */
414 bool
416 {
417  if (solving_) {
418  return false;
419  }
420 
421  BoolMutexLocker locker(&control_mutex_, control_is_locked_);
422  if (debug_level_ >= ASP_DBG_TIME) {
423  logger_->log_info(log_comp_.c_str(), "Start sync solving.");
424  }
425 
426  solving_ = true;
427  model_mutex_.lock();
428  model_counter_ = 0;
429  model_mutex_.unlock();
430  control_->solve(Clingo::SymbolicLiteralSpan{}, this, false, true);
431  return true;
432 }
433 
434 /** Stops the solving process, if it is running.
435  * @return If it was stopped. (Check solving() for actual state!)
436  */
437 bool
439 {
440  BoolMutexLocker locker(&control_mutex_, control_is_locked_);
441  if (!solving_) {
442  return false;
443  }
444 
445  if (debug_level_ >= ASP_DBG_TIME) {
446  logger_->log_info(log_comp_.c_str(), "Cancel solving.");
447  }
448 
449  control_->interrupt();
450  return true;
451 }
452 
453 /** Tries to reset Clingo.
454  * That means deletes the control object and creates a new one.
455  * @return true, if successful
456  */
457 bool
459 {
460  if (solving_) {
461  logger_->log_warn(log_comp_.c_str(),
462  "Could not reset while solving. "
463  "Please try again when the solving is stopped.");
464  cancel_solving();
465  return false;
466  }
467  logger_->log_warn(log_comp_.c_str(), "Resetting Clingo");
468  delete control_;
469  control_ = nullptr;
470  alloc_control();
471  return true;
472 }
473 
474 /** Sets the number of threads Clingo should use.
475  * @param[in] threads The number.
476  * @param[in] thread_mode_splitting Wether splitting should be used.
477  * @warning This will call reset().
478  * @exception Exception If it is called while solving.
479  * @exception Exception If it is called with @c threads < 1.
480  */
481 void
482 ClingoAccess::set_num_threads(const int threads, const bool thread_mode_splitting)
483 {
484  if (solving_) {
485  throw Exception("Tried to set the number of threads while Clingo was solving.");
486  }
487  if (threads < 1) {
488  throw Exception("Tried to set thread count to %d, only values >= 1 are valid.", threads);
489  }
490  logger_->log_info(log_comp_.c_str(),
491  "Change # of threads for solving from %d to %d "
492  "and splitting from %s to %s.",
493  num_threads_,
494  threads,
495  thread_mode_splitting_ ? "true" : "false",
496  thread_mode_splitting ? "true" : "false");
497  num_threads_ = threads;
498  thread_mode_splitting_ = thread_mode_splitting;
499  reset();
500  return;
501 }
502 
503 /** Returns how many threads Clingo should use.
504  * @return number of threads
505  * @see ClingoAccess::num_threads_
506  */
507 int
508 ClingoAccess::num_threads(void) const noexcept
509 {
510  return num_threads_;
511 }
512 
513 /** Get current debug level.
514  * @return current debug level
515  */
518 {
519  return debug_level_.load();
520 }
521 
522 /** Set debug level.
523  * @param log_level new debug level
524  */
525 void
527 {
528  return debug_level_.store(log_level);
529 }
530 
531 /** Returns a copy of the last symbols found.
532  * @return copy of last symbols found
533  */
534 Clingo::SymbolVector
536 {
537  MutexLocker locker(&model_mutex_);
538  return model_symbols_;
539 }
540 
541 /** Loads a file in the solver.
542  * @param[in] path The path of the file.
543  * @return true, if file was loaded
544  */
545 bool
546 ClingoAccess::load_file(const std::string &path)
547 {
548  BoolMutexLocker locker(&control_mutex_, control_is_locked_);
549  if (solving_) {
550  return false;
551  }
552 
553  logger_->log_info(log_comp_.c_str(), "Loading file program file %s.", path.c_str());
554  control_->load(path.c_str());
555  return true;
556 }
557 
558 /** Grounds a program part.
559  * @param[in] parts The parts to ground.
560  * @return true if parts could be grounded
561  */
562 bool
563 ClingoAccess::ground(const Clingo::PartSpan &parts)
564 {
565  if (parts.empty()) {
566  return true;
567  }
568 
569  BoolMutexLocker locker(&control_mutex_, control_is_locked_);
570  if (solving_) {
571  return false;
572  }
573  if (debug_level_ >= ASP_DBG_TIME) {
574  logger_->log_info(log_comp_.c_str(), "Grounding %zu parts:", parts.size());
575  if (debug_level_ >= ASP_DBG_PROGRAMS) {
576  auto i = 0;
577  for (const Clingo::Part &part : parts) {
578  std::string params;
579  bool first = true;
580  for (const auto &param : part.params()) {
581  if (first) {
582  first = false;
583  } else {
584  params += ", ";
585  }
586  params += param.to_string();
587  }
588  logger_->log_info(log_comp_.c_str(), "Part #%d: %s [%s]", ++i, part.name(), params.c_str());
589  }
590  }
591  }
592 
593  control_->ground(parts, ground_callback_);
594 
595  if (debug_level_ >= ASP_DBG_TIME) {
596  logger_->log_info(log_comp_.c_str(), "Grounding done.");
597  }
598  return true;
599 }
600 
601 /** Assigns an external value.
602  * @param[in] atom The atom to assign.
603  * @param[in] value The assigned value.
604  * @return If it could be assigned.
605  */
606 bool
607 ClingoAccess::assign_external(const Clingo::Symbol &atom, const Clingo::TruthValue value)
608 {
609  BoolMutexLocker locker(&control_mutex_, control_is_locked_);
610  if (solving_) {
611  return false;
612  }
613 
614  if (debug_level_ >= ASP_DBG_EXTERNALS) {
615  logger_->log_info(
616  log_comp_.c_str(),
617  "Assigning %s to %s.",
618  [value](void) {
619  const char *ret = "Unknown Value";
620  switch (value) {
621  case Clingo::TruthValue::Free: ret = "Free"; break;
622  case Clingo::TruthValue::True: ret = "True"; break;
623  case Clingo::TruthValue::False: ret = "False"; break;
624  }
625  return ret;
626  }(),
627  atom.to_string().c_str());
628  }
629  control_->assign_external(atom, value);
630  return true;
631 }
632 
633 /** Releases an external value.
634  * @param[in] atom The atom to release.
635  * @return true, if it could be released
636  */
637 bool
638 ClingoAccess::release_external(const Clingo::Symbol &atom)
639 {
640  BoolMutexLocker locker(&control_mutex_, control_is_locked_);
641  if (solving_) {
642  return false;
643  }
644 
645  if (debug_level_ >= ASP_DBG_EXTERNALS) {
646  logger_->log_info(log_comp_.c_str(), "Releasing %s.", atom.to_string().c_str());
647  }
648  control_->release_external(atom);
649  return true;
650 }
651 
652 } // end namespace fawkes
Helper class to incorporate bool into mutex locker with RAII.
void relock(void)
Relock mutex after unlock.
~BoolMutexLocker(void)
Destructor.
void unlock(void)
Unlock mutex.
BoolMutexLocker(Mutex *mutex, bool &associated_bool)
Constructor.
bool cancel_solving(void)
Stops the solving process, if it is running.
Clingo::SymbolVector model_symbols(void) const
Returns a copy of the last symbols found.
int num_threads(void) const noexcept
Returns how many threads Clingo should use.
DebugLevel_t
Debug levels, higher levels include the lower values.
Definition: clingo_access.h:42
@ ASP_DBG_MODELS
Print new models.
Definition: clingo_access.h:47
@ ASP_DBG_ALL_MODEL_SYMBOLS
Ignore '#show' statements and print all symbols of a model.
Definition: clingo_access.h:48
@ ASP_DBG_EVEN_CLINGO
Activates the –output-debug=text option for clingo.
Definition: clingo_access.h:51
@ ASP_DBG_PROGRAMS
Print which programs are grounded.
Definition: clingo_access.h:45
@ ASP_DBG_EXTERNALS
Print assignments and releases of externals.
Definition: clingo_access.h:46
@ ASP_DBG_TIME
Print when starting/finishing grounding/solving for analysis.
Definition: clingo_access.h:44
DebugLevel_t debug_level() const
Get current debug level.
void set_ground_callback(Clingo::GroundCallback &&callback)
Sets the ground callback, to implement custom functions.
bool start_solving(void)
Starts the solving process, if it isn't already running.
bool assign_external(const Clingo::Symbol &atom, const bool value)
Assign external value.
Definition: clingo_access.h:82
void register_finish_callback(std::shared_ptr< std::function< void(Clingo::SolveResult)>> callback)
Registers a callback for the event of finishing the solving process.
void unregister_model_callback(std::shared_ptr< std::function< bool(void)>> callback)
Unregisters a callback for the event of a new model.
ClingoAccess(Logger *logger, const std::string &log_component)
Constructor.
void set_num_threads(const int threads, const bool use_splitting=false)
Sets the number of threads Clingo should use.
bool load_file(const std::string &path)
Loads a file in the solver.
~ClingoAccess(void)
Destructor.
bool reset(void)
Tries to reset Clingo.
bool ground(const Clingo::PartSpan &parts)
Grounds a program part.
bool solving(void) const noexcept
Returns whether the solving process is running.
void set_debug_level(DebugLevel_t log_level)
Set debug level.
void unregister_finish_callback(std::shared_ptr< std::function< void(Clingo::SolveResult)>> callback)
Unregisters a callback for the event of finishing the solving process.
void register_model_callback(std::shared_ptr< std::function< bool(void)>> callback)
Registers a callback for the event of a new model.
bool start_solving_blocking(void)
Starts the solving process.
Base class for exceptions in Fawkes.
Definition: exception.h:36
Interface for logging.
Definition: logger.h:42
virtual void log_warn(const char *component, const char *format,...)=0
Log warning message.
virtual void log(LogLevel level, const char *component, const char *format,...)
Log message of given log level.
Definition: logger.cpp:326
LogLevel
Log level.
Definition: logger.h:51
@ LL_INFO
informational output about normal procedures
Definition: logger.h:53
@ LL_WARN
warning, should be investigated but software still functions, an example is that something was reques...
Definition: logger.h:54
@ LL_NONE
use this to disable log output
Definition: logger.h:60
@ LL_ERROR
error, may be recoverable (software still running) or not (software has to terminate).
Definition: logger.h:57
virtual void log_info(const char *component, const char *format,...)=0
Log informational message.
Mutex locking helper.
Definition: mutex_locker.h:34
Mutex mutual exclusion lock.
Definition: mutex.h:33
void lock()
Lock this mutex.
Definition: mutex.cpp:87
void unlock()
Unlock the mutex.
Definition: mutex.cpp:131
Fawkes library namespace.