formula.hh 47 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
    public:
110
111
112
113
      /// \brief Clone an fnode.
      ///
      /// This simply increment the reference counter.  If the counter
      /// saturates, the fnode will stay permanently allocated.
114
115
116
117
118
119
120
121
      const fnode* clone() const
      {
        // Saturate.
        ++refs_;
        if (SPOT_UNLIKELY(!refs_))
          saturated_ = 1;
        return this;
      }
122

123
124
125
126
127
      /// \brief Dereference an fnode.
      ///
      /// This decrement the reference counter (unless the counter is
      /// saturated), and actually deallocate the fnode when the
      /// counder reaches 0 (unless the fnode denotes a constant).
128
129
130
131
132
133
134
135
      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();
      }
136

137
      /// \see formula::unbounded
138
139
140
141
      static constexpr uint8_t unbounded()
      {
        return UINT8_MAX;
      }
142

143
      /// \see formula::ap
144
      static const fnode* ap(const std::string& name);
145
      /// \see formula::unop
146
      static const fnode* unop(op o, const fnode* f);
147
      /// \see formula::binop
148
      static const fnode* binop(op o, const fnode* f, const fnode* g);
149
      /// \see formula::multop
150
      static const fnode* multop(op o, std::vector<const fnode*> l);
151
      /// \see formula::bunop
152
153
      static const fnode* bunop(op o, const fnode* f,
          uint8_t min, uint8_t max = unbounded());
154

155
      /// \see formula::kind
156
157
158
159
      op kind() const
      {
        return op_;
      }
160

161
      /// \see formula::kindstr
162
      std::string kindstr() const;
163

164
      /// \see formula::is
165
166
167
168
      bool is(op o) const
      {
        return op_ == o;
      }
169

170
      /// \see formula::is
171
172
173
174
      bool is(op o1, op o2) const
      {
        return op_ == o1 || op_ == o2;
      }
175

176
      /// \see formula::is
177
178
179
180
181
182
183
184
185
186
187
      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;
      }
188

189
      /// \see formula::get_child_of
190
191
192
193
      const fnode* get_child_of(op o) const
      {
        if (op_ != o)
          return nullptr;
194
195
196
        if (SPOT_UNLIKELY(size_ != 1))
          throw std::invalid_argument
            ("get_child_of() expecting single-child node");
197
198
        return nth(0);
      }
199

200
      /// \see formula::get_child_of
201
202
203
204
205
206
207
208
209
210
211
      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;
      }
212

213
      /// \see formula::min
214
215
      unsigned min() const
      {
216
217
218
        if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
          throw std::invalid_argument
            ("min() only works on Star and FStar nodes");
219
220
        return min_;
      }
221

222
      /// \see formula::max
223
224
      unsigned max() const
      {
225
226
227
        if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
          throw std::invalid_argument
            ("max() only works on Star and FStar nodes");
228
229
        return max_;
      }
230

231
      /// \see formula::size
232
233
234
235
      unsigned size() const
      {
        return size_;
      }
236

237
      /// \see formula::id
238
239
240
241
      size_t id() const
      {
        return id_;
      }
242

243
      /// \see formula::begin
244
245
246
247
      const fnode*const* begin() const
      {
        return children;
      }
248

249
      /// \see formula::end
250
251
252
253
      const fnode*const* end() const
      {
        return children + size();
      }
254

255
      /// \see formula::nth
256
257
258
259
260
261
      const fnode* nth(unsigned i) const
      {
        if (i >= size())
          throw std::runtime_error("access to non-existing child");
        return children[i];
      }
262

263
      /// \see formula::ff
264
265
266
267
      static const fnode* ff()
      {
        return ff_;
      }
268

269
      /// \see formula::is_ff
270
271
272
273
      bool is_ff() const
      {
        return op_ == op::ff;
      }
274

275
      /// \see formula::tt
276
277
278
279
      static const fnode* tt()
      {
        return tt_;
      }
280

281
      /// \see formula::is_tt
282
283
284
285
      bool is_tt() const
      {
        return op_ == op::tt;
      }
286

287
      /// \see formula::eword
288
289
290
291
      static const fnode* eword()
      {
        return ew_;
      }
292

293
      /// \see formula::is_eword
294
295
296
297
      bool is_eword() const
      {
        return op_ == op::eword;
      }
