diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 8fec855af..4c4013ce7 100644 --- a/spot/twa/acc.cc +++ b/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 &colors, - std::vector 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 &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& colors) const - { - return code_.has_parity_prefix(new_cond, colors); - } - - bool - acc_cond::is_parity_max_equiv(std::vector&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& 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 diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 6d673bb8c..766dd5224 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -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& 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 permut); - - #ifndef SWIG /// Create a mark_t from a range of set numbers. template @@ -489,15 +480,6 @@ namespace spot acc_code unit_propagation(); - bool - has_parity_prefix(acc_cond& new_cond, - std::vector& colors) const; - - bool - is_parity_max_equiv(std::vector& 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& 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::vectorpermut) - { - return acc_cond(apply_permutation_aux(permut)); - } - - acc_code - apply_permutation_aux(std::vectorpermut) - { - auto conj = top_conjuncts(); - auto disj = top_disjuncts(); - - if (conj.size() > 1) - { - auto transformed = std::vector(); - 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(); - 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 permut) - { - mark_t result { }; - for (auto color : sets()) - if (color < permut.size()) - result.set(permut[color]); - return result; - } } namespace std diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 055d6ca11..3f74d4d99 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -108,15 +108,6 @@ namespace namespace spot { - void - twa_graph::apply_permutation(std::vector permut) - { - for (auto& e : edges()) - { - e.acc.apply_permutation(permut); - } - } - std::string twa_graph::format_state(unsigned n) const { if (is_univ_dest(n)) diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 742a4d69a..1540692c6 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -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 permut); - twa_graph(const bdd_dict_ptr& dict) : twa(dict), init_number_(0)