dtgbasat.cc 24.1 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 "dtgbasat.hh"
#include "reachiter.hh"
#include <map>
#include <utility>
27
#include "sccinfo.hh"
28
29
30
31
#include "tgba/bddprint.hh"
#include "ltlast/constant.hh"
#include "stats.hh"
#include "ltlenv/defaultenv.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
32
#include "misc/satsolver.hh"
33
#include "misc/timer.hh"
34
#include "isweakscc.hh"
35
#include "dotty.hh"
36

37
38
39
// 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.
40
//
41
42
43
44
// 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 (dtgba-sat.dbg) will be created with a list
// of all positive variables in the result and their meaning.
45
46
47
48

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

namespace spot
{
  namespace
  {
59
    static bdd_dict_ptr debug_dict = 0;
60
61
    static const acc_cond* debug_ref_acc = 0;
    static const acc_cond* debug_cand_acc = 0;
62
63
64

    struct transition
    {
65
      unsigned src;
66
      bdd cond;
67
      unsigned dst;
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94

      transition(int src, bdd cond, int dst)
	: 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());
      }
    };

95
96
    struct src_cond
    {
97
      unsigned src;
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
      bdd cond;

      src_cond(int src, bdd cond)
	: 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());
      }
    };

121
122
    struct transition_acc
    {
123
      unsigned src;
124
      bdd cond;
125
      acc_cond::mark_t acc;
126
      unsigned dst;
127

128
      transition_acc(int src, bdd cond, acc_cond::mark_t acc, int dst)
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
	: src(src), cond(cond), acc(acc), dst(dst)
      {
      }

      bool operator<(const transition_acc& 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;
	if (this->cond.id() < other.cond.id())
	  return true;
	if (this->cond.id() > other.cond.id())
	  return false;
147
	return this->acc < other.acc;
148
149
150
151
152
153
154
      }

      bool operator==(const transition_acc& other) const
      {
	return (this->src == other.src
		&& this->dst == other.dst
		&& this->cond.id() == other.cond.id()
155
		&& this->acc == other.acc);
156
157
158
159
160
      }
    };

    struct path
    {
161
162
163
164
      unsigned src_cand;
      unsigned src_ref;
      unsigned dst_cand;
      unsigned dst_ref;
165
166
      acc_cond::mark_t acc_cand;
      acc_cond::mark_t acc_ref;
167

168
      path(unsigned src_cand, unsigned src_ref)
169
170
	: src_cand(src_cand), src_ref(src_ref),
	  dst_cand(src_cand), dst_ref(src_ref),
171
	  acc_cand(0U), acc_ref(0U)
172
173
174
      {
      }

175
176
      path(unsigned src_cand, unsigned src_ref,
	   unsigned dst_cand, unsigned dst_ref,
177
	   acc_cond::mark_t acc_cand, acc_cond::mark_t acc_ref)
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
	: src_cand(src_cand), src_ref(src_ref),
	  dst_cand(dst_cand), dst_ref(dst_ref),
	  acc_cand(acc_cand), acc_ref(acc_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;
202
	if (this->acc_ref < other.acc_ref)
203
	  return true;
204
	if (this->acc_ref > other.acc_ref)
205
	  return false;
206
	if (this->acc_cand < other.acc_cand)
207
	  return true;
208
	if (this->acc_cand > other.acc_cand)
209
210
211
212
213
214
215
216
217
	  return false;

	return false;
      }

    };

    std::ostream& operator<<(std::ostream& os, const transition& t)
    {
218
      os << '<' << t.src << ','
219
	 << bdd_format_formula(debug_dict, t.cond)
220
	 << ',' << t.dst << '>';
221
222
223
224
225
226
      return os;
    }


    std::ostream& operator<<(std::ostream& os, const transition_acc& t)
    {
227
228
      os << '<' << t.src << ','
	 << bdd_format_formula(debug_dict, t.cond) << ','
229
	 << debug_cand_acc->format(t.acc)
230
	 << ',' << t.dst << '>';
231
232
233
234
235
      return os;
    }

    std::ostream& operator<<(std::ostream& os, const path& p)
    {
236
237
238
239
      os << '<'
	 << p.src_cand << ','
	 << p.src_ref << ','
	 << p.dst_cand << ','
240
	 << p.dst_ref << ", "
241
242
	 << debug_cand_acc->format(p.acc_cand) << ", "
	 << debug_ref_acc->format(p.acc_ref) << '>';
243
244
245
246
247
      return os;
    }

    struct dict
    {
248
      dict(const const_tgba_ptr& a)
249
	: aut(a)
250
251
252
      {
      }

253
      const_tgba_ptr aut;
254
255
256
257
258
259
260
261
262
263
      typedef std::map<transition, int> trans_map;
      typedef std::map<transition_acc, int> trans_acc_map;
      trans_map transid;
      trans_acc_map transaccid;
      typedef std::map<int, transition> rev_map;
      typedef std::map<int, transition_acc> rev_acc_map;
      rev_map revtransid;
      rev_acc_map revtransaccid;

      std::map<path, int> pathid;
264
265
266
267
268
269
270
      int nvars = 0;
      //typedef std::unordered_map<const state*, int,
      //state_ptr_hash, state_ptr_equal> state_map;
      //typedef std::unordered_map<int, const state*> int_map;
      //state_map state_to_int;
      //      int_map int_to_state;
      unsigned cand_size;
271
      unsigned int cand_nacc;
272
      std::vector<acc_cond::mark_t> cand_acc; // size cand_nacc
273

274
275
      std::vector<acc_cond::mark_t> all_cand_acc;
      std::vector<acc_cond::mark_t> all_ref_acc;
276

277
278
      std::vector<bool> is_weak_scc;

279
280
      acc_cond cacc;

281
282
283
284
285
286
287
      ~dict()
      {
	aut->get_dict()->unregister_all_my_variables(this);
      }
    };


