formula.hh 42.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
3
// 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
784
    /// \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
785
786
787
788
    static formula binop(op o, const formula& f, const formula& g)
    {
      return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
    }
789
790

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

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

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

807
808
809
#endif //SWIG

#ifdef SWIG
810
811
812
813
#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
814
    }
815
#else // !SWIG
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
#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
832
    }
833
#endif // !SWIG
834
835
    /// \brief Construct an Xor formula
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
836
    SPOT_DEF_BINOP(Xor);
837
838
839
840
    /// @}

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

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

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

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

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

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

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

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

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

885
886
887
888
889
    /// \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
890
891
892
893
894
    static formula multop(op o, const std::vector<formula>& l)
    {
      std::vector<const fnode*> tmp;
      tmp.reserve(l.size());
      for (auto f: l)
895
896
        if (f.ptr_)
          tmp.push_back(f.ptr_->clone());
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
897
898
      return formula(fnode::multop(o, std::move(tmp)));
    }
899
900

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

#ifdef SWIG
914
915
916
917
#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
918
    }
919
#else // !SWIG
920
921
922
923
924
925
926
927
928
#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
929
    }
930
#endif // !SWIG
931
932
    /// \brief Construct an Or formula.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
933
    SPOT_DEF_MULTOP(Or);
934
935
936
937
    /// @}

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

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

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

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

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

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

967
968
969
970
    /// \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
971
    static formula bunop(op o, const formula& f,
972
973
        uint8_t min = 0U,
        uint8_t max = unbounded())
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
974
975
976
    {
      return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
    }
977
978

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

#if SWIG
989
990
991
992
993
994
#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
995
    }
996
#else // !SWIG
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
#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
1009
    }
1010
#endif
1011
1012
    /// \brief Create SERE for f[*min..max]
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1013
    SPOT_DEF_BUNOP(Star);
1014
1015
1016
1017
1018
1019
1020
    /// @}

    /// \brief Create SERE for f[:*min..max]
    ///
    /// This operator is a generalization of the (+) operator
    /// defined in the following paper.
    /** \verbatim
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
      @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 */
1035
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1036
    SPOT_DEF_BUNOP(FStar);
1037
    /// @}
1038
1039
#undef SPOT_DEF_BUNOP

1040
1041
1042
1043
1044
    /// \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
1045
    static formula sugar_goto(const formula& b, uint8_t min, uint8_t max);
1046

1047
1048
1049
1050
1051
    /// 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
1052
    static formula sugar_equal(const formula& b, uint8_t min, uint8_t max);
1053
1054

#ifndef SWIG
1055
1056
1057
1058
1059
1060
1061
1062
1063
    /// \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
1064
1065
1066
1067
1068
1069
    const fnode* to_node_()
    {
      auto tmp = ptr_;
      ptr_ = nullptr;
      return tmp;
    }
1070
1071
#endif

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

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

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

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

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

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

1115
#ifndef SWIG
1116
1117
1118
1119
1120
1121
    /// \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
1122
1123
1124
1125
    formula get_child_of(std::initializer_list<op> l) const
    {
      auto f = ptr_->get_child_of(l);
      if (f)
1126
        f->clone();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1127
1128
      return formula(f);
    }
1129
#endif
1130

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

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

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

1153
1154
1155
1156
1157
1158
1159
1160
    /// \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
1161
1162
1163
1164
    size_t id() const
    {
      return ptr_->id();
    }
1165

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1177