alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

acc: remove some dead functions

Browse source 
* 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 2023-07-26 23:00:24 +02:00
parent 61e43edde8
commit 37325f1942
4 changed files with 1 additions and 273 deletions
Download patch file Download diff file Expand all files Collapse all files

180
spot/twa/acc.cc
View file

@ -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>

81
spot/twa/acc.hh
View file

@ -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();
@ -1814,8 +1796,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
@ -1997,57 +1977,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
@ -2522,16 +2451,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

9
spot/twa/twagraph.cc
View file

@ -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))

4
spot/twa/twagraph.hh
View file

@ -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)