diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 93ec9479..c0b9f644 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -4,6 +4,8 @@ repos: rev: v1.3.5 hooks: - id: clang-format + exclude: _clingodl.c args: ["-i"] - id: clang-tidy + exclude: _clingodl.c args: ["-fix"] diff --git a/app/lib/clingo-dl-app/app.hh b/app/lib/clingo-dl-app/app.hh index c456212a..b92ddb0a 100644 --- a/app/lib/clingo-dl-app/app.hh +++ b/app/lib/clingo-dl-app/app.hh @@ -25,8 +25,8 @@ #ifndef CLINGODL_APP_HH #define CLINGODL_APP_HH -#include #include +#include #include namespace ClingoDL { @@ -36,19 +36,19 @@ using int_value_t = int; //! Helper class to rewrite logic programs to use with the clingo DL theory. class Rewriter { -public: + public: Rewriter(clingodl_theory_t *theory, clingo_program_builder_t *builder); //! Rewrite the given files. void rewrite(Clingo::Control &ctl, Clingo::StringSpan files); //! Rewrite the given program. void rewrite(Clingo::Control &ctl, char const *str); -private: + private: //! C callback to add a statement using the builder. - static bool add_(clingo_ast_t *stm, void *data); + static auto add_(clingo_ast_t *stm, void *data) -> bool; //! C callback to rewrite a statement and add it via the builder. - static bool rewrite_(clingo_ast_t *stm, void *data); + static auto rewrite_(clingo_ast_t *stm, void *data) -> bool; clingodl_theory_t *theory_; //!< A theory handle to rewrite statements. clingo_program_builder_t *builder_; //!< The builder to add rewritten statements to. @@ -66,12 +66,12 @@ struct OptimizerConfig { //! Class providing a configurable optimization algorithm. class Optimizer : private Clingo::SolveEventHandler { -private: + private: //! Type used to store bounds. using Bound = std::optional; using EventHandler = Clingo::SolveEventHandler; -public: + public: Optimizer(OptimizerConfig const &opt_cfg, EventHandler &handler, clingodl_theory_t *theory); //! Run the optimization algorithm. //! @@ -79,23 +79,23 @@ public: //! With an API extension to implement a custom enumerator, one could //! implement this more nicely. Right now, this implementation is //! restricted to the application. - void solve(Clingo::Control& ctl); + void solve(Clingo::Control &ctl); -private: + private: //! Function to add DL specific statistics. void on_statistics(Clingo::UserStatistics step, Clingo::UserStatistics accu) override; //! Add information about bounds to the given root statistics object and //! pass call the theory specific handler. void add_stats(Clingo::UserStatistics root) const; //! Function to extract the current bound and pass the model to the theory. - bool on_model(Clingo::Model &model) override; + auto on_model(Clingo::Model &model) -> bool override; //! Extract the bound from the given model. - int_value_t get_bound(Clingo::Model &model); + auto get_bound(Clingo::Model &model) -> int_value_t; //! Prepare the program for solving. //! //! This adds constraints to enforce the current upper or search bound as //! well as removes no longer required bounds. - void prepare_(Clingo::Control& ctl); + void prepare_(Clingo::Control &ctl); OptimizerConfig const &opt_cfg_; //!< Configuration of the optimization algorithm. EventHandler &handler_; //!< Theory specific solve event handler. diff --git a/app/lib/src/app.cc b/app/lib/src/app.cc index 1b12839b..6a00b05d 100644 --- a/app/lib/src/app.cc +++ b/app/lib/src/app.cc @@ -24,52 +24,47 @@ #include +#include #include #include -#include namespace ClingoDL { -Rewriter::Rewriter(clingodl_theory_t *theory, clingo_program_builder_t *builder) -: theory_{theory} -, builder_{builder} { -} +Rewriter::Rewriter(clingodl_theory_t *theory, clingo_program_builder_t *builder) : theory_{theory}, builder_{builder} {} void Rewriter::rewrite(Clingo::Control &ctl, Clingo::StringSpan files) { - Clingo::Detail::handle_error(clingo_ast_parse_files(files.begin(), files.size(), rewrite_, this, ctl.to_c(), nullptr, nullptr, 0)); + Clingo::Detail::handle_error( + clingo_ast_parse_files(files.begin(), files.size(), rewrite_, this, ctl.to_c(), nullptr, nullptr, 0)); } void Rewriter::rewrite(Clingo::Control &ctl, char const *str) { Clingo::Detail::handle_error(clingo_ast_parse_string(str, rewrite_, this, ctl.to_c(), nullptr, nullptr, 0)); } -bool Rewriter::add_(clingo_ast_t *stm, void *data) { - auto *self = static_cast(data); +auto Rewriter::add_(clingo_ast_t *stm, void *data) -> bool { + auto *self = static_cast(data); return clingo_program_builder_add(self->builder_, stm); } -bool Rewriter::rewrite_(clingo_ast_t *stm, void *data) { - auto *self = static_cast(data); +auto Rewriter::rewrite_(clingo_ast_t *stm, void *data) -> bool { + auto *self = static_cast(data); return clingodl_rewrite_ast(self->theory_, stm, add_, self); } Optimizer::Optimizer(OptimizerConfig const &opt_cfg, Clingo::SolveEventHandler &handler, clingodl_theory_t *theory) -: opt_cfg_{opt_cfg} -, handler_{handler} -, theory_{theory} { -} + : opt_cfg_{opt_cfg}, handler_{handler}, theory_{theory} {} -void Optimizer::solve(Clingo::Control& ctl) { +void Optimizer::solve(Clingo::Control &ctl) { Clingo::AST::with_builder(ctl, [&](Clingo::AST::ProgramBuilder &builder) { Rewriter rewriter{theory_, builder.to_c()}; rewriter.rewrite(ctl, - // add a fixed bound - "#program __ub(s,b)." - "&diff { s-0 } <= b." - // add a retractable bound - "#program __sb(s,b)." - "#external __sb(b). [true]" - "&diff { s-0 } <= b :- __sb(b)."); + // add a fixed bound + "#program __ub(s,b)." + "&diff { s-0 } <= b." + // add a retractable bound + "#program __sb(s,b)." + "#external __sb(b). [true]" + "&diff { s-0 } <= b :- __sb(b)."); }); if (opt_cfg_.has_initial) { upper_bound_ = opt_cfg_.initial; @@ -111,7 +106,7 @@ void Optimizer::add_stats(Clingo::UserStatistics root) const { } } -bool Optimizer::on_model(Clingo::Model &model) { +auto Optimizer::on_model(Clingo::Model &model) -> bool { // update (upper) bound optimization = get_bound(model); upper_bound_ = *optimization - 1; @@ -134,7 +129,7 @@ bool Optimizer::on_model(Clingo::Model &model) { return false; } -int_value_t Optimizer::get_bound(Clingo::Model &model) { +auto Optimizer::get_bound(Clingo::Model &model) -> int_value_t { // get bound if (opt_cfg_.index == 0) { if (!clingodl_lookup_symbol(theory_, opt_cfg_.symbol.to_c(), &opt_cfg_.index)) { @@ -153,7 +148,7 @@ int_value_t Optimizer::get_bound(Clingo::Model &model) { return value.int_number; // NOLINT } -void Optimizer::prepare_(Clingo::Control& ctl) { +void Optimizer::prepare_(Clingo::Control &ctl) { if (upper_bound_ && upper_bound_ != upper_bound_last_) { upper_bound_last_ = upper_bound_; ctl.ground({{"__ub", {opt_cfg_.symbol, Clingo::Number(*upper_bound_)}}}); @@ -165,8 +160,7 @@ void Optimizer::prepare_(Clingo::Control& ctl) { if (search_bound_ && search_bound_ != upper_bound_) { search_bound_last_ = search_bound_; ctl.ground({{"__sb", {opt_cfg_.symbol, Clingo::Number(*search_bound_)}}}); - } - else { + } else { search_bound_last_ = Bound{}; } } diff --git a/app/src/main.cc b/app/src/main.cc index e30c2369..36dbd0d5 100644 --- a/app/src/main.cc +++ b/app/src/main.cc @@ -22,12 +22,12 @@ // }}} -#include -#include #include -#include +#include +#include #include #include +#include #ifdef CLINGODL_PROFILE #include @@ -39,27 +39,19 @@ using Clingo::Detail::handle_error; //! Application class to run clingo-dl. class App : public Clingo::Application, private Clingo::SolveEventHandler { -public: - App() { - handle_error(clingodl_create(&theory_)); - } + public: + App() { handle_error(clingodl_create(&theory_)); } App(App const &) = default; App(App &&) = default; - App &operator=(App const &) = default; - App &operator=(App &&) = default; - ~App() override { - clingodl_destroy(theory_); - } + auto operator=(App const &) -> App & = default; + auto operator=(App &&) -> App & = default; + ~App() override { clingodl_destroy(theory_); } //! Set program name to clingo-dl. - char const *program_name() const noexcept override { - return "clingo-dl"; - } + auto program_name() const noexcept -> char const * override { return "clingo-dl"; } //! Set the version. - char const *version() const noexcept override { - return CLINGODL_VERSION; - } + auto version() const noexcept -> char const * override { return CLINGODL_VERSION; } //! Pass models to the theory. - bool on_model(Clingo::Model &model) override { + auto on_model(Clingo::Model &model) -> bool override { handle_error(clingodl_on_model(theory_, model.to_c())); return true; } @@ -82,8 +74,7 @@ class App : public Clingo::Application, private Clingo::SolveEventHandler { #endif if (!opt_cfg_.active) { ctl.solve(Clingo::SymbolicLiteralSpan{}, this, false, false).get(); - } - else { + } else { Optimizer{opt_cfg_, *this, theory_}.solve(ctl); } #ifdef CLINGODL_PROFILE @@ -91,7 +82,7 @@ class App : public Clingo::Application, private Clingo::SolveEventHandler { #endif } //! Parse the variable to minimize and an optional initial bound. - bool parse_bound(char const *value) { + auto parse_bound(char const *value) -> bool { std::ostringstream oss; oss << "(" << value << ",)"; auto term = Clingo::parse_term(oss.str().c_str()); @@ -109,7 +100,7 @@ class App : public Clingo::Application, private Clingo::SolveEventHandler { return true; } //! Parse factor to adjust optimization step length. - bool parse_factor(char const *value) { + auto parse_factor(char const *value) -> bool { std::stringstream strValue; strValue.imbue(std::locale::classic()); strValue << value; @@ -124,32 +115,29 @@ class App : public Clingo::Application, private Clingo::SolveEventHandler { //! Register options of the theory and optimization related options. void register_options(Clingo::ClingoOptions &options) override { handle_error(clingodl_register_options(theory_, options.to_c())); - char const * group = "Clingo.DL Options"; + char const *group = "Clingo.DL Options"; options.add(group, "minimize-variable", - "Minimize the given variable\n" - " : [,]\n" - " : the variable to minimize\n" - " : upper bound for the variable", - [this](char const *value) { return parse_bound(value); }); - options.add(group, "minimize-factor", - "Factor to adjust minimization step size [1]", - [this](char const *value) { return parse_factor(value); }, - false, ""); + "Minimize the given variable\n" + " : [,]\n" + " : the variable to minimize\n" + " : upper bound for the variable", + [this](char const *value) { return parse_bound(value); }); + options.add( + group, "minimize-factor", "Factor to adjust minimization step size [1]", + [this](char const *value) { return parse_factor(value); }, false, ""); } //! Validate options of the theory. - void validate_options() override { - handle_error(clingodl_validate_options(theory_)); - } + void validate_options() override { handle_error(clingodl_validate_options(theory_)); } -private: + private: clingodl_theory_t *theory_{nullptr}; //!< The underlying DL theory. OptimizerConfig opt_cfg_; //!< The optimization configuration. }; -} // namespace CLingoDL +} // namespace ClingoDL //! Run the clingo-dl application. -int main(int argc, char *argv[]) { // NOLINT(bugprone-exception-escape) +auto main(int argc, char *argv[]) -> int { // NOLINT(bugprone-exception-escape) ClingoDL::App app; return Clingo::clingo_main(app, {argv + 1, static_cast(argc - 1)}); } diff --git a/libclingo-dl/clingo-dl.h b/libclingo-dl/clingo-dl.h index bc756e5c..baf92679 100644 --- a/libclingo-dl/clingo-dl.h +++ b/libclingo-dl/clingo-dl.h @@ -25,6 +25,8 @@ #ifndef CLINGODL_H #define CLINGODL_H +#include + //! Major version number. #define CLINGODL_VERSION_MAJOR 1 //! Minor version number. @@ -39,31 +41,31 @@ extern "C" { #endif #if defined _WIN32 || defined __CYGWIN__ -# define CLINGODL_WIN +#define CLINGODL_WIN #endif #ifdef CLINGODL_NO_VISIBILITY -# define CLINGODL_VISIBILITY_DEFAULT -# define CLINGODL_VISIBILITY_PRIVATE +#define CLINGODL_VISIBILITY_DEFAULT +#define CLINGODL_VISIBILITY_PRIVATE +#else +#ifdef CLINGODL_WIN +#ifdef CLINGODL_BUILD_LIBRARY +#define CLINGODL_VISIBILITY_DEFAULT __declspec(dllexport) +#else +#define CLINGODL_VISIBILITY_DEFAULT __declspec(dllimport) +#endif +#define CLINGODL_VISIBILITY_PRIVATE #else -# ifdef CLINGODL_WIN -# ifdef CLINGODL_BUILD_LIBRARY -# define CLINGODL_VISIBILITY_DEFAULT __declspec (dllexport) -# else -# define CLINGODL_VISIBILITY_DEFAULT __declspec (dllimport) -# endif -# define CLINGODL_VISIBILITY_PRIVATE -# else -# if __GNUC__ >= 4 -# define CLINGODL_VISIBILITY_DEFAULT __attribute__ ((visibility ("default"))) -# define CLINGODL_VISIBILITY_PRIVATE __attribute__ ((visibility ("hidden"))) -# else -# define CLINGODL_VISIBILITY_DEFAULT -# define CLINGODL_VISIBILITY_PRIVATE -# endif -# endif +#if __GNUC__ >= 4 +#define CLINGODL_VISIBILITY_DEFAULT __attribute__((visibility("default"))) +#define CLINGODL_VISIBILITY_PRIVATE __attribute__((visibility("hidden"))) +#else +#define CLINGODL_VISIBILITY_DEFAULT +#define CLINGODL_VISIBILITY_PRIVATE +#endif +#endif #endif -#include +// NOLINTBEGIN(modernize-use-using,modernize-use-trailing-return-type) enum clingodl_value_type { clingodl_value_type_int = 0, @@ -93,13 +95,14 @@ CLINGODL_VISIBILITY_DEFAULT void clingodl_version(int *major, int *minor, int *p CLINGODL_VISIBILITY_DEFAULT bool clingodl_create(clingodl_theory_t **theory); //! registers the theory with the control -CLINGODL_VISIBILITY_DEFAULT bool clingodl_register(clingodl_theory_t *theory, clingo_control_t* control); +CLINGODL_VISIBILITY_DEFAULT bool clingodl_register(clingodl_theory_t *theory, clingo_control_t *control); //! Rewrite asts before adding them via the given callback. -CLINGODL_VISIBILITY_DEFAULT bool clingodl_rewrite_ast(clingodl_theory_t *theory, clingo_ast_t *ast, clingodl_ast_callback_t add, void *data); +CLINGODL_VISIBILITY_DEFAULT bool clingodl_rewrite_ast(clingodl_theory_t *theory, clingo_ast_t *ast, + clingodl_ast_callback_t add, void *data); //! prepare the theory between grounding and solving -CLINGODL_VISIBILITY_DEFAULT bool clingodl_prepare(clingodl_theory_t *theory, clingo_control_t* control); +CLINGODL_VISIBILITY_DEFAULT bool clingodl_prepare(clingodl_theory_t *theory, clingo_control_t *control); //! destroys the theory, currently no way to unregister a theory CLINGODL_VISIBILITY_DEFAULT bool clingodl_destroy(clingodl_theory_t *theory); @@ -109,18 +112,19 @@ CLINGODL_VISIBILITY_DEFAULT bool clingodl_destroy(clingodl_theory_t *theory); CLINGODL_VISIBILITY_DEFAULT bool clingodl_configure(clingodl_theory_t *theory, char const *key, char const *value); //! add options for your theory -CLINGODL_VISIBILITY_DEFAULT bool clingodl_register_options(clingodl_theory_t *theory, clingo_options_t* options); +CLINGODL_VISIBILITY_DEFAULT bool clingodl_register_options(clingodl_theory_t *theory, clingo_options_t *options); //! validate options for your theory CLINGODL_VISIBILITY_DEFAULT bool clingodl_validate_options(clingodl_theory_t *theory); //! callback on every model -CLINGODL_VISIBILITY_DEFAULT bool clingodl_on_model(clingodl_theory_t *theory, clingo_model_t* model); +CLINGODL_VISIBILITY_DEFAULT bool clingodl_on_model(clingodl_theory_t *theory, clingo_model_t *model); //! obtain a symbol index which can be used to get the value of a symbol //! returns true if the symbol exists //! does not throw -CLINGODL_VISIBILITY_DEFAULT bool clingodl_lookup_symbol(clingodl_theory_t *theory, clingo_symbol_t symbol, size_t *index); +CLINGODL_VISIBILITY_DEFAULT bool clingodl_lookup_symbol(clingodl_theory_t *theory, clingo_symbol_t symbol, + size_t *index); //! obtain the symbol at the given index //! does not throw @@ -128,7 +132,8 @@ CLINGODL_VISIBILITY_DEFAULT clingo_symbol_t clingodl_get_symbol(clingodl_theory_ //! initialize index so that it can be used with clingodl_assignment_next //! does not throw -CLINGODL_VISIBILITY_DEFAULT void clingodl_assignment_begin(clingodl_theory_t *theory, uint32_t thread_id, size_t *index); +CLINGODL_VISIBILITY_DEFAULT void clingodl_assignment_begin(clingodl_theory_t *theory, uint32_t thread_id, + size_t *index); //! move to the next index that has a value //! returns true if the updated index is valid @@ -137,15 +142,20 @@ CLINGODL_VISIBILITY_DEFAULT bool clingodl_assignment_next(clingodl_theory_t *the //! check if the symbol at the given index has a value //! does not throw -CLINGODL_VISIBILITY_DEFAULT bool clingodl_assignment_has_value(clingodl_theory_t *theory, uint32_t thread_id, size_t index); +CLINGODL_VISIBILITY_DEFAULT bool clingodl_assignment_has_value(clingodl_theory_t *theory, uint32_t thread_id, + size_t index); //! get the symbol and it's value at the given index //! does not throw -CLINGODL_VISIBILITY_DEFAULT void clingodl_assignment_get_value(clingodl_theory_t *theory, uint32_t thread_id, size_t index, clingodl_value_t *value); +CLINGODL_VISIBILITY_DEFAULT void clingodl_assignment_get_value(clingodl_theory_t *theory, uint32_t thread_id, + size_t index, clingodl_value_t *value); //! callback on statistic updates /// please add a subkey with the name of your theory -CLINGODL_VISIBILITY_DEFAULT bool clingodl_on_statistics(clingodl_theory_t *theory, clingo_statistics_t* step, clingo_statistics_t* accu); +CLINGODL_VISIBILITY_DEFAULT bool clingodl_on_statistics(clingodl_theory_t *theory, clingo_statistics_t *step, + clingo_statistics_t *accu); + +// NOLINTEND(modernize-use-using,modernize-use-trailing-return-type) #ifdef __cplusplus } diff --git a/libclingo-dl/clingo-dl/config.hh b/libclingo-dl/clingo-dl/config.hh index 443bc1c0..2348898f 100644 --- a/libclingo-dl/clingo-dl/config.hh +++ b/libclingo-dl/clingo-dl/config.hh @@ -26,36 +26,36 @@ #define CLINGODL_CONFIG_HH #include -#include #include +#include #include namespace ClingoDL { //! Enumeration to configure propagation strength. enum class PropagationMode { - Check = 0, //!< Only check for conflicting assignments. - Trivial = 1, //!< Check inverse constraits. - Weak = 2, //!< Perform weak propagation. + Check = 0, //!< Only check for conflicting assignments. + Trivial = 1, //!< Check inverse constraits. + Weak = 2, //!< Perform weak propagation. WeakPlus = 3, //!< Perform weak propagation with some extra effort. - Zero = 4, //!< Perform propagation through zero node. - Strong = 5 //!< Perform full propagation. + Zero = 4, //!< Perform propagation through zero node. + Strong = 5 //!< Perform full propagation. }; //! Enumeration to configure sorting of edges before propagation. enum class SortMode { - No = 0, //! Do not sort edges. - Weight = 1, //! Sort edges by weight in ascending order. - WeightRev = 2, //! Sort edges by weight in descending order. - Potential = 3, //! Sort edges by potential in ascending order. - PotentialRev = 4 //! Sort edges by potential in descending order. + No = 0, //! Do not sort edges. + Weight = 1, //! Sort edges by weight in ascending order. + WeightRev = 2, //! Sort edges by weight in descending order. + Potential = 3, //! Sort edges by potential in ascending order. + PotentialRev = 4 //! Sort edges by potential in descending order. }; //! Enumeration to configure sorting of edges before propagation. enum class DecisionMode { - Disabled = 0, //! Do not modify decision heuristic. - MinConflict = 1, //! Try to minimize conflicts. - MaxConflict = 2, //! Try to maximize conflicts. + Disabled = 0, //! Do not modify decision heuristic. + MinConflict = 1, //! Try to minimize conflicts. + MaxConflict = 2, //! Try to maximize conflicts. }; //! Default value for PropagatorConfig::sort_mode. @@ -109,34 +109,33 @@ struct PropagatorConfig { bool calculate_cc{CALCULATE_CC}; //! Get per thread propagate_root if present or global value. - [[nodiscard]] uint64_t get_propagate_root(Clingo::id_t thread_id) const { + [[nodiscard]] auto get_propagate_root(Clingo::id_t thread_id) const -> uint64_t { return get_prop(thread_id, propagate_root, &ThreadConfig::propagate_root); } //! Get per thread propagate_budget if present or global value. - [[nodiscard]] uint64_t get_propagate_budget(Clingo::id_t thread_id) const { + [[nodiscard]] auto get_propagate_budget(Clingo::id_t thread_id) const -> uint64_t { return get_prop(thread_id, propagate_budget, &ThreadConfig::propagate_budget); } //! Get per thread propagate_mode if present or global value. - [[nodiscard]] PropagationMode get_propagate_mode(Clingo::id_t thread_id) const { + [[nodiscard]] auto get_propagate_mode(Clingo::id_t thread_id) const -> PropagationMode { return get_prop(thread_id, propagate_mode, &ThreadConfig::propagate_mode); } //! Get per thread sort_mode if present or global value. - [[nodiscard]] SortMode get_sort_mode(Clingo::id_t thread_id) const { + [[nodiscard]] auto get_sort_mode(Clingo::id_t thread_id) const -> SortMode { return get_prop(thread_id, sort_mode, &ThreadConfig::sort_mode); } //! Return the thread config for the given thread or return a default //! constructed object if absent. - ThreadConfig &ensure(Clingo::id_t thread_id) { + auto ensure(Clingo::id_t thread_id) -> ThreadConfig & { if (thread_config.size() < thread_id + 1) { thread_config.resize(thread_id + 1); } return thread_config[thread_id]; } -private: + private: //! Helper to access per thread or global properties. - template - [[nodiscard]] T get_prop(Clingo::id_t thread_id, T &&def, P &&prop) const { + template [[nodiscard]] auto get_prop(Clingo::id_t thread_id, T &&def, P &&prop) const -> T { if (thread_id < thread_config.size() && thread_config[thread_id].*prop) { return *(thread_config[thread_id].*prop); } diff --git a/libclingo-dl/clingo-dl/graph.hh b/libclingo-dl/clingo-dl/graph.hh index 6670b79a..31d2638e 100644 --- a/libclingo-dl/clingo-dl/graph.hh +++ b/libclingo-dl/clingo-dl/graph.hh @@ -25,16 +25,15 @@ #ifndef CLINGODL_GRAPH_HH #define CLINGODL_GRAPH_HH -#include -#include #include +#include #include +#include namespace ClingoDL { //! Struct to represent an edge in the difference logic graph. -template -struct Edge { +template struct Edge { using value_t = T; //!< The value type (integral or floating point). vertex_t from; //!< Start vertex index of the edge. vertex_t to; //!< End vertex index of the edge. @@ -69,14 +68,12 @@ struct ThreadStatistics { //! edges, perform propagation, and access the assignment to vertices. //! //! The class is meant to be used by the DLPropagator. -template -class Graph { -private: +template class Graph { + private: struct Vertex; struct EdgeState; struct TrailEntry; - template - struct Impl; + template struct Impl; using HeapType = Heap<4>; //!< The heap type used in (dijkstra-like) algorithms. using index_t = HeapType::index_type; //!< Type for indexing (32bit unsigned). using value_t = T; //!< The value type (integral or floating point). @@ -87,25 +84,25 @@ private: //! Trail of bound changes involving a vertex, path, and value. using BoundTrailVec = std::vector>; -public: + public: Graph(ThreadStatistics &stats, EdgeVec const &edges, PropagationMode propagate); Graph(Graph const &other) = delete; Graph(Graph &&other) noexcept; - Graph &operator=(Graph const &other) = delete; - Graph &operator=(Graph &&other) = delete; + auto operator=(Graph const &other) -> Graph & = delete; + auto operator=(Graph &&other) -> Graph & = delete; ~Graph(); //! Return no edges have been added to the graph yet. - [[nodiscard]] bool empty() const; + [[nodiscard]] auto empty() const -> bool; //! Return true if a potential has been assigned to the vertex. - [[nodiscard]] bool has_value(vertex_t idx) const; + [[nodiscard]] auto has_value(vertex_t idx) const -> bool; //! Return true the (inverted) potential of a vertex. - [[nodiscard]] value_t get_value(vertex_t idx) const; + [[nodiscard]] auto get_value(vertex_t idx) const -> value_t; //! Return true if the edge is enabled. //! //! Disabled edges are ignored during full propagation. - [[nodiscard]] bool edge_is_enabled(edge_t edge_idx) const; + [[nodiscard]] auto edge_is_enabled(edge_t edge_idx) const -> bool; //! Check if the edge is negative w.r.t. the current assginment of potentials. - [[nodiscard]] bool edge_is_negative(edge_t edge_idx) const; + [[nodiscard]] auto edge_is_negative(edge_t edge_idx) const -> bool; //! This disables an edge. //! //! Any edge whose literal became true or false is disabled. See also @@ -115,7 +112,7 @@ public: //! //! Propagation can be disabled on a decision level. It will stay disabled //! on higher decision level and reset during backtracking. - [[nodiscard]] bool can_propagate() const; + [[nodiscard]] auto can_propagate() const -> bool; //! Disable propagation on the current and higher decision levels. //! //! See also can_propagate(). @@ -125,28 +122,28 @@ public: //! Add an edge to the graph and return false if the edge induces a negative cycle. //! //! This function assumes that the graph is not conflicting. - [[nodiscard]] bool add_edge(Clingo::PropagateControl &ctl, edge_t uv_idx, vertex_t zero_idx); + [[nodiscard]] auto add_edge(Clingo::PropagateControl &ctl, edge_t uv_idx, vertex_t zero_idx) -> bool; //! Backtracks the last decision level established with ensure_decision_level(). void backtrack(); //! Return the configured propagation mode. - [[nodiscard]] PropagationMode mode() const; + [[nodiscard]] auto mode() const -> PropagationMode; -private: + private: //! Checks if there is a cycle after adding the given edge. //! //! The function does not clean up information about found shortest paths. //! //! \note Has to be called during add_edge(). - bool check_cycle_(Clingo::PropagateControl &ctl, edge_t uv_idx); + auto check_cycle_(Clingo::PropagateControl &ctl, edge_t uv_idx) -> bool; //! Perform configured simple propagations after adding the given edge. //! //! \note Has to be called during add_edge() and uses temporary state //! established during check_cycle_(). - bool propagate_simple_(Clingo::PropagateControl &ctl, edge_t uv_idx); + auto propagate_simple_(Clingo::PropagateControl &ctl, edge_t uv_idx) -> bool; //! Propagates edges to avoid cycles through the zero node. //! //! \note Has to be called during add_edge(). - bool propagate_zero_(Clingo::PropagateControl &ctl, edge_t uv_idx, vertex_t zero_idx); + auto propagate_zero_(Clingo::PropagateControl &ctl, edge_t uv_idx, vertex_t zero_idx) -> bool; //! Fully propagates the graph after adding the given edge. //! //! Afterward any of the remaining edges can be added to the graph without @@ -154,7 +151,7 @@ private: //! propagated before the edge was added. //! //! \note Has to be called during add_edge(). - [[nodiscard]] bool propagate_full_(Clingo::PropagateControl &ctl, edge_t xy_idx); + [[nodiscard]] auto propagate_full_(Clingo::PropagateControl &ctl, edge_t xy_idx) -> bool; //! Traverse the incoming edges of a vertex. //! //! Edges that were disabled will be removed during the traversal. The @@ -162,23 +159,22 @@ private: //! the callback returns true. Furthermore, the functions assumes that the //! callback provides a clause in this case. If adding the clause causes a //! conflict, the traversal will stop and the function returns false. - template - [[nodiscard]] bool with_incoming_(Clingo::PropagateControl &ctl, vertex_t s_idx, F f); + template [[nodiscard]] auto with_incoming_(Clingo::PropagateControl &ctl, vertex_t s_idx, F f) -> bool; //! If s has been reached from u, we can use the current potentials to //! detect some conflicts involving incoming edges of s. - [[nodiscard]] bool cheap_propagate_(Clingo::PropagateControl &ctl, vertex_t u_idx, vertex_t s_idx); + [[nodiscard]] auto cheap_propagate_(Clingo::PropagateControl &ctl, vertex_t u_idx, vertex_t s_idx) -> bool; //! Helper to add candidate edges initially and during backtracking. void add_candidate_edge_(edge_t uv_idx); //! Disable edge u -> v, if there is a shorter path u ->* v. - template - [[nodiscard]] bool propagate_edge_true_(edge_t uv_idx, edge_t xy_idx); + template [[nodiscard]] auto propagate_edge_true_(edge_t uv_idx, edge_t xy_idx) -> bool; //! Make edge u -> v false, if there is a negative cycle u ->* v -> u. template - [[nodiscard]] bool propagate_edge_false_(Clingo::PropagateControl &ctl, edge_t uv_idx, edge_t xy_idx, bool &ret); + [[nodiscard]] auto propagate_edge_false_(Clingo::PropagateControl &ctl, edge_t uv_idx, edge_t xy_idx, bool &ret) + -> bool; //! Sets the potential of a vertex and ensures that it can be backtracked. void set_potential_(Vertex &vtx, level_t level, value_t potential); //! Returns the current decision level. - [[nodiscard]] level_t current_decision_level_(); + [[nodiscard]] auto current_decision_level_() -> level_t; HeapType costs_heap_; //!< Heap used throught various algorithms. std::vector visited_from_; //!< Vertices visited during traversal of the original graph. diff --git a/libclingo-dl/clingo-dl/impl/util.hh b/libclingo-dl/clingo-dl/impl/util.hh index e5f85492..5cc35752 100644 --- a/libclingo-dl/clingo-dl/impl/util.hh +++ b/libclingo-dl/clingo-dl/impl/util.hh @@ -22,11 +22,12 @@ // // }}} +#define CLINGODL_UTIL_IMPL #include namespace std { -inline size_t hash>::operator()(std::pair const &p) const { +inline auto hash>::operator()(std::pair const &p) const -> size_t { return static_cast(p.first) + (static_cast(p.second) >> 32); // NOLINT } @@ -37,26 +38,22 @@ namespace ClingoDL { namespace Detail { //! Check if casting a signed to a signed integer preserves the number. -template -using int_type = std::integral_constant; -template -inline void nc_check(S s, int_type<0> t) { // same sign +template using int_type = std::integral_constant; +template inline void nc_check(S s, int_type<0> t) { // same sign static_cast(s); static_cast(t); assert((std::is_same_v) || (s >= std::numeric_limits::min() && s <= std::numeric_limits::max())); } //! Check if casting a signed to an unsigned integer preserves the number. -template -inline void nc_check(S s, int_type<-1> t) { // Signed -> Unsigned +template inline void nc_check(S s, int_type<-1> t) { // Signed -> Unsigned static_cast(s); static_cast(t); assert(s >= 0 && static_cast(static_cast(s)) == s); } //! Check if casting an unsigned to a signed integer preserves the number. -template -inline void nc_check(S s, int_type<1> t) { // Unsigned -> Signed +template inline void nc_check(S s, int_type<1> t) { // Unsigned -> Signed static_cast(s); static_cast(t); assert(!(s > static_cast>(std::numeric_limits::max()))); @@ -64,15 +61,13 @@ inline void nc_check(S s, int_type<1> t) { // Unsigned -> Signed } // namespace Detail -template -inline T numeric_cast(S s) { +template inline auto numeric_cast(S s) -> T { constexpr int sv = int(std::numeric_limits::is_signed) - int(std::numeric_limits::is_signed); Detail::nc_check(s, Detail::int_type()); return static_cast(s); } -template -std::ostream &operator<<(std::ostream &out, std::vector const &vec) { +template auto operator<<(std::ostream &out, std::vector const &vec) -> std::ostream & { out << "{"; for (auto &x : vec) { out << " " << x; @@ -81,8 +76,7 @@ std::ostream &operator<<(std::ostream &out, std::vector const &vec) { return out; } -template -std::ostream &operator<<(std::ostream &out, std::unordered_map const &map) { +template auto operator<<(std::ostream &out, std::unordered_map const &map) -> std::ostream & { using T = std::pair; std::vector vec; vec.assign(map.begin(), map.end()); @@ -91,22 +85,18 @@ std::ostream &operator<<(std::ostream &out, std::unordered_map const &map) return out; } -template -std::ostream &operator<<(std::ostream &out, std::pair const &pair) { +template auto operator<<(std::ostream &out, std::pair const &pair) -> std::ostream & { out << "( " << pair.first << " " << pair.second << " )"; return out; } -template -void ensure_index(C &c, size_t index) { +template void ensure_index(C &c, size_t index) { if (index >= c.size()) { c.resize(index + 1); } } -inline Timer::Timer(Duration &elapsed) - : elapsed_(elapsed) - , start_(std::chrono::steady_clock::now()) {} +inline Timer::Timer(Duration &elapsed) : elapsed_(elapsed), start_(std::chrono::steady_clock::now()) {} inline void Timer::stop() { if (!stopped_) { @@ -115,22 +105,15 @@ inline void Timer::stop() { } } -inline Timer::~Timer() { - stop(); -} - +inline Timer::~Timer() { stop(); } -template -template -void Heap::push(M &m, index_type item) { +template template void Heap::push(M &m, index_type item) { m.offset(item) = size(); heap_.push_back(item); decrease(m, item); } -template -template -auto Heap::pop(M &m) -> index_type { +template template auto Heap::pop(M &m) -> index_type { assert(!heap_.empty()); auto ret = heap_[0]; if (size() > 1) { @@ -138,32 +121,26 @@ auto Heap::pop(M &m) -> index_type { m.offset(heap_[0]) = 0; heap_.pop_back(); increase(m, heap_[0]); - } - else { + } else { heap_.pop_back(); } return ret; } -template -template -void Heap::decrease(M &m, index_type item) { +template template void Heap::decrease(M &m, index_type item) { auto i = m.offset(item); while (i > 0) { index_type p = parent_(i); if (less_(m, i, p)) { swap_(m, i, p); i = p; - } - else { + } else { break; } } } -template -template -void Heap::increase(M &m, index_type item) { +template template void Heap::increase(M &m, index_type item) { auto i = m.offset(item); for (index_type p = i, j = children_(p), s = size(); j < s; j = children_(p)) { index_type min = j; @@ -175,58 +152,38 @@ void Heap::increase(M &m, index_type item) { if (less_(m, min, p)) { swap_(m, min, p); p = min; - } - else { + } else { return; } } } -template -auto Heap::size() -> size_type { - return numeric_cast(heap_.size()); -} +template auto Heap::size() -> size_type { return numeric_cast(heap_.size()); } -template -bool Heap::empty() { - return heap_.empty(); -} +template auto Heap::empty() -> bool { return heap_.empty(); } -template -void Heap::clear() { heap_.clear(); } +template void Heap::clear() { heap_.clear(); } -template -template -void Heap::swap_(M &m, index_type i, index_type j) { +template template void Heap::swap_(M &m, index_type i, index_type j) { m.offset(heap_[j]) = i; m.offset(heap_[i]) = j; std::swap(heap_[i], heap_[j]); } -template -auto Heap::parent_(index_type offset) -> index_type { - return (offset - 1) / N; -} +template auto Heap::parent_(index_type offset) -> index_type { return (offset - 1) / N; } -template -auto Heap::children_(index_type offset) -> index_type { - return N * offset + 1; -} +template auto Heap::children_(index_type offset) -> index_type { return N * offset + 1; } -template -template -bool Heap::less_(M &m, index_type a, index_type b) { +template template auto Heap::less_(M &m, index_type a, index_type b) -> bool { return m.less(heap_[a], heap_[b]); } -template , int>> -Int safe_add(Int a, Int b) { +template , int>> auto safe_add(Int a, Int b) -> Int { if (b > 0) { if (a > std::numeric_limits::max() - b) { throw std::overflow_error("integer overflow"); } - } - else if (b < 0) { + } else if (b < 0) { if (a < std::numeric_limits::min() - b) { throw std::underflow_error("integer underflow"); } @@ -235,18 +192,16 @@ Int safe_add(Int a, Int b) { } template , int>> -Float safe_add(Float a, Float b) { +auto safe_add(Float a, Float b) -> Float { return a + b; } -template , int>> -Int safe_sub(Int a, Int b) { +template , int>> auto safe_sub(Int a, Int b) -> Int { if (b > 0) { if (a < std::numeric_limits::min() + b) { throw std::underflow_error("integer underflow"); } - } - else if (b < 0) { + } else if (b < 0) { if (a > std::numeric_limits::max() + b) { throw std::overflow_error("integer overflow"); } @@ -255,19 +210,17 @@ Int safe_sub(Int a, Int b) { } template , int>> -Float safe_sub(Float a, Float b) { +auto safe_sub(Float a, Float b) -> Float { return a - b; } -template , int>> -Int safe_mul(Int a, Int b) { +template , int>> auto safe_mul(Int a, Int b) -> Int { if (a > 0) { if (b > 0) { if (a > (std::numeric_limits::max() / b)) { throw std::overflow_error("integer overflow"); } - } - else if (b < (std::numeric_limits::min() / a)) { + } else if (b < (std::numeric_limits::min() / a)) { throw std::underflow_error("integer underflow"); } } else { @@ -283,12 +236,11 @@ Int safe_mul(Int a, Int b) { } template , int>> -Float safe_mul(Float a, Float b) { +auto safe_mul(Float a, Float b) -> Float { return a * b; } -template , int>> -Int safe_div(Int a, Int b) { +template , int>> auto safe_div(Int a, Int b) -> Int { if (a == std::numeric_limits::min() && b == -1) { throw std::overflow_error("integer overflow"); } @@ -302,12 +254,11 @@ Int safe_div(Int a, Int b) { } template , int>> -Float safe_div(Float a, Float b) { +auto safe_div(Float a, Float b) -> Float { return a / b; } -template , int>> -Int safe_mod(Int a, Int b) { +template , int>> auto safe_mod(Int a, Int b) -> Int { if (a == std::numeric_limits::min() && b == -1) { throw std::overflow_error("integer overflow"); } @@ -321,25 +272,22 @@ Int safe_mod(Int a, Int b) { } template , int>> -Float safe_mod(Float a, Float b) { - return fmod(a,b); +auto safe_mod(Float a, Float b) -> Float { + return fmod(a, b); } -template , int>> -Int safe_inv(Int a) { +template , int>> auto safe_inv(Int a) -> Int { if (a == std::numeric_limits::min()) { throw std::overflow_error("integer overflow"); } return -a; } -template , int>> -Float safe_inv(Float a) { +template , int>> auto safe_inv(Float a) -> Float { return -a; } -template , int>> -Int safe_pow(Int a, Int b) { +template , int>> auto safe_pow(Int a, Int b) -> Int { if (a == 0) { throw std::overflow_error("integer overflow"); } @@ -354,11 +302,11 @@ Int safe_pow(Int a, Int b) { } template , int>> -Float safe_pow(Float a, Float b) { - return std::pow(a,b); +auto safe_pow(Float a, Float b) -> Float { + return std::pow(a, b); } -inline std::string unquote(char const* str) { +inline auto unquote(char const *str) -> std::string { std::string res; bool slash = false; for (char const *it = *str == '"' ? str + 1 : str; *it != '\0'; ++it) { // NOLINT @@ -382,10 +330,14 @@ inline std::string unquote(char const* str) { } } slash = false; + } else if (*it == '"' && *(it + 1) == '\0') { + break; + } // NOLINT + else if (*it == '\\') { + slash = true; + } else { + res.push_back(*it); } - else if (*it == '"' && *(it + 1) == '\0') { break; } // NOLINT - else if (*it == '\\') { slash = true; } - else { res.push_back(*it); } } return res; } diff --git a/libclingo-dl/clingo-dl/parsing.hh b/libclingo-dl/clingo-dl/parsing.hh index 6904efe4..17d205da 100644 --- a/libclingo-dl/clingo-dl/parsing.hh +++ b/libclingo-dl/clingo-dl/parsing.hh @@ -25,8 +25,8 @@ #ifndef CLINGODL_PARSING_HH #define CLINGODL_PARSING_HH -#include #include +#include namespace ClingoDL { @@ -44,8 +44,7 @@ term { }.)"; //! Throw a syntax error with the given message. -template -inline T throw_syntax_error(char const *message = "Invalid Syntax") { +template inline auto throw_syntax_error(char const *message = "Invalid Syntax") -> T { throw std::runtime_error(message); } @@ -67,11 +66,12 @@ using NodeCallback = std::function; void transform(Clingo::AST::Node const &ast, NodeCallback const &cb, bool shift); //! Return true if the given theory term matches the given signature. -[[nodiscard]] bool match(Clingo::TheoryTerm const &term, char const *name, size_t arity); +[[nodiscard]] auto match(Clingo::TheoryTerm const &term, char const *name, size_t arity) -> bool; //! Parse a theory atom for a difference constraint. template -[[nodiscard]] EdgeAtom parse(Clingo::TheoryAtom const &atom, std::function const &map_vert); +[[nodiscard]] auto parse(Clingo::TheoryAtom const &atom, std::function const &map_vert) + -> EdgeAtom; } // namespace ClingoDL diff --git a/libclingo-dl/clingo-dl/propagator.hh b/libclingo-dl/clingo-dl/propagator.hh index 701b0893..b1eff006 100644 --- a/libclingo-dl/clingo-dl/propagator.hh +++ b/libclingo-dl/clingo-dl/propagator.hh @@ -25,10 +25,10 @@ #ifndef CLINGODL_PROPAGATOR_HH #define CLINGODL_PROPAGATOR_HH -#include -#include -#include #include +#include +#include +#include #include @@ -56,29 +56,28 @@ struct Statistics { }; //! A propagator for difference constraints. -template -class DLPropagator : public Clingo::Heuristic { -public: +template class DLPropagator : public Clingo::Heuristic { + public: using value_t = T; // construction DLPropagator(Statistics &stats, PropagatorConfig conf); DLPropagator(DLPropagator const &other) = delete; DLPropagator(DLPropagator &&other) = delete; - DLPropagator &operator=(DLPropagator const &other) = delete; - DLPropagator &operator=(DLPropagator &&other) = delete; + auto operator=(DLPropagator const &other) -> DLPropagator & = delete; + auto operator=(DLPropagator &&other) -> DLPropagator & = delete; ~DLPropagator() override; //! Get the number of vertices in the graph. - [[nodiscard]] vertex_t num_vertices() const; + [[nodiscard]] auto num_vertices() const -> vertex_t; //! Get the symbol associated with a vertex index. - [[nodiscard]] Clingo::Symbol symbol(vertex_t index) const; + [[nodiscard]] auto symbol(vertex_t index) const -> Clingo::Symbol; //! Lookup the index of a vertex. - vertex_t lookup(Clingo::Symbol symbol); + auto lookup(Clingo::Symbol symbol) -> vertex_t; //! Check if the given vertex has a lower bound in the given thread. - [[nodiscard]] bool has_lower_bound(Clingo::id_t thread_id, vertex_t index) const; + [[nodiscard]] auto has_lower_bound(Clingo::id_t thread_id, vertex_t index) const -> bool; //! Get the lower bound of a vertex in the given thread. - [[nodiscard]] value_t lower_bound(Clingo::id_t thread_id, vertex_t index) const; + [[nodiscard]] auto lower_bound(Clingo::id_t thread_id, vertex_t index) const -> value_t; //! Extend the model with vertex assignments. void extend_model(Clingo::Model &model); @@ -94,8 +93,9 @@ public: // heuristic interface //! Customize the decision heuristic. - literal_t decide(id_t thread_id, Clingo::Assignment const &assign, literal_t fallback) override; -private: + auto decide(id_t thread_id, Clingo::Assignment const &assign, literal_t fallback) -> literal_t override; + + private: struct VertexInfo; struct ThreadState; struct FactState; @@ -113,23 +113,26 @@ private: // initialization functions //! Map a symbol to an integer. - vertex_t map_vertex_(Clingo::Symbol symbol); + auto map_vertex_(Clingo::Symbol symbol) -> vertex_t; //! Add constraints in the theory data. - [[nodiscard]] bool add_constraints_(Clingo::PropagateInit &init); + [[nodiscard]] auto add_constraints_(Clingo::PropagateInit &init) -> bool; //! Normalize constraints to individual edges over `<=`. - [[nodiscard]] bool normalize_constraint_(Clingo::PropagateInit &init, literal_t literal, CoVarVec const &elements, char const *op, value_t rhs, bool strict); + [[nodiscard]] auto normalize_constraint_(Clingo::PropagateInit &init, literal_t literal, CoVarVec const &elements, + char const *op, value_t rhs, bool strict) -> bool; //! Add up to two edges for the given constraint if the has at most 2 variables and suitable coefficients. - [[nodiscard]] bool add_edges_(Clingo::PropagateInit& init, literal_t literal, CoVarVec const &covec, value_t rhs, bool strict); + [[nodiscard]] auto add_edges_(Clingo::PropagateInit &init, literal_t literal, CoVarVec const &covec, value_t rhs, + bool strict) -> bool; //! Add up to two edges for a constraint. - void add_edges_(Clingo::PropagateInit& init, vertex_t u_id, vertex_t v_id, value_t weight, literal_t lit, bool strict); + void add_edges_(Clingo::PropagateInit &init, vertex_t u_id, vertex_t v_id, value_t weight, literal_t lit, + bool strict); //! Add (up to one) edge for a constraint. void add_edge_(Clingo::PropagateInit &init, vertex_t u_id, vertex_t v_id, value_t weight, literal_t lit); //! Reset connected components (to be recalculated with the next call to cc_calculate_). void cc_reset_(); //! Mark a vertex in a component as visited. - [[nodiscard]] bool cc_visited_(vertex_t index) const; + [[nodiscard]] auto cc_visited_(vertex_t index) const -> bool; //! Check if the given vertex is a zero vertex. - [[nodiscard]] bool is_zero_(vertex_t index) const; + [[nodiscard]] auto is_zero_(vertex_t index) const -> bool; //! Calculate the connected components. void cc_calculate_(AdjacencyMap &outgoing, AdjacencyMap &incoming); //! Calculate mutually exclusive edges. @@ -141,11 +144,11 @@ private: //! Disable all edges associated with the given literal in the thread state. void disable_edge_by_lit(ThreadState &state, literal_t lit); //! Compute the current potential of a vertex in the given graph. - [[nodiscard]] value_t get_potential_(Graph const &graph, vertex_t index) const; + [[nodiscard]] auto get_potential_(Graph const &graph, vertex_t index) const -> value_t; //! Compute the current cost of a vertex in the given graph. - [[nodiscard]] value_t cost_(Graph const &graph, Edge const &edge) const; + [[nodiscard]] auto cost_(Graph const &graph, Edge const &edge) const -> value_t; //! Compute a weight to sort vertices before propagation. - [[nodiscard]] value_t cost_(SortMode mode, Graph const &graph, edge_t index) const; + [[nodiscard]] auto cost_(SortMode mode, Graph const &graph, edge_t index) const -> value_t; //! Sort vertices in the propagation queue according to the given mode. void sort_edges(SortMode mode, ThreadState &state); //! Propagate the given literals. diff --git a/libclingo-dl/clingo-dl/theory.hh b/libclingo-dl/clingo-dl/theory.hh index 9309cf13..94b2484c 100644 --- a/libclingo-dl/clingo-dl/theory.hh +++ b/libclingo-dl/clingo-dl/theory.hh @@ -45,12 +45,10 @@ using level_t = uint32_t; using index_t = uint32_t; //! Vector of coefficients and variables. -template -using CoVarVec = std::vector>; +template using CoVarVec = std::vector>; //! An edge in the difference logic graph. -template -struct EdgeAtom { +template struct EdgeAtom { CoVarVec lhs; //!< The terms associated with the atom. char const *rel; //!< The comparision relation of the atom. T rhs; //!< The value on the right hand side. @@ -59,9 +57,8 @@ struct EdgeAtom { }; //! Epsilon value depending on number type. -template -[[nodiscard]] T epsilon(); +template [[nodiscard]] auto epsilon() -> T; -} // namespace +} // namespace ClingoDL #endif diff --git a/libclingo-dl/clingo-dl/util.hh b/libclingo-dl/clingo-dl/util.hh index fcabf7ba..85afbbf3 100644 --- a/libclingo-dl/clingo-dl/util.hh +++ b/libclingo-dl/clingo-dl/util.hh @@ -25,20 +25,19 @@ #ifndef CLINGODL_UTIL_HH #define CLINGODL_UTIL_HH +#include +#include #include +#include #include #include #include -#include -#include -#include namespace std { //! Specialization to compute hashes for pairs. -template<> -struct hash> { - size_t operator()(std::pair const &p) const; +template <> struct hash> { + auto operator()(std::pair const &p) const -> size_t; }; } // namespace std @@ -47,44 +46,39 @@ namespace ClingoDL { //! A cast for integrals that causes an assertion if the target type cannot //! represent the number. -template -inline T numeric_cast(S s); +template inline auto numeric_cast(S s) -> T; //! Helper to print unordered maps. -template -std::ostream &operator<<(std::ostream &out, std::unordered_map const &map); +template auto operator<<(std::ostream &out, std::unordered_map const &map) -> std::ostream &; //! Helper to print vectors. -template -std::ostream &operator<<(std::ostream &out, std::vector const &vec); +template auto operator<<(std::ostream &out, std::vector const &vec) -> std::ostream &; //! Helper to print pairs. -template -std::ostream &operator<<(std::ostream &out, std::pair const &pair); +template auto operator<<(std::ostream &out, std::pair const &pair) -> std::ostream &; //! Helper to ensure that a resizable container can hold the given index. -template -void ensure_index(C &c, size_t index); +template void ensure_index(C &c, size_t index); //! Duration used by the Timer class. using Duration = std::chrono::duration; //! Simple timer class to measure durations. class Timer { -private: + private: //! Data type for time points. using TimePoint = std::chrono::time_point; -public: + public: //! The constructor expects a reference to a duration which is incremented //! by the lifetime of the timer. Timer(Duration &elapsed); Timer(Timer const &other) = delete; Timer(Timer &&other) = delete; - Timer &operator=(Timer const &other) = delete; - Timer &operator=(Timer &&other) = delete; + auto operator=(Timer const &other) -> Timer & = delete; + auto operator=(Timer &&other) -> Timer & = delete; void stop(); ~Timer(); -private: + private: Duration &elapsed_; //!< The duration to increment. TimePoint start_; //!< The time when the timer was started. bool stopped_{false}; //!< Whether the timer has been stopped. @@ -94,44 +88,37 @@ private: //! //! The heap stores indices and each member function takes a struct as argument //! to get its current cost and set it's offset/index in the heap. -template -class Heap { -public: +template class Heap { + public: //! We use 32bit integers for indexing. using index_type = uint32_t; //! We use 32bit integers for sizes. using size_type = uint32_t; //! Add an element to the heap. - template - void push(M &m, index_type item); + template void push(M &m, index_type item); //! Remove the element with the lowest cost. - template - index_type pop(M &m); + template auto pop(M &m) -> index_type; //! Update an element after it's cost has been decreased. - template - void decrease(M &m, index_type item); + template void decrease(M &m, index_type item); //! Update an element after it's cost has been increased. - template - void increase(M &m, index_type item); + template void increase(M &m, index_type item); //! Get the number of elements in the heap. - size_type size(); + auto size() -> size_type; //! Test if the heap is empty. - bool empty(); + auto empty() -> bool; //! Remove all elements from the heap. void clear(); -private: + private: //! Swap to elements in the heap. - template - void swap_(M &m, index_type i, index_type j); + template void swap_(M &m, index_type i, index_type j); //! Get the parent index of an element. - index_type parent_(index_type offset); + auto parent_(index_type offset) -> index_type; //! Get the index of the left most child of an element in the heap. - index_type children_(index_type offset); + auto children_(index_type offset) -> index_type; //! Compare two elements by costs preferring relevant elements if the costs //! are equal. - template - bool less_(M &m, index_type a, index_type b); + template auto less_(M &m, index_type a, index_type b) -> bool; //! The vector storing the elements. std::vector heap_; @@ -140,73 +127,68 @@ private: // Some of the functions below could also be implemented using (much faster) // compiler specific built-ins. For more information check the following links: // - https://gcc.gnu.org/onlinedocs/gcc/Integer-Overflow-Builtins.html -// - https://wiki.sei.cmu.edu/confluence/display/c/INT32-C.+Ensure+that+operations+on+signed+integers+do+not+result+in+overflow +// - +// https://wiki.sei.cmu.edu/confluence/display/c/INT32-C.+Ensure+that+operations+on+signed+integers+do+not+result+in+overflow //! Safely add a and b throwing an exception in case of overflow/underflow. -template , int> = 0> -Int safe_add(Int a, Int b); +template , int> = 0> auto safe_add(Int a, Int b) -> Int; //! Add floating point numbers without specific overflow checking. template , int> = 0> -Float safe_add(Float a, Float b); +auto safe_add(Float a, Float b) -> Float; //! Safely subtract a and b throwing an exception in case of //! overflow/underflow. -template , int> = 0> -Int safe_sub(Int a, Int b); +template , int> = 0> auto safe_sub(Int a, Int b) -> Int; //! Subtract floating point numbers without specific overflow checking. template , int> = 0> -Float safe_sub(Float a, Float b); +auto safe_sub(Float a, Float b) -> Float; //! Safely multiply a and b throwing an exception in case of //! overflow/underflow. -template , int> = 0> -Int safe_mul(Int a, Int b); +template , int> = 0> auto safe_mul(Int a, Int b) -> Int; //! Multiply floating point numbers without specific overflow checking. template , int> = 0> -Float safe_mul(Float a, Float b); +auto safe_mul(Float a, Float b) -> Float; //! Safely divide a and b throwing an exception in case of overflow/underflow. -template , int> = 0> -Int safe_div(Int a, Int b); +template , int> = 0> auto safe_div(Int a, Int b) -> Int; //! Divide floating point numbers without specific overflow checking. template , int> = 0> -Float safe_div(Float a, Float b); +auto safe_div(Float a, Float b) -> Float; //! Safely calculate the modulo of a and b throwing an exception in case of //! overflow/underflow. -template , int> = 0> -Int safe_mod(Int a, Int b); +template , int> = 0> auto safe_mod(Int a, Int b) -> Int; //! Compute the modulo for floating point numbers without specific overflow checking. template , int> = 0> -Float safe_mod(Float a, Float b); +auto safe_mod(Float a, Float b) -> Float; //! Safely invert a throwing an exception in case of an underflow. -template , int> = 0> -Int safe_inv(Int a); +template , int> = 0> auto safe_inv(Int a) -> Int; //! Invert a floating point number without specific overflow checking. -template , int> = 0> -Float safe_inv(Float a); +template , int> = 0> auto safe_inv(Float a) -> Float; //! Safely exponentiate a and b throwing an exception in case of //! overflow/underflow. -template , int> = 0> -Int safe_pow(Int a, Int b); +template , int> = 0> auto safe_pow(Int a, Int b) -> Int; //! Exponentiate floating point numbers without specific overflow checking. template , int> = 0> -Float safe_pow(Float a, Float b); +auto safe_pow(Float a, Float b) -> Float; //! Restores quoted characters in the given string. -std::string unquote(char const* str); +auto unquote(char const *str) -> std::string; } // namespace ClingoDL +#ifndef CLINGODL_UTIL_IMPL #include +#endif #endif // CLINGODL_UTIL_HH diff --git a/libclingo-dl/src/clingo-dl.cc b/libclingo-dl/src/clingo-dl.cc index 2b26188d..708d8d79 100644 --- a/libclingo-dl/src/clingo-dl.cc +++ b/libclingo-dl/src/clingo-dl.cc @@ -30,7 +30,12 @@ #include #define CLINGODL_TRY try // NOLINT -#define CLINGODL_CATCH catch (...){ Clingo::Detail::handle_cxx_error(); return false; } return true // NOLINT +#define CLINGODL_CATCH \ + catch (...) { \ + Clingo::Detail::handle_cxx_error(); \ + return false; \ + } \ + return true // NOLINT using namespace ClingoDL; @@ -39,81 +44,80 @@ namespace { using Clingo::Detail::handle_error; //! C initialization callback for the DL propagator. -template -bool init(clingo_propagate_init_t* i, void* data) { +template auto init(clingo_propagate_init_t *i, void *data) -> bool { CLINGODL_TRY { Clingo::PropagateInit in(i); - static_cast*>(data)->init(in); + static_cast *>(data)->init(in); } CLINGODL_CATCH; } //! C propagation callback for the DL propagator. template -bool propagate(clingo_propagate_control_t* i, const clingo_literal_t *changes, size_t size, void* data) { +auto propagate(clingo_propagate_control_t *i, const clingo_literal_t *changes, size_t size, void *data) -> bool { CLINGODL_TRY { Clingo::PropagateControl in(i); - static_cast*>(data)->propagate(in, {changes, size}); + static_cast *>(data)->propagate(in, {changes, size}); } CLINGODL_CATCH; } //! C undo callback for the DL propagator. template -void undo(clingo_propagate_control_t const* i, const clingo_literal_t *changes, size_t size, void* data) { +void undo(clingo_propagate_control_t const *i, const clingo_literal_t *changes, size_t size, void *data) { Clingo::PropagateControl in(const_cast(i)); // NOLINT - static_cast*>(data)->undo(in, {changes, size}); + static_cast *>(data)->undo(in, {changes, size}); } //! C check callback for the DL propagator. -template -bool check(clingo_propagate_control_t* i, void* data) { +template auto check(clingo_propagate_control_t *i, void *data) -> bool { CLINGODL_TRY { Clingo::PropagateControl in(i); - static_cast*>(data)->check(in); + static_cast *>(data)->check(in); } CLINGODL_CATCH; } //! C decide callback for the DL heuristic. template -bool decide(clingo_id_t thread_id, clingo_assignment_t const *assignment, clingo_literal_t fallback, void *data, clingo_literal_t *decision) { +auto decide(clingo_id_t thread_id, clingo_assignment_t const *assignment, clingo_literal_t fallback, void *data, + clingo_literal_t *decision) -> bool { CLINGODL_TRY { Clingo::Assignment ass(assignment); - *decision = static_cast*>(data)->decide(thread_id, ass, fallback); + *decision = static_cast *>(data)->decide(thread_id, ass, fallback); } CLINGODL_CATCH; } //! High level interface to use the DL propagator hiding the value type. class PropagatorFacade { -public: + public: PropagatorFacade() = default; PropagatorFacade(PropagatorFacade const &other) = default; PropagatorFacade(PropagatorFacade &&other) = default; - PropagatorFacade &operator=(PropagatorFacade const &other) = default; - PropagatorFacade &operator=(PropagatorFacade &&other) noexcept = default; + auto operator=(PropagatorFacade const &other) -> PropagatorFacade & = default; + auto operator=(PropagatorFacade &&other) noexcept -> PropagatorFacade & = default; virtual ~PropagatorFacade() = default; //! Look up the index of a symbol. //! //! The function returns false if the symbol could not be found. - virtual bool lookup_symbol(clingo_symbol_t name, size_t *index) = 0; + virtual auto lookup_symbol(clingo_symbol_t name, size_t *index) -> bool = 0; //! Get the symbol associated with an index. - virtual clingo_symbol_t get_symbol(size_t index) = 0; + virtual auto get_symbol(size_t index) -> clingo_symbol_t = 0; //! Check if a symbol has a value in a thread. - virtual bool has_value(uint32_t thread_id, size_t index) = 0; + virtual auto has_value(uint32_t thread_id, size_t index) -> bool = 0; //! Get the value of a symbol in a thread. virtual void get_value(uint32_t thread_id, size_t index, clingodl_value_t *value) = 0; //! Function to iterato over the thread specific assignment of symbols and values. //! //! Argument current should initially be set to 0. The function returns //! false if no more values are available. - virtual bool next(uint32_t thread_id, size_t *current) = 0; + virtual auto next(uint32_t thread_id, size_t *current) -> bool = 0; //! Extend the given model with the assignment stored in the propagator. virtual void extend_model(Clingo::Model &m) = 0; //! Add the propagator statistics to clingo's statistics. - virtual void on_statistics(Clingo::UserStatistics& step, Clingo::UserStatistics &accu) = 0; + virtual void on_statistics(Clingo::UserStatistics &step, Clingo::UserStatistics &accu) = 0; }; //! Set variant to an integer value. @@ -129,32 +133,25 @@ void set_value(clingodl_value_t *variant, double value) { } //! High level interface to use the DL propagator. -template -class DLPropagatorFacade : public PropagatorFacade { -public: - DLPropagatorFacade(clingo_control_t *control, PropagatorConfig const &conf) - : prop_{step_, conf} { +template class DLPropagatorFacade : public PropagatorFacade { + public: + DLPropagatorFacade(clingo_control_t *control, PropagatorConfig const &conf) : prop_{step_, conf} { handle_error(clingo_control_add(control, "base", nullptr, 0, THEORY)); - static clingo_propagator_t prop = { - init, - propagate, - undo, - check, - conf.decision_mode != DecisionMode::Disabled ? decide : nullptr - }; + static clingo_propagator_t prop = {init, propagate, undo, check, + conf.decision_mode != DecisionMode::Disabled ? decide : nullptr}; handle_error(clingo_control_register_propagator(control, &prop, &prop_, false)); } - bool lookup_symbol(clingo_symbol_t name, size_t *index) override { + auto lookup_symbol(clingo_symbol_t name, size_t *index) -> bool override { *index = prop_.lookup(Clingo::Symbol{name}) + 1; return *index <= prop_.num_vertices(); } - clingo_symbol_t get_symbol(size_t index) override { + auto get_symbol(size_t index) -> clingo_symbol_t override { return prop_.symbol(numeric_cast(index - 1)).to_c(); } - bool has_value(uint32_t thread_id, size_t index) override { + auto has_value(uint32_t thread_id, size_t index) -> bool override { return prop_.has_lower_bound(thread_id, numeric_cast(index - 1)); } @@ -163,7 +160,7 @@ class DLPropagatorFacade : public PropagatorFacade { set_value(value, prop_.lower_bound(thread_id, numeric_cast(index - 1))); } - bool next(uint32_t thread_id, size_t *current) override { + auto next(uint32_t thread_id, size_t *current) -> bool override { for (++*current; *current <= prop_.num_vertices(); ++*current) { if (prop_.has_lower_bound(thread_id, numeric_cast(*current - 1))) { return true; @@ -172,18 +169,16 @@ class DLPropagatorFacade : public PropagatorFacade { return false; } - void extend_model(Clingo::Model &m) override { - prop_.extend_model(m); - } + void extend_model(Clingo::Model &m) override { prop_.extend_model(m); } - void on_statistics(Clingo::UserStatistics& step, Clingo::UserStatistics &accu) override { + void on_statistics(Clingo::UserStatistics &step, Clingo::UserStatistics &accu) override { accu_.accu(step_); add_statistics_(step, step_); add_statistics_(accu, accu_); step_.reset(); } -private: + private: //! Add an integral value to the statistics. template , bool> = true> static void add_subkey_(Clingo::UserStatistics &root, char const *name, V value) { @@ -196,7 +191,7 @@ class DLPropagatorFacade : public PropagatorFacade { } //!< Helper function to add the DL statistics to clingo's statistics. - void add_statistics_(Clingo::UserStatistics& root, Statistics const &stats) { + void add_statistics_(Clingo::UserStatistics &root, Statistics const &stats) { Clingo::UserStatistics diff = root.add_subkey("DifferenceLogic", Clingo::StatisticsType::Map); add_subkey_(diff, "Time init(s)", stats.time_init.count()); add_subkey_(diff, "CCs", stats.ccs); @@ -231,15 +226,17 @@ class DLPropagatorFacade : public PropagatorFacade { }; //! Check if b is a lower case prefix of a returning a pointer to the remainder of a. -char const *iequals_pre(char const *a, char const *b) { +auto iequals_pre(char const *a, char const *b) -> char const * { for (; *a && *b; ++a, ++b) { // NOLINT - if (tolower(*a) != tolower(*b)) { return nullptr; } + if (tolower(*a) != tolower(*b)) { + return nullptr; + } } return *b != '\0' ? nullptr : a; } //! Check if two strings are lower case equal. -bool iequals(char const *a, char const *b) { +auto iequals(char const *a, char const *b) -> bool { a = iequals_pre(a, b); return a != nullptr && *a == '\0'; } @@ -248,8 +245,8 @@ bool iequals(char const *a, char const *b) { //! //! The function returns a nullpointer if there are no leading digits. The //! result is stored in data which is assumed to be a pointer to an uint64_t. -char const *parse_uint64_pre(const char *value, void *data) { - auto &res = *static_cast(data); +auto parse_uint64_pre(const char *value, void *data) -> char const * { + auto &res = *static_cast(data); char const *it = value; res = 0; @@ -258,9 +255,12 @@ char const *parse_uint64_pre(const char *value, void *data) { auto tmp = res; res *= 10; // NOLINT res += *it - '0'; - if (res < tmp) { return nullptr; } + if (res < tmp) { + return nullptr; + } + } else { + break; } - else { break; } } return value != it ? it : nullptr; @@ -268,7 +268,7 @@ char const *parse_uint64_pre(const char *value, void *data) { //! Turn the value into an uint64_t assuming that data is a pointer to an //! uint64_t. -bool parse_uint64(const char *value, void *data) { +auto parse_uint64(const char *value, void *data) -> bool { value = parse_uint64_pre(value, data); return value != nullptr && *value == '\0'; } @@ -276,10 +276,9 @@ bool parse_uint64(const char *value, void *data) { //! Parse thread-specific option via a callback. //! //! The thread number is optional and can follow separated with a comma. -template -bool set_config(char const *value, void *data, F f, G g) { +template auto set_config(char const *value, void *data, F f, G g) -> bool { try { - auto &config = *static_cast(data); + auto &config = *static_cast(data); uint64_t id = 0; if (*value == '\0') { f(config); @@ -289,45 +288,51 @@ bool set_config(char const *value, void *data, F f, G g) { g(config.ensure(id)); return true; } + } catch (...) { } - catch (...) { } return false; } //! Parse a level to limit full propagation. //! //! Return false if there is a parse error. -bool parse_root(const char *value, void *data) { +auto parse_root(const char *value, void *data) -> bool { uint64_t x = 0; - return (value = parse_uint64_pre(value, &x)) != nullptr && set_config(value, data, - [x](PropagatorConfig &config) { config.propagate_root = x; }, - [x](ThreadConfig &config) { config.propagate_root = x; }); + return (value = parse_uint64_pre(value, &x)) != nullptr && + set_config( + value, data, [x](PropagatorConfig &config) { config.propagate_root = x; }, + [x](ThreadConfig &config) { config.propagate_root = x; }); } //! Parse the propagation budget and store it data. //! //! Return false if there is a parse error. -bool parse_budget(const char *value, void *data) { +auto parse_budget(const char *value, void *data) -> bool { uint64_t x = 0; - return (value = parse_uint64_pre(value, &x)) != nullptr && set_config(value, data, - [x](PropagatorConfig &config) { config.propagate_budget = x; }, - [x](ThreadConfig &config) { config.propagate_budget = x; }); + return (value = parse_uint64_pre(value, &x)) != nullptr && + set_config( + value, data, [x](PropagatorConfig &config) { config.propagate_budget = x; }, + [x](ThreadConfig &config) { config.propagate_budget = x; }); } //! Parse the mutex detection mode and store it data. //! //! Return false if there is a parse error. -bool parse_mutex(const char *value, void *data) { - auto &pc = *static_cast(data); +auto parse_mutex(const char *value, void *data) -> bool { + auto &pc = *static_cast(data); uint64_t x = 0; - if ((value = parse_uint64_pre(value, &x)) == nullptr) { return false; } + if ((value = parse_uint64_pre(value, &x)) == nullptr) { + return false; + } pc.mutex_size = x; if (*value == '\0') { pc.mutex_cutoff = 10 * x; // NOLINT return true; } if (*value == ',') { - if (!parse_uint64(value + 1, &x)) { return false; } // NOLINT + if (!parse_uint64(value + 1, &x)) { + return false; + } // NOLINT pc.mutex_cutoff = x; } return true; @@ -336,81 +341,70 @@ bool parse_mutex(const char *value, void *data) { //! Parse the propagation mode and store it data. //! //! Return false if there is a parse error. -bool parse_mode(const char *value, void *data) { +auto parse_mode(const char *value, void *data) -> bool { PropagationMode mode = PropagationMode::Check; char const *rem = nullptr; if ((rem = iequals_pre(value, "no")) != nullptr) { mode = PropagationMode::Check; - } - else if ((rem = iequals_pre(value, "inverse")) != nullptr) { + } else if ((rem = iequals_pre(value, "inverse")) != nullptr) { mode = PropagationMode::Trivial; - } - else if ((rem = iequals_pre(value, "partial+")) != nullptr) { + } else if ((rem = iequals_pre(value, "partial+")) != nullptr) { mode = PropagationMode::WeakPlus; - } - else if ((rem = iequals_pre(value, "partial")) != nullptr) { + } else if ((rem = iequals_pre(value, "partial")) != nullptr) { mode = PropagationMode::Weak; - } - else if ((rem = iequals_pre(value, "zero")) != nullptr) { + } else if ((rem = iequals_pre(value, "zero")) != nullptr) { mode = PropagationMode::Zero; - } - else if ((rem = iequals_pre(value, "full")) != nullptr) { + } else if ((rem = iequals_pre(value, "full")) != nullptr) { mode = PropagationMode::Strong; } - return rem != nullptr && set_config(rem, data, - [mode](PropagatorConfig &config) { config.propagate_mode = mode; }, - [mode](ThreadConfig &config) { config.propagate_mode = mode; }); + return rem != nullptr && set_config( + rem, data, [mode](PropagatorConfig &config) { config.propagate_mode = mode; }, + [mode](ThreadConfig &config) { config.propagate_mode = mode; }); } //! Parse the sort mode and store it data. //! //! Return false if there is a parse error. -bool parse_sort(const char *value, void *data) { +auto parse_sort(const char *value, void *data) -> bool { SortMode sort = SortMode::Weight; char const *rem = nullptr; if ((rem = iequals_pre(value, "no")) != nullptr) { sort = SortMode::No; - } - else if ((rem = iequals_pre(value, "weight-reversed")) != nullptr) { + } else if ((rem = iequals_pre(value, "weight-reversed")) != nullptr) { sort = SortMode::WeightRev; - } - else if ((rem = iequals_pre(value, "weight")) != nullptr) { + } else if ((rem = iequals_pre(value, "weight")) != nullptr) { sort = SortMode::Weight; - } - else if ((rem = iequals_pre(value, "potential-reversed")) != nullptr) { + } else if ((rem = iequals_pre(value, "potential-reversed")) != nullptr) { sort = SortMode::PotentialRev; - } - else if ((rem = iequals_pre(value, "potential")) != nullptr) { + } else if ((rem = iequals_pre(value, "potential")) != nullptr) { sort = SortMode::Potential; } - return rem != nullptr && set_config(rem, data, - [sort](PropagatorConfig &config) { config.sort_mode = sort; }, - [sort](ThreadConfig &config) { config.sort_mode = sort; }); + return rem != nullptr && set_config( + rem, data, [sort](PropagatorConfig &config) { config.sort_mode = sort; }, + [sort](ThreadConfig &config) { config.sort_mode = sort; }); } //! Parse the decision mode. //! //! Return false if there is a parse error. -bool parse_decide(const char *value, void *data) { +auto parse_decide(const char *value, void *data) -> bool { DecisionMode mode = DecisionMode::Disabled; if (iequals(value, "no")) { mode = DecisionMode::Disabled; - } - else if (iequals(value, "min")) { + } else if (iequals(value, "min")) { mode = DecisionMode::MinConflict; - } - else if (iequals(value, "max")) { + } else if (iequals(value, "max")) { mode = DecisionMode::MaxConflict; } - static_cast(data)->decision_mode = mode; + static_cast(data)->decision_mode = mode; return true; } //! Parse a Boolean and store it in data. //! //! Return false if there is a parse error. -bool parse_bool(const char *value, void *data) { - auto &result = *static_cast(data); +auto parse_bool(const char *value, void *data) -> bool { + auto &result = *static_cast(data); if (iequals(value, "no") || iequals(value, "off") || iequals(value, "0")) { result = false; return true; @@ -425,7 +419,7 @@ bool parse_bool(const char *value, void *data) { //! Set the given error message if the Boolean is false. //! //! Return false if there is a parse error. -bool check_parse(char const *key, bool ret) { +auto check_parse(char const *key, bool ret) -> bool { if (!ret) { std::ostringstream msg; msg << "invalid value for '" << key << "'"; @@ -455,46 +449,46 @@ extern "C" void clingodl_version(int *major, int *minor, int *patch) { } } -extern "C" bool clingodl_create(clingodl_theory_t **theory) { +extern "C" auto clingodl_create(clingodl_theory_t **theory) -> bool { CLINGODL_TRY { *theory = new clingodl_theory{}; } // NOLINT CLINGODL_CATCH; } -extern "C" bool clingodl_register(clingodl_theory_t *theory, clingo_control_t* control) { +extern "C" auto clingodl_register(clingodl_theory_t *theory, clingo_control_t *control) -> bool { CLINGODL_TRY { if (!theory->rdl) { theory->clingodl = std::make_unique>(control, theory->config); - } - else { + } else { theory->clingodl = std::make_unique>(control, theory->config); } } CLINGODL_CATCH; } -extern "C" bool clingodl_rewrite_ast(clingodl_theory_t *theory, clingo_ast_t *ast, clingodl_ast_callback_t add, void *data) { +extern "C" auto clingodl_rewrite_ast(clingodl_theory_t *theory, clingo_ast_t *ast, clingodl_ast_callback_t add, + void *data) -> bool { CLINGODL_TRY { clingo_ast_acquire(ast); Clingo::AST::Node ast_cpp{ast}; - transform(ast_cpp, [add, data](Clingo::AST::Node &&ast_trans){ - handle_error(add(ast_trans.to_c(), data)); - }, theory->shift_constraints); + transform( + ast_cpp, [add, data](Clingo::AST::Node &&ast_trans) { handle_error(add(ast_trans.to_c(), data)); }, + theory->shift_constraints); } CLINGODL_CATCH; } -extern "C" bool clingodl_prepare(clingodl_theory_t *theory, clingo_control_t *control) { +extern "C" auto clingodl_prepare(clingodl_theory_t *theory, clingo_control_t *control) -> bool { static_cast(theory); static_cast(control); return true; } -extern "C" bool clingodl_destroy(clingodl_theory_t *theory) { +extern "C" auto clingodl_destroy(clingodl_theory_t *theory) -> bool { CLINGODL_TRY { delete theory; } // NOLINT CLINGODL_CATCH; } -extern "C" bool clingodl_configure(clingodl_theory_t *theory, char const *key, char const *value) { +extern "C" auto clingodl_configure(clingodl_theory_t *theory, char const *key, char const *value) -> bool { CLINGODL_TRY { if (strcmp(key, "propagate") == 0) { return check_parse("propagate", parse_mode(value, &theory->config)); @@ -531,74 +525,72 @@ extern "C" bool clingodl_configure(clingodl_theory_t *theory, char const *key, c CLINGODL_CATCH; } -extern "C" bool clingodl_register_options(clingodl_theory_t *theory, clingo_options_t* options) { +extern "C" auto clingodl_register_options(clingodl_theory_t *theory, clingo_options_t *options) -> bool { CLINGODL_TRY { - char const * group = "Clingo.DL Options"; + char const *group = "Clingo.DL Options"; handle_error(clingo_options_add(options, group, "propagate", - "Set propagation mode [no]\n" - " : {no,inverse,partial,partial+,zero,full}[,]\n" - " no : No propagation; only detect conflicts\n" - " inverse : Check inverse constraints\n" - " partial : Detect some conflicts\n" - " partial+: Detect some more conflicts\n" - " zero : Detect all immediate conflicts through zero nodes\n" - " full : Detect all immediate conflicts\n" - " : Restrict to thread", - &parse_mode, &theory->config, true, "")); + "Set propagation mode [no]\n" + " : {no,inverse,partial,partial+,zero,full}[,]\n" + " no : No propagation; only detect conflicts\n" + " inverse : Check inverse constraints\n" + " partial : Detect some conflicts\n" + " partial+: Detect some more conflicts\n" + " zero : Detect all immediate conflicts through zero nodes\n" + " full : Detect all immediate conflicts\n" + " : Restrict to thread", + &parse_mode, &theory->config, true, "")); handle_error(clingo_options_add(options, group, "propagate-root", - "Enable full propagation below decision level [0]\n" - " : [,]\n" - " : Upper bound for decision level\n" - " : Restrict to thread", - &parse_root, &theory->config, true, "")); + "Enable full propagation below decision level [0]\n" + " : [,]\n" + " : Upper bound for decision level\n" + " : Restrict to thread", + &parse_root, &theory->config, true, "")); handle_error(clingo_options_add(options, group, "propagate-budget", - "Enable full propagation limiting to budget [0]\n" - " : [,]\n" - " : Budget roughly corresponding to cost of consistency checks\n" - " (if possible use with --propagate-root greater 0)\n" - " : Restrict to thread", - &parse_budget, &theory->config, true, "")); + "Enable full propagation limiting to budget [0]\n" + " : [,]\n" + " : Budget roughly corresponding to cost of consistency checks\n" + " (if possible use with --propagate-root greater 0)\n" + " : Restrict to thread", + &parse_budget, &theory->config, true, "")); handle_error(clingo_options_add(options, group, "add-mutexes", - "Add mutexes in a preprocessing step [0]\n" - " : [,]\n" - " : Maximum size of mutexes to add\n" - " : Limit costs to calculate mutexes", - &parse_mutex, &theory->config, true, "")); + "Add mutexes in a preprocessing step [0]\n" + " : [,]\n" + " : Maximum size of mutexes to add\n" + " : Limit costs to calculate mutexes", + &parse_mutex, &theory->config, true, "")); handle_error(clingo_options_add(options, group, "sort-edges", - "Sort edges for propagation [weight]\n" - " : {no, weight, weight-reversed, potential, potential-reversed}\n" - " no : No sorting\n" - " weight : Sort by edge weight\n" - " weight-reversed : Sort by negative edge weight\n" - " potential : Sort by relative potential\n" - " potential-reversed: Sort by relative negative potential", - &parse_sort, &theory->config, true, "")); + "Sort edges for propagation [weight]\n" + " : {no, weight, weight-reversed, potential, potential-reversed}\n" + " no : No sorting\n" + " weight : Sort by edge weight\n" + " weight-reversed : Sort by negative edge weight\n" + " potential : Sort by relative potential\n" + " potential-reversed: Sort by relative negative potential", + &parse_sort, &theory->config, true, "")); handle_error(clingo_options_add(options, group, "dl-heuristic", - "Decision heuristic for difference constraints\n" - " : {none, min, max}\n" - " no : Use default decision heuristic\n" - " min: Try to minimize conflicts\n" - " max: Try to maximize conflicts", - &parse_decide, &theory->config, false, "")); - handle_error(clingo_options_add_flag(options, group, "rdl", - "Enable support for real numbers [no]", - &theory->rdl)); + "Decision heuristic for difference constraints\n" + " : {none, min, max}\n" + " no : Use default decision heuristic\n" + " min: Try to minimize conflicts\n" + " max: Try to maximize conflicts", + &parse_decide, &theory->config, false, "")); + handle_error( + clingo_options_add_flag(options, group, "rdl", "Enable support for real numbers [no]", &theory->rdl)); handle_error(clingo_options_add_flag(options, group, "shift-constraints", - "Shift constraints into head of integrity constraints [no]", - &theory->shift_constraints)); - handle_error(clingo_options_add_flag(options, group, "compute-components", - "Compute connected components [yes]", - &theory->config.calculate_cc)); + "Shift constraints into head of integrity constraints [no]", + &theory->shift_constraints)); + handle_error(clingo_options_add_flag(options, group, "compute-components", "Compute connected components [yes]", + &theory->config.calculate_cc)); } CLINGODL_CATCH; } -extern "C" bool clingodl_validate_options(clingodl_theory_t *theory) { +extern "C" auto clingodl_validate_options(clingodl_theory_t *theory) -> bool { static_cast(theory); return true; } -extern "C" bool clingodl_on_model(clingodl_theory_t *theory, clingo_model_t* model) { +extern "C" auto clingodl_on_model(clingodl_theory_t *theory, clingo_model_t *model) -> bool { CLINGODL_TRY { Clingo::Model m(model); theory->clingodl->extend_model(m); @@ -606,11 +598,11 @@ extern "C" bool clingodl_on_model(clingodl_theory_t *theory, clingo_model_t* mod CLINGODL_CATCH; } -extern "C" bool clingodl_lookup_symbol(clingodl_theory_t *theory, clingo_symbol_t symbol, size_t *index) { +extern "C" auto clingodl_lookup_symbol(clingodl_theory_t *theory, clingo_symbol_t symbol, size_t *index) -> bool { return theory->clingodl->lookup_symbol(symbol, index); } -extern "C" clingo_symbol_t clingodl_get_symbol(clingodl_theory_t *theory, size_t index) { +extern "C" auto clingodl_get_symbol(clingodl_theory_t *theory, size_t index) -> clingo_symbol_t { return theory->clingodl->get_symbol(index); } @@ -621,19 +613,21 @@ extern "C" void clingodl_assignment_begin(clingodl_theory_t *theory, uint32_t th *index = 1; } -extern "C" bool clingodl_assignment_next(clingodl_theory_t *theory, uint32_t thread_id, size_t *index) { +extern "C" auto clingodl_assignment_next(clingodl_theory_t *theory, uint32_t thread_id, size_t *index) -> bool { return theory->clingodl->next(thread_id, index); } -extern "C" bool clingodl_assignment_has_value(clingodl_theory_t *theory, uint32_t thread_id, size_t index) { +extern "C" auto clingodl_assignment_has_value(clingodl_theory_t *theory, uint32_t thread_id, size_t index) -> bool { return theory->clingodl->has_value(thread_id, index); } -extern "C" void clingodl_assignment_get_value(clingodl_theory_t *theory, uint32_t thread_id, size_t index, clingodl_value_t *value) { +extern "C" void clingodl_assignment_get_value(clingodl_theory_t *theory, uint32_t thread_id, size_t index, + clingodl_value_t *value) { theory->clingodl->get_value(thread_id, index, value); } -extern "C" bool clingodl_on_statistics(clingodl_theory_t *theory, clingo_statistics_t* step, clingo_statistics_t* accu) { +extern "C" auto clingodl_on_statistics(clingodl_theory_t *theory, clingo_statistics_t *step, clingo_statistics_t *accu) + -> bool { CLINGODL_TRY { uint64_t root_s{0}; uint64_t root_a{0}; diff --git a/libclingo-dl/src/graph.cc b/libclingo-dl/src/graph.cc index 7e8e799a..a2867ca9 100644 --- a/libclingo-dl/src/graph.cc +++ b/libclingo-dl/src/graph.cc @@ -29,50 +29,43 @@ namespace ClingoDL { namespace { //!< Tag for traversals of the original graph. -struct From { }; +struct From {}; //!< Tag for traversals of the transposed graph. -struct To { }; +struct To {}; //! An index different from all valid edge indices. constexpr auto invalid_edge_index = std::numeric_limits::max(); } // namespace -void ThreadStatistics::reset() { - *this = ThreadStatistics{}; -} +void ThreadStatistics::reset() { *this = ThreadStatistics{}; } void ThreadStatistics::accu(ThreadStatistics const &x) { - time_propagate += x.time_propagate; - time_undo += x.time_undo; - time_dijkstra += x.time_dijkstra; - true_edges += x.true_edges; - false_edges += x.false_edges; - false_edges_trivial += x.false_edges_trivial; - false_edges_weak += x.false_edges_weak; + time_propagate += x.time_propagate; + time_undo += x.time_undo; + time_dijkstra += x.time_dijkstra; + true_edges += x.true_edges; + false_edges += x.false_edges; + false_edges_trivial += x.false_edges_trivial; + false_edges_weak += x.false_edges_weak; false_edges_weak_plus += x.false_edges_weak_plus; - propagate_cost_add += x.propagate_cost_add; - propagate_cost_from += x.propagate_cost_from; - propagate_cost_to += x.propagate_cost_to; - edges_added += x.edges_added; - edges_skipped += x.edges_skipped; - edges_propagated += x.edges_propagated; + propagate_cost_add += x.propagate_cost_add; + propagate_cost_from += x.propagate_cost_from; + propagate_cost_to += x.propagate_cost_to; + edges_added += x.edges_added; + edges_skipped += x.edges_skipped; + edges_propagated += x.edges_propagated; } //!< Thread specific information for vertices. -template -struct Graph::Vertex { +template struct Graph::Vertex { using value_t = T; using PotentialStack = std::vector>; //! Return true if the vertex has a value assigned. - [[nodiscard]] bool defined() const { - return !potential_stack.empty(); - } + [[nodiscard]] auto defined() const -> bool { return !potential_stack.empty(); } //! Return the current value associated with the vertex. - [[nodiscard]] value_t potential() const { - return potential_stack.back().second; - } + [[nodiscard]] auto potential() const -> value_t { return potential_stack.back().second; } VertexIndexVec outgoing; //!< Outgoing edges from this vertex that are true. VertexIndexVec incoming; //!< Incoming edges to this vertex that are true. @@ -99,16 +92,14 @@ struct Graph::Vertex { }; //!< Thread specific information for edges. -template -struct Graph::EdgeState { +template struct Graph::EdgeState { uint8_t removed_outgoing : 1; //!< Flag to mark edges as removed from the candidate_outgoing vector. uint8_t removed_incoming : 1; //!< Flag to mark edges as removed from the candidate_incoming vector. uint8_t enabled : 1; //!< Flag to mark the edge as enabled. }; //!< Struct holding information to backtrack a decision level. -template -struct Graph::TrailEntry { +template struct Graph::TrailEntry { level_t level; //!< The corresponding decision level. index_t vertex_offset; //!< Index up to which to backtrack changed vertices. index_t edge_offset; //!< Index up to which to backtrack changed edges. @@ -129,105 +120,93 @@ struct Graph::TrailEntry { //! \note The same effect could be achieved by providing a lot of private //! template member functions. This implementation has the advantage that the //! complexity is hidden in the implementation. -template -template -struct Graph::Impl : Graph { +template template struct Graph::Impl : Graph { using index_t = HeapType::index_type; //! The index of the vertex in the heap vector. - index_t &offset(vertex_t idx) { - return vertices_[idx].offset; - } + auto offset(vertex_t idx) -> index_t & { return vertices_[idx].offset; } //! Compare two vertices by cost/relevant. - bool less(vertex_t a, vertex_t b) { + auto less(vertex_t a, vertex_t b) -> bool { auto ca = cost(a); auto cb = cost(b); return ca < cb || (ca == cb && relevant(a) < relevant(b)); } //! Compare a cost with a vertex. - bool less(value_t ca, bool ra, vertex_t b) { + auto less(value_t ca, bool ra, vertex_t b) -> bool { auto cb = cost(b); return ca < cb || (ca == cb && ra < relevant(b)); } //! The cost of the vertex. - value_t &cost(vertex_t idx) { + auto cost(vertex_t idx) -> value_t & { if constexpr (std::is_same_v) { return vertices_[idx].cost_from; - } - else { + } else { return vertices_[idx].cost_to; } } //! The bound of a vertex. - value_t &bound_value(vertex_t idx) { + auto bound_value(vertex_t idx) -> value_t & { if constexpr (std::is_same_v) { return vertices_[idx].bound_lower; - } - else { + } else { return vertices_[idx].bound_upper; } } //! The bound changes during bound propagation. - BoundTrailVec &bound_trail() { + auto bound_trail() -> BoundTrailVec & { if constexpr (std::is_same_v) { return lower_trail_; - } - else { + } else { return upper_trail_; } } //! The end point of the given edge. - vertex_t to(edge_t idx) { + auto to(edge_t idx) -> vertex_t { if constexpr (std::is_same_v) { return edges_[idx].to; - } - else { + } else { return edges_[idx].from; } } //! The starting point of the given edge. - vertex_t from(edge_t idx) { + auto from(edge_t idx) -> vertex_t { if constexpr (std::is_same_v) { return edges_[idx].from; - } - else { + } else { return edges_[idx].to; } } //! The outgoing vertices of the given vertex. - std::vector &out(vertex_t idx) { + auto out(vertex_t idx) -> std::vector & { if constexpr (std::is_same_v) { return vertices_[idx].outgoing; - } - else { + } else { return vertices_[idx].incoming; } } //! The edge that was used to reach the given vertex. - edge_t &path(vertex_t idx) { + auto path(vertex_t idx) -> edge_t & { if constexpr (std::is_same_v) { return vertices_[idx].path_from; - } - else { + } else { return vertices_[idx].path_to; } } //! The edge that was used to reach the given vertex when computing bounds. - edge_t &bound_path(vertex_t idx) { + auto bound_path(vertex_t idx) -> edge_t & { if constexpr (std::is_same_v) { return vertices_[idx].path_lower; - } - else { + } else { return vertices_[idx].path_upper; } } @@ -236,71 +215,64 @@ struct Graph::Impl : Graph { //! //! \note This is a integer here because it is also used as a dfs index //! when adding edges. - std::conditional_t, vertex_t, bool> &visited(vertex_t idx) { - if constexpr(std::is_same_v) { + auto visited(vertex_t idx) -> std::conditional_t, vertex_t, bool> & { + if constexpr (std::is_same_v) { return vertices_[idx].visited_from; - } - else { + } else { return vertices_[idx].visited_to; } } //! Flag indicating whether the vertex has been visited during bound traversals. - bool &bound_visited(vertex_t idx) { - if constexpr(std::is_same_v) { + auto bound_visited(vertex_t idx) -> bool & { + if constexpr (std::is_same_v) { return vertices_[idx].visited_lower; - } - else { + } else { return vertices_[idx].visited_upper; } } //! Whether the vertex is relevant for propagation. - bool &relevant(vertex_t idx) { + auto relevant(vertex_t idx) -> bool & { if constexpr (std::is_same_v) { return vertices_[idx].relevant_from; - } - else { + } else { return vertices_[idx].relevant_to; } } //! The set of all visited vertices. - std::vector &visited_set() { + auto visited_set() -> std::vector & { if constexpr (std::is_same_v) { return visited_from_; - } - else { + } else { return visited_to_; } } //! The set of all visited vertices. - std::vector &bound_visited_set() { + auto bound_visited_set() -> std::vector & { if constexpr (std::is_same_v) { return visited_lower_; - } - else { + } else { return visited_upper_; } } //! Outgoing candidate edges that are not false. - std::vector &candidate_outgoing(vertex_t idx) { + auto candidate_outgoing(vertex_t idx) -> std::vector & { if constexpr (std::is_same_v) { return vertices_[idx].candidate_outgoing; - } - else { + } else { return vertices_[idx].candidate_incoming; } } //! Incoming candidate edges that are not false. - std::vector &candidate_incoming(vertex_t idx) { + auto candidate_incoming(vertex_t idx) -> std::vector & { if constexpr (std::is_same_v) { return vertices_[idx].candidate_incoming; - } - else { + } else { return vertices_[idx].candidate_outgoing; } } @@ -309,8 +281,7 @@ struct Graph::Impl : Graph { void remove_incoming(edge_t idx) { if constexpr (std::is_same_v) { edge_states_[idx].removed_incoming = true; - } - else { + } else { edge_states_[idx].removed_outgoing = true; } } @@ -319,25 +290,24 @@ struct Graph::Impl : Graph { void remove_outgoing(edge_t idx) { if constexpr (std::is_same_v) { edge_states_[idx].removed_outgoing = true; - } - else { + } else { edge_states_[idx].removed_incoming = true; } } //! The cost to propagate the edge. - uint64_t &propagation_cost() { + auto propagation_cost() -> uint64_t & { if constexpr (std::is_same_v) { return stats_.propagate_cost_from; - } - else { + } else { return stats_.propagate_cost_to; } } #ifdef CLINGODL_CROSSCHECK //! Compute shortests paths using the Bellman Ford algorithm. - std::optional> bellman_ford_(std::vector const &edges, vertex_t source) { + std::optional> bellman_ford_(std::vector const &edges, + vertex_t source) { std::unordered_map costs; costs[source] = 0; vertex_t vertices = 0; @@ -356,8 +326,7 @@ struct Graph::Impl : Graph { auto dist = u_cost->second + uv.weight; if (v_cost == costs.end()) { costs[u_idx] = dist; - } - else if (dist < v_cost->second) { + } else if (dist < v_cost->second) { v_cost->second = dist; } } @@ -434,8 +403,7 @@ struct Graph::Impl : Graph { visited(v_idx) = true; relevant(v_idx) = relevant_u || uv_idx == relevant_idx; costs_heap_.push(*this, v_idx); - } - else { + } else { // vertex v became or lost relevance if (relevant_u != relevant_v) { relevant(v_idx) = relevant_u; @@ -501,7 +469,8 @@ struct Graph::Impl : Graph { auto c = cost(s_idx) + vertices_[st.from].potential() + st.weight - vertices_[st.to].potential(); auto bound_st = bound_value(s_idx) + st.weight; assert(vertices_[st.from].potential() + st.weight - vertices_[st.to].potential() >= 0); - if ((!visited(t_idx) || less(c, false, t_idx)) && (!bound_visited(t_idx) || bound_st < bound_value(t_idx))) { + if ((!visited(t_idx) || less(c, false, t_idx)) && + (!bound_visited(t_idx) || bound_st < bound_value(t_idx))) { cost(t_idx) = c; if (!visited(t_idx)) { visited(t_idx) = true; @@ -510,8 +479,7 @@ struct Graph::Impl : Graph { bound_trail().emplace_back(std::make_tuple(t_idx, bound_path(t_idx), bound_value(t_idx))); } costs_heap_.push(*this, t_idx); - } - else { + } else { costs_heap_.decrease(*this, t_idx); } bound_path(t_idx) = st_idx; @@ -575,35 +543,33 @@ struct Graph::Impl : Graph { if (!full || relevant(vertex)) { if (forward) { auto &in = candidate_incoming(vertex); - in.resize( - std::remove_if( - in.begin(), in.end(), - [&](edge_t uv_idx) { - if (!edge_states_[uv_idx].enabled || propagate_edge_true_(uv_idx, xy_idx)) { - remove_incoming(uv_idx); - return true; - } - return false; - }) - - in.begin()); + in.resize(std::remove_if(in.begin(), in.end(), + [&](edge_t uv_idx) { + if (!edge_states_[uv_idx].enabled || + propagate_edge_true_(uv_idx, xy_idx)) { + remove_incoming(uv_idx); + return true; + } + return false; + }) - + in.begin()); } if (backward) { bool ret = true; auto &out = candidate_outgoing(vertex); - out.resize( - std::remove_if( - out.begin(), out.end(), - [&](edge_t uv_idx) { - if (!ret) { - return false; - } - if (!edge_states_[uv_idx].enabled || propagate_edge_false_(ctl, uv_idx, xy_idx, ret)) { - remove_outgoing(uv_idx); - return true; - } - return false; - }) - - out.begin()); + out.resize(std::remove_if(out.begin(), out.end(), + [&](edge_t uv_idx) { + if (!ret) { + return false; + } + if (!edge_states_[uv_idx].enabled || + propagate_edge_false_(ctl, uv_idx, xy_idx, ret)) { + remove_outgoing(uv_idx); + return true; + } + return false; + }) - + out.begin()); if (!ret) { return false; } @@ -616,9 +582,7 @@ struct Graph::Impl : Graph { template Graph::Graph(ThreadStatistics &stats, EdgeVec const &edges, PropagationMode propagate) -: edges_{edges} -, stats_{stats} -, propagate_{propagate} { + : edges_{edges}, stats_{stats}, propagate_{propagate} { edge_states_.resize(edges_.size(), {1, 1, 0}); for (edge_t i = 0; i < numeric_cast(edges_.size()); ++i) { ensure_index(vertices_, std::max(edges_[i].from, edges_[i].to)); @@ -626,35 +590,26 @@ Graph::Graph(ThreadStatistics &stats, EdgeVec const &edges, PropagationMode p } } -template -Graph::~Graph() = default; +template Graph::~Graph() = default; -template -Graph::Graph(Graph &&other) noexcept = default; +template Graph::Graph(Graph &&other) noexcept = default; -template -bool Graph::empty() const { - return vertices_.empty(); -} +template auto Graph::empty() const -> bool { return vertices_.empty(); } -template -bool Graph::has_value(vertex_t idx) const { +template auto Graph::has_value(vertex_t idx) const -> bool { return idx < vertices_.size() && vertices_[idx].defined(); } -template -T Graph::get_value(vertex_t idx) const { +template auto Graph::get_value(vertex_t idx) const -> T { assert(has_value(idx)); return -vertices_[idx].potential(); } -template -bool Graph::edge_is_enabled(edge_t edge_idx) const { +template auto Graph::edge_is_enabled(edge_t edge_idx) const -> bool { return edge_states_[edge_idx].enabled; } -template -bool Graph::edge_is_negative(edge_t edge_idx) const { +template auto Graph::edge_is_negative(edge_t edge_idx) const -> bool { auto const &st = edges_[edge_idx]; auto const &u = vertices_[st.from]; auto const &v = vertices_[st.to]; @@ -663,34 +618,24 @@ bool Graph::edge_is_negative(edge_t edge_idx) const { return up + st.weight - vp < 0; } -template -bool Graph::can_propagate() const { +template auto Graph::can_propagate() const -> bool { return changed_trail_.empty() || changed_trail_.back().can_propagate; } -template -void Graph::disable_propagate() { - changed_trail_.back().can_propagate = false; -} +template void Graph::disable_propagate() { changed_trail_.back().can_propagate = false; } -template -void Graph::ensure_decision_level(level_t level, bool enable_propagate) { +template void Graph::ensure_decision_level(level_t level, bool enable_propagate) { // initialize the trail if (changed_trail_.empty() || current_decision_level_() < level) { - changed_trail_.push_back({level, - numeric_cast(changed_vertices_.size()), - numeric_cast(changed_edges_.size()), - numeric_cast(disabled_edges_.size()), - numeric_cast(visited_lower_.size()), - numeric_cast(visited_upper_.size()), - numeric_cast(lower_trail_.size()), - numeric_cast(upper_trail_.size()), - can_propagate() && enable_propagate}); + changed_trail_.push_back( + {level, numeric_cast(changed_vertices_.size()), numeric_cast(changed_edges_.size()), + numeric_cast(disabled_edges_.size()), numeric_cast(visited_lower_.size()), + numeric_cast(visited_upper_.size()), numeric_cast(lower_trail_.size()), + numeric_cast(upper_trail_.size()), can_propagate() && enable_propagate}); } } -template -bool Graph::add_edge(Clingo::PropagateControl &ctl, edge_t uv_idx, vertex_t zero_idx) { +template auto Graph::add_edge(Clingo::PropagateControl &ctl, edge_t uv_idx, vertex_t zero_idx) -> bool { // This function adds an edge to the graph and returns false if the edge // induces a negative cycle. // @@ -750,8 +695,8 @@ bool Graph::propagate_zero_(Clingo::PropagateControl &ctl, edge_t uv_idx, ver #ifdef CLINGODL_CROSSCHECK if (ret) { auto ass = ctl.assignment(); - auto cost_from_zero = static_cast*>(this)->bellman_ford_(changed_edges_, zero_idx); - auto cost_to_zero = static_cast*>(this)->bellman_ford_(changed_edges_, zero_idx); + auto cost_from_zero = static_cast *>(this)->bellman_ford_(changed_edges_, zero_idx); + auto cost_to_zero = static_cast *>(this)->bellman_ford_(changed_edges_, zero_idx); if (cost_from_zero && cost_to_zero) { for (auto [x_idx, cost_x] : *cost_from_zero) { for (auto &xy : edges_) { @@ -765,7 +710,7 @@ bool Graph::propagate_zero_(Clingo::PropagateControl &ctl, edge_t uv_idx, ver auto cost_y = it_y->second; static_cast(cost_y); static_cast(ass); - assert (cost_x + cost_y + xy.weight >= 0 || ass.is_false(xy.lit)); + assert(cost_x + cost_y + xy.weight >= 0 || ass.is_false(xy.lit)); } } } @@ -776,8 +721,7 @@ bool Graph::propagate_zero_(Clingo::PropagateControl &ctl, edge_t uv_idx, ver return ret; } -template -bool Graph::check_cycle_(Clingo::PropagateControl &ctl, edge_t uv_idx) { // NOLINT +template bool Graph::check_cycle_(Clingo::PropagateControl &ctl, edge_t uv_idx) { // NOLINT // NOTE: would be more efficient if relevant would return statically false here // for the compiler to make comparison cheaper @@ -801,8 +745,7 @@ bool Graph::check_cycle_(Clingo::PropagateControl &ctl, edge_t uv_idx) { // N visited_from_.emplace_back(uv.to); v.visited_from = 1; v.path_from = uv_idx; - } - else { + } else { ++stats_.edges_skipped; } @@ -828,8 +771,7 @@ bool Graph::check_cycle_(Clingo::PropagateControl &ctl, edge_t uv_idx) { // N t.visited_from = 1; visited_from_.emplace_back(st.to); costs_heap_.push(m, st.to); - } - else { + } else { costs_heap_.decrease(m, st.to); } } @@ -871,8 +813,7 @@ bool Graph::check_cycle_(Clingo::PropagateControl &ctl, edge_t uv_idx) { // N return ctl.add_clause(clause_) && ctl.propagate(); } -template -bool Graph::propagate_simple_(Clingo::PropagateControl &ctl, edge_t uv_idx) { // NOLINT +template bool Graph::propagate_simple_(Clingo::PropagateControl &ctl, edge_t uv_idx) { // NOLINT if (propagate_ >= PropagationMode::Trivial) { auto &uv = edges_[uv_idx]; if (visited_from_.empty() || propagate_ == PropagationMode::Trivial) { @@ -903,8 +844,7 @@ bool Graph::propagate_simple_(Clingo::PropagateControl &ctl, edge_t uv_idx) { return true; } -template -bool Graph::propagate_full_(Clingo::PropagateControl &ctl, edge_t xy_idx) { +template auto Graph::propagate_full_(Clingo::PropagateControl &ctl, edge_t xy_idx) -> bool { // The function is best understood considering the following example graph: // // v ->* x -> y ->* u @@ -930,20 +870,23 @@ bool Graph::propagate_full_(Clingo::PropagateControl &ctl, edge_t xy_idx) { vertex_t num_relevant_in_to{0}; { Timer t{stats_.time_dijkstra}; - std::tie(num_relevant_out_from, num_relevant_in_from) = static_cast*>(this)->dijkstra_full(xy.from, xy_idx); - std::tie(num_relevant_out_to, num_relevant_in_to) = static_cast*>(this)->dijkstra_full(xy.to, xy_idx); + std::tie(num_relevant_out_from, num_relevant_in_from) = + static_cast *>(this)->dijkstra_full(xy.from, xy_idx); + std::tie(num_relevant_out_to, num_relevant_in_to) = static_cast *>(this)->dijkstra_full(xy.to, xy_idx); } #ifdef CLINGODL_CROSSCHECK // check if the counts of relevant incoming/outgoing vertices are correct - assert(std::make_pair(num_relevant_in_from, num_relevant_out_from) == static_cast *>(this)->count_relevant_()); + assert(std::make_pair(num_relevant_in_from, num_relevant_out_from) == + static_cast *>(this)->count_relevant_()); assert(std::make_pair(num_relevant_out_to, num_relevant_in_to) == static_cast *>(this)->count_relevant_()); #endif bool forward_from = num_relevant_in_from < num_relevant_out_to; bool backward_from = num_relevant_out_from < num_relevant_in_to; - bool ret = static_cast *>(this)->template propagate_edges(ctl, xy_idx, forward_from, backward_from) && - static_cast *>(this)->template propagate_edges(ctl, xy_idx, !forward_from, !backward_from); + bool ret = + static_cast *>(this)->template propagate_edges(ctl, xy_idx, forward_from, backward_from) && + static_cast *>(this)->template propagate_edges(ctl, xy_idx, !forward_from, !backward_from); for (auto &x : visited_from_) { vertices_[x].visited_from = 0; @@ -960,7 +903,7 @@ bool Graph::propagate_full_(Clingo::PropagateControl &ctl, edge_t xy_idx) { template template -bool Graph::with_incoming_(Clingo::PropagateControl &ctl, vertex_t s_idx, F f) { +auto Graph::with_incoming_(Clingo::PropagateControl &ctl, vertex_t s_idx, F f) -> bool { auto &s = vertices_[s_idx]; auto &in = s.candidate_incoming; auto jt = in.begin(); @@ -982,7 +925,7 @@ bool Graph::with_incoming_(Clingo::PropagateControl &ctl, vertex_t s_idx, F f // add constraint for the negative cycle if (!(ctl.add_clause(clause_) && ctl.propagate())) { // erease edges marked as removed - in.erase(jt, it+1); + in.erase(jt, it + 1); return false; } continue; @@ -994,7 +937,7 @@ bool Graph::with_incoming_(Clingo::PropagateControl &ctl, vertex_t s_idx, F f } template -[[nodiscard]] bool Graph::cheap_propagate_(Clingo::PropagateControl &ctl, vertex_t u_idx, vertex_t s_idx) { +[[nodiscard]] auto Graph::cheap_propagate_(Clingo::PropagateControl &ctl, vertex_t u_idx, vertex_t s_idx) -> bool { // we check for the following case: // u ->* s ->* t // ^----/ @@ -1018,8 +961,7 @@ template if (r_idx == s_idx) { if (u_idx == s_idx) { ++stats_.false_edges_weak; - } - else { + } else { ++stats_.false_edges_weak_plus; } assert(weight == check); @@ -1032,8 +974,7 @@ template }); } -template -void Graph::backtrack() { +template void Graph::backtrack() { auto entry = changed_trail_.back(); for (auto it = changed_vertices_.rbegin(), ie = changed_vertices_.rend() - entry.vertex_offset; it != ie; ++it) { vertices_[*it].potential_stack.pop_back(); @@ -1072,8 +1013,7 @@ void Graph::backtrack() { changed_trail_.pop_back(); } -template -void Graph::disable_edge(edge_t uv_idx) { +template void Graph::disable_edge(edge_t uv_idx) { auto &uv = edges_[uv_idx]; auto &u = vertices_[uv.from]; auto &v = vertices_[uv.to]; @@ -1084,13 +1024,9 @@ void Graph::disable_edge(edge_t uv_idx) { edge_states_[uv_idx].enabled = false; } -template -PropagationMode Graph::mode() const { - return propagate_; -} +template auto Graph::mode() const -> PropagationMode { return propagate_; } -template -void Graph::add_candidate_edge_(edge_t uv_idx) { +template void Graph::add_candidate_edge_(edge_t uv_idx) { auto &uv = edges_[uv_idx]; auto &uv_state = edge_states_[uv_idx]; auto &u = vertices_[uv.from]; @@ -1109,9 +1045,7 @@ void Graph::add_candidate_edge_(edge_t uv_idx) { } } -template -template -bool Graph::propagate_edge_true_(edge_t uv_idx, edge_t xy_idx) { // NOLINT +template template bool Graph::propagate_edge_true_(edge_t uv_idx, edge_t xy_idx) { // NOLINT // The function is best understood considering the following example graph: // // u ->* x -> y ->* v @@ -1131,11 +1065,10 @@ bool Graph::propagate_edge_true_(edge_t uv_idx, edge_t xy_idx) { // NOLINT auto &u = vertices_[uv.from]; auto &v = vertices_[uv.to]; bool relevant = false; - if constexpr(full) { + if constexpr (full) { assert(u.relevant_to || v.relevant_from); relevant = u.relevant_to && v.relevant_from; - } - else { + } else { assert(u.visited_upper || v.visited_lower); relevant = u.visited_upper && v.visited_lower; } @@ -1146,7 +1079,7 @@ bool Graph::propagate_edge_true_(edge_t uv_idx, edge_t xy_idx) { // NOLINT auto &y = vertices_[xy.to]; value_t cost_uv{0}; - if constexpr(full) { + if constexpr (full) { auto cost_uy = u.cost_to + y.potential() - u.potential(); auto cost_xv = v.cost_from + v.potential() - x.potential(); cost_uv = cost_uy + cost_xv - xy.weight; @@ -1163,14 +1096,13 @@ bool Graph::propagate_edge_true_(edge_t uv_idx, edge_t xy_idx) { // NOLINT assert(bf_cost_uy->second == cost_uy); assert(bf_cost_xv->second == cost_xv); #endif - } - else { + } else { cost_uv = u.bound_upper + v.bound_lower; } if (cost_uv <= uv.weight) { #ifdef CLINGODL_CROSSCHECK // make sure that the graph does not have a negative cycle even if it contains the edge - if constexpr(full) { + if constexpr (full) { auto edges = changed_edges_; edges.emplace_back(uv_idx); auto &m = *static_cast *>(this); @@ -1208,11 +1140,10 @@ bool Graph::propagate_edge_false_(Clingo::PropagateControl &ctl, edge_t uv_id auto &u = vertices_[uv.from]; auto &v = vertices_[uv.to]; bool relevant = true; - if constexpr(full) { + if constexpr (full) { assert(v.relevant_to || u.relevant_from); relevant = v.relevant_to && u.relevant_from; - } - else { + } else { assert(v.visited_upper || u.visited_lower); relevant = v.visited_upper && u.visited_lower; } @@ -1223,12 +1154,11 @@ bool Graph::propagate_edge_false_(Clingo::PropagateControl &ctl, edge_t uv_id auto &y = vertices_[xy.to]; value_t cost_vu{0}; - if constexpr(full) { + if constexpr (full) { auto cost_vy = v.cost_to + y.potential() - v.potential(); auto cost_xu = u.cost_from + u.potential() - x.potential(); cost_vu = cost_vy + cost_xu - xy.weight; - } - else { + } else { cost_vu = v.bound_upper + u.bound_lower; } @@ -1237,7 +1167,7 @@ bool Graph::propagate_edge_false_(Clingo::PropagateControl &ctl, edge_t uv_id if (!ctl.assignment().is_false(uv.lit)) { #ifdef CLINGODL_CROSSCHECK value_t sum = uv.weight; - if constexpr(full) { + if constexpr (full) { sum -= xy.weight; } #endif @@ -1275,7 +1205,7 @@ bool Graph::propagate_edge_false_(Clingo::PropagateControl &ctl, edge_t uv_id } #ifdef CLINGODL_CROSSCHECK // make sure that the graph does not have a negative cycle even if it contains the edge - if constexpr(full) { + if constexpr (full) { auto edges = changed_edges_; edges.emplace_back(uv_idx); auto &m = *static_cast *>(this); @@ -1287,19 +1217,16 @@ bool Graph::propagate_edge_false_(Clingo::PropagateControl &ctl, edge_t uv_id return false; } -template -void Graph::set_potential_(Vertex &vtx, level_t level, T potential) { +template void Graph::set_potential_(Vertex &vtx, level_t level, T potential) { if (!vtx.defined() || vtx.potential_stack.back().first < level) { vtx.potential_stack.emplace_back(level, potential); changed_vertices_.emplace_back(numeric_cast(&vtx - vertices_.data())); - } - else { + } else { vtx.potential_stack.back().second = potential; } } -template -level_t Graph::current_decision_level_() { +template auto Graph::current_decision_level_() -> level_t { assert(!changed_trail_.empty()); return changed_trail_.back().level; } diff --git a/libclingo-dl/src/parsing.cc b/libclingo-dl/src/parsing.cc index 3091f3ee..a221c883 100644 --- a/libclingo-dl/src/parsing.cc +++ b/libclingo-dl/src/parsing.cc @@ -31,7 +31,7 @@ namespace ClingoDL { namespace { //! Negate a relation symbol. -char const *negate_relation(char const *op) { +auto negate_relation(char const *op) -> char const * { if (std::strcmp(op, "=") == 0) { return "!="; } @@ -56,7 +56,7 @@ char const *negate_relation(char const *op) { using ClingoDL::match; //! Match if the given node represents a constant with the given name. -bool match_constant(Clingo::AST::Node const &ast, char const *name) { +auto match_constant(Clingo::AST::Node const &ast, char const *name) -> bool { using namespace Clingo::AST; switch (ast.type()) { case Type::SymbolicTerm: { @@ -78,7 +78,7 @@ bool match_constant(Clingo::AST::Node const &ast, char const *name) { } //! Shift difference constraints in integrity constraints to the head. -Clingo::AST::Node shift_rule(Clingo::AST::Node ast) { +auto shift_rule(Clingo::AST::Node ast) -> Clingo::AST::Node { using namespace Clingo::AST; if (ast.type() != Type::Rule) { return ast; @@ -128,7 +128,7 @@ Clingo::AST::Node shift_rule(Clingo::AST::Node ast) { } //! Tag terms depending on whether they occur in heads or bodies. -Clingo::AST::Node tag_terms(Clingo::AST::Node &ast, char const *tag) { +auto tag_terms(Clingo::AST::Node &ast, char const *tag) -> Clingo::AST::Node { using namespace Clingo::AST; if (ast.type() == Type::SymbolicTerm) { auto ret = ast.copy(); @@ -143,7 +143,7 @@ Clingo::AST::Node tag_terms(Clingo::AST::Node &ast, char const *tag) { if (ast.type() == Type::Function) { auto ret = ast.copy(); std::string name{"__"}; - name += ret.get(Attribute::Name); + name += ret.get(Attribute::Name); name += tag; ret.set(Attribute::Name, Clingo::add_string(name.c_str())); return ret; @@ -153,7 +153,7 @@ Clingo::AST::Node tag_terms(Clingo::AST::Node &ast, char const *tag) { //! Tag head/body theory atoms. struct TheoryRewriter { - Clingo::AST::Node operator()(Clingo::AST::Node const &ast) { + auto operator()(Clingo::AST::Node const &ast) -> Clingo::AST::Node { using namespace Clingo::AST; if (ast.type() == Type::Literal) { in_literal = true; @@ -188,13 +188,10 @@ struct TheoryRewriter { constexpr int INVALID_VAR{std::numeric_limits::max()}; //! Test whether a variable is valid. -[[nodiscard]] inline bool is_valid_var(int var) { - return var < INVALID_VAR; -} +[[nodiscard]] inline auto is_valid_var(int var) -> bool { return var < INVALID_VAR; } //! Convert a symbol to a double or integer. -template -[[nodiscard]] T to_number(Clingo::Symbol const &a) { +template [[nodiscard]] auto to_number(Clingo::Symbol const &a) -> T { if (a.type() == Clingo::SymbolType::Number) { return static_cast(a.number()); } @@ -205,12 +202,11 @@ template } //! Evaluate a theory term to a number (represented by a symbol). -template -[[nodiscard]] Clingo::Symbol evaluate(Clingo::TheoryTerm const &term); +template [[nodiscard]] auto evaluate(Clingo::TheoryTerm const &term) -> Clingo::Symbol; //! Evaluate two theory terms involved involved in a binary operation to an integral number. template , bool>::type = true> -[[nodiscard]] Clingo::Symbol evaluate_binary(Clingo::TheoryTerm const &a, Clingo::TheoryTerm const &b, F &&f) { +[[nodiscard]] auto evaluate_binary(Clingo::TheoryTerm const &a, Clingo::TheoryTerm const &b, F &&f) -> Clingo::Symbol { auto ea = evaluate(a); check_syntax(ea.type() == Clingo::SymbolType::Number); auto eb = evaluate(b); @@ -220,23 +216,22 @@ template , bool> //! Evaluate two theory terms involved involved in a binary operation to a floating point number. template , bool>::type = true> -[[nodiscard]] Clingo::Symbol evaluate_binary(Clingo::TheoryTerm const &a, Clingo::TheoryTerm const &b, F &&f) { +[[nodiscard]] auto evaluate_binary(Clingo::TheoryTerm const &a, Clingo::TheoryTerm const &b, F &&f) -> Clingo::Symbol { auto ea = evaluate(a); auto eb = evaluate(b); return Clingo::String(std::to_string(f(to_number(ea), to_number(eb))).c_str()); } //! Parse a string to a number. -template -[[nodiscard]] std::optional parse_number(char const *name) { +template [[nodiscard]] auto parse_number(char const *name) -> std::optional { static const std::string chars = "\""; auto len = std::strlen(name); if (len < 2 || name[0] != '"' || name[len - 1] != '"') { // NOLINT return std::nullopt; } - char *parsed = nullptr; // NOLINT + char *parsed = nullptr; // NOLINT auto res = std::strtod(name + 1, &parsed); // NOLINT - if (parsed != name + len - 1) { // NOLINT + if (parsed != name + len - 1) { // NOLINT return std::nullopt; } auto ret = static_cast(res); @@ -246,8 +241,7 @@ template return ret; } -template -Clingo::Symbol evaluate(Clingo::TheoryTerm const &term) { +template auto evaluate(Clingo::TheoryTerm const &term) -> Clingo::Symbol { if (term.type() == Clingo::TheoryTermType::Symbol) { auto const *name = term.name(); if (std::strncmp(name, "\"", 1) == 0) { @@ -305,16 +299,15 @@ Clingo::Symbol evaluate(Clingo::TheoryTerm const &term) { //! Parse the given theory term for an arithmetic expression. template -void parse_elem(Clingo::TheoryTerm const &term, std::function const &map_vert, CoVarVec &res) { // NOLINT +void parse_elem(Clingo::TheoryTerm const &term, std::function const &map_vert, + CoVarVec &res) { // NOLINT if (term.type() == Clingo::TheoryTermType::Number) { res.emplace_back(term.number(), INVALID_VAR); - } - else if (match(term, "+", 2)) { + } else if (match(term, "+", 2)) { auto args = term.arguments(); parse_elem(args.front(), map_vert, res); parse_elem(args.back(), map_vert, res); - } - else if (match(term, "-", 2)) { + } else if (match(term, "-", 2)) { auto args = term.arguments(); parse_elem(args.front(), map_vert, res); auto pos = res.size(); @@ -322,18 +315,15 @@ void parse_elem(Clingo::TheoryTerm const &term, std::functionfirst = safe_inv(it->first); } - } - else if (match(term, "-", 1)) { + } else if (match(term, "-", 1)) { auto pos = res.size(); parse_elem(term.arguments().front(), map_vert, res); for (auto it = res.begin() + pos, ie = res.end(); it != ie; ++it) { it->first = safe_inv(it->first); } - } - else if (match(term, "+", 1)) { + } else if (match(term, "+", 1)) { parse_elem(term.arguments().front(), map_vert, res); - } - else if (match(term, "*", 2)) { + } else if (match(term, "*", 2)) { auto args = term.arguments(); CoVarVec lhs; parse_elem(args.front(), map_vert, lhs); @@ -343,35 +333,28 @@ void parse_elem(Clingo::TheoryTerm const &term, std::function(term.name()); val) { res.emplace_back(*val, INVALID_VAR); - } - else { + } else { res.emplace_back(1, map_vert(evaluate(term))); } - } - else if (term.type() == Clingo::TheoryTermType::Function || term.type() == Clingo::TheoryTermType::Tuple) { + } else if (term.type() == Clingo::TheoryTermType::Function || term.type() == Clingo::TheoryTermType::Tuple) { res.emplace_back(1, map_vert(evaluate(term))); - } - else { + } else { throw_syntax_error("Invalid Syntax: invalid diff constraint"); } } //! Simplify the given vector of terms. -template -[[nodiscard]] N simplify(CoVarVec &vec) { +template [[nodiscard]] auto simplify(CoVarVec &vec) -> N { static thread_local std::unordered_map::iterator> seen; N rhs = 0; seen.clear(); @@ -384,15 +367,13 @@ template } if (!is_valid_var(var)) { rhs = safe_sub(rhs, co); - } - else { + } else { auto r = seen.emplace(var, jt); auto kt = r.first; auto ins = r.second; if (!ins) { kt->second->first = safe_add(kt->second->first, co); - } - else { + } else { if (it != jt) { *jt = *it; } @@ -401,20 +382,17 @@ template } } - jt = std::remove_if(vec.begin(), jt, [](auto &co_var) { return co_var.first == 0; } ); + jt = std::remove_if(vec.begin(), jt, [](auto &co_var) { return co_var.first == 0; }); vec.erase(jt, vec.end()); return rhs; } } // namespace -bool match(Clingo::TheoryTerm const &term, char const *name, size_t arity) { - return (term.type() == Clingo::TheoryTermType::Symbol && - std::strcmp(term.name(), name) == 0 && - arity == 0) || - (term.type() == Clingo::TheoryTermType::Function && - std::strcmp(term.name(), name) == 0 && - term.arguments().size() == arity); +auto match(Clingo::TheoryTerm const &term, char const *name, size_t arity) -> bool { + return (term.type() == Clingo::TheoryTermType::Symbol && std::strcmp(term.name(), name) == 0 && arity == 0) || + (term.type() == Clingo::TheoryTermType::Function && std::strcmp(term.name(), name) == 0 && + term.arguments().size() == arity); } void transform(Clingo::AST::Node const &ast, NodeCallback const &cb, bool shift) { @@ -427,7 +405,7 @@ void transform(Clingo::AST::Node const &ast, NodeCallback const &cb, bool shift) } template -EdgeAtom parse(Clingo::TheoryAtom const &atom, std::function const &map_vert) { +auto parse(Clingo::TheoryAtom const &atom, std::function const &map_vert) -> EdgeAtom { char const *msg = "parsing difference constraint failed: only constraints of form &diff {u - v} <= b are accepted"; if (!atom.has_guard()) { throw std::runtime_error(msg); @@ -458,7 +436,7 @@ EdgeAtom parse(Clingo::TheoryAtom const &atom, std::function parse(Clingo::TheoryAtom const &, std::function const &); -template EdgeAtom parse(Clingo::TheoryAtom const &, std::function const &); +template EdgeAtom parse(Clingo::TheoryAtom const &, std::function const &); +template EdgeAtom parse(Clingo::TheoryAtom const &, std::function const &); } // namespace ClingoDL diff --git a/libclingo-dl/src/propagator.cc b/libclingo-dl/src/propagator.cc index 79849cb9..54276a8a 100644 --- a/libclingo-dl/src/propagator.cc +++ b/libclingo-dl/src/propagator.cc @@ -33,12 +33,12 @@ namespace ClingoDL { namespace { template , bool>::type = true> -inline Clingo::Symbol to_symbol(T value) { +inline auto to_symbol(T value) -> Clingo::Symbol { return Clingo::Number(value); } template , bool>::type = true> -inline Clingo::Symbol to_symbol(T value) { +inline auto to_symbol(T value) -> Clingo::Symbol { return Clingo::String(std::to_string(value).c_str()); } @@ -71,12 +71,8 @@ void Statistics::accu(Statistics const &x) { } //! Struct to store vertex specific information. -template -struct DLPropagator::VertexInfo { - VertexInfo(Clingo::Symbol symbol) - : symbol{symbol} - , cc{0} - , visited{0} { } +template struct DLPropagator::VertexInfo { + VertexInfo(Clingo::Symbol symbol) : symbol{symbol}, cc{0}, visited{0} {} //! Mark the vertex visited in the given connected component. void set_visited(index_t cc, bool visited) { this->cc = cc; @@ -89,13 +85,11 @@ struct DLPropagator::VertexInfo { }; //! Struct to store thread specific state. -template -struct DLPropagator::ThreadState { - ThreadState(ThreadStatistics &stats, const std::vector &edges, PropagationMode propagate, level_t propagate_root, uint64_t propagate_budget) - : stats{stats} - , graph{stats, edges, propagate} - , propagate_root{propagate_root} - , propagate_budget{propagate_budget} { } +template struct DLPropagator::ThreadState { + ThreadState(ThreadStatistics &stats, const std::vector &edges, PropagationMode propagate, + level_t propagate_root, uint64_t propagate_budget) + : stats{stats}, graph{stats, edges, propagate}, propagate_root{propagate_root}, + propagate_budget{propagate_budget} {} ThreadStatistics &stats; //!< Thread specific statistics. Graph graph; //!< The incremental graph associated with the thread. @@ -110,48 +104,35 @@ struct DLPropagator::ThreadState { //! The solver never backtracks the top-level level. When solving a new step, //! we simply rebuild the per thread states and repropagate the facts stored //! here. -template -struct DLPropagator::FactState { +template struct DLPropagator::FactState { std::vector lits; //!< Literals that are true on level 0. size_t limit{0}; //!< Offset until which literals have to be repropagated. }; template -DLPropagator::DLPropagator(Statistics &stats, PropagatorConfig conf) -: stats_{stats} -, conf_{std::move(conf)} { +DLPropagator::DLPropagator(Statistics &stats, PropagatorConfig conf) : stats_{stats}, conf_{std::move(conf)} { zero_vertices_.emplace_back(map_vertex_(Clingo::Number(0))); cc_reset_(); } -template -DLPropagator::~DLPropagator() = default; +template DLPropagator::~DLPropagator() = default; -template -vertex_t DLPropagator::num_vertices() const { - return vertex_info_.size(); -} +template auto DLPropagator::num_vertices() const -> vertex_t { return vertex_info_.size(); } -template -Clingo::Symbol DLPropagator::symbol(vertex_t index) const { +template auto DLPropagator::symbol(vertex_t index) const -> Clingo::Symbol { return vertex_info_[index].symbol; } -template -vertex_t DLPropagator::lookup(Clingo::Symbol symbol) { +template auto DLPropagator::lookup(Clingo::Symbol symbol) -> vertex_t { auto it = vert_map_inv_.find(symbol); - return it != vert_map_inv_.end() - ? it->second - : num_vertices(); + return it != vert_map_inv_.end() ? it->second : num_vertices(); } -template -bool DLPropagator::has_lower_bound(Clingo::id_t thread_id, vertex_t index) const { +template auto DLPropagator::has_lower_bound(Clingo::id_t thread_id, vertex_t index) const -> bool { return index < vertex_info_.size() && !is_zero_(index) && states_[thread_id].graph.has_value(index); } -template -auto DLPropagator::lower_bound(Clingo::id_t thread_id, vertex_t index) const -> value_t { +template auto DLPropagator::lower_bound(Clingo::id_t thread_id, vertex_t index) const -> value_t { assert(has_lower_bound(thread_id, index)); auto &state = states_[thread_id]; auto zero_vertex = zero_vertices_[vertex_info_[index].cc]; @@ -159,8 +140,7 @@ auto DLPropagator::lower_bound(Clingo::id_t thread_id, vertex_t index) const return state.graph.get_value(index) - adjust; } -template -void DLPropagator::extend_model(Clingo::Model &model) { +template void DLPropagator::extend_model(Clingo::Model &model) { auto &state = states_[model.thread_id()]; Clingo::SymbolVector vec; for (vertex_t idx = 0; idx < numeric_cast(vertex_info_.size()); ++idx) { @@ -176,8 +156,7 @@ void DLPropagator::extend_model(Clingo::Model &model) { model.extend(vec); } -template -void DLPropagator::init(Clingo::PropagateInit &init) { +template void DLPropagator::init(Clingo::PropagateInit &init) { if (!edges_.empty()) { init.set_check_mode(Clingo::PropagatorCheckMode::Partial); } @@ -208,8 +187,7 @@ void DLPropagator::init(Clingo::PropagateInit &init) { initialize_states_(init); } -template -void DLPropagator::propagate(Clingo::PropagateControl &ctl, Clingo::LiteralSpan changes) { +template void DLPropagator::propagate(Clingo::PropagateControl &ctl, Clingo::LiteralSpan changes) { // add facts for propagation at the next step if (ctl.assignment().decision_level() == 0) { auto &facts = facts_[ctl.thread_id()]; @@ -226,8 +204,7 @@ void DLPropagator::undo(Clingo::PropagateControl const &ctl, Clingo::LiteralS state.graph.backtrack(); } -template -void DLPropagator::check(Clingo::PropagateControl &ctl) { +template void DLPropagator::check(Clingo::PropagateControl &ctl) { ThreadState &state = states_[ctl.thread_id()]; auto &facts = facts_[ctl.thread_id()]; auto assignment = ctl.assignment(); @@ -240,7 +217,8 @@ void DLPropagator::check(Clingo::PropagateControl &ctl) { if (ctl.assignment().is_total()) { for (auto &x : edges_) { if (ctl.assignment().is_true(x.lit)) { - if (!state.graph.has_value(x.from) || !state.graph.has_value(x.to) || !(state.graph.get_value(x.from) - state.graph.get_value(x.to) <= x.weight)) { + if (!state.graph.has_value(x.from) || !state.graph.has_value(x.to) || + !(state.graph.get_value(x.from) - state.graph.get_value(x.to) <= x.weight)) { throw std::logic_error("not a valid solution"); } } @@ -249,8 +227,7 @@ void DLPropagator::check(Clingo::PropagateControl &ctl) { #endif } -template -vertex_t DLPropagator::map_vertex_(Clingo::Symbol symbol) { +template auto DLPropagator::map_vertex_(Clingo::Symbol symbol) -> vertex_t { auto [it, ins] = vert_map_inv_.emplace(symbol, numeric_cast(vertex_info_.size())); if (ins) { vertex_info_.emplace_back(it->first); @@ -258,8 +235,7 @@ vertex_t DLPropagator::map_vertex_(Clingo::Symbol symbol) { return it->second; } -template -bool DLPropagator::add_constraints_(Clingo::PropagateInit &init) { +template auto DLPropagator::add_constraints_(Clingo::PropagateInit &init) -> bool { for (auto atom : init.theory_atoms()) { auto term = atom.term(); if (match(term, "__diff_h", 0) || match(term, "__diff_b", 0)) { @@ -274,13 +250,13 @@ bool DLPropagator::add_constraints_(Clingo::PropagateInit &init) { } template -bool DLPropagator::normalize_constraint_(Clingo::PropagateInit &init, literal_t literal, CoVarVec const &elements, char const *op, T rhs, bool strict) { // NOLINT +auto DLPropagator::normalize_constraint_(Clingo::PropagateInit &init, literal_t literal, CoVarVec const &elements, + char const *op, T rhs, bool strict) -> bool { // NOLINT // rewrite '>', '<', and '>=' into '<=' if (std::strcmp(op, ">") == 0) { op = ">="; rhs = safe_add(rhs, epsilon()); - } - else if (std::strcmp(op, "<") == 0) { + } else if (std::strcmp(op, "<") == 0) { op = "<="; rhs = safe_sub(rhs, epsilon()); } @@ -299,15 +275,13 @@ bool DLPropagator::normalize_constraint_(Clingo::PropagateInit &init, literal if (!init.assignment().is_true(-literal) && !add_edges_(init, literal, elements, rhs, false)) { return false; } - } - else if (std::strcmp(op, "=") == 0) { + } else if (std::strcmp(op, "=") == 0) { literal_t a = 0; literal_t b = 0; if (strict) { if (init.assignment().is_true(literal)) { a = b = 1; - } - else { + } else { a = init.add_literal(); b = init.add_literal(); } @@ -322,8 +296,7 @@ bool DLPropagator::normalize_constraint_(Clingo::PropagateInit &init, literal if (!init.add_clause({-a, -b, literal})) { return false; } - } - else { + } else { a = b = literal; } @@ -337,8 +310,7 @@ bool DLPropagator::normalize_constraint_(Clingo::PropagateInit &init, literal if (strict) { return true; } - } - else if (std::strcmp(op, "!=") == 0) { + } else if (std::strcmp(op, "!=") == 0) { if (strict) { return normalize_constraint_(init, -literal, elements, "=", rhs, true); } @@ -372,8 +344,7 @@ bool DLPropagator::normalize_constraint_(Clingo::PropagateInit &init, literal if (std::strcmp(op, "<=") == 0) { op = ">"; - } - else if (std::strcmp(op, "!=") == 0) { + } else if (std::strcmp(op, "!=") == 0) { op = "="; } @@ -386,8 +357,10 @@ bool DLPropagator::normalize_constraint_(Clingo::PropagateInit &init, literal } template -bool DLPropagator::add_edges_(Clingo::PropagateInit& init, literal_t literal, CoVarVec const &covec, T rhs, bool strict) { - char const *msg = "normalizing difference constraint failed: only constraints of form &diff {u - v} <= b are accepted"; +auto DLPropagator::add_edges_(Clingo::PropagateInit &init, literal_t literal, CoVarVec const &covec, T rhs, + bool strict) -> bool { + char const *msg = + "normalizing difference constraint failed: only constraints of form &diff {u - v} <= b are accepted"; if (strict && init.assignment().is_false(literal)) { return true; } @@ -405,34 +378,27 @@ bool DLPropagator::add_edges_(Clingo::PropagateInit& init, literal_t literal, if (covec.size() == 1) { if (covec[0].first == 1) { u_id = covec[0].second; - } - else if (covec[0].first == -1) { + } else if (covec[0].first == -1) { v_id = covec[0].second; - } - else { + } else { throw std::runtime_error(msg); } - } - else if (covec.size() == 2) { + } else if (covec.size() == 2) { if (covec[0].first == 1) { u_id = covec[0].second; if (covec[1].first == -1) { v_id = covec[1].second; - } - else { + } else { throw std::runtime_error(msg); } - } - else if (covec[0].first == -1) { + } else if (covec[0].first == -1) { v_id = covec[0].second; if (covec[1].first == 1) { u_id = covec[1].second; - } - else { + } else { throw std::runtime_error(msg); } - } - else { + } else { throw std::runtime_error(msg); } } @@ -441,29 +407,31 @@ bool DLPropagator::add_edges_(Clingo::PropagateInit& init, literal_t literal, } template -void DLPropagator::add_edges_(Clingo::PropagateInit& init, vertex_t u_id, vertex_t v_id, value_t weight, literal_t lit, bool strict) { +void DLPropagator::add_edges_(Clingo::PropagateInit &init, vertex_t u_id, vertex_t v_id, value_t weight, + literal_t lit, bool strict) { add_edge_(init, u_id, v_id, weight, lit); if (strict) { - add_edge_(init, v_id, u_id, -weight-1, -lit); + add_edge_(init, v_id, u_id, -weight - 1, -lit); } } template -void DLPropagator::add_edge_(Clingo::PropagateInit &init, vertex_t u_id, vertex_t v_id, value_t weight, literal_t lit) { +void DLPropagator::add_edge_(Clingo::PropagateInit &init, vertex_t u_id, vertex_t v_id, value_t weight, + literal_t lit) { auto id = numeric_cast(edges_.size()); edges_.push_back({u_id, v_id, weight, lit}); lit_to_edges_.emplace(lit, id); for (int i = 0; i < init.number_of_threads(); ++i) { init.add_watch(lit, i); - if (conf_.get_propagate_mode(i) >= PropagationMode::Zero || conf_.get_propagate_root(i) > 0 || conf_.get_propagate_budget(i) > 0) { + if (conf_.get_propagate_mode(i) >= PropagationMode::Zero || conf_.get_propagate_root(i) > 0 || + conf_.get_propagate_budget(i) > 0) { disable_edges_ = true; init.add_watch(-lit, i); } } } -template -void DLPropagator::cc_reset_() { +template void DLPropagator::cc_reset_() { for (auto &info : vertex_info_) { info.set_visited(0, false); } @@ -472,19 +440,16 @@ void DLPropagator::cc_reset_() { } } -template -bool DLPropagator::cc_visited_(vertex_t index) const { +template auto DLPropagator::cc_visited_(vertex_t index) const -> bool { return vertex_info_[index].visited; } -template -bool DLPropagator::is_zero_(vertex_t index) const { +template auto DLPropagator::is_zero_(vertex_t index) const -> bool { assert(vertex_info_[index].cc < zero_vertices_.size()); return zero_vertices_[vertex_info_[index].cc] == index; } -template -void DLPropagator::cc_calculate_(AdjacencyMap &outgoing, AdjacencyMap &incoming) { +template void DLPropagator::cc_calculate_(AdjacencyMap &outgoing, AdjacencyMap &incoming) { index_t cc = 0; // Note that this marks zero vertices as visited. cc_reset_(); @@ -557,7 +522,8 @@ void DLPropagator::cc_calculate_(AdjacencyMap &outgoing, AdjacencyMap &incomi } template -void DLPropagator::calculate_mutexes_(Clingo::PropagateInit &init, edge_t edge_start, AdjacencyMap &outgoing) { // NOLINT +void DLPropagator::calculate_mutexes_(Clingo::PropagateInit &init, edge_t edge_start, + AdjacencyMap &outgoing) { // NOLINT // let r and s be edge literals and T be the true literal: // // r T @@ -601,7 +567,8 @@ void DLPropagator::calculate_mutexes_(Clingo::PropagateInit &init, edge_t edg auto st_id = it->second; auto &st = edges_[st_id]; auto st_truth = ass.truth_value(st.lit); - if ((st_id > start_id && st_truth == Clingo::TruthValue::Free) || st_truth == Clingo::TruthValue::False) { + if ((st_id > start_id && st_truth == Clingo::TruthValue::Free) || + st_truth == Clingo::TruthValue::False) { continue; } auto w = rs_state.weight + st.weight; @@ -638,8 +605,7 @@ void DLPropagator::calculate_mutexes_(Clingo::PropagateInit &init, edge_t edg return; } clause.clear(); - } - else if (n < conf_.mutex_size && queue.size() < conf_.mutex_cutoff) { + } else if (n < conf_.mutex_size && queue.size() < conf_.mutex_cutoff) { queue.emplace_back(State{w, st_id, n, queue_offset}); } } @@ -648,21 +614,20 @@ void DLPropagator::calculate_mutexes_(Clingo::PropagateInit &init, edge_t edg } } -template -void DLPropagator::initialize_states_(Clingo::PropagateInit &init) { +template void DLPropagator::initialize_states_(Clingo::PropagateInit &init) { states_.clear(); stats_.thread_statistics.resize(init.number_of_threads()); if (facts_.size() < numeric_cast(init.number_of_threads())) { facts_.resize(init.number_of_threads()); } for (Clingo::id_t i = 0; i < numeric_cast(init.number_of_threads()); ++i) { - states_.emplace_back(stats_.thread_statistics[i], edges_, conf_.get_propagate_mode(i), conf_.get_propagate_root(i), conf_.get_propagate_budget(i)); + states_.emplace_back(stats_.thread_statistics[i], edges_, conf_.get_propagate_mode(i), + conf_.get_propagate_root(i), conf_.get_propagate_budget(i)); facts_[i].limit = facts_[i].lits.size(); } } -template -void DLPropagator::disable_edge_by_lit(ThreadState &state, literal_t lit) { +template void DLPropagator::disable_edge_by_lit(ThreadState &state, literal_t lit) { if (disable_edges_) { for (auto it = lit_to_edges_.find(-lit), ie = lit_to_edges_.end(); it != ie && it->first == -lit; ++it) { if (state.graph.edge_is_enabled(it->second)) { @@ -672,19 +637,16 @@ void DLPropagator::disable_edge_by_lit(ThreadState &state, literal_t lit) { } } -template -auto DLPropagator::get_potential_(Graph const &graph, vertex_t index) const -> value_t { +template auto DLPropagator::get_potential_(Graph const &graph, vertex_t index) const -> value_t { return graph.has_value(index) ? -graph.get_value(index) : 0; } -template -auto DLPropagator::cost_(Graph const &graph, Edge const &edge) const -> value_t { +template auto DLPropagator::cost_(Graph const &graph, Edge const &edge) const -> value_t { return get_potential_(graph, edge.from) + edge.weight - get_potential_(graph, edge.to); } -template -auto DLPropagator::cost_(SortMode mode, Graph const &graph, edge_t index) const -> value_t { - switch(mode) { +template auto DLPropagator::cost_(SortMode mode, Graph const &graph, edge_t index) const -> value_t { + switch (mode) { case SortMode::Weight: { return edges_[index].weight; } @@ -704,11 +666,9 @@ auto DLPropagator::cost_(SortMode mode, Graph const &graph, edge_t index) con return 0; } -template -void DLPropagator::sort_edges(SortMode mode, ThreadState &state) { - std::sort(state.todo_edges.begin(), state.todo_edges.end(), [&](edge_t l, edge_t r) { - return cost_(mode, state.graph, l) < cost_(mode, state.graph, r); - }); +template void DLPropagator::sort_edges(SortMode mode, ThreadState &state) { + std::sort(state.todo_edges.begin(), state.todo_edges.end(), + [&](edge_t l, edge_t r) { return cost_(mode, state.graph, l) < cost_(mode, state.graph, r); }); } template @@ -759,8 +719,7 @@ void DLPropagator::do_propagate(Clingo::PropagateControl &ctl, Clingo::Litera auto ie = lit_to_edges_.end(); if (state.graph.can_propagate()) { disable_edge_by_lit(state, lit); - } - else if (it == ie) { + } else if (it == ie) { state.removed_watchs.emplace_back(lit); ctl.remove_watch(lit); } @@ -776,7 +735,9 @@ void DLPropagator::do_propagate(Clingo::PropagateControl &ctl, Clingo::Litera for (auto edge_idx : state.todo_edges) { if (state.graph.edge_is_enabled(edge_idx)) { // disable propagation once budget exceeded - bool has_budget = state.propagate_budget > 0 && state.stats.propagate_cost_add + state.propagate_budget > state.stats.propagate_cost_from + state.stats.propagate_cost_to; + bool has_budget = + state.propagate_budget > 0 && state.stats.propagate_cost_add + state.propagate_budget > + state.stats.propagate_cost_from + state.stats.propagate_cost_to; if (!propagate && !has_budget) { state.graph.disable_propagate(); } @@ -791,7 +752,7 @@ void DLPropagator::do_propagate(Clingo::PropagateControl &ctl, Clingo::Litera } template -literal_t DLPropagator::decide(id_t thread_id, Clingo::Assignment const &assign, literal_t fallback) { +auto DLPropagator::decide(id_t thread_id, Clingo::Assignment const &assign, literal_t fallback) -> literal_t { static_cast(assign); if (conf_.decision_mode == DecisionMode::Disabled) { return fallback; diff --git a/libclingo-dl/src/theory.cc b/libclingo-dl/src/theory.cc index 724ed92d..25325979 100644 --- a/libclingo-dl/src/theory.cc +++ b/libclingo-dl/src/theory.cc @@ -33,22 +33,19 @@ constexpr double DOUBLE_EPSILON = 0.00001; //! Epsilon value for integral numbers. template , bool>::type = true> -[[nodiscard]] T epsilon_() { +[[nodiscard]] auto epsilon_() -> T { return 1; } //! Epsilon value for floating point numbers. template , bool>::type = true> -[[nodiscard]] T epsilon_() { +[[nodiscard]] auto epsilon_() -> T { return DOUBLE_EPSILON; } } // namespace -template -T epsilon() { - return epsilon_(); -} +template auto epsilon() -> T { return epsilon_(); } template int epsilon(); template double epsilon(); diff --git a/libclingo-dl/tests/optimize.cc b/libclingo-dl/tests/optimize.cc index 60da44da..f37fc903 100644 --- a/libclingo-dl/tests/optimize.cc +++ b/libclingo-dl/tests/optimize.cc @@ -22,11 +22,11 @@ // // }}} -#include +#include +#include #include #include -#include -#include +#include namespace ClingoDL { @@ -34,18 +34,14 @@ namespace { //! Helper class to extract the last model while solving. class SolveHandler : public Clingo::SolveEventHandler { -public: - SolveHandler(clingodl_theory_t *theory) - : theory_{theory} { - } + public: + SolveHandler(clingodl_theory_t *theory) : theory_{theory} {} //! Return the symbols in the last model found while solving. - [[nodiscard]] Clingo::SymbolVector const &symbols() const { - return symbols_; - } + [[nodiscard]] auto symbols() const -> Clingo::SymbolVector const & { return symbols_; } -private: + private: //! Stores the last model. - bool on_model(Clingo::Model &model) override { + auto on_model(Clingo::Model &model) -> bool override { REQUIRE(clingodl_on_model(theory_, model.to_c())); symbols_ = model.symbols(Clingo::ShowType::Theory); std::sort(symbols_.begin(), symbols_.end()); @@ -69,12 +65,12 @@ void parse_program(clingodl_theory_t *theory, Clingo::Control &ctl, const char * } //! Create symbols representing DL assignments. -Clingo::Symbol assign(Clingo::Symbol name, int value) { +auto assign(Clingo::Symbol name, int value) -> Clingo::Symbol { return Clingo::Function("dl", {name, Clingo::Number(value)}); } //! Run the optimization algorithm minimizing the given variable. -Clingo::SymbolVector optimize(Clingo::Control &ctl, Clingo::Symbol bound, double factor, char const *prg) { +auto optimize(Clingo::Control &ctl, Clingo::Symbol bound, double factor, char const *prg) -> Clingo::SymbolVector { clingodl_theory_t *theory{nullptr}; REQUIRE(clingodl_create(&theory)); REQUIRE(clingodl_register(theory, ctl.to_c())); @@ -99,11 +95,10 @@ TEST_CASE("optimize", "[clingo-dl]") { // NOLINT for (auto factor : {1.0, 2.0, 4.0, 8.0, 16.0, 32.0, 64.0, 128.0, 256.0, 512.0, 1024.0}) { Clingo::Control ctl{{"1"}}; Clingo::SymbolVector ret{assign(a, 100), assign(b, -50)}; // NOLINT - REQUIRE(optimize( - ctl, b, factor, - "&diff { a - 0 } >= 100.\n" - "&diff { b - 0 } >= -100.\n" - "&diff { a - b } <= 150.\n") == ret); + REQUIRE(optimize(ctl, b, factor, + "&diff { a - 0 } >= 100.\n" + "&diff { b - 0 } >= -100.\n" + "&diff { a - b } <= 150.\n") == ret); REQUIRE(ctl.statistics()["user_step"]["DifferenceLogic"].has_subkey("Optimization")); REQUIRE(ctl.statistics()["user_step"]["DifferenceLogic"]["Optimization"].value() == -50); } @@ -111,11 +106,11 @@ TEST_CASE("optimize", "[clingo-dl]") { // NOLINT SECTION("unsat") { Clingo::Control ctl{{"1"}}; REQUIRE(optimize( // NOLINT - ctl, b, 1.0, - "&diff { a - 0 } >= 100.\n" - "&diff { b - 0 } >= -100.\n" - "&diff { a - b } <= 150.\n" - "&diff { b - 0 } < -50.\n") == Clingo::SymbolVector{}); + ctl, b, 1.0, + "&diff { a - 0 } >= 100.\n" + "&diff { b - 0 } >= -100.\n" + "&diff { a - b } <= 150.\n" + "&diff { b - 0 } < -50.\n") == Clingo::SymbolVector{}); REQUIRE(!ctl.statistics()["user_step"]["DifferenceLogic"].has_subkey("Optimization")); } } diff --git a/libclingo-dl/tests/parsing.cc b/libclingo-dl/tests/parsing.cc index 3a6b993d..d4448789 100644 --- a/libclingo-dl/tests/parsing.cc +++ b/libclingo-dl/tests/parsing.cc @@ -22,11 +22,11 @@ // // }}} -#include -#include #include -#include +#include +#include #include +#include namespace ClingoDL { @@ -37,14 +37,13 @@ using V = std::vector; //! Parse the theory atoms in the given program and return their string //! representations. -V parse(char const *prg) { +auto parse(char const *prg) -> V { Clingo::Control ctl; { Clingo::AST::ProgramBuilder builder{ctl}; Clingo::AST::parse_string(prg, [&](Clingo::AST::Node const &ast) { - transform(ast, [&](Clingo::AST::Node &&trans) { - builder.add(trans); - }, true); + transform( + ast, [&](Clingo::AST::Node &&trans) { builder.add(trans); }, true); }); } ctl.add("base", {}, THEORY); diff --git a/libclingo-dl/tests/solve.cc b/libclingo-dl/tests/solve.cc index 703f040c..cdd02ee9 100644 --- a/libclingo-dl/tests/solve.cc +++ b/libclingo-dl/tests/solve.cc @@ -22,11 +22,11 @@ // // }}} -#include +#include +#include #include #include -#include -#include +#include namespace ClingoDL { @@ -91,70 +91,66 @@ bound(104). )"; //! Create a symbol for sequence atoms of task/machine pairs. -Clingo::Symbol seq(int a, int b, int c, int d, int e) { - return Clingo::Function("seq", { - Clingo::Function("", {Clingo::Number(a), Clingo::Number(b)}), - Clingo::Function("", {Clingo::Number(c), Clingo::Number(d)}), - Clingo::Number(e) - }); +auto seq(int a, int b, int c, int d, int e) -> Clingo::Symbol { + return Clingo::Function("seq", {Clingo::Function("", {Clingo::Number(a), Clingo::Number(b)}), + Clingo::Function("", {Clingo::Number(c), Clingo::Number(d)}), Clingo::Number(e)}); } //! A DL assignment for task/machine pairs. -A ass(int a, int b, int c) { - return A(Clingo::Function("", {Clingo::Number(a), Clingo::Number(b)}), c); -} +auto ass(int a, int b, int c) -> A { return A(Clingo::Function("", {Clingo::Number(a), Clingo::Number(b)}), c); } //! Solutions to the task assignment problem. RV const SOLS = {SP{{ - ass(1, 1, 100), ass(1, 2, 0), ass(1, 3, 34), ass(1, 4, 95), // NOLINT - ass(2, 1, 95), ass(2, 2, 72), ass(2, 3, 104), ass(2, 4, 0), // NOLINT - ass(3, 1, 34), ass(3, 2, 0), ass(3, 3, 72), ass(3, 4, 104) // NOLINT - }, { - seq(1, 2, 1, 1, 34), seq(1, 2, 1, 3, 34), seq(1, 2, 1, 4, 34), // NOLINT - seq(1, 2, 2, 2, 34), seq(1, 2, 3, 1, 34), seq(1, 3, 1, 1, 61), // NOLINT - seq(1, 3, 1, 4, 61), seq(1, 3, 2, 1, 61), seq(1, 3, 3, 4, 61), // NOLINT - seq(1, 4, 1, 1, 2), seq(1, 4, 2, 3, 2), // NOLINT - seq(2, 1, 2, 3, 9), seq(2, 1, 3, 4, 9), seq(2, 2, 2, 1, 15), // NOLINT - seq(2, 2, 2, 3, 15), seq(2, 4, 1, 1, 70), seq(2, 4, 2, 1, 70), // NOLINT - seq(2, 4, 2, 2, 70), seq(2, 4, 2, 3, 70), seq(2, 4, 3, 3, 70), // NOLINT - seq(3, 1, 2, 2, 38), seq(3, 1, 3, 3, 38), seq(3, 1, 3, 4, 38), // NOLINT - seq(3, 2, 1, 4, 19), seq(3, 2, 2, 3, 19), seq(3, 2, 3, 1, 19), // NOLINT - seq(3, 2, 3, 3, 19), seq(3, 2, 3, 4, 19), seq(3, 3, 1, 1, 28), // NOLINT - seq(3, 3, 3, 4, 28), // NOLINT - }}, SP{{ - ass(1, 1, 104), ass(1, 2, 70), ass(1, 3, 9), ass(1, 4, 0), // NOLINT - ass(2, 1, 0), ass(2, 2, 9), ass(2, 3, 98), ass(2, 4, 28), // NOLINT - ass(3, 1, 28), ass(3, 2, 66), ass(3, 3, 0), ass(3, 4, 85) // NOLINT - }, { - seq(1, 2, 1, 1, 34), seq(1, 3, 1, 1, 61), seq(1, 3, 1, 2, 61), // NOLINT - seq(1, 3, 3, 4, 61), seq(1, 4, 1, 1, 2), seq(1, 4, 1, 2, 2), // NOLINT - seq(1, 4, 1, 3, 2), seq(1, 4, 2, 3, 2), seq(1, 4, 3, 2, 2), // NOLINT - seq(2, 1, 1, 3, 9), seq(2, 1, 2, 2, 9), seq(2, 1, 2, 3, 9), // NOLINT - seq(2, 1, 2, 4, 9), seq(2, 1, 3, 4, 9), seq(2, 2, 1, 2, 15), // NOLINT - seq(2, 2, 2, 3, 15), seq(2, 2, 2, 4, 15), seq(2, 2, 3, 1, 15), // NOLINT - seq(2, 4, 1, 1, 70), seq(2, 4, 2, 3, 70), seq(3, 1, 1, 2, 38), // NOLINT - seq(3, 1, 3, 2, 38), seq(3, 1, 3, 4, 38), seq(3, 2, 2, 3, 19), // NOLINT - seq(3, 2, 3, 4, 19), seq(3, 3, 1, 1, 28), seq(3, 3, 2, 4, 28), // NOLINT - seq(3, 3, 3, 1, 28), seq(3, 3, 3, 2, 28), seq(3, 3, 3, 4, 28), // NOLINT -}}}; + ass(1, 1, 100), ass(1, 2, 0), ass(1, 3, 34), ass(1, 4, 95), // NOLINT + ass(2, 1, 95), ass(2, 2, 72), ass(2, 3, 104), ass(2, 4, 0), // NOLINT + ass(3, 1, 34), ass(3, 2, 0), ass(3, 3, 72), ass(3, 4, 104) // NOLINT + }, + { + seq(1, 2, 1, 1, 34), seq(1, 2, 1, 3, 34), seq(1, 2, 1, 4, 34), // NOLINT + seq(1, 2, 2, 2, 34), seq(1, 2, 3, 1, 34), seq(1, 3, 1, 1, 61), // NOLINT + seq(1, 3, 1, 4, 61), seq(1, 3, 2, 1, 61), seq(1, 3, 3, 4, 61), // NOLINT + seq(1, 4, 1, 1, 2), seq(1, 4, 2, 3, 2), // NOLINT + seq(2, 1, 2, 3, 9), seq(2, 1, 3, 4, 9), seq(2, 2, 2, 1, 15), // NOLINT + seq(2, 2, 2, 3, 15), seq(2, 4, 1, 1, 70), seq(2, 4, 2, 1, 70), // NOLINT + seq(2, 4, 2, 2, 70), seq(2, 4, 2, 3, 70), seq(2, 4, 3, 3, 70), // NOLINT + seq(3, 1, 2, 2, 38), seq(3, 1, 3, 3, 38), seq(3, 1, 3, 4, 38), // NOLINT + seq(3, 2, 1, 4, 19), seq(3, 2, 2, 3, 19), seq(3, 2, 3, 1, 19), // NOLINT + seq(3, 2, 3, 3, 19), seq(3, 2, 3, 4, 19), seq(3, 3, 1, 1, 28), // NOLINT + seq(3, 3, 3, 4, 28), // NOLINT + }}, + SP{{ + ass(1, 1, 104), ass(1, 2, 70), ass(1, 3, 9), ass(1, 4, 0), // NOLINT + ass(2, 1, 0), ass(2, 2, 9), ass(2, 3, 98), ass(2, 4, 28), // NOLINT + ass(3, 1, 28), ass(3, 2, 66), ass(3, 3, 0), ass(3, 4, 85) // NOLINT + }, + { + seq(1, 2, 1, 1, 34), seq(1, 3, 1, 1, 61), seq(1, 3, 1, 2, 61), // NOLINT + seq(1, 3, 3, 4, 61), seq(1, 4, 1, 1, 2), seq(1, 4, 1, 2, 2), // NOLINT + seq(1, 4, 1, 3, 2), seq(1, 4, 2, 3, 2), seq(1, 4, 3, 2, 2), // NOLINT + seq(2, 1, 1, 3, 9), seq(2, 1, 2, 2, 9), seq(2, 1, 2, 3, 9), // NOLINT + seq(2, 1, 2, 4, 9), seq(2, 1, 3, 4, 9), seq(2, 2, 1, 2, 15), // NOLINT + seq(2, 2, 2, 3, 15), seq(2, 2, 2, 4, 15), seq(2, 2, 3, 1, 15), // NOLINT + seq(2, 4, 1, 1, 70), seq(2, 4, 2, 3, 70), seq(3, 1, 1, 2, 38), // NOLINT + seq(3, 1, 3, 2, 38), seq(3, 1, 3, 4, 38), seq(3, 2, 2, 3, 19), // NOLINT + seq(3, 2, 3, 4, 19), seq(3, 3, 1, 1, 28), seq(3, 3, 2, 4, 28), // NOLINT + seq(3, 3, 3, 1, 28), seq(3, 3, 3, 2, 28), seq(3, 3, 3, 4, 28), // NOLINT + }}}; //! A handler to gather statistics in a DL theory. class Handler : public Clingo::SolveEventHandler { -public: - Handler(clingodl_theory_t *theory) - : theory_{theory} { - } + public: + Handler(clingodl_theory_t *theory) : theory_{theory} {} //! Add theory specific statistics. void on_statistics(Clingo::UserStatistics step, Clingo::UserStatistics accu) override { clingodl_on_statistics(theory_, step.to_c(), accu.to_c()); } -private: + private: clingodl_theory_t *theory_; //!< The DL theory. }; //! Solve a given DL problem returning all models. -RV solve(clingodl_theory_t *theory, Clingo::Control &ctl) { +auto solve(clingodl_theory_t *theory, Clingo::Control &ctl) -> RV { Handler h{theory}; using namespace Clingo; RV result; @@ -164,16 +160,14 @@ RV solve(clingodl_theory_t *theory, Clingo::Control &ctl) { auto &sol_bool = result.back().second; auto id = m.thread_id(); size_t index{0}; - for (clingodl_assignment_begin(theory, id, &index); clingodl_assignment_next(theory, id, &index); ) { + for (clingodl_assignment_begin(theory, id, &index); clingodl_assignment_next(theory, id, &index);) { clingodl_value_t value; clingodl_assignment_get_value(theory, id, index, &value); if (value.type == clingodl_value_type_int) { sol.emplace_back(Symbol{clingodl_get_symbol(theory, index)}, value.int_number); // NOLINT - } - else if (value.type == clingodl_value_type_double) { + } else if (value.type == clingodl_value_type_double) { sol.emplace_back(Symbol{clingodl_get_symbol(theory, index)}, value.double_number); // NOLINT - } - else { + } else { REQUIRE(false); } } @@ -209,53 +203,53 @@ TEST_CASE("solving", "[clingo]") { // NOLINT SECTION("solve") { REQUIRE(clingodl_register(theory, ctl.to_c())); parse_program(theory, ctl, - "#program base.\n" - "1 { a; b } 1. &diff { a - b } <= 3.\n" - "&diff { 0 - a } <= -5 :- a.\n" - "&diff { 0 - b } <= -7 :- b.\n"); + "#program base.\n" + "1 { a; b } 1. &diff { a - b } <= 3.\n" + "&diff { 0 - a } <= -5 :- a.\n" + "&diff { 0 - b } <= -7 :- b.\n"); ctl.ground({{"base", {}}}); REQUIRE(clingodl_prepare(theory, ctl.to_c())); auto result = solve(theory, ctl); - REQUIRE(result == (RV{{{{a, 0}, {b, 7}},{b}}, {{{a, 5}, {b, 2}},{a}}})); + REQUIRE(result == (RV{{{{a, 0}, {b, 7}}, {b}}, {{{a, 5}, {b, 2}}, {a}}})); parse_program(theory, ctl, - "#program ext.\n" - "&diff { a - 0 } <= 4.\n"); + "#program ext.\n" + "&diff { a - 0 } <= 4.\n"); ctl.ground({{"ext", {}}}); REQUIRE(clingodl_prepare(theory, ctl.to_c())); result = solve(theory, ctl); - REQUIRE(result == (RV{{{{a, 0}, {b, 7}},{b}}})); + REQUIRE(result == (RV{{{{a, 0}, {b, 7}}, {b}}})); } SECTION("unequal") { REQUIRE(clingodl_register(theory, ctl.to_c())); parse_program(theory, ctl, - "#program base.\n" - "{ a }. &diff { b } != 5 :- not a.\n"); + "#program base.\n" + "{ a }. &diff { b } != 5 :- not a.\n"); ctl.ground({{"base", {}}}); REQUIRE(clingodl_prepare(theory, ctl.to_c())); auto result = solve(theory, ctl); - REQUIRE(result == (RV{{{},{a}}, {{{b, 0}},{}},{{{b, 6}},{}}})); + REQUIRE(result == (RV{{{}, {a}}, {{{b, 0}}, {}}, {{{b, 6}}, {}}})); } SECTION("cc") { REQUIRE(clingodl_register(theory, ctl.to_c())); parse_program(theory, ctl, - "#program base.\n" - "&diff { 0 - a } <= -5.\n" - "&diff { 0 - b } <= -10.\n"); + "#program base.\n" + "&diff { 0 - a } <= -5.\n" + "&diff { 0 - b } <= -10.\n"); ctl.ground({{"base", {}}}); REQUIRE(clingodl_prepare(theory, ctl.to_c())); auto result = solve(theory, ctl); - REQUIRE(result == (RV{{{{a, 5}, {b, 10}},{}}})); + REQUIRE(result == (RV{{{{a, 5}, {b, 10}}, {}}})); REQUIRE(ctl.statistics()["user_step"]["DifferenceLogic"]["CCs"] == 2); parse_program(theory, ctl, - "#program ext.\n" - "&diff { b - a } <= 3.\n"); + "#program ext.\n" + "&diff { b - a } <= 3.\n"); ctl.ground({{"ext", {}}}); REQUIRE(clingodl_prepare(theory, ctl.to_c())); result = solve(theory, ctl); - REQUIRE(result == (RV{{{{a, 7}, {b, 10}},{}}})); + REQUIRE(result == (RV{{{{a, 7}, {b, 10}}, {}}})); REQUIRE(ctl.statistics()["user_step"]["DifferenceLogic"]["CCs"] == 1); } @@ -264,59 +258,55 @@ TEST_CASE("solving", "[clingo]") { // NOLINT REQUIRE(clingodl_register(theory, ctl.to_c())); parse_program(theory, ctl, - "#program base.\n" - "&diff { a - 0 } <= 0.\n" - "a :- &diff { a - 0 } <= 0.\n" - "b :- &diff { 0 - a } <= -1.\n" - "c :- &diff { a } <= -1.\n" - ); + "#program base.\n" + "&diff { a - 0 } <= 0.\n" + "a :- &diff { a - 0 } <= 0.\n" + "b :- &diff { 0 - a } <= -1.\n" + "c :- &diff { a } <= -1.\n"); ctl.ground({{"base", {}}}); REQUIRE(clingodl_prepare(theory, ctl.to_c())); auto result = solve(theory, ctl); - REQUIRE(result == (RV{{{{a, -1}},{a, c}},{{{a, 0}},{a}}})); + REQUIRE(result == (RV{{{{a, -1}}, {a, c}}, {{{a, 0}}, {a}}})); } SECTION("rdl") { REQUIRE(clingodl_configure(theory, "rdl", "yes")); REQUIRE(clingodl_register(theory, ctl.to_c())); parse_program(theory, ctl, - "#program base.\n" - "&diff { a } >= \"0.5\" * 3.\n" - ); + "#program base.\n" + "&diff { a } >= \"0.5\" * 3.\n"); ctl.ground({{"base", {}}}); REQUIRE(clingodl_prepare(theory, ctl.to_c())); auto result = solve(theory, ctl); - REQUIRE(result == (RV{{{{a, 1.5}},{}}})); // NOLINT + REQUIRE(result == (RV{{{{a, 1.5}}, {}}})); // NOLINT } SECTION("parse") { REQUIRE(clingodl_register(theory, ctl.to_c())); parse_program(theory, ctl, - "#program base.\n" - "&diff { p( 1 + 2 ) - q( 3 * 4 - 7 ) } <= 3 - \"9.0\".\n" - ); + "#program base.\n" + "&diff { p( 1 + 2 ) - q( 3 * 4 - 7 ) } <= 3 - \"9.0\".\n"); ctl.ground({{"base", {}}}); REQUIRE(clingodl_prepare(theory, ctl.to_c())); auto result = solve(theory, ctl); auto p = Clingo::parse_term("p(3)"); auto q = Clingo::parse_term("q(5)"); - REQUIRE(result == (RV{{{{p, 0}, {q, 6}},{}}})); + REQUIRE(result == (RV{{{{p, 0}, {q, 6}}, {}}})); } SECTION("normalize") { REQUIRE(clingodl_register(theory, ctl.to_c())); parse_program(theory, ctl, - "#program base.\n" - "&diff { a } = b.\n" - "&diff { 5 } >= 0.\n" - "&diff { b } > c.\n" - "&diff { c } >= d + 1.\n" - "&diff { e } != (f,f).\n" - ); + "#program base.\n" + "&diff { a } = b.\n" + "&diff { 5 } >= 0.\n" + "&diff { b } > c.\n" + "&diff { c } >= d + 1.\n" + "&diff { e } != (f,f).\n"); ctl.ground({{"base", {}}}); REQUIRE(clingodl_prepare(theory, ctl.to_c())); @@ -326,36 +316,35 @@ TEST_CASE("solving", "[clingo]") { // NOLINT auto d = Id("d"); auto e = Id("e"); auto f = Function("", {Id("f"), Id("f")}); - REQUIRE(result == (RV{{{{a, 2}, {b, 2}, {c, 1}, {d, 0}, {e, 0}, {f, 1}}, {}}, {{{a, 2}, {b, 2},{c, 1},{d, 0}, {e, 1}, {f, 0}}, {}}})); + REQUIRE(result == (RV{{{{a, 2}, {b, 2}, {c, 1}, {d, 0}, {e, 0}, {f, 1}}, {}}, + {{{a, 2}, {b, 2}, {c, 1}, {d, 0}, {e, 1}, {f, 0}}, {}}})); } SECTION("empty constraints") { REQUIRE(clingodl_register(theory, ctl.to_c())); parse_program(theory, ctl, - "#program base.\n" - "a :- &diff { a - a } <= 5.\n" - "{ b }.\n" - "&diff { 0 } < -4 :- b.\n" - ); + "#program base.\n" + "a :- &diff { a - a } <= 5.\n" + "{ b }.\n" + "&diff { 0 } < -4 :- b.\n"); ctl.ground({{"base", {}}}); REQUIRE(clingodl_prepare(theory, ctl.to_c())); auto result = solve(theory, ctl); - REQUIRE(result == (RV{{{},{a}}})); + REQUIRE(result == (RV{{{}, {a}}})); REQUIRE(ctl.statistics()["solving"]["solvers"]["choices"] == 0); } SECTION("symbols") { REQUIRE(clingodl_register(theory, ctl.to_c())); parse_program(theory, ctl, - "#program base.\n" - "&diff{ (\"foo\\\\\\nbar\\\"foo\",123) - 0 } <= 17.\n" - ); + "#program base.\n" + "&diff{ (\"foo\\\\\\nbar\\\"foo\",123) - 0 } <= 17.\n"); ctl.ground({{"base", {}}}); REQUIRE(clingodl_prepare(theory, ctl.to_c())); auto result = solve(theory, ctl); - REQUIRE(result == (RV{{{{Function("",{String("foo\\\nbar\"foo"), Number(123)}), 0}},{}}})); + REQUIRE(result == (RV{{{{Function("", {String("foo\\\nbar\"foo"), Number(123)}), 0}}, {}}})); } clingodl_destroy(theory); }