298

299
      /// \see formula::is_constant
300
301
302
303
      bool is_constant() const
      {
        return op_ == op::ff || op_ == op::tt || op_ == op::eword;
      }
304

305
      /// \see formula::is_Kleene_star
306
307
308
309
310
311
      bool is_Kleene_star() const
      {
        if (op_ != op::Star)
          return false;
        return min_ == 0 && max_ == unbounded();
      }
312

313
      /// \see formula::one_star
314
315
316
317
318
319
      static const fnode* one_star()
      {
        if (!one_star_)
          one_star_ = bunop(op::Star, tt(), 0);
        return one_star_;
      }
320

321
      /// \see formula::ap_name
322
      const std::string& ap_name() const;
323
324

      /// \see formula::dump
325
      std::ostream& dump(std::ostream& os) const;
326

327
      /// \see formula::all_but
328
      const fnode* all_but(unsigned i) const;
329

330
      /// \see formula::boolean_count
331
332
333
334
335
336
337
338
      unsigned boolean_count() const
      {
        unsigned pos = 0;
        unsigned s = size();
        while (pos < s && children[pos]->is_boolean())
          ++pos;
        return pos;
      }
339

340
      /// \see formula::boolean_operands
341
      const fnode* boolean_operands(unsigned* width = nullptr) const;
342

343
344
345
      /// \brief safety check for the reference counters
      ///
      /// \return true iff the unicity map contains only the globally
346
      /// pre-allocated formulas.
347
348
349
350
351
352
      ///
      /// This is meant to be used as
      /// \code
      /// assert(spot::fnode::instances_check());
      /// \endcode
      /// at the end of a program.
353
      static bool instances_check();
354

355
356
357
      ////////////////
      // Properties //
      ////////////////
358

359
      /// \see formula::is_boolean
360
361
362
363
      bool is_boolean() const
      {
        return is_.boolean;
      }
364

365
      /// \see formula::is_sugar_free_boolean
366
367
368
369
      bool is_sugar_free_boolean() const
      {
        return is_.sugar_free_boolean;
      }
370

371
      /// \see formula::is_in_nenoform
372
373
374
375
      bool is_in_nenoform() const
      {
        return is_.in_nenoform;
      }
376

377
      /// \see formula::is_syntactic_stutter_invariant
378
379
380
381
      bool is_syntactic_stutter_invariant() const
      {
        return is_.syntactic_si;
      }
382

383
      /// \see formula::is_sugar_free_ltl
384
385
386
387
      bool is_sugar_free_ltl() const
      {
        return is_.sugar_free_ltl;
      }
388

389
      /// \see formula::is_ltl_formula
390
391
392
393
      bool is_ltl_formula() const
      {
        return is_.ltl_formula;
      }
394

395
      /// \see formula::is_psl_formula
396
397
398
399
      bool is_psl_formula() const
      {
        return is_.psl_formula;
      }
400

401
      /// \see formula::is_sere_formula
402
403
404
405
      bool is_sere_formula() const
      {
        return is_.sere_formula;
      }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
406

407
      /// \see formula::is_finite
408
409
410
411
      bool is_finite() const
      {
        return is_.finite;
      }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
412

413
      /// \see formula::is_eventual
414
415
416
417
      bool is_eventual() const
      {
        return is_.eventual;
      }
418

419
      /// \see formula::is_universal
420
421
422
423
      bool is_universal() const
      {
        return is_.universal;
      }
424

425
      /// \see formula::is_syntactic_safety
426
427
428
429
      bool is_syntactic_safety() const
      {
        return is_.syntactic_safety;
      }
430

431
      /// \see formula::is_syntactic_guarantee
432
433
434
435
      bool is_syntactic_guarantee() const
      {
        return is_.syntactic_guarantee;
      }
436

437
      /// \see formula::is_syntactic_obligation
438
439
440
441
      bool is_syntactic_obligation() const
      {
        return is_.syntactic_obligation;
      }
442

443
      /// \see formula::is_syntactic_recurrence
444
445
446
447
      bool is_syntactic_recurrence() const
      {
        return is_.syntactic_recurrence;
      }
448

449
      /// \see formula::is_syntactic_persistence
450
451
452
453
      bool is_syntactic_persistence() const
      {
        return is_.syntactic_persistence;
      }
