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
32namespace fawkes {
33
34/** Helper class to incorporate bool into mutex locker with RAII */
36{
37public:
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
79private:
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 */
173bool
174ClingoAccess::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 */
224void
225ClingoAccess::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 */
252void
253ClingoAccess::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 */
299ClingoAccess::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 */
324void
325ClingoAccess::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 */
335void
336ClingoAccess::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 */
346void
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 */
358void
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 */
370void
371ClingoAccess::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 */
380bool
381ClingoAccess::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 */
390bool
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 */
414bool
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 */
437bool
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 */
457bool
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.");
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 */
481void
482ClingoAccess::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 */
507int
508ClingoAccess::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 */
525void
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 */
534Clingo::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 */
545bool
546ClingoAccess::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 */
562bool
563ClingoAccess::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 */
606bool
607ClingoAccess::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 */
637bool
638ClingoAccess::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_model_callback(std::shared_ptr< std::function< bool(void)> > callback)
Registers 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.
void unregister_model_callback(std::shared_ptr< std::function< bool(void)> > callback)
Unregisters a callback for the event of a new model.
~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_finish_callback(std::shared_ptr< std::function< void(Clingo::SolveResult)> > callback)
Registers a callback for the event of finishing the solving process.
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.