acc.cc 55.6 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2015-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
20
//
// 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/>.


21
#include "config.h"
22
#include <iostream>
23
#include <sstream>
24
#include <set>
25
26
#include <cctype>
#include <cstring>
27
#include <map>
28
29
30
31
#include <spot/twa/acc.hh>
#include "spot/priv/bddalloc.hh"
#include <spot/misc/minato.hh>
#include <spot/misc/random.hh>
32
33
34
35
36

namespace spot
{
  std::ostream& operator<<(std::ostream& os, spot::acc_cond::mark_t m)
  {
37
    auto a = m;
38
39
40
41
42
    os << '{';
    unsigned level = 0;
    const char* comma = "";
    while (a)
      {
43
        if (a.has(0))
44
45
46
47
48
49
          {
            os << comma << level;
            comma = ",";
          }
        a >>= 1;
        ++level;
50
51
52
53
54
      }
    os << '}';
    return os;
  }

55
56
57
58
59
  std::ostream& operator<<(std::ostream& os, const acc_cond& acc)
  {
    return os << '(' << acc.num_sets() << ", " << acc.get_acceptance() << ')';
  }

60
61
  namespace
  {
62
63
64
65
66
    void default_set_printer(std::ostream& os, int v)
    {
      os << v;
    }

67
68
69
    enum code_output {HTML, TEXT, LATEX};

    template<enum code_output style>
70
71
    static void
    print_code(std::ostream& os,
72
73
               const acc_cond::acc_code& code, unsigned pos,
               std::function<void(std::ostream&, int)> set_printer)
74
    {
75
      const char* op_ = style == LATEX ? " \\lor " : " | ";
76
      auto& w = code[pos];
77
78
79
80
81
82
83
84
85
86
87
88
89
      const char* negated_pre = "";
      const char* negated_post = "";
      auto set_neg = [&]() {
        if (style == LATEX)
          {
            negated_pre = "\\overline{";
            negated_post = "}";
          }
        else
          {
            negated_pre = "!";
          }
      };
90
      bool top = pos == code.size() - 1;
91
      switch (w.sub.op)
92
93
        {
        case acc_cond::acc_op::And:
94
95
96
97
98
99
100
101
102
103
104
105
          switch (style)
            {
            case HTML:
              op_ = " &amp; ";
              break;
            case TEXT:
              op_ = " & ";
              break;
            case LATEX:
              op_ = " \\land ";
              break;
            }
106
          SPOT_FALLTHROUGH;
107
108
        case acc_cond::acc_op::Or:
          {
109
            unsigned sub = pos - w.sub.size;
110
111
112
113
114
115
116
117
118
            if (!top)
              os << '(';
            bool first = true;
            while (sub < pos)
              {
                --pos;
                if (first)
                  first = false;
                else
119
120
                  os << op_;
                print_code<style>(os, code, pos, set_printer);
121
                pos -= code[pos].sub.size;
122
123
124
125
126
127
              }
            if (!top)
              os << ')';
          }
          break;
        case acc_cond::acc_op::InfNeg:
128
          set_neg();
129
          SPOT_FALLTHROUGH;
130
131
        case acc_cond::acc_op::Inf:
          {
132
133
            auto a = code[pos - 1].mark;
            if (!a)
134
              {
135
136
137
138
                if (style == LATEX)
                  os << "\\mathsf{t}";
                else
                  os << 't';
139
140
141
142
143
144
145
146
              }
            else
              {
                if (!top)
                  // Avoid extra parentheses if there is only one set
                  top = code[pos - 1].mark.count() == 1;
                unsigned level = 0;
                const char* and_ = "";
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
                const char* and_next_ = []() {
                  // The lack of surrounding space in HTML and
                  // TEXT is on purpose: we want to
                  // distinguish those grouped "Inf"s from
                  // other terms that are ANDed together.
                  switch (style)
                    {
                    case HTML:
                      return "&amp;";
                    case TEXT:
                      return "&";
                    case LATEX:
                      return " \\land ";
                    }
                }();
162
163
                if (!top)
                  os << '(';
164
                const char* inf_ = (style == LATEX) ? "\\mathsf{Inf}(" : "Inf(";
165
166
                while (a)
                  {
167
                    if (a.has(0))
168
                      {
169
                        os << and_ << inf_ << negated_pre;
170
                        set_printer(os, level);
171
172
                        os << negated_post << ')';
                        and_ = and_next_;
173
174
175
176
177
178
179
180
181
182
                      }
                    a >>= 1;
                    ++level;
                  }
                if (!top)
                  os << ')';
              }
          }
          break;
        case acc_cond::acc_op::FinNeg:
183
          set_neg();
184
          SPOT_FALLTHROUGH;
185
186
        case acc_cond::acc_op::Fin:
          {
187
188
            auto a = code[pos - 1].mark;
            if (!a)
189
              {
190
191
192
193
                if (style == LATEX)
                  os << "\\mathsf{f}";
                else
                  os << 'f';
194
195
196
197
198
199
200
201
202
203
              }
            else
              {
                if (!top)
                  // Avoid extra parentheses if there is only one set
                  top = code[pos - 1].mark.count() == 1;
                unsigned level = 0;
                const char* or_ = "";
                if (!top)
                  os << '(';
204
                const char* fin_ = (style == LATEX) ? "\\mathsf{Fin}(" : "Fin(";
205
206
                while (a)
                  {
207
                    if (a.has(0))
208
                      {
209
                        os << or_ << fin_ << negated_pre;
210
                        set_printer(os, level);
211
212
213
214
215
216
                        os << negated_post << ')';
                        // The lack of surrounding space in HTML and
                        // TEXT is on purpose: we want to distinguish
                        // those grouped "Fin"s from other terms that
                        // are ORed together.
                        or_ = style == LATEX ? " \\lor " : "|";
217
218
219
220
221
222
223
224
225
226
                      }
                    a >>= 1;
                    ++level;
                  }
                if (!top)
                  os << ')';
              }
          }
          break;
        }
227
228
229
230
    }


