acc: remove some dead functions
* spot/twa/acc.hh, spot/twa/acc.cc (has_parity_prefix, is_parity_max_equiv): Remove. * spot/twa/acc.hh, spot/twa/twagraph.cc, spot/twa/twagraph.hh (apply_permutation): Remove.
This commit is contained in:
Alexandre Duret-Lutz
parent
69b9ffef9a
commit
e548bf0a8e
4 changed files with 1 additions and 273 deletions
180
spot/twa/acc.cc
180
spot/twa/acc.cc
|
|
@ -1067,81 +1067,6 @@ namespace spot
|
|||
return res;
|
||||
}
|
||||
|
||||
namespace
|
||||
{
|
||||
bool
|
||||
has_parity_prefix_aux(acc_cond original,
|
||||
acc_cond &new_cond,
|
||||
std::vector<unsigned> &colors,
|
||||
std::vector<acc_cond::acc_code> elements,
|
||||
acc_cond::acc_op op)
|
||||
{
|
||||
if (elements.size() > 2)
|
||||
{
|
||||
new_cond = original;
|
||||
return false;
|
||||
}
|
||||
if (elements.size() == 2)
|
||||
{
|
||||
unsigned pos = (elements[1].back().sub.op == op
|
||||
&& elements[1][0].mark.is_singleton());
|
||||
if (!(elements[0].back().sub.op == op || pos))
|
||||
{
|
||||
new_cond = original;
|
||||
return false;
|
||||
}
|
||||
if ((elements[1 - pos].used_sets() & elements[pos][0].mark))
|
||||
{
|
||||
new_cond = original;
|
||||
return false;
|
||||
}
|
||||
if (!elements[pos][0].mark.is_singleton())
|
||||
{
|
||||
return false;
|
||||
}
|
||||
colors.push_back(elements[pos][0].mark.min_set() - 1);
|
||||
elements[1 - pos].has_parity_prefix(new_cond, colors);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
bool
|
||||
acc_cond::acc_code::has_parity_prefix(acc_cond &new_cond,
|
||||
std::vector<unsigned> &colors) const
|
||||
{
|
||||
auto disj = top_disjuncts();
|
||||
if (!(has_parity_prefix_aux((*this), new_cond, colors,
|
||||
disj, acc_cond::acc_op::Inf) ||
|
||||
has_parity_prefix_aux((*this), new_cond, colors,
|
||||
top_conjuncts(), acc_cond::acc_op::Fin)))
|
||||
new_cond = acc_cond((*this));
|
||||
return disj.size() == 2;
|
||||
}
|
||||
|
||||
bool
|
||||
acc_cond::has_parity_prefix(acc_cond& new_cond,
|
||||
std::vector<unsigned>& colors) const
|
||||
{
|
||||
return code_.has_parity_prefix(new_cond, colors);
|
||||
}
|
||||
|
||||
bool
|
||||
acc_cond::is_parity_max_equiv(std::vector<int>&permut, bool even) const
|
||||
{
|
||||
if (code_.used_once_sets() != code_.used_sets())
|
||||
return false;
|
||||
bool result = code_.is_parity_max_equiv(permut, 0, even);
|
||||
int max_value = *std::max_element(std::begin(permut), std::end(permut));
|
||||
for (unsigned i = 0; i < permut.size(); ++i)
|
||||
if (permut[i] != -1)
|
||||
permut[i] = max_value - permut[i];
|
||||
else
|
||||
permut[i] = i;
|
||||
return result;
|
||||
}
|
||||
|
||||
bool acc_cond::is_parity(bool& max, bool& odd, bool equiv) const
|
||||
{
|
||||
unsigned sets = num_;
|
||||
|
|
@ -1408,111 +1333,6 @@ namespace spot
|
|||
return patterns;
|
||||
}
|
||||
|
||||
bool
|
||||
acc_cond::acc_code::is_parity_max_equiv(std::vector<int>& permut,
|
||||
unsigned new_color,
|
||||
bool even) const
|
||||
{
|
||||
auto conj = top_conjuncts();
|
||||
auto disj = top_disjuncts();
|
||||
if (conj.size() == 1)
|
||||
{
|
||||
if (disj.size() == 1)
|
||||
{
|
||||
acc_cond::acc_code elem = conj[0];
|
||||
if ((even && elem.back().sub.op == acc_cond::acc_op::Inf)
|
||||
|| (!even && elem.back().sub.op == acc_cond::acc_op::Fin))
|
||||
{
|
||||
for (auto color : disj[0][0].mark.sets())
|
||||
{
|
||||
if (permut[color] != -1
|
||||
&& ((unsigned) permut[color]) != new_color)
|
||||
return false;
|
||||
permut[color] = new_color;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
else
|
||||
{
|
||||
std::sort(disj.begin(), disj.end(),
|
||||
[](acc_code c1, acc_code c2)
|
||||
{
|
||||
return (c1 != c2) &&
|
||||
c1.back().sub.op == acc_cond::acc_op::Inf;
|
||||
});
|
||||
unsigned i = 0;
|
||||
for (; i < disj.size() - 1; ++i)
|
||||
{
|
||||
if (disj[i].back().sub.op != acc_cond::acc_op::Inf
|
||||
|| !disj[i][0].mark.is_singleton())
|
||||
return false;
|
||||
for (auto color : disj[i][0].mark.sets())
|
||||
{
|
||||
if (permut[color] != -1
|
||||
&& ((unsigned) permut[color]) != new_color)
|
||||
return false;
|
||||
permut[color] = new_color;
|
||||
}
|
||||
}
|
||||
if (disj[i].back().sub.op == acc_cond::acc_op::Inf)
|
||||
{
|
||||
if (!even || !disj[i][0].mark.is_singleton())
|
||||
return false;
|
||||
for (auto color : disj[i][0].mark.sets())
|
||||
{
|
||||
if (permut[color] != -1
|
||||
&& ((unsigned) permut[color]) != new_color)
|
||||
return false;
|
||||
permut[color] = new_color;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
return disj[i].is_parity_max_equiv(permut, new_color + 1, even);
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
std::sort(conj.begin(), conj.end(),
|
||||
[](acc_code c1, acc_code c2)
|
||||
{
|
||||
return (c1 != c2)
|
||||
&& c1.back().sub.op == acc_cond::acc_op::Fin;
|
||||
});
|
||||
unsigned i = 0;
|
||||
for (; i < conj.size() - 1; i++)
|
||||
{
|
||||
if (conj[i].back().sub.op != acc_cond::acc_op::Fin
|
||||
|| !conj[i][0].mark.is_singleton())
|
||||
return false;
|
||||
for (auto color : conj[i][0].mark.sets())
|
||||
{
|
||||
if (permut[color] != -1 && permut[color != new_color])
|
||||
return false;
|
||||
permut[color] = new_color;
|
||||
}
|
||||
}
|
||||
if (conj[i].back().sub.op == acc_cond::acc_op::Fin)
|
||||
{
|
||||
if (even)
|
||||
return 0;
|
||||
if (!conj[i][0].mark.is_singleton())
|
||||
return false;
|
||||
for (auto color : conj[i][0].mark.sets())
|
||||
{
|
||||
if (permut[color] != -1 && permut[color != new_color])
|
||||
return false;
|
||||
permut[color] = new_color;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
return conj[i].is_parity_max_equiv(permut, new_color + 1, even);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
namespace
|
||||
{
|
||||
template<typename Fun>
|
||||
|
|
|
|||
|
|
@ -60,11 +60,6 @@ namespace spot
|
|||
/// could be removed.)
|
||||
class SPOT_API acc_cond
|
||||
{
|
||||
|
||||
public:
|
||||
bool
|
||||
has_parity_prefix(acc_cond& new_acc, std::vector<unsigned>& colors) const;
|
||||
|
||||
#ifndef SWIG
|
||||
private:
|
||||
[[noreturn]] static void report_too_many_sets();
|
||||
|
|
@ -102,10 +97,6 @@ namespace spot
|
|||
/// Initialize an empty mark_t.
|
||||
mark_t() = default;
|
||||
|
||||
mark_t
|
||||
apply_permutation(std::vector<unsigned> permut);
|
||||
|
||||
|
||||
#ifndef SWIG
|
||||
/// Create a mark_t from a range of set numbers.
|
||||
template<class iterator>
|
||||
|
|
@ -489,15 +480,6 @@ namespace spot
|
|||
acc_code
|
||||
unit_propagation();
|
||||
|
||||
bool
|
||||
has_parity_prefix(acc_cond& new_cond,
|
||||
std::vector<unsigned>& colors) const;
|
||||
|
||||
bool
|
||||
is_parity_max_equiv(std::vector<int>& permut,
|
||||
unsigned new_color,
|
||||
bool even) const;
|
||||
|
||||
bool operator==(const acc_code& other) const
|
||||
{
|
||||
unsigned pos = size();
|
||||
|
|
@ -1793,8 +1775,6 @@ namespace spot
|
|||
bool is_parity(bool& max, bool& odd, bool equiv = false) const;
|
||||
|
||||
|
||||
bool is_parity_max_equiv(std::vector<int>& permut, bool even) const;
|
||||
|
||||
/// \brief check is the acceptance condition matches one of the
|
||||
/// four type of parity acceptance defined in the HOA format.
|
||||
bool is_parity() const
|
||||
|
|
@ -1976,57 +1956,6 @@ namespace spot
|
|||
return all_;
|
||||
}
|
||||
|
||||
acc_cond
|
||||
apply_permutation(std::vector<unsigned>permut)
|
||||
{
|
||||
return acc_cond(apply_permutation_aux(permut));
|
||||
}
|
||||
|
||||
acc_code
|
||||
apply_permutation_aux(std::vector<unsigned>permut)
|
||||
{
|
||||
auto conj = top_conjuncts();
|
||||
auto disj = top_disjuncts();
|
||||
|
||||
if (conj.size() > 1)
|
||||
{
|
||||
auto transformed = std::vector<acc_code>();
|
||||
for (auto elem : conj)
|
||||
transformed.push_back(elem.apply_permutation_aux(permut));
|
||||
std::sort(transformed.begin(), transformed.end());
|
||||
auto uniq = std::unique(transformed.begin(), transformed.end());
|
||||
auto result = std::accumulate(transformed.begin(), uniq, acc_code::t(),
|
||||
[](acc_code c1, acc_code c2)
|
||||
{
|
||||
return c1 & c2;
|
||||
});
|
||||
return result;
|
||||
}
|
||||
else if (disj.size() > 1)
|
||||
{
|
||||
auto transformed = std::vector<acc_code>();
|
||||
for (auto elem : disj)
|
||||
transformed.push_back(elem.apply_permutation_aux(permut));
|
||||
std::sort(transformed.begin(), transformed.end());
|
||||
auto uniq = std::unique(transformed.begin(), transformed.end());
|
||||
auto result = std::accumulate(transformed.begin(), uniq, acc_code::f(),
|
||||
[](acc_code c1, acc_code c2)
|
||||
{
|
||||
return c1 | c2;
|
||||
});
|
||||
return result;
|
||||
}
|
||||
else
|
||||
{
|
||||
if (code_.back().sub.op == acc_cond::acc_op::Fin)
|
||||
return fin(code_[0].mark.apply_permutation(permut));
|
||||
if (code_.back().sub.op == acc_cond::acc_op::Inf)
|
||||
return inf(code_[0].mark.apply_permutation(permut));
|
||||
}
|
||||
SPOT_ASSERT(false);
|
||||
return {};
|
||||
}
|
||||
|
||||
/// \brief Check whether visiting *exactly* all sets \a inf
|
||||
/// infinitely often satisfies the acceptance condition.
|
||||
bool accepting(mark_t inf) const
|
||||
|
|
@ -2473,16 +2402,6 @@ namespace spot
|
|||
{
|
||||
return {*this};
|
||||
}
|
||||
|
||||
inline acc_cond::mark_t
|
||||
acc_cond::mark_t::apply_permutation(std::vector<unsigned> permut)
|
||||
{
|
||||
mark_t result { };
|
||||
for (auto color : sets())
|
||||
if (color < permut.size())
|
||||
result.set(permut[color]);
|
||||
return result;
|
||||
}
|
||||
}
|
||||
|
||||
namespace std
|
||||
|
|
|
|||
|
|
@ -108,15 +108,6 @@ namespace
|
|||
namespace spot
|
||||
{
|
||||
|
||||
void
|
||||
twa_graph::apply_permutation(std::vector<unsigned> permut)
|
||||
{
|
||||
for (auto& e : edges())
|
||||
{
|
||||
e.acc.apply_permutation(permut);
|
||||
}
|
||||
}
|
||||
|
||||
std::string twa_graph::format_state(unsigned n) const
|
||||
{
|
||||
if (is_univ_dest(n))
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2014-2022 Laboratoire de Recherche et Développement
|
||||
// Copyright (C) 2014-2023 Laboratoire de Recherche et Développement
|
||||
// de l'Epita.
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
|
|
@ -220,8 +220,6 @@ namespace spot
|
|||
|
||||
public:
|
||||
|
||||
void apply_permutation(std::vector<unsigned> permut);
|
||||
|
||||
twa_graph(const bdd_dict_ptr& dict)
|
||||
: twa(dict),
|
||||
init_number_(0)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue