dtwasat.cc 52.5 KB
Newer Older
1
// -*- coding: utf-8 -*-
Alexandre Duret-Lutz's avatar
typos  
Alexandre Duret-Lutz committed
2
// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et
3
// 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/>.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
20
#include <fstream>
21
22
#include <sstream>
#include <map>
23
24
#include <spot/misc/bddlt.hh>
#include <spot/misc/optionmap.hh>
25
26
#include <spot/misc/satsolver.hh>
#include <spot/misc/timer.hh>
27
28
#include <spot/priv/satcommon.hh>
#include <spot/twa/bddprint.hh>
29
#include <spot/twaalgos/complete.hh>
30
31
32
#include <spot/twaalgos/dtbasat.hh>
#include <spot/twaalgos/dtwasat.hh>
#include <spot/twaalgos/isdet.hh>
33
#include <spot/twaalgos/langmap.hh>
34
#include <spot/twaalgos/postproc.hh>
35
36
37
38
#include <spot/twaalgos/sbacc.hh>
#include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/stats.hh>
39

40
41
42
// If you set the SPOT_TMPKEEP environment variable the temporary
// file used to communicate with the sat solver will be left in
// the current directory.
43
//
44
45
// Additionally, if the following DEBUG macro is set to 1, the CNF
// file will be output with a comment before each clause, and an
46
// additional output file (dtwa-sat.dbg) will be created with a list
47
// of all positive variables in the result and their meaning.
48
49

#define DEBUG 0
50

51
52
#if DEBUG
#define dout out << "c "
53
#define cnf_comment(...)  solver.comment(__VA_ARGS__)
54
#define trace std::cerr
55
#else
56
#define cnf_comment(...) while (0) solver.comment(__VA_ARGS__)
57
58
#define dout while (0) std::cout
#define trace dout
59
60
61
62
63
64
#endif

namespace spot
{
  namespace
  {
65
66
67
    static bdd_dict_ptr debug_dict = nullptr;
    static const acc_cond* debug_ref_acc = nullptr;
    static const acc_cond* debug_cand_acc = nullptr;
68
69
70

    struct path
    {
71
72
      unsigned src_ref;
      unsigned dst_ref;
73
74
      acc_cond::mark_t acc_cand;
      acc_cond::mark_t acc_ref;
75

76
77
      path(unsigned src_ref)
        : src_ref(src_ref), dst_ref(src_ref),
78
          acc_cand(0U), acc_ref(0U)
79
80
81
      {
      }

82
     path(unsigned src_ref, unsigned dst_ref,
83
           acc_cond::mark_t acc_cand, acc_cond::mark_t acc_ref)
84
        : src_ref(src_ref), dst_ref(dst_ref),
85
          acc_cand(acc_cand), acc_ref(acc_ref)
86
87
88
89
90
      {
      }

      bool operator<(const path& other) const
      {
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
        if (this->src_ref < other.src_ref)
          return true;
        if (this->src_ref > other.src_ref)
          return false;
        if (this->dst_ref < other.dst_ref)
          return true;
        if (this->dst_ref > other.dst_ref)
          return false;
        if (this->acc_ref < other.acc_ref)
          return true;
        if (this->acc_ref > other.acc_ref)
          return false;
        if (this->acc_cand < other.acc_cand)
          return true;
        if (this->acc_cand > other.acc_cand)
          return false;
        return false;
108
109
110
111
      }

    };

112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
    // If the DNF is
    //  Fin(1)&Fin(2)&Inf(3) | Fin(0)&Inf(3) | Fin(4)&Inf(5)&Inf(6)
    // this returns the following map:
    //  {3} => [{1,2} {0}]
    //  {5} => [{4}]
    //  {6} => [{4}]
    // We use that do detect (and disallow) what we call "silly histories",
    // i.e., transitions or histories labeled by sets such as
    // {3,1,0}, that have no way to be satisfied.  So whenever we see
    // such history in a path, we actually map it to {1,0} instead,
    // which is enough to remember that this history is not satisfiable.
    // We also forbid any transition from being labeled by {3,1,0}.
    typedef std::map<unsigned, std::vector<acc_cond::mark_t>> trimming_map;
    static trimming_map
    split_dnf_acc_by_inf(const acc_cond::acc_code& input_acc)
    {
      trimming_map res;
      auto acc = input_acc.to_dnf();
      auto pos = &acc.back();
      if (pos->op == acc_cond::acc_op::Or)
132
        --pos;
133
134
135
      acc_cond::mark_t all_fin = 0U;
      auto start = &acc.front();
      while (pos > start)
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
        {
          if (pos->op == acc_cond::acc_op::Fin)
            {
              // We have only a Fin term, without Inf.
              // There is nothing to do about it.
              pos -= pos->size + 1;
            }
          else
            {
              // We have a conjunction of Fin and Inf sets.
              auto end = pos - pos->size - 1;
              acc_cond::mark_t fin = 0U;
              acc_cond::mark_t inf = 0U;
              while (pos > end)
                {
                  switch (pos->op)
                    {
                    case acc_cond::acc_op::And:
                      --pos;
                      break;
                    case acc_cond::acc_op::Fin:
                      fin |= pos[-1].mark;
                      assert(pos[-1].mark.count() == 1);
                      pos -= 2;
                      break;
                    case acc_cond::acc_op::Inf:
                      inf |= pos[-1].mark;
                      pos -= 2;
                      break;
                    case acc_cond::acc_op::FinNeg:
                    case acc_cond::acc_op::InfNeg:
                    case acc_cond::acc_op::Or:
                      SPOT_UNREACHABLE();
                      break;
                    }
                }
              assert(pos == end);

              all_fin |= fin;
              for (unsigned i: inf.sets())
                if (fin)
                  {
                    res[i].emplace_back(fin);
                  }
                else
                  {
                    // Make sure the empty set is always the first one.
                    res[i].clear();
                    res[i].emplace_back(fin);
                  }
            }
        }
188
189
190
191
192
      // Remove entries that are necessarily false because they
      // contain an emptyset, or entries that also appear as Fin
      // somewhere in the acceptance.
      auto i = res.begin();
      while (i != res.end())
193
194
195
196
197
198
        {
          if (all_fin.has(i->first) || !i->second[0])
            i = res.erase(i);
          else
            ++i;
        }
199
200
201
202

      return res;
    }

203
204
    struct dict
    {
205
      dict(const const_twa_ptr& a)
206
        : aut(a)
207
208
209
      {
      }

210
      const_twa_ptr aut;
211
212
213
214
215
216

