dtbasat.cc 20.2 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
// de l'Epita.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

#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
306
307
      // Compute the AP used in the hard way.
      bdd ap = bddtrue;
      for (auto& t: ref->transitions())
	if (!ref->is_dead_transition(t))
	  ap &= bdd_support(t.cond);
308

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

321
322
323
324
      scc_info sm(ref);

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

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

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

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

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

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

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

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

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

	      ++nclauses;
	    }
	}

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

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

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

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

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

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

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

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

      // 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
447
      for (unsigned q1p = 0; q1p < ref_size; ++q1p)
448
	{
449
450
451
452
	  if (!sm.reachable_state(q1p))
	    continue;
	  unsigned q1p_scc = sm.scc_of(q1p);
	  if (sm.is_trivial(q1p_scc))
453
	    continue;
454
	  for (unsigned q2p = 0; q2p < ref_size; ++q2p)
455
	    {
456
457
	      if (!sm.reachable_state(q2p))
		continue;
458
459
	      // We are only interested in transition that can form a
	      // cycle, so they must belong to the same SCC.
460
	      if (sm.scc_of(q2p) != q1p_scc)
461
		continue;
462
463
	      for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
		for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
464
465
		  {
		    path p1(q1, q1p, q2, q2p);
466

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

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

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

483
			if (ra.accepting(tr.acc))
484
			  continue;
485
			for (unsigned q3 = 0; q3 < d.cand_size; ++q3)
486
487
			  {
			    if (dp == q1p && q3 == q1) // (4) looping
488
			      {
489
				bdd all = tr.cond;
490
				while (all != bddfalse)
491
				  {
492
493
494
495
496
497
498
499
500
				    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";
501
				    out << -pid1 << ' ' << -ti << ' '
502
503
504
					<< -ta << " 0\n";
				    ++nclauses;
				  }
505
506


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

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

516
				bdd all = tr.cond;
517
				while (all != bddfalse)
518
				  {
519
520
521
522
523
524
525
526
				    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";
527
				    out << -pid1 << ' ' << -ti << ' '
528
529
					<< pid2 << " 0\n";
				    ++nclauses;
530
531
532
533
				  }
			      }
			  }
		      }
534
		  }
535
536
	    }
	}
537
538
539
      // 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.
540
      for (unsigned q1p = 0; q1p < ref_size; ++q1p)
541
	{
542
	  if (!sm.reachable_state(q1p))
543
	    continue;
544
545
546
547
	  unsigned q1p_scc = sm.scc_of(q1p);
	  if (sm.is_trivial(q1p_scc))
	    continue;
	  for (unsigned q2p = 0; q2p < ref_size; ++q2p)
548
	    {
549
550
	      if (!sm.reachable_state(q2p))
		continue;
551
552
	      // We are only interested in transition that can form a
	      // cycle, so they must belong to the same SCC.
553
	      if (sm.scc_of(q2p) != q1p_scc)
554
		continue;
555
556
	      for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
		for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
557
558
559
		  {
		    path p1(q1, q1p, q2, q2p);
		    dout << "(6&7) matching paths from candidate based on "
560
			 << p1 << '\n';
561
562
563
564
565
566

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

568
		    for (auto& tr: ref->out(q2p))
569
		      {
570
			unsigned dp = tr.dst;
571
			// Skip destinations not in the SCC.
572
573
574
			if (sm.scc_of(dp) != q1p_scc)
			  continue;
			for (unsigned q3 = 0; q3 < d.cand_size; q3++)
575
576
577
578
579
			  {
			    if (dp == q1p && q3 == q1) // (6) looping
			      {
				// We only care about the looping case if
				// it is accepting in the reference.
580
				if (!ra.accepting(tr.acc))
581
				  continue;
582
				bdd all = tr.cond;
583
584
585
586
587
588
589
590
591
592
593
				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";
594
				    out << -pid1 << ' ' << -ti << ' ' << ta
595
596
597
598
599
600
601
602
603
604
605
606
					<< " 0\n";
				    ++nclauses;
				  }
			      }
			    else // (7) no loop
			      {
				path p2 = path(q1, q1p, q3, dp);
				int pid2 = d.pathid_cand[p2];

				if (pid1 == pid2)
				  continue;

607
				bdd all = tr.cond;
608
609
610
611
612
613
614
615
616
617
618
619
				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";

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

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

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

#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
651
      out.exceptions(std::ifstream::failbit | std::ifstream::badbit);
652
653
654
655
      std::set<int> positive;
#endif

      dout << "--- transition variables ---\n";
656
      std::set<int> acc_states;
657
      std::set<src_cond> seen_trans;
658
      for (int v: solution)
659
660
661
662
663
664
665
666
667
668
669
670
	{
	  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())
	    {
671
672
673
674
675
	      // 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.
676
677
678
679
		  bool accept = state_based
		    && acc_states.find(t->second.src) != acc_states.end();

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

		  dout << v << '\t' << t->second << \n";
685
		}
686
687
688
689
690
691
	    }
	  else
	    {
	      t = satdict.revtransacc.find(v);
	      if (t != satdict.revtransacc.end())
		{
692
		  dout << v << '\t' << t->second << "F\n";
693
		  if (last_sat_trans && t->second == *last_sat_trans)
694
695
696
697
		    {
		      assert(!state_based);
		      // This assumes that the SAT solvers output
		      // variables in increasing order.
698
		      a->trans_data(last_aut_trans).acc = acc;
699
700
701
702
703
704
705
706
707
708
		    }
		  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);
		    }
709
710
711
712
713
		}
	    }
	}
#if DEBUG
      dout << "--- state_pair variables ---\n";
714
715
716
      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
717
	else
718
	  dout << -pit.second << "\t¬" << pit.first << "C\n";
719
720

      dout << "--- pathid_cand variables ---\n";
721
722
723
      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
724
	else
725
	  dout << -pit.second << "\t¬" << pit.first << "C\n";
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
726

727
      dout << "--- pathid_ref variables ---\n";
728
729
730
      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
731
	else
732
	  dout << -pit.second << "\t¬" << pit.first << "C\n";
733
734
735
736
737
738
#endif
      a->merge_transitions();
      return a;
    }
  }

739
  tgba_digraph_ptr
740
741
  dtba_sat_synthetize(const const_tgba_digraph_ptr& a,
		      int target_state_number, bool state_based)
742
  {
743
    if (target_state_number == 0)
744
      return nullptr;
745
746
    trace << "dtba_sat_synthetize(..., states = " << target_state_number
	  << ", state_based = " << state_based << ")\n";
747
748
    dict d;
    d.cand_size = target_state_number;
749

750
751
    satsolver solver;
    satsolver::solution_pair solution;
752

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

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

765
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
    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);

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

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

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

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

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