formula.hh 46.6 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
194
195
196
      const fnode* get_child_of(op o) const
      {
        if (op_ != o)
          return nullptr;
        assert(size_ == 1);
        return nth(0);
      }
197

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

211
      /// \see formula::min
212
213
214
215
216
      unsigned min() const
      {
        assert(op_ == op::FStar || op_ == op::Star);
        return min_;
      }
217

218
      /// \see formula::max
219
220
221
222
223
      unsigned max() const
      {
        assert(op_ == op::FStar || op_ == op::Star);
        return max_;
      }
224

225
      /// \see formula::size
226
227
228
229
      unsigned size() const
      {
        return size_;
      }
230

231
      /// \see formula::id
232
233
234
235
      size_t id() const
      {
        return id_;
      }
236

237
      /// \see formula::begin
238
239
240
241
      const fnode*const* begin() const
      {
        return children;
      }
242

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

249
      /// \see formula::nth
250
251
252
253
254
255
      const fnode* nth(unsigned i) const
      {
        if (i >= size())
          throw std::runtime_error("access to non-existing child");
        return children[i];
      }
256

257
      /// \see formula::ff
258
259
260
261
      static const fnode* ff()
      {
        return ff_;
      }
262

263
      /// \see formula::is_ff
264
265
266
267
      bool is_ff() const
      {
        return op_ == op::ff;
      }
268

269
      /// \see formula::tt
270
271
272
273
      static const fnode* tt()
      {
        return tt_;
      }
274

275
      /// \see formula::is_tt
276
277
278
279
      bool is_tt() const
      {
        return op_ == op::tt;
      }
280

281
      /// \see formula::eword
282
283
284
285
      static const fnode* eword()
      {
        return ew_;
      }
286

287
      /// \see formula::is_eword
288
289
290
291
      bool is_eword() const
      {
        return op_ == op::eword;
      }
292

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

299
      /// \see formula::is_Kleene_star
300
301
302
303
304
305
      bool is_Kleene_star() const
      {
        if (op_ != op::Star)
          return false;
        return min_ == 0 && max_ == unbounded();
      }
306

307
      /// \see formula::one_star
308
309
310
311
312
313
      static const fnode* one_star()
      {
        if (!one_star_)
          one_star_ = bunop(op::Star, tt(), 0);
        return one_star_;
      }
314

315
      /// \see formula::ap_name
316
      const std::string& ap_name() const;
317
318

      /// \see formula::dump
319
      std::ostream& dump(std::ostream& os) const;
320

321
      /// \see formula::all_but
322
      const fnode* all_but(unsigned i) const;
323

324
      /// \see formula::boolean_count
325
326
327
328
329
330
331
332
      unsigned boolean_count() const
      {
        unsigned pos = 0;
        unsigned s = size();
        while (pos < s && children[pos]->is_boolean())
          ++pos;
        return pos;
      }
333

334
      /// \see formula::boolean_operands
335
      const fnode* boolean_operands(unsigned* width = nullptr) const;
336

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

349
350
351
      ////////////////
      // Properties //
      ////////////////
352

353
      /// \see formula::is_boolean
354
355
356
357
      bool is_boolean() const
      {
        return is_.boolean;
      }
358

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

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

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

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

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

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

395
      /// \see formula::is_sere_formula
396
397
398
399
      bool is_sere_formula() const
      {
        return is_.sere_formula;
      }
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
400

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

407
      /// \see formula::is_eventual
408
409
410
411
      bool is_eventual() const
      {
        return is_.eventual;
      }
412

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

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

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

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

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

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

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

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

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

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

473
474
475
    private:
      void setup_props(op o);
      void destroy_aux() const;
476

477
      static const fnode* unique(const fnode*);
478

479
480
481
482
483
      // Destruction may only happen via destroy().
      ~fnode() = default;
      // Disallow copies.
      fnode(const fnode&) = delete;
      fnode& operator=(const fnode&) = delete;
484
485
486



487
488
489
490
491
492
493
494
495
496
497
498
      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);
        }
499

500
501
      fnode(op o, std::initializer_list<const fnode*> l)
        : fnode(o, l.begin(), l.end())
502
      {
503
      }
504

505
      fnode(op o, const fnode* f, uint8_t min, uint8_t max)
506
      {
507
508
509
510
511
        size_ = 1;
        children[0] = f;
        min_ = min;
        max_ = max;
        setup_props(o);
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
      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_;
      };
570

571
      const fnode* children[1];
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
572
  };
573

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
574
575
  /// Order two atomic propositions.
  SPOT_API
576
    int atomic_prop_cmp(const fnode* f, const fnode* g);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
577
578
579
580

  struct formula_ptr_less_than_bool_first
  {
    bool
581
582
583
584
585
586
587
588
589
590
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
      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
644
  };
645
646
647

#endif // SWIG