      vars_helper helper;
      std::vector<bdd> alpha_vect;
      std::map<path, unsigned> path_map;
      std::map<bdd, unsigned, bdd_less_than> alpha_map;

217
      int nvars = 0;
218
219
      unsigned int ref_size;
      unsigned int cand_size;
220
      unsigned int cand_nacc;
221
      acc_cond::acc_code cand_acc;
222

223
224
      std::vector<acc_cond::mark_t> all_cand_acc;
      std::vector<acc_cond::mark_t> all_ref_acc;
225
226
227
      // Markings that make no sense and that we do not want to see in
      // the candidate.  See comment above split_dnf_acc_by_inf().
      std::vector<acc_cond::mark_t> all_silly_cand_acc;
228

229
      std::vector<bool> is_weak_scc;
230
      std::vector<acc_cond::mark_t> scc_marks;
231

232
      acc_cond cacc;
233
234
      trimming_map ref_inf_trim_map;
      trimming_map cand_inf_trim_map;
235

236
237
      ~dict()
      {
238
        aut->get_dict()->unregister_all_my_variables(this);
239
      }
240

241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
      int
      transid(unsigned src, unsigned cond, unsigned dst)
      {
        return helper.get_t(src, cond, dst);
      }

      int
      transid(unsigned src, bdd& cond, unsigned dst)
      {
#if DEBUG
        try
        {
          return helper.get_t(src, alpha_map.at(cond), dst);
        }
        catch (const std::out_of_range& c)
        {
          std::cerr << "label of transid " << fmt_t(src, cond, dst)
            << " not found.\n";
          throw c;
        }
#else
        return helper.get_t(src, alpha_map[cond], dst);
#endif
      }

      int
      transacc(unsigned src, unsigned cond, unsigned dst, unsigned nacc)
      {
        return helper.get_ta(src, cond, dst, nacc);
      }

      int
      transacc(unsigned src, bdd& cond, unsigned dst, unsigned nacc)
      {
#if DEBUG
        try
        {
          return helper.get_ta(src, alpha_map.at(cond), dst, nacc);
        }
        catch (const std::out_of_range& c)
        {
          std::cerr << "label of transacc " << fmt_ta(src, cond, dst, nacc)
            << " not found.\n";
          throw c;
        }
#else
        return helper.get_ta(src, alpha_map[cond], dst, nacc);
#endif
      }

      int
      pathid(unsigned src_cand, unsigned src_ref, unsigned dst_cand,
          unsigned dst_ref, acc_cond::mark_t acc_cand = 0U,
          acc_cond::mark_t acc_ref = 0U)
      {
#if DEBUG
        try
        {
          return helper.get_p(
              path_map.at(path(src_ref, dst_ref, acc_cand, acc_ref)),
              src_cand, dst_cand);
        }
        catch (const std::out_of_range& c)
        {
          std::cerr << "path(" << src_ref << ',' << dst_ref << ",...) of pathid"
            << ' '
            << fmt_p(src_cand, src_ref, dst_cand, dst_ref, acc_cand, acc_ref)
            << " not found.\n";
          throw c;
        }
#else
        return helper.get_p(
            path_map[path(src_ref, dst_ref, acc_cand, acc_ref)],
            src_cand, dst_cand);
#endif
      }

#if DEBUG
      int
      pathid(unsigned path, unsigned src_cand, unsigned dst_cand)
      {
        return helper.get_p(path, src_cand, dst_cand);
      }
#endif

