acc.hh

// -*- coding: utf-8 -*-
// Copyright (C) 2014-2022 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
#pragma once
 
#include <functional>
#include <sstream>
#include <vector>
#include <iostream>
#include <algorithm>
#include <numeric>
#include <bddx.h>
#include <tuple>
#include <spot/misc/_config.h>
#include <spot/misc/bitset.hh>
#include <spot/misc/trival.hh>
 
namespace spot
{
  namespace internal
  {
    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
  {
#ifndef SWIG
  private:
    [[noreturn]] static void report_too_many_sets();
#endif
  public:
 
    struct mark_t :
      public internal::_32acc<SPOT_MAX_ACCSETS == 8*sizeof(unsigned)>
    {
    private:
      // configure guarantees that SPOT_MAX_ACCSETS % (8*sizeof(unsigned)) == 0
      typedef bitset<SPOT_MAX_ACCSETS / (8*sizeof(unsigned))> _value_t;
      _value_t id;
 
      mark_t(_value_t id) noexcept
        : id(id)
      {
      }
 
    public:
      mark_t() = default;
 
#ifndef SWIG
      template<class iterator>
      mark_t(const iterator& begin, const iterator& end)
        : mark_t(_value_t::zero())
      {
        for (iterator i = begin; i != end; ++i)
          if (SPOT_LIKELY(*i < SPOT_MAX_ACCSETS))
            set(*i);
          else
            report_too_many_sets();
      }
 
      mark_t(std::initializer_list<unsigned> vals)
        : mark_t(vals.begin(), vals.end())
      {
      }
 
      SPOT_DEPRECATED("use brace initialization instead")
      mark_t(unsigned i)
      {
        unsigned j = 0;
        while (i)
          {
            if (i & 1U)
              this->set(j);
            ++j;
            i >>= 1;
          }
      }
#endif
 
      constexpr static unsigned max_accsets()
      {
        return SPOT_MAX_ACCSETS;
      }
 
      static mark_t all()
      {
        return mark_t(_value_t::mone());
      }
 
      size_t hash() const noexcept
      {
        std::hash<decltype(id)> h;
        return h(id);
      }
 
      SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
      bool operator==(unsigned o) const
      {
        SPOT_ASSERT(o == 0U);
        (void)o;
        return !id;
      }
 
      SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
      bool operator!=(unsigned o) const
      {
        SPOT_ASSERT(o == 0U);
        (void)o;
        return !!id;
      }
 
      bool operator==(mark_t o) const
      {
        return id == o.id;
      }
 
      bool operator!=(mark_t o) const
      {
        return id != o.id;
      }
 
      bool operator<(mark_t o) const
      {
        return id < o.id;
      }
 
      bool operator<=(mark_t o) const
      {
        return id <= o.id;
      }
 
      bool operator>(mark_t o) const
      {
        return id > o.id;
      }
 
      bool operator>=(mark_t o) const
      {
        return id >= o.id;
      }
 
      explicit operator bool() const
      {
        return !!id;
      }
 
      bool has(unsigned u) const
      {
        return !!this->operator&(mark_t({0}) << u);
      }
 
      void set(unsigned u)
      {
        id.set(u);
      }
 
      void clear(unsigned u)
      {
        id.clear(u);
      }
 
      mark_t& operator&=(mark_t r)
      {
        id &= r.id;
        return *this;
      }
 
      mark_t& operator|=(mark_t r)
      {
        id |= r.id;
        return *this;
      }
 
      mark_t& operator-=(mark_t r)
      {
        id &= ~r.id;
        return *this;
      }
 
      mark_t& operator^=(mark_t r)
      {
        id ^= r.id;
        return *this;
      }
 
      mark_t operator&(mark_t r) const
      {
        return id & r.id;
      }
 
      mark_t operator|(mark_t r) const
      {
        return id | r.id;
      }
 
      mark_t operator-(mark_t r) const
      {
        return id & ~r.id;
      }
 
      mark_t operator~() const
      {
        return ~id;
      }
 
      mark_t operator^(mark_t r) const
      {
        return id ^ r.id;
      }
 
#if SPOT_DEBUG || defined(SWIGPYTHON)
#  define SPOT_WRAP_OP(ins)                     \
        try                                     \
          {                                     \
            ins;                                \
          }                                     \
        catch (const std::runtime_error& e)     \
          {                                     \
            report_too_many_sets();             \
          }
#else
#  define SPOT_WRAP_OP(ins) ins;
#endif
      mark_t operator<<(unsigned i) const
      {
        SPOT_WRAP_OP(return id << i);
      }
 
      mark_t& operator<<=(unsigned i)
      {
        SPOT_WRAP_OP(id <<= i; return *this);
      }
 
      mark_t operator>>(unsigned i) const
      {
        SPOT_WRAP_OP(return id >> i);
      }
 
      mark_t& operator>>=(unsigned i)
      {
        SPOT_WRAP_OP(id >>= i; return *this);
      }
#undef SPOT_WRAP_OP
 
      mark_t strip(mark_t y) const
      {
        // strip every bit of id that is marked in y
        //       100101110100.strip(
        //       001011001000)
        //   ==  10 1  11 100
        //   ==      10111100
 
        auto xv = id;                // 100101110100
        auto yv = y.id;                // 001011001000
 
        while (yv && xv)
          {
            // Mask for everything after the last 1 in y
            auto rm = (~yv) & (yv - 1);        // 000000000111
            // Mask for everything before the last 1 in y
            auto lm = ~(yv ^ (yv - 1));        // 111111110000
            xv = ((xv & lm) >> 1) | (xv & rm);
            yv = (yv & lm) >> 1;
          }
        return xv;
      }
 
      bool subset(mark_t m) const
      {
        return !((*this) - m);
      }
 
      bool proper_subset(mark_t m) const
      {
        return *this != m && this->subset(m);
      }
 
      unsigned count() const
      {
        return id.count();
      }
 
      unsigned max_set() const
      {
        if (id)
          return id.highest()+1;
        else
          return 0;
      }
 
      unsigned min_set() const
      {
        if (id)
          return id.lowest()+1;
        else
          return 0;
      }
 
      mark_t lowest() const
      {
        return id & -id;
      }
 
      bool is_singleton() const
      {
#if __GNUC__
        /* With GCC and Clang, count() is implemented using popcount. */
        return count() == 1;
#else
        return id && !(id & (id - 1));
#endif
      }
 
      bool has_many() const
      {
#if __GNUC__
        /* With GCC and Clang, count() is implemented using popcount. */
        return count() > 1;
#else
        return !!(id & (id - 1));
#endif
      }
 
      mark_t& remove_some(unsigned n)
      {
        while (n--)
          id &= id - 1;
        return *this;
      }
 
      template<class iterator>
      void fill(iterator here) const
      {
        auto a = *this;
        unsigned level = 0;
        while (a)
          {
            if (a.has(0))
              *here++ = level;
            ++level;
            a >>= 1;
          }
      }
 
      spot::internal::mark_container sets() const;
 
      SPOT_API
      friend std::ostream& operator<<(std::ostream& os, mark_t m);
 
      std::string as_string() const
      {
        std::ostringstream os;
        os << *this;
        return os.str();
      }
    };
 
    enum class acc_op : unsigned short
    { Inf, Fin, InfNeg, FinNeg, And, Or };
 
    union acc_word
    {
      mark_t mark;
      struct {
        acc_op op;             // Operator
        unsigned short size; // Size of the subtree (number of acc_word),
                             // not counting this node.
      } sub;
    };
 
    struct SPOT_API acc_code: public std::vector<acc_word>
    {
      acc_code
      unit_propagation();
 
     bool operator==(const acc_code& other) const
      {
        unsigned pos = size();
        if (other.size() != pos)
          return false;
        while (pos > 0)
          {
            auto op = (*this)[pos - 1].sub.op;
            auto sz = (*this)[pos - 1].sub.size;
            if (other[pos - 1].sub.op != op ||
                other[pos - 1].sub.size != sz)
              return false;
            switch (op)
              {
              case acc_cond::acc_op::And:
              case acc_cond::acc_op::Or:
                --pos;
                break;
              case acc_cond::acc_op::Inf:
              case acc_cond::acc_op::InfNeg:
              case acc_cond::acc_op::Fin:
              case acc_cond::acc_op::FinNeg:
                pos -= 2;
                if (other[pos].mark != (*this)[pos].mark)
                  return false;
                break;
              }
          }
        return true;
      };
 
      bool operator<(const acc_code& other) const
      {
        unsigned pos = size();
        auto osize = other.size();
        if (pos < osize)
          return true;
        if (pos > osize)
          return false;
        while (pos > 0)
          {
            auto op = (*this)[pos - 1].sub.op;
            auto oop = other[pos - 1].sub.op;
            if (op < oop)
              return true;
            if (op > oop)
              return false;
            auto sz = (*this)[pos - 1].sub.size;
            auto osz = other[pos - 1].sub.size;
            if (sz < osz)
              return true;
            if (sz > osz)
              return false;
            switch (op)
              {
              case acc_cond::acc_op::And:
              case acc_cond::acc_op::Or:
                --pos;
                break;
              case acc_cond::acc_op::Inf:
              case acc_cond::acc_op::InfNeg:
              case acc_cond::acc_op::Fin:
              case acc_cond::acc_op::FinNeg:
                {
                  pos -= 2;
                  auto m = (*this)[pos].mark;
                  auto om = other[pos].mark;
                  if (m < om)
                    return true;
                  if (m > om)
                    return false;
                  break;
                }
              }
          }
        return false;
      }
 
      bool operator>(const acc_code& other) const
      {
        return other < *this;
      }
 
      bool operator<=(const acc_code& other) const
      {
        return !(other < *this);
      }
 
      bool operator>=(const acc_code& other) const
      {
        return !(*this < other);
      }
 
      bool operator!=(const acc_code& other) const
      {
        return !(*this == other);
      }
 
      bool is_t() const
      {
        // We store "t" as an empty condition, or as Inf({}).
        unsigned s = size();
        return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
                          && !((*this)[s - 2].mark));
      }
 
      bool is_f() const
      {
        // We store "f" as Fin({}).
        unsigned s = size();
        return s > 1
          && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
      }
 
      static acc_code f()
      {
        acc_code res;
        res.resize(2);
        res[0].mark = {};
        res[1].sub.op = acc_op::Fin;
        res[1].sub.size = 1;
        return res;
      }
 
      static acc_code t()
      {
        return {};
      }
 
      static acc_code fin(mark_t m)
      {
        acc_code res;
        res.resize(2);
        res[0].mark = m;
        res[1].sub.op = acc_op::Fin;
        res[1].sub.size = 1;
        return res;
      }
 
      static acc_code fin(std::initializer_list<unsigned> vals)
      {
        return fin(mark_t(vals));
      }
 
      static acc_code fin_neg(mark_t m)
      {
        acc_code res;
        res.resize(2);
        res[0].mark = m;
        res[1].sub.op = acc_op::FinNeg;
        res[1].sub.size = 1;
        return res;
      }
 
      static acc_code fin_neg(std::initializer_list<unsigned> vals)
      {
        return fin_neg(mark_t(vals));
      }
 
      static acc_code inf(mark_t m)
      {
        acc_code res;
        res.resize(2);
        res[0].mark = m;
        res[1].sub.op = acc_op::Inf;
        res[1].sub.size = 1;
        return res;
      }
 
      static acc_code inf(std::initializer_list<unsigned> vals)
      {
        return inf(mark_t(vals));
      }
 
      static acc_code inf_neg(mark_t m)
      {
        acc_code res;
        res.resize(2);
        res[0].mark = m;
        res[1].sub.op = acc_op::InfNeg;
        res[1].sub.size = 1;
        return res;
      }
 
      static acc_code inf_neg(std::initializer_list<unsigned> vals)
      {
        return inf_neg(mark_t(vals));
      }
 
      static acc_code buchi()
      {
        return inf({0});
      }
 
      static acc_code cobuchi()
      {
        return fin({0});
      }
 
      static acc_code generalized_buchi(unsigned n)
      {
        if (n == 0)
          return inf({});
        acc_cond::mark_t m = mark_t::all();
        m >>= mark_t::max_accsets() - n;
        return inf(m);
      }
 
      static acc_code generalized_co_buchi(unsigned n)
      {
        if (n == 0)
          return fin({});
        acc_cond::mark_t m = mark_t::all();
        m >>= mark_t::max_accsets() - n;
        return fin(m);
      }
 
      static acc_code rabin(unsigned n)
      {
        acc_cond::acc_code res = f();
        while (n > 0)
          {
            res |= inf({2*n - 1}) & fin({2*n - 2});
            --n;
          }
        return res;
      }
 
      static acc_code streett(unsigned n)
      {
        acc_cond::acc_code res = t();
        while (n > 0)
          {
            res &= inf({2*n - 1}) | fin({2*n - 2});
            --n;
          }
        return res;
      }
 
      template<class Iterator>
      static acc_code generalized_rabin(Iterator begin, Iterator end)
      {
        acc_cond::acc_code res = f();
        unsigned n = 0;
        for (Iterator i = begin; i != end; ++i)
          {
            unsigned f = n++;
            acc_cond::mark_t m = {};
            for (unsigned ni = *i; ni > 0; --ni)
              m.set(n++);
            auto pair = inf(m) & fin({f});
            std::swap(pair, res);
            res |= std::move(pair);
          }
        return res;
      }
 
      static acc_code parity(bool is_max, bool is_odd, unsigned sets);
      static acc_code parity_max(bool is_odd, unsigned sets)
      {
        return parity(true, is_odd, sets);
      }
      static acc_code parity_max_odd(unsigned sets)
      {
        return parity_max(true, sets);
      }
      static acc_code parity_max_even(unsigned sets)
      {
        return parity_max(false, sets);
      }
      static acc_code parity_min(bool is_odd, unsigned sets)
      {
        return parity(false, is_odd, sets);
      }
      static acc_code parity_min_odd(unsigned sets)
      {
        return parity_min(true, sets);
      }
      static acc_code parity_min_even(unsigned sets)
      {
        return parity_min(false, sets);
      }
 
      static acc_code random(unsigned n, double reuse = 0.0);
 
      acc_code& operator&=(const acc_code& r)
      {
        if (is_t() || r.is_f())
          {
            *this = r;
            return *this;
          }
        if (is_f() || r.is_t())
          return *this;
        unsigned s = size() - 1;
        unsigned rs = r.size() - 1;
        // We want to group all Inf(x) operators:
        //   Inf(a) & Inf(b) = Inf(a & b)
        if (((*this)[s].sub.op == acc_op::Inf
             && r[rs].sub.op == acc_op::Inf)
            || ((*this)[s].sub.op == acc_op::InfNeg
                && r[rs].sub.op == acc_op::InfNeg))
          {
            (*this)[s - 1].mark |= r[rs - 1].mark;
            return *this;
          }
 
        // In the more complex scenarios, left and right may both
        // be conjunctions, and Inf(x) might be a member of each
        // side.  Find it if it exists.
        // left_inf points to the left Inf mark if any.
        // right_inf points to the right Inf mark if any.
        acc_word* left_inf = nullptr;
        if ((*this)[s].sub.op == acc_op::And)
          {
            auto start = &(*this)[s] - (*this)[s].sub.size;
            auto pos = &(*this)[s] - 1;
            pop_back();
            while (pos > start)
              {
                if (pos->sub.op == acc_op::Inf)
                  {
                    left_inf = pos - 1;
                    break;
                  }
                pos -= pos->sub.size + 1;
              }
          }
        else if ((*this)[s].sub.op == acc_op::Inf)
          {
            left_inf = &(*this)[s - 1];
          }
 
        const acc_word* right_inf = nullptr;
        auto right_end = &r.back();
        if (right_end->sub.op == acc_op::And)
          {
            auto start = &r[0];
            auto pos = --right_end;
            while (pos > start)
            {
              if (pos->sub.op == acc_op::Inf)
                {
                  right_inf = pos - 1;
                  break;
                }
              pos -= pos->sub.size + 1;
            }
          }
        else if (right_end->sub.op == acc_op::Inf)
          {
            right_inf = right_end - 1;
          }
 
        acc_cond::mark_t carry = {};
        if (left_inf && right_inf)
          {
            carry = left_inf->mark;
            auto pos = left_inf - &(*this)[0];
            erase(begin() + pos, begin() + pos + 2);
          }
        auto sz = size();
        insert(end(), &r[0], right_end + 1);
        if (carry)
          (*this)[sz + (right_inf - &r[0])].mark |= carry;
 
        acc_word w;
        w.sub.op = acc_op::And;
        w.sub.size = size();
        emplace_back(w);
        return *this;
      }
 
      acc_code operator&(const acc_code& r) const
      {
        acc_code res = *this;
        res &= r;
        return res;
      }
 
#ifndef SWIG
      acc_code operator&(acc_code&& r) const
      {
        acc_code res = *this;
        res &= r;
        return res;
      }
#endif // SWIG
 
      acc_code& operator|=(const acc_code& r)
      {
        if (is_t() || r.is_f())
          return *this;
        if (is_f() || r.is_t())
          {
            *this = r;
            return *this;
          }
        unsigned s = size() - 1;
        unsigned rs = r.size() - 1;
        // Fin(a) | Fin(b) = Fin(a | b)
        if (((*this)[s].sub.op == acc_op::Fin
             && r[rs].sub.op == acc_op::Fin)
            || ((*this)[s].sub.op == acc_op::FinNeg
                && r[rs].sub.op == acc_op::FinNeg))
          {
            (*this)[s - 1].mark |= r[rs - 1].mark;
            return *this;
          }
 
        // In the more complex scenarios, left and right may both
        // be disjunctions, and Fin(x) might be a member of each
        // side.  Find it if it exists.
        // left_inf points to the left Inf mark if any.
        // right_inf points to the right Inf mark if any.
        acc_word* left_fin = nullptr;
        if ((*this)[s].sub.op == acc_op::Or)
          {
            auto start = &(*this)[s] - (*this)[s].sub.size;
            auto pos = &(*this)[s] - 1;
            pop_back();
            while (pos > start)
              {
                if (pos->sub.op == acc_op::Fin)
                  {
                    left_fin = pos - 1;
                    break;
                  }
                pos -= pos->sub.size + 1;
              }
          }
        else if ((*this)[s].sub.op == acc_op::Fin)
          {
            left_fin = &(*this)[s - 1];
          }
 
        const acc_word* right_fin = nullptr;
        auto right_end = &r.back();
        if (right_end->sub.op == acc_op::Or)
          {
            auto start = &r[0];
            auto pos = --right_end;
            while (pos > start)
            {
              if (pos->sub.op == acc_op::Fin)
                {
                  right_fin = pos - 1;
                  break;
                }
              pos -= pos->sub.size + 1;
            }
          }
        else if (right_end->sub.op == acc_op::Fin)
          {
            right_fin = right_end - 1;
          }
 
        acc_cond::mark_t carry = {};
        if (left_fin && right_fin)
          {
            carry = left_fin->mark;
            auto pos = (left_fin - &(*this)[0]);
            this->erase(begin() + pos, begin() + pos + 2);
          }
        auto sz = size();
        insert(end(), &r[0], right_end + 1);
        if (carry)
          (*this)[sz + (right_fin - &r[0])].mark |= carry;
        acc_word w;
        w.sub.op = acc_op::Or;
        w.sub.size = size();
        emplace_back(w);
        return *this;
      }
 
#ifndef SWIG
      acc_code operator|(acc_code&& r) const
      {
        acc_code res = *this;
        res |= r;
        return res;
      }
#endif // SWIG
 
      acc_code operator|(const acc_code& r) const
      {
        acc_code res = *this;
        res |= r;
        return res;
      }
 
      acc_code& operator<<=(unsigned sets)
      {
        if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
          report_too_many_sets();
        if (empty())
          return *this;
        unsigned pos = size();
        do
          {
            switch ((*this)[pos - 1].sub.op)
              {
              case acc_cond::acc_op::And:
              case acc_cond::acc_op::Or:
                --pos;
                break;
              case acc_cond::acc_op::Inf:
              case acc_cond::acc_op::InfNeg:
              case acc_cond::acc_op::Fin:
              case acc_cond::acc_op::FinNeg:
                pos -= 2;
                (*this)[pos].mark <<= sets;
                break;
              }
          }
        while (pos > 0);
        return *this;
      }
 
      acc_code operator<<(unsigned sets) const
      {
        acc_code res = *this;
        res <<= sets;
        return res;
      }
 
      bool is_dnf() const;
 
      bool is_cnf() const;
 
      acc_code to_dnf() const;
 
      acc_code to_cnf() const;
 
      bdd to_bdd(const bdd* map) const;
 
      std::vector<acc_code> top_disjuncts() const;
 
      std::vector<acc_code> top_conjuncts() const;
 
      acc_code complement() const;
 
      mark_t fin_unit() const;
 
      mark_t inf_unit() const;
 
      int fin_one() const;
 
      std::pair<int, acc_code> fin_one_extract() const;
 
      std::tuple<int, acc_cond::acc_code, acc_cond::acc_code>
      fin_unit_one_split() const;
 
      std::vector<std::vector<int>>
        missing(mark_t inf, bool accepting) const;
 
      bool accepting(mark_t inf) const;
 
      bool inf_satisfiable(mark_t inf) const;
 
      trival maybe_accepting(mark_t infinitely_often,
                             mark_t always_present) const;
 
      std::vector<unsigned> symmetries() const;
 
      acc_code remove(acc_cond::mark_t rem, bool missing) const;
 
      acc_code strip(acc_cond::mark_t rem, bool missing) const;
      acc_code force_inf(mark_t m) const;
 
      acc_cond::mark_t used_sets() const;
 
      std::vector<std::pair<acc_cond::mark_t, acc_cond::mark_t>>
      useless_colors_patterns() const;
 
      mark_t used_once_sets() const;
 
      std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
 
      std::ostream&
      to_html(std::ostream& os,
              std::function<void(std::ostream&, int)>
              set_printer = nullptr) const;
 
      std::ostream&
      to_text(std::ostream& os,
              std::function<void(std::ostream&, int)>
              set_printer = nullptr) const;
 
      std::ostream&
      to_latex(std::ostream& os,
               std::function<void(std::ostream&, int)>
               set_printer = nullptr) const;
 
      acc_code(const char* input);
 
      acc_code()
      {
      }
 
      acc_code(const acc_word* other)
        : std::vector<acc_word>(other - other->sub.size, other + 1)
      {
      }
 
      SPOT_API
      friend std::ostream& operator<<(std::ostream& os, const acc_code& code);
    };
 
