simplify.cc 106 KB
Newer Older
1
2
// Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE).
3
4
5
6
7
//
// 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
8
// the Free Software Foundation; either version 3 of the License, or
9
10
11
12
13
14
15
16
17
18
19
20
// (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 Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

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

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

namespace spot
{
  namespace ltl
  {

43

44
45
46
47
48
49
50
    // 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;
51
52
      typedef std::pair<const formula*, const formula*> pairf;
      typedef std::map<pairf, bool> syntimpl_cache_t;
53
    public:
54
      bdd_dict* dict;
55
      ltl_simplifier_options options;
56
      language_containment_checker lcc;
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
88

      ~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();
	    }
	}
89
90
91
92
93
94
95
96
97
98
	{
	  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();
	    }
	}
99
100
101
102
103
104
105
106
107
108
	{
	  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();
	    }
	}
109

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

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

118
119
      ltl_simplifier_cache(bdd_dict* d, ltl_simplifier_options opt)
	: dict(d), options(opt), lcc(d, true, true, false, false)
120
      {
121
	opt.containment_checks |= opt.containment_checks_stronger;
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
      }

      // 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())
141
	      result = bddfalse;
142
143
144
145
	    else
	      assert(!"Unsupported operator");
	    break;
	  case formula::AtomicProp:
146
	    result = bdd_ithvar(dict->register_proposition(f, this));
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
	    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;
		  }
197
		case multop::AndNLM:
198
199
		case multop::AndRat:
		case multop::OrRat:
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
		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();
      }

233
234
235
236
237
238
239
240
241
242
      // 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)
      {
	return (options.synt_impl && syntactic_implication(f1, f2))
	  || (options.containment_checks && contained(f1, f2));
      }

      // Return true if f1 => f2 syntactically
243
      bool
244
      syntactic_implication(const formula* f1, const formula* f2);
245
246
      bool
      syntactic_implication_aux(const formula* f1, const formula* f2);
247

248
249
250
      // Return true if f1 => f2
      bool
      contained(const formula* f1, const formula* f2)
251
      {
252
253
254
255
256
257
258
259
	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
260
261
      syntactic_implication_neg(const formula* f1, const formula* f2,
				bool right);
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
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

      // 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;
	  }
324
325
      }

326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
      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();
      }

341
342
343
344
345
346
      const formula*
      star_normal_form(const formula* f)
      {
	return ltl::star_normal_form(f, &snf_cache_);
      }

347
348
349
350
    private:
      f2b_map as_bdd_;
      f2f_map simplified_;
      f2f_map nenoform_;
351
      syntimpl_cache_t syntimpl_;
352
      snf_cache snf_cache_;
