simplify.cc 113 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE).
4
5
6
7
8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
10
11
12
13
14
15
16
17
// (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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19

20
21
22
23
24
25
26
27
#include <iostream>
//#define TRACE
#ifdef TRACE
#define trace std::cerr
#else
#define trace while (0) std::cerr
#endif

28
29
30
31
#include "simplify.hh"
#include "misc/hash.hh"
#include "ltlast/allnodes.hh"
#include "ltlast/visitor.hh"
32
33
#include "ltlvisit/contain.hh"
#include "ltlvisit/tostring.hh"
34
#include "ltlvisit/snf.hh"
35
36
37
38
39
40
41
#include <cassert>

namespace spot
{
  namespace ltl
  {

42

43
44
45
46
47
48
49
    // The name of this class is public, but not its contents.
    class ltl_simplifier_cache
    {
      typedef Sgi::hash_map<const formula*, const formula*,
			    ptr_hash<formula> > f2f_map;
      typedef Sgi::hash_map<const formula*, bdd,
			    ptr_hash<formula> > f2b_map;
50
51
      typedef std::pair<const formula*, const formula*> pairf;
      typedef std::map<pairf, bool> syntimpl_cache_t;
52
    public:
53
      bdd_dict* dict;
54
      ltl_simplifier_options options;
55
      language_containment_checker lcc;
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87

      ~ltl_simplifier_cache()
      {
	{
	  f2f_map::iterator i = simplified_.begin();
	  f2f_map::iterator end = simplified_.end();
	  while (i != end)
	    {
	      f2f_map::iterator old = i++;
	      old->second->destroy();
	      old->first->destroy();
	    }
	}
	{
	  f2f_map::iterator i = nenoform_.begin();
	  f2f_map::iterator end = nenoform_.end();
	  while (i != end)
	    {
	      f2f_map::iterator old = i++;
	      old->second->destroy();
	      old->first->destroy();
	    }
	}
	{
	  f2b_map::iterator i = as_bdd_.begin();
	  f2b_map::iterator end = as_bdd_.end();
	  while (i != end)
	    {
	      f2b_map::iterator old = i++;
	      old->first->destroy();
	    }
	}
88
89
90
91
92
93
94
95
96
97
	{
	  syntimpl_cache_t::iterator i = syntimpl_.begin();
	  syntimpl_cache_t::iterator end = syntimpl_.end();
	  while (i != end)
	    {
	      syntimpl_cache_t::iterator old = i++;
	      old->first.first->destroy();
	      old->first.second->destroy();
	    }
	}
98
99
100
101
102
103
104
105
106
107
	{
	  snf_cache::iterator i = snf_cache_.begin();
	  snf_cache::iterator end = snf_cache_.end();
	  while (i != end)
	    {
	      snf_cache::iterator old = i++;
	      old->second->destroy();
	      old->first->destroy();
	    }
	}
108

109
	dict->unregister_all_my_variables(this);
110
111
      }

112
113
      ltl_simplifier_cache(bdd_dict* d)
	: dict(d), lcc(d, true, true, false, false)
114
115
116
      {
      }

117
      ltl_simplifier_cache(bdd_dict* d, const ltl_simplifier_options& opt)
118
	: dict(d), options(opt), lcc(d, true, true, false, false)
119
      {
120
	options.containment_checks |= options.containment_checks_stronger;
121
122
      }

123
124
125
126
127
128
129
130
131
132
      void
      print_stats(std::ostream& os) const
      {
	os << "simplified formulae:    " << simplified_.size() << " entries\n"
	   << "negative normal form:   " << nenoform_.size() << " entries\n"
	   << "syntactic implications: " << syntimpl_.size() << " entries\n"
	   << "boolean to bdd:         " << as_bdd_.size() << " entries\n"
	   << "star normal form:       " << snf_cache_.size() << " entries\n";
      }

133
134
135
136
137
138
139
140
141
142
143
144
145
      void
      clear_as_bdd_cache()
      {
	f2b_map::iterator i = as_bdd_.begin();
	f2b_map::iterator end = as_bdd_.end();
	while (i != end)
	  {
	    f2b_map::iterator old = i++;
	    old->first->destroy();
	  }
	as_bdd_.clear();
      }

146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
      // Convert a Boolean formula into a BDD for easier comparison.
      bdd
      as_bdd(const formula* f)
      {
	// Lookup the result in case it has already been computed.
	f2b_map::const_iterator it = as_bdd_.find(f);
	if (it != as_bdd_.end())
	  return it->second;

	bdd result = bddfalse;

	switch (f->kind())
	  {
	  case formula::Constant:
	    if (f == constant::true_instance())
	      result = bddtrue;
	    else if (f == constant::false_instance())
163
	      result = bddfalse;
164
165
166
167
	    else
	      assert(!"Unsupported operator");
	    break;
	  case formula::AtomicProp:
168
	    result = bdd_ithvar(dict->register_proposition(f, this));
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
	    break;
	  case formula::UnOp:
	    {
	      const unop* uo = static_cast<const unop*>(f);
	      assert(uo->op() == unop::Not);
	      result = !as_bdd(uo->child());
	      break;
	    }
	  case formula::BinOp:
	    {
	      const binop* bo = static_cast<const binop*>(f);
	      int op = 0;
	      switch (bo->op())
		{
		case binop::Xor:
		  op = bddop_xor;
		  break;
		case binop::Implies:
		  op = bddop_imp;
		  break;
		case binop::Equiv:
		  op = bddop_biimp;
		  break;
		default:
		  assert(!"Unsupported operator");
		}
	      result = bdd_apply(as_bdd(bo->first()), as_bdd(bo->second()), op);
	      break;
	    }
	  case formula::MultOp:
	    {
	      const multop* mo = static_cast<const multop*>(f);
	      switch (mo->op())
		{
		case multop::And:
		  {
		    result = bddtrue;
		    unsigned s = mo->size();
		    for (unsigned n = 0; n < s; ++n)
		      result &= as_bdd(mo->nth(n));
		    break;
		  }
		case multop::Or:
		  {
		    result = bddfalse;
		    unsigned s = mo->size();
		    for (unsigned n = 0; n < s; ++n)
		      result |= as_bdd(mo->nth(n));
		    break;
		  }
219
		case multop::AndNLM:
220
221
		case multop::AndRat:
		case multop::OrRat:
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
		case multop::Concat:
		case multop::Fusion:
		  assert(!"Unsupported operator");
		  break;
		}
	      break;
	    }
	  case formula::BUnOp:
	  case formula::AutomatOp:
	    assert(!"Unsupported operator");
	    break;
	  }

	// Cache the result before returning.
	as_bdd_[f->clone()] = result;
	return result;
      }