454

455
      /// \see formula::is_marked
456
457
458
459
      bool is_marked() const
      {
        return !is_.not_marked;
      }
460

461
      /// \see formula::accepts_eword
462
463
464
465
      bool accepts_eword() const
      {
        return is_.accepting_eword;
      }
466

467
      /// \see formula::has_lbt_atomic_props
468
469
470
471
      bool has_lbt_atomic_props() const
      {
        return is_.lbt_atomic_props;
      }
472

473
      /// \see formula::has_spin_atomic_props
474
475
476
477
      bool has_spin_atomic_props() const
      {
        return is_.spin_atomic_props;
      }
478

479
480
481
    private:
      void setup_props(op o);
      void destroy_aux() const;
482

483
      static const fnode* unique(const fnode*);
484

485
486
487
488
489
      // Destruction may only happen via destroy().
      ~fnode() = default;
      // Disallow copies.
      fnode(const fnode&) = delete;
      fnode& operator=(const fnode&) = delete;
490
491
492



493
494
495
496
497
498
499
500
501
502
503
504
      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);
        }
505

506
507
      fnode(op o, std::initializer_list<const fnode*> l)
        : fnode(o, l.begin(), l.end())
508
      {
509
      }
510

511
      fnode(op o, const fnode* f, uint8_t min, uint8_t max)
512
      {
513
514
515
516
517
        size_ = 1;
        children[0] = f;
        min_ = min;
        max_ = max;
        setup_props(o);
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
572
573
574
575
      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_;
      };
576

577
      const fnode* children[1];
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
578
  };
579

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
580
581
  /// Order two atomic propositions.
  SPOT_API
582
    int atomic_prop_cmp(const fnode* f, const fnode* g);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
