formula.hh

Go to the documentation of this file.

// -*- coding: utf-8 -*-
// Copyright (C) by the Spot authors, see the AUTHORS file for details.
//
// 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
// the Free Software Foundation; either version 3 of the License, or
// (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
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
#pragma once
 
 
 
 
 
 
 
#include <spot/misc/common.hh>
#include <memory>
#include <cstdint>
#include <initializer_list>
#include <cassert>
#include <vector>
#include <string>
#include <iterator>
#include <iosfwd>
#include <sstream>
#include <list>
#include <cstddef>
#include <limits>
 
// The strong_X operator was introduced in Spot 2.8.2 to fix an issue
// with from_ltlf().  As adding a new operator is a backward
// incompatibility, causing new warnings from the compiler.
#if defined(SPOT_BUILD) || defined(SPOT_USES_STRONG_X)
// Use #if SPOT_HAS_STRONG_X in code that need to be backward
// compatible with older Spot versions.
#  define SPOT_HAS_STRONG_X 1
// You may #define SPOT_WANT_STRONG_X yourself before including
// this file to force the use of STRONG_X
#  define SPOT_WANT_STRONG_X 1
#endif
 
namespace spot
{
 
 
  enum class op: uint8_t
  {
    ff,                        
    tt,                        
    eword,                     
    ap,                        
    // unary operators
    Not,                       
    X,                         
    F,                         
    G,                         
    Closure,                   
    NegClosure,                
    NegClosureMarked,          
    // binary operators
    Xor,                       
    Implies,                   
    Equiv,                     
    U,                         
    R,                         
    W,                         
    M,                         
    EConcat,                   
    EConcatMarked,             
    UConcat,                   
    // n-ary operators
    Or,                        
    OrRat,                     
    And,                       
    AndRat,                    
    AndNLM,                    
    Concat,                    
    Fusion,                    
    // star-like operators
    Star,                      
    FStar,                     
    first_match,               
#ifdef SPOT_WANT_STRONG_X
    strong_X,                  
#endif
  };
 
#ifndef SWIG
  class SPOT_API fnode final
  {
    public:
      const fnode* clone() const
      {
        // Saturate.
        ++refs_;
        if (SPOT_UNLIKELY(!refs_))
          saturated_ = 1;
        return this;
      }
 
      void destroy() const
      {
        if (SPOT_LIKELY(refs_))
          --refs_;
        else if (SPOT_LIKELY(!saturated_))
          // last reference to a node that is not a constant
          destroy_aux();
      }
 
      static constexpr uint8_t unbounded()
      {
        return UINT8_MAX;
      }
 
      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,
          unsigned min, unsigned max = unbounded());
 
      static const fnode* nested_unop_range(op uo, op bo, unsigned min,
                                            unsigned max, const fnode* f);
 
      op kind() const
      {
        return op_;
      }
 
      std::string kindstr() const;
 
      bool is(op o) const
      {
        return op_ == o;
      }
 
      bool is(op o1, op o2) const
      {
        return op_ == o1 || op_ == o2;
      }
 
      bool is(op o1, op o2, op o3) const
      {
        return op_ == o1 || op_ == o2 || op_ == o3;
      }
 
