formula.hh 42.7 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
80
81
82
83
84
85
86
    Xor,                       ///< Exclusive Or
    Implies,                   ///< Implication
    Equiv,                     ///< Equivalence
    U,                         ///< until
    R,                         ///< release (dual of until)
    W,                         ///< weak until
    M,                         ///< strong release (dual of weak until)
    EConcat,                   ///< Seq
    EConcatMarked,             ///< Seq, Marked
    UConcat,                   ///< Triggers
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
87
    // n-ary operators
88
89
90
91
92
93
94
    Or,                        ///< (omega-Rational) Or
    OrRat,                     ///< Rational Or
    And,                       ///< (omega-Rational) And
    AndRat,                    ///< Rational And
    AndNLM,                    ///< Non-Length-Matching Rational-And
    Concat,                    ///< Concatenation
    Fusion,                    ///< Fusion
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
95
    // star-like operators
96
97
98
    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
  class SPOT_API fnode final
  {
109
110
111
112
113
114
115
116
117
    public:
      const fnode* clone() const
      {
        // Saturate.
        ++refs_;
        if (SPOT_UNLIKELY(!refs_))
          saturated_ = 1;
        return this;
      }
118

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

128
129
130
131
      static constexpr uint8_t unbounded()
      {
        return UINT8_MAX;
      }
132

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

140
141
142
143
      op kind() const
      {
        return op_;
      }
144

145
      std::string kindstr() const;
146

147
148
149
150
      bool is(op o) const
      {
        return op_ == o;
      }
151

152
153
154
155
      bool is(op o1, op o2) const
      {
        return op_ == o1 || op_ == o2;
      }
156

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

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

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
190
191
192
193
      unsigned min() const
      {
        assert(op_ == op::FStar || op_ == op::Star);
        return min_;
      }
194

195
196
197
198
199
      unsigned max() const
      {
        assert(op_ == op::FStar || op_ == op::Star);
        return max_;
      }
200

201
202
203
204
      unsigned size() const
      {
        return size_;
      }
205

206
207
208
209
      size_t id() const
      {
        return id_;
      }
210

211
212
213
214
      const fnode*const* begin() const
      {
        return children;
      }
215

216
217
218
219
      const fnode*const* end() const
      {
        return children + size();
      }
220

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

228
229
230
231
      static const fnode* ff()
      {
        return ff_;
      }
232

233
234
235
236
      bool is_ff() const
      {
        return op_ == op::ff;
      }
237

238
239
240
241
      static const fnode* tt()
      {
        return tt_;
      }
242

243
244
245
246
      bool is_tt() const
      {
        return op_ == op::tt;
      }
247

248
249
250
251
      static const fnode* eword()
      {
        return ew_;
      }
252

253
254
255
256
      bool is_eword() const
      {
        return op_ == op::eword;
      }
257

258
259
260
261
      bool is_constant() const
      {
        return op_ == op::ff || op_ == op::tt || op_ == op::eword;
      }
262

263
264
265
266
267
268
      bool is_Kleene_star() const
      {
        if (op_ != op::Star)
          return false;
        return min_ == 0 && max_ == unbounded();
      }
269

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

277
278
      const std::string& ap_name() const;
      std::ostream& dump(std::ostream& os) const;
279

280
      const fnode* all_but(unsigned i) const;
281

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

291
      const fnode* boolean_operands(unsigned* width = nullptr) const;
292

293
294
295
      /// return true if the unicity map contains only the globally
      /// pre-allocated formulas.
      static bool instances_check();
296

297
298
299
      ////////////////
      // Properties //
      ////////////////
300

301
302
303
304
      bool is_boolean() const
      {
        return is_.boolean;
      }
305

306
307
308
309
      bool is_sugar_free_boolean() const
      {
        return is_.sugar_free_boolean;
      }
310

311
312
313
314
      bool is_in_nenoform() const
      {
        return is_.in_nenoform;
      }
315

316
317
318
319
      bool is_syntactic_stutter_invariant() const
      {
        return is_.syntactic_si;
      }
320

321
322
323
324
      bool is_sugar_free_ltl() const
      {
        return is_.sugar_free_ltl;
      }
325

326
327
328
329
      bool is_ltl_formula() const
      {
        return is_.ltl_formula;
      }
330

331
332
333
334
      bool is_psl_formula() const
      {
        return is_.psl_formula;
      }
335

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

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

346
347
348
349
      bool is_eventual() const
      {
        return is_.eventual;
      }
350

351
352
353
354
      bool is_universal() const
      {
        return is_.universal;
      }
355

356
357
358
359
      bool is_syntactic_safety() const
      {
        return is_.syntactic_safety;
      }
360

361
362
363
364
      bool is_syntactic_guarantee() const
      {
        return is_.syntactic_guarantee;
      }
365

366
367
368
369
      bool is_syntactic_obligation() const
      {
        return is_.syntactic_obligation;
      }
370

371
372
373
374
      bool is_syntactic_recurrence() const
      {
        return is_.syntactic_recurrence;
      }
375

376
377
378
379
      bool is_syntactic_persistence() const
      {
        return is_.syntactic_persistence;
      }
380

381
382
383
384
      bool is_marked() const
      {
        return !is_.not_marked;
      }
385

386
387
388
389
      bool accepts_eword() const
      {
        return is_.accepting_eword;
      }
390

391
392
393
394
      bool has_lbt_atomic_props() const
      {
        return is_.lbt_atomic_props;
      }
395

396
397
398
399
      bool has_spin_atomic_props() const
      {
        return is_.spin_atomic_props;
      }
400

401
402
403
    private:
      void setup_props(op o);
      void destroy_aux() const;
404

405
      static const fnode* unique(const fnode*);
406

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



415
416
417
418
419
420
421
422
423
424
425
426
      template<class iter>
        fnode(op o, iter begin, iter end)
        {
          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

428
429
      fnode(op o, std::initializer_list<const fnode*> l)
        : fnode(o, l.begin(), l.end())
430
      {
431
      }
432

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

442
443
444
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
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
497
      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;
      mutable uint8_t saturated_ = 0;
      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_;

      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_;
      };
498

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

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

  struct formula_ptr_less_than_bool_first
  {
    bool
509
510
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
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
      operator()(const fnode* left, const fnode* right) const
      {
        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;
            }
          }
        }

        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();
      }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