583
584
585
586

  struct formula_ptr_less_than_bool_first
  {
    bool
587
588
      operator()(const fnode* left, const fnode* right) const
      {
589
590
        SPOT_ASSERT(left);
        SPOT_ASSERT(right);
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
        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
650
  };
651
652
653

#endif // SWIG

654
655
  /// \ingroup tl_essentials
  /// \brief Main class for temporal logic formula
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
656
657
658
  class SPOT_API formula final
  {
    const fnode* ptr_;
659
    public:
660
661
662
663
    /// \brief Create a formula from an fnode.
    ///
    /// This constructor is mainly for internal use, as spot::fnode
    /// object should usually not be manipulated from user code.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
664
665
    explicit formula(const fnode* f) noexcept
      : ptr_(f)
666
667
      {
      }
668

669
670
    /// \brief Create a null formula.
    ///
671
    /// This could be used to default-initialize a formula, however
672
    /// null formula should be short lived: most algorithms and member
673
    /// functions assume that formulas should not be null.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
674
675
    formula(std::nullptr_t) noexcept
      : ptr_(nullptr)
676
677
678
      {
      }

679
    /// \brief Default initialize a formula to nullptr.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
680
681
    formula() noexcept
      : ptr_(nullptr)
682
683
684
      {
      }

685
    /// Clone a formula.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
686
687
    formula(const formula& f) noexcept
      : ptr_(f.ptr_)
688
      {
689
690
        if (ptr_)
          ptr_->clone();
691
692
      }

693
    /// Move-construct a formula.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
694
695
    formula(formula&& f) noexcept
      : ptr_(f.ptr_)
696
      {
697
        f.ptr_ = nullptr;
698
699
      }

700
    /// Destroy a formula.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
701
    ~formula()
702
703
704
705
    {
      if (ptr_)
        ptr_->destroy();
    }
706

707
708
709
710
711
712
713
    /// \brief Reset a formula to null
    ///
    /// Note that null formula should be short lived: most algorithms
    /// and member function assume that formulas should not be null.
    /// Assigning nullptr to a formula can be useful when cleaning an
    /// array of formula using multiple passes and marking some
    /// formula as nullptr before actually erasing them.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
714
    const formula& operator=(std::nullptr_t)
715
716
717
718
719
    {
      this->~formula();
      ptr_ = nullptr;
      return *this;
    }
720

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
721
    const formula& operator=(const formula& f)
722
723
724
725
726
727
    {
      this->~formula();
      if ((ptr_ = f.ptr_))
        ptr_->clone();
      return *this;
    }
728

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
729
    const formula& operator=(formula&& f) noexcept
730
731
732
733
    {
      std::swap(f.ptr_, ptr_);
      return *this;
    }
734

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
735
736
737
    bool operator<(const formula& other) const noexcept
    {
      if (SPOT_UNLIKELY(!other.ptr_))
738
        return false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
739
      if (SPOT_UNLIKELY(!ptr_))
740
        return true;
741
      if (id() < other.id())
742
        return true;
743
      if (id() > other.id())
744
        return false;
745
746
747
748
749
      // 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
750
    }
751

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
752
753
    bool operator<=(const formula& other) const noexcept
    {
754
      return *this == other || *this < other;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
755
    }
756

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
757
758
    bool operator>(const formula& other) const noexcept
    {
759
      return !(*this <= other);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
760
    }
761

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
762
763
    bool operator>=(const formula& other) const noexcept
    {
764
      return !(*this < other);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
765
    }
766

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
767
768
769
770
    bool operator==(const formula& other) const noexcept
    {
      return other.ptr_ == ptr_;
    }
771

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
772
773
774
775
    bool operator==(std::nullptr_t) const noexcept
    {
      return ptr_ == nullptr;
    }
776

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
777
778
779
780
    bool operator!=(const formula& other) const noexcept
    {
      return other.ptr_ != ptr_;
    }
781

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
782
783
784
785
    bool operator!=(std::nullptr_t) const noexcept
    {
      return ptr_ != nullptr;
    }
786

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
787
788
789
790
    operator bool() const
    {
      return ptr_ != nullptr;
    }
791

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
792
793
794
    /////////////////////////
    // Forwarded functions //
    /////////////////////////
795

796
    /// Unbounded constant to use as end of range for bounded operators.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
797
798
799
800
    static constexpr uint8_t unbounded()
    {
      return fnode::unbounded();
    }
801

802
    /// Build an atomic proposition.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
803
804
805
806
    static formula ap(const std::string& name)
    {
      return formula(fnode::ap(name));
    }
807

808
809
810
811
812
813
814
815
816
817
818
819
820
821
    /// \brief Build an atomic proposition from... an atomic proposition.
    ///
    /// The only practical interest of this methods is for the Python
    /// bindings, where ap() can therefore work both from string or
    /// atomic propositions.
    static formula ap(const formula& a)
    {
      if (a.kind() == op::ap)
        return a;
      else
        throw std::invalid_argument("atomic propositions cannot be "
                                    "constructed from arbitrary formulas");
    }

822
823
824
825
    /// \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
826
827
828
829
    static formula unop(op o, const formula& f)
    {
      return formula(fnode::unop(o, f.ptr_->clone()));
    }
830
831

#ifndef SWIG
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
832
833
834
835
    static formula unop(op o, formula&& f)
    {
      return formula(fnode::unop(o, f.to_node_()));
    }
836
#endif // !SWIG
837
    /// @}
838
839

#ifdef SWIG
840
841
842
843
#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
844
    }
845
#else // !SWIG
846
847
848
849
850
851
852
853
#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
854
    }
855
#endif // !SWIG
856
857
    /// \brief Construct a negation
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
858
    SPOT_DEF_UNOP(Not);
859
860
861
862
    /// @}

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

    /// \brief Construct an F
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
868
    SPOT_DEF_UNOP(F);
869
870
871
872
    /// @}

    /// \brief Construct a G
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
873
    SPOT_DEF_UNOP(G);
874
875
876
877
    /// @}

    /// \brief Construct a PSL Closure
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
878
    SPOT_DEF_UNOP(Closure);
879
880
881
882
    /// @}

    /// \brief Construct a negated PSL Closure
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
883
    SPOT_DEF_UNOP(NegClosure);
884
885
886
887
    /// @}

    /// \brief Construct a marked negated PSL Closure
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
888
    SPOT_DEF_UNOP(NegClosureMarked);
889
    /// @}
890
891
#undef SPOT_DEF_UNOP

892
    /// @{
893
894
895
896
    /// \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
897
898
899
900
    static formula binop(op o, const formula& f, const formula& g)
    {
      return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
    }
901
902

#ifndef SWIG
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
903
904
905
906
    static formula binop(op o, const formula& f, formula&& g)
    {
      return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
    }