      const formula*
      lookup_nenoform(const formula* f)
      {
	f2f_map::const_iterator i = nenoform_.find(f);
	if (i == nenoform_.end())
	  return 0;
	return i->second->clone();
      }

      void
      cache_nenoform(const formula* orig, const formula* nenoform)
      {
	nenoform_[orig->clone()] = nenoform->clone();
      }

255
256
257
258
259
      // Return true iff the option set (syntactic implication
      // or containment checks) allow to prove that f1 => f2.
      bool
      implication(const formula* f1, const formula* f2)
      {
260
261
262
263
264
265
266
267
268
269
	trace << "[->] does " << to_string(f1) << " implies "
	      << to_string(f2) << " ?" << std::endl;
	if ((options.synt_impl && syntactic_implication(f1, f2))
	    || (options.containment_checks && contained(f1, f2)))
	  {
	    trace << "[->] Yes" << std::endl;
	    return true;
	  }
	trace << "[->] No" << std::endl;
	return false;
270
271
272
      }

      // Return true if f1 => f2 syntactically
273
      bool
274
      syntactic_implication(const formula* f1, const formula* f2);
275
276
      bool
      syntactic_implication_aux(const formula* f1, const formula* f2);
277

278
279
280
      // Return true if f1 => f2
      bool
      contained(const formula* f1, const formula* f2)
281
      {
282
283
284
285
286
287
288
289
	if (!f1->is_psl_formula() || !f2->is_psl_formula())
	  return false;
	return lcc.contained(f1, f2);
      }

      // If right==false, true if !f1 => f2, false otherwise.
      // If right==true, true if f1 => !f2, false otherwise.
      bool
290
291
      syntactic_implication_neg(const formula* f1, const formula* f2,
				bool right);
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353

      // Return true if f1 => !f2
      bool contained_neg(const formula* f1, const formula* f2)
      {
	if (!f1->is_psl_formula() || !f2->is_psl_formula())
	  return false;
	trace << "[CN] Does (" << to_string(f1) << ") implies !("
	      << to_string(f2) << ") ?" << std::endl;
	if (lcc.contained_neg(f1, f2))
	  {
	    trace << "[CN] Yes" << std::endl;
	    return true;
	  }
	else
	  {
	    trace << "[CN] No" << std::endl;
	    return false;
	  }
      }

      // Return true if f1 => !f2
      bool neg_contained(const formula* f1, const formula* f2)
      {
	if (!f1->is_psl_formula() || !f2->is_psl_formula())
	  return false;
	trace << "[NC] Does (" << to_string(f1) << ") implies !("
	      << to_string(f2) << ") ?" << std::endl;
	if (lcc.neg_contained(f1, f2))
	  {
	    trace << "[NC] Yes" << std::endl;
	    return true;
	  }
	else
	  {
	    trace << "[NC] No" << std::endl;
	    return false;
	  }
      }

      // Return true iff the option set (syntactic implication
      // or containment checks) allow to prove that
      //   - !f2 => f2   (case where right=false)
      //   - f1 => !f2   (case where right=true)
      bool
      implication_neg(const formula* f1, const formula* f2, bool right)
      {
	trace << "[IN] Does " << (right ? "(" : "!(")
	      << to_string(f1) << ") implies "
	      << (right ? "!(" : "(") << to_string(f2) << ") ?"
	      << std::endl;
	if ((options.synt_impl && syntactic_implication_neg(f1, f2, right))
	    || (options.containment_checks && right && contained_neg(f1, f2))
	    || (options.containment_checks && !right && neg_contained(f1, f2)))
	  {
	    trace << "[IN] Yes" << std::endl;
	    return true;
	  }
	else
	  {
	    trace << "[IN] No" << std::endl;
	    return false;
	  }
354
355
      }

356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
      const formula*
      lookup_simplified(const formula* f)
      {
	f2f_map::const_iterator i = simplified_.find(f);
	if (i == simplified_.end())
	  return 0;
	return i->second->clone();
      }

      void
      cache_simplified(const formula* orig, const formula* simplified)
      {
	simplified_[orig->clone()] = simplified->clone();
      }

371
372
373
374
375
376
      const formula*
      star_normal_form(const formula* f)
      {
	return ltl::star_normal_form(f, &snf_cache_);
      }

377
378
379
380
    private:
      f2b_map as_bdd_;
      f2f_map simplified_;
      f2f_map nenoform_;
381
      syntimpl_cache_t syntimpl_;
382
      snf_cache snf_cache_;
383
384
385
386
387
    };


    namespace
    {
388
389
390
391
392
393
      //////////////////////////////////////////////////////////////////////
      //
      //  NEGATIVE_NORMAL_FORM_VISITOR
      //
      //////////////////////////////////////////////////////////////////////

394
395
396
397
398
399
400
401
402
      // Forward declaration.
      const formula*
      nenoform_recursively(const formula* f,
			   bool negated,
			   ltl_simplifier_cache* c);

