diff --git a/bin/autcross.cc b/bin/autcross.cc index 0d1ab9de7..137966342 100644 --- a/bin/autcross.cc +++ b/bin/autcross.cc @@ -509,8 +509,7 @@ namespace const spot::const_twa_graph_ptr& aut_j, size_t i, size_t j) { - if (aut_i->num_sets() + aut_j->num_sets() - > 8 * sizeof(spot::acc_cond::mark_t::value_t)) + if (aut_i->num_sets() + aut_j->num_sets() > SPOT_NB_ACC) { std::cerr << "info: building " << autname(i) << '*' << autname(j, true) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 9b0fe7419..e51450cbb 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -930,8 +930,7 @@ parse_opt(int key, char* arg, struct argp_state*) if (res < 0) error(2, 0, "acceptance sets should be non-negative:" " --mask-acc=%ld", res); - if (static_cast(res) - > sizeof(spot::acc_cond::mark_t::value_t)) + if (static_cast(res) > SPOT_NB_ACC) error(2, 0, "this implementation does not support that many" " acceptance sets: --mask-acc=%ld", res); opt_mask_acc.set(res); diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index e7195bb75..4706d2f6b 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -691,8 +691,7 @@ namespace const spot::const_twa_graph_ptr& aut_j, size_t i, size_t j, bool icomp, bool jcomp) { - if (aut_i->num_sets() + aut_j->num_sets() - > 8 * sizeof(spot::acc_cond::mark_t::value_t)) + if (aut_i->num_sets() + aut_j->num_sets() > SPOT_NB_ACC) { // Report the skipped test if both automata are not // complemented, or the --verbose option is used, diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy index be7df7ff6..a4a0db623 100644 --- a/spot/parseaut/parseaut.yy +++ b/spot/parseaut/parseaut.yy @@ -772,7 +772,7 @@ header-item: "States:" INT "acceptance condition..."); error(res.accset_loc, "... previously defined here."); } - else if ($2 > 8 * sizeof(spot::acc_cond::mark_t::value_t)) + else if ($2 > SPOT_NB_ACC) { error(@1 + @2, "this implementation cannot support such a large " diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 1cac6c534..93e6a16f2 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -33,19 +33,28 @@ namespace spot namespace internal { class mark_container; + + template + struct _32acc {}; + template<> + struct _32acc + { + SPOT_DEPRECATED("mark_t no longer relies on unsigned, stop using value_t") + typedef unsigned value_t; + }; } class SPOT_API acc_cond { public: - struct mark_t + struct mark_t : public internal::_32acc { - // configure guarantees that SPOT_NB_ACC % (8*sizeof(unsigned)) == 0 - typedef bitset value_t; - value_t id; - private: - mark_t(value_t id) noexcept + // configure guarantees that SPOT_NB_ACC % (8*sizeof(unsigned)) == 0 + typedef bitset _value_t; + _value_t id; + + mark_t(_value_t id) noexcept : id(id) { } @@ -55,7 +64,7 @@ namespace spot template mark_t(const iterator& begin, const iterator& end) noexcept - : mark_t(value_t::zero()) + : mark_t(_value_t::zero()) { for (iterator i = begin; i != end; ++i) set(*i); @@ -86,6 +95,12 @@ namespace spot return res; } + size_t hash() const noexcept + { + std::hash h; + return h(id); + } + bool operator==(unsigned o) const { SPOT_ASSERT(o == 0U); @@ -140,12 +155,12 @@ namespace spot void set(unsigned u) { - id |= (value_t::one() << u); + id |= (_value_t::one() << u); } void clear(unsigned u) { - id &= ~(value_t::one() << u); + id &= ~(_value_t::one() << u); } mark_t& operator&=(mark_t r) @@ -532,7 +547,7 @@ namespace spot if (n == 0) return inf({}); acc_cond::mark_t m = mark_t::all(); - m >>= (8*sizeof(mark_t::value_t) - n); + m >>= (SPOT_NB_ACC - n); return inf(m); } @@ -541,7 +556,7 @@ namespace spot if (n == 0) return fin({}); acc_cond::mark_t m = mark_t::all(); - m >>= (8*sizeof(mark_t::value_t) - n); + m >>= (SPOT_NB_ACC - n); return fin(m); } @@ -1202,7 +1217,7 @@ namespace spot return -1U; unsigned j = num_; num_ += num; - if (num_ > 8 * sizeof(mark_t::value_t)) + if (num_ > SPOT_NB_ACC) throw std::runtime_error("Too many acceptance sets used."); all_ = all_sets_(); return j; @@ -1340,7 +1355,7 @@ namespace spot protected: mark_t all_sets_() const { - return mark_t::all() >> (8*sizeof(mark_t::value_t) - num_); + return mark_t::all() >> (SPOT_NB_ACC - num_); } unsigned num_; @@ -1519,8 +1534,7 @@ namespace std { size_t operator()(spot::acc_cond::mark_t m) const noexcept { - std::hash h; - return h(m.id); + return m.hash(); } }; }