    static bool
231
    eval(acc_cond::mark_t inf, const acc_cond::acc_word* pos)
232
    {
233
      switch (pos->sub.op)
234
235
236
        {
        case acc_cond::acc_op::And:
          {
237
            auto sub = pos - pos->sub.size;
238
239
240
241
242
            while (sub < pos)
              {
                --pos;
                if (!eval(inf, pos))
                  return false;
243
                pos -= pos->sub.size;
244
245
246
247
248
              }
            return true;
          }
        case acc_cond::acc_op::Or:
          {
249
            auto sub = pos - pos->sub.size;
250
251
252
253
254
            while (sub < pos)
              {
                --pos;
                if (eval(inf, pos))
                  return true;
255
                pos -= pos->sub.size;
256
257
258
259
260
261
262
263
264
265
266
              }
            return false;
          }
        case acc_cond::acc_op::Inf:
          return (pos[-1].mark & inf) == pos[-1].mark;
        case acc_cond::acc_op::Fin:
          return (pos[-1].mark & inf) != pos[-1].mark;
        case acc_cond::acc_op::FinNeg:
        case acc_cond::acc_op::InfNeg:
          SPOT_UNREACHABLE();
        }
267
268
269
      SPOT_UNREACHABLE();
      return false;
    }
270

271
272
273
274
    static trival
    partial_eval(acc_cond::mark_t infinitely_often,
                 acc_cond::mark_t always_present,
                 const acc_cond::acc_word* pos)
275
    {
276
      switch (pos->sub.op)
277
278
279
        {
        case acc_cond::acc_op::And:
          {
280
            auto sub = pos - pos->sub.size;
281
            trival res = true;
282
283
284
            while (sub < pos)
              {
                --pos;
285
286
287
288
                res = res &&
                  partial_eval(infinitely_often, always_present, pos);
                if (res.is_false())
                  return res;
289
                pos -= pos->sub.size;
290
              }
291
            return res;
292
293
294
          }
        case acc_cond::acc_op::Or:
          {
295
            auto sub = pos - pos->sub.size;
296
            trival res = false;
297
298
299
            while (sub < pos)
              {
                --pos;
300
301
302
303
                res = res ||
                  partial_eval(infinitely_often, always_present, pos);
                if (res.is_true())
                  return res;
304
                pos -= pos->sub.size;
305
              }
306
            return res;
307
308
          }
        case acc_cond::acc_op::Inf:
309
          return (pos[-1].mark & infinitely_often) == pos[-1].mark;
310
        case acc_cond::acc_op::Fin:
311
          if ((pos[-1].mark & always_present) == pos[-1].mark)
312
            return false;
313
          else if ((pos[-1].mark & infinitely_often) != pos[-1].mark)
314
            return true;
315
316
          else
            return trival::maybe();
317
318
319
320
        case acc_cond::acc_op::FinNeg:
        case acc_cond::acc_op::InfNeg:
          SPOT_UNREACHABLE();
        }
321
322
323
324
      SPOT_UNREACHABLE();
      return false;
    }

325
326
327
    static acc_cond::mark_t
    eval_sets(acc_cond::mark_t inf, const acc_cond::acc_word* pos)
    {
328
      switch (pos->sub.op)
329
330
331
        {
        case acc_cond::acc_op::And:
          {
332
            auto sub = pos - pos->sub.size;
333
            acc_cond::mark_t m = {};
334
335
336
337
338
339
            while (sub < pos)
              {
                --pos;
                if (auto s = eval_sets(inf, pos))
                  m |= s;
                else
340
                  return {};
341
                pos -= pos->sub.size;
342
343
344
345
346
              }
            return m;
          }
        case acc_cond::acc_op::Or:
          {
347
            auto sub = pos - pos->sub.size;
348
349
350
351
352
            while (sub < pos)
              {
                --pos;
                if (auto s = eval_sets(inf, pos))
                  return s;
353
                pos -= pos->sub.size;
354
              }
355
            return {};
356
357
358
359
360
          }
        case acc_cond::acc_op::Inf:
          if ((pos[-1].mark & inf) == pos[-1].mark)
            return pos[-1].mark;
          else
361
            return {};
362
363
364
365
366
        case acc_cond::acc_op::Fin:
        case acc_cond::acc_op::FinNeg:
        case acc_cond::acc_op::InfNeg:
          SPOT_UNREACHABLE();
        }
367
      SPOT_UNREACHABLE();
368
      return {};
369
    }
370
371
  }

372
  bool acc_cond::acc_code::accepting(mark_t inf) const
373
  {
374
    if (empty())
375
      return true;
376
    return eval(inf, &back());
377
378
  }

379
380
  trival acc_cond::acc_code::maybe_accepting(mark_t infinitely_often,
                                             mark_t always_present) const
381
  {
382
    if (empty())
383
      return true;
384
385
    return partial_eval(infinitely_often | always_present,
                        always_present, &back());
386
387
  }

388
389
  bool acc_cond::acc_code::inf_satisfiable(mark_t inf) const
  {
390
    return !maybe_accepting(inf, {}).is_false();
391
392
393
  }


394
395
396
397
  acc_cond::mark_t acc_cond::accepting_sets(mark_t inf) const
  {
    if (uses_fin_acceptance())
      throw std::runtime_error
398
        ("Fin acceptance is not supported by this code path.");
399
    if (code_.empty())
400
      return {};
401
402
403
    return eval_sets(inf, &code_.back());
  }

404
405
406
407
408
409
410
  bool acc_cond::check_fin_acceptance() const
  {
    if (code_.empty())
      return false;
    unsigned pos = code_.size();
    do
      {
411
        switch (code_[pos - 1].sub.op)
412
413
414
415
416
417
418
419
420
421
          {
          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:
            pos -= 2;
            break;
          case acc_cond::acc_op::Fin:
422
            if (!code_[pos - 2].mark) // f
423
424
425
426
              {
                pos -= 2;
                break;
              }
427
            SPOT_FALLTHROUGH;
428
429
430
          case acc_cond::acc_op::FinNeg:
            return true;
          }
431
432
433
434
435
      }
    while (pos > 0);
    return false;
  }

436
437
438
439
440
441