    acc_cond(unsigned n_sets = 0, const acc_code& code = {})
      : num_(0U), all_({}), code_(code)
    {
      add_sets(n_sets);
      uses_fin_acceptance_ = check_fin_acceptance();
    }
 
    acc_cond(const acc_code& code)
      : num_(0U), all_({}), code_(code)
    {
      add_sets(code.used_sets().max_set());
      uses_fin_acceptance_ = check_fin_acceptance();
    }
 
    acc_cond(const acc_cond& o)
      : num_(o.num_), all_(o.all_), code_(o.code_),
        uses_fin_acceptance_(o.uses_fin_acceptance_)
    {
    }
 
    acc_cond& operator=(const acc_cond& o)
    {
      num_ = o.num_;
      all_ = o.all_;
      code_ = o.code_;
      uses_fin_acceptance_ = o.uses_fin_acceptance_;
      return *this;
    }
 
    ~acc_cond()
    {
    }
 
    void set_acceptance(const acc_code& code)
    {
      code_ = code;
      uses_fin_acceptance_ = check_fin_acceptance();
    }
 
    const acc_code& get_acceptance() const
    {
      return code_;
    }
 
    acc_code& get_acceptance()
    {
      return code_;
    }
 
    bool operator==(const acc_cond& other) const
    {
      return other.num_sets() == num_ && other.get_acceptance() == code_;
    }
 
    bool operator!=(const acc_cond& other) const
    {
      return !(*this == other);
    }
 
    bool uses_fin_acceptance() const
    {
      return uses_fin_acceptance_;
    }
 
    bool is_t() const
    {
      return code_.is_t();
    }
 
    bool is_all() const
    {
      return num_ == 0 && is_t();
    }
 
    bool is_f() const
    {
      return code_.is_f();
    }
 
    bool is_none() const
    {
      return num_ == 0 && is_f();
    }
 
    bool is_buchi() const
    {
      unsigned s = code_.size();
      return num_ == 1 &&
        s == 2 && code_[1].sub.op == acc_op::Inf && code_[0].mark == all_sets();
    }
 
    bool is_co_buchi() const
    {
      return num_ == 1 && is_generalized_co_buchi();
    }
 
    void set_generalized_buchi()
    {
      set_acceptance(inf(all_sets()));
    }
 
    void set_generalized_co_buchi()
    {
      set_acceptance(fin(all_sets()));
    }
 
    bool is_generalized_buchi() const
    {
      unsigned s = code_.size();
      return (s == 0 && num_ == 0) || (s == 2 && code_[1].sub.op == acc_op::Inf
                                       && code_[0].mark == all_sets());
    }
 
    bool is_generalized_co_buchi() const
    {
      unsigned s = code_.size();
      return (s == 2 &&
              code_[1].sub.op == acc_op::Fin && code_[0].mark == all_sets());
    }
 
    int is_rabin() const;
 
    int is_streett() const;
 
    struct SPOT_API rs_pair
    {
#ifndef SWIG
      rs_pair() = default;
      rs_pair(const rs_pair&) = default;
      rs_pair& operator=(const rs_pair&) = default;
#endif
 
      rs_pair(acc_cond::mark_t fin, acc_cond::mark_t inf) noexcept:
        fin(fin),
        inf(inf)
        {}
      acc_cond::mark_t fin;
      acc_cond::mark_t inf;
 
      bool operator==(rs_pair o) const
      {
        return fin == o.fin && inf == o.inf;
      }
      bool operator!=(rs_pair o) const
      {
        return fin != o.fin || inf != o.inf;
      }
      bool operator<(rs_pair o) const
      {
        return fin < o.fin || (!(o.fin < fin) && inf < o.inf);
      }
      bool operator<=(rs_pair o) const
      {
        return !(o < *this);
      }
      bool operator>(rs_pair o) const
      {
        return o < *this;
      }
      bool operator>=(rs_pair o) const
      {
        return !(*this < o);
      }
    };
    bool is_streett_like(std::vector<rs_pair>& pairs) const;
 
    bool is_rabin_like(std::vector<rs_pair>& pairs) const;
 
    bool is_generalized_rabin(std::vector<unsigned>& pairs) const;
 
