acc.hh 64.6 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2014-2018 Laboratoire de Recherche et Développement
// de l'Epita.
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
//
// 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/>.

20
#pragma once
21

22
23
24
25
#include <functional>
#include <sstream>
#include <vector>
#include <iostream>
26

27
28
29
30
#include <spot/misc/_config.h>
#include <spot/misc/bitset.hh>
#include <spot/misc/trival.hh>

31
32
namespace spot
{
33
34
35
  namespace internal
  {
    class mark_container;
36
37
38
39
40
41
42
43
44

    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;
    };
45
  }
46

47
48
49
50
51
52
53
54
55
56
57
  /// \ingroup twa_essentials
  /// @{

  /// \brief An acceptance condition
  ///
  /// This represent an acceptance condition in the HOA sense, that
  /// is, an acceptance formula plus a number of acceptance sets.  The
  /// acceptance formula is expected to use a subset of the acceptance
  /// sets.  (It usually uses *all* sets, otherwise that means that
  /// some of the sets have no influence on the automaton language and
  /// could be removed.)
58
  class SPOT_API acc_cond
59
  {
60
61
62

#ifndef SWIG
  private:
63
    [[noreturn]] static void report_too_many_sets();
64
#endif
65
  public:
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80

    /// \brief An acceptance mark
    ///
    /// This type is used to represent a set of acceptance sets.  It
    /// works (and is implemented) like a bit vector where bit at
    /// index i represents the membership to the i-th acceptance set.
    ///
    /// Typically, each transition of an automaton is labeled by a
    /// mark_t that represents the membership of the transition to
    /// each of the acceptance sets.
    ///
    /// For efficiency reason, the maximum number of acceptance sets
    /// (i.e., the size of the bit vector) supported is a compile-time
    /// constant.  It can be changed by passing an option to the
    /// configure script of Spot.
81
    struct mark_t :
82
      public internal::_32acc<SPOT_MAX_ACCSETS == 8*sizeof(unsigned)>
83
    {
84
    private:
85
86
      // configure guarantees that SPOT_MAX_ACCSETS % (8*sizeof(unsigned)) == 0
      typedef bitset<SPOT_MAX_ACCSETS / (8*sizeof(unsigned))> _value_t;
87
      _value_t id;
88

89
      mark_t(_value_t id) noexcept
90
        : id(id)
91
92
93
      {
      }

94
    public:
95
      /// Initialize an empty mark_t.
96
97
      mark_t() = default;

98
#ifndef SWIG
99
      /// Create a mark_t from a range of set numbers.
100
      template<class iterator>
101
      mark_t(const iterator& begin, const iterator& end)
102
        : mark_t(_value_t::zero())
103
      {
104
105
        for (iterator i = begin; i != end; ++i)
          set(*i);
106
107
      }

108
      /// Create a mark_t from a list of set numbers.
109
      mark_t(std::initializer_list<unsigned> vals)
110
        : mark_t(vals.begin(), vals.end())
111
112
113
      {
      }

114
115
116
117
118
119
120
121
122
123
124
125
      SPOT_DEPRECATED("use brace initialization instead")
      mark_t(unsigned i)
      {
        unsigned j = 0;
        while (i)
          {
            if (i & 1U)
              this->set(j);
            ++j;
            i >>= 1;
          }
      }
126
#endif
127

128
129
130
131
132
133
134
135
136
137
      /// \brief The maximum number of acceptance sets supported by
      /// this implementation.
      ///
      /// The value can be changed at compile-time using configure's
      /// --enable-max-accsets=N option.
      constexpr static unsigned max_accsets()
      {
        return SPOT_MAX_ACCSETS;
      }

138
139
140
141
142
      /// \brief A mark_t with all bits set to one.
      ///
      /// Beware that *all* bits are sets, not just the bits used in
      /// the acceptance condition.  This class is unaware of the
      /// acceptance condition.
143
144
      static mark_t all()
      {
145
        return mark_t(_value_t::mone());
146
147
      }

148
149
150
151
152
153
      size_t hash() const noexcept
      {
        std::hash<decltype(id)> h;
        return h(id);
      }

154
      SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
155
156
      bool operator==(unsigned o) const
      {
157
        SPOT_ASSERT(o == 0U);
158
        (void)o;
159
        return !id;
160
161
      }

162
      SPOT_DEPRECATED("compare mark_t to mark_t, not to unsigned")
163
164
      bool operator!=(unsigned o) const
      {
165
        SPOT_ASSERT(o == 0U);
166
        (void)o;
167
        return !!id;
168
169
170
171
      }

      bool operator==(mark_t o) const
      {
172
        return id == o.id;
173
174
175
176
      }

      bool operator!=(mark_t o) const
      {
177
        return id != o.id;
178
179
180
181
      }

      bool operator<(mark_t o) const
      {
182
        return id < o.id;
183
184
185
186
      }

      bool operator<=(mark_t o) const
      {
187
        return id <= o.id;
188
189
190
191
      }

      bool operator>(mark_t o) const
      {
192
        return id > o.id;
193
194
195
196
      }

      bool operator>=(mark_t o) const
      {
197
        return id >= o.id;
198
199
      }

200
      explicit operator bool() const
201
      {
202
        return !!id;
203
204
205
206
      }

      bool has(unsigned u) const
      {
207
        return !!this->operator&(mark_t({0}) << u);
208
209
210
211
      }

      void set(unsigned u)
      {
212
        id.set(u);
213
214
      }

215
216
      void clear(unsigned u)
      {
217
        id.clear(u);
218
219
      }

220
221
      mark_t& operator&=(mark_t r)
      {
222
223
        id &= r.id;
        return *this;
224
225
226
227
      }

      mark_t& operator|=(mark_t r)
      {
228
229
        id |= r.id;
        return *this;
230
231
232
233
      }

      mark_t& operator-=(mark_t r)
      {
234
235
        id &= ~r.id;
        return *this;
236
237
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
238
239
      mark_t& operator^=(mark_t r)
      {
240
241
        id ^= r.id;
        return *this;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
242
243
      }

244
245
      mark_t operator&(mark_t r) const
      {
246
        return id & r.id;
247
248
249
250
      }

      mark_t operator|(mark_t r) const
      {
251
        return id | r.id;
252
253
254
255
      }

      mark_t operator-(mark_t r) const
      {
256
        return id & ~r.id;
257
258
      }

259
260
      mark_t operator~() const
      {
261
        return ~id;
262
263
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
264
265
      mark_t operator^(mark_t r) const
      {
266
        return id ^ r.id;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
267
268
      }

269
#if SPOT_DEBUG || defined(SWIGPYTHON)
270
271
272
273
274
275
276
277
278
279
280
281
#  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
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
282
      mark_t operator<<(unsigned i) const
283
      {
284
        SPOT_WRAP_OP(return id << i);
285
286
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
287
      mark_t& operator<<=(unsigned i)
288
      {
289
        SPOT_WRAP_OP(id <<= i; return *this);
290
291
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
292
      mark_t operator>>(unsigned i) const
293
      {
294
        SPOT_WRAP_OP(return id >> i);
295
296
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
297
      mark_t& operator>>=(unsigned i)
298
      {
299
        SPOT_WRAP_OP(id >>= i; return *this);
300
      }
301
#undef SPOT_WRAP_OP
302

303
304
      mark_t strip(mark_t y) const
      {
305
306
307
308
309
        // strip every bit of id that is marked in y
        //       100101110100.strip(
        //       001011001000)
        //   ==  10 1  11 100
        //   ==      10111100
310

311
312
        auto xv = id;                // 100101110100
        auto yv = y.id;                // 001011001000
313

314
315
316
317
318
319
320
321
322
323
        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;
324
325
      }

326
327
      /// \brief Whether the set of bits represented by *this is a
      /// subset of those represented by \a m.
328
329
      bool subset(mark_t m) const
      {
330
        return !((*this) - m);
331
332
      }

333
334
      /// \brief Whether the set of bits represented by *this is a
      /// proper subset of those represented by \a m.
335
336
337
338
339
      bool proper_subset(mark_t m) const
      {
        return *this != m && this->subset(m);
      }

340
      /// \brief Number of bits sets.
341
342
      unsigned count() const
      {
343
        return id.count();
344
345
      }

346
347
348
349
      /// \brief The number of the highest set used plus one.
      ///
      /// If no set is used, this returns 0,
      /// If the sets {1,3,8} are used, this returns 9.
350
351
      unsigned max_set() const
      {
352
353
354
355
        if (id)
          return id.highest()+1;
        else
          return 0;
356
357
      }

358
359
360
361
      /// \brief The number of the lowest set used plus one.
      ///
      /// If no set is used, this returns 0.
      /// If the sets {1,3,8} are used, this returns 2.
362
363
      unsigned min_set() const
      {
364
365
366
        if (id)
          return id.lowest()+1;
        else
367
          return 0;
368
369
      }

370
371
372
373
      /// \brief A mark_t where all bits have been removed except the
      /// lowest one.
      ///
      /// For instance if this contains {1,3,8}, the output is {1}.
374
375
      mark_t lowest() const
      {
376
        return id & -id;
377
378
      }

379
380
381
      /// \brief Remove n bits that where set.
      ///
      /// If there are less than n bits set, the output is empty.
382
383
      mark_t& remove_some(unsigned n)
      {
384
385
386
        while (n--)
          id &= id - 1;
        return *this;
387
388
      }

389
      /// \brief Fill a container with the indices of the bits that are set.
390
391
      template<class iterator>
      void fill(iterator here) const
392
      {
393
        auto a = *this;
394
395
396
        unsigned level = 0;
        while (a)
          {
397
            if (a.has(0))
398
399
400
401
              *here++ = level;
            ++level;
            a >>= 1;
          }
402
403
      }

404
      /// Returns some iterable object that contains the used sets.
405
      spot::internal::mark_container sets() const;
406
407
408
409
410

      SPOT_API
      friend std::ostream& operator<<(std::ostream& os, mark_t m);
    };

411
    /// \brief Operators for acceptance formulas.
412
    enum class acc_op : unsigned short
413
    { Inf, Fin, InfNeg, FinNeg, And, Or };
414
415
416
417
418
419
420
421

    /// \brief A "node" in an acceptance formulas.
    ///
    /// Acceptance formulas are stored as a vector of acc_word in a
    /// kind of reverse polish notation.  Each acc_word is either an
    /// operator, or a set of acceptance sets.  Operators come with a
    /// size that represent the number of words in the subtree,
    /// current operator excluded.
422
423
424
425
    union acc_word
    {
      mark_t mark;
      struct {
426
427
428
        acc_op op;             // Operator
        unsigned short size; // Size of the subtree (number of acc_word),
                             // not counting this node.
429
      } sub;
430
431
    };

Clément Gillard's avatar
Clément Gillard committed
432
    /// \brief An acceptance formula.
433
434
435
436
437
438
439
440
441
442
443
    ///
    /// Acceptance formulas are stored as a vector of acc_word in a
    /// kind of reverse polish notation.  The motivation for this
    /// design was that we could evaluate the acceptance condition
    /// using a very simple stack-based interpreter; however it turned
    /// out that such a stack-based interpretation would prevent us
    /// from doing short-circuit evaluation, so we are not evaluating
    /// acceptance conditions this way, and maybe the implementation
    /// of acc_code could change in the future.  It's best not to rely
    /// on the fact that formulas are stored as vectors.  Use the
    /// provided methods instead.
444
    struct SPOT_API acc_code: public std::vector<acc_word>
445
    {
446
      bool operator==(const acc_code& other) const
447
      {
448
449
450
451
452
        unsigned pos = size();
        if (other.size() != pos)
          return false;
        while (pos > 0)
          {
453
454
455
456
            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)
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
              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;
475
476
      };

477
478
      bool operator<(const acc_code& other) const
      {
479
480
481
482
483
484
485
486
        unsigned pos = size();
        auto osize = other.size();
        if (pos < osize)
          return true;
        if (pos > osize)
          return false;
        while (pos > 0)
          {
487
488
            auto op = (*this)[pos - 1].sub.op;
            auto oop = other[pos - 1].sub.op;
489
490
491
492
            if (op < oop)
              return true;
            if (op > oop)
              return false;
493
494
            auto sz = (*this)[pos - 1].sub.size;
            auto osz = other[pos - 1].sub.size;
495
496
497
498
499
500
501
502
503
504
505
506
507
508
            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:
509
510
511
512
513
514
515
516
517
518
                {
                  pos -= 2;
                  auto m = (*this)[pos].mark;
                  auto om = other[pos].mark;
                  if (m < om)
                    return true;
                  if (m > om)
                    return false;
                  break;
                }
519
520
521
              }
          }
        return false;
522
523
524
525
      }

      bool operator>(const acc_code& other) const
      {
526
        return other < *this;
527
528
529
530
      }

      bool operator<=(const acc_code& other) const
      {
531
        return !(other < *this);
532
533
534
535
      }

      bool operator>=(const acc_code& other) const
      {
536
        return !(*this < other);
537
538
539
      }

      bool operator!=(const acc_code& other) const
540
      {
541
        return !(*this == other);
542
543
      }

544
545
546
547
      /// \brief Is this the "true" acceptance condition?
      ///
      /// This corresponds to "t" in the HOA format.  Under this
      /// acceptance condition, all runs are accepting.
548
      bool is_t() const
549
      {
550
        // We store "t" as an empty condition, or as Inf({}).
551
        unsigned s = size();
552
        return s == 0 || ((*this)[s - 1].sub.op == acc_op::Inf
553
                          && !((*this)[s - 2].mark));
554
555
      }

556
557
558
559
560
561
      /// \brief Is this the "false" acceptance condition?
      ///
      /// This corresponds to "f" in the HOA format.  Under this
      /// acceptance condition, no runs is accepting.  Obviously, this
      /// has very few practical application, except as neutral
      /// element in some construction.
562
      bool is_f() const
563
      {
564
        // We store "f" as Fin({}).
565
566
        unsigned s = size();
        return s > 1
567
          && (*this)[s - 1].sub.op == acc_op::Fin && !((*this)[s - 2].mark);
568
569
      }

570
571
572
573
574
575
      /// \brief Construct the "false" acceptance condition.
      ///
      /// This corresponds to "f" in the HOA format.  Under this
      /// acceptance condition, no runs is accepting.  Obviously, this
      /// has very few practical application, except as neutral
      /// element in some construction.
576
577
      static acc_code f()
      {
578
579
        acc_code res;
        res.resize(2);
580
        res[0].mark = {};
581
582
        res[1].sub.op = acc_op::Fin;
        res[1].sub.size = 1;
583
        return res;
584
585
      }

586
587
588
589
      /// \brief Construct the "true" acceptance condition.
      ///
      /// This corresponds to "t" in the HOA format.  Under this
      /// acceptance condition, all runs are accepting.
590
591
      static acc_code t()
      {
592
        return {};
593
594
      }

595
596
597
598
599
600
601
      /// \brief Construct a generalized co-Büchi acceptance
      ///
      /// For the input m={1,8,9}, this constructs Fin(1)|Fin(8)|Fin(9).
      ///
      /// Internally, such a formula is stored using a single word
      /// Fin({1,8,9}).
      /// @{
602
603
      static acc_code fin(mark_t m)
      {
604
605
606
        acc_code res;
        res.resize(2);
        res[0].mark = m;
607
608
        res[1].sub.op = acc_op::Fin;
        res[1].sub.size = 1;
609
        return res;
610
611
      }

612
613
      static acc_code fin(std::initializer_list<unsigned> vals)
      {
614
        return fin(mark_t(vals));
615
      }
616
      /// @}
617

618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
      /// \brief Construct a generalized co-Büchi acceptance for
      /// complemented sets.
      ///
      /// For the input `m={1,8,9}`, this constructs
      /// `Fin(!1)|Fin(!8)|Fin(!9)`.
      ///
      /// Internally, such a formula is stored using a single word
      /// `FinNeg({1,8,9})`.
      ///
      /// Note that `FinNeg` formulas are not supported by most methods
      /// of this class, and not supported by algorithms in Spot.
      /// This is mostly used in the parser for HOA files: if the
      /// input file uses `Fin(!0)` as acceptance condition, the
      /// condition will eventually be rewritten as `Fin(0)` by toggling
      /// the membership to set 0 of each transition.
      /// @{
634
635
      static acc_code fin_neg(mark_t m)
      {
636
637
638
        acc_code res;
        res.resize(2);
        res[0].mark = m;
639
640
        res[1].sub.op = acc_op::FinNeg;
        res[1].sub.size = 1;
641
        return res;
642
643
      }

644
645
      static acc_code fin_neg(std::initializer_list<unsigned> vals)
      {
646
        return fin_neg(mark_t(vals));
647
      }
648
      /// @}
649

650
651
652
653
654
655
656
657
      /// \brief Construct a generalized Büchi acceptance
      ///
      /// For the input `m={1,8,9}`, this constructs
      /// `Inf(1)&Inf(8)&Inf(9)`.
      ///
      /// Internally, such a formula is stored using a single word
      /// `Inf({1,8,9})`.
      /// @{
658
659
      static acc_code inf(mark_t m)
      {
660
661
662
        acc_code res;
        res.resize(2);
        res[0].mark = m;
663
664
        res[1].sub.op = acc_op::Inf;
        res[1].sub.size = 1;
665
        return res;
666
667
      }

668
669
      static acc_code inf(std::initializer_list<unsigned> vals)
      {
670
        return inf(mark_t(vals));
671
      }
672
      /// @}
673

674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
      /// \brief Construct a generalized Büchi acceptance for
      /// complemented sets.
      ///
      /// For the input `m={1,8,9}`, this constructs
      /// `Inf(!1)&Inf(!8)&Inf(!9)`.
      ///
      /// Internally, such a formula is stored using a single word
      /// `InfNeg({1,8,9})`.
      ///
      /// Note that `InfNeg` formulas are not supported by most methods
      /// of this class, and not supported by algorithms in Spot.
      /// This is mostly used in the parser for HOA files: if the
      /// input file uses `Inf(!0)` as acceptance condition, the
      /// condition will eventually be rewritten as `Inf(0)` by toggling
      /// the membership to set 0 of each transition.
      /// @{
690
691
      static acc_code inf_neg(mark_t m)
      {
692
693
694
        acc_code res;
        res.resize(2);
        res[0].mark = m;
695
696
        res[1].sub.op = acc_op::InfNeg;
        res[1].sub.size = 1;
697
        return res;
698
699
      }

700
701
      static acc_code inf_neg(std::initializer_list<unsigned> vals)
      {
702
        return inf_neg(mark_t(vals));
703
      }
704
      /// @}
705

706
707
708
      /// \brief Build a Büchi acceptance condition.
      ///
      /// This builds the formula `Inf(0)`.
709
710
      static acc_code buchi()
      {
711
        return inf({0});
712
713
      }

714
715
716
      /// \brief Build a co-Büchi acceptance condition.
      ///
      /// This builds the formula `Fin(0)`.
717
718
      static acc_code cobuchi()
      {
719
        return fin({0});
720
721
      }

722
723
724
725
726
      /// \brief Build a generalized-Büchi acceptance condition with n sets
      ///
      /// This builds the formula `Inf(0)&Inf(1)&...&Inf(n-1)`.
      ///
      /// When n is zero, the acceptance condition reduces to true.
727
728
      static acc_code generalized_buchi(unsigned n)
      {
729
730
731
        if (n == 0)
          return inf({});
        acc_cond::mark_t m = mark_t::all();
732
        m >>= mark_t::max_accsets() - n;
733
        return inf(m);
734
735
      }

736
737
738
739
740
      /// \brief Build a generalized-co-Büchi acceptance condition with n sets
      ///
      /// This builds the formula `Fin(0)|Fin(1)|...|Fin(n-1)`.
      ///
      /// When n is zero, the acceptance condition reduces to false.
741
742
      static acc_code generalized_co_buchi(unsigned n)
      {
743
744
745
        if (n == 0)
          return fin({});
        acc_cond::mark_t m = mark_t::all();
746
        m >>= mark_t::max_accsets() - n;
747
        return fin(m);
748
749
      }

750
751
752
753
      /// \brief Build a Rabin condition with n pairs.
      ///
      /// This builds the formula
      /// `(Fin(0)&Inf(1))|(Fin(2)&Inf(3))|...|(Fin(2n-2)&Inf(2n-1))`
754
755
      static acc_code rabin(unsigned n)
      {
756
757
758
759
760
761
762
        acc_cond::acc_code res = f();
        while (n > 0)
          {
            res |= inf({2*n - 1}) & fin({2*n - 2});
            --n;
          }
        return res;
763
764
      }

765
766
767
768
      /// \brief Build a Streett condition with n pairs.
      ///
      /// This builds the formula
      /// `(Fin(0)|Inf(1))&(Fin(2)|Inf(3))&...&(Fin(2n-2)|Inf(2n-1))`
769
770
      static acc_code streett(unsigned n)
      {
771
772
773
774
775
776
777
        acc_cond::acc_code res = t();
        while (n > 0)
          {
            res &= inf({2*n - 1}) | fin({2*n - 2});
            --n;
          }
        return res;
778
779
      }

780
781
782
783
784
785
786
787
788
789
790
791
      /// \brief Build a generalized Rabin condition.
      ///
      /// The two iterators should point to a range of integers, each
      /// integer being the number of Inf term in a generalized Rabin pair.
      ///
      /// For instance if the input is `[2,3,0]`, the output
      /// will have three clauses (=generalized pairs), with 2 Inf terms in
      /// the first clause, 3 in the second, and 0 in the last:
      ///   `(Fin(0)&Inf(1)&Inf(2))|Fin(3)&Inf(4)&Inf(5)&Inf(6)|Fin(7)`.
      ///
      /// Since set numbers are not reused, the number of sets used is
      /// the sum of all input integers plus their count.
792
793
      template<class Iterator>
      static acc_code generalized_rabin(Iterator begin, Iterator end)
794
      {
795
796
797
798
        acc_cond::acc_code res = f();
        unsigned n = 0;
        for (Iterator i = begin; i != end; ++i)
          {
799
            unsigned f = n++;
800
            acc_cond::mark_t m = {};
801
802
            for (unsigned ni = *i; ni > 0; --ni)
              m.set(n++);
803
            auto pair = inf(m) & fin({f});
804
805
806
807
            std::swap(pair, res);
            res |= std::move(pair);
          }
        return res;
808
809
      }

810
811
812
813
814
815
      /// \brief Build a parity acceptance condition
      ///
      /// In parity acceptance a word is accepting if the maximum (or
      /// minimum) set number that is seen infinitely often is odd (or
      /// even).  This function will build a formula for that, as
      /// specified in the HOA format.
816
817
      static acc_code parity(bool max, bool odd, unsigned sets);

818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
      /// \brief Build a random acceptance condition
      ///
      /// If \a n is 0, this will always generate the true acceptance,
      /// because working with false acceptance is somehow pointless.
      ///
      /// For \a n>0, we randomly create a term Fin(i) or Inf(i) for
      /// each set 0≤i<n.  If \a reuse>0.0, it gives the probability
      /// that a set i can generate more than one Fin(i)/Inf(i) term.
      /// Set i will be reused as long as our [0,1) random number
      /// generator gives a value ≤reuse.  (Do not set reuse≥1.0 as
      /// that will give an infinite loop.)
      ///
      /// All these Fin/Inf terms are the leaves of the tree we are
      /// building.  That tree is then build by picking two random
      /// subtrees, and joining them with & and | randomly, until we
      /// are left with a single tree.
834
835
      static acc_code random(unsigned n, double reuse = 0.0);

836
      /// \brief Conjunct the current condition in place with \a r.
837
      acc_code& operator&=(const acc_code& r)
838
      {
839
840
        if (is_t() || r.is_f())
          {
841
            *this = r;
842
843
844
845
846
847
848
849
            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)
850
851
852
853
        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))
854
855
856
857
858
859
860
861
862
863
864
          {
            (*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;
865
        if ((*this)[s].sub.op == acc_op::And)
866
          {
867
            auto start = &(*this)[s] - (*this)[s].sub.size;
868
869
870
871
            auto pos = &(*this)[s] - 1;
            pop_back();
            while (pos > start)
              {
872
                if (pos->sub.op == acc_op::Inf)
873
874
875
876
                  {
                    left_inf = pos - 1;
                    break;
                  }
877
                pos -= pos->sub.size + 1;
878
879
              }
          }
880
        else if ((*this)[s].sub.op == acc_op::Inf)
881
882
883
884
          {
            left_inf = &(*this)[s - 1];
          }

885
        const acc_word* right_inf = nullptr;
886
        auto right_end = &r.back();
887
        if (right_end->sub.op == acc_op::And)
888
889
890
891
892
          {
            auto start = &r[0];
            auto pos = --right_end;
            while (pos > start)
            {
893
              if (pos->sub.op == acc_op::Inf)
894
895
896
897
                {
                  right_inf = pos - 1;
                  break;
                }
898
              pos -= pos->sub.size + 1;
899
900
            }
          }
901
        else if (right_end->sub.op == acc_op::Inf)
902
903
904
905
          {
            right_inf = right_end - 1;
          }

906
        acc_cond::mark_t carry = {};
907
908
        if (left_inf && right_inf)
          {
909
910
911
            carry = left_inf->mark;
            auto pos = left_inf - &(*this)[0];
            erase(begin() + pos, begin() + pos + 2);
912
          }
913
914
915
916
        auto sz = size();
        insert(end(), &r[0], right_end + 1);
        if (carry)
          (*this)[sz + (right_inf - &r[0])].mark |= carry;
917
918

        acc_word w;
919
920
        w.sub.op = acc_op::And;
        w.sub.size = size();
921
        emplace_back(w);
922
        return *this;
923
924
      }

925
      /// \brief Conjunct the current condition with \a r.
926
      acc_code operator&(const acc_code& r) const
927
      {
928
929
930
        acc_code res = *this;
        res &= r;
        return res;
931
932
      }

933
      /// \brief Conjunct the current condition with \a r.
934
      acc_code operator&(acc_code&& r) const
935
936
937
938
939
940
      {
        acc_code res = *this;
        res &= r;
        return res;
      }

941
      /// \brief Disjunct the current condition in place with \a r.
942
      acc_code& operator|=(const acc_code& r)
943
      {
944
        if (is_t() || r.is_f())
945
946
          return *this;
        if (is_f() || r.is_t())
947
948
949
950
951
952
          {
            *this = r;
            return *this;
          }
        unsigned s = size() - 1;
        unsigned rs = r.size() - 1;
953
954
955
956
957
        // 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))
958
959
960
961
962
963
          {
            (*this)[s - 1].mark |= r[rs - 1].mark;
            return *this;
          }

        // In the more complex scenarios, left and right may both
964
        // be disjunctions, and Fin(x) might be a member of each
965
966
967
        // 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.
968
969
        acc_word* left_fin = nullptr;
        if ((*this)[s].sub.op == acc_op::Or)
970
          {
971
            auto start = &(*this)[s] - (*this)[s].sub.size;
972
973
974
975
            auto pos = &(*this)[s] - 1;
            pop_back();
            while (pos > start)
              {
976
                if (pos->sub.op == acc_op::Fin)
977
                  {
978
                    left_fin = pos - 1;
979
980
                    break;
                  }
981
                pos -= pos->sub.size + 1;
982
983
              }
          }
984
        else if ((*this)[s].sub.op == acc_op::Fin)
985
          {
986
            left_fin = &(*this)[s - 1];
987
988
          }

989
        const acc_word* right_fin = nullptr;
990
        auto right_end = &r.back();
991
        if (right_end->sub.op == acc_op::Or)
992
993
994
995
996
          {
            auto start = &r[0];
            auto pos = --right_end;
            while (pos > start)
            {
997
              if (pos->sub.op == acc_op::Fin)
998
                {
999
                  right_fin = pos - 1;
1000
1001
                  break;
                }
1002
              pos -= pos->sub.size + 1;
1003
1004
            }
          }
1005
        else if (right_end->sub.op == acc_op::Fin)
1006
          {
1007
            right_fin = right_end - 1;
1008
          }
1009

1010
        acc_cond::mark_t carry = {};
1011
        if (left_fin && right_fin)
1012
          {
1013
1014
1015
            carry = left_fin->mark;
            auto pos = (left_fin - &(*this)[0]);
            this->erase(begin() + pos, begin() + pos + 2);
1016
          }
1017
1018
1019
1020
        auto sz = size();
        insert(end(), &r[0], right_end + 1);
        if (carry)
          (*this)[sz + (right_fin - &r[0])].mark |= carry;
1021
        acc_word w;
1022
1023
        w.sub.op = acc_op::Or;
        w.sub.size = size();
1024
        emplace_back(w);
1025
        return *this;
1026
1027
      }

1028
      /// \brief Disjunct the current condition with \a r.
1029
      acc_code operator|(acc_code&& r) const
1030
      {
1031
1032
1033
        acc_code res = *this;
        res |= r;
        return res;
1034
1035
      }

1036
      /// \brief Disjunct the current condition with \a r.
1037
      acc_code operator|(const acc_code& r) const
1038
      {
1039
1040
1041
        acc_code res = *this;
        res |= r;
        return res;
1042
1043
      }

1044
1045
1046
1047
1048
      /// \brief Apply a left shift to all mark_t that appear in the condition.
      ///
      /// Shifting `Fin(0)&Inf(3)` by 2 will give `Fin(2)&Inf(5)`.
      ///
      /// The result is modified in place.
1049
      acc_code& operator<<=(unsigned sets)
1050
      {
1051
1052
        if (SPOT_UNLIKELY(sets >= mark_t::max_accsets()))
          report_too_many_sets();
1053
1054
1055
1056
1057
        if (empty())
          return *this;
        unsigned pos = size();
        do
          {
1058
            switch ((*this)[pos - 1].sub.op)
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
              {
              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;
1069
                (*this)[pos].mark <<= sets;
1070
1071
1072
1073
1074
                break;
              }
          }
        while (pos > 0);
        return *this;
1075
1076
      }

1077