288
289
    unsigned declare_vars(const const_tgba_digraph_ptr& aut,
			  dict& d, bdd ap, bool state_based, scc_info& sm)
290
    {
291
292
      bdd_dict_ptr bd = aut->get_dict();
      d.cand_acc.resize(d.cand_nacc);
293
294
      d.cacc.add_sets(d.cand_nacc);
      d.all_cand_acc.push_back(0U);
295
296
      for (unsigned n = 0; n < d.cand_nacc; ++n)
	{
297
	  auto c = d.cacc.mark(n);
298
299
300
301
302
	  d.cand_acc[n] = c;
	  size_t s = d.all_cand_acc.size();
	  for (size_t i = 0; i < s; ++i)
	    d.all_cand_acc.push_back(d.all_cand_acc[i] | c);
	}
303
304


305
306
307
      d.all_ref_acc.push_back(0U);
      unsigned ref_nacc = aut->acc().num_sets();
      for (unsigned n = 0; n < ref_nacc; ++n)
308
	{
309
	  auto c = aut->acc().mark(n);
310
311
312
313
	  size_t s = d.all_ref_acc.size();
	  for (size_t i = 0; i < s; ++i)
	    d.all_ref_acc.push_back(d.all_ref_acc[i] | c);
	}
314

315
      unsigned ref_size = aut->num_states();
316

317
318
319
320
321
322
      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.
323

324
325
326
327
328
329
      for (unsigned i = 0; i < ref_size; ++i)
	{
	  if (!sm.reachable_state(i))
	    continue;
	  unsigned i_scc = sm.scc_of(i);
	  bool is_weak = d.is_weak_scc[i_scc];
330

331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
	  for (unsigned j = 0; j < d.cand_size; ++j)
	    {
	      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)
		    {
		      size_t sfp = is_weak ? 1 : d.all_ref_acc.size();
		      for (size_t fp = 0; fp < sfp; ++fp)
			{
			  size_t sf = d.all_cand_acc.size();
			  for (size_t f = 0; f < sf; ++f)
			    {
			      path p(j, i, l, k,
				     d.all_cand_acc[f],
				     d.all_ref_acc[fp]);
			      d.pathid[p] = ++d.nvars;
			    }
352

353
354
355
356
357
			}
		    }
		}
	    }
	}