  namespace
  {
    // Is Rabin or Streett, depending on highop and lowop.
    static bool
    is_rs(const acc_cond::acc_code& code,
442
443
444
          acc_cond::acc_op highop,
          acc_cond::acc_op lowop,
          acc_cond::mark_t all_sets)
445
    {
446
447
      unsigned s = code.back().sub.size;
      auto mainop = code.back().sub.op;
448
      if (mainop == highop)
449
450
451
452
453
454
455
456
457
        {
          // The size must be a multiple of 5.
          if ((s != code.size() - 1) || (s % 5))
            return false;
        }
      else                        // Single pair?
        {
          if (s != 4 || mainop != lowop)
            return false;
458
          // Pretend we were in a unary highop.
459
460
          s = 5;
        }
461
462
      acc_cond::mark_t seen_fin = {};
      acc_cond::mark_t seen_inf = {};
463
      while (s)
464
        {
465
          if (code[--s].sub.op != lowop)
466
            return false;
467
          auto o1 = code[--s].sub.op;
468
          auto m1 = code[--s].mark;
469
          auto o2 = code[--s].sub.op;
470
471
472
473
474
475
476
477
478
479
480
481
482
483
          auto m2 = code[--s].mark;

          // We assume
          //   Fin(n) lowop Inf(n+1)
          //   o1 (m1)       o2 (m2)
          // swap if it is the converse
          if (o2 == acc_cond::acc_op::Fin)
            {
              std::swap(o1, o2);
              std::swap(m1, m2);
            }
          if (o1 != acc_cond::acc_op::Fin
              || o2 != acc_cond::acc_op::Inf
              || m1.count() != 1
484
              || m2 != (m1 << 1))
485
486
487
488
            return false;
          seen_fin |= m1;
          seen_inf |= m2;
        }
489
490

      return (!(seen_fin & seen_inf)
491
              && (seen_fin | seen_inf) == all_sets);
492
    }
493
494
495
496
497
498