      class negative_normal_form_visitor: public visitor
      {
      public:
403
404
	negative_normal_form_visitor(bool negated, ltl_simplifier_cache* c)
	  : negated_(negated), cache_(c)
405
406
407
408
409
410
411
412
	{
	}

	virtual
	~negative_normal_form_visitor()
	{
	}

413
	const formula* result() const
414
415
416
417
418
	{
	  return result_;
	}

	void
419
	visit(const atomic_prop* ap)
420
	{
421
	  const formula* f = ap->clone();
422
423
424
425
426
427
428
	  if (negated_)
	    result_ = unop::instance(unop::Not, f);
	  else
	    result_ = f;
	}

	void
429
	visit(const constant* c)
430
431
432
433
434
435
436
437
438
439
	{
	  // Negation of constants is taken care of in the constructor
	  // of unop::Not, so these cases should be caught by
	  // nenoform_recursively().
	  assert(!negated_);
	  result_ = c;
	  return;
	}

	void
440
	visit(const unop* uo)
441
	{
442
	  const formula* f = uo->child();
443
444
	  unop::type op = uo->op();
	  switch (op)
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
	    {
	    case unop::Not:
	      // "Not"s should be caught by nenoform_recursively().
	      assert(!"Not should not occur");
	      //result_ = recurse_(f, negated_ ^ true);
	      return;
	    case unop::X:
	      /* !Xa == X!a */
	      result_ = unop::instance(unop::X, recurse(f));
	      return;
	    case unop::F:
	      /* !Fa == G!a */
	      result_ = unop::instance(negated_ ? unop::G : unop::F,
				       recurse(f));
	      return;
	    case unop::G:
	      /* !Ga == F!a */
	      result_ = unop::instance(negated_ ? unop::F : unop::G,
				       recurse(f));
	      return;
	    case unop::Closure:
	      result_ = unop::instance(negated_ ?
				       unop::NegClosure : unop::Closure,
				       recurse_(f, false));
	      return;
	    case unop::NegClosure:
471
	    case unop::NegClosureMarked:
472
	      result_ = unop::instance(negated_ ?
473
				       unop::Closure : op,
474
475
476
477
478
479
480
481
482
483
484
485
486
487
				       recurse_(f, false));
	      return;
	      /* !Finish(x), is not simplified */
	    case unop::Finish:
	      result_ = unop::instance(uo->op(), recurse_(f, false));
	      if (negated_)
		result_ = unop::instance(unop::Not, result_);
	      return;
	    }
	  /* Unreachable code.  */
	  assert(0);
	}

	void
488
	visit(const bunop* bo)
489
	{
490
491
	  // !(a*) should never occur.
	  assert(!negated_);
492
493
494
495
	  result_ = bunop::instance(bo->op(), recurse_(bo->child(), false),
				    bo->min(), bo->max());
	}

496
497
498
	const formula* equiv_or_xor(bool equiv,
				    const formula* f1,
				    const formula* f2)
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
	{
	  // Rewrite a<=>b as (a&b)|(!a&!b)
	  if (equiv)
	    return
	      multop::instance(multop::Or,
			       multop::instance(multop::And,
						recurse_(f1, false),
						recurse_(f2, false)),
			       multop::instance(multop::And,
						recurse_(f1, true),
						recurse_(f2, true)));
	  else
	    // Rewrite a^b as (a&!b)|(!a&b)
	    return
	      multop::instance(multop::Or,
			       multop::instance(multop::And,
						recurse_(f1, false),
						recurse_(f2, true)),
			       multop::instance(multop::And,
						recurse_(f1, true),
						recurse_(f2, false)));
	}

522
	void
523
	visit(const binop* bo)
524
	{
525
526
	  const formula* f1 = bo->first();
	  const formula* f2 = bo->second();
527
528
529
	  switch (bo->op())
	    {
	    case binop::Xor:
530
531
	      // !(a ^ b) == a <=> b
	      result_ = equiv_or_xor(negated_, f1, f2);
532
533
	      return;
	    case binop::Equiv:
534
535
	      // !(a <=> b) == a ^ b
	      result_ = equiv_or_xor(!negated_, f1, f2);
536
537
538
	      return;
	    case binop::Implies:
	      if (negated_)
539
		// !(a => b) == a & !b
540
541
542
		result_ = multop::instance(multop::And,
					   recurse_(f1, false),
					   recurse_(f2, true));
543
544
545
546
	      else // a => b == !a | b
		result_ = multop::instance(multop::Or,
					   recurse_(f1, true),
					   recurse_(f2, false));
547
548
	      return;
	    case binop::U:
549
	      // !(a U b) == !a R !b
550
551
552
553
	      result_ = binop::instance(negated_ ? binop::R : binop::U,
					recurse(f1), recurse(f2));
	      return;
	    case binop::R:
554
	      // !(a R b) == !a U !b
555
556
557
558
	      result_ = binop::instance(negated_ ? binop::U : binop::R,
					recurse(f1), recurse(f2));
	      return;
	    case binop::W:
559
	      // !(a W b) == !a M !b
560
561
562
563
	      result_ = binop::instance(negated_ ? binop::M : binop::W,
					recurse(f1), recurse(f2));
	      return;
	    case binop::M:
564
	      // !(a M b) == !a W !b
565
566
567
568
	      result_ = binop::instance(negated_ ? binop::W : binop::M,
					recurse(f1), recurse(f2));
	      return;
	    case binop::UConcat:
569
	      // !(a []-> b) == a<>-> !b
570
571
572
573
574
	      result_ = binop::instance(negated_ ?
					binop::EConcat : binop::UConcat,
					recurse_(f1, false), recurse(f2));
	      return;
	    case binop::EConcat:
575
	      // !(a <>-> b) == a[]-> !b
576
577
578
579
580
	      result_ = binop::instance(negated_ ?
					binop::UConcat : binop::EConcat,
					recurse_(f1, false), recurse(f2));
	      return;
	    case binop::EConcatMarked:
581
	      // !(a <>-> b) == a[]-> !b
582
583
584
585
586
587
	      result_ = binop::instance(negated_ ?
					binop::UConcat :
					binop::EConcatMarked,
					recurse_(f1, false), recurse(f2));
	      return;
	    }
588
	  // Unreachable code.
589
590
591
592
	  assert(0);
	}

