Skip to content

Commit

Permalink
Minor fixes.
Browse files Browse the repository at this point in the history
* Fix some typos and add missing return to UniqueVector::operator=.
  • Loading branch information
BenKaufmann committed Jan 17, 2025
1 parent 3047d37 commit 39768da
Show file tree
Hide file tree
Showing 11 changed files with 61 additions and 61 deletions.
2 changes: 1 addition & 1 deletion app/main.cc
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
#include <clingo.hh>
#include <fstream>
#include <optional>
#include <sstream>
#include <iostream>

#ifdef CLINGCON_PROFILE
#include <gperftools/profiler.h>
Expand Down
2 changes: 1 addition & 1 deletion libclingcon/clingcon.h
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down
8 changes: 4 additions & 4 deletions libclingcon/clingcon/base.hh
Original file line number Diff line number Diff line change
Expand Up @@ -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<val_t, var_t>; //!< coeffcient/variable pair
using co_var_t = std::pair<val_t, var_t>; //!< coefficient/variable pair
using CoVarVec = std::vector<co_var_t>;

enum class Heuristic : val_t { None, MaxChain };
Expand All @@ -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<val_t>::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.
Expand Down Expand Up @@ -96,7 +96,7 @@ template <class I> inline auto check_valid_value(I val) -> val_t {
}
return val;
}
static_assert(std::is_same<Clingo::weight_t, val_t>::value);
static_assert(std::is_same_v<Clingo::weight_t, val_t>);

//! Solver specific statistics.
struct SolverStatistics {
Expand Down Expand Up @@ -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;

Expand Down
8 changes: 4 additions & 4 deletions libclingcon/clingcon/constraints.hh
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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.
Expand Down
42 changes: 21 additions & 21 deletions libclingcon/clingcon/solver.hh
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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;
Expand Down Expand Up @@ -158,7 +158,7 @@ class AbstractConstraintState {
//! contain the smallest and largest allowed integer.
class VarState {
using OrderMap = std::map<val_t, lit_t>; //!< Map to store order literals.
using OrderVec = std::vector<lit_t>; //!< Vetor to store order literals.
using OrderVec = std::vector<lit_t>; //!< 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.
Expand Down Expand Up @@ -402,15 +402,15 @@ class VarState {
return call_vec_(std::forward<F>(f), litvec_.begin(), litvec_.end());
}

//! Traverse literals preceeding value.
//! Traverse literals preceding value.
template <typename F> [[nodiscard]] auto with_lt(val_t value, F &&f) const -> RetType<F, ReverseIteratorVec> {
if (offset_ == unused) {
return call_map_(std::forward<F>(f), ReverseIteratorMap{litmap_.lower_bound(value)}, litmap_.rend());
}
auto offset = std::min<val_t>(std::max(0, value - offset_), static_cast<val_t>(litvec_.size()));
return call_vec_(std::forward<F>(f), ReverseIteratorVec{litvec_.begin() + offset}, litvec_.rend());
}
//! Traverse literals preceeding and including value.
//! Traverse literals preceding and including value.
template <typename F> [[nodiscard]] auto with_le(val_t value, F &&f) const -> RetType<F, ReverseIteratorVec> {
if (offset_ == unused) {
return call_map_(std::forward<F>(f), ReverseIteratorMap{litmap_.upper_bound(value)}, litmap_.rend());
Expand All @@ -436,15 +436,15 @@ class VarState {
return call_vec_(std::forward<F>(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<void>(get_val);
static_cast<void>(inc);
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<void>(get_val);
Expand All @@ -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<void>(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<void>(inc);
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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:
Expand All @@ -691,9 +691,9 @@ class Solver {
[[nodiscard]] auto add_dom(AbstractClauseCreator &cc, lit_t lit, var_t var, IntervalSet<val_t> 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;
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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<lit_t, lit_t>;

Expand All @@ -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 <int sign, class It, class L, class I>
[[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;

Expand All @@ -830,7 +830,7 @@ class Solver {

//! Solver configuration.
SolverConfig const &config_;
//! Solver statitstics;
//! Solver statistics;
SolverStatistics &stats_;
//! Vector of all VarState objects.
std::vector<VarState> var2vs_;
Expand Down
9 changes: 5 additions & 4 deletions libclingcon/clingcon/util.hh
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ namespace detail {
template <int X> using int_type = std::integral_constant<int, X>;
template <class T, class S> inline void sc_check(S s, int_type<0> t) { // same sign
static_cast<void>(t);
if (!std::is_same<T, S>::value && (s < std::numeric_limits<T>::min() || s > std::numeric_limits<T>::max())) {
if (!std::is_same_v<T, S> && (s < std::numeric_limits<T>::min() || s > std::numeric_limits<T>::max())) {
throw std::overflow_error("safe cast failed");
}
}
Expand All @@ -55,7 +55,7 @@ template <class T, class S> inline void sc_check(S s, int_type<-1> t) { // Signe
}
template <class T, class S> inline void sc_check(S s, int_type<1> t) { // Unsigned -> Signed
static_cast<void>(t);
if (s > static_cast<typename std::make_unsigned<T>::type>(std::numeric_limits<T>::max())) {
if (s > static_cast<std::make_unsigned_t<T>>(std::numeric_limits<T>::max())) {
throw std::overflow_error("safe cast failed");
}
}
Expand Down Expand Up @@ -132,7 +132,7 @@ template <class T> struct FlagUnique {
//! Like a vector but only adds an element if it is not contained yet.
template <typename T, class Flagger = FlagUnique<T>> class UniqueVector : private Flagger {
public:
using Vector = typename std::vector<T>;
using Vector = std::vector<T>;
using Iterator = typename Vector::iterator;
using ConstIterator = typename Vector::const_iterator;

Expand All @@ -155,6 +155,7 @@ template <typename T, class Flagger = FlagUnique<T>> class UniqueVector : privat
auto operator=(UniqueVector &&x) noexcept -> UniqueVector & {
*static_cast<Flagger *>(this) = std::move(*static_cast<Flagger *>(x));
std::swap(vec_, x.vec_);
return *this;
}

UniqueVector(UniqueVector const &) = delete;
Expand Down Expand Up @@ -229,7 +230,7 @@ template <typename T, class Flagger = FlagUnique<T>> class UniqueVector : privat
//! `&dom` statements.
template <typename T> class IntervalSet {
public:
using Map = typename std::map<T, T>;
using Map = std::map<T, T>;
using Iterator = typename Map::const_iterator;
using ReverseIterator = typename Map::const_reverse_iterator;

Expand Down
3 changes: 1 addition & 2 deletions libclingcon/src/clingcon.cc
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,6 @@ auto heuristic_str(Heuristic heu) -> char const * {
}
case Heuristic::MaxChain: {
return "max-chain";
break;
}
};
return "";
Expand Down Expand Up @@ -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"
" <arg>: {none,max-chain}[,<i>]\n"
Expand Down
Loading

0 comments on commit 39768da

Please sign in to comment.