    bool is_generalized_streett(std::vector<unsigned>& pairs) const;
 
    bool is_parity(bool& max, bool& odd, bool equiv = false) const;
 
 
    bool is_parity() const
    {
      bool max;
      bool odd;
      return is_parity(max, odd);
    }
 
    acc_cond unit_propagation()
    {
      return acc_cond(num_, code_.unit_propagation());
    }
 
    // Return (true, m) if there exist some acceptance mark m that
    // does not satisfy the acceptance condition.  Return (false, 0U)
    // otherwise.
    std::pair<bool, acc_cond::mark_t> unsat_mark() const
    {
      return sat_unsat_mark(false);
    }
    // Return (true, m) if there exist some acceptance mark m that
    // does satisfy the acceptance condition.  Return (false, 0U)
    // otherwise.
    std::pair<bool, acc_cond::mark_t> sat_mark() const
    {
      return sat_unsat_mark(true);
    }
 
  protected:
    bool check_fin_acceptance() const;
    std::pair<bool, acc_cond::mark_t> sat_unsat_mark(bool) const;
 
  public:
    static acc_code inf(mark_t mark)
    {
      return acc_code::inf(mark);
    }
 
    static acc_code inf(std::initializer_list<unsigned> vals)
    {
      return inf(mark_t(vals.begin(), vals.end()));
    }
 