    // Is Rabin-like or Streett-like, depending on highop and lowop.
    static bool
    is_rs_like(const acc_cond::acc_code& code,
              acc_cond::acc_op highop,
              acc_cond::acc_op lowop,
499
              acc_cond::acc_op singleop,
500
501
502
503
504
505
506
507
              std::vector<acc_cond::rs_pair>& pairs)
    {
      assert(pairs.empty());
      unsigned s = code.back().sub.size;
      auto mainop = code.back().sub.op;

      if (mainop == acc_cond::acc_op::Fin || mainop == acc_cond::acc_op::Inf)
        {
508
          assert(code.size() == 2);
509
510

          auto m = code[0].mark;
511
          if (mainop == singleop && m.count() != 1)
512
513
            return false;

514
515
          acc_cond::mark_t fin = {};
          acc_cond::mark_t inf = {};
516
517
518
519
520
521
          for (unsigned mark: m.sets())
            {
              if (mainop == acc_cond::acc_op::Fin)
                fin = {mark};
              else
                inf = {mark};
522

523
524
              pairs.emplace_back(fin, inf);
            }
525
526
527
528
529
530
531
532
533
534
          return true;
        }
      else if (mainop == lowop)      // Single pair?
        {
          if (s != 4)
            return false;
          // Pretend we were in a unary highop.
          s = 5;
        }
      else if (mainop != highop)
535
536
537
        {
          return false;
        }
538
539
540
541
542
543
544
545
      while (s)
        {
          auto op = code[--s].sub.op;
          auto size = code[s].sub.size;
          if (op == acc_cond::acc_op::Fin
              || op == acc_cond::acc_op::Inf)
            {
              auto m = code[--s].mark;
546
547
              acc_cond::mark_t fin = {};
              acc_cond::mark_t inf = {};
548

549
              if (op == singleop && m.count() != 1)
550
551
552
553
                {
                  pairs.clear();
                  return false;
                }
554
555
556
557
558
559
560
561
              for (unsigned mark: m.sets())
                {
                  if (op == acc_cond::acc_op::Fin)
                    fin = {mark};
                  else //fin
                    inf = {mark};
                  pairs.emplace_back(fin, inf);
                }
562
563
564
565
            }
          else
            {
              if (op != lowop || size != 4)
566
567
568
569
                {
                  pairs.clear();
                  return false;
                }
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588

              auto o1 = code[--s].sub.op;
              auto m1 = code[--s].mark;
              auto o2 = code[--s].sub.op;
              auto m2 = code[--s].mark;

              // We assume
              //   Fin(n) lowop Inf(n+1)
              //   o1 (m1)       o2 (m2)
              // swap if it is the converse
              if (o2 == acc_cond::acc_op::Fin)
                {
                  std::swap(o1, o2);
                  std::swap(m1, m2);
                }
              if (o1 != acc_cond::acc_op::Fin
                  || o2 != acc_cond::acc_op::Inf
                  || m1.count() != 1
                  || m2.count() != 1)
589
590
591
592
                {
                  pairs.clear();
                  return false;
                }
593
594
595
596
597
598
              pairs.emplace_back(m1, m2);
            }
        }

      return true;
    }
599
600
  }

601
602
  int acc_cond::is_rabin() const
  {
603
    if (code_.is_f())
604
      return num_ == 0 ? 0 : -1;
605
    if ((num_ & 1) || code_.is_t())
606
      return -1;
607
608
609
610

    if (is_rs(code_, acc_op::Or, acc_op::And, all_sets()))
      return num_ / 2;
    else
611
612
613
614
615
      return -1;
  }