358

359
360
361
362
      if (!state_based)
	{
	  for (unsigned i = 0; i < d.cand_size; ++i)
	    for (unsigned j = 0; j < d.cand_size; ++j)
363
	      {
364
365
		bdd all = bddtrue;
		while (all != bddfalse)
366
		  {
367
368
369
370
371
372
373
374
375
376
377
		    bdd one = bdd_satoneset(all, ap, bddfalse);
		    all -= one;

		    transition t(i, one, j);
		    d.transid[t] = ++d.nvars;
		    d.revtransid.emplace(d.nvars, t);

		    // Create the variable for the accepting transition
		    // immediately afterwards.  It helps parsing the
		    // result.
		    for (unsigned n = 0; n < d.cand_nacc; ++n)
378
		      {
379
380
381
			transition_acc ta(i, one, d.cand_acc[n], j);
			d.transaccid[ta] = ++d.nvars;
			d.revtransaccid.emplace(d.nvars, ta);
382
383
		      }
		  }
384
	      }
385
386
387
388
389
390
391
392
393
394
395
396
397
398
	}
      else // state based
	{
	  for (unsigned i = 0; i < d.cand_size; ++i)
	    for (unsigned n = 0; n < d.cand_nacc; ++n)
	      {
		++d.nvars;
		for (unsigned j = 1; j < d.cand_size; ++j)
		  {
		    bdd all = bddtrue;
		    while (all != bddfalse)
		      {
			bdd one = bdd_satoneset(all, ap, bddfalse);
			all -= one;
399

400
401
402
403
404
405
406
407
408
409
410
411
412
413
			transition_acc ta(i, one, d.cand_acc[n], j);
			d.transaccid[ta] = d.nvars;
			d.revtransaccid.emplace(d.nvars, ta);
		      }
		  }
	      }
	  for (unsigned i = 0; i < d.cand_size; ++i)
	    for (unsigned j = 0; j < d.cand_size; ++j)
	      {
		bdd all = bddtrue;
		while (all != bddfalse)
		  {
		    bdd one = bdd_satoneset(all, ap, bddfalse);
		    all -= one;
414

415
416
417
418
419
420
421
422
		    transition t(i, one, j);
		    d.transid[t] = ++d.nvars;
		    d.revtransid.emplace(d.nvars, t);
		  }
	      }
	}
      return ref_size;
    }
423

424
425
    typedef std::pair<int, int> sat_stats;

426
    static
427
    sat_stats dtgba_to_sat(std::ostream& out, const_tgba_digraph_ptr ref,
428
			   dict& d, bool state_based)