	void
593
	visit(const automatop* ao)
594
595
596
597
598
599
600
601
602
603
604
	{
	  bool negated = negated_;
	  negated_ = false;
	  automatop::vec* res = new automatop::vec;
	  unsigned aos = ao->size();
	  for (unsigned i = 0; i < aos; ++i)
	    res->push_back(recurse(ao->nth(i)));
	  result_ = automatop::instance(ao->get_nfa(), res, negated);
	}

	void
605
	visit(const multop* mo)
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
	{
	  multop::type op = mo->op();
	  /* !(a & b & c) == !a | !b | !c  */
	  /* !(a | b | c) == !a & !b & !c  */
	  if (negated_)
	    switch (op)
	      {
	      case multop::And:
		op = multop::Or;
		break;
	      case multop::Or:
		op = multop::And;
		break;
	      case multop::Concat:
	      case multop::Fusion:
	      case multop::AndNLM:
622
623
	      case multop::OrRat:
	      case multop::AndRat:
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
		break;
	      }
	  multop::vec* res = new multop::vec;
	  unsigned mos = mo->size();
	  switch (op)
	    {
	    case multop::And:
	    case multop::Or:
	      {
		for (unsigned i = 0; i < mos; ++i)
		  res->push_back(recurse(mo->nth(i)));
		result_ = multop::instance(op, res);
		break;
	      }
	    case multop::Concat:
	    case multop::Fusion:
	    case multop::AndNLM:
641
642
	    case multop::AndRat:
	    case multop::OrRat:
643
644
645
646
647
648
649
650
651
	      {
		for (unsigned i = 0; i < mos; ++i)
		  res->push_back(recurse_(mo->nth(i), false));
		result_ = multop::instance(op, res);
		assert(!negated_);
	      }
	    }
	}

652
653
	const formula*
	recurse_(const formula* f, bool negated)
654
	{
655
	  return nenoform_recursively(f, negated, cache_);
656
657
	}

658
659
	const formula*
	recurse(const formula* f)
660
661
662
663
664
	{
	  return recurse_(f, negated_);
	}

      protected:
665
	const formula* result_;
666
667
668
669
670
671
672
673
674
675
	bool negated_;
	ltl_simplifier_cache* cache_;
      };


      const formula*
      nenoform_recursively(const formula* f,
			   bool negated,
			   ltl_simplifier_cache* c)
      {
676
	if (const unop* uo = is_Not(f))
677
	  {
678
679
	    negated = !negated;
	    f = uo->child();
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
	  }

	const formula* key = f;
	if (negated)
	  key = unop::instance(unop::Not, f->clone());
	const formula* result = c->lookup_nenoform(key);
	if (result)
	  goto done;

	if (key->is_in_nenoform()
	    || (c->options.nenoform_stop_on_boolean && key->is_boolean()))
	  {
	    result = key->clone();
	  }
	else
	  {
696
	    negative_normal_form_visitor v(negated, c);
697
	    f->accept(v);
698
699
700
701
702
703
704
705
706
707
708
	    result = v.result();
	  }

	c->cache_nenoform(key, result);
      done:
	if (negated)
	  key->destroy();

	return result;
      }

709
710
711
712
713
714
      //////////////////////////////////////////////////////////////////////
      //
      //  SIMPLIFY_VISITOR
      //
      //////////////////////////////////////////////////////////////////////

715
      // Forward declaration.
716
      const formula*
717
      simplify_recursively(const formula* f, ltl_simplifier_cache* c);
718

719

720

721
722
      // X(a) R b   or   X(a) M b
      // This returns a.
723
724
      const formula*
      is_XRM(const formula* f)
725
      {
726
	const binop* bo = is_binop(f, binop::R, binop::M);
727
	if (!bo)
728
	  return 0;
729
	const unop* uo = is_X(bo->first());
730
731
732
733
734
735
736
	if (!uo)
	  return 0;
	return uo->child();
      }

      // X(a) W b   or   X(a) U b
      // This returns a.
737
738
      const formula*
      is_XWU(const formula* f)
739
      {
740
	const binop* bo = is_binop(f, binop::W, binop::U);
741
	if (!bo)
742
	  return 0;
743
	const unop* uo = is_X(bo->first());
744
745
746
747
748
	if (!uo)
	  return 0;
	return uo->child();
      }

749
750
      // b & X(b W a)  or   b & X(b U a)
      // This returns (b W a) or (b U a).
751
752
      const binop*
      is_bXbWU(const formula* f)
753
      {
754
	const multop* mo = is_multop(f, multop::And);
755
756
757
758
759
	if (!mo)
	  return 0;
	unsigned s = mo->size();
	for (unsigned pos = 0; pos < s; ++pos)
	  {
760
	    const unop* u = is_X(mo->nth(pos));
761
762
	    if (!u)
	      continue;
763
	    const binop* bo = is_binop(u->child(), binop::U, binop::W);
764
765
	    if (!bo)
	      continue;
766
	    const formula* b = mo->all_but(pos);
767
768
769
770
771
772
773
774
775
776
	    bool result = (b == bo->first());
	    b->destroy();
	    if (result)
	      return bo;
	  }
	return 0;
      }