      bool is(op o1, op o2, op o3, op o4) const
      {
        return op_ == o1 || op_ == o2 || op_ == o3 || op_ == o4;
      }
 
      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;
      }
 
      const fnode* get_child_of(op o) const
      {
        if (op_ != o)
          return nullptr;
        if (SPOT_UNLIKELY(size_ != 1))
          report_get_child_of_expecting_single_child_node();
        return nth(0);
      }
 
      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;
      }
 
      unsigned min() const
      {
        if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
          report_min_invalid_arg();
        return min_;
      }
 
      unsigned max() const
      {
        if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
          report_max_invalid_arg();
        return max_;
      }
 
      unsigned size() const
      {
        return size_;
      }
 
      bool is_leaf() const
      {
        return size_ == 0;
      }
 
      size_t id() const
      {
        return id_;
      }
 
      const fnode*const* begin() const
      {
        return children;
      }
 
      const fnode*const* end() const
      {
        return children + size();
      }
 
      const fnode* nth(unsigned i) const
      {
        if (SPOT_UNLIKELY(i >= size()))
          report_non_existing_child();
        const fnode* c = children[i];
        SPOT_ASSUME(c != nullptr);
        return c;
      }
 
      static const fnode* ff()
      {
        return ff_;
      }
 
      bool is_ff() const
      {
        return op_ == op::ff;
      }
 
      static const fnode* tt()
      {
        return tt_;
      }
 
      bool is_tt() const
      {
        return op_ == op::tt;
      }
 
      static const fnode* eword()
      {
        return ew_;
      }
 
      bool is_eword() const
      {
        return op_ == op::eword;
      }
 
      bool is_constant() const
      {
        return op_ == op::ff || op_ == op::tt || op_ == op::eword;
      }
 
      bool is_Kleene_star() const
      {
        if (op_ != op::Star)
          return false;
        return min_ == 0 && max_ == unbounded();
      }
 
      static const fnode* one_star()
      {
        if (!one_star_)
          one_star_ = new fnode(op::Star, tt_, 0, unbounded(), true);
        return one_star_;
      }
 
      static const fnode* one_plus()
      {
        if (!one_plus_)
          one_plus_ = new fnode(op::Star, tt_, 1, unbounded(), true);
        return one_plus_;
      }
 
      const std::string& ap_name() const;
 
      std::ostream& dump(std::ostream& os) const;
 
      const fnode* all_but(unsigned i) const;
 
      unsigned boolean_count() const
      {
        unsigned pos = 0;
        unsigned s = size();
        while (pos < s && children[pos]->is_boolean())
          ++pos;
        return pos;
      }
 
      const fnode* boolean_operands(unsigned* width = nullptr) const;
 
      static bool instances_check();
 
      // Properties //
 
      bool is_boolean() const
      {
        return is_.boolean;
      }
 
      bool is_sugar_free_boolean() const
      {
        return is_.sugar_free_boolean;
      }
 
      bool is_in_nenoform() const
      {
        return is_.in_nenoform;
      }
 
      bool is_syntactic_stutter_invariant() const
      {
        return is_.syntactic_si;
      }
 
      bool is_sugar_free_ltl() const
      {
        return is_.sugar_free_ltl;
      }
 
      bool is_ltl_formula() const
      {
        return is_.ltl_formula;
      }
 
      bool is_psl_formula() const
      {
        return is_.psl_formula;
      }
 
      bool is_sere_formula() const
      {
        return is_.sere_formula;
      }
 
      bool is_finite() const
      {
        return is_.finite;
      }
 
      bool is_eventual() const
      {
        return is_.eventual;
      }
 
      bool is_universal() const
      {
        return is_.universal;
      }
 
      bool is_syntactic_safety() const
      {
        return is_.syntactic_safety;
      }
 
      bool is_syntactic_guarantee() const
      {
        return is_.syntactic_guarantee;
      }
 
      bool is_syntactic_obligation() const
      {
        return is_.syntactic_obligation;
      }
 
      bool is_syntactic_recurrence() const
      {
        return is_.syntactic_recurrence;
      }
 
      bool is_syntactic_persistence() const
      {
        return is_.syntactic_persistence;
      }
 
      bool is_marked() const
      {
        return !is_.not_marked;
      }
 
      bool accepts_eword() const
      {
        return is_.accepting_eword;
      }
 
      bool has_lbt_atomic_props() const
      {
        return is_.lbt_atomic_props;
      }
 
      bool has_spin_atomic_props() const
      {
        return is_.spin_atomic_props;
      }
 
      bool is_sigma2() const
      {
        return is_.sigma2;
      }
 
      bool is_pi2() const
      {
        return is_.pi2;
      }
 
      bool is_delta1() const
      {
        return is_.delta1;
      }
 
      bool is_delta2() const
      {
        return is_.delta2;
      }
 
    private:
      static size_t bump_next_id();
      void setup_props(op o);
      void destroy_aux() const;
 
      [[noreturn]] static void report_non_existing_child();
      [[noreturn]] static void report_too_many_children();
      [[noreturn]] static void
        report_get_child_of_expecting_single_child_node();
      [[noreturn]] static void report_min_invalid_arg();
      [[noreturn]] static void report_max_invalid_arg();
 
      static const fnode* unique(fnode*);
 
      // Destruction may only happen via destroy().
      ~fnode() = default;
      // Disallow copies.
      fnode(const fnode&) = delete;
      fnode& operator=(const fnode&) = delete;
 
 
 
      template<class iter>
      fnode(op o, iter begin, iter end, bool saturated = false)
        // Clang has some optimization where is it able to combine the
        // 4 movb initializing op_,min_,max_,saturated_ into a single
        // movl.  Also it can optimize the three byte-comparisons of
        // is_Kleene_star() into a single masked 32-bit comparison.
        // The latter optimization triggers warnings from valgrind if
        // min_ and max_ are not initialized.  So to benefit from the
        // initialization optimization and the is_Kleene_star()
        // optimization in Clang, we always initialize min_ and max_
        // with this compiler.  Do not do it the rest of the time,
        // since the optimization is not done.
        : op_(o),
#if __llvm__
         min_(0), max_(0),
#endif
         saturated_(saturated)
      {
        size_t s = std::distance(begin, end);
        if (SPOT_UNLIKELY(s > (size_t) UINT16_MAX))
          report_too_many_children();
        size_ = s;
        auto pos = children;
        for (auto i = begin; i != end; ++i)
          *pos++ = *i;
        setup_props(o);
      }
 
      fnode(op o, std::initializer_list<const fnode*> l,
            bool saturated = false)
        : fnode(o, l.begin(), l.end(), saturated)
      {
      }
 
      fnode(op o, const fnode* f, uint8_t min, uint8_t max,
            bool saturated = false)
        : op_(o), min_(min), max_(max), saturated_(saturated), size_(1)
      {
        children[0] = f;
        setup_props(o);
      }
 
      static const fnode* ff_;
      static const fnode* tt_;
      static const fnode* ew_;
      static const fnode* one_star_;
      static const fnode* one_plus_;
 
      op op_;                      // operator
      uint8_t min_;                // range minimum (for star-like operators)
      uint8_t max_;                // range maximum;
      mutable uint8_t saturated_;
      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 (S).
        bool syntactic_guarantee:1;    // Syntactic Guarantee Property (G).
        bool syntactic_obligation:1;   // Syntactic Obligation Property (O).
        bool syntactic_recurrence:1;   // Syntactic Recurrence Property (R).
        bool syntactic_persistence:1;  // Syntactic Persistence Property (P).
        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.
        bool delta1:1;                 // Boolean combination of (S) and (G).
        bool sigma2:1; // Boolean comb. of (S) with X/F/U/M possibly applied.
        bool pi2:1;    // Boolean comb. of (G) with X/G/R/W possibly applied.
        bool delta2:1;                 // Boolean combination of (Σ₂) and (Π₂).
      };
      union
      {
        // Use an unsigned for fast computation of all properties.
        unsigned props;
        ltl_prop is_;
      };
 
      const fnode* children[1];
  };
 
  SPOT_API
    int atomic_prop_cmp(const fnode* f, const fnode* g);
 
  class SPOT_API formula;
 
  struct formula_ptr_less_than_bool_first
  {
    bool
      operator()(const fnode* left, const fnode* right) const
      {
        SPOT_ASSERT(left);
        SPOT_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();
      }
 
    SPOT_API bool
    operator()(const formula& left, const formula& right) const;
};
 