  int acc_cond::is_streett() const
  {
616
    if (code_.is_t())
617
      return num_ == 0 ? 0 : -1;
618
    if ((num_ & 1) || code_.is_f())
619
      return -1;
620
621
622
623

    if (is_rs(code_, acc_op::And, acc_op::Or, all_sets()))
      return num_ / 2;
    else
624
625
626
      return -1;
  }

627
628
629
630
631
632
633
  bool acc_cond::is_streett_like(std::vector<rs_pair>& pairs) const
  {
    pairs.clear();
    if (code_.is_t())
      return true;
    if (code_.is_f())
      {
634
        pairs.emplace_back(mark_t({}), mark_t({}));
635
636
        return true;
      }
637
    return is_rs_like(code_, acc_op::And, acc_op::Or, acc_op::Fin, pairs);
638
639
640
641
642
643
644
645
646
  }

  bool acc_cond::is_rabin_like(std::vector<rs_pair>& pairs) const
  {
    pairs.clear();
    if (code_.is_f())
      return true;
    if (code_.is_t())
      {
647
        pairs.emplace_back(mark_t({}), mark_t({}));
648
649
        return true;
      }
650
    return is_rs_like(code_, acc_op::Or, acc_op::And, acc_op::Inf, pairs);
651
652
  }

653

654
  // PAIRS contains the number of Inf in each pair.
655
656
657
658
659
  bool acc_cond::is_generalized_rabin(std::vector<unsigned>& pairs) const
  {
    pairs.clear();
    if (is_generalized_co_buchi())
      {
660
661
        pairs.resize(num_);
        return true;
662
      }
663
664
665
666
    // "Acceptance: 0 f" is caught by is_generalized_rabin() above.
    // Therefore is_f() below catches "Acceptance: n f" with n>0.
    if (code_.is_f()
        || code_.is_t()
667
        || code_.back().sub.op != acc_op::Or)
668
      return false;
669

670
    auto s = code_.back().sub.size;
671
672
    acc_cond::mark_t seen_fin = {};
    acc_cond::mark_t seen_inf = {};
673
    // Each pair is the position of a Fin followed
674
675
    // by the number of Inf.
    std::map<unsigned, unsigned> p;
676
677
    while (s)
      {
678
        --s;
679
        if (code_[s].sub.op == acc_op::And)
680
          {
681
            auto o1 = code_[--s].sub.op;
682
            auto m1 = code_[--s].mark;
683
            auto o2 = code_[--s].sub.op;
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
            auto m2 = code_[--s].mark;

            // We assume
            //   Fin(n) & Inf({n+1,n+2,...,n+i})
            //   o1 (m1)       o2 (m2)
            // swap if it is the converse
            if (o2 == acc_cond::acc_op::Fin)
              {
                std::swap(o1, o2);
                std::swap(m1, m2);
              }

            if (o1 != acc_cond::acc_op::Fin
                || o2 != acc_cond::acc_op::Inf
                || m1.count() != 1)
              return false;

            unsigned i = m2.count();
            // If we have seen this pair already, it must have the
            // same size.
704
            if (p.emplace(m1.max_set() - 1, i).first->second != i)
705
706
707
708
709
710
711
712
713
714
              return false;
            assert(i > 0);
            unsigned j = m1.max_set(); // == n+1
            do
              if (!m2.has(j++))
                return false;
            while (--i);
            seen_fin |= m1;
            seen_inf |= m2;
          }
715
        else if (code_[s].sub.op == acc_op::Fin)
716
717
718
719
720
          {
            auto m1 = code_[--s].mark;
            for (auto s: m1.sets())
              // If we have seen this pair already, it must have the
              // same size.
721
722
723
724
              {
                if (p.emplace(s, 0U).first->second != 0U)
                  return false;
              }
725
726
727
728
729
730
            seen_fin |= m1;
          }
        else
          {
            return false;
          }
731
      }
732
    for (auto i: p)
733
      pairs.emplace_back(i.second);
734
    return (!(seen_fin & seen_inf)
735
            && (seen_fin | seen_inf) == all_sets());
736
737
  }

738
739
740
741
742
743
744
745
746
  // PAIRS contains the number of Inf in each pair.
  bool acc_cond::is_generalized_streett(std::vector<unsigned>& pairs) const
  {
    pairs.clear();
    if (is_generalized_buchi())
      {
        pairs.resize(num_);
        return true;
      }
747
748
749
750
    // "Acceptance: 0 t" is caught by is_generalized_buchi() above.
    // Therefore is_t() below catches "Acceptance: n t" with n>0.
    if (code_.is_t()
        || code_.is_f()
751
752
753
754
        || code_.back().sub.op != acc_op::And)
      return false;

    auto s = code_.back().sub.size;
755
756
    acc_cond::mark_t seen_fin = {};
    acc_cond::mark_t seen_inf = {};
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
    // Each pairs is the position of a Inf followed
    // by the number of Fin.
    std::map<unsigned, unsigned> p;
    while (s)
      {
        --s;
        if (code_[s].sub.op == acc_op::Or)
          {
            auto o1 = code_[--s].sub.op;
            auto m1 = code_[--s].mark;
            auto o2 = code_[--s].sub.op;
            auto m2 = code_[--s].mark;

            // We assume
            //   Inf(n) | Fin({n+1,n+2,...,n+i})
            //   o1 (m1)       o2 (m2)
            // swap if it is the converse
            if (o2 == acc_cond::acc_op::Inf)
              {
                std::swap(o1, o2);
                std::swap(m1, m2);
              }

            if (o1 != acc_cond::acc_op::Inf
                || o2 != acc_cond::acc_op::Fin
                || m1.count() != 1)
              return false;

            unsigned i = m2.count();
            // If we have seen this pair already, it must have the
            // same size.
788
            if (p.emplace(m1.max_set() - 1, i).first->second != i)
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
              return false;
            assert(i > 0);
            unsigned j = m1.max_set(); // == n+1
            do
              if (!m2.has(j++))
                return false;
            while (--i);

            seen_inf |= m1;
            seen_fin |= m2;
          }
        else if (code_[s].sub.op == acc_op::Inf)
          {
            auto m1 = code_[--s].mark;
            for (auto s: m1.sets())
              // If we have seen this pair already, it must have the
              // same size.
              if (p.emplace(s, 0U).first->second != 0U)
                return false;
            seen_inf |= m1;
          }
        else
          {
            return false;
          }
      }
    for (auto i: p)
      pairs.emplace_back(i.second);
    return (!(seen_inf & seen_fin)
            && (seen_inf | seen_fin) == all_sets());
  }

821
822
823
  acc_cond::acc_code
  acc_cond::acc_code::parity(bool max, bool odd, unsigned sets)
  {
824
825
826
827
828
    acc_cond::acc_code res;

    if (max)
      res = odd ? t() : f();
    else
829
      res = ((sets & 1) == odd) ? t() : f();
830

831
    if (sets == 0)
832
833
      return res;

834
835
836
837
838
839
840
841
842
    // When you look at something like
    //    acc-name: parity min even 5
    //    Acceptance: 5 Inf(0) | (Fin(1) & (Inf(2) | (Fin(3) & Inf(4))))
    // remember that we build it from right to left.
    int start = max ? 0 : sets - 1;
    int inc = max ? 1 : -1;
    int end = max ? sets : -1;
    for (int i = start; i != end; i += inc)
      {
843
844
845
846
        if ((i & 1) == odd)
          res |= inf({(unsigned)i});
        else
          res &= fin({(unsigned)i});
847
848
849
850
      }
    return res;
  }

851
852
853
854
855
856
857
858
859
860
861
862
863
864
  acc_cond::acc_code
  acc_cond::acc_code::random(unsigned n_accs, double reuse)
  {
    // With 0 acceptance sets, we always generate the true acceptance.
    // (Working with false is somehow pointless, and the formulas we
    // generate for n_accs>0 are always satisfiable, so it makes sense
    // that it should be satisfiable for n_accs=0 as well.)
    if (n_accs == 0)
      return {};

    std::vector<acc_cond::acc_code> codes;
    codes.reserve(n_accs);
    for (unsigned i = 0; i < n_accs; ++i)
      {
865
        codes.emplace_back(drand() < 0.5 ? inf({i}) : fin({i}));
866
867
        if (reuse > 0.0 && drand() < reuse)
          --i;
868
869
870
871
872
      }

    int s = codes.size();
    while (s > 1)
      {
873
874
        // Pick a random code and put it at the end
        int p1 = mrand(s--);
875
876
        if (p1 != s) // https://gcc.gnu.org/bugzilla//show_bug.cgi?id=59603
          std::swap(codes[p1], codes[s]);
877
878
879
880
881
882
883
884
885
        // and another one
        int p2 = mrand(s);

        if (drand() < 0.5)
          codes[p2] |= std::move(codes.back());
        else
          codes[p2] &= std::move(codes.back());

        codes.pop_back();
886
887
888
889
      }
    return codes[0];
  }

890
891
  namespace
  {
892
    bdd to_bdd_rec(const acc_cond::acc_word* c, const bdd* map)
893
    {
894
      auto sz = c->sub.size;
895
      auto start = c - sz - 1;
896
      auto op = c->sub.op;
897
      switch (op)
898
899
900
901
902
903
904
905
        {
        case acc_cond::acc_op::Or:
          {
            --c;
            bdd res = bddfalse;
            do
              {
                res |= to_bdd_rec(c, map);
906
                c -= c->sub.size + 1;
907
908
909
910
911
912
913
914
915
916
917
              }
            while (c > start);
            return res;
          }
        case acc_cond::acc_op::And:
          {
            --c;
            bdd res = bddtrue;
            do
              {
                res &= to_bdd_rec(c, map);
918
                c -= c->sub.size + 1;
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
              }
            while (c > start);
            return res;
          }
        case acc_cond::acc_op::Fin:
          {
            bdd res = bddfalse;
            for (auto i: c[-1].mark.sets())
              res |= !map[i];
            return res;
          }
        case acc_cond::acc_op::Inf:
          {
            bdd res = bddtrue;
            for (auto i: c[-1].mark.sets())
              res &= map[i];
            return res;
          }
        case acc_cond::acc_op::InfNeg:
        case acc_cond::acc_op::FinNeg:
          SPOT_UNREACHABLE();
          return bddfalse;
        }
942
      SPOT_UNREACHABLE();
943
      return bddfalse;
944
    }
945
946
947