429
    {
430
      clause_counter nclauses;
431

432
433
434
      // Compute the AP used in the hard way.
      bdd ap = bddtrue;
      for (auto& t: ref->transitions())
435
	ap &= bdd_support(t.cond);
436

437
438
439
440
441
442
443
444
445
446
447
      // Count the number of atomic propositions
      int nap = 0;
      {
	bdd cur = ap;
	while (cur != bddtrue)
	  {
	    ++nap;
	    cur = bdd_high(cur);
	  }
	nap = 1 << nap;
      }
448

449
450
451
452
453
      scc_info sm(ref);
      d.is_weak_scc = sm.weak_sccs();

      // Number all the SAT variables we may need.
      unsigned ref_size = declare_vars(ref, d, ap, state_based, sm);
454
455
456
457
458

      // empty automaton is impossible
      if (d.cand_size == 0)
	{
	  out << "p cnf 1 2\n-1 0\n1 0\n";
459
	  return std::make_pair(1, 2);
460
461
462
463
464
	}

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

465
466
#if DEBUG
      debug_dict = ref->get_dict();
467
468
      debug_ref_acc = &ref->acc();
      debug_cand_acc = &d.cacc;
469
470
      dout << "ref_size: " << ref_size << '\n';
      dout << "cand_size: " << d.cand_size << '\n';
471
#endif
472
      auto& racc = ref->acc();
473
474
475
476
477
478
479
480

      dout << "symmetry-breaking clauses\n";
      int j = 0;
      bdd all = bddtrue;
      while (all != bddfalse)
 	{
 	  bdd s = bdd_satoneset(all, ap, bddfalse);
 	  all -= s;
481
482
 	  for (unsigned i = 0; i < d.cand_size - 1; ++i)
 	    for (unsigned k = i * nap + j + 2; k < d.cand_size; ++k)
483
484
485
	      {
		transition t(i, s, k);
		int ti = d.transid[t];
486
		dout << "¬" << t << '\n';
487
488
489
490
491
		out << -ti << " 0\n";
		++nclauses;
	      }
 	  ++j;
 	}
492
      if (!nclauses.nb_clauses())
493
494
 	dout << "(none)\n";

495
      dout << "(8) the candidate automaton is complete\n";
496
      for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
497
498
499
500
501
502
503
504
505
	{
	  bdd all = bddtrue;
	  while (all != bddfalse)
	    {
	      bdd s = bdd_satoneset(all, ap, bddfalse);
	      all -= s;

#if DEBUG
	      dout;
506
	      for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
507
508
509
510
511
512
		{
		  transition t(q1, s, q2);
		  out << t << "δ";
		  if (q2 != d.cand_size)
		    out << " ∨ ";
		}
513
	      out << '\n';
514
515
#endif

516
	      for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
517
518
519
520
		{
		  transition t(q1, s, q2);
		  int ti = d.transid[t];

521
		  out << ti << ' ';
522
523
524
525
526
527
528
		}
	      out << "0\n";
	      ++nclauses;
	    }
	}

      dout << "(9) the initial state is reachable\n";
529
530
531
532
533
534
      {
	unsigned init = ref->get_init_state_number();
	dout << path(0, init) << '\n';
	out << d.pathid[path(0, init)] << " 0\n";
	++nclauses;
      }
535

536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
      for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
	for (unsigned q1p = 0; q1p < ref_size; ++q1p)
	  {
	    if (!sm.reachable_state(q1p))
	      continue;
	    dout << "(10) augmenting paths based on Cand[" << q1
		 << "] and Ref[" << q1p << "]\n";
	    path p1(q1, q1p);
	    int p1id = d.pathid[p1];

	    for (auto& tr: ref->out(q1p))
	      {
		unsigned dp = tr.dst;
		bdd all = tr.cond;
		while (all != bddfalse)
		  {
		    bdd s = bdd_satoneset(all, ap, bddfalse);
		    all -= s;
554

555
556
557
558
		    for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
		      {
			transition t(q1, s, q2);
			int ti = d.transid[t];
559

560
561
			path p2(q2, dp);
			int succ = d.pathid[p2];
562

563
564
			if (p1id == succ)
			  continue;
565

566
567
568
569
570
571
572
			dout << p1 << " ∧ " << t << "δ → " << p2 << '\n';
			out << -p1id << ' ' << -ti << ' ' << succ << " 0\n";
			++nclauses;
		      }
		  }
	      }
	  }
573
574

      // construction of constraints (11,12,13)
575
      for (unsigned q1p = 0; q1p < ref_size; ++q1p)
576
	{
577
578
579
580
	  if (!sm.reachable_state(q1p))
	    continue;
	  unsigned q1p_scc = sm.scc_of(q1p);
	  for (unsigned q2p = 0; q2p < ref_size; ++q2p)
581
	    {
582
583
	      if (!sm.reachable_state(q2p))
		continue;
584
585
	      // We are only interested in transition that can form a
	      // cycle, so they must belong to the same SCC.
586
	      if (sm.scc_of(q2p) != q1p_scc)
587
		continue;
588
589
	      bool is_weak = d.is_weak_scc[q1p_scc];
	      bool is_acc = sm.is_accepting_scc(q1p_scc);
590

591
592
	      for (unsigned q1 = 0; q1 < d.cand_size; ++q1)
		for (unsigned q2 = 0; q2 < d.cand_size; ++q2)
593
594
		  {
		    size_t sf = d.all_cand_acc.size();
595
		    size_t sfp = is_weak ? 1 : d.all_ref_acc.size();
596
597
598
599
600
		    for (size_t f = 0; f < sf; ++f)
		      for (size_t fp = 0; fp < sfp; ++fp)
			{
			  path p(q1, q1p, q2, q2p,
				 d.all_cand_acc[f], d.all_ref_acc[fp]);
601

602
			  dout << "(11&12&13) paths from " << p << '\n';
603

604
			  int pid = d.pathid[p];
605

606
			  for (auto& tr: ref->out(q2p))
607
			    {
608
			      unsigned dp = tr.dst;
609
			      // Skip destinations not in the SCC.
610
611
			      if (sm.scc_of(dp) != q1p_scc)
				continue;
612

613
			      for (unsigned q3 = 0; q3 < d.cand_size; ++q3)
614
				{
615
				  bdd all = tr.cond;
616
				  acc_cond::mark_t curacc = tr.acc;
617
				  while (all != bddfalse)
618
				    {
619
620
				      bdd l = bdd_satoneset(all, ap, bddfalse);
				      all -= l;
621

622
623
				      transition t(q2, l, q3);
				      int ti = d.transid[t];
624

625
				      if (dp == q1p && q3 == q1) // (11,12) loop
626
					{
627
628
					  if ((!is_acc) ||
					      (!is_weak &&
629
630
					       !racc.accepting
					       (curacc | d.all_ref_acc[fp])))
631
					    {
632
633
634
635
636
#if DEBUG
					      dout << "(11) " << p << " ∧ "
						   << t << "δ → ¬(";

					      bool notfirst = false;
637
638
639
640
					      acc_cond::mark_t all_ =
						d.all_cand_acc.back() -
						d.all_cand_acc[f];
					      for (auto m: d.cacc.sets(all_))
641
						{
642
643
644
						  transition_acc
						    ta(q2, l,
						       d.cacc.mark(m), q1);
645
646
647
648
649
650
651
						  if (notfirst)
						    out << " ∧ ";
						  else
						    notfirst = true;
						  out << ta << "FC";
						}
					      out << ")\n";
652
#endif // DEBUG
653
					      out << -pid << ' ' << -ti;
654
655

					      // 11
656
657
658
659
					      acc_cond::mark_t all_f =
						d.all_cand_acc.back() -
						d.all_cand_acc[f];
					      for (auto m: d.cacc.sets(all_f))
660
						{
661
662
663
						  transition_acc
						    ta(q2, l,
						       d.cacc.mark(m), q1);
664
665
						  int tai = d.transaccid[ta];
						  assert(tai != 0);
666
						  out << ' ' << -tai;
667
668
						}
					      out << " 0\n";
669
670
					      ++nclauses;
					    }
671
672
673
674
675
676
					  else
					    {
#if DEBUG
					      dout << "(12) " << p << " ∧ "
						   << t << "δ → (";
					      bool notfirst = false;
677
678
679
680
					      // 11
					      acc_cond::mark_t all_ =
						d.cacc.comp(d.all_cand_acc[f]);
					      for (auto m: d.cacc.sets(all_))
681
						{
682
683
684
						  transition_acc
						    ta(q2, l,
						       d.cacc.mark(m), q1);
685
686
687
688
689
690
691
692
693
						  if (notfirst)
						    out << " ∧ ";
						  else
						    notfirst = true;
						  out << ta << "FC";
						}
					      out << ")\n";
#endif // DEBUG
					      // 12
694
695
696
					      acc_cond::mark_t all_f =
						d.cacc.comp(d.all_cand_acc[f]);
					      for (auto m: d.cacc.sets(all_f))
697
						{
698
699
700
						  transition_acc
						    ta(q2, l,
						       d.cacc.mark(m), q1);
701
702
703
						  int tai = d.transaccid[ta];
						  assert(tai != 0);

704
705
						  out << -pid << ' ' << -ti
						      << ' ' << tai << " 0\n";
706
707
708
						  ++nclauses;
						}
					    }
709
					}
710
				      // (13) augmenting paths (always).
711
				      {
712
713
					size_t sf = d.all_cand_acc.size();
					for (size_t f = 0; f < sf; ++f)
714
					  {
715
716
717
					    acc_cond::mark_t f2 =
					      p.acc_cand | d.all_cand_acc[f];
					    acc_cond::mark_t f2p = 0U;
718
719
					    if (!is_weak)
					      f2p = p.acc_ref | curacc;
720

721
722
723
724
725
726
727
728
729
					    path p2(p.src_cand, p.src_ref,
						    q3, dp, f2, f2p);
					    int p2id = d.pathid[p2];
					    if (pid == p2id)
					      continue;
#if DEBUG
					    dout << "(13) " << p << " ∧ "
						 << t << "δ ";

730
731
732
					    auto biga_ = d.all_cand_acc[f];
					    for (unsigned m = 0;
						 m < d.cand_nacc; ++m)
733
					      {
734
735
736
737
738
739
740
741
						transition_acc
						  ta(q2, l,
						     d.cacc.mark(m), q3);
						const char* not_ = "¬";
						if (d.cacc.has(biga_, m))
						  not_ = "";
						out <<  " ∧ " << not_
						    << ta << "FC";
742
					      }
743
					    out << " → " << p2 << '\n';
744
#endif
745
					    out << -pid << ' ' << -ti << ' ';
746
747
748
					    auto biga = d.all_cand_acc[f];
					    for (unsigned m = 0;
						 m < d.cand_nacc; ++m)
749
					      {
750
751
752
						transition_acc
						  ta(q2, l,
						     d.cacc.mark(m), q3);
753
						int tai = d.transaccid[ta];
754
755
						if (d.cacc.has(biga, m))
						  tai = -tai;
756
						out << tai << ' ';
757
758
759
760
					      }

					    out << p2id << " 0\n";
					    ++nclauses;
761
762
					  }
				      }
763
				    }
764
765
766
				}
			    }
			}
767
768
769
		  }
	    }
	}
770
      out.seekp(0);
771
      out << "p cnf " << d.nvars << ' ' << nclauses.nb_clauses();
772
      return std::make_pair(d.nvars, nclauses.nb_clauses());
773
774
    }

775
    static tgba_digraph_ptr
776
    sat_build(const satsolver::solution& solution, dict& satdict,
777
	      const_tgba_digraph_ptr aut, bool state_based)
778
    {
779
      auto autdict = aut->get_dict();
780
      auto a = make_tgba_digraph(autdict);
781
      a->copy_ap_of(aut);
782
      a->set_generalized_buchi(satdict.cand_nacc);
783

784
      a->new_states(satdict.cand_size);
785

786
787
788
789
      // Last transition set in the automaton.
      unsigned last_aut_trans = -1U;
      // Last transition read from the SAT result.
      const transition* last_sat_trans = nullptr;
790
791
792
793

#if DEBUG
      std::fstream out("dtgba-sat.dbg",
		       std::ios_base::trunc | std::ios_base::out);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
794
      out.exceptions(std::ifstream::failbit | std::ifstream::badbit);
795
796
797
798
      std::set<int> positive;
#endif

      dout << "--- transition variables ---\n";
799
      std::map<int, acc_cond::mark_t> state_acc;
800
      std::set<src_cond> seen_trans;
801
      for (int v: solution)
802
803
804
805
806
807
808
809
810
811
812
813
	{
	  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())
	    {
814
815
816
817
	      // 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)
		{
818
		  acc_cond::mark_t acc = 0U;
819
820
		  if (state_based)
		    {
821
		      auto i = state_acc.find(t->second.src);
822
		      if (i != state_acc.end())
823
			acc = i->second;
824
		    }
825

826
827
		  last_aut_trans = a->new_transition(t->second.src,
						     t->second.dst,
828
829
						     t->second.cond,
						     acc);
830
831
832
		  last_sat_trans = &t->second;

		  dout << v << '\t' << t->second << \n";
833
		}
834
835
836
837
838
839
840
841
842
	    }
	  else
	    {
	      dict::rev_acc_map::const_iterator ta;
	      ta = satdict.revtransaccid.find(v);
	      // This assumes that the sat solvers output variables in
	      // increasing order.
	      if (ta != satdict.revtransaccid.end())
		{
843
		  dout << v << '\t' << ta->second << "F\n";
844
845
846
847
848

		  if (last_sat_trans &&
		      ta->second.src == last_sat_trans->src &&
		      ta->second.cond == last_sat_trans->cond &&
		      ta->second.dst == last_sat_trans->dst)
849
850
		    {
		      assert(!state_based);
851
852
		      auto& v = a->trans_data(last_aut_trans).acc;
		      v |= ta->second.acc;
853
854
855
		    }
		  else if (state_based)
		    {
856
857
		      auto& v = state_acc[ta->second.src];
		      v |= ta->second.acc;
858
		    }
859
860
861
862
		}
	    }
	}
