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(argumentsChar,
276  [this](const Clingo::WarningCode code, char const *msg) {
278  switch (code) {
279  case Clingo::WarningCode::AtomUndefined:
280  case Clingo::WarningCode::OperationUndefined:
281  case Clingo::WarningCode::RuntimeError:
282  level = fawkes::Logger::LL_ERROR;
283  break;
284  case Clingo::WarningCode::Other:
285  case Clingo::WarningCode::VariableUnbounded:
286  level = fawkes::Logger::LL_WARN;
287  break;
288  case Clingo::WarningCode::FileIncluded:
289  case Clingo::WarningCode::GlobalVariable:
290  level = fawkes::Logger::LL_INFO;
291  break;
292  }
293  logger_->log(level, log_comp_.c_str(), msg);
294  return;
295  },
296  100);
297  return;
298 }
299 
300 /** Constructor.
301  * @param[in] logger The used logger.
302  * @param[in] log_component The logging component.
303  */
304 ClingoAccess::ClingoAccess(Logger *logger, const std::string &log_component)
305 : logger_(logger),
306  log_comp_(log_component.empty() ? "Clingo" : log_component),
307  debug_level_(ASP_DBG_NONE),
308  num_threads_(1),
309  thread_mode_splitting_(false),
310  control_is_locked_(false),
311  control_(nullptr),
312  model_mutex_(Mutex::RECURSIVE),
313  solving_(false)
314 {
315  alloc_control();
316 }
317 
318 /** Destructor. */
320 {
321  delete control_;
322 }
323 
324 /**
325  * @brief Registers a callback for the event of a new model. The callback can control with it's return value if the
326  * search for models should continue. If one of the callbacks says yes the search is continued.
327  * @param[in] callback The callback to register.
328  */
329 void
330 ClingoAccess::register_model_callback(std::shared_ptr<std::function<bool(void)>> callback)
331 {
332  MutexLocker locker(&callback_mutex_);
333  model_callbacks_.emplace_back(callback);
334 }
335 
336 /**
337  * @brief Unregisters a callback for the event of a new model.
338  * @param[in] callback The callback to unregister.
339  */
340 void
341 ClingoAccess::unregister_model_callback(std::shared_ptr<std::function<bool(void)>> callback)
342 {
343  MutexLocker locker(&callback_mutex_);
344  model_callbacks_.erase(std::find(model_callbacks_.begin(), model_callbacks_.end(), callback));
345 }
346 
347 /**
348  * @brief Registers a callback for the event of finishing the solving process.
349  * @param[in] callback The callback to register.
350  */
351 void
353  std::shared_ptr<std::function<void(Clingo::SolveResult)>> callback)
354 {
355  MutexLocker locker(&callback_mutex_);
356  finish_callbacks_.emplace_back(callback);
357 }
358 
359 /**
360  * @brief Unregisters a callback for the event of finishing the solving process.
361  * @param[in] callback The callback to unregister.
362  */
363 void
365  std::shared_ptr<std::function<void(Clingo::SolveResult)>> callback)
366 {
367  MutexLocker locker(&callback_mutex_);
368  finish_callbacks_.erase(std::find(finish_callbacks_.begin(), finish_callbacks_.end(), callback));
369 }
370 
371 /**
372  * @brief Sets the ground callback, to implement custom functions.
373  * @param[in, out] callback The callback, will be moved.
374  */
375 void
376 ClingoAccess::set_ground_callback(Clingo::GroundCallback &&callback)
377 {
378  MutexLocker locker(&callback_mutex_);
379  ground_callback_ = std::move(callback);
380 }
381 
382 /** Returns whether the solving process is running.
383  * @return true if currently solving, false otherwise
384  */
385 bool
386 ClingoAccess::solving(void) const noexcept
387 {
388  return solving_;
389 }
390 
391 /**
392  * @brief Starts the solving process, if it isn't already running.
393  * @return If the process is started.
394  */
395 bool
397 {
398  BoolMutexLocker locker(&control_mutex_, control_is_locked_);
399  if (solving_) {
400  return false;
401  }
402  if (debug_level_ >= ASP_DBG_TIME) {
403  logger_->log_info(log_comp_.c_str(), "Start async solving.");
404  }
405 
406  solving_ = true;
407  model_mutex_.lock();
408  model_counter_ = 0;
409  model_mutex_.unlock();
410  async_handle_ = control_->solve(Clingo::SymbolicLiteralSpan{}, this, true, true);
411  return true;
412 }
413 
414 /** Starts the solving process.
415  * If it isn't already running, in a blocking manner, that means it
416  * does not start the computation in an asynchronous way.
417  * @return true, if the process was started
418  */
419 bool
421 {
422  if (solving_) {
423  return false;
424  }
425 
426  BoolMutexLocker locker(&control_mutex_, control_is_locked_);
427  if (debug_level_ >= ASP_DBG_TIME) {
428  logger_->log_info(log_comp_.c_str(), "Start sync solving.");
429  }
430 
431  solving_ = true;
432  model_mutex_.lock();
433  model_counter_ = 0;
434  model_mutex_.unlock();
435  control_->solve(Clingo::SymbolicLiteralSpan{}, this, false, true);
436  return true;
437 }
438 
439 /** Stops the solving process, if it is running.
440  * @return If it was stopped. (Check solving() for actual state!)
441  */
442 bool
444 {
445  BoolMutexLocker locker(&control_mutex_, control_is_locked_);
446  if (!solving_) {
447  return false;
448  }
449 
450  if (debug_level_ >= ASP_DBG_TIME) {
451  logger_->log_info(log_comp_.c_str(), "Cancel solving.");
452  }
453 
454  control_->interrupt();
455  return true;
456 }
457 
458 /** Tries to reset Clingo.
459  * That means deletes the control object and creates a new one.
460  * @return true, if successful
461  */
462 bool
464 {
465  if (solving_) {
466  logger_->log_warn(log_comp_.c_str(),
467  "Could not reset while solving. "
468  "Please try again when the solving is stopped.");
469  cancel_solving();
470  return false;
471  }
472  logger_->log_warn(log_comp_.c_str(), "Resetting Clingo");
473  delete control_;
474  control_ = nullptr;
475  alloc_control();
476  return true;
477 }
478 
479 /** Sets the number of threads Clingo should use.
480  * @param[in] threads The number.
481  * @param[in] thread_mode_splitting Wether splitting should be used.
482  * @warning This will call reset().
483  * @exception Exception If it is called while solving.
484  * @exception Exception If it is called with @c threads < 1.
485  */
486 void
487 ClingoAccess::set_num_threads(const int threads, const bool thread_mode_splitting)
488 {
489  if (solving_) {
490  throw Exception("Tried to set the number of threads while Clingo was solving.");
491  }
492  if (threads < 1) {
493  throw Exception("Tried to set thread count to %d, only values >= 1 are valid.", threads);
494  }
495  logger_->log_info(log_comp_.c_str(),
496  "Change # of threads for solving from %d to %d "
497  "and splitting from %s to %s.",
498  num_threads_,
499  threads,
500  thread_mode_splitting_ ? "true" : "false",
501  thread_mode_splitting ? "true" : "false");
502  num_threads_ = threads;
503  thread_mode_splitting_ = thread_mode_splitting;
504  reset();
505  return;
506 }
507 
508 /** Returns how many threads Clingo should use.
509  * @return number of threads
510  * @see ClingoAccess::num_threads_
511  */
512 int
513 ClingoAccess::num_threads(void) const noexcept
514 {
515  return num_threads_;
516 }
517 
518 /** Get current debug level.
519  * @return current debug level
520  */
523 {
524  return debug_level_.load();
525 }
526 
527 /** Set debug level.
528  * @param log_level new debug level
529  */
530 void
532 {
533  return debug_level_.store(log_level);
534 }
535 
536 /** Returns a copy of the last symbols found.
537  * @return copy of last symbols found
538  */
539 Clingo::SymbolVector
541 {
542  MutexLocker locker(&model_mutex_);
543  return model_symbols_;
544 }
545 
546 /** Loads a file in the solver.
547  * @param[in] path The path of the file.
548  * @return true, if file was loaded
549  */
550 bool
551 ClingoAccess::load_file(const std::string &path)
552 {
553  BoolMutexLocker locker(&control_mutex_, control_is_locked_);
554  if (solving_) {
555  return false;
556  }
557 
558  logger_->log_info(log_comp_.c_str(), "Loading file program file %s.", path.c_str());
559  control_->load(path.c_str());
560  return true;
561 }
562 
563 /** Grounds a program part.
564  * @param[in] parts The parts to ground.
565  * @return true if parts could be grounded
566  */
567 bool
568 ClingoAccess::ground(const Clingo::PartSpan &parts)
569 {
570  if (parts.empty()) {
571  return true;
572  }
573 
574  BoolMutexLocker locker(&control_mutex_, control_is_locked_);
575  if (solving_) {
576  return false;
577  }
578  if (debug_level_ >= ASP_DBG_TIME) {
579  logger_->log_info(log_comp_.c_str(), "Grounding %zu parts:", parts.size());
580  if (debug_level_ >= ASP_DBG_PROGRAMS) {
581  auto i = 0;
582  for (const Clingo::Part &part : parts) {
583  std::string params;
584  bool first = true;
585  for (const auto &param : part.params()) {
586  if (first) {
587  first = false;
588  } else {
589  params += ", ";
590  }
591  params += param.to_string();
592  }
593  logger_->log_info(log_comp_.c_str(), "Part #%d: %s [%s]", ++i, part.name(), params.c_str());
594  }
595  }
596  }
597 
598  control_->ground(parts, ground_callback_);
599 
600  if (debug_level_ >= ASP_DBG_TIME) {
601  logger_->log_info(log_comp_.c_str(), "Grounding done.");
602  }
603  return true;
604 }
605 
606 /** Assigns an external value.
607  * @param[in] atom The atom to assign.
608  * @param[in] value The assigned value.
609  * @return If it could be assigned.
610  */
611 bool
612 ClingoAccess::assign_external(const Clingo::Symbol &atom, const Clingo::TruthValue value)
613 {
614  BoolMutexLocker locker(&control_mutex_, control_is_locked_);
615  if (solving_) {
616  return false;
617  }
618 
619  if (debug_level_ >= ASP_DBG_EXTERNALS) {
620  logger_->log_info(log_comp_.c_str(),
621  "Assigning %s to %s.",
622  [value](void) {
623  const char *ret = "Unknown Value";
624  switch (value) {
625  case Clingo::TruthValue::Free: ret = "Free"; break;
626  case Clingo::TruthValue::True: ret = "True"; break;
627  case Clingo::TruthValue::False: ret = "False"; break;
628  }
629  return ret;
630  }(),
631  atom.to_string().c_str());
632  }
633  control_->assign_external(atom, value);
634  return true;
635 }
636 
637 /** Releases an external value.
638  * @param[in] atom The atom to release.
639  * @return true, if it could be released
640  */
641 bool
642 ClingoAccess::release_external(const Clingo::Symbol &atom)
643 {
644  BoolMutexLocker locker(&control_mutex_, control_is_locked_);
645  if (solving_) {
646  return false;
647  }
648 
649  if (debug_level_ >= ASP_DBG_EXTERNALS) {
650  logger_->log_info(log_comp_.c_str(), "Releasing %s.", atom.to_string().c_str());
651  }
652  control_->release_external(atom);
653  return true;
654 }
655 
656 } // end namespace fawkes
LogLevel
Log level.
Definition: logger.h:51
bool start_solving(void)
Starts the solving process, if it isn't already running.
informational output about normal procedures
Definition: logger.h:53
virtual void log_info(const char *component, const char *format,...)=0
Log informational message.
int num_threads(void) const noexcept
Returns how many threads Clingo should use.
bool load_file(const std::string &path)
Loads a file in the solver.
void relock(void)
Relock mutex after unlock.
Fawkes library namespace.
void unlock()
Unlock the mutex.
Definition: mutex.cpp:131
void unlock(void)
Unlock mutex.
Mutex locking helper.
Definition: mutex_locker.h:33
Print which programs are grounded.
Definition: clingo_access.h:45
warning, should be investigated but software still functions, an example is that something was reques...
Definition: logger.h:54
bool start_solving_blocking(void)
Starts the solving process.
Print assignments and releases of externals.
Definition: clingo_access.h:46
void set_debug_level(DebugLevel_t log_level)
Set debug level.
bool reset(void)
Tries to reset Clingo.
void set_ground_callback(Clingo::GroundCallback &&callback)
Sets the ground callback, to implement custom functions.
void unregister_model_callback(std::shared_ptr< std::function< bool(void)>> callback)
Unregisters a callback for the event of a new model.
bool release_external(const Clingo::Symbol &atom)
Releases an external value.
error, may be recoverable (software still running) or not (software has to terminate).
Definition: logger.h:57
DebugLevel_t debug_level() const
Get current debug level.
Base class for exceptions in Fawkes.
Definition: exception.h:35
Clingo::SymbolVector model_symbols(void) const
Returns a copy of the last symbols found.
void register_finish_callback(std::shared_ptr< std::function< void(Clingo::SolveResult)>> callback)
Registers a callback for the event of finishing the solving process.
~BoolMutexLocker(void)
Destructor.
DebugLevel_t
Debug levels, higher levels include the lower values.
Definition: clingo_access.h:42
void register_model_callback(std::shared_ptr< std::function< bool(void)>> callback)
Registers a callback for the event of a new model.
Print when starting/finishing grounding/solving for analysis.
Definition: clingo_access.h:44
virtual void log_warn(const char *component, const char *format,...)=0
Log warning message.
Ignore '#show' statements and print all symbols of a model.
Definition: clingo_access.h:48
void unregister_finish_callback(std::shared_ptr< std::function< void(Clingo::SolveResult)>> callback)
Unregisters a callback for the event of finishing the solving process.
bool solving(void) const noexcept
Returns whether the solving process is running.
bool ground(const Clingo::PartSpan &parts)
Grounds a program part.
BoolMutexLocker(Mutex *mutex, bool &associated_bool)
Constructor.
void set_num_threads(const int threads, const bool use_splitting=false)
Sets the number of threads Clingo should use.
void lock()
Lock this mutex.
Definition: mutex.cpp:87
ClingoAccess(Logger *logger, const std::string &log_component)
Constructor.
Mutex mutual exclusion lock.
Definition: mutex.h:32
virtual void log(LogLevel level, const char *component, const char *format,...)
Log message of given log level.
Definition: logger.cpp:326
Helper class to incorporate bool into mutex locker with RAII.
~ClingoAccess(void)
Destructor.
use this to disable log output
Definition: logger.h:60
bool assign_external(const Clingo::Symbol &atom, const bool value)
Assign external value.
Definition: clingo_access.h:82
bool cancel_solving(void)
Stops the solving process, if it is running.
Activates the –output-debug=text option for clingo.
Definition: clingo_access.h:51
Interface for logging.
Definition: logger.h:41