648
649
  /// \ingroup tl_essentials
  /// \brief Main class for temporal logic formula
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
650
651
652
  class SPOT_API formula final
  {
    const fnode* ptr_;
653
    public:
654
655
656
657
    /// \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
658
659
    explicit formula(const fnode* f) noexcept
      : ptr_(f)
660
661
      {
      }
662

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

673
    /// \brief Default initialize a formula to nullptr.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
674
675
    formula() noexcept
      : ptr_(nullptr)
676
677
678
      {
      }

679
    /// Clone a formula.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
680
681
    formula(const formula& f) noexcept
      : ptr_(f.ptr_)
682
      {
683
684
        if (ptr_)
          ptr_->clone();
685
686
      }

687
    /// Move-construct a formula.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
688
689
    formula(formula&& f) noexcept
      : ptr_(f.ptr_)
690
      {
691
        f.ptr_ = nullptr;
692
693
      }

694
    /// Destroy a formula.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
695
    ~formula()
696
697
698
699
    {
      if (ptr_)
        ptr_->destroy();
    }
700

701
702
703
704
705
706
707
    /// \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
708
    const formula& operator=(std::nullptr_t)
709
710
711
712
713
    {
      this->~formula();
      ptr_ = nullptr;
      return *this;
    }
714

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
715
    const formula& operator=(const formula& f)
716
717
718
719
720
721
    {
      this->~formula();
      if ((ptr_ = f.ptr_))
        ptr_->clone();
      return *this;
    }
722

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
723
    const formula& operator=(formula&& f) noexcept
724
725
726
727
    {
      std::swap(f.ptr_, ptr_);
      return *this;
    }
728

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
746
747
    bool operator<=(const formula& other) const noexcept
    {
748
      return *this == other || *this < other;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
749
    }
750

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

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
761
762
763
764
    bool operator==(const formula& other) const noexcept
    {
      return other.ptr_ == ptr_;
    }
765

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
766
767
768
769
    bool operator==(std::nullptr_t) const noexcept
    {
      return ptr_ == nullptr;
    }
770

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
771
772
773
774
    bool operator!=(const formula& other) const noexcept
    {
      return other.ptr_ != ptr_;
    }
775

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
776
777
778
779
    bool operator!=(std::nullptr_t) const noexcept
    {
      return ptr_ != nullptr;
    }
780

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
786
787
788
    /////////////////////////
    // Forwarded functions //
    /////////////////////////
789

790
    /// Unbounded constant to use as end of range for bounded operators.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
791
792
793
794
    static constexpr uint8_t unbounded()
    {
      return fnode::unbounded();
    }
795

796
    /// Build an atomic proposition.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
797
798
799
800
    static formula ap(const std::string& name)
    {
      return formula(fnode::ap(name));
    }
801

802
803
804
805
806
807
808
809
810
811
812
813
814
815
    /// \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");
    }

816
817
818
819
    /// \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
820
821
822
823
    static formula unop(op o, const formula& f)
    {
      return formula(fnode::unop(o, f.ptr_->clone()));
    }
824
825

#ifndef SWIG
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
826
827
828
829
    static formula unop(op o, formula&& f)
    {
      return formula(fnode::unop(o, f.to_node_()));
    }
830
#endif // !SWIG
831
    /// @}
832
833

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

    /// \brief Construct an X
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
857
    SPOT_DEF_UNOP(X);
858
859
860
861
    /// @}

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

    /// \brief Construct a G
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
867
    SPOT_DEF_UNOP(G);
868
869
870
871
    /// @}

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

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

    /// \brief Construct a marked negated PSL Closure
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
882
    SPOT_DEF_UNOP(NegClosureMarked);
883
    /// @}
884
885
#undef SPOT_DEF_UNOP

886
    /// @{
887
888
889
890
    /// \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
891
892
893
894
    static formula binop(op o, const formula& f, const formula& g)
    {
      return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
    }
895
896

#ifndef SWIG
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
897
898
899
900
    static formula binop(op o, const formula& f, formula&& g)
    {
      return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
    }
901

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

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

913
914
915
#endif //SWIG

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

945
    /// \brief Construct an `->` formula
946
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
947
    SPOT_DEF_BINOP(Implies);
948
949
    /// @}

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

955
    /// \brief Construct a `U` formula
956
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
957
    SPOT_DEF_BINOP(U);
958
959
    /// @}

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

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

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

975
    /// \brief Construct a `<>->` PSL formula
976
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
977
    SPOT_DEF_BINOP(EConcat);
978
979
    /// @}

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

985
    /// \brief Construct a `[]->` PSL formula
986
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
987
    SPOT_DEF_BINOP(UConcat);
988
    /// @}
989
990
#undef SPOT_DEF_BINOP

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

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

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

    /// \brief Construct an Or SERE.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1044
    SPOT_DEF_MULTOP(OrRat);
1045
1046
1047
1048
    /// @}

    /// \brief Construct an And formula.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1049
    SPOT_DEF_MULTOP(And);
1050
1051
1052
1053
    /// @}

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

    /// \brief Construct a non-length-matching And SERE.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1059
    SPOT_DEF_MULTOP(AndNLM);
1060
1061
1062
1063
    /// @}

    /// \brief Construct a Concatenation SERE.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1064
    SPOT_DEF_MULTOP(Concat);
1065
1066
1067
1068
    /// @}

    /// \brief Construct a Fusion SERE.
    /// @{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1069
    SPOT_DEF_MULTOP(Fusion);
1070
    /// @}
1071
1072
#undef SPOT_DEF_MULTOP

1073
1074
1075
1076
    /// \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
1077
    static formula bunop(op o, const formula& f,
1078
1079
        uint8_t min = 0U,
        uint8_t max = unbounded())
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1080
1081
1082
    {
      return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
    }
1083
1084

#ifndef SWIG
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1085
    static formula bunop(op o, formula&& f,
1086
1087
        uint8_t min = 0U,
        uint8_t max = unbounded())