907

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
908
909
910
911
    static formula binop(op o, formula&& f, const formula& g)
    {
      return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
    }
912

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
913
914
915
916
    static formula binop(op o, formula&& f, formula&& g)
    {
      return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
    }
917
918
    ///@}

919
920
921
#endif //SWIG

#ifdef SWIG
922
923
924
925
#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
926
    }
927
#else // !SWIG
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
#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
944
    }
945
#endif // !SWIG
946
    /// \brief Construct an `Xor` formula
947
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
948
    SPOT_DEF_BINOP(Xor);
949
950
    /// @}

951
    /// \brief Construct an `->` formula
952
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
953
    SPOT_DEF_BINOP(Implies);
954
955
    /// @}

956
    /// \brief Construct an `<->` formula
957
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
958
    SPOT_DEF_BINOP(Equiv);
959
960
    /// @}

961
    /// \brief Construct a `U` formula
962
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
963
    SPOT_DEF_BINOP(U);
964
965
    /// @}

966
    /// \brief Construct an `R` formula
967
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
968
    SPOT_DEF_BINOP(R);
969
970
    /// @}

971
    /// \brief Construct a `W` formula
972
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
973
    SPOT_DEF_BINOP(W);
974
975
    /// @}

976
    /// \brief Construct an `M` formula
977
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
978
    SPOT_DEF_BINOP(M);
979
980
    /// @}

981
    /// \brief Construct a `<>->` PSL formula
982
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
983
    SPOT_DEF_BINOP(EConcat);
984
985
    /// @}

986
    /// \brief Construct a marked `<>->` PSL formula
987
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
988
    SPOT_DEF_BINOP(EConcatMarked);
989
990
    /// @}

991
    /// \brief Construct a `[]->` PSL formula
992
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
993
    SPOT_DEF_BINOP(UConcat);
994
    /// @}
995
996
#undef SPOT_DEF_BINOP

997
998
999
1000
1001
    /// \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
1002
1003
1004
1005
1006
    static formula multop(op o, const std::vector<formula>& l)
    {
      std::vector<const fnode*> tmp;
      tmp.reserve(l.size());
      for (auto f: l)
1007
1008
        if (f.ptr_)
          tmp.push_back(f.ptr_->clone());
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1009
1010
      return formula(fnode::multop(o, std::move(tmp)));
    }
1011
1012

#ifndef SWIG
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1013
1014
1015
1016
1017
    static formula multop(op o, std::vector<formula>&& l)
    {
      std::vector<const fnode*> tmp;
      tmp.reserve(l.size());
      for (auto f: l)
1018
1019
        if (f.ptr_)
          tmp.push_back(f.to_node_());
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1020
1021
      return formula(fnode::multop(o, std::move(tmp)));
    }
1022
#endif // !SWIG
1023
    /// @}
1024
1025

#ifdef SWIG
1026
1027
1028
1029
#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
1030
    }
1031
#else // !SWIG
1032
1033
1034
1035
1036
1037
1038
1039
1040
#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
1041
    }
1042
#endif // !SWIG
1043
1044
    /// \brief Construct an Or formula.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1045
    SPOT_DEF_MULTOP(Or);
1046
1047
1048
1049
    /// @}

    /// \brief Construct an Or SERE.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1050
    SPOT_DEF_MULTOP(OrRat);
1051
1052
1053
1054
    /// @}

    /// \brief Construct an And formula.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1055
    SPOT_DEF_MULTOP(And);
1056
1057
1058
1059
    /// @}

    /// \brief Construct an And SERE.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1060
    SPOT_DEF_MULTOP(AndRat);
1061
1062
1063
1064
    /// @}

    /// \brief Construct a non-length-matching And SERE.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1065
    SPOT_DEF_MULTOP(AndNLM);
1066
1067
1068
1069
    /// @}

    /// \brief Construct a Concatenation SERE.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1070
    SPOT_DEF_MULTOP(Concat);
1071
1072
1073
1074
    /// @}

    /// \brief Construct a Fusion SERE.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1075
    SPOT_DEF_MULTOP(Fusion);
1076
    /// @}
1077
1078
#undef SPOT_DEF_MULTOP

1079
1080
1081
1082
    /// \brief Define a bounded unary-operator (i.e. star-like)
    ///
    /// \pre \a o should be op::Star or op::FStar.
    /// @{