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
      dout << state_pair(0, 0) << '\n';
      out << d.prodid[state_pair(0, 0)] << " 0\n";
400
401
402
403
404
      ++nclauses;

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

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

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

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

427
428
429
		      if (pit->second == succ)
			continue;

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

      bdd all_acc = ref->all_acceptance_conditions();

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

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

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

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

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


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

510
511
				if (pid1 == pid2)
				  continue;
512

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

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

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

				if (pid1 == pid2)
				  continue;

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

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

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

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

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

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

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

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

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

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

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

747
748
    satsolver solver;
    satsolver::solution_pair solution;
749

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

758
    tgba_digraph_ptr res = nullptr;
759
760
    if (!solution.second.empty())
      res = sat_build(solution.second, d, a, state_based);
761

762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
    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);

790
    trace << "dtba_sat_synthetize(...) = " << res << '\n';
791
792
793
    return res;
  }

794
  tgba_digraph_ptr
795
  dtba_sat_minimize(const const_tgba_digraph_ptr& a, bool state_based)
796
797
798
  {
    int n_states = stats_reachable(a).states;

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

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

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