hide implementation of spot::acc_cond::mark_t
* bin/autcross.cc, bin/autfilt.cc, bin/ltlcross.cc, spot/parseaut/parseaut.yy: use SPOT_NB_ACC * spot/twa/acc.hh: make implementation private
This commit is contained in:
parent
c6c085ab22
commit
cde0977ef8
5 changed files with 33 additions and 22 deletions
|
|
@ -509,8 +509,7 @@ namespace
|
||||||
const spot::const_twa_graph_ptr& aut_j,
|
const spot::const_twa_graph_ptr& aut_j,
|
||||||
size_t i, size_t j)
|
size_t i, size_t j)
|
||||||
{
|
{
|
||||||
if (aut_i->num_sets() + aut_j->num_sets()
|
if (aut_i->num_sets() + aut_j->num_sets() > SPOT_NB_ACC)
|
||||||
> 8 * sizeof(spot::acc_cond::mark_t::value_t))
|
|
||||||
{
|
{
|
||||||
std::cerr << "info: building " << autname(i)
|
std::cerr << "info: building " << autname(i)
|
||||||
<< '*' << autname(j, true)
|
<< '*' << autname(j, true)
|
||||||
|
|
|
||||||
|
|
@ -930,8 +930,7 @@ parse_opt(int key, char* arg, struct argp_state*)
|
||||||
if (res < 0)
|
if (res < 0)
|
||||||
error(2, 0, "acceptance sets should be non-negative:"
|
error(2, 0, "acceptance sets should be non-negative:"
|
||||||
" --mask-acc=%ld", res);
|
" --mask-acc=%ld", res);
|
||||||
if (static_cast<unsigned long>(res)
|
if (static_cast<unsigned long>(res) > SPOT_NB_ACC)
|
||||||
> sizeof(spot::acc_cond::mark_t::value_t))
|
|
||||||
error(2, 0, "this implementation does not support that many"
|
error(2, 0, "this implementation does not support that many"
|
||||||
" acceptance sets: --mask-acc=%ld", res);
|
" acceptance sets: --mask-acc=%ld", res);
|
||||||
opt_mask_acc.set(res);
|
opt_mask_acc.set(res);
|
||||||
|
|
|
||||||
|
|
@ -691,8 +691,7 @@ namespace
|
||||||
const spot::const_twa_graph_ptr& aut_j,
|
const spot::const_twa_graph_ptr& aut_j,
|
||||||
size_t i, size_t j, bool icomp, bool jcomp)
|
size_t i, size_t j, bool icomp, bool jcomp)
|
||||||
{
|
{
|
||||||
if (aut_i->num_sets() + aut_j->num_sets()
|
if (aut_i->num_sets() + aut_j->num_sets() > SPOT_NB_ACC)
|
||||||
> 8 * sizeof(spot::acc_cond::mark_t::value_t))
|
|
||||||
{
|
{
|
||||||
// Report the skipped test if both automata are not
|
// Report the skipped test if both automata are not
|
||||||
// complemented, or the --verbose option is used,
|
// complemented, or the --verbose option is used,
|
||||||
|
|
|
||||||
|
|
@ -772,7 +772,7 @@ header-item: "States:" INT
|
||||||
"acceptance condition...");
|
"acceptance condition...");
|
||||||
error(res.accset_loc, "... previously defined here.");
|
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,
|
error(@1 + @2,
|
||||||
"this implementation cannot support such a large "
|
"this implementation cannot support such a large "
|
||||||
|
|
|
||||||
|
|
@ -33,19 +33,28 @@ namespace spot
|
||||||
namespace internal
|
namespace internal
|
||||||
{
|
{
|
||||||
class mark_container;
|
class mark_container;
|
||||||
|
|
||||||
|
template<bool>
|
||||||
|
struct _32acc {};
|
||||||
|
template<>
|
||||||
|
struct _32acc<true>
|
||||||
|
{
|
||||||
|
SPOT_DEPRECATED("mark_t no longer relies on unsigned, stop using value_t")
|
||||||
|
typedef unsigned value_t;
|
||||||
|
};
|
||||||
}
|
}
|
||||||
|
|
||||||
class SPOT_API acc_cond
|
class SPOT_API acc_cond
|
||||||
{
|
{
|
||||||
public:
|
public:
|
||||||
struct mark_t
|
struct mark_t : public internal::_32acc<SPOT_NB_ACC == 8*sizeof(unsigned)>
|
||||||
{
|
{
|
||||||
// configure guarantees that SPOT_NB_ACC % (8*sizeof(unsigned)) == 0
|
|
||||||
typedef bitset<SPOT_NB_ACC / (8*sizeof(unsigned))> value_t;
|
|
||||||
value_t id;
|
|
||||||
|
|
||||||
private:
|
private:
|
||||||
mark_t(value_t id) noexcept
|
// configure guarantees that SPOT_NB_ACC % (8*sizeof(unsigned)) == 0
|
||||||
|
typedef bitset<SPOT_NB_ACC / (8*sizeof(unsigned))> _value_t;
|
||||||
|
_value_t id;
|
||||||
|
|
||||||
|
mark_t(_value_t id) noexcept
|
||||||
: id(id)
|
: id(id)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
@ -55,7 +64,7 @@ namespace spot
|
||||||
|
|
||||||
template<class iterator>
|
template<class iterator>
|
||||||
mark_t(const iterator& begin, const iterator& end) noexcept
|
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)
|
for (iterator i = begin; i != end; ++i)
|
||||||
set(*i);
|
set(*i);
|
||||||
|
|
@ -86,6 +95,12 @@ namespace spot
|
||||||
return res;
|
return res;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
size_t hash() const noexcept
|
||||||
|
{
|
||||||
|
std::hash<decltype(id)> h;
|
||||||
|
return h(id);
|
||||||
|
}
|
||||||
|
|
||||||
bool operator==(unsigned o) const
|
bool operator==(unsigned o) const
|
||||||
{
|
{
|
||||||
SPOT_ASSERT(o == 0U);
|
SPOT_ASSERT(o == 0U);
|
||||||
|
|
@ -140,12 +155,12 @@ namespace spot
|
||||||
|
|
||||||
void set(unsigned u)
|
void set(unsigned u)
|
||||||
{
|
{
|
||||||
id |= (value_t::one() << u);
|
id |= (_value_t::one() << u);
|
||||||
}
|
}
|
||||||
|
|
||||||
void clear(unsigned u)
|
void clear(unsigned u)
|
||||||
{
|
{
|
||||||
id &= ~(value_t::one() << u);
|
id &= ~(_value_t::one() << u);
|
||||||
}
|
}
|
||||||
|
|
||||||
mark_t& operator&=(mark_t r)
|
mark_t& operator&=(mark_t r)
|
||||||
|
|
@ -532,7 +547,7 @@ namespace spot
|
||||||
if (n == 0)
|
if (n == 0)
|
||||||
return inf({});
|
return inf({});
|
||||||
acc_cond::mark_t m = mark_t::all();
|
acc_cond::mark_t m = mark_t::all();
|
||||||
m >>= (8*sizeof(mark_t::value_t) - n);
|
m >>= (SPOT_NB_ACC - n);
|
||||||
return inf(m);
|
return inf(m);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -541,7 +556,7 @@ namespace spot
|
||||||
if (n == 0)
|
if (n == 0)
|
||||||
return fin({});
|
return fin({});
|
||||||
acc_cond::mark_t m = mark_t::all();
|
acc_cond::mark_t m = mark_t::all();
|
||||||
m >>= (8*sizeof(mark_t::value_t) - n);
|
m >>= (SPOT_NB_ACC - n);
|
||||||
return fin(m);
|
return fin(m);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -1202,7 +1217,7 @@ namespace spot
|
||||||
return -1U;
|
return -1U;
|
||||||
unsigned j = num_;
|
unsigned j = num_;
|
||||||
num_ += 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.");
|
throw std::runtime_error("Too many acceptance sets used.");
|
||||||
all_ = all_sets_();
|
all_ = all_sets_();
|
||||||
return j;
|
return j;
|
||||||
|
|
@ -1340,7 +1355,7 @@ namespace spot
|
||||||
protected:
|
protected:
|
||||||
mark_t all_sets_() const
|
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_;
|
unsigned num_;
|
||||||
|
|
@ -1519,8 +1534,7 @@ namespace std
|
||||||
{
|
{
|
||||||
size_t operator()(spot::acc_cond::mark_t m) const noexcept
|
size_t operator()(spot::acc_cond::mark_t m) const noexcept
|
||||||
{
|
{
|
||||||
std::hash<decltype(m.id)> h;
|
return m.hash();
|
||||||
return h(m.id);
|
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue