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

#include <iostream>
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
21
#include <fstream>
22
23
24
25
26
#include <sstream>
#include "dtgbasat.hh"
#include "reachiter.hh"
#include <map>
#include <utility>
27
#include "sccinfo.hh"
28
#include "twa/bddprint.hh"
29
30
31
#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_twa_ptr& a)
249
	: aut(a)
250
251
252
      {
      }

253
      const_twa_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
    unsigned declare_vars(const const_twa_graph_ptr& aut,
289
			  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_twa_graph_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 twa_graph_ptr
776
    sat_build(const satsolver::solution& solution, dict& satdict,
777
	      const_twa_graph_ptr aut, bool state_based)
778
    {
779
      auto autdict = aut->get_dict();
780
      auto a = make_twa_graph(autdict);
781
      a->copy_ap_of(aut);
782
      a->set_generalized_buchi(satdict.cand_nacc);
783
784
      if (state_based)
	a->prop_state_based_acc();
785
      a->new_states(satdict.cand_size);
786

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

#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
795
      out.exceptions(std::ifstream::failbit | std::ifstream::badbit);
796
797
798
799
      std::set<int> positive;
#endif

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

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

		  dout << v << '\t' << t->second << \n";
834
		}
835
836
837
838
839
840
841
842
843
	    }
	  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())
		{
844
		  dout << v << '\t' << ta->second << "F\n";
845
846
847
848
849

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

      a->merge_transitions();

      return a;
    }
  }

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

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

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

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

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

909
910
911
912
913
914
915
916
917
    // 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())
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
      {
	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';
      }
940
    static bool show = getenv("SPOT_SATSHOW");
941
942
943
    if (show && res)
      dotty_reachable(std::cout, res);

944
    trace << "dtgba_sat_synthetize(...) = " << res << '\n';
945
946
947
    return res;
  }

948
949
  twa_graph_ptr
  dtgba_sat_minimize(const const_twa_graph_ptr& a,
950
		     unsigned target_acc_number,
951
952
953
954
		     bool state_based)
  {
    int n_states = stats_reachable(a).states;

955
    twa_graph_ptr prev = nullptr;
956
    for (;;)
957
      {
958
	auto next =
959
960
	  dtgba_sat_synthetize(prev ? prev : a, target_acc_number,
			       --n_states, state_based);
961
	if (!next)
962
	  return prev;
963
964
	else
	  n_states = stats_reachable(next).states;
965
	prev = next;
966
      }
967
    SPOT_UNREACHABLE();
968
969
  }

970
971
  twa_graph_ptr
  dtgba_sat_minimize_dichotomy(const const_twa_graph_ptr& a,
972
			       unsigned target_acc_number,
973
974
975
976
			       bool state_based)
  {
    int max_states = stats_reachable(a).states - 1;
    int min_states = 1;
977

978
    twa_graph_ptr prev = nullptr;
979
    while (min_states <= max_states)
980
      {
981
	int target = (max_states + min_states) / 2;
982
	auto next =
983
984
	  dtgba_sat_synthetize(prev ? prev : a, target_acc_number, target,
			       state_based);
985
	if (!next)
986
	  {
987
988
989
990
991
	    min_states = target + 1;
	  }
	else
	  {
	    prev = next;
992
	    max_states = stats_reachable(next).states - 1;
993
994
	  }
      }
995
    return prev;
996
997
998
  }

}