#if DEBUG
863
      dout << "--- pathid variables ---\n";
864
865
866
      for (auto pit: satdict.pathid)
	if (positive.find(pit.second) != positive.end())
	  dout << pit.second << '\t' << pit.first << "C\n";
867
868
869
870
871
872
873
874
#endif

      a->merge_transitions();

      return a;
    }
  }

875
  tgba_digraph_ptr
876
877
878
  dtgba_sat_synthetize(const const_tgba_digraph_ptr& a,
		       unsigned target_acc_number,
		       int target_state_number, bool state_based)
879
  {
880
881
882
    if (!a->acc().is_generalized_buchi())
      throw std::runtime_error
	("dtgba_sat() can only work with generalized Büchi acceptance");
883
    if (target_state_number == 0)
884
      return nullptr;
885
886
887
888
    trace << "dtgba_sat_synthetize(..., acc = " << target_acc_number
	  << ", states = " << target_state_number
	  << ", state_based = " << state_based << ")\n";

889
890
891
    dict d(a);
    d.cand_size = target_state_number;
    d.cand_nacc = target_acc_number;
892

893
894
    satsolver solver;
    satsolver::solution_pair solution;
895

896
897
898
899
900
    timer_map t;
    t.start("encode");
    sat_stats s = dtgba_to_sat(solver(), a, d, state_based);
    t.stop("encode");
    t.start("solve");
901
    solution = solver.get_solution();
902
    t.stop("solve");
903

904
    tgba_digraph_ptr res = nullptr;
905
906
    if (!solution.second.empty())
      res = sat_build(solution.second, d, a, state_based);
907

908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
    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);