      // b | X(b R a)  or   b | X(b M a)
      // This returns (b R a) or (b M a).
777
778
      const binop*
      is_bXbRM(const formula* f)
779
      {
780
	const multop* mo = is_multop(f, multop::Or);
781
782
783
784
785
	if (!mo)
	  return 0;
	unsigned s = mo->size();
	for (unsigned pos = 0; pos < s; ++pos)
	  {
786
	    const unop* u = is_X(mo->nth(pos));
787
788
	    if (!u)
	      continue;
789
	    const binop* bo = is_binop(u->child(), binop::R, binop::M);
790
791
	    if (!bo)
	      continue;
792
	    const formula* b = mo->all_but(pos);
793
794
795
796
797
798
799
800
	    bool result = (b == bo->first());
	    b->destroy();
	    if (result)
	      return bo;
	  }
	return 0;
      }

801
      const formula*
802
803
804
805
806
      unop_multop(unop::type uop, multop::type mop, multop::vec* v)
      {
	return unop::instance(uop, multop::instance(mop, v));
      }

807
      const formula*
808
809
810
811
812
813
      unop_unop_multop(unop::type uop1, unop::type uop2, multop::type mop,
		       multop::vec* v)
      {
	return unop::instance(uop1, unop_multop(uop2, mop, v));
      }

814
815
      const formula*
      unop_unop(unop::type uop1, unop::type uop2, const formula* f)
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
      {
	return unop::instance(uop1, unop::instance(uop2, f));
      }

      struct mospliter
      {
	enum what { Split_GF = (1 << 0),
		    Strip_GF = (1 << 1) | (1 << 0),
		    Split_FG = (1 << 2),
		    Strip_FG = (1 << 3) | (1 << 2),
		    Split_F = (1 << 4),
		    Strip_F = (1 << 5) | (1 << 4),
		    Split_G = (1 << 6),
		    Strip_G = (1 << 7) | (1 << 6),
		    Strip_X = (1 << 8),
		    Split_U_or_W = (1 << 9),
		    Split_R_or_M = (1 << 10),
		    Split_EventUniv = (1 << 11),
834
835
836
		    Split_Event = (1 << 12),
		    Split_Univ = (1 << 13),
		    Split_Bool = (1 << 14)
837
838
839
840
841
842
843
844
845
846
847
	};

	void init()
	{
	  res_GF = (split_ & Split_GF) ? new multop::vec : 0;
	  res_FG = (split_ & Split_FG) ? new multop::vec : 0;
	  res_F = (split_ & Split_F) ? new multop::vec : 0;
	  res_G = (split_ & Split_G) ? new multop::vec : 0;
	  res_X = (split_ & Strip_X) ? new multop::vec : 0;
	  res_U_or_W = (split_ & Split_U_or_W) ? new multop::vec : 0;
	  res_R_or_M = (split_ & Split_R_or_M) ? new multop::vec : 0;
848
849
850
	  res_EventUniv = (split_ & Split_EventUniv) ? new multop::vec : 0;
	  res_Event = (split_ & Split_Event) ? new multop::vec : 0;
	  res_Univ = (split_ & Split_Univ) ? new multop::vec : 0;
851
852
853
854
	  res_Bool = (split_ & Split_Bool) ? new multop::vec : 0;
	  res_other = new multop::vec;
	}

855
	void process(const formula* f)
856
857
858
859
860
	{
	  switch (f->kind())
	    {
	    case formula::UnOp:
	      {
861
862
		const unop* uo = static_cast<const unop*>(f);
		const formula* c = uo->child();
863
864
865
866
		switch (uo->op())
		  {
		  case unop::X:
		    if (res_X)
867
868
869
870
		      {
			res_X->push_back(c->clone());
			return;
		      }
871
872
873
		    break;
		  case unop::F:
		    if (res_FG)
874
875
876
877
878
879
		      if (const unop* cc = is_G(c))
			{
			  res_FG->push_back(((split_ & Strip_FG) == Strip_FG
					     ? cc->child() : f)->clone());
			  return;
			}
880
		    if (res_F)
881
882
883
884
885
		      {
			res_F->push_back(((split_ & Strip_F) == Strip_F
					  ? c : f)->clone());
			return;
		      }
886
887
888
		    break;
		  case unop::G:
		    if (res_GF)
889
890
891
892
893
894
		      if (const unop* cc = is_F(c))
			{
			  res_GF->push_back(((split_ & Strip_GF) == Strip_GF
					     ? cc->child() : f)->clone());
			  return;
			}
895
		    if (res_G)
896
897
898
899
900
		      {
			res_G->push_back(((split_ & Strip_G) == Strip_G
					  ? c : f)->clone());
			return;
		      }
901
902
903
904
905
906
907
908
		    break;
		  default:
		    break;
		  }
	      }
	      break;
	    case formula::BinOp:
	      {
909
		const binop* bo = static_cast<const binop*>(f);
910
911
912
913
914
		switch (bo->op())
		  {
		  case binop::U:
		  case binop::W:
		    if (res_U_or_W)
915
916
917
918
		      {
			res_U_or_W->push_back(bo->clone());
			return;
		      }
919
920
921
922
		    break;
		  case binop::R:
		  case binop::M:
		    if (res_R_or_M)
923
924
925
926
		      {
			res_R_or_M->push_back(bo->clone());
			return;
		      }
927
928
929
930
931
932
933
934
		    break;
		  default:
		    break;
		  }
	      }
	      break;
	    default:
	      if (res_Bool && f->is_boolean())
935
936
937
938
		{
		  res_Bool->push_back(f->clone());
		  return;
		}
939
940
	      break;
	    }
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
	  if (c_->options.event_univ)
	    {
	      bool e = f->is_eventual();
	      bool u = f->is_universal();
	      if (res_EventUniv && e && u)
		{
		  res_EventUniv->push_back(f->clone());
		  return;
		}
	      if (res_Event && e)
		{
		  res_Event->push_back(f->clone());
		  return;
		}
	      if (res_Univ && u)
		{
		  res_Univ->push_back(f->clone());
		  return;
		}
	    }

	  res_other->push_back(f->clone());
963
964
	}

965
966
	mospliter(unsigned split, multop::vec* v, ltl_simplifier_cache* cache)
	  : split_(split), c_(cache)
967
968
969
970
971
	{
	  init();
	  multop::vec::const_iterator end = v->end();
	  for (multop::vec::const_iterator i = v->begin(); i < end; ++i)
	    {
972
973
974
975
976
	      if (*i) // skip null pointers left by previous simplifications
		{
		  process(*i);
		  (*i)->destroy();
		}
977
978
979
980
	    }
	  delete v;
	}

981
982
	mospliter(unsigned split, const multop* mo,
		  ltl_simplifier_cache* cache)
983
	  : split_(split), c_(cache)
984
985
986
987
988
	{
	  init();
	  unsigned mos = mo->size();
	  for (unsigned i = 0; i < mos; ++i)
	    {
989
	      const formula* f = simplify_recursively(mo->nth(i), cache);
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
	      process(f);
	      f->destroy();
	    }
	  mo->destroy();
	}