    static bool
    equiv_codes(const acc_cond::acc_code& lhs,
948
                const acc_cond::acc_code& rhs)
949
950
951
952
953
954
955
956
957
958
959
    {
      auto used = lhs.used_sets() | rhs.used_sets();

      unsigned c = used.count();
      unsigned umax = used.max_set();

      bdd_allocator ba;
      int base = ba.allocate_variables(c);
      assert(base == 0);
      std::vector<bdd> r;
      for (unsigned i = 0; r.size() < umax; ++i)
960
        if (used.has(i))
961
          r.emplace_back(bdd_ithvar(base++));
962
        else
963
          r.emplace_back(bddfalse);
964
965
966
967
968
969
970
971
972
      return to_bdd_rec(&lhs.back(), &r[0]) == to_bdd_rec(&rhs.back(), &r[0]);
    }
  }

  bool acc_cond::is_parity(bool& max, bool& odd, bool equiv) const
  {
    unsigned sets = num_;
    if (sets == 0)
      {
973
974
975
        max = true;
        odd = is_t();
        return true;
976
977
978
979
980
981
982
983
      }
    acc_cond::mark_t u_inf;
    acc_cond::mark_t u_fin;
    std::tie(u_inf, u_fin) = code_.used_inf_fin_sets();

    odd = !u_inf.has(0);
    for (auto s: u_inf.sets())
      if ((s & 1) != odd)
984
985
986
987
        {
          max = false;             // just so the value is not uninitialized
          return false;
        }
988
989
990
991

    auto max_code = acc_code::parity(true, odd, sets);
    if (max_code == code_)
      {
992
993
        max = true;
        return true;
994
995
996
997
      }
    auto min_code = acc_code::parity(false, odd, sets);
    if (min_code == code_)
      {
998
999
        max = false;
        return true;
1000
1001
1002
1003
1004
1005
1006
      }

    if (!equiv)
      return false;

    if (equiv_codes(code_, max_code))
      {
1007
1008
        max = true;
        return true;
1009
1010
1011
      }
    if (equiv_codes(code_, min_code))
      {
1012
1013
        max = false;
        return true;
1014
1015
      }
    return false;
1016
1017
1018
1019
  }

