dtbasat.cc 20.5 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
#include "twa/bddprint.hh"
29
#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
    unsigned declare_vars(const const_twa_graph_ptr& aut,
218
219
220
221
			  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
    sat_stats dtba_to_sat(std::ostream& out,
298
			  const const_twa_graph_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 twa_graph_ptr
635
    sat_build(const satsolver::solution& solution, dict& satdict,
636
	      const_twa_graph_ptr aut, bool state_based)
637
    {
638
      auto autdict = aut->get_dict();
639
      auto a = make_twa_graph(autdict);
640
      a->copy_ap_of(aut);
641
      acc_cond::mark_t acc = a->set_buchi();
642
643
      if (state_based)
	a->prop_state_based_acc();
644
      a->new_states(satdict.cand_size);
645

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

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

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

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

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

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

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

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

754
755
    satsolver solver;
    satsolver::solution_pair solution;
756

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

765
    twa_graph_ptr res = nullptr;
766
767
    if (!solution.second.empty())
      res = sat_build(solution.second, d, a, state_based);
768

769
770
771
772
773
774
775
776
777
    // Always copy the environment variable into a static string,
    // so that we (1) look it up once, but (2) won't crash if the
    // environment is changed.
    static std::string log = []()
      {
	auto s = getenv("SPOT_SATLOG");
	return s ? s : "";
      }();
    if (!log.empty())
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
      {
	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';
      }
800
    static bool show = getenv("SPOT_SATSHOW");
801
802
803
    if (show && res)
      dotty_reachable(std::cout, res);

804
    trace << "dtba_sat_synthetize(...) = " << res << '\n';
805
806
807
    return res;
  }

808
809
  twa_graph_ptr
  dtba_sat_minimize(const const_twa_graph_ptr& a, bool state_based)
810
811
812
  {
    int n_states = stats_reachable(a).states;

813
    twa_graph_ptr prev = nullptr;
814
    for (;;)
815
      {
816
	auto next =
817
	  dtba_sat_synthetize(prev ? prev : a, --n_states, state_based);
818
	if (!next)
819
	  return prev;
820
821
	else
	  n_states = stats_reachable(next).states;
822
	prev = next;
823
      }
824
    SPOT_UNREACHABLE();
825
  }
826

827
828
  twa_graph_ptr
  dtba_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
829
			      bool state_based)
830
831
832
833
  {
    int max_states = stats_reachable(a).states - 1;
    int min_states = 1;

834
    twa_graph_ptr prev = nullptr;
835
    while (min_states <= max_states)
836
      {
837
	int target = (max_states + min_states) / 2;
838
	auto next = dtba_sat_synthetize(prev ? prev : a, target, state_based);
839
	if (!next)
840
	  {
841
842
843
844
845
	    min_states = target + 1;
	  }
	else
	  {
	    prev = next;
846
	    max_states = stats_reachable(next).states - 1;
847
848
	  }
      }
849
    return prev;
850
851
  }
}