#endif // SWIG
 
  class SPOT_API formula final
  {
    friend struct formula_ptr_less_than_bool_first;
    const fnode* ptr_;
    public:
    explicit formula(const fnode* f) noexcept
      : ptr_(f)
      {
      }
 
    formula(std::nullptr_t) noexcept
      : ptr_(nullptr)
      {
      }
 
    formula() noexcept
      : ptr_(nullptr)
      {
      }
 
    formula(const formula& f) noexcept
      : ptr_(f.ptr_)
      {
        if (ptr_)
          ptr_->clone();
      }
 
    formula(formula&& f) noexcept
      : ptr_(f.ptr_)
      {
        f.ptr_ = nullptr;
      }
 
    ~formula()
    {
      if (ptr_)
        ptr_->destroy();
    }
 
    const formula& operator=(std::nullptr_t)
    {
      this->~formula();
      ptr_ = nullptr;
      return *this;
    }
 
    const formula& operator=(const formula& f)
    {
      this->~formula();
      if ((ptr_ = f.ptr_))
        ptr_->clone();
      return *this;
    }
 
    const formula& operator=(formula&& f) noexcept
    {
      std::swap(f.ptr_, ptr_);
      return *this;
    }
 
    bool operator<(const formula& other) const noexcept
    {
      if (SPOT_UNLIKELY(!other.ptr_))
        return false;
      if (SPOT_UNLIKELY(!ptr_))
        return true;
      if (id() < other.id())
        return true;
      if (id() > other.id())
        return false;
      // The case where id()==other.id() but ptr_ != other.ptr_ is
      // very unlikely (we would need to build more than UINT_MAX
      // formulas), so let's just compare pointers, and ignore the
      // fact that it may introduce some nondeterminism.
      return ptr_ < other.ptr_;
    }
 
    bool operator<=(const formula& other) const noexcept
    {
      return *this == other || *this < other;
    }
 
    bool operator>(const formula& other) const noexcept
    {
      return !(*this <= other);
    }
 
    bool operator>=(const formula& other) const noexcept
    {
      return !(*this < other);
    }
 
    bool operator==(const formula& other) const noexcept
    {
      return other.ptr_ == ptr_;
    }
 
    bool operator==(std::nullptr_t) const noexcept
    {
      return ptr_ == nullptr;
    }
 
    bool operator!=(const formula& other) const noexcept
    {
      return other.ptr_ != ptr_;
    }
 
    bool operator!=(std::nullptr_t) const noexcept
    {
      return ptr_ != nullptr;
    }
 
    explicit operator bool() const noexcept
    {
      return ptr_ != nullptr;
    }
 
    // Forwarded functions //
 
    static constexpr uint8_t unbounded()
    {
      return fnode::unbounded();
    }
 
    static formula ap(const std::string& name)
    {
      return formula(fnode::ap(name));
    }
 
    static formula ap(const formula& a)
    {
      if (SPOT_UNLIKELY(a.kind() != op::ap))
        report_ap_invalid_arg();
      return a;
    }
 
    static formula unop(op o, const formula& f)
    {
      return formula(fnode::unop(o, f.ptr_->clone()));
    }
 
#ifndef SWIG
    static formula unop(op o, formula&& f)
    {
      return formula(fnode::unop(o, f.to_node_()));
    }
#endif // !SWIG
 
#ifdef SWIG
#define SPOT_DEF_UNOP(Name)                          \
    static formula Name(const formula& f)            \
    {                                                \
      return unop(op::Name, f);                      \
    }
#else // !SWIG
#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));           \
    }
#endif // !SWIG
    SPOT_DEF_UNOP(Not);
 
    SPOT_DEF_UNOP(X);
 
    static formula X(unsigned level, const formula& f)
    {
      return nested_unop_range(op::X, op::Or /* unused */, level, level, f);
    }
 
#if SPOT_WANT_STRONG_X
    SPOT_DEF_UNOP(strong_X);
 
    static formula strong_X(unsigned level, const formula& f)
    {
      return nested_unop_range(op::strong_X, op::Or /* unused */,
                               level, level, f);
    }
#endif
 
    SPOT_DEF_UNOP(F);
 
    static formula F(unsigned min_level, unsigned max_level, const formula& f)
    {
      return nested_unop_range(op::X, op::Or, min_level, max_level, f);
    }
 
    static formula G(unsigned min_level, unsigned max_level, const formula& f)
    {
      return nested_unop_range(op::X, op::And, min_level, max_level, f);
    }
 
    SPOT_DEF_UNOP(G);
 
    SPOT_DEF_UNOP(Closure);
 
    SPOT_DEF_UNOP(NegClosure);
 
    SPOT_DEF_UNOP(NegClosureMarked);
 
    SPOT_DEF_UNOP(first_match);
#undef SPOT_DEF_UNOP
 
    static formula binop(op o, const formula& f, const formula& g)
    {
      return formula(fnode::binop(o, f.ptr_->clone(), g.ptr_->clone()));
    }
 
#ifndef SWIG
    static formula binop(op o, const formula& f, formula&& g)
    {
      return formula(fnode::binop(o, f.ptr_->clone(), g.to_node_()));
    }
 
    static formula binop(op o, formula&& f, const formula& g)
    {
      return formula(fnode::binop(o, f.to_node_(), g.ptr_->clone()));
    }
 
    static formula binop(op o, formula&& f, formula&& g)
    {
      return formula(fnode::binop(o, f.to_node_(), g.to_node_()));
    }
 
#endif //SWIG
 
#ifdef SWIG
#define SPOT_DEF_BINOP(Name)                                         \
    static formula Name(const formula& f, const formula& g)          \
    {                                                                \
      return binop(op::Name, f, g);                                  \
    }
#else // !SWIG
#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));            \
    }
#endif // !SWIG
    SPOT_DEF_BINOP(Xor);
 
    SPOT_DEF_BINOP(Implies);
 
    SPOT_DEF_BINOP(Equiv);
 
    SPOT_DEF_BINOP(U);
 
    SPOT_DEF_BINOP(R);
 
    SPOT_DEF_BINOP(W);
 
    SPOT_DEF_BINOP(M);
 
    SPOT_DEF_BINOP(EConcat);
 
    SPOT_DEF_BINOP(EConcatMarked);
 
    SPOT_DEF_BINOP(UConcat);
#undef SPOT_DEF_BINOP
 
    static formula multop(op o, const std::vector<formula>& l)
    {
      std::vector<const fnode*> tmp;
      tmp.reserve(l.size());
      for (auto f: l)
        if (f.ptr_)
          tmp.emplace_back(f.ptr_->clone());
      return formula(fnode::multop(o, std::move(tmp)));
    }
 
#ifndef SWIG
    static formula multop(op o, std::vector<formula>&& l)
    {
      std::vector<const fnode*> tmp;
      tmp.reserve(l.size());
      for (auto f: l)
        if (f.ptr_)
          tmp.emplace_back(f.to_node_());
      return formula(fnode::multop(o, std::move(tmp)));
    }
#endif // !SWIG
 
#ifdef SWIG
#define SPOT_DEF_MULTOP(Name)                                \
    static formula Name(const std::vector<formula>& l)       \
    {                                                        \
      return multop(op::Name, l);                            \
    }
#else // !SWIG
#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));                 \
    }
#endif // !SWIG
    SPOT_DEF_MULTOP(Or);
 
    SPOT_DEF_MULTOP(OrRat);
 
    SPOT_DEF_MULTOP(And);
 
    SPOT_DEF_MULTOP(AndRat);
 
    SPOT_DEF_MULTOP(AndNLM);
 
    SPOT_DEF_MULTOP(Concat);
 
    SPOT_DEF_MULTOP(Fusion);
#undef SPOT_DEF_MULTOP
 
    static formula bunop(op o, const formula& f,
        unsigned min = 0U,
        unsigned max = unbounded())
    {
      return formula(fnode::bunop(o, f.ptr_->clone(), min, max));
    }
 
#ifndef SWIG
    static formula bunop(op o, formula&& f,
        unsigned min = 0U,
        unsigned max = unbounded())
    {
      return formula(fnode::bunop(o, f.to_node_(), min, max));
    }
#endif // !SWIG
 
#if SWIG
#define SPOT_DEF_BUNOP(Name)                                \
    static formula Name(const formula& f,                   \
        unsigned min = 0U,                                  \
        unsigned max = unbounded())                         \
    {                                                       \
      return bunop(op::Name, f, min, max);                  \
    }
#else // !SWIG
#define SPOT_DEF_BUNOP(Name)                                \
    static formula Name(const formula& f,                   \
        unsigned min = 0U,                                  \
        unsigned max = unbounded())                         \
    {                                                       \
      return bunop(op::Name, f, min, max);                  \
    }                                                       \
    static formula Name(formula&& f,                        \
        unsigned min = 0U,                                  \
        unsigned max = unbounded())                         \
    {                                                       \
      return bunop(op::Name, std::move(f), min, max);       \
    }
#endif
    SPOT_DEF_BUNOP(Star);
 
    SPOT_DEF_BUNOP(FStar);
#undef SPOT_DEF_BUNOP
 
    static const formula nested_unop_range(op uo, op bo, unsigned min,
                                           unsigned max, formula f)
    {
      return formula(fnode::nested_unop_range(uo, bo, min, max,
                                              f.ptr_->clone()));
    }
 
    static formula sugar_goto(const formula& b, unsigned min, unsigned max);
 
    static formula sugar_equal(const formula& b, unsigned min, unsigned max);
 
    static formula sugar_delay(const formula& a, const formula& b,
                               unsigned min, unsigned max);
    static formula sugar_delay(const formula& b,
                               unsigned min, unsigned max);
 