  acc_cond::acc_code acc_cond::acc_code::to_dnf() const
  {
1020
    if (empty() || size() == 2)
1021
      return *this;
1022
1023
1024

    auto used = acc_cond::acc_code::used_sets();
    unsigned c = used.count();
1025
    unsigned max = used.max_set();
1026
1027
1028

    bdd_allocator ba;
    int base = ba.allocate_variables(c);
1029
    assert(base == 0);
1030
1031
    std::vector<bdd> r;
    std::vector<unsigned> sets(c);
1032
    for (unsigned i = 0; r.size() < max; ++i)
1033
      {
1034
1035
1036
        if (used.has(i))
          {
            sets[base] = i;
1037
            r.emplace_back(bdd_ithvar(base++));
1038
1039
1040
          }
        else
          {
1041
            r.emplace_back(bddfalse);
1042
          }
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
      }

    bdd res = to_bdd_rec(&back(), &r[0]);

    if (res == bddtrue)
      return t();
    if (res == bddfalse)
      return f();

    minato_isop isop(res);
    bdd cube;
    acc_code rescode = f();
    while ((cube = isop.next()) != bddfalse)
      {
1057
        mark_t i = {};
1058
        acc_code f;
1059
1060
1061
        while (cube != bddtrue)
          {
            // The acceptance set associated to this BDD variable
1062
            mark_t s = {};
1063
1064
1065
1066
1067
1068
1069
1070
1071
            s.set(sets[bdd_var(cube)]);

            bdd h = bdd_high(cube);
            if (h == bddfalse)        // Negative variable? -> Fin
              {
                cube = bdd_low(cube);
                // The strange order here make sure we can smaller set
                // numbers at the end of the acceptance code, i.e., at
                // the front of the output.
1072
                f = fin(s) & f;
1073
1074
1075
1076
1077
1078
1079
1080
              }
            else                // Positive variable? -> Inf
              {
                i |= s;
                cube = h;
              }
          }
        // See comment above for the order.
1081
        rescode = (inf(i) & f) | rescode;
1082
      }
1083

1084
    return rescode;
1085
1086
  }

1087
1088
1089
1090
1091
1092
1093
  acc_cond::acc_code acc_cond::acc_code::to_cnf() const
  {
    if (empty() || size() == 2)
      return *this;

    auto used = acc_cond::acc_code::used_sets();
    unsigned c = used.count();
1094
    unsigned max = used.max_set();
1095
1096
1097

    bdd_allocator ba;
    int base = ba.allocate_variables(c);
1098
    assert(base == 0);
1099
1100
    std::vector<bdd> r;
    std::vector<unsigned> sets(c);
1101
    for (unsigned i = 0; r.size() < max; ++i)
1102
      {
1103
1104
1105
        if (used.has(i))
          {
            sets[base] = i;
1106
            r.emplace_back(bdd_ithvar(base++));
1107
1108
1109
          }
        else
          {
1110
            r.emplace_back(bddfalse);
1111
          }
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
      }

    bdd res = to_bdd_rec(&back(), &r[0]);

    if (res == bddtrue)
      return t();
    if (res == bddfalse)
      return f();

    minato_isop isop(!res);
    bdd cube;
    acc_code rescode;
    while ((cube = isop.next()) != bddfalse)
      {
1126
        mark_t m = {};
1127
        acc_code i = f();
1128
1129
1130
        while (cube != bddtrue)
          {
            // The acceptance set associated to this BDD variable
1131
            mark_t s = {};
1132
1133
1134
1135
1136
1137
1138
1139
1140
            s.set(sets[bdd_var(cube)]);

            bdd h = bdd_high(cube);
            if (h == bddfalse)        // Negative variable? -> Inf
              {
                cube = bdd_low(cube);
                // The strange order here make sure we can smaller set
                // numbers at the end of the acceptance code, i.e., at
                // the front of the output.
1141
                i = inf(s) | i;
1142
1143
1144
1145
1146
1147
1148
1149
              }
            else                // Positive variable? -> Fin
              {
                m |= s;
                cube = h;
              }
          }
        // See comment above for the order.
1150
        rescode = (fin(m) | i) & rescode;
1151
1152
1153
1154
      }
    return rescode;
  }

1155
  std::pair<bool, acc_cond::mark_t>
1156
  acc_cond::unsat_mark() const
1157
  {
1158
    if (is_t())
1159
      return {false, mark_t({})};
1160
    if (!uses_fin_acceptance())
1161
      return {true, mark_t({})};
1162

1163
    auto used = code_.used_sets();
1164
    unsigned c = used.count();
1165
    unsigned max = used.max_set();
1166
1167
1168
1169
1170
1171

    bdd_allocator ba;
    int base = ba.allocate_variables(c);
    assert(base == 0);
    std::vector<bdd> r;
    std::vector<unsigned> sets(c);
1172
    for (unsigned i = 0; r.size() < max; ++i)
1173
      {
1174
1175
1176
        if (used.has(i))
          {
            sets[base] = i;
1177
            r.emplace_back(bdd_ithvar(base++));
1178
1179
1180
          }
        else
          {
1181
            r.emplace_back(bddfalse);
1182
          }
1183
1184
      }

1185
    bdd res = to_bdd_rec(&code_.back(), &r[0]);