dtbasat.cc 20.3 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2013, 2014, 2015 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/>.

#include <iostream>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
21
#include <fstream>
22
23
24
25
26
#include <sstream>
#include "dtbasat.hh"
#include "reachiter.hh"
#include <map>
#include <utility>
27
#include "sccinfo.hh"
28
29
#include "tgba/bddprint.hh"
#include "stats.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
30
#include "misc/satsolver.hh"
31
32
#include "misc/timer.hh"
#include "dotty.hh"
33

34
35
36
// 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.
37
//
38
39
40
41
// Additionally, if the following DEBUG macro is set to 1, the CNF
// file will be output with a comment before each clause, and an
// additional output file (dtba-sat.dbg) will be created with a list
// of all positive variables in the result and their meaning.
42
43
44
45

#define DEBUG 0
#if DEBUG
#define dout out << "c "
46
#define trace std::cerr
47
#else
48
49
#define dout while (0) std::cout
#define trace dout
50
51
52
53
54
55
#endif

namespace spot
{
  namespace
  {
56
    static bdd_dict_ptr debug_dict;
57
58
59

    struct transition
    {
60
      unsigned src;
61
      bdd cond;
62
      unsigned dst;
63

64
      transition(unsigned src, bdd cond, unsigned dst)
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
	: src(src), cond(cond), dst(dst)
      {
      }

      bool operator<(const transition& other) const
      {
	if (this->src < other.src)
	  return true;
	if (this->src > other.src)
	  return false;
	if (this->dst < other.dst)
	  return true;
	if (this->dst > other.dst)
	  return false;
	return this->cond.id() < other.cond.id();
      }

      bool operator==(const transition& other) const
      {
	return (this->src == other.src
		&& this->dst == other.dst
		&& this->cond.id() == other.cond.id());
      }
    };

90
91
    struct src_cond
    {
92
      unsigned src;
93
94
      bdd cond;

95
      src_cond(unsigned src, bdd cond)
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
	: src(src), cond(cond)
      {
      }

      bool operator<(const src_cond& other) const
      {
	if (this->src < other.src)
	  return true;
	if (this->src > other.src)
	  return false;
	return this->cond.id() < other.cond.id();
      }

      bool operator==(const src_cond& other) const
      {
	return (this->src == other.src
		&& this->cond.id() == other.cond.id());
      }
    };

116
117
    struct state_pair
    {
118
119
      unsigned a;
      unsigned b;
120

121
      state_pair(unsigned a, unsigned b)
122
123
124
125
126
127
128
129
130
131
132
133
134
135
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
	: a(a), b(b)
      {
      }

      bool operator<(const state_pair& other) const
      {
	if (this->a < other.a)
	  return true;
	if (this->a > other.a)
	  return false;
	if (this->b < other.b)
	  return true;
	if (this->b > other.b)
	  return false;
	return false;
      }
    };

    struct path
    {
      int src_cand;
      int src_ref;
      int dst_cand;
      int dst_ref;

      path(int src_cand, int src_ref,
	   int dst_cand, int dst_ref)
	: src_cand(src_cand), src_ref(src_ref),
	  dst_cand(dst_cand), dst_ref(dst_ref)
      {
      }

      bool operator<(const path& other) const
      {
	if (this->src_cand < other.src_cand)
	  return true;
	if (this->src_cand > other.src_cand)
	  return false;
	if (this->src_ref < other.src_ref)
	  return true;
	if (this->src_ref > other.src_ref)
	  return false;
	if (this->dst_cand < other.dst_cand)
	  return true;
	if (this->dst_cand > other.dst_cand)
	  return false;
	if (this->dst_ref < other.dst_ref)
	  return true;
	if (this->dst_ref > other.dst_ref)
	  return false;
	return false;
      }

    };

    std::ostream& operator<<(std::ostream& os, const state_pair& p)
    {
179
      os << '<' << p.a << ',' << p.b << '>';
180
181
182
183
184
      return os;
    }

    std::ostream& operator<<(std::ostream& os, const transition& t)
    {
185
      os << '<' << t.src << ','
186
	 << bdd_format_formula(debug_dict, t.cond)
187
	 << ',' << t.dst << '>';
188
189
190
191
192
      return os;
    }

    std::ostream& operator<<(std::ostream& os, const path& p)
    {
193
194
195
196
197
      os << '<'
	 << p.src_cand << ','
	 << p.src_ref << ','
	 << p.dst_cand << ','
	 << p.dst_ref << '>';
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
      return os;
    }