572
  };
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
  class SPOT_API formula final
  {
    const fnode* ptr_;
581
    public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
582
583
    explicit formula(const fnode* f) noexcept
      : ptr_(f)
584
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
        if (ptr_)
          ptr_->clone();
602
603
      }

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

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

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

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

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
637
638
639
    bool operator<(const formula& other) const noexcept
    {
      if (SPOT_UNLIKELY(!other.ptr_))
640
        return false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
641
      if (SPOT_UNLIKELY(!ptr_))
642
        return true;
643
      if (id() < other.id())
644
        return true;
645
      if (id() > other.id())
646
        return false;
647
648
649
650
651
      // 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

#ifdef SWIG
728
729
730
731
#define SPOT_DEF_UNOP(Name)                          \
    static formula Name(const formula& f)            \
    {                                                \
      return unop(op::Name, f);                      \
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
732
    }
733
#else // !SWIG
734
735
736
737
738
739
740
741
#define SPOT_DEF_UNOP(Name)                          \
    static formula Name(const formula& f)            \
    {                                                \
      return unop(op::Name, f);                      \
    }                                                \
    static formula Name(formula&& f)                 \
    {                                                \
      return unop(op::Name, std::move(f));           \
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
742
    }
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
#endif //SWIG

#ifdef SWIG
807
808
809
810
#define SPOT_DEF_BINOP(Name)                                         \
    static formula Name(const formula& f, const formula& g)          \
    {                                                                \
      return binop(op::Name, f, g);                                  \
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
811
    }
812
#else // !SWIG
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
#define SPOT_DEF_BINOP(Name)                                         \
    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));            \
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
829
    }
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
    static formula multop(op o, const std::vector<formula>& l)
    {
      std::vector<const fnode*> tmp;
      tmp.reserve(l.size());
      for (auto f: l)
892
893
        if (f.ptr_)
          tmp.push_back(f.ptr_->clone());
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
894
895
      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
    static formula multop(op o, std::vector<formula>&& l)
    {
      std::vector<const fnode*> tmp;
      tmp.reserve(l.size());
      for (auto f: l)
903
904
        if (f.ptr_)
          tmp.push_back(f.to_node_());
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
905
906
      return formula(fnode::multop(o, std::move(tmp)));
    }
907
#endif // !SWIG
908
    /// @}
909
910

#ifdef SWIG
911
912
913
914
#define SPOT_DEF_MULTOP(Name)                                \
    static formula Name(const std::vector<formula>& l)       \
    {                                                        \
      return multop(op::Name, l);                            \
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
915
    }
916
#else // !SWIG
917
918
919
920
921
922
923
924
925
#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));                 \
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
926
    }
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
    static formula bunop(op o, const formula& f,
969
970
        uint8_t min = 0U,
        uint8_t max = unbounded())
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
971
972
973
    {
      return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
    }
974
975

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

#if SWIG
986
987
988
989
990
991
#define SPOT_DEF_BUNOP(Name)                                \
    static formula Name(const formula& f,                   \
        uint8_t min = 0U,                                   \
        uint8_t max = unbounded())                          \
    {                                                       \
      return bunop(op::Name, f, min, max);                  \
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
992
    }
993
#else // !SWIG
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
#define SPOT_DEF_BUNOP(Name)                                \
    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);       \
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1006
    }
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
    /// @}

    /// \brief Create SERE for f[:*min..max]
    ///
    /// This operator is a generalization of the (+) operator
    /// defined in the following paper.
    /** \verbatim
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
      @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 */
1032
    /// @{
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
    formula get_child_of(op o) const
    {
      auto f = ptr_->get_child_of(o);
      if (f)
1108
        f->clone();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1109
1110
      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
    formula get_child_of(std::initializer_list<op> l) const
    {
      auto f = ptr_->get_child_of(l);
      if (f)
1123
        f->clone();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1124
1125
      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
    class SPOT_API formula_child_iterator final
    {
      const fnode*const* ptr_;
1168
      public:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1169
      formula_child_iterator()
1170
1171
1172
        : ptr_(nullptr)
      {
      }
1173

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