      std::string
      fmt_t(unsigned src, bdd& cond, unsigned dst)
      {
        return helper.format_t(debug_dict, src, cond, dst);
      }

      std::string
      fmt_t(unsigned src, unsigned cond, unsigned dst)
      {
        return helper.format_t(debug_dict, src, alpha_vect[cond], dst);
      }

      std::string
      fmt_ta(unsigned src, bdd& cond, unsigned dst, unsigned nacc)
      {
        return helper.format_ta(debug_dict, debug_cand_acc, src, cond,
            dst, cacc.mark(nacc));
      }

      std::string
      fmt_ta(unsigned src, unsigned cond, unsigned dst, unsigned nacc)
      {
        return helper.format_ta(debug_dict, debug_cand_acc, src,
            alpha_vect[cond], dst, cacc.mark(nacc));
      }

      std::string
      fmt_p(unsigned src_cand, unsigned src_ref, unsigned dst_cand,
          unsigned dst_ref, acc_cond::mark_t acc_cand = 0U,
          acc_cond::mark_t acc_ref = 0U)
      {
        return helper.format_p(debug_cand_acc, debug_ref_acc, src_cand,
            src_ref, dst_cand, dst_ref, acc_cand, acc_ref);
      }

361
362
363
      acc_cond::mark_t
      inf_trim(acc_cond::mark_t m, trimming_map& tm)
      {
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
        for (auto& s: tm)
          {
            unsigned inf = s.first;
            if (m.has(inf))
              {
                bool remove = true;
                for (auto fin: s.second)
                  if (!(m & fin))
                    {
                      remove = false;
                      break;
                    }
                if (remove)
                  m.clear(inf);
              }
          }
        return m;
381
382
383
384
385
      }

      acc_cond::mark_t
      ref_inf_trim(acc_cond::mark_t m)
      {
386
        return inf_trim(m, ref_inf_trim_map);
387
388
389
390
391
      }

