From 39768da837935032aeb2fe530b87e63e59a89beb Mon Sep 17 00:00:00 2001 From: Benjamin Kaufmann Date: Fri, 17 Jan 2025 18:40:08 +0100 Subject: [PATCH] Minor fixes. * Fix some typos and add missing return to UniqueVector::operator=. --- app/main.cc | 2 +- libclingcon/clingcon.h | 2 +- libclingcon/clingcon/base.hh | 8 +++--- libclingcon/clingcon/constraints.hh | 8 +++--- libclingcon/clingcon/solver.hh | 42 ++++++++++++++--------------- libclingcon/clingcon/util.hh | 9 ++++--- libclingcon/src/clingcon.cc | 3 +-- libclingcon/src/constraints.cc | 22 +++++++-------- libclingcon/src/parsing.cc | 8 +++--- libclingcon/src/propagator.cc | 4 +-- libclingcon/src/solver.cc | 14 +++++----- 11 files changed, 61 insertions(+), 61 deletions(-) diff --git a/app/main.cc b/app/main.cc index a8456c1..1de11f8 100644 --- a/app/main.cc +++ b/app/main.cc @@ -2,7 +2,7 @@ #include #include #include -#include +#include #ifdef CLINGCON_PROFILE #include diff --git a/libclingcon/clingcon.h b/libclingcon/clingcon.h index 5709acf..af972cc 100644 --- a/libclingcon/clingcon.h +++ b/libclingcon/clingcon.h @@ -116,7 +116,7 @@ CLINGCON_VISIBILITY_DEFAULT bool clingcon_prepare(clingcon_theory_t *theory, cli //! Destroy the theory. //! -//! Currently no way to unregister a theory. +//! Currently, there is no way to unregister a theory. CLINGCON_VISIBILITY_DEFAULT bool clingcon_destroy(clingcon_theory_t *theory); //! Configure theory manually (without using clingo's options facility). diff --git a/libclingcon/clingcon/base.hh b/libclingcon/clingcon/base.hh index cc4fc8a..136e023 100644 --- a/libclingcon/clingcon/base.hh +++ b/libclingcon/clingcon/base.hh @@ -43,7 +43,7 @@ using var_t = uint32_t; //!< indexes of variables using val_t = int32_t; //!< type for values of variables and coefficients using sum_t = int64_t; //!< type for summing up values using nsum_t = math::wide_integer::int128_t; //!< type for summing up values of nonlinear terms -using co_var_t = std::pair; //!< coeffcient/variable pair +using co_var_t = std::pair; //!< coefficient/variable pair using CoVarVec = std::vector; enum class Heuristic : val_t { None, MaxChain }; @@ -54,7 +54,7 @@ enum class Heuristic : val_t { None, MaxChain }; //! MAX_VAL-MIN_VAL does not overflow and we can always add 1 even to the //! difference. constexpr val_t MAX_VAL = std::numeric_limits::max() / 2; -//! The minimum value for variables/coefficionts in clingcon. +//! The minimum value for variables/coefficients in clingcon. //! //! The minimum is chosen so that the product of two values will always fit //! into Clingcon::sum_t. @@ -96,7 +96,7 @@ template inline auto check_valid_value(I val) -> val_t { } return val; } -static_assert(std::is_same::value); +static_assert(std::is_same_v); //! Solver specific statistics. struct SolverStatistics { @@ -263,7 +263,7 @@ class AbstractClauseCreator { //! Call unit propagation on the solver. virtual auto propagate() -> bool = 0; - //! Add the given clause to the sovler. + //! Add the given clause to the solver. virtual auto add_clause(Clingo::LiteralSpan clause, Clingo::ClauseType type = Clingo::ClauseType::Learnt) -> bool = 0; diff --git a/libclingcon/clingcon/constraints.hh b/libclingcon/clingcon/constraints.hh index 225c81a..afe6545 100644 --- a/libclingcon/clingcon/constraints.hh +++ b/libclingcon/clingcon/constraints.hh @@ -67,7 +67,7 @@ class SumConstraint final : public AbstractConstraint { //! Get the literal associated with the constraint. [[nodiscard]] auto literal() const -> lit_t override { return lit_; } - //! Get the rhs of the consraint. + //! Get the rhs of the constraint. [[nodiscard]] auto rhs() const -> val_t { return rhs_; } //! Get the number of elements in the constraint. @@ -126,13 +126,13 @@ class NonlinearConstraint final : public AbstractConstraint { [[nodiscard]] auto var_x() const -> var_t { return var_x_; } //! Get the second variable of the nonlinear term. [[nodiscard]] auto var_y() const -> var_t { return var_y_; } - //! Check if the costraint has a linear term. + //! Check if the constraint has a linear term. [[nodiscard]] auto has_co_c() const -> bool { return co_b_ != 0; } //! Get the coefficient of the linear term. [[nodiscard]] auto co_b() const -> val_t { return co_b_; } //! Get the variable of the linear term. [[nodiscard]] auto var_z() const -> var_t { return var_z_; } - //! Get the rhs of the consraint. + //! Get the rhs of the constraint. [[nodiscard]] auto rhs() const -> val_t { return rhs_; } private: @@ -175,7 +175,7 @@ class MinimizeConstraint final : public AbstractConstraint { //! Get the literal associated with the constraint. [[nodiscard]] auto literal() const -> lit_t override { return TRUE_LIT; } - //! Get the adjustment of the consraint. + //! Get the adjustment of the constraint. [[nodiscard]] auto adjust() const -> val_t { return adjust_; } //! Get the number of elements in the constraint. diff --git a/libclingcon/clingcon/solver.hh b/libclingcon/clingcon/solver.hh index 1696306..13edfba 100644 --- a/libclingcon/clingcon/solver.hh +++ b/libclingcon/clingcon/solver.hh @@ -92,7 +92,7 @@ class AbstractConstraintState { //! @} - //! @name Functions for Constraint Progation + //! @name Functions for Constraint Propagation //! @{ //! Inform the solver about updated bounds of a variable. @@ -102,7 +102,7 @@ class AbstractConstraintState { [[nodiscard]] virtual auto update(val_t i, val_t diff) -> bool = 0; //! Similar to update but when the bound of a variable is backtracked. virtual void undo(val_t i, val_t diff) = 0; - //! Prepagates the constraint. + //! Propagates the constraint. [[nodiscard]] virtual auto propagate(Solver &solver, AbstractClauseCreator &cc, bool check_state) -> bool = 0; //! Check if the solver meets the state invariants. virtual void check_full(Solver &solver) = 0; @@ -158,7 +158,7 @@ class AbstractConstraintState { //! contain the smallest and largest allowed integer. class VarState { using OrderMap = std::map; //!< Map to store order literals. - using OrderVec = std::vector; //!< Vetor to store order literals. + using OrderVec = std::vector; //!< Vector to store order literals. using ReverseIteratorMap = OrderMap::const_reverse_iterator; //!< Reverse iterator over order literals in map. using IteratorVec = OrderVec::const_iterator; //!< Iterator over order literals in vector. using ReverseIteratorVec = OrderVec::const_reverse_iterator; //!< Reverse iterator over order literals in vector. @@ -402,7 +402,7 @@ class VarState { return call_vec_(std::forward(f), litvec_.begin(), litvec_.end()); } - //! Traverse literals preceeding value. + //! Traverse literals preceding value. template [[nodiscard]] auto with_lt(val_t value, F &&f) const -> RetType { if (offset_ == unused) { return call_map_(std::forward(f), ReverseIteratorMap{litmap_.lower_bound(value)}, litmap_.rend()); @@ -410,7 +410,7 @@ class VarState { auto offset = std::min(std::max(0, value - offset_), static_cast(litvec_.size())); return call_vec_(std::forward(f), ReverseIteratorVec{litvec_.begin() + offset}, litvec_.rend()); } - //! Traverse literals preceeding and including value. + //! Traverse literals preceding and including value. template [[nodiscard]] auto with_le(val_t value, F &&f) const -> RetType { if (offset_ == unused) { return call_map_(std::forward(f), ReverseIteratorMap{litmap_.upper_bound(value)}, litmap_.rend()); @@ -436,7 +436,7 @@ class VarState { return call_vec_(std::forward(f), litvec_.begin() + offset, litvec_.end()); } - //! Get preceeding literal. + //! Get preceding literal. [[nodiscard]] auto lit_lt(val_t value) const -> lit_t { return with_lt(value, [](auto ib, auto ie, auto get_lit, auto get_val, auto inc) -> lit_t { static_cast(get_val); @@ -444,7 +444,7 @@ class VarState { return ib != ie ? get_lit(ib) : 0; }); } - //! Get preceeding or equal literal. + //! Get preceding or equal literal. [[nodiscard]] auto lit_le(val_t value) const -> lit_t { return with_le(value, [](auto ib, auto ie, auto get_lit, auto get_val, auto inc) -> lit_t { static_cast(get_val); @@ -469,14 +469,14 @@ class VarState { }); } - //! Get preceeding order literal. + //! Get preceding order literal. [[nodiscard]] auto order_lit_lt(val_t value) const -> OrderLiteralOpt { return with_lt(value, [](auto ib, auto ie, auto get_lit, auto get_val, auto inc) -> OrderLiteralOpt { static_cast(inc); return ib != ie ? OrderLiteralOpt{{get_lit(ib), get_val(ib)}} : std::nullopt; }); } - //! Get preceeding or equal order literal. + //! Get preceding or equal order literal. [[nodiscard]] auto order_lit_le(val_t value) const -> OrderLiteralOpt { return with_le(value, [](auto ib, auto ie, auto get_lit, auto get_val, auto inc) -> OrderLiteralOpt { static_cast(inc); @@ -560,7 +560,7 @@ class VarState { var_t var_; //!< variable associated with the state val_t lower_bound_; //!< current lower bound of the variable val_t upper_bound_; //!< current upper bound of the variable - val_t offset_{unused}; //!< minimium bound at the time of mogrification + val_t offset_{unused}; //!< minimum bound at the time of mogrification BoundStack lower_bound_stack_; //!< lower bounds of lower levels BoundStack upper_bound_stack_; //!< upper bounds of lower levels union { @@ -676,7 +676,7 @@ class Solver { //! Adds a new VarState object and returns its index; [[nodiscard]] auto add_variable(val_t min_int, val_t max_int) -> var_t; - //! Integrates the given domain for varibale var. + //! Integrates the given domain for variable var. //! //! Consider x in {[1,3), [4,6), [7,9)}. We can simply add the binary //! constraints: @@ -691,9 +691,9 @@ class Solver { [[nodiscard]] auto add_dom(AbstractClauseCreator &cc, lit_t lit, var_t var, IntervalSet const &domain) -> bool; - //! This function integrates singleton constraints intwatches_o the state. + //! This function integrates singleton constraints into the state. //! - //! We explicitely handle the strict case here to avoid introducing + //! We explicitly handle the strict case here to avoid introducing //! unnecessary literals. [[nodiscard]] auto add_simple(AbstractClauseCreator &cc, lit_t clit, val_t co, var_t var, val_t rhs, bool strict) -> bool; @@ -705,7 +705,7 @@ class Solver { void remove_constraint(AbstractConstraint &constraint); //! Simplify the state using fixed literals in the trail up to the given - //! offset and the enqued constraints in the todo list. + //! offset and the enqueued constraints in the todo list. //! //! Note that this functions assumes that newly added constraints have been //! enqueued before. @@ -770,7 +770,7 @@ class Solver { //! This function should only be called total assignments. void check_full(AbstractClauseCreator &cc, bool check_solution); - //! This function undos decision level specific state. + //! This function undoes decision level specific state. //! //! This includes undoing changed bounds of variables clearing constraints //! that where not propagated on the current decision level. @@ -780,7 +780,7 @@ class Solver { //! @} private: - //! Update preceeding and succeeding literals of order literal with the + //! Update preceding and succeeding literals of order literal with the //! given value. auto update_litmap_(VarState &vs, lit_t lit, val_t value) -> std::pair; @@ -790,22 +790,22 @@ class Solver { //! See Solver::propagate. [[nodiscard]] auto propagate_(AbstractClauseCreator &cc, lit_t lit) -> bool; - //! Propagates the preceeding or succeeding order literals of lit until a + //! Propagates the preceding or succeeding order literals of lit until a //! true literal is found or the end is reached. template [[nodiscard]] auto propagate_variables_(AbstractClauseCreator &cc, lit_t reason_lit, It begin, It end, L get_lit, I inc) -> bool; - //! Update and propgate the given variable due to a lower bound change. + //! Update and propagate the given variable due to a lower bound change. [[nodiscard]] auto update_lower_(Level &lvl, AbstractClauseCreator &cc, var_t var, lit_t lit, val_t value, lit_t prev_lit) -> bool; - //! Update and propgate the given variable due to an upper bound change. + //! Update and propagate the given variable due to an upper bound change. [[nodiscard]] auto update_upper_(Level &lvl, AbstractClauseCreator &cc, var_t var, lit_t lit, val_t value, lit_t succ_lit) -> bool; //! If the given literal is an order literal, this function updates the lower - //! or upper bound of the corresponding variables. Furthermore, the preceeding + //! or upper bound of the corresponding variables. Furthermore, the preceding //! or succeeding order literals are propagated. [[nodiscard]] auto update_domain_(AbstractClauseCreator &cc, lit_t lit) -> bool; @@ -830,7 +830,7 @@ class Solver { //! Solver configuration. SolverConfig const &config_; - //! Solver statitstics; + //! Solver statistics; SolverStatistics &stats_; //! Vector of all VarState objects. std::vector var2vs_; diff --git a/libclingcon/clingcon/util.hh b/libclingcon/clingcon/util.hh index 74ab195..a8ed04b 100644 --- a/libclingcon/clingcon/util.hh +++ b/libclingcon/clingcon/util.hh @@ -43,7 +43,7 @@ namespace detail { template using int_type = std::integral_constant; template inline void sc_check(S s, int_type<0> t) { // same sign static_cast(t); - if (!std::is_same::value && (s < std::numeric_limits::min() || s > std::numeric_limits::max())) { + if (!std::is_same_v && (s < std::numeric_limits::min() || s > std::numeric_limits::max())) { throw std::overflow_error("safe cast failed"); } } @@ -55,7 +55,7 @@ template inline void sc_check(S s, int_type<-1> t) { // Signe } template inline void sc_check(S s, int_type<1> t) { // Unsigned -> Signed static_cast(t); - if (s > static_cast::type>(std::numeric_limits::max())) { + if (s > static_cast>(std::numeric_limits::max())) { throw std::overflow_error("safe cast failed"); } } @@ -132,7 +132,7 @@ template struct FlagUnique { //! Like a vector but only adds an element if it is not contained yet. template > class UniqueVector : private Flagger { public: - using Vector = typename std::vector; + using Vector = std::vector; using Iterator = typename Vector::iterator; using ConstIterator = typename Vector::const_iterator; @@ -155,6 +155,7 @@ template > class UniqueVector : privat auto operator=(UniqueVector &&x) noexcept -> UniqueVector & { *static_cast(this) = std::move(*static_cast(x)); std::swap(vec_, x.vec_); + return *this; } UniqueVector(UniqueVector const &) = delete; @@ -229,7 +230,7 @@ template > class UniqueVector : privat //! `&dom` statements. template class IntervalSet { public: - using Map = typename std::map; + using Map = std::map; using Iterator = typename Map::const_iterator; using ReverseIterator = typename Map::const_reverse_iterator; diff --git a/libclingcon/src/clingcon.cc b/libclingcon/src/clingcon.cc index f7e15b3..c020c03 100644 --- a/libclingcon/src/clingcon.cc +++ b/libclingcon/src/clingcon.cc @@ -108,7 +108,6 @@ auto heuristic_str(Heuristic heu) -> char const * { } case Heuristic::MaxChain: { return "max-chain"; - break; } }; return ""; @@ -492,7 +491,7 @@ extern "C" auto clingcon_register_options(clingcon_theory_t *theory, clingo_opti // propagation opts.add(group, "order-heuristic", - format("Make the decision heuristic aware of order literls [", + format("Make the decision heuristic aware of order literals [", heuristic_str(config.default_solver_config.heuristic), "]\n" " : {none,max-chain}[,]\n" diff --git a/libclingcon/src/constraints.cc b/libclingcon/src/constraints.cc index 7d41133..f117a50 100644 --- a/libclingcon/src/constraints.cc +++ b/libclingcon/src/constraints.cc @@ -156,7 +156,7 @@ template class SumConstraintStateImpl final : public T auto rhs = T::rhs(solver); auto clit = T::constraint_.literal(); - // Note: this has a noticible cost because of the shortcuts below + // Note: this has a noticeable cost because of the shortcuts below if (check_state) { check_state_(solver); } @@ -523,7 +523,7 @@ class SumConstraintState : public AbstractConstraintState { // two. In the current system design, this requires storing the // weight constraints and detect complementary constraints. It // might be a good idea in general to add translation constraints - // later because we can run into the problem of successivly adding + // later because we can run into the problem of successively adding // variables and constraints here. return {cc.add_weight_constraint(constraint_.literal(), wlits, static_cast(slack), Clingo::WeightConstraintType::RightImplication), @@ -612,7 +612,7 @@ class SumConstraintState : public AbstractConstraintState { if (std::abs(a.first) != std::abs(b.first)) { return std::abs(a.first) > std::abs(b.first); } - // i do not see why any of the below should matter... + // I do not see why any of the below should matter... auto &vs_a = solver.var_state(a.second); auto &vs_b = solver.var_state(b.second); // sort by minimum value (ascending) @@ -1067,7 +1067,7 @@ class DistinctConstraintState final : public AbstractConstraintState { //! Estimate the size of the translation in terms of the number of weight //! constraints and return whether the constraint should be translated. //! - //! Since terms might be represented by by auxiliary variables, we also + //! Since terms might be represented by auxiliary variables, we also //! make sure that they can be represented by auxiliary variables. auto estimate_(sum_t maximum) -> bool { sum_t cost = 0; @@ -1124,7 +1124,7 @@ class DistinctConstraintState final : public AbstractConstraintState { } //! Propagate a distinct constraint assuming that element i is assigned and - //! one of element element j's bounds as determined by s match the value of + //! one of element j's bounds as determined by s match the value of //! element i. //! //! The reasons generated by this function are not necessarily unit. @@ -1456,7 +1456,7 @@ class NonlinearConstraintState : public AbstractConstraintState { // TODO: For nonlinear constraints it is probably necessary to add // the range, in general. But there should also be some cases where // this is not required. For example, if all bounds are positive - // (or negative) the term a*b should behave monotonely. + // (or negative) the term a*b should behave monotonically. // std::cerr << " the constraint is conflicting" << std::endl; auto &reason = solver.temp_reason(); reason.emplace_back(-solver.get_literal(cc, vs_x, vs_x.upper_bound())); @@ -1534,8 +1534,8 @@ class NonlinearConstraintState : public AbstractConstraintState { // the other cases are more complicated // we can get different bound combinations for reasons for ub(x*y) // we can get a conjunction of x => l | x <= u as reason - // if one of the terms is false, we can stil propgate - // or by relaxing the bounds until one of the becomes false and the other can be propgate + // if one of the terms is false, we can still propagate + // or by relaxing the bounds until one of the becomes false and the other can be propagated // this looks tedious and is probably best developed on paper } } @@ -1639,14 +1639,14 @@ class DisjointConstraintState final : public AbstractConstraintState { reason.emplace_back(solver.get_literal(cc, vs, vs.lower_bound() - 1)); // Note: we cap the new lower bound here to the upper bound to // avoid introducing variables above the upper bound. It is - // possible to introduce a new variable but it would have to be + // possible to introduce a new variable, but it would have to be // implied by the closest order literal to not have it dangling // around later. And it should only be done on the current - // decision level to avoid backtracking with out a conflict. + // decision level to avoid backtracking without a conflict. // // See for example the sum constraint state, which refines // reasons in the hope of getting better conflict but making - // sure to avoid the above mentioned cases. + // sure to avoid the above-mentioned cases. auto val = std::min(b - 1, vs.upper_bound()); auto lit = -solver.update_literal( cc, vs, val, reason.empty() ? Clingo::TruthValue::False : Clingo::TruthValue::Free); diff --git a/libclingcon/src/parsing.cc b/libclingcon/src/parsing.cc index 671c02c..47ee89f 100644 --- a/libclingcon/src/parsing.cc +++ b/libclingcon/src/parsing.cc @@ -437,7 +437,7 @@ auto simplify(NonlinearTermVec &vec, bool drop_zero) -> val_t { vec.erase(jt, vec.end()); - // overflow checking (maybe put in seperate function) + // overflow checking (maybe put in separate function) check_valid_value(rhs); nsum_t min = rhs; nsum_t max = rhs; @@ -600,7 +600,7 @@ template elems = © } - // hanle remainig '<=', '=', and '!=' + // handle remaining '<=', '=', and '!=' if (std::strcmp(op, "<=") == 0) { if (strict && elems->size() == 1) { return add_constraint(builder, literal, *elems, rhs, true); @@ -694,7 +694,7 @@ template // If `is_sum` is true parses a sum constraint. Otherwise, it parses a // difference constraint as supported by clingo-dl. // -// Contraints are represented as a triple of a literal, its elements, and an +// Constraints are represented as a triple of a literal, its elements, and an // upper bound. template [[nodiscard]] auto parse_constraint(AbstractConstraintBuilder &builder, Clingo::TheoryAtom const &atom, @@ -870,7 +870,7 @@ auto simplify(CoVarVec &vec, bool drop_zero) -> val_t { vec.erase(jt, vec.end()); - // overflow checking (maybe put in seperate function) + // overflow checking (maybe put in separate function) check_valid_value(rhs); sum_t min = rhs; sum_t max = rhs; diff --git a/libclingcon/src/propagator.cc b/libclingcon/src/propagator.cc index 06036f5..80604b5 100644 --- a/libclingcon/src/propagator.cc +++ b/libclingcon/src/propagator.cc @@ -32,8 +32,8 @@ namespace { //! CSP builder to use with the parse_theory function. class ConstraintBuilder final : public AbstractConstraintBuilder { public: - ConstraintBuilder(Propagator &propgator, InitClauseCreator &cc, UniqueMinimizeConstraint minimize) - : propagator_{propgator}, cc_{cc}, minimize_{std::move(minimize)} {} + ConstraintBuilder(Propagator &propagator, InitClauseCreator &cc, UniqueMinimizeConstraint minimize) + : propagator_{propagator}, cc_{cc}, minimize_{std::move(minimize)} {} ConstraintBuilder(ConstraintBuilder const &) = delete; ConstraintBuilder(ConstraintBuilder &&) noexcept = delete; diff --git a/libclingcon/src/solver.cc b/libclingcon/src/solver.cc index e55c7ba..c7a6ded 100644 --- a/libclingcon/src/solver.cc +++ b/libclingcon/src/solver.cc @@ -70,7 +70,7 @@ class Solver::Level { solver.udiff_[vs.var()] += diff; } - //! Update watches and enque constraints. + //! Update watches and enqueue constraints. //! //! The parameters determine whether the lookup tables for lower or upper //! bounds are used. @@ -111,7 +111,7 @@ class Solver::Level { } } - //! This function undos decision level specific state. + //! This function undoes decision level specific state. //! //! This includes undoing changed bounds of variables clearing constraints //! that where not propagated on the current decision level. @@ -497,7 +497,7 @@ auto Solver::update_litmap_(VarState &vs, lit_t lit, val_t value) -> std::pair lit_t { - // order literals can only be update on level 0 + // order literals can only be updated on level 0 if (truth == Clingo::TruthValue::Free || cc.assignment().decision_level() > 0) { return get_literal(cc, vs, value); } @@ -616,7 +616,7 @@ auto Solver::translate(InitClauseCreator &cc, Statistics &stats, Config const &c constraints.erase(constraints.begin() + static_cast(jdx), constraints.end()); - // This readds binary clauses when multishot-solving. Probably clasp can + // This re-adds binary clauses when multishot-solving. Probably clasp can // handle this. if (conf.add_order_clauses) { for (auto &vs : var2vs_) { @@ -852,7 +852,7 @@ auto Solver::check(AbstractClauseCreator &cc, bool check_state) -> bool { } // update the bounds of the constraints (this is the only place where - // the todo queue is filled after initializaton) + // the todo queue is filled after initialization) for (auto var : in_udiff_) { lvl.update_constraints_(*this, var, udiff_[var]); udiff_[var] = 0; @@ -1021,7 +1021,7 @@ auto Solver::update_bounds(AbstractClauseCreator &cc, Solver &other, bool check_ } } - // update_domain_ in check makes sure that unnecassary facts are removed + // update_domain_ in check makes sure that unnecessary facts are removed return check(cc, check_state); } @@ -1130,7 +1130,7 @@ auto Solver::add_simple(AbstractClauseCreator &cc, lit_t clit, val_t co, var_t v } #if 0 -// This is a usefull function for debugging. +// This is a useful function for debugging. void Solver::check_litmap_() { for (auto [lit, tup] : litmap_) { auto [var, value, prev_lit, succ_lit] = tup;