    static acc_code inf_neg(mark_t mark)
    {
      return acc_code::inf_neg(mark);
    }
 
    static acc_code inf_neg(std::initializer_list<unsigned> vals)
    {
      return inf_neg(mark_t(vals.begin(), vals.end()));
    }
 
    static acc_code fin(mark_t mark)
    {
      return acc_code::fin(mark);
    }
 
    static acc_code fin(std::initializer_list<unsigned> vals)
    {
      return fin(mark_t(vals.begin(), vals.end()));
    }
 
    static acc_code fin_neg(mark_t mark)
    {
      return acc_code::fin_neg(mark);
    }
 
    static acc_code fin_neg(std::initializer_list<unsigned> vals)
    {
      return fin_neg(mark_t(vals.begin(), vals.end()));
    }
 
    unsigned add_sets(unsigned num)
    {
      if (num == 0)
        return -1U;
      unsigned j = num_;
      num += j;
      if (num > mark_t::max_accsets())
        report_too_many_sets();
      // Make sure we do not update if we raised an exception.
      num_ = num;
      all_ = all_sets_();
      return j;
    }
 
    unsigned add_set()
    {
      return add_sets(1);
    }
 
    mark_t mark(unsigned u) const
    {
      SPOT_ASSERT(u < num_sets());
      return mark_t({u});
    }
 