    struct dict
    {
      typedef std::map<transition, int> trans_map;
      trans_map transid;
      trans_map transacc;
      typedef std::map<int, transition> rev_map;
      rev_map revtransid;
      rev_map revtransacc;

      std::map<state_pair, int> prodid;
      std::map<path, int> pathid_ref;
      std::map<path, int> pathid_cand;
213
214
      int nvars = 0;
      unsigned cand_size;
215
216
    };

217
218
219
220
221
    unsigned declare_vars(const const_tgba_digraph_ptr& aut,
			  dict& d,
			  bdd ap,
			  bool state_based,
			  scc_info& sm)
222
    {
223
      unsigned ref_size = aut->num_states();
224

225
226
227
228
229
230
      if (d.cand_size == -1U)
	for (unsigned i = 0; i < ref_size; ++i)
	  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.
231

232
233
234
235
      for (unsigned i = 0; i < ref_size; ++i)
	{
	  if (!sm.reachable_state(i))
	    continue;
236

237
238
	  unsigned i_scc = sm.scc_of(i);
	  bool is_trivial = sm.is_trivial(i_scc);
239

240
241
242
	  for (unsigned j = 0; j < d.cand_size; ++j)
	    {
	      d.prodid[state_pair(j, i)] = ++d.nvars;
243

244
245
246
	      // skip trivial SCCs
	      if (is_trivial)
		continue;
247

248
249
250
251
252
253
254
	      for (unsigned k = 0; k < ref_size; ++k)
		{
		  if (!sm.reachable_state(k))
		    continue;
		  if (sm.scc_of(k) != i_scc)
		    continue;
		  for (unsigned l = 0; l < d.cand_size; ++l)
255
		    {
256
257
		      if (i == k && j == l)
			continue;
258
259
260
261
		      path p(j, i, l, k);
		      d.pathid_ref[p] = ++d.nvars;
		      d.pathid_cand[p] = ++d.nvars;
		    }
262
263
264
		}
	    }
	}
265

266
	for (unsigned i = 0; i < d.cand_size; ++i)
267
268
	  {
	    int transacc = -1;
269
	    if (state_based)
270
271
272
	      // All outgoing transitions use the same acceptance variable.
	      transacc = ++d.nvars;

273
	    for (unsigned j = 0; j < d.cand_size; ++j)
274
275
276
277
	      {
		bdd all = bddtrue;
		while (all != bddfalse)
		  {
278
		    bdd one = bdd_satoneset(all, ap, bddfalse);
279
280
281
282
		    all -= one;

		    transition t(i, one, j);
		    d.transid[t] = ++d.nvars;
283
		    d.revtransid.emplace(d.nvars, t);
284
		    int ta = d.transacc[t] =
285
		      state_based ? transacc : ++d.nvars;
286
		    d.revtransacc.emplace(ta, t);
287
288
289
		  }
	      }
	  }
290
291
292

	return ref_size;
    }
293

294
295
    typedef std::pair<int, int> sat_stats;

296
    static
297
298
    sat_stats dtba_to_sat(std::ostream& out,
			  const const_tgba_digraph_ptr& ref,
299
			  dict& d, bool state_based)
300
    {
301
      clause_counter nclauses;
302

303
304
305
      // Compute the AP used in the hard way.
      bdd ap = bddtrue;
      for (auto& t: ref->transitions())
306
	ap &= bdd_support(t.cond);
307

308
309
310
311
312
313
314
315
316
317
318
319
      // Count the number of atomic propositions
      int nap = 0;
      {
	bdd cur = ap;
	while (cur != bddtrue)
	  {
	    ++nap;
	    cur = bdd_high(cur);
	  }
	nap = 1 << nap;
      }

320
321
322
323
      scc_info sm(ref);

      // Number all the SAT variables we may need.
      unsigned ref_size = declare_vars(ref, d, ap, state_based, sm);
324
325
326
327
328

      // empty automaton is impossible
      if (d.cand_size == 0)
	{
	  out << "p cnf 1 2\n-1 0\n1 0\n";
329
	  return std::make_pair(1, 2);
330
331
332
333
334
335
336
	}

      // An empty line for the header
      out << "                                                 \n";

#if DEBUG
      debug_dict = ref->get_dict();
337
338
      dout << "ref_size: " << ref_size << '\n';
      dout << "cand_size: " << d.cand_size << '\n';
339
340
#endif

341
      dout << "symmetry-breaking clauses\n";
342
      unsigned j = 0;
343
344
345
346
347
      bdd all = bddtrue;
      while (all != bddfalse)
 	{
 	  bdd s = bdd_satoneset(all, ap, bddfalse);
 	  all -= s;
348
349
	  for (unsigned i = 0; i < d.cand_size - 1; ++i)
	    for (unsigned k = i * nap + j + 2; k < d.cand_size; ++k)
350
351
352
	      {
		transition t(i, s, k);
		int ti = d.transid[t];
353
		dout << "¬" << t << '\n';
354
355
356
357
358
		out << -ti << " 0\n";
		++nclauses;
	      }
 	  ++j;
 	}
359
      if (!nclauses.nb_clauses())
360
 	dout << "(none)\n";
361

362
      dout << "(1) the candidate automaton is complete\n";
363
      for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
364
365
366
367
368
369
370
371
372
	{
	  bdd all = bddtrue;
	  while (all != bddfalse)
	    {
	      bdd s = bdd_satoneset(all, ap, bddfalse);
	      all -= s;

#if DEBUG
	      dout;
373
	      for (unsigned q2 = 0; q2 < d.cand_size; q2++)
374
375
376
377
378
379
		{
		  transition t(q1, s, q2);
		  out << t << "δ";
		  if (q2 != d.cand_size)
		    out << " ∨ ";
		}
380
	      out << '\n';
381
382
#endif

383
	      for (unsigned q2 = 0; q2 < d.cand_size; q2++)
384
385
386
387
		{
		  transition t(q1, s, q2);
		  int ti = d.transid[t];

388
		  out << ti << ' ';
389
390
391
392
393
394
395
396
		}
	      out << "0\n";

	      ++nclauses;
	    }
	}

      dout << "(2) the initial state is reachable\n";
397
398
399
400
401
402
      {
	unsigned init = ref->get_init_state_number();
	dout << state_pair(0, init) << '\n';
	out << d.prodid[state_pair(0, init)] << " 0\n";
	++nclauses;
      }
403
404
405
406

      for (std::map<state_pair, int>::const_iterator pit = d.prodid.begin();
	   pit != d.prodid.end(); ++pit)
	{
407
408
	  unsigned q1 = pit->first.a;
	  unsigned q1p = pit->first.b;
409
410
411

	  dout << "(3) augmenting paths based on Cand[" << q1
	       << "] and Ref[" << q1p << "]\n";
412
	  for (auto& tr: ref->out(q1p))
413
	    {
414
415
	      unsigned dp = tr.dst;
	      bdd all = tr.cond;
416
417
418
419
420
	      while (all != bddfalse)
		{
		  bdd s = bdd_satoneset(all, ap, bddfalse);
		  all -= s;

421
		  for (unsigned q2 = 0; q2 < d.cand_size; q2++)
422
423
424
425
426
427
428
		    {
		      transition t(q1, s, q2);
		      int ti = d.transid[t];

		      state_pair p2(q2, dp);
		      int succ = d.prodid[p2];

429
430
431
		      if (pit->second == succ)
			continue;

432
433
		      dout << pit->first << " ∧ " << t << "δ → " << p2 << '\n';
		      out << -pit->second << ' ' << -ti << ' '
434
435
436
437
438
439
440
			  << succ << " 0\n";
		      ++nclauses;
		    }
		}
	    }
	}

441
      const acc_cond& ra = ref->acc();
442
443
444
445

      // construction of contraints (4,5) : all loops in the product
      // where no accepting run is detected in the ref. automaton,
      // must also be marked as not accepting in the cand. automaton
446
      for (unsigned q1p = 0; q1p < ref_size; ++q1p)
447
	{
448
449
450
451
	  if (!sm.reachable_state(q1p))
	    continue;
	  unsigned q1p_scc = sm.scc_of(q1p);
	  if (sm.is_trivial(q1p_scc))
452
	    continue;
453
	  for (unsigned q2p = 0; q2p < ref_size; ++q2p)
454
	    {
455
456
	      if (!sm.reachable_state(q2p))
		continue;
457
458
	      // We are only interested in transition that can form a
	      // cycle, so they must belong to the same SCC.
459
	      if (sm.scc_of(q2p) != q1p_scc)
460
		continue;
461
462
	      for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
		for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
463
464
		  {
		    path p1(q1, q1p, q2, q2p);
465

466
		    dout << "(4&5) matching paths from reference based on "
467
			 << p1 << '\n';
468

469
470
471
472
473
		    int pid1;
		    if (q1 == q2 && q1p == q2p)
		      pid1 = d.prodid[state_pair(q1, q1p)];
		    else
		      pid1 = d.pathid_ref[p1];
474

475
		    for (auto& tr: ref->out(q2p))
476
		      {
477
			unsigned dp = tr.dst;
478
			// Skip destinations not in the SCC.
479
480
			if (sm.scc_of(dp) != q1p_scc)
			  continue;
481

482
			if (ra.accepting(tr.acc))
483
			  continue;
484
			for (unsigned q3 = 0; q3 < d.cand_size; ++q3)
485
486
			  {
			    if (dp == q1p && q3 == q1) // (4) looping
487
			      {
488
				bdd all = tr.cond;
489
				while (all != bddfalse)
490
				  {
491
492
493
494
495
496
497
498
499
				    bdd s = bdd_satoneset(all, ap, bddfalse);
				    all -= s;

				    transition t(q2, s, q1);
				    int ti = d.transid[t];
				    int ta = d.transacc[t];

				    dout << p1 << "R ∧ " << t << "δ → ¬" << t
					 << "F\n";
500
				    out << -pid1 << ' ' << -ti << ' '
501
502
503
					<< -ta << " 0\n";
				    ++nclauses;
				  }
504
505


506
507
508
509
510
			      }
			    else // (5) not looping
			      {
				path p2 = path(q1, q1p, q3, dp);
				int pid2 = d.pathid_ref[p2];
511

512
513
				if (pid1 == pid2)
				  continue;
514

515
				bdd all = tr.cond;
516
				while (all != bddfalse)
517
				  {
518
519
520
521
522
523
524
525
				    bdd s = bdd_satoneset(all, ap, bddfalse);
				    all -= s;

				    transition t(q2, s, q3);
				    int ti = d.transid[t];

				    dout << p1 << "R ∧ " << t << "δ → " << p2
					 << "R\n";
526
				    out << -pid1 << ' ' << -ti << ' '
527
528
					<< pid2 << " 0\n";
				    ++nclauses;
529
530
531
532
				  }
			      }
			  }
		      }
533
		  }
534
535
	    }
	}
536
537
538
      // construction of contraints (6,7): all loops in the product
      // where accepting run is detected in the ref. automaton, must
      // also be marked as accepting in the candidate.
539
      for (unsigned q1p = 0; q1p < ref_size; ++q1p)
540
	{
541
	  if (!sm.reachable_state(q1p))
542
	    continue;
543
544
545
546
	  unsigned q1p_scc = sm.scc_of(q1p);
	  if (sm.is_trivial(q1p_scc))
	    continue;
	  for (unsigned q2p = 0; q2p < ref_size; ++q2p)
547
	    {
548
549
	      if (!sm.reachable_state(q2p))
		continue;
550
551
	      // We are only interested in transition that can form a
	      // cycle, so they must belong to the same SCC.
552
	      if (sm.scc_of(q2p) != q1p_scc)
553
		continue;
554
555
	      for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
		for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
556
557
558
		  {
		    path p1(q1, q1p, q2, q2p);
		    dout << "(6&7) matching paths from candidate based on "
559
			 << p1 << '\n';
560
561
562
563
564
565

		    int pid1;
		    if (q1 == q2 && q1p == q2p)
		      pid1 = d.prodid[state_pair(q1, q1p)];
		    else
		      pid1 = d.pathid_cand[p1];
566

567
		    for (auto& tr: ref->out(q2p))
568
		      {
569
			unsigned dp = tr.dst;
570
			// Skip destinations not in the SCC.
571
572
573
			if (sm.scc_of(dp) != q1p_scc)
			  continue;
			for (unsigned q3 = 0; q3 < d.cand_size; q3++)
574
575
576
577
578
			  {
			    if (dp == q1p && q3 == q1) // (6) looping
			      {
				// We only care about the looping case if
				// it is accepting in the reference.
579
				if (!ra.accepting(tr.acc))
580
				  continue;
581
				bdd all = tr.cond;
582
583
584
585
586
587
588
589
590
591
592
				while (all != bddfalse)
				  {
				    bdd s = bdd_satoneset(all, ap, bddfalse);
				    all -= s;

				    transition t(q2, s, q1);
				    int ti = d.transid[t];
				    int ta = d.transacc[t];

				    dout << p1 << "C ∧ " << t << "δ → " << t
					 << "F\n";
593
				    out << -pid1 << ' ' << -ti << ' ' << ta
594
595
596
597
598
599
600
601
602
603
604
605
					<< " 0\n";
				    ++nclauses;
				  }
			      }
			    else // (7) no loop
			      {
				path p2 = path(q1, q1p, q3, dp);
				int pid2 = d.pathid_cand[p2];

				if (pid1 == pid2)
				  continue;

606
				bdd all = tr.cond;
607
608
609
610
611
612
613
614
615
616
617
618
				while (all != bddfalse)
				  {
				    bdd s = bdd_satoneset(all, ap, bddfalse);
				    all -= s;

				    transition t(q2, s, q3);
				    int ti = d.transid[t];
				    int ta = d.transacc[t];

				    dout << p1 << "C ∧ " << t << "δ ∧ ¬"
					 << t << "F → " << p2 << "C\n";

619
620
				    out << -pid1 << ' ' << -ti << ' '
					<< ta << ' ' << pid2 << " 0\n";
621
622
623
624
625
626
627
628
				    ++nclauses;
				  }
			      }
			  }
		      }
		  }
	    }
	}
629
      out.seekp(0);
630
      out << "p cnf " << d.nvars << ' ' << nclauses.nb_clauses();
631
      return std::make_pair(d.nvars, nclauses.nb_clauses());
632
633
    }

634
    static tgba_digraph_ptr
635
    sat_build(const satsolver::solution& solution, dict& satdict,
636
	      const_tgba_digraph_ptr aut, bool state_based)
637
    {
638
      auto autdict = aut->get_dict();
639
      auto a = make_tgba_digraph(autdict);
640
      a->copy_ap_of(aut);
641
      acc_cond::mark_t acc = a->set_single_acceptance_set();
642
      a->new_states(satdict.cand_size);
643

644
645
      unsigned last_aut_trans = -1U;
      const transition* last_sat_trans = nullptr;
646
647
648
649

#if DEBUG
      std::fstream out("dtba-sat.dbg",
		       std::ios_base::trunc | std::ios_base::out);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
650
      out.exceptions(std::ifstream::failbit | std::ifstream::badbit);
651
652
653
654
      std::set<int> positive;
#endif

      dout << "--- transition variables ---\n";
655
      std::set<int> acc_states;
656
      std::set<src_cond> seen_trans;
657
      for (int v: solution)
658
659
660
661
662
663
664
665
666
667
668
669
	{
	  if (v < 0)  // FIXME: maybe we can have (v < NNN)?
	    continue;

#if DEBUG
	  positive.insert(v);
#endif

	  dict::rev_map::const_iterator t = satdict.revtransid.find(v);

	  if (t != satdict.revtransid.end())
	    {
670
671
672
673
674
	      // Skip (s,l,d2) if we have already seen some (s,l,d1).
	      if (seen_trans.insert(src_cond(t->second.src,
					     t->second.cond)).second)
		{
		  // Mark the transition as accepting if the source is.
675
676
677
678
		  bool accept = state_based
		    && acc_states.find(t->second.src) != acc_states.end();

		  last_aut_trans =
679
		    a->new_acc_transition(t->second.src, t->second.dst,
680
					  t->second.cond, accept);
681
682
683
		  last_sat_trans = &t->second;

		  dout << v << '\t' << t->second << \n";
684
		}
685
686
687
688
689
690
	    }
	  else
	    {
	      t = satdict.revtransacc.find(v);
	      if (t != satdict.revtransacc.end())
		{
691
		  dout << v << '\t' << t->second << "F\n";
692
		  if (last_sat_trans && t->second == *last_sat_trans)
693
694
695
696
		    {
		      assert(!state_based);
		      // This assumes that the SAT solvers output
		      // variables in increasing order.
697
		      a->trans_data(last_aut_trans).acc = acc;
698
699
700
701
702
703
704
705
706
707
		    }
		  else if (state_based)
		    {
		      // Accepting translations actually correspond to
		      // states and are announced before listing
		      // outgoing transitions.  Again, this assumes
		      // that the SAT solvers output variables in
		      // increasing order.
		      acc_states.insert(t->second.src);
		    }
708
709
710
711
712
		}
	    }
	}
#if DEBUG
      dout << "--- state_pair variables ---\n";
713
714
715
      for (auto pit: satdict.prodid)
	if (positive.find(pit.second) != positive.end())
	  dout << pit.second << '\t' << pit.first << "C\n";
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
716
	else
717
	  dout << -pit.second << "\t¬" << pit.first << "C\n";
718
719

      dout << "--- pathid_cand variables ---\n";
720
721
722
      for (auto pit: satdict.pathid_cand)
	if (positive.find(pit.second) != positive.end())
	  dout << pit.second << '\t' << pit.first << "C\n";
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
723
	else
724
	  dout << -pit.second << "\t¬" << pit.first << "C\n";
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
725

726
      dout << "--- pathid_ref variables ---\n";
727
728
729
      for (auto pit: satdict.pathid_ref)
	if (positive.find(pit.second) != positive.end())
	  dout << pit.second << '\t' << pit.first << "R\n";
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
730
	else
731
	  dout << -pit.second << "\t¬" << pit.first << "C\n";
732
733
734
735
736
737
#endif
      a->merge_transitions();
      return a;
    }
  }

738
  tgba_digraph_ptr
739
740
  dtba_sat_synthetize(const const_tgba_digraph_ptr& a,
		      int target_state_number, bool state_based)
741
  {
742
743
744
    if (!a->acc().is_buchi())
      throw std::runtime_error
	("dtba_sat() can only work with Büchi acceptance");
745
    if (target_state_number == 0)
746
      return nullptr;
747
748
    trace << "dtba_sat_synthetize(..., states = " << target_state_number
	  << ", state_based = " << state_based << ")\n";
749
750
    dict d;
    d.cand_size = target_state_number;
751

752
753
    satsolver solver;
    satsolver::solution_pair solution;
754

755
756
757
758
759
    timer_map t;
    t.start("encode");
    sat_stats s = dtba_to_sat(solver(), a, d, state_based);
    t.stop("encode");
    t.start("solve");
760
    solution = solver.get_solution();
761
    t.stop("solve");
762

763
    tgba_digraph_ptr res = nullptr;
764
765
    if (!solution.second.empty())
      res = sat_build(solution.second, d, a, state_based);
766

767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
    static const char* log = getenv("SPOT_SATLOG");
    if (log)
      {
	std::fstream out(log,
			 std::ios_base::app | std::ios_base::out);
	out.exceptions(std::ifstream::failbit | std::ifstream::badbit);
	const timer& te = t.timer("encode");
	const timer& ts = t.timer("solve");
	out << target_state_number << ',';
	if (res)
	  {
	    tgba_sub_statistics st = sub_stats_reachable(res);
	    out << st.states << ',' << st.transitions
		<< ',' << st.sub_transitions;
	  }
	else
	  {
	    out << ",,";
	  }
	out << ','
	    << s.first << ',' << s.second << ','
	    << te.utime() << ',' << te.stime() << ','
	    << ts.utime() << ',' << ts.stime() << '\n';
      }
    static const char* show = getenv("SPOT_SATSHOW");
    if (show && res)
      dotty_reachable(std::cout, res);

795
    trace << "dtba_sat_synthetize(...) = " << res << '\n';
796
797
798
    return res;
  }

799
  tgba_digraph_ptr
800
  dtba_sat_minimize(const const_tgba_digraph_ptr& a, bool state_based)
801
802
803
  {
    int n_states = stats_reachable(a).states;

804
    tgba_digraph_ptr prev = nullptr;
805
    for (;;)
806
      {
807
	auto next =
808
	  dtba_sat_synthetize(prev ? prev : a, --n_states, state_based);
809
	if (!next)
810
	  return prev;
811
812
	else
	  n_states = stats_reachable(next).states;
813
	prev = next;
814
      }
815
    SPOT_UNREACHABLE();
816
  }
817

818
  tgba_digraph_ptr
819
820
  dtba_sat_minimize_dichotomy(const const_tgba_digraph_ptr& a,
			      bool state_based)
821
822
823
824
  {
    int max_states = stats_reachable(a).states - 1;
    int min_states = 1;

825
    tgba_digraph_ptr prev = nullptr;
826
    while (min_states <= max_states)
827
      {
828
	int target = (max_states + min_states) / 2;
829
	auto next = dtba_sat_synthetize(prev ? prev : a, target, state_based);
830
	if (!next)
831
	  {
832
833
834
835
836
	    min_states = target + 1;
	  }
	else
	  {
	    prev = next;
837
	    max_states = stats_reachable(next).states - 1;
838
839
	  }
      }
840
    return prev;
841
842
  }
}