	multop::vec* res_GF;
	multop::vec* res_FG;
	multop::vec* res_F;
	multop::vec* res_G;
	multop::vec* res_X;
	multop::vec* res_U_or_W;
	multop::vec* res_R_or_M;
	multop::vec* res_Event;
	multop::vec* res_Univ;
	multop::vec* res_EventUniv;
	multop::vec* res_Bool;
	multop::vec* res_other;
	unsigned split_;
1009
	ltl_simplifier_cache* c_;
1010
1011
      };

1012
1013
1014
      class simplify_visitor: public visitor
      {
      public:
1015

1016
1017
1018
1019
	simplify_visitor(ltl_simplifier_cache* cache)
	  : c_(cache), opt_(cache->options)
	{
	}
1020

1021
1022
1023
1024
	virtual ~simplify_visitor()
	{
	}

1025
	const formula*
1026
1027
1028
1029
1030
1031
	result() const
	{
	  return result_;
	}

	void
1032
	visit(const atomic_prop* ap)
1033
	{
1034
	  result_ = ap->clone();
1035
1036
1037
	}

	void
1038
	visit(const constant* c)
1039
1040
1041
1042
1043
	{
	  result_ = c;
	}

	void
1044
	visit(const bunop* bo)
1045
	{
1046
1047
	  bunop::type op = bo->op();
	  unsigned min = bo->min();
1048
	  const formula* h = recurse(bo->child());
1049
1050
1051
1052
1053
1054
1055
1056
1057
	  switch (op)
	    {
	    case bunop::Star:
	      if (h->accepts_eword())
		min = 0;
	      if (min == 0)
		{
		  const formula* s = c_->star_normal_form(h);
		  h->destroy();
1058
		  h = s;
1059
1060
1061
1062
		}
	      result_ = bunop::instance(op, h, min, bo->max());
	      break;
	    }
1063
	}
1064

1065
1066
	// if !neg build c&X(c&X(...&X(tail))) with n occurences of c
	// if neg build !c|X(!c|X(...|X(tail))).
1067
1068
1069
	const formula*
	dup_b_x_tail(bool neg, const formula* c,
		     const formula* tail, unsigned n)
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
	{
	  c->clone();
	  multop::type mop;
	  if (neg)
	    {
	      c = unop::instance(unop::Not, c);
	      mop = multop::Or;
	    }
	  else
	    {
	      mop = multop::And;
	    }
	  while (n--)
	    {
	      tail = unop::instance(unop::X, tail);
	      tail = // b&X(tail) or !b|X(tail)
		multop::instance(mop, c->clone(), tail);
	    }
	  c->destroy();
	  return tail;
	}

1092
	void
1093
	visit(const unop* uo)
1094
1095
1096
	{
	  result_ = recurse(uo->child());

1097
1098
	  unop::type op = uo->op();
	  switch (op)
1099
	    {
1100
1101
1102
1103
	    case unop::Not:
	      break;

	    case unop::X:
1104
1105
1106
1107
1108
	      // X(constant) = constant is a trivial identity, but if
	      // the constant has been constructed by recurse() this
	      // identity has not been applied.
	      if (is_constant(result_))
		  return;
1109

1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
	      // Xf = f if f is both eventual and universal.
	      if (result_->is_universal() && result_->is_eventual())
		{
		  if (opt_.event_univ)
		    return;
		  // If EventUniv simplification is disabled, use
		  // only the following basic rewriting rules:
		  //   XGF(f) = GF(f) and XFG(f) = FG(f)
		  // The former comes from Somenzi&Bloem (CAV'00).
		  // It's not clear why they do not list the second.
1120
1121
		  if (opt_.reduce_basics &&
		      (is_GF(result_) || is_FG(result_)))
1122
1123
		    return;
		}
1124

1125
1126
1127
1128
1129
1130

	      // If Xa = a, keep only a.
	      if (opt_.containment_checks_stronger
		  && c_->lcc.equal(result_, uo))
		return;

1131
1132
1133
1134
	      // Disabled: X(f1 & GF(f2)) = X(f1) & GF(f2)
	      // Disabled: X(f1 | GF(f2)) = X(f1) | GF(f2)
	      // Disabled: X(f1 & FG(f2)) = X(f1) & FG(f2)
	      // Disabled: X(f1 | FG(f2)) = X(f1) | FG(f2)
1135
1136
	      // The above make more sense when reversed,
	      // so see them in the And and Or rewritings.
1137
1138
	      break;

1139
	    case unop::F:
1140
1141
1142
1143
1144
	      // F(constant) = constant is a trivial identity, but if
	      // the constant has been constructed by recurse() this
	      // identity has not been applied.
	      if (is_constant(result_))
		  return;
1145
1146
1147
1148
1149

	      // If f is a pure eventuality formula then F(f)=f.
	      if (opt_.event_univ && result_->is_eventual())
		return;

1150
1151
1152
	      if (opt_.reduce_basics)
		{
		  // F(a U b) = F(b)
1153
		  const binop* bo = is_U(result_);
1154
1155
		  if (bo)
		    {
1156
		      const formula* r =
1157
1158
1159
1160
1161
			unop::instance(unop::F, bo->second()->clone());
		      bo->destroy();
		      result_ = recurse_destroy(r);
		      return;
		    }
1162

1163
1164
1165
1166
		  // F(a M b) = F(a & b)
		  bo = is_M(result_);
		  if (bo)
		    {
1167
		      const formula* r =
1168
1169
1170
1171
1172
1173
1174
1175
1176
			unop::instance(unop::F,
				       multop::instance(multop::And,
							bo->first()->clone(),
							bo->second()->clone()));
		      bo->destroy();
		      result_ = recurse_destroy(r);
		      return;
		    }

1177
		  // FX(a) = XF(a)
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
		  if (const unop* u = is_X(result_))
		    {
		      const formula* res =
			unop_unop(unop::X, unop::F, u->child()->clone());
		      u->destroy();
		      // FXX(a) = XXF(a) ...
		      // FXG(a) = XFG(a) = FG(a) ...
		      result_ = recurse_destroy(res);
		      return;
		    }
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228

		  // FG(a & Xb) = FG(a & b)
		  // FG(a & Gb) = FG(a & b)
		  if (const unop* g = is_G(result_))
		    if (const multop* m = is_And(g->child()))
		      if (!m->is_boolean())
			{
			  m->clone();
			  mospliter s(mospliter::Strip_G | mospliter::Strip_X,
				      m, c_);
			  if (!s.res_G->empty() || !s.res_X->empty())
			    {
			      result_->destroy();
			      s.res_other->insert(s.res_other->begin(),
						  s.res_G->begin(),
						  s.res_G->end());
			      delete s.res_G;
			      s.res_other->insert(s.res_other->begin(),
						  s.res_X->begin(),
						  s.res_X->end());
			      delete s.res_X;
			      const formula* in =
				multop::instance(multop::And, s.res_other);
			      result_ =
				recurse_destroy(unop_unop(unop::F, unop::G,
							  in));
			      return;
			    }
			  else
			    {
			      for (multop::vec::iterator j =
				     s.res_other->begin();
				   j != s.res_other->end(); ++j)
				if (*j)
				  (*j)->destroy();
			      delete s.res_other;
			      delete s.res_G;
			      delete s.res_X;
			      // and continue...
			    }
			}
1229
		}
1230
1231
1232
1233
1234

	      // if Fa => a, keep a.
	      if (opt_.containment_checks_stronger
		  && c_->lcc.contained(uo, result_))
		return;
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250

	      // Disabled: F(f1 & GF(f2)) = F(f1) & GF(f2)
	      //
	      // As is, these two formulae are translated into
	      // equivalent Büchi automata so the rewriting is
	      // useless.
	      //
	      // However when taken in a larger formula such as F(f1
	      // & GF(f2)) | F(a & GF(b)), this rewriting used to
	      // produce (F(f1) & GF(f2)) | (F(a) & GF(b)), missing
	      // the opportunity to apply the F(E1)|F(E2) = F(E1|E2)
	      // rule which really helps the translation. F((f1 &
	      // GF(f2)) | (a & GF(b))) is indeed easier to translate.
	      //
	      // So let's not consider this rewriting rule.
	      break;
1251
1252

	    case unop::G:
1253
1254
1255
1256
1257
	      // G(constant) = constant is a trivial identity, but if
	      // the constant has been constructed by recurse() this
	      // identity has not been applied.
	      if (is_constant(result_))
		  return;
1258

1259
1260
1261
1262
	      // If f is a pure universality formula then G(f)=f.
	      if (opt_.event_univ && result_->is_universal())
		return;

1263
	      if (opt_.reduce_basics)
1264
		{
1265
		  // G(a R b) = G(b)
1266
		  const binop* bo = is_R(result_);
1267
		  if (bo)
1268
		    {
1269
		      const formula* r =
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
			unop::instance(unop::G, bo->second()->clone());
		      bo->destroy();
		      result_ = recurse_destroy(r);
		      return;
		    }

		  // G(a W b) = G(a | b)
		  bo = is_W(result_);
		  if (bo)
		    {
1280
		      const formula* r =
1281
1282
1283
1284
1285
1286
1287
			unop::instance(unop::G,
				       multop::instance(multop::Or,
							bo->first()->clone(),
							bo->second()->clone()));
		      bo->destroy();
		      result_ = recurse_destroy(r);
		      return;
1288
1289
		    }

1290
		  // GX(a) = XG(a)
1291
		  if (const unop* u = is_X(result_))
1292
		    {
1293
1294
1295
1296
1297
1298
1299
		      const formula* res =
			unop_unop(unop::X, unop::G, u->child()->clone());
		      u->destroy();
		      // GXX(a) = XXG(a) ...
		      // GXF(a) = XGF(a) = GF(a) ...
		      result_ = recurse_destroy(res);
		      return;
1300
1301
		    }

1302
1303
1304
		  // G(f1|f2|GF(f3)|GF(f4)|f5|f6) =
		  //                        G(f1|f2) | GF(f3|f4) | f5 | f6
		  // if f5 and f6 are both eventual and universal.
1305
		  if (const multop* mo = is_Or(result_))
1306
		    {
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
		      mo->clone();
		      mospliter s(mospliter::Strip_GF |
				  mospliter::Split_EventUniv,
				  mo, c_);
		      s.res_EventUniv->
			push_back(unop_multop(unop::G, multop::Or,
					      s.res_other));
		      s.res_EventUniv->
			push_back(unop_unop_multop(unop::G, unop::F,
						   multop::Or, s.res_GF));
		      result_ = multop::instance(multop::Or,
						 s.res_EventUniv);
		      if (result_ != uo)
1320
			{
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
			  mo->destroy();
			  result_ = recurse_destroy(result_);
			  return;
			}
		      else
			{
			  // Revert to the previous value of result_,
			  // for the next simplification.
			  result_->destroy();
			  result_ = mo;
1331
			}
1332
		    }
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373

		  // GF(a | Xb) = GF(a | b)
		  // GF(a | Fb) = GF(a | b)
		  if (const unop* f = is_F(result_))
		    if (const multop* m = is_Or(f->child()))
		      if (!m->is_boolean())
			{
			  m->clone();
			  mospliter s(mospliter::Strip_F | mospliter::Strip_X,
				      m, c_);
			  if (!s.res_F->empty() || !s.res_X->empty())
			    {
			      result_->destroy();
			      s.res_other->insert(s.res_other->begin(),
						  s.res_F->begin(),
						  s.res_F->end());
			      delete s.res_F;
			      s.res_other->insert(s.res_other->begin(),
						  s.res_X->begin(),
						  s.res_X->end());
			      delete s.res_X;
			      const formula* in =
				multop::instance(multop::Or, s.res_other);
			      result_ =
				recurse_destroy(unop_unop(unop::G, unop::F,
							  in));
			      return;
			    }
			  else
			    {
			      for (multop::vec::iterator j =
				     s.res_other->begin();
				   j != s.res_other->end(); ++j)
				if (*j)
				  (*j)->destroy();
			      delete s.res_other;
			      delete s.res_F;
			      delete s.res_X;
			      // and continue...
			    }
			}
1374
		}
1375
1376
1377
1378
	      // if a => Ga, keep a.
	      if (opt_.containment_checks_stronger
		  && c_->lcc.contained(result_, uo))
		return;
1379
	      break;
1380
1381
	    case unop::Closure:
	    case unop::NegClosure:
1382
	    case unop::NegClosureMarked:
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
	      // {e} = 1 if e accepts [*0]
	      // !{e} = 0 if e accepts [*0]
	      if (result_->accepts_eword())
		{
		  result_->destroy();
		  result_ = ((op == unop::Closure)
			     ? constant::true_instance()
			     : constant::false_instance());
		  return;
		}
1393
	      if (!opt_.reduce_size_strictly)
1394
		if (const multop* mo = is_OrRat(result_))
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
		  {
		    //  {a₁|a₂} =  {a₁}| {a₂}
		    // !{a₁|a₂} = !{a₁}&!{a₂}
		    unsigned s = mo->size();
		    multop::vec* v = new multop::vec;
		    for (unsigned n = 0; n < s; ++n)
		      v->push_back(unop::instance(op, mo->nth(n)->clone()));
		    mo->destroy();
		    result_ =
		      recurse_destroy(multop::instance(op == unop::Closure
						       ? multop::Or
						       : multop::And, v));
		    return;
		  }
1409
	      if (const multop* mo = is_Concat(result_))
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
		{
		  unsigned end = mo->size() - 1;
		  // {b₁;b₂;b₃*;e₁;f₁;e₂;f₂;e₂;e₃;e₄}
		  //    = b₁&X(b₂&X(b₃ W {e₁;f₁;e₂;f₂}))
		  // !{b₁;b₂;b₃*;e₁;f₁;e₂;f₂;e₂;e₃;e₄}
		  //    = !b₁|X(!b₂|X(!b₃ M !{e₁;f₁;e₂;f₂}))
		  // if e denotes a term that accepts [*0]
		  // and b denotes a Boolean formula.
		  while (mo->nth(end)->accepts_eword())
		    --end;
		  unsigned start = 0;
		  while (start <= end)
		    {
1423
1424
		      const formula* r = mo->nth(start);
		      const bunop* es = is_KleenStar(r);
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
		      if ((r->is_boolean() && !opt_.reduce_size_strictly)
			  || (es && es->child()->is_boolean()))
			++start;
		      else
			break;
		    }
		  unsigned s = end + 1 - start;
		  if (s != mo->size())
		    {
		      multop::vec* v = new multop::vec;
		      v->reserve(s);
		      for (unsigned n = start; n <= end; ++n)
			v->push_back(mo->nth(n)->clone());
1438
1439
		      const formula* tail =
			multop::instance(multop::Concat, v);
1440
1441
		      tail = unop::instance(op, tail);

1442
		      bool doneg = op != unop::Closure;
1443
1444
1445
		      for (unsigned n = start; n > 0;)
			{
			  --n;
1446
			  const formula* e = mo->nth(n);
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
			  // {b;f} = b & X{f}
			  // !{b;f} = !b | X!{f}
			  if (e->is_boolean())
			    {
			      tail = unop::instance(unop::X, tail);
			      e->clone();
			      if (doneg)
				tail =
				  multop::instance(multop::Or,
						   unop::instance(unop::Not, e),
						   tail);
			      else
				tail =
				  multop::instance(multop::And, e, tail);
			    }
			  // {b*;f} = b W {f}
			  // !{b*;f} = !b M !{f}
			  else
			    {
1466
			      const bunop* es = is_KleenStar(e);
1467
			      assert(es);
1468
			      const formula* c = es->child()->clone();
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
			      if (doneg)
				tail =
				  binop::instance(binop::M,
						  unop::instance(unop::Not, c),