    mark_t comp(const mark_t& l) const
    {
      return all_ ^ l;
    }
 
    mark_t all_sets() const
    {
      return all_;
    }
 
    bool accepting(mark_t inf) const
    {
      return code_.accepting(inf);
    }
 
    bool inf_satisfiable(mark_t inf) const
    {
      return code_.inf_satisfiable(inf);
    }
 
    trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const
    {
      return code_.maybe_accepting(infinitely_often, always_present);
    }
 
    mark_t accepting_sets(mark_t inf) const;
 
    // Deprecated since Spot 2.8
    SPOT_DEPRECATED("Use operator<< instead.")
    std::ostream& format(std::ostream& os, mark_t m) const
    {
      if (!m)
        return os;
      return os << m;
    }
 
    // Deprecated since Spot 2.8
    SPOT_DEPRECATED("Use operator<< or mark_t::as_string() instead.")
    std::string format(mark_t m) const
    {
      std::ostringstream os;
      if (m)
        os << m;
      return os.str();
    }
 
    unsigned num_sets() const
    {
      return num_;
    }
 
    template<class iterator>
    mark_t useless(iterator begin, iterator end) const
    {
      mark_t u = {};        // The set of useless sets
      for (unsigned x = 0; x < num_; ++x)
        {
          // Skip sets that are already known to be useless.
          if (u.has(x))
            continue;
          auto all = comp(u | mark_t({x}));
          // Iterate over all mark_t, and keep track of
          // set numbers that always appear with x.
          for (iterator y = begin; y != end; ++y)
            {
              const mark_t& v = *y;
              if (v.has(x))
                {
                  all &= v;
                  if (!all)
                    break;
                }
            }
          u |= all;
        }
      return u;
    }
 
    acc_cond remove(mark_t rem, bool missing) const
    {
      return {num_sets(), code_.remove(rem, missing)};
    }
 
    acc_cond strip(mark_t rem, bool missing) const
    {
      return
        { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) };
    }
 
    acc_cond force_inf(mark_t m) const
    {
      return {num_sets(), code_.force_inf(m)};
    }
 
    acc_cond restrict_to(mark_t rem) const
    {
      return {num_sets(), code_.remove(all_sets() - rem, true)};
    }
 
    std::string name(const char* fmt = "alo") const;
 
    mark_t fin_unit() const
    {
      return code_.fin_unit();
    }
 
    mark_t inf_unit() const
    {
      return code_.inf_unit();
    }
 
    int fin_one() const
    {
      return code_.fin_one();
    }
 
    std::pair<int, acc_cond> fin_one_extract() const
    {
      auto [f, c] = code_.fin_one_extract();
      return {f, {num_sets(), std::move(c)}};
    }
 