      acc_cond::mark_t
      cand_inf_trim(acc_cond::mark_t m)
      {
392
        return inf_trim(m, cand_inf_trim_map);
393
      }
394
395
396
    };


397
    void declare_vars(const const_twa_graph_ptr& aut,
398
                          dict& d, bdd ap, bool state_based, scc_info& sm)
399
    {
400
401
402
      d.is_weak_scc = sm.weak_sccs();
      unsigned scccount = sm.scc_count();
      {
403
404
405
406
407
408
409
410
411
        auto tmp = sm.used_acc();
        d.scc_marks.reserve(scccount);
        for (auto& v: tmp)
          {
            acc_cond::mark_t m = 0U;
            for (auto i: v)
              m |= i;
            d.scc_marks.emplace_back(m);
          }
412
413
      }

414
      d.cacc.add_sets(d.cand_nacc);
415
416
417
418
419
      d.cacc.set_acceptance(d.cand_acc);

      // If the acceptance conditions use both Fin and Inf primitives,
      // we may have some silly history configurations to ignore.
      if (aut->acc().uses_fin_acceptance())
420
        d.ref_inf_trim_map = split_dnf_acc_by_inf(aut->get_acceptance());
421
      if (d.cacc.uses_fin_acceptance())
422
        d.cand_inf_trim_map = split_dnf_acc_by_inf(d.cand_acc);
423
424

      bdd_dict_ptr bd = aut->get_dict();
425
      d.all_cand_acc.emplace_back(0U);
426
      for (unsigned n = 0; n < d.cand_nacc; ++n)
427
428
429
430
431
        {
          auto c = d.cacc.mark(n);

          size_t ss = d.all_silly_cand_acc.size();
          for (size_t i = 0; i < ss; ++i)
432
            d.all_silly_cand_acc.emplace_back(d.all_silly_cand_acc[i] | c);
433
434
435
436
437
438

          size_t s = d.all_cand_acc.size();
          for (size_t i = 0; i < s; ++i)
            {
              acc_cond::mark_t m = d.all_cand_acc[i] | c;
              if (d.cand_inf_trim(m) == m)
439
                d.all_cand_acc.emplace_back(m);
440
              else
441
                d.all_silly_cand_acc.emplace_back(m);
442
443
            }
        }
444

445
      d.all_ref_acc.emplace_back(0U);
446
      unsigned ref_nacc = aut->num_sets();
447
      for (unsigned n = 0; n < ref_nacc; ++n)
448
449
450
451
452
453
454
455
        {
          auto c = aut->acc().mark(n);
          size_t s = d.all_ref_acc.size();
          for (size_t i = 0; i < s; ++i)
            {
              acc_cond::mark_t m = d.all_ref_acc[i] | c;
              if (d.ref_inf_trim(m) != m)
                continue;
456
              d.all_ref_acc.emplace_back(m);
457
458
            }
        }
459

460
      d.ref_size = aut->num_states();
461

462
      if (d.cand_size == -1U)
463
        for (unsigned i = 0; i < d.ref_size; ++i)
464
465
466
467
          if (sm.reachable_state(i))
            ++d.cand_size;      // Note that we start from -1U the
                                // cand_size is one less than the
                                // number of reachable states.
468

469
470
471
472
473
474
475
476
477
478
479
480
      // In order to optimize memory usage, src_cand & dst_cand have been
      // removed from path struct (the reasons are: they were no optimization
      // on them and their values are known from the beginning).
      //
      // However, since some optimizations are based on the following i, k, f,
      // refhist, it is necessary to associate to each path constructed,
      // an ID number.
      //
      // Given this ID, src_cand, dst_cand, the corresponding litteral can be
      // retrived thanks to get_prc(...) a vars_helper's method.
      unsigned path_size = 0;
      for (unsigned i = 0; i < d.ref_size; ++i)
481
482
483
484
485
        {
          if (!sm.reachable_state(i))
            continue;
          unsigned i_scc = sm.scc_of(i);
          bool is_weak = d.is_weak_scc[i_scc];
486
          for (unsigned k = 0; k < d.ref_size; ++k)
487
            {
488
489
490
491
492
493
494
              if (!sm.reachable_state(k))
                continue;
              if (sm.scc_of(k) != i_scc)
                continue;
              size_t sfp = is_weak ? 1 : d.all_ref_acc.size();
              acc_cond::mark_t sccmarks = d.scc_marks[i_scc];
              for (size_t fp = 0; fp < sfp; ++fp)
495
                {
496
497
498
                  auto refhist = d.all_ref_acc[fp];
                  // refhist cannot have more sets than used in the SCC.
                  if (!is_weak && (sccmarks & refhist) != refhist)
499
500
                    continue;

501
502
503
504
505
                  size_t sf = d.all_cand_acc.size();
                  for (size_t f = 0; f < sf; ++f)
                    {
                      path p(i, k, d.all_cand_acc[f], refhist);
                      d.path_map[p] = path_size++;
506
507
508
509
                    }
                }
            }
        }
510

511
512
513
514
515
516
      // Fill dict's bdd vetor (alpha_vect) and save each bdd and it's
      // corresponding index in alpha_map. This is necessary beacause some
      // loops start from a precise bdd. Therefore, it's useful to know
      // it's corresponding index to deal with vars_helper.
      bdd all = bddtrue;
      for (unsigned j = 0; all != bddfalse; ++j)
517
        {
518
519
520
521
          bdd one = bdd_satoneset(all, ap, bddfalse);
          d.alpha_vect.push_back(one);
          d.alpha_map[d.alpha_vect[j]] = j;
          all -= one;
522
523
        }

524
525
526
527
      // Initialize vars_helper by giving it all the necessary information.
      // false: means dtwasat, i-e not dtbasat.
      d.helper.init(d.cand_size, d.alpha_vect.size(), d.cand_size,
          d.cand_nacc, path_size, state_based, false);
528

529
530
      // Based on all previous informations, helper knows all litterals.
      d.helper.declare_all_vars(++d.nvars);
531
    }
532

533
534
    typedef std::pair<int, int> sat_stats;

535
    static
536
537
538
539
540
    sat_stats dtwa_to_sat(satsolver& solver,
                          const_twa_graph_ptr ref,
                          dict& d,
                          bool state_based,
                          bool colored)
541
    {
542
543
544
#if DEBUG
      debug_dict = ref->get_dict();
#endif
545
546
      // Compute the AP used.
      bdd ap = ref->ap_vars();
547

548
      // Count the number of atomic propositions.
549
550
      int nap = 0;
      {
551
552
553
554
555
556
557
        bdd cur = ap;
        while (cur != bddtrue)
          {
            ++nap;
            cur = bdd_high(cur);
          }
        nap = 1 << nap;
558
      }
559

560
      scc_info sm(ref);
561
      sm.determine_unknown_acceptance();
562
563

      // Number all the SAT variables we may need.
564
565
566
567
      declare_vars(ref, d, ap, state_based, sm);

      // Store alphabet size once for all.
      unsigned alpha_size = d.alpha_vect.size();
568

569
      // Tell the satsolver the number of variables.
570
571
      solver.adjust_nvars(d.nvars);

572
      // Empty automaton is impossible.
573
      assert(d.cand_size > 0);
574

575
#if DEBUG
576
577
      debug_ref_acc = &ref->acc();
      debug_cand_acc = &d.cacc;
578
579
      solver.comment("d.ref_size:", d.ref_size, '\n');
      solver.comment("d.cand_size:", d.cand_size, '\n');
580
#endif
581
      auto& racc = ref->acc();
582

583
      cnf_comment("symmetry-breaking clauses\n");
584
      int j = 0;
585
586
587
588
589
590
591
592
      for (unsigned l = 0; l < alpha_size; ++l, ++j)
        for (unsigned i = 0; i < d.cand_size - 1; ++i)
          for (unsigned k = i * nap + j + 2; k < d.cand_size; ++k)
            {
              cnf_comment("¬", d.fmt_t(i, l, k), '\n');
              solver.add({-d.transid(i, l, k), 0});
            }

593
594
      if (!solver.get_nb_clauses())
        cnf_comment("(none)\n");
595

596
      cnf_comment("(8) the candidate automaton is complete\n");
597
      for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
598
599
        for (unsigned l = 0; l < alpha_size; ++l)
          {
600
#if DEBUG
601
602
603
604
605
606
607
608
            solver.comment("");
            for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
              {
                solver.comment_rec(d.fmt_t(q1, l, q2), "δ");
                if (q2 != d.cand_size)
                  solver.comment_rec(" ∨ ");
              }
            solver.comment_rec('\n');
609
#endif
610
611
612
613
            for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
              solver.add(d.transid(q1, l, q2));
            solver.add(0);
          }
614

615
      cnf_comment("(9) the initial state is reachable\n");
616
      {
617
        unsigned init = ref->get_init_state_number();
618
619
        cnf_comment(d.fmt_p(0, init, 0, init), '\n');
        solver.add({d.pathid(0, init, 0, init), 0});
620
      }
621

622
      if (colored)
623
624
        {
          unsigned nacc = d.cand_nacc;
625
          cnf_comment("transitions belong to exactly one of the", nacc,
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
                      "acceptance set\n");
          for (unsigned l = 0; l < alpha_size; ++l)
            for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
              for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
                {
                  for (unsigned i = 0; i < nacc; ++i)
                    for (unsigned j = 0; j < nacc; ++j)
                      if (i != j)
                        solver.add(
                            {-d.transacc(q1, l, q2, i),
                             -d.transacc(q1, l, q2, j),
                             0});
                  for (unsigned i = 0; i < nacc; ++i)
                    solver.add(d.transacc(q1, l, q2, i));
                  solver.add(0);
                }
        }

      if (!d.all_silly_cand_acc.empty())
        {
          cnf_comment("no transition with silly acceptance\n");
          for (unsigned l = 0; l < alpha_size; ++l)
            for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
              for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
                for (auto& s: d.all_silly_cand_acc)
651
                  {
652
653
654
655
                    cnf_comment("no (", q1, ',',
                        bdd_format_formula(debug_dict, d.alpha_vect[l]),
                        ',', s, ',', q2, ")\n");
                    for (unsigned v: s.sets())
656
                      {
657
658
659
                        int tai = d.transacc(q1, l, q2, v);
                        assert(tai != 0);
                        solver.add(-tai);
660
                      }
661
                    for (unsigned v: d.cacc.comp(s).sets())
662
                      {
663
664
                        int tai = d.transacc(q1, l, q2, v);
                        assert(tai != 0);
665
                        solver.add(tai);
666
                      }
667
                    solver.add(0);
668
669
                  }
        }
670

671
      for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
672
        for (unsigned q1p = 0; q1p < d.ref_size; ++q1p)
673
674
675
          {
            if (!sm.reachable_state(q1p))
              continue;
676
677
            cnf_comment("(10) augmenting paths based on Cand[", q1,
                        "] and Ref[", q1p, "]\n");
678

679
            int p1id = d.pathid(q1, q1p, q1, q1p);
680
681
682
683
684
685
686
687
688
689
690
            for (auto& tr: ref->out(q1p))
              {
                unsigned dp = tr.dst;
                bdd all = tr.cond;
                while (all != bddfalse)
                  {
                    bdd s = bdd_satoneset(all, ap, bddfalse);
                    all -= s;

                    for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
                      {
691
                        int succ = d.pathid(q2, dp, q2, dp);
692
693
694
                        if (p1id == succ)
                          continue;

695
696
697
698
                        cnf_comment(d.fmt_p(q1, q1p, q1, q1p), " ∧ ",
                                    d.fmt_t(q1, s, q2), "δ → ",
                                    d.fmt_p(q2, dp, q2, dp), '\n');
                        solver.add({-p1id, -d.transid(q1, s, q2), succ, 0});
699
700
701
702
                      }
                  }
              }
          }
703
704

      // construction of constraints (11,12,13)
705
      for (unsigned q1p = 0; q1p < d.ref_size; ++q1p)
706
707
708
709
        {
          if (!sm.reachable_state(q1p))
            continue;
          unsigned q1p_scc = sm.scc_of(q1p);
710
          for (unsigned q2p = 0; q2p < d.ref_size; ++q2p)
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
            {
              if (!sm.reachable_state(q2p))
                continue;
              // We are only interested in transition that can form a
              // cycle, so they must belong to the same SCC.
              if (sm.scc_of(q2p) != q1p_scc)
                continue;
              bool is_weak = d.is_weak_scc[q1p_scc];
              bool is_rej = sm.is_rejecting_scc(q1p_scc);

              for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
                for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
                  {
                    size_t sf = d.all_cand_acc.size();
                    size_t sfp = is_weak ? 1 : d.all_ref_acc.size();
                    acc_cond::mark_t sccmarks = d.scc_marks[q1p_scc];

                    for (size_t f = 0; f < sf; ++f)
                      for (size_t fp = 0; fp < sfp; ++fp)
                        {
                          auto refhist = d.all_ref_acc[fp];
                          // refhist cannot have more sets than used in the SCC
                          if (!is_weak && (sccmarks & refhist) != refhist)
                            continue;

736
737
738
739
740
741
                          acc_cond::mark_t candhist_p = d.all_cand_acc[f];
                          std::string f_p =
                              d.fmt_p(q1, q1p, q2, q2p, candhist_p, refhist);
                          cnf_comment("(11&12&13) paths from ", f_p, '\n');
                          int pid =
                            d.pathid(q1, q1p, q2, q2p, candhist_p, refhist);
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
                          for (auto& tr: ref->out(q2p))
                            {
                              unsigned dp = tr.dst;
                              // Skip destinations not in the SCC.
                              if (sm.scc_of(dp) != q1p_scc)
                                continue;

                              for (unsigned q3 = 0; q3 < d.cand_size; ++q3)
                                {
                                  bdd all = tr.cond;
                                  acc_cond::mark_t curacc = tr.acc;
                                  while (all != bddfalse)
                                    {
                                      bdd l = bdd_satoneset(all, ap, bddfalse);
                                      all -= l;

758
                                      int ti = d.transid(q2, l, q3);
759
760
761
762
763
764
765
                                      if (dp == q1p && q3 == q1) // (11,12) loop
                                        {
                                          bool rejloop =
                                            (is_rej ||
                                             !racc.accepting
                                             (curacc | d.all_ref_acc[fp]));

766
767
                                          auto missing = d.cand_acc
                                            .missing(candhist_p, !rejloop);
768
769
770

                                          for (auto& v: missing)
                                            {
771
#if DEBUG
772
                                              solver.comment((rejloop ?
773
774
775
                                                       "(11) " : "(12) "), f_p,
                                                  " ∧ ", d.fmt_t(q2, l, q3),
                                                  "δ → (");
776
777
778
779
                                              const char* orsep = "";
                                              for (int s: v)
                                                {
                                                  if (s < 0)
780
781
782
                                                    solver.comment_rec(orsep,
                                                      "¬", d.fmt_ta(
                                                        q2, l, q1, -s - 1));
783
                                                  else
784
785
                                                    solver.comment_rec(orsep,
                                                        d.fmt_ta(q2, l, q1, s));
786
                                                  solver.comment_rec("FC");
787
788
                                                  orsep = " ∨ ";
                                                }
789
                                              solver.comment_rec(")\n");
790
#endif // DEBUG
791
                                              solver.add({-pid, -ti});
792
793
794
                                              for (int s: v)
                                                if (s < 0)
                                                  {
795
796
797
                                                    int tai =
                                                      d.transacc(q2, l, q1,
                                                          -s - 1);
798
                                                    assert(tai != 0);
799
                                                    solver.add(-tai);
800
801
802
                                                  }
                                                else
                                                  {
803
804
                                                    int tai =
                                                      d.transacc(q2, l, q1, s);
805
                                                    assert(tai != 0);
806
                                                    solver.add(tai);
807
                                                  }
808
                                              solver.add(0);
809
810
811
812
813
814
815
816
817
                                            }
                                        }
                                      // (13) augmenting paths (always).
                                      {
                                        size_t sf = d.all_cand_acc.size();
                                        for (size_t f = 0; f < sf; ++f)
                                          {
                                            acc_cond::mark_t f2 =
                                              d.cand_inf_trim
818
                                              (candhist_p |
819
820
821
                                               d.all_cand_acc[f]);
                                            acc_cond::mark_t f2p = 0U;
                                            if (!is_weak)
822
                                              f2p = d.ref_inf_trim(refhist |
823
                                                                   curacc);
824
825
                                            int p2id = d.pathid(
                                                q1, q1p, q3, dp, f2, f2p);
826
827
                                            if (pid == p2id)
                                              continue;
828
#if DEBUG
829
830
                                            solver.comment("(13) ", f_p, " ∧ ",
                                                 d.fmt_t(q1, l, q3), "δ ");
831
832
833
834
835
836

                                            auto biga_ = d.all_cand_acc[f];
                                            for (unsigned m = 0;
                                                 m < d.cand_nacc; ++m)
                                              {
                                                const char* not_ = "¬";
837
                                                if (biga_.has(m))
838
                                                  not_ = "";
839
                                                solver.comment_rec(" ∧ ", not_,
840
841
                                                    d.fmt_ta(q2, l, q3, m),
                                                    "FC");
842
                                              }
843
844
845
                                            solver.comment_rec(" → ",
                                                d.fmt_p(q1, q1p, q3, dp, f2,
                                                  f2p), '\n');
846
#endif
847
                                            solver.add({-pid, -ti});
848
849
850
851
                                            auto biga = d.all_cand_acc[f];
                                            for (unsigned m = 0;
                                                 m < d.cand_nacc; ++m)
                                              {
852
853
                                                int tai =
                                                  d.transacc(q2, l, q3, m);
854
855
                                                if (biga.has(m))
                                                  tai = -tai;
856
                                                solver.add(tai);
857
                                              }
858
                                            solver.add({p2id, 0});
859
860
861
862
863
864
865
866
867
                                          }
                                      }
                                    }
                                }
                            }
                        }
                  }
            }
        }
868
      return solver.stats();
869
870
    }

871
    static twa_graph_ptr
872
    sat_build(const satsolver::solution& solution, dict& satdict,
873
              const_twa_graph_ptr aut, bool state_based)
874
    {
875
876
      trace << "sat_build(..., state_based=" << state_based << ")\n";

877
      auto autdict = aut->get_dict();
878
      auto a = make_twa_graph(autdict);
879
      a->copy_ap_of(aut);
880
      if (state_based)
881
        a->prop_state_acc(true);
882
      a->prop_deterministic(true);
883
      a->set_acceptance(satdict.cand_nacc, satdict.cand_acc);
884
      a->new_states(satdict.cand_size);
885
886

#if DEBUG
887
      std::fstream out("dtwa-sat.dbg",
888
                       std::ios_base::trunc | std::ios_base::out);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
889
      out.exceptions(std::ifstream::failbit | std::ifstream::badbit);
890
#endif
891
      std::map<int, acc_cond::mark_t> state_acc;
892
      std::set<src_cond> seen_trans;
893

894
895
896
897
898
899
      unsigned alpha_size = satdict.alpha_vect.size();
      for (unsigned i = 0; i < satdict.cand_size; ++i)
        for (unsigned j = 0; j < alpha_size; ++j)
          for (unsigned k = 0; k < satdict.cand_size; ++k)
          {
            if (solution[satdict.transid(i, j, k) - 1])
900
            {
901
              // Ignore unuseful transitions because of reduced cand_size.
902
              if (i >= satdict.cand_size)
903
904
                continue;

905
              // Skip (s,l,d2) if we have already seen some (s,l,d1).
906
907
908
909
910
911
912
913
914
              if (seen_trans.insert(src_cond(i, satdict.alpha_vect[j])).second)
              {
                acc_cond::mark_t acc = 0U;
                if (state_based)
                  {
                    auto tmp = state_acc.find(i);
                    if (tmp != state_acc.end())
                      acc = tmp->second;
                  }
915

916
917
918
                for (unsigned n = 0; n < satdict.cand_nacc; ++n)
                  if (solution[satdict.transacc(i, j, k, n) - 1])
                    acc |= satdict.cacc.mark(n);
919

920
921
                a->new_edge(i, k, satdict.alpha_vect[j], acc);
              }
922
            }
923
          }
924

925
#if DEBUG
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
      dout << "--- transition variables ---\n";
      for (unsigned i = 0; i < satdict.cand_size; ++i)
        for (unsigned j = 0; j < alpha_size; ++j)
          for (unsigned k = 0; k < satdict.cand_size; ++k)
          {
            int var = satdict.transid(i, j, k);
            std::string f_t = satdict.fmt_t(i, j, k);
            if (solution[var - 1])
              dout << ' ' << var << "\t " << f_t << '\n';
            else
              dout << -var << "\t¬" << f_t << '\n';
          }
      dout << "--- transition_acc variables ---\n";
      if (state_based)
      {
        dout << "In state_based mode, there is only 1 litteral for each "
          "combination of src and nacc, regardless of dst or cond!\n";
        for (unsigned i = 0; i < satdict.cand_size; ++i)
          for (unsigned j = 0; j < satdict.cand_nacc; ++j)
          {
            int var = satdict.transacc(i, 0, 0, j);
            std::string f_ta = satdict.fmt_ta(i, 0, 0, j);
            if (solution[var - 1])
              dout << ' ' << var << "\t " << f_ta << '\n';
            else
              dout << -var << "\t¬" << f_ta << '\n';
          }
      }
      else
        for (unsigned i = 0; i < satdict.cand_size; ++i)
          for (unsigned j = 0; j < alpha_size; ++j)
            for (unsigned k = 0; k < satdict.cand_size; ++k)
              for (unsigned l = 0; l < satdict.cand_nacc; ++l)
              {
                int var = satdict.transacc(i, j, k, l);
                std::string f_ta = satdict.fmt_ta(i, j, k, l);
                if (solution[var - 1])
                  dout << ' ' << var << "\t " << f_ta << '\n';
                else
                  dout << -var << "\t¬" << f_ta << '\n';
              }
      dout << "--- path_map variables ---\n";
      for (auto it = satdict.path_map.begin(); it != satdict.path_map.end();
          ++it)
        for (unsigned k = 0; k < satdict.cand_size; ++k)
          for (unsigned l = 0; l < satdict.cand_size; ++l)
          {
            int var = satdict.pathid(it->second, k, l);
            std::string f_p = satdict.fmt_p(k, it->first.src_ref, l,
                it->first.dst_ref, it->first.acc_cand, it->first.acc_ref);
            if (solution[var - 1])
              dout << ' ' << var << "\t " << f_p << '\n';
            else
              dout << -var << "\t¬" << f_p << '\n';
          }
981
982
#endif

983
      a->merge_edges();
984
985
986
987
      return a;
    }
  }

988
  twa_graph_ptr
989
  dtwa_sat_synthetize(const const_twa_graph_ptr& a,
990
991
992
993
                      unsigned target_acc_number,
                      const acc_cond::acc_code& target_acc,
                      int target_state_number,
                      bool state_based, bool colored)
994
  {
995
    if (target_state_number == 0)
996
      return nullptr;
997
    trace << "dtwa_sat_synthetize(..., nacc = " << target_acc_number
998
999
1000
          << ", acc = \"" << target_acc
          << "\", states = " << target_state_number
          << ", state_based = " << state_based << ")\n";
1001

1002
1003
1004
    dict d(a);
    d.cand_size = target_state_number;
    d.cand_nacc = target_acc_number;
1005
    d.cand_acc = target_acc;
1006

1007
1008
    satsolver solver;
    satsolver::solution_pair solution;
1009

1010
1011
    timer_map t;
    t.start("encode");
1012
    dtwa_to_sat(solver, a, d, state_based, colored);
1013
1014
    t.stop("encode");
    t.start("solve");
1015
    solution = solver.get_solution();
1016
    t.stop("solve");
1017

1018
    twa_graph_ptr res = nullptr;
1019
1020
    if (!solution.second.empty())
      res = sat_build(solution.second, d, a, state_based);
1021

1022
    print_log(t, target_state_number, res, solver); // if SPOT_SATLOG is set.
1023

1024
    trace << "dtwa_sat_synthetize(...) = " << res << '\n';
1025
1026
1027
    return res;
  }

1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040

  namespace
  {
    // Chose a good reference automaton given two automata.
    //
    // The right automaton only is allowed to be null.  In that
    // case the left automaton is returned.
    //
    // The selection relies on the fact that the SAT encoding is
    // quadratic in the number of input states, and exponential in the
    // number of input sets.
    static const_twa_graph_ptr
    best_aut(const const_twa_graph_ptr& left,
1041
             const const_twa_graph_ptr& right)
1042
1043
    {
      if (right == nullptr)
1044
        return left;
1045
1046
1047
1048
1049
      auto lstates = left->num_states();
      auto lsets = left->num_sets();
      auto rstates = right->num_states();
      auto rsets = right->num_sets();
      if (lstates <= rstates && lsets <= rsets)
1050
        return left;
1051
      if (lstates >= rstates && lsets >= rsets)
1052
        return right;
1053
1054
1055
1056
1057
1058
1059
1060

      long long unsigned lw = (1ULL << lsets) * lstates * lstates;
      long long unsigned rw = (1ULL << rsets) * rstates * rstates;

      return lw <= rw ? left : right;
    }
  }

1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
  static twa_graph_ptr
  dichotomy_dtwa_research(int max,
                          dict& d,
                          satsolver& solver,
                          timer_map& t1,
                          const_twa_graph_ptr& prev,
                          bool state_based)
  {
    trace << "dichotomy_dtwa_research(...)\n";
    int min = 1;
    int target = 0;
    twa_graph_ptr res = nullptr;

    while (min < max)
    {
      target = (max + min) / 2;
      trace << "min:" << min << ", max:" << max << ", target:" << target
        << '\n';

      solver.assume(d.nvars + target);
      trace << "solver.assume(" << d.nvars + target << ")\n";

      satsolver::solution_pair solution = solver.get_solution();
      if (solution.second.empty())
      {
        trace << "UNSAT\n";
        max = target;
      }
      else
      {
        trace << "SAT\n";
        res = sat_build(solution.second, d, prev, state_based);
        min = d.cand_size - stats_reachable(res).states + 1;
      }
    }

    trace << "End with max:" << max << ", min:" << min << '\n';
    if (!res)
    {
      trace << "All assumptions are UNSAT, let's try without...";
      satsolver::solution_pair solution = solver.get_solution();
      trace << (solution.second.empty() ? "UNSAT!\n" : "SAT\n");
      res = solution.second.empty() ? nullptr :
        sat_build(solution.second, d, prev, state_based);
    }

    t1.stop("solve");
    print_log(t1, d.cand_size - target , res,