936
    trace << "dtgba_sat_synthetize(...) = " << res << '\n';
937
938
939
    return res;
  }

940
  tgba_digraph_ptr
941
  dtgba_sat_minimize(const const_tgba_digraph_ptr& a,
942
		     unsigned target_acc_number,
943
944
945
946
		     bool state_based)
  {
    int n_states = stats_reachable(a).states;

947
    tgba_digraph_ptr prev = nullptr;
948
    for (;;)
949
      {
950
	auto next =
951
952
	  dtgba_sat_synthetize(prev ? prev : a, target_acc_number,
			       --n_states, state_based);
953
	if (!next)
954
	  return prev;
955
956
	else
	  n_states = stats_reachable(next).states;
957
	prev = next;
958
      }
959
    SPOT_UNREACHABLE();
960
961
  }

962
  tgba_digraph_ptr
963
  dtgba_sat_minimize_dichotomy(const const_tgba_digraph_ptr& a,
964
			       unsigned target_acc_number,
965
966
967
968
			       bool state_based)
  {
    int max_states = stats_reachable(a).states - 1;
    int min_states = 1;
969

970
    tgba_digraph_ptr prev = nullptr;
971
    while (min_states <= max_states)
972
      {
973
	int target = (max_states + min_states) / 2;
974
	auto next =
975
976
	  dtgba_sat_synthetize(prev ? prev : a, target_acc_number, target,
			       state_based);
977
	if (!next)
978
	  {
979
980
981
982
983
	    min_states = target + 1;
	  }
	else
	  {
	    prev = next;
984
	    max_states = stats_reachable(next).states - 1;
985
986
	  }
      }
987
    return prev;
988
989
990
  }

}