    std::tuple<int, acc_cond, acc_cond>
    fin_unit_one_split() const
    {
      auto [f, l, r] = code_.fin_unit_one_split();
      return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}};
    }
 
    std::vector<acc_cond> top_disjuncts() const;
 
    std::vector<acc_cond> top_conjuncts() const;
 
  protected:
    mark_t all_sets_() const
    {
      return mark_t::all() >> (spot::acc_cond::mark_t::max_accsets() - num_);
    }
 
    unsigned num_;
    mark_t all_;
    acc_code code_;
    bool uses_fin_acceptance_ = false;
 
  };
 
  struct rs_pairs_view {
    typedef std::vector<acc_cond::rs_pair> rs_pairs;
 
    // Creates view of pairs 'p' with restriction only to marks in 'm'
    explicit rs_pairs_view(const rs_pairs& p, const acc_cond::mark_t& m)
      : pairs_(p), view_marks_(m) {}
 
    // Creates view of pairs without restriction to marks
    explicit rs_pairs_view(const rs_pairs& p)
      : rs_pairs_view(p, acc_cond::mark_t::all()) {}
 
    acc_cond::mark_t infs() const
    {
      return do_view([&](const acc_cond::rs_pair& p)
        {
          return visible(p.inf) ? p.inf : acc_cond::mark_t({});
        });
    }
 
    acc_cond::mark_t fins() const
    {
      return do_view([&](const acc_cond::rs_pair& p)
        {
          return visible(p.fin) ? p.fin : acc_cond::mark_t({});
        });
    }
 
    acc_cond::mark_t fins_alone() const
    {
      return do_view([&](const acc_cond::rs_pair& p)
        {
          return !visible(p.inf) && visible(p.fin) ? p.fin
                                                   : acc_cond::mark_t({});
        });
    }
 
    acc_cond::mark_t infs_alone() const
    {
      return do_view([&](const acc_cond::rs_pair& p)
        {
          return !visible(p.fin) && visible(p.inf) ? p.inf
                                                   : acc_cond::mark_t({});
        });
    }
 
    acc_cond::mark_t paired_with_fin(unsigned mark) const
    {
      acc_cond::mark_t res = {};
      for (const auto& p: pairs_)
        if (p.fin.has(mark) && visible(p.fin) && visible(p.inf))
          res |= p.inf;
      return res;
    }
 
    const rs_pairs& pairs() const
    {
      return pairs_;
    }
 
  private:
    template<typename filter>
    acc_cond::mark_t do_view(const filter& filt) const
    {
      acc_cond::mark_t res = {};
      for (const auto& p: pairs_)
        res |= filt(p);
      return res;
    }
 
    bool visible(const acc_cond::mark_t& v) const
    {
      return !!(view_marks_ & v);
    }
 
    const rs_pairs& pairs_;
    acc_cond::mark_t view_marks_;
  };
 
 
  SPOT_API
  std::ostream& operator<<(std::ostream& os, const acc_cond& acc);
 
 
  namespace internal
  {
    class SPOT_API mark_iterator
    {
    public:
      typedef unsigned value_type;
      typedef const value_type& reference;
      typedef const value_type* pointer;
      typedef std::ptrdiff_t difference_type;
      typedef std::forward_iterator_tag iterator_category;
 
      mark_iterator() noexcept
        : m_({})
      {
      }
 
      mark_iterator(acc_cond::mark_t m) noexcept
        : m_(m)
      {
      }
 
      bool operator==(mark_iterator m) const
      {
        return m_ == m.m_;
      }
 
      bool operator!=(mark_iterator m) const
      {
        return m_ != m.m_;
      }
 
      value_type operator*() const
      {
        SPOT_ASSERT(m_);
        return m_.min_set() - 1;
      }
 
      mark_iterator& operator++()
      {
        m_.clear(this->operator*());
        return *this;
      }
 
      mark_iterator operator++(int)
      {
        mark_iterator it = *this;
        ++(*this);
        return it;
      }
    private:
      acc_cond::mark_t m_;
    };
 
    class SPOT_API mark_container
    {
    public:
      mark_container(spot::acc_cond::mark_t m) noexcept
        : m_(m)
      {
      }
 
      mark_iterator begin() const
      {
        return {m_};
      }
      mark_iterator end() const
      {
        return {};
      }
    private:
      spot::acc_cond::mark_t m_;
    };
  }
 
  inline spot::internal::mark_container acc_cond::mark_t::sets() const
  {
    return {*this};
  }
}
 
namespace std
{
  template<>
  struct hash<spot::acc_cond::mark_t>
  {
    size_t operator()(spot::acc_cond::mark_t m) const noexcept
    {
      return m.hash();
    }
  };
}