formula.hh 38 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2015 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
19

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
20
/// \file tl/formula.hh
21
/// \brief LTL/PSL formula interface
22
#pragma once
23

24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
/// \defgroup tl Temporal Logic
///
/// Spot supports the future-time fragment of LTL, and the linear-time
/// fragment of and PSL formulas.  The former is included in the
/// latter.  Both types of formulas are represented by instances of
/// the spot::formula class.

/// \addtogroup tl_essentials Essential Temporal Logic Types
/// \ingroup tl

/// \addtogroup tl_io Input and Output of Formulas
/// \ingroup tl

/// \addtogroup tl_rewriting Rewriting Algorithms for Formulas
/// \ingroup tl

/// \addtogroup tl_misc Miscellaneous Algorithms for Formulas
/// \ingroup tl

43
#include <spot/misc/common.hh>
44
45
46
#include <memory>
#include <cstdint>
#include <initializer_list>
47
#include <cassert>
48
49
50
51
52
#include <vector>
#include <string>
#include <iterator>
#include <iosfwd>
#include <sstream>
53
#include <list>
54
55
#include <cstddef>
#include <initializer_list>
56
#include <limits>
57

58
namespace spot
59
{
60
61
  /// \ingroup tl_essentials
  /// \brief Operator types
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
62
  enum class op: uint8_t
63
  {
64
65
66
67
    ff,				///< False
      tt,			///< True
      eword,			///< Empty word
      ap,                   	///< Atomic proposition
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
68
    // unary operators
69
70
71
72
73
74
75
      Not,			///< Negation
      X,			///< Next
      F,			///< Eventually
      G,			///< Globally
      Closure,			///< PSL Closure
      NegClosure,		///< Negated PSL Closure
      NegClosureMarked,		///< marked version of the Negated PSL Clusure
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
76
    // binary operators
77
78
79
      Xor,			///< Exclusive Or
      Implies,			///< Implication
      Equiv,			///< Equivalence
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
80
81
82
83
84
85
86
87
88
89
90
91
92
      U,		      ///< until
      R,		      ///< release (dual of until)
      W,		      ///< weak until
      M,		      ///< strong release (dual of weak until)
      EConcat,	      ///< Seq
      EConcatMarked,	      ///< Seq, Marked
      UConcat,	      ///< Triggers
    // n-ary operators
      Or,		      ///< (omega-Rational) Or
      OrRat,		      ///< Rational Or
      And,		      ///< (omega-Rational) And
      AndRat,		      ///< Rational And
      AndNLM,		      ///< Non-Length-Matching Rational-And
93
94
      Concat,		      ///< Concatenation
      Fusion,		      ///< Fusion
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
95
96
97
98
    // star-like operators
      Star,		      ///< Star
      FStar,		      ///< Fustion Star
      };
99

100
#ifndef SWIG
101
102
103
104
105
106
  /// \brief Actual storage for formula nodes.
  ///
  /// spot::formula objects contain references to instances of this
  /// class, and delegate most of their methods.  Because
  /// spot::formula is meant to be the public interface, most of the
  /// methods are documented there, rather than here.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
107
108
109
110
  class SPOT_API fnode final
  {
  public:
    const fnode* clone() const
111
    {
112
      // Saturate.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
113
      ++refs_;
114
115
      if (SPOT_UNLIKELY(!refs_))
	saturated_ = 1;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
116
117
      return this;
    }
118

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
119
120
    void destroy() const
    {
121
      if (SPOT_LIKELY(refs_))
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
122
	--refs_;
123
124
125
      else if (SPOT_LIKELY(id_ > 2) && SPOT_LIKELY(!saturated_))
	// last reference to a node that is not a constant
	destroy_aux();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
126
    }
127

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
128
129
130
131
    static constexpr uint8_t unbounded()
    {
      return UINT8_MAX;
    }
132

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
133
134
135
136
137
138
    static const fnode* ap(const std::string& name);
    static const fnode* unop(op o, const fnode* f);
    static const fnode* binop(op o, const fnode* f, const fnode* g);
    static const fnode* multop(op o, std::vector<const fnode*> l);
    static const fnode* bunop(op o, const fnode* f,
			      uint8_t min, uint8_t max = unbounded());
139

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
140
141
142
143
    op kind() const
    {
      return op_;
    }
144

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
145
    std::string kindstr() const;
146

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
147
148
149
150
    bool is(op o) const
    {
      return op_ == o;
    }
151

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
152
153
154
155
    bool is(op o1, op o2) const
    {
      return op_ == o1 || op_ == o2;
    }
156

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
157
158
159
160
161
162
163
164
165
166
167
    bool is(std::initializer_list<op> l) const
    {
      const fnode* n = this;
      for (auto o: l)
	{
	  if (!n->is(o))
	    return false;
	  n = n->nth(0);
	}
      return true;
    }
168

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
169
170
171
172
173
174
175
    const fnode* get_child_of(op o) const
    {
      if (op_ != o)
	return nullptr;
      assert(size_ == 1);
      return nth(0);
    }
176

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
177
178
179
180
181
182
183
184
185
186
187
    const fnode* get_child_of(std::initializer_list<op> l) const
    {
      auto c = this;
      for (auto o: l)
	{
	  c = c->get_child_of(o);
	  if (c == nullptr)
	    return c;
	}
      return c;
    }
188

189
    unsigned min() const
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
190
191
192
193
    {
      assert(op_ == op::FStar || op_ == op::Star);
      return min_;
    }
194

195
    unsigned max() const
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
196
197
198
199
    {
      assert(op_ == op::FStar || op_ == op::Star);
      return max_;
    }
200

201
    unsigned size() const
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
202
203
204
    {
      return size_;
    }
205

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
206
207
208
209
    size_t id() const
    {
      return id_;
    }
210

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
211
212
213
214
    const fnode*const* begin() const
    {
      return children;
    }
215

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
216
217
218
219
    const fnode*const* end() const
    {
      return children + size();
    }
220

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
221
222
223
224
225
226
    const fnode* nth(unsigned i) const
    {
      if (i >= size())
	throw std::runtime_error("access to non-existing child");
      return children[i];
    }
227

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
228
229
230
231
    static const fnode* ff()
    {
      return ff_;
    }
232

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
233
234
235
236
    bool is_ff() const
    {
      return op_ == op::ff;
    }
237

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
238
239
240
241
    static const fnode* tt()
    {
      return tt_;
    }
242

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
243
244
245
246
    bool is_tt() const
    {
      return op_ == op::tt;
    }
247

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
248
249
250
251
    static const fnode* eword()
    {
      return ew_;
    }
252

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
253
254
255
256
    bool is_eword() const
    {
      return op_ == op::eword;
    }
257

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
258
259
260
261
    bool is_constant() const
    {
      return op_ == op::ff || op_ == op::tt || op_ == op::eword;
    }
262

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
263
264
265
266
267
268
    bool is_Kleene_star() const
    {
      if (op_ != op::Star)
	return false;
      return min_ == 0 && max_ == unbounded();
    }
269

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
270
271
272
273
274
275
    static const fnode* one_star()
    {
      if (!one_star_)
	one_star_ = bunop(op::Star, tt(), 0);
      return one_star_;
    }
276

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
277
278
    const std::string& ap_name() const;
    std::ostream& dump(std::ostream& os) const;
279

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
280
    const fnode* all_but(unsigned i) const;
281

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
282
283
284
285
286
287
288
289
    unsigned boolean_count() const
    {
      unsigned pos = 0;
      unsigned s = size();
      while (pos < s && children[pos]->is_boolean())
	++pos;
      return pos;
    }
290

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
291
    const fnode* boolean_operands(unsigned* width = nullptr) const;
292

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
293
294
295
    /// return true if the unicity map contains only the globally
    /// pre-allocated formulas.
    static bool instances_check();
296

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
297
298
299
    ////////////////
    // Properties //
    ////////////////
300

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
301
302
303
304
    bool is_boolean() const
    {
      return is_.boolean;
    }
305

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
306
307
308
309
    bool is_sugar_free_boolean() const
    {
      return is_.sugar_free_boolean;
    }
310

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
311
312
313
314
    bool is_in_nenoform() const
    {
      return is_.in_nenoform;
    }
315

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
316
317
318
319
    bool is_syntactic_stutter_invariant() const
    {
      return is_.syntactic_si;
    }
320

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
321
322
323
324
    bool is_sugar_free_ltl() const
    {
      return is_.sugar_free_ltl;
    }
325

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
326
327
328
329
    bool is_ltl_formula() const
    {
      return is_.ltl_formula;
    }
330

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
331
332
333
334
    bool is_psl_formula() const
    {
      return is_.psl_formula;
    }
335

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
336
337
338
339
    bool is_sere_formula() const
    {
      return is_.sere_formula;
    }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
340

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
341
342
343
344
    bool is_finite() const
    {
      return is_.finite;
    }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
345

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
346
347
348
349
    bool is_eventual() const
    {
      return is_.eventual;
    }
350

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
351
352
353
354
    bool is_universal() const
    {
      return is_.universal;
    }
355

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
356
357
358
359
    bool is_syntactic_safety() const
    {
      return is_.syntactic_safety;
    }
360

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
361
362
363
364
    bool is_syntactic_guarantee() const
    {
      return is_.syntactic_guarantee;
    }
365

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
366
367
368
369
    bool is_syntactic_obligation() const
    {
      return is_.syntactic_obligation;
    }
370

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
371
372
373
374
    bool is_syntactic_recurrence() const
    {
      return is_.syntactic_recurrence;
    }
375

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
376
377
378
379
    bool is_syntactic_persistence() const
    {
      return is_.syntactic_persistence;
    }
380

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
381
382
383
384
    bool is_marked() const
    {
      return !is_.not_marked;
    }
385

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
386
387
388
389
    bool accepts_eword() const
    {
      return is_.accepting_eword;
    }
390

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
391
392
393
394
    bool has_lbt_atomic_props() const
    {
      return is_.lbt_atomic_props;
    }
395

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
396
397
398
399
    bool has_spin_atomic_props() const
    {
      return is_.spin_atomic_props;
    }
400

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
401
402
403
  private:
    void setup_props(op o);
    void destroy_aux() const;
404

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
405
    static const fnode* unique(const fnode*);
406

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
407
408
409
410
411
    // Destruction may only happen via destroy().
    ~fnode() = default;
    // Disallow copies.
    fnode(const fnode&) = delete;
    fnode& operator=(const fnode&) = delete;
412
413
414



Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
415
    template<class iter>
416
      fnode(op o, iter begin, iter end)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
417
418
419
420
421
422
423
424
425
426
    {
      size_t s = std::distance(begin, end);
      if (s > (size_t) UINT16_MAX)
	throw std::runtime_error("too many children for formula");
      size_ = s;
      auto pos = children;
      for (auto i = begin; i != end; ++i)
	*pos++ = *i;
      setup_props(o);
    }
427

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
428
429
    fnode(op o, std::initializer_list<const fnode*> l)
      : fnode(o, l.begin(), l.end())
430
      {
431
      }
432

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
433
    fnode(op o, const fnode* f, uint8_t min, uint8_t max)
434
      {
435
436
437
438
439
	size_ = 1;
	children[0] = f;
	min_ = min;
	max_ = max;
	setup_props(o);
440
      }
441

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
442
443
444
445
446
447
448
449
    static const fnode* ff_;
    static const fnode* tt_;
    static const fnode* ew_;
    static const fnode* one_star_;

    op op_;			// operator
    uint8_t min_;		// range minimum (for star-like operators)
    uint8_t max_;		// range maximum;
450
    mutable uint8_t saturated_ = 0;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
451
452
453
454
    uint16_t size_;		// number of children
    mutable uint16_t refs_ = 0; // reference count - 1;
    size_t id_;		// Also used as hash.
    static size_t next_id_;
455

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
    struct ltl_prop
    {
      // All properties here should be expressed in such a a way
      // that property(f && g) is just property(f)&property(g).
      // This allows us to compute all properties of a compound
      // formula in one operation.
      //
      // For instance we do not use a property that says "has
      // temporal operator", because it would require an OR between
      // the two arguments.  Instead we have a property that
      // says "no temporal operator", and that one is computed
      // with an AND between the arguments.
      //
      // Also choose a name that makes sense when prefixed with
      // "the formula is".
      bool boolean:1;		   // No temporal operators.
      bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
      bool in_nenoform:1;	   // Negative Normal Form.
      bool syntactic_si:1;	   // LTL-X or siPSL
      bool sugar_free_ltl:1;	   // No F and G operators.
      bool ltl_formula:1;	   // Only LTL operators.
      bool psl_formula:1;	   // Only PSL operators.
      bool sere_formula:1;	   // Only SERE operators.
      bool finite:1;		   // Finite SERE formulae, or Bool+X forms.
      bool eventual:1;	   // Purely eventual formula.
      bool universal:1;	   // Purely universal formula.
      bool syntactic_safety:1;   // Syntactic Safety Property.
      bool syntactic_guarantee:1;   // Syntactic Guarantee Property.
      bool syntactic_obligation:1;  // Syntactic Obligation Property.
      bool syntactic_recurrence:1;  // Syntactic Recurrence Property.
      bool syntactic_persistence:1; // Syntactic Persistence Property.
      bool not_marked:1;	   // No occurrence of EConcatMarked.
      bool accepting_eword:1;	   // Accepts the empty word.
      bool lbt_atomic_props:1;   // Use only atomic propositions like p42.
      bool spin_atomic_props:1;  // Use only spin-compatible atomic props.
    };
    union
    {
      // Use an unsigned for fast computation of all properties.
      unsigned props;
      ltl_prop is_;
497
    };
498

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
499
500
    const fnode* children[1];
  };
501

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
502
503
504
505
506
507
508
509
  /// Order two atomic propositions.
  SPOT_API
  int atomic_prop_cmp(const fnode* f, const fnode* g);

  struct formula_ptr_less_than_bool_first
  {
    bool
    operator()(const fnode* left, const fnode* right) const
510
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
      assert(left);
      assert(right);
      if (left == right)
	return false;

      // We want Boolean formulae first.
      bool lib = left->is_boolean();
      if (lib != right->is_boolean())
	return lib;

      // We have two Boolean formulae
      if (lib)
	{
	  bool lconst = left->is_constant();
	  if (lconst != right->is_constant())
	    return lconst;
	  if (!lconst)
	    {
	      auto get_literal = [](const fnode* f) -> const fnode*
		{
		  if (f->is(op::Not))
		    f = f->nth(0);
		  if (f->is(op::ap))
		    return f;
		  return nullptr;
		};
	      // Literals should come first
	      const fnode* litl = get_literal(left);
	      const fnode* litr = get_literal(right);
	      if (!litl != !litr)
		return litl;
	      if (litl)
		{
		  // And they should be sorted alphabetically
		  int cmp = atomic_prop_cmp(litl, litr);
		  if (cmp)
		    return cmp < 0;
		}
	    }
	}
551

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
      size_t l = left->id();
      size_t r = right->id();
      if (l != r)
	return l < r;
      // Because the hash code assigned to each formula is the
      // number of formulae constructed so far, it is very unlikely
      // that we will ever reach a case were two different formulae
      // have the same hash.  This will happen only ever with have
      // produced 256**sizeof(size_t) formulae (i.e. max_count has
      // looped back to 0 and started over).  In that case we can
      // order two formulas by looking at their text representation.
      // We could be more efficient and look at their AST, but it's
      // not worth the burden.  (Also ordering pointers is ruled out
      // because it breaks the determinism of the implementation.)
      std::ostringstream old;
      left->dump(old);
      std::ostringstream ord;
      right->dump(ord);
      return old.str() < ord.str();
    }
  };