353
354
355
356
357
    };


    namespace
    {
358
359
360
361
362
363
      //////////////////////////////////////////////////////////////////////
      //
      //  NEGATIVE_NORMAL_FORM_VISITOR
      //
      //////////////////////////////////////////////////////////////////////

364
365
366
367
368
369
370
371
372
      // Forward declaration.
      const formula*
      nenoform_recursively(const formula* f,
			   bool negated,
			   ltl_simplifier_cache* c);

      class negative_normal_form_visitor: public visitor
      {
      public:
373
374
	negative_normal_form_visitor(bool negated, ltl_simplifier_cache* c)
	  : negated_(negated), cache_(c)
375
376
377
378
379
380
381
382
	{
	}

	virtual
	~negative_normal_form_visitor()
	{
	}

383
	const formula* result() const
384
385
386
387
388
	{
	  return result_;
	}

	void
389
	visit(const atomic_prop* ap)
390
	{
391
	  const formula* f = ap->clone();
392
393
394
395
396
397
398
	  if (negated_)
	    result_ = unop::instance(unop::Not, f);
	  else
	    result_ = f;
	}

	void
399
	visit(const constant* c)
400
401
402
403
404
405
406
407
408
409
	{
	  // 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
410
	visit(const unop* uo)
411
	{
412
	  const formula* f = uo->child();
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
	  switch (uo->op())
	    {
	    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:
	      result_ = unop::instance(negated_ ?
				       unop::Closure : uo->op(),
				       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
456
	visit(const bunop* bo)
457
	{
458
459
	  // !(a*) should never occur.
	  assert(!negated_);
460
461
462
463
	  result_ = bunop::instance(bo->op(), recurse_(bo->child(), false),
				    bo->min(), bo->max());
	}

464
465
466
	const formula* equiv_or_xor(bool equiv,
				    const formula* f1,
				    const formula* f2)
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
	{
	  // 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)));
	}

490
	void
491
	visit(const binop* bo)
492
	{
493
494
	  const formula* f1 = bo->first();
	  const formula* f2 = bo->second();
495
496
497
	  switch (bo->op())
	    {
	    case binop::Xor:
498
499
	      // !(a ^ b) == a <=> b
	      result_ = equiv_or_xor(negated_, f1, f2);
500
501
	      return;
	    case binop::Equiv:
502
503
	      // !(a <=> b) == a ^ b
	      result_ = equiv_or_xor(!negated_, f1, f2);
504
505
506
	      return;
	    case binop::Implies:
	      if (negated_)
507
		// !(a => b) == a & !b
508
509
510
		result_ = multop::instance(multop::And,
					   recurse_(f1, false),
					   recurse_(f2, true));
511
512
513
514
	      else // a => b == !a | b
		result_ = multop::instance(multop::Or,
					   recurse_(f1, true),
					   recurse_(f2, false));
515
516
	      return;
	    case binop::U:
517
	      // !(a U b) == !a R !b
518
519
520
521
	      result_ = binop::instance(negated_ ? binop::R : binop::U,
					recurse(f1), recurse(f2));
	      return;
	    case binop::R:
522
	      // !(a R b) == !a U !b
523
524
525
526
	      result_ = binop::instance(negated_ ? binop::U : binop::R,
					recurse(f1), recurse(f2));
	      return;
	    case binop::W:
527
	      // !(a W b) == !a M !b
528
529
530
531
	      result_ = binop::instance(negated_ ? binop::M : binop::W,
					recurse(f1), recurse(f2));
	      return;
	    case binop::M:
532
	      // !(a M b) == !a W !b
533
534
535
536
	      result_ = binop::instance(negated_ ? binop::W : binop::M,
					recurse(f1), recurse(f2));
	      return;
	    case binop::UConcat:
537
	      // !(a []-> b) == a<>-> !b
538
539
540
541
542
	      result_ = binop::instance(negated_ ?
					binop::EConcat : binop::UConcat,
					recurse_(f1, false), recurse(f2));
	      return;
	    case binop::EConcat:
543
	      // !(a <>-> b) == a[]-> !b
544
545
546
547
548
	      result_ = binop::instance(negated_ ?
					binop::UConcat : binop::EConcat,
					recurse_(f1, false), recurse(f2));
	      return;
	    case binop::EConcatMarked:
549
	      // !(a <>-> b) == a[]-> !b
550
551
552
553
554
555
	      result_ = binop::instance(negated_ ?
					binop::UConcat :
					binop::EConcatMarked,
					recurse_(f1, false), recurse(f2));
	      return;
	    }
556
	  // Unreachable code.
557
558
559
560
	  assert(0);
	}

	void
561
	visit(const automatop* ao)
562
563
564
565
566
567
568
569
570
571
572
	{
	  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
573
	visit(const multop* mo)
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
	{
	  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:
590
591
	      case multop::OrRat:
	      case multop::AndRat:
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
		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:
609
610
	    case multop::AndRat:
	    case multop::OrRat:
611
612
613
614
615
616
617
618
619
	      {
		for (unsigned i = 0; i < mos; ++i)
		  res->push_back(recurse_(mo->nth(i), false));
		result_ = multop::instance(op, res);
		assert(!negated_);
	      }
	    }
	}

620
621
	const formula*
	recurse_(const formula* f, bool negated)
622
	{
623
	  return nenoform_recursively(f, negated, cache_);
624
625
	}

626
627
	const formula*
	recurse(const formula* f)
628
629
630
631
632
	{
	  return recurse_(f, negated_);
	}

      protected:
633
	const formula* result_;
634
635
636
637
638
639
640
641
642
643
	bool negated_;
	ltl_simplifier_cache* cache_;
      };


      const formula*
      nenoform_recursively(const formula* f,
			   bool negated,
			   ltl_simplifier_cache* c)
      {
644
	if (const unop* uo = is_Not(f))
645
	  {
646
647
	    negated = !negated;
	    f = uo->child();
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
	  }

	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
	  {
664
	    negative_normal_form_visitor v(negated, c);
665
	    f->accept(v);
666
667
668
669
670
671
672
673
674
675
676
	    result = v.result();
	  }

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

	return result;
      }

677
678
679
680
681
682
      //////////////////////////////////////////////////////////////////////
      //
      //  SIMPLIFY_VISITOR
      //
      //////////////////////////////////////////////////////////////////////

683
      // Forward declaration.
684
      const formula*
685
      simplify_recursively(const formula* f, ltl_simplifier_cache* c);
686

687

688

689
690
      // X(a) R b   or   X(a) M b
      // This returns a.
691
692
      const formula*
      is_XRM(const formula* f)
693
      {
694
	const binop* bo = is_binop(f, binop::R, binop::M);
695
	if (!bo)
696
	  return 0;
697
	const unop* uo = is_X(bo->first());
698
699
700
701
702
703
704
	if (!uo)
	  return 0;
	return uo->child();
      }

      // X(a) W b   or   X(a) U b
      // This returns a.
705
706
      const formula*
      is_XWU(const formula* f)
707
      {
708
	const binop* bo = is_binop(f, binop::W, binop::U);
709
	if (!bo)
710
	  return 0;
711
	const unop* uo = is_X(bo->first());
712
713
714
715
716
	if (!uo)
	  return 0;
	return uo->child();
      }

717
718
      // b & X(b W a)  or   b & X(b U a)
      // This returns (b W a) or (b U a).
719
720
      const binop*
      is_bXbWU(const formula* f)
721
      {
722
	const multop* mo = is_multop(f, multop::And);
723
724
725
726
727
	if (!mo)
	  return 0;
	unsigned s = mo->size();
	for (unsigned pos = 0; pos < s; ++pos)
	  {
728
	    const unop* u = is_X(mo->nth(pos));
729
730
	    if (!u)
	      continue;
731
	    const binop* bo = is_binop(u->child(), binop::U, binop::W);
732
733
	    if (!bo)
	      continue;
734
	    const formula* b = mo->all_but(pos);
735
736
737
738
739
740
741
742
743
744
	    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).
745
746
      const binop*
      is_bXbRM(const formula* f)
747
      {
748
	const multop* mo = is_multop(f, multop::Or);
749
750
751
752
753
	if (!mo)
	  return 0;
	unsigned s = mo->size();
	for (unsigned pos = 0; pos < s; ++pos)
	  {
754
	    const unop* u = is_X(mo->nth(pos));
755
756
	    if (!u)
	      continue;
757
	    const binop* bo = is_binop(u->child(), binop::R, binop::M);
758
759
	    if (!bo)
	      continue;
760
	    const formula* b = mo->all_but(pos);
761
762
763
764
765
766
767
768
	    bool result = (b == bo->first());
	    b->destroy();
	    if (result)
	      return bo;
	  }
	return 0;
      }

769
      const formula*
770
771
772
773
774
      unop_multop(unop::type uop, multop::type mop, multop::vec* v)
      {
	return unop::instance(uop, multop::instance(mop, v));
      }

775
      const formula*
776
777
778
779
780
781
      unop_unop_multop(unop::type uop1, unop::type uop2, multop::type mop,
		       multop::vec* v)
      {
	return unop::instance(uop1, unop_multop(uop2, mop, v));
      }

782
783
      const formula*
      unop_unop(unop::type uop1, unop::type uop2, const formula* f)
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
      {
	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),
802
803
804
		    Split_Event = (1 << 12),
		    Split_Univ = (1 << 13),
		    Split_Bool = (1 << 14)
805
806
807
808
809
810
811
812
813
814
815
	};

	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;
816
817
818
	  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;
819
820
821
822
	  res_Bool = (split_ & Split_Bool) ? new multop::vec : 0;
	  res_other = new multop::vec;
	}

823
	void process(const formula* f)
824
825
826
827
828
	{
	  switch (f->kind())
	    {
	    case formula::UnOp:
	      {
829
830
		const unop* uo = static_cast<const unop*>(f);
		const formula* c = uo->child();
831
832
833
834
		switch (uo->op())
		  {
		  case unop::X:
		    if (res_X)
835
836
837
838
		      {
			res_X->push_back(c->clone());
			return;
		      }
839
840
841
		    break;
		  case unop::F:
		    if (res_FG)
842
843
844
845
846
847
		      if (const unop* cc = is_G(c))
			{
			  res_FG->push_back(((split_ & Strip_FG) == Strip_FG
					     ? cc->child() : f)->clone());
			  return;
			}
848
		    if (res_F)
849
850
851
852
853
		      {
			res_F->push_back(((split_ & Strip_F) == Strip_F
					  ? c : f)->clone());
			return;
		      }
854
855
856
		    break;
		  case unop::G:
		    if (res_GF)
857
858
859
860
861
862
		      if (const unop* cc = is_F(c))
			{
			  res_GF->push_back(((split_ & Strip_GF) == Strip_GF
					     ? cc->child() : f)->clone());
			  return;
			}
863
		    if (res_G)
864
865
866
867
868
		      {
			res_G->push_back(((split_ & Strip_G) == Strip_G
					  ? c : f)->clone());
			return;
		      }
869
870
871
872
873
874
875
876
		    break;
		  default:
		    break;
		  }
	      }
	      break;
	    case formula::BinOp:
	      {
877
		const binop* bo = static_cast<const binop*>(f);
878
879
880
881
882
		switch (bo->op())
		  {
		  case binop::U:
		  case binop::W:
		    if (res_U_or_W)
883
884
885
886
		      {
			res_U_or_W->push_back(bo->clone());
			return;
		      }
887
888
889
890
		    break;
		  case binop::R:
		  case binop::M:
		    if (res_R_or_M)
891
892
893
894
		      {
			res_R_or_M->push_back(bo->clone());
			return;
		      }
895
896
897
898
899
900
901
902
		    break;
		  default:
		    break;
		  }
	      }
	      break;
	    default:
	      if (res_Bool && f->is_boolean())
903
904
905
906
		{
		  res_Bool->push_back(f->clone());
		  return;
		}
907
908
	      break;
	    }
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
	  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());
931
932
	}

933
934
	mospliter(unsigned split, multop::vec* v, ltl_simplifier_cache* cache)
	  : split_(split), c_(cache)
935
936
937
938
939
	{
	  init();
	  multop::vec::const_iterator end = v->end();
	  for (multop::vec::const_iterator i = v->begin(); i < end; ++i)
	    {
940
941
942
943
944
	      if (*i) // skip null pointers left by previous simplifications
		{
		  process(*i);
		  (*i)->destroy();
		}
945
946
947
948
	    }
	  delete v;
	}

949
950
	mospliter(unsigned split, const multop* mo,
		  ltl_simplifier_cache* cache)
951
	  : split_(split), c_(cache)
952
953
954
955
956
	{
	  init();
	  unsigned mos = mo->size();
	  for (unsigned i = 0; i < mos; ++i)
	    {
957
	      const formula* f = simplify_recursively(mo->nth(i), cache);
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
	      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_;
977
	ltl_simplifier_cache* c_;
978
979
      };

980
981
982
      class simplify_visitor: public visitor
      {
      public:
983

984
985
986
987
	simplify_visitor(ltl_simplifier_cache* cache)
	  : c_(cache), opt_(cache->options)
	{
	}
988

989
990
991
992
	virtual ~simplify_visitor()
	{
	}

993
	const formula*
994
995
996
997
998
999
	result() const
	{
	  return result_;
	}

	void
1000
	visit(const atomic_prop* ap)