#ifndef SWIG
    const fnode* to_node_()
    {
      auto tmp = ptr_;
      ptr_ = nullptr;
      return tmp;
    }
#endif
 
    op kind() const
    {
      return ptr_->kind();
    }
 
    std::string kindstr() const
    {
      return ptr_->kindstr();
    }
 
    bool is(op o) const
    {
      return ptr_->is(o);
    }
 
#ifndef SWIG
    bool is(op o1, op o2) const
    {
      return ptr_->is(o1, o2);
    }
 
    bool is(op o1, op o2, op o3) const
    {
      return ptr_->is(o1, o2, o3);
    }
 
    bool is(op o1, op o2, op o3, op o4) const
    {
      return ptr_->is(o1, o2, o3, o4);
    }
 
    bool is(std::initializer_list<op> l) const
    {
      return ptr_->is(l);
    }
#endif
 
    formula get_child_of(op o) const
    {
      auto f = ptr_->get_child_of(o);
      if (f)
        f->clone();
      return formula(f);
    }
 
#ifndef SWIG
    formula get_child_of(std::initializer_list<op> l) const
    {
      auto f = ptr_->get_child_of(l);
      if (f)
        f->clone();
      return formula(f);
    }
#endif
 
    unsigned min() const
    {
      return ptr_->min();
    }
 
    unsigned max() const
    {
      return ptr_->max();
    }
 
    unsigned size() const
    {
      return ptr_->size();
    }
 
    bool is_leaf() const
    {
      return ptr_->is_leaf();
    }
 
    size_t id() const
    {
      return ptr_->id();
    }
 
#ifndef SWIG
    class SPOT_API formula_child_iterator final
    {
      const fnode*const* ptr_;
    public:
      formula_child_iterator()
        : ptr_(nullptr)
      {
      }
 
      formula_child_iterator(const fnode*const* f)
        : ptr_(f)
      {
      }
 
      bool operator==(formula_child_iterator o)
      {
        return ptr_ == o.ptr_;
      }
 
      bool operator!=(formula_child_iterator o)
      {
        return ptr_ != o.ptr_;
      }
 
      formula operator*()
      {
        return formula((*ptr_)->clone());
      }
 
      formula_child_iterator operator++()
      {
        ++ptr_;
        return *this;
      }
 
      formula_child_iterator operator++(int)
      {
        auto tmp = *this;
        ++ptr_;
        return tmp;
      }
    };
 
    formula_child_iterator begin() const
    {
      return ptr_->begin();
    }
 
    formula_child_iterator end() const
    {
      return ptr_->end();
    }
 
    formula operator[](unsigned i) const
    {
      return formula(ptr_->nth(i)->clone());
    }
#endif
 
    static formula ff()
    {
      return formula(fnode::ff());
    }
 
    bool is_ff() const
    {
      return ptr_->is_ff();
    }
 
    static formula tt()
    {
      return formula(fnode::tt());
    }
 
    bool is_tt() const
    {
      return ptr_->is_tt();
    }
 
    static formula eword()
    {
      return formula(fnode::eword());
    }
 
    bool is_eword() const
    {
      return ptr_->is_eword();
    }
 
    bool is_constant() const
    {
      return ptr_->is_constant();
    }
 
    bool is_Kleene_star() const
    {
      return ptr_->is_Kleene_star();
    }
 
    static formula one_star()
    {
      // no need to clone, 1[*] is not reference counted
      return formula(fnode::one_star());
    }
 
    static formula one_plus()
    {
      // no need to clone, 1[+] is not reference counted
      return formula(fnode::one_plus());
    }
 
    bool is_literal() const
    {
      return (is(op::ap) ||
          // If f is in nenoform, Not can only occur in front of
          // an atomic proposition.  So this way we do not have
          // to check the type of the child.
          (is(op::Not) && is_boolean() && is_in_nenoform()));
    }
 
    const std::string& ap_name() const
    {
      return ptr_->ap_name();
    }
 
    std::ostream& dump(std::ostream& os) const
    {
      return ptr_->dump(os);
    }
 
    formula all_but(unsigned i) const
    {
      return formula(ptr_->all_but(i));
    }
 
    unsigned boolean_count() const
    {
      return ptr_->boolean_count();
    }
 
    formula boolean_operands(unsigned* width = nullptr) const
    {
      return formula(ptr_->boolean_operands(width));
    }
 
#define SPOT_DEF_PROP(Name)                        \
    bool Name() const                              \
    {                                              \
      return ptr_->Name();                         \
    }
    // Properties //
 
    SPOT_DEF_PROP(is_boolean);
    SPOT_DEF_PROP(is_sugar_free_boolean);
    SPOT_DEF_PROP(is_in_nenoform);
    SPOT_DEF_PROP(is_syntactic_stutter_invariant);
    SPOT_DEF_PROP(is_sugar_free_ltl);
    SPOT_DEF_PROP(is_ltl_formula);
    SPOT_DEF_PROP(is_psl_formula);
    SPOT_DEF_PROP(is_sere_formula);
    SPOT_DEF_PROP(is_finite);
    SPOT_DEF_PROP(is_eventual);
    SPOT_DEF_PROP(is_universal);
    SPOT_DEF_PROP(is_syntactic_safety);
    SPOT_DEF_PROP(is_syntactic_guarantee);
    SPOT_DEF_PROP(is_delta1);
    SPOT_DEF_PROP(is_syntactic_obligation);
    SPOT_DEF_PROP(is_sigma2);
    SPOT_DEF_PROP(is_pi2);
    SPOT_DEF_PROP(is_syntactic_recurrence);
    SPOT_DEF_PROP(is_syntactic_persistence);
    SPOT_DEF_PROP(is_delta2);
    SPOT_DEF_PROP(is_marked);
    SPOT_DEF_PROP(accepts_eword);
    SPOT_DEF_PROP(has_lbt_atomic_props);
    SPOT_DEF_PROP(has_spin_atomic_props);
#undef SPOT_DEF_PROP
 
    template<typename Trans, typename... Args>
      formula map(Trans trans, Args&&... args)
      {
        switch (op o = kind())
        {
          case op::ff:
          case op::tt:
          case op::eword:
          case op::ap:
            return *this;
          case op::Not:
          case op::X:
#if SPOT_HAS_STRONG_X
          case op::strong_X:
#endif
          case op::F:
          case op::G:
          case op::Closure:
          case op::NegClosure:
          case op::NegClosureMarked:
          case op::first_match:
            return unop(o, trans((*this)[0], std::forward<Args>(args)...));
          case op::Xor:
          case op::Implies:
          case op::Equiv:
          case op::U:
          case op::R:
          case op::W:
          case op::M:
          case op::EConcat:
          case op::EConcatMarked:
          case op::UConcat:
            {
              formula tmp = trans((*this)[0], std::forward<Args>(args)...);
              return binop(o, tmp,
                           trans((*this)[1], std::forward<Args>(args)...));
            }
          case op::Or:
          case op::OrRat:
          case op::And:
          case op::AndRat:
          case op::AndNLM:
          case op::Concat:
          case op::Fusion:
            {
              std::vector<formula> tmp;
              tmp.reserve(size());
              for (auto f: *this)
                tmp.emplace_back(trans(f, std::forward<Args>(args)...));
              return multop(o, std::move(tmp));
            }
          case op::Star:
          case op::FStar:
            return bunop(o, trans((*this)[0], std::forward<Args>(args)...),
                         min(), max());
        }
        SPOT_UNREACHABLE();
      }
 
    template<typename Func, typename... Args>
      void traverse(Func func, Args&&... args)
      {
        if (func(*this, std::forward<Args>(args)...))
          return;
        for (auto f: *this)
          f.traverse(func, std::forward<Args>(args)...);
      }
 
  private:
#ifndef SWIG
    [[noreturn]] static void report_ap_invalid_arg();
#endif
  };
 
  SPOT_API
    std::ostream& print_formula_props(std::ostream& out, const formula& f,
        bool abbreviated = false);
 
  SPOT_API
    std::list<std::string> list_formula_props(const formula& f);
 
  SPOT_API
    std::ostream& operator<<(std::ostream& os, const formula& f);
}
 
#ifndef SWIG
namespace std
{
  template <>
    struct hash<spot::formula>
    {
      size_t operator()(const spot::formula& x) const noexcept
      {
        return x.id();
      }
    };
}
#endif