573
574
575

#endif // SWIG

576
577
  /// \ingroup tl_essentials
  /// \brief Main class for temporal logic formula
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
578
579
580
581
582
583
  class SPOT_API formula final
  {
    const fnode* ptr_;
  public:
    explicit formula(const fnode* f) noexcept
      : ptr_(f)
584
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
585
    }
586

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
587
588
    formula(std::nullptr_t) noexcept
      : ptr_(nullptr)
589
590
591
      {
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
592
593
    formula() noexcept
      : ptr_(nullptr)
594
595
596
      {
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
597
598
    formula(const formula& f) noexcept
      : ptr_(f.ptr_)
599
600
601
602
603
      {
	if (ptr_)
	  ptr_->clone();
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
604
605
    formula(formula&& f) noexcept
      : ptr_(f.ptr_)
606
607
608
609
      {
	f.ptr_ = nullptr;
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
610
    ~formula()
611
612
613
614
615
      {
	if (ptr_)
	  ptr_->destroy();
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
616
    const formula& operator=(std::nullptr_t)
617
618
619
620
621
622
      {
	this->~formula();
	ptr_ = nullptr;
	return *this;
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
623
    const formula& operator=(const formula& f)
624
625
626
627
628
629
630
      {
	this->~formula();
	if ((ptr_ = f.ptr_))
	  ptr_->clone();
	return *this;
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
631
    const formula& operator=(formula&& f) noexcept
632
633
634
635
636
      {
	std::swap(f.ptr_, ptr_);
	return *this;
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
637
638
639
640
641
642
    bool operator<(const formula& other) const noexcept
    {
      if (SPOT_UNLIKELY(!other.ptr_))
	return false;
      if (SPOT_UNLIKELY(!ptr_))
	return true;
643
644
645
646
647
648
649
650
651
      if (id() < other.id())
	return true;
      if (id() > other.id())
	return false;
      // The case where id()==other.id() but ptr_ != other.ptr_ is
      // very unlikely (we would need to build more that UINT_MAX
      // formulas), so let's just compare pointer, and ignore the fact
      // that it may give some nondeterminism.
      return ptr_ < other.ptr_;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
652
    }
653

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
654
655
    bool operator<=(const formula& other) const noexcept
    {
656
      return *this == other || *this < other;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
657
    }
658

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
659
660
    bool operator>(const formula& other) const noexcept
    {
661
      return !(*this <= other);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
662
    }
663

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
664
665
    bool operator>=(const formula& other) const noexcept
    {
666
      return !(*this < other);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
667
    }
668

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
669
670
671
672
    bool operator==(const formula& other) const noexcept
    {
      return other.ptr_ == ptr_;
    }
673

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
674
675
676
677
    bool operator==(std::nullptr_t) const noexcept
    {
      return ptr_ == nullptr;
    }
678

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
679
680
681
682
    bool operator!=(const formula& other) const noexcept
    {
      return other.ptr_ != ptr_;
    }
683

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
684
685
686
687
    bool operator!=(std::nullptr_t) const noexcept
    {
      return ptr_ != nullptr;
    }
688

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
689
690
691
692
    operator bool() const
    {
      return ptr_ != nullptr;
    }
693

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
694
695
696
    /////////////////////////
    // Forwarded functions //
    /////////////////////////
697

698
    /// Unbounded constant to use as end of range for bounded operators.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
699
700
701
702
    static constexpr uint8_t unbounded()
    {
      return fnode::unbounded();
    }
703

704
    /// Build an atomic proposition.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
705
706
707
708
    static formula ap(const std::string& name)
    {
      return formula(fnode::ap(name));
    }
709

710
711
712
713
    /// \brief Build a unary operator.
    /// \pre \a o should be one of op::Not, op::X, op::F, op::G,
    /// op::Closure, op::NegClosure, op::NegClosureMarked.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
714
715
716
717
    static formula unop(op o, const formula& f)
    {
      return formula(fnode::unop(o, f.ptr_->clone()));
    }
718
719

#ifndef SWIG
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
720
721
722
723
    static formula unop(op o, formula&& f)
    {
      return formula(fnode::unop(o, f.to_node_()));
    }
724
#endif // !SWIG
725
    /// @}
726
727
728

#ifdef SWIG
#define SPOT_DEF_UNOP(Name)			\
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
729
730
731
732
    static formula Name(const formula& f)	\
    {						\
      return unop(op::Name, f);			\
    }
733
734
#else // !SWIG
#define SPOT_DEF_UNOP(Name)			\
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
735
736
737
738
739
740
741
742
    static formula Name(const formula& f)	\
    {						\
      return unop(op::Name, f);			\
    }						\
    static formula Name(formula&& f)		\
    {						\
      return unop(op::Name, std::move(f));	\
    }
743
#endif // !SWIG
744
745
    /// \brief Construct a negation
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
746
    SPOT_DEF_UNOP(Not);
747
748
749
750
    /// @}

    /// \brief Construct an X
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
751
    SPOT_DEF_UNOP(X);
752
753
754
755
    /// @}

    /// \brief Construct an F
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
756
    SPOT_DEF_UNOP(F);
757
758
759
760
    /// @}

    /// \brief Construct a G
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
761
    SPOT_DEF_UNOP(G);
762
763
764
765
    /// @}

    /// \brief Construct a PSL Closure
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
766
    SPOT_DEF_UNOP(Closure);
767
768
769
770
    /// @}

    /// \brief Construct a negated PSL Closure
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
771
    SPOT_DEF_UNOP(NegClosure);
772
773
774
775
    /// @}

    /// \brief Construct a marked negated PSL Closure
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
776
    SPOT_DEF_UNOP(NegClosureMarked);
777
    /// @}
778
779
#undef SPOT_DEF_UNOP

780
781
782
783
    /// \brief Construct a binary operator
    /// \pre \a o should be one of op::Xor, op::Implies, op::Equiv,
    /// op::U, op::R, op::W, op::M, op::EConcat, op::EConcatMarked,
    /// or op::UConcat.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
784
785
786
787
    static formula binop(op o, const formula& f, const formula& g)
    {
      return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
    }
788
789

#ifndef SWIG
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
790
791
792
793
    static formula binop(op o, const formula& f, formula&& g)
    {
      return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
    }
794

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
795
796
797
798
    static formula binop(op o, formula&& f, const formula& g)
    {
      return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
    }
799

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
800
801
802
803
    static formula binop(op o, formula&& f, formula&& g)
    {
      return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
    }
804
805
806
807
#endif //SWIG

#ifdef SWIG
#define SPOT_DEF_BINOP(Name)					\
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
808
809
810
811
    static formula Name(const formula& f, const formula& g)	\
    {								\
      return binop(op::Name, f, g);				\
    }
812
813
#else // !SWIG
#define SPOT_DEF_BINOP(Name)					\
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
    static formula Name(const formula& f, const formula& g)	\
    {								\
      return binop(op::Name, f, g);				\
    }								\
    static formula Name(const formula& f, formula&& g)		\
    {								\
      return binop(op::Name, f, std::move(g));			\
    }								\
    static formula Name(formula&& f, const formula& g)		\
    {								\
      return binop(op::Name, std::move(f), g);			\
    }								\
    static formula Name(formula&& f, formula&& g)		\
    {								\
      return binop(op::Name, std::move(f), std::move(g));	\
    }
830
#endif // !SWIG
831
832
    /// \brief Construct an Xor formula
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
833
    SPOT_DEF_BINOP(Xor);
834
835
836
837
    /// @}

    /// \brief Construct an Implies formula
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
838
    SPOT_DEF_BINOP(Implies);
839
840
841
842
    /// @}

    /// \brief Construct an Equiv formula
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
843
    SPOT_DEF_BINOP(Equiv);
844
845
846
847
    /// @}

    /// \brief Construct an U formula
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
848
    SPOT_DEF_BINOP(U);
849
850
851
852
    /// @}

    /// \brief Construct an R formula
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
853
    SPOT_DEF_BINOP(R);
854
855
856
857
    /// @}

    /// \brief Construct an W formula
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
858
    SPOT_DEF_BINOP(W);
859
860
861
862
    /// @}

    /// \brief Construct an < formula
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
863
    SPOT_DEF_BINOP(M);
864
865
866
867
    /// @}

    /// \brief Construct an <>-> PSL formula
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
868
    SPOT_DEF_BINOP(EConcat);
869
870
871
872
    /// @}

    /// \brief Construct a marked <>-> PSL formula
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
873
    SPOT_DEF_BINOP(EConcatMarked);
874
875
876
877
    /// @}

    /// \brief Construct an []-> PSL formula
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
878
    SPOT_DEF_BINOP(UConcat);
879
    /// @}
880
881
#undef SPOT_DEF_BINOP

882
883
884
885
886
    /// \brief Construct an n-ary operator
    ///
    /// \pre \a o should be one of op::Or, op::OrRat, op::And,
    /// op::AndRat, op::AndNLM, op::Concat, op::Fusion.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
887
888
889
890
891
892
893
894
895
    static formula multop(op o, const std::vector<formula>& l)
    {
      std::vector<const fnode*> tmp;
      tmp.reserve(l.size());
      for (auto f: l)
	if (f.ptr_)
	  tmp.push_back(f.ptr_->clone());
      return formula(fnode::multop(o, std::move(tmp)));
    }
896
897

#ifndef SWIG
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
898
899
900
901
902
903
904
905
906
    static formula multop(op o, std::vector<formula>&& l)
    {
      std::vector<const fnode*> tmp;
      tmp.reserve(l.size());
      for (auto f: l)
	if (f.ptr_)
	  tmp.push_back(f.to_node_());
      return formula(fnode::multop(o, std::move(tmp)));
    }
907
#endif // !SWIG
908
    /// @}
909
910

#ifdef SWIG
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
911
912
913
914
915
#define SPOT_DEF_MULTOP(Name)				\
    static formula Name(const std::vector<formula>& l)	\
    {							\
      return multop(op::Name, l);			\
    }
916
#else // !SWIG
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
917
918
919
920
921
922
923
924
925
926
#define SPOT_DEF_MULTOP(Name)				\
    static formula Name(const std::vector<formula>& l)	\
    {							\
      return multop(op::Name, l);			\
    }							\
							\
    static formula Name(std::vector<formula>&& l)	\
    {							\
      return multop(op::Name, std::move(l));		\
    }
927
#endif // !SWIG
928
929
    /// \brief Construct an Or formula.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
930
    SPOT_DEF_MULTOP(Or);
931
932
933
934
    /// @}

    /// \brief Construct an Or SERE.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
935
    SPOT_DEF_MULTOP(OrRat);
936
937
938
939
    /// @}

    /// \brief Construct an And formula.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
940
    SPOT_DEF_MULTOP(And);
941
942
943
944
    /// @}

    /// \brief Construct an And SERE.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
945
    SPOT_DEF_MULTOP(AndRat);
946
947
948
949
    /// @}

    /// \brief Construct a non-length-matching And SERE.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
950
    SPOT_DEF_MULTOP(AndNLM);
951
952
953
954
    /// @}

    /// \brief Construct a Concatenation SERE.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
955
    SPOT_DEF_MULTOP(Concat);
956
957
958
959
    /// @}

    /// \brief Construct a Fusion SERE.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
960
    SPOT_DEF_MULTOP(Fusion);
961
    /// @}
962
963
#undef SPOT_DEF_MULTOP

964
965
966
967
    /// \brief Define a bounded unary-operator (i.e. star-like)
    ///
    /// \pre \a o should be op::Star or op::FStar.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
968
969
970
971
972
973
    static formula bunop(op o, const formula& f,
			 uint8_t min = 0U,
			 uint8_t max = unbounded())
    {
      return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
    }
974
975

#ifndef SWIG
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
976
977
978
979
980
981
    static formula bunop(op o, formula&& f,
			 uint8_t min = 0U,
			 uint8_t max = unbounded())
    {
      return formula(fnode::bunop(o, f.to_node_(), min, max));
    }
982
#endif // !SWIG
983
    ///@}
984
985
986

#if SWIG
#define SPOT_DEF_BUNOP(Name)				\
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
987
988
989
990
991
992
    static formula Name(const formula& f,		\
			uint8_t min = 0U,		\
			uint8_t max = unbounded())	\
    {							\
      return bunop(op::Name, f, min, max);		\
    }
993
994
#else // !SWIG
#define SPOT_DEF_BUNOP(Name)				\
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
    static formula Name(const formula& f,		\
			uint8_t min = 0U,		\
			uint8_t max = unbounded())	\
    {							\
      return bunop(op::Name, f, min, max);		\
    }							\
    static formula Name(formula&& f,			\
			uint8_t min = 0U,		\
			uint8_t max = unbounded())	\
    {							\
      return bunop(op::Name, std::move(f), min, max);	\
    }
1007
#endif
1008
1009
    /// \brief Create SERE for f[*min..max]
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1010
    SPOT_DEF_BUNOP(Star);
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
    /// @}

    /// \brief Create SERE for f[:*min..max]
    ///
    /// This operator is a generalization of the (+) operator
    /// defined in the following paper.
    /** \verbatim
        @InProceedings{	  dax.09.atva,
	  author	= {Christian Dax and Felix Klaedtke and Stefan Leue},
	  title		= {Specification Languages for Stutter-Invariant Regular
			  Properties},
	  booktitle	= {Proceedings of the 7th International Symposium on
			  Automated Technology for Verification and Analysis
			  (ATVA'09)},
	  pages		= {244--254},
	  year		= {2009},
	  volume	= {5799},
	  series	= {Lecture Notes in Computer Science},
	  publisher	= {Springer-Verlag}
	}
	\endverbatim */
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1033
    SPOT_DEF_BUNOP(FStar);
1034
    /// @}
1035
1036
#undef SPOT_DEF_BUNOP

1037
1038
1039
1040
1041
    /// \brief Create a SERE equivalent to b[->min..max]
    ///
    /// The operator does not exist: it is handled as sugar by the parser
    /// and the printer.  This functions is used by the parser to create
    /// the equivalent SERE.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1042
    static formula sugar_goto(const formula& b, uint8_t min, uint8_t max);
1043

1044
1045
1046
1047
1048
    /// Create the SERE b[=min..max]
    ///
    /// The operator does not exist: it is handled as sugar by the parser
    /// and the printer.  This functions is used by the parser to create
    /// the equivalent SERE.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1049
    static formula sugar_equal(const formula& b, uint8_t min, uint8_t max);
1050
1051

#ifndef SWIG
1052
1053
1054
1055
1056
1057
1058
1059
1060
    /// \brief Return the underlying pointer to the formula.
    ///
    /// It is not recommended to call this function, which is
    /// mostly meant for internal use.
    ///
    /// By calling this function you take ownership of the fnode
    /// instance pointed by this formula instance, and should take
    /// care of calling its destroy() methods once you are done with
    /// it.  Otherwise the fnode will be leaked.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1061
1062
1063
1064
1065
1066
    const fnode* to_node_()
    {
      auto tmp = ptr_;
      ptr_ = nullptr;
      return tmp;
    }
1067
1068
#endif

1069
    /// Return top-most operator.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1070
1071
1072
1073
    op kind() const
    {
      return ptr_->kind();
    }
1074

1075
    /// Return the name of the top-most operator.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1076
1077
1078
1079
    std::string kindstr() const
    {
      return ptr_->kindstr();
    }
1080

1081
    /// Return true if the formula is of kind \a o.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1082
1083
1084
1085
    bool is(op o) const
    {
      return ptr_->is(o);
    }
1086

1087
#ifndef SWIG
1088
    /// Return true if the formula is of kind \a o1 or \a o2.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1089
1090
1091
1092
    bool is(op o1, op o2) const
    {
      return ptr_->is(o1, o2);
    }
1093

1094
    /// Return true if the formulas nests all the operators in \a l.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1095
1096
1097
1098
    bool is(std::initializer_list<op> l) const
    {
      return ptr_->is(l);
    }
1099
#endif
1100

1101
1102
1103
    /// \brief Remove operator \a o and return the child.
    ///
    /// This works only for unary operators.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1104
1105
1106
1107
1108
1109
1110
    formula get_child_of(op o) const
    {
      auto f = ptr_->get_child_of(o);
      if (f)
	f->clone();
      return formula(f);
    }
1111

1112
#ifndef SWIG
1113
1114
1115
1116
1117
1118
    /// \brief Remove all operators in \a l and return the child.
    ///
    /// This works only for a list of unary operators.
    /// For instance if \c f  is a formula for XG(a U b),
    /// then <code>f.get_child_of({op::X, op::G})</code>
    /// will return the subformula a U b.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1119
1120
1121
1122
1123
1124
1125
    formula get_child_of(std::initializer_list<op> l) const
    {
      auto f = ptr_->get_child_of(l);
      if (f)
	f->clone();
      return formula(f);
    }
1126
#endif
1127

1128
1129
1130
    /// \brief Return start of the range for star-like operators.
    ///
    /// \pre The formula should have kind op::Star or op::FStar.
1131
    unsigned min() const
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1132
1133
1134
    {
      return ptr_->min();
    }
1135

1136
1137
1138
    /// \brief Return end of the range for star-like operators.
    ///
    /// \pre The formula should have kind op::Star or op::FStar.
1139
    unsigned max() const
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1140
1141
1142
    {
      return ptr_->max();
    }
1143

1144
    /// Return the number of children.
1145
    unsigned size() const
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1146
1147
1148
    {
      return ptr_->size();
    }
1149

1150
1151
1152
1153
1154
1155
1156
1157
    /// \brief Return the id of a formula.
    ///
    /// Can be used as a hash number.
    ///
    /// The id is almost unique as it is an unsigned number
    /// incremented at each formula construction, and the unsigned may
    /// wrap around zero.  If this is used for ordering, make sure to
    /// deal with equality
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1158
1159
1160
1161
    size_t id() const
    {
      return ptr_->id();
    }
1162

1163
#ifndef SWIG
1164
    /// Allow iterating over children
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1165
1166
1167
1168
1169
1170
    class SPOT_API formula_child_iterator final
    {
      const fnode*const* ptr_;
    public:
      formula_child_iterator()
	: ptr_(nullptr)
1171
1172
1173
	{
	}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1174
1175
      formula_child_iterator(const fnode*const* f)
	: ptr_(f)
1176
1177
1178
	{
	}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1179
      bool operator==(formula_child_iterator o)
1180
      {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1181
	return ptr_ == o.ptr_;
1182
1183
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1184
      bool operator!=(formula_child_iterator o)
1185
      {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1186
	return ptr_ != o.ptr_;
1187
1188
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1189
      formula operator*()
1190
      {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1191
	return formula((*ptr_)->clone());
1192
1193
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1194
      formula_child_iterator operator++()
1195
      {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1196
1197
	++ptr_;
	return *this;
1198
1199
      }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1200
      formula_child_iterator operator++(int)
1201
      {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1202
1203
1204
	auto tmp = *this;
	++ptr_;
	return tmp;
1205
      }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1206
    };
1207

1208
    /// Allow iterating over children
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1209
1210
1211
1212
    formula_child_iterator begin() const
    {
      return ptr_->begin();
    }
1213

1214
    /// Allow iterating over children
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1215
1216
1217
1218
    formula_child_iterator end() const
    {
      return ptr_->end();
    }
Alexandre Duret-Lutz's avatar