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>
 
// strong_X was conditionally defined starting with version 2.9.
// You had to "#define SPOT_USES_STRONG_X 1" before including this
// file to get the definition.  Since Spot 2.13, it is always defined,
// so users may have to update their code.  The following macro
// is only defined when strong_X exists.
#  define SPOT_HAS_STRONG_X 1
// This was defined since 2.9 along with SPOT_HAS_STRONG_X when
// SPOT_USES_STRONG_X was defined so we are keeping it just in case
// someone depends on it.
#  define SPOT_WANT_STRONG_X 1
// This was defined in Spot 2.15 when exists/forall where introduced.
#  define SPOT_HAS_QUANTIFIERS 1
 
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,               
    // strong_X was introduced in Spot 2.9, but was hidden from the
    // public API by default in order not to break existing code.
    //
    // Starting with Spot 2.13, strong_X will be part of the public
    // API by default.  If you have a switch case listing all possible
    // operators, strong_X needs to be part of it.  If you have code
    // using Spot but that you also want to support versions older
    // than 2.13, there are two ways to do that
    //
    // Option 1: define SPOT_USES_STRONG_X before including this file.
    //
    //   #define SPOT_USES_STRONG_X 1
    //   #include <spot/tl/formula.hh>
    //
    // This will force any version of Spot since 2.9 to define
    // strong_X.  It won't work with older Spot versions, where
    // strong_X did not exist.
    //
    // Option 2: make any code using strong_X conditional on
    // SPOT_HAS_STRONG_X.  Typically, a switch over all possible
    // operators would include something like this:
    //
    //   #if SPOT_HAS_STRONG_X
    //      case op::strong_X:
    //         /* do something */
    //   #endif
    //
    // The two options are not mutually exclusive.  Using both allows
    // you to use strong_X whenever it exists.
    strong_X,                  
    // The following two operators are new in Spot 2.15
    // If you need to support an earlier version of Spot, you can
    // use the SPOT_HAS_QUANTIFIERS variable.
    //
    //   #if SPOT_HAS_QUANTIFIERS
    //      case op::exists:
    //         /* do something */
    //      case op::forall:
    //         /* do something */
    //   #endif
    exists,                    
    forall,                    
  };
 
#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, const fnode* f, const fnode* g);
      static const fnode* multop(op o, std::vector<const fnode*> l);
      template<op o>
      static const fnode* multop_build_and_or(const fnode* left,
                                              const fnode* right);
      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);

      static const fnode* quantify(op quantifier,
                                   const fnode* ap,
                                   const fnode* f);
      static const fnode* quantify(op quantifier,
                                   std::vector<const fnode*> aps,
                                   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 range_.min;
      }

      unsigned max() const
      {
        if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
          report_max_invalid_arg();
        return range_.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 range_.min == 0 && range_.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;

      unsigned apid() const
      {
        if (SPOT_UNLIKELY(op_ != op::ap))
          report_apid_on_nonap();
        return ap_id_;
      }

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

      bool is_quantified() const
      {
        return is_.quantified;
      }
 
    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();
      [[noreturn]] static void report_apid_on_nonap();
 
      static const fnode* unique(fnode*);
      static const fnode* multop_sorted(op o, std::vector<const fnode*>&& l);
 
      // 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_,ap_id_,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&max (aka ap_id_) are not initialized.  So to benefit
        // from the initialization optimization and the
        // is_Kleene_star() optimization in Clang, we always
        // initialize ap_id_ with this compiler.  Do not do it the
        // rest of the time, since the optimization is not done.
        : op_(o),
#if __llvm__
        saturated_(saturated), ap_id_(0)
#else
        saturated_(saturated)
#endif
      {
        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), saturated_(saturated), size_(1)
      {
        range_.min = min;
        range_.max = max;
        children[0] = f;
        setup_props(o);
      }
 
      fnode(op o, uint16_t apid, bool saturated = false)
        : op_(o), saturated_(saturated), size_(0)
      {
        ap_id_ = apid;
        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
      mutable uint8_t saturated_;
      struct range_t
      {
        uint8_t min;     // range minimum (for star-like operators)
        uint8_t max;     // range maximum;
      };
      union
      {
        range_t range_;
        uint16_t ap_id_;           // id for atomic proposition
      };
      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 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 formulas, 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 (Π₂).
        bool quantified:1;             // Use forall/exists
      };
      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 formulas first.
        bool lib = left->is_boolean();
        if (lib != right->is_boolean())
          return lib;
 
        // We have two Boolean formulas
        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 id() assigned to each formula is the
        // number of formulas constructed so far, it is very unlikely
        // that we will ever reach a case were two different formulas
        // have the same hash.  This will happen only ever with have
        // produced 256**sizeof(size_t) formulas (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;
    }

    static unsigned apid_count() noexcept;
    static bool is_valid_apid(unsigned id) noexcept;
    static const std::string& apname_from_apid(unsigned id);
    static formula ap_from_apid(unsigned id);
    static std::vector<formula> apid_map();

    void throw_if_quantified(const char* message)
    {
      if (SPOT_UNLIKELY(is_quantified()))
        report_message(message);
    }

    // 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);
    }

    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);
    }

    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
 
    static formula multop(op o, const formula& f, const formula& g)
    {
      return formula(fnode::multop(o, f.ptr_->clone(), g.ptr_->clone()));
    }
 
#ifndef SWIG
    static formula multop(op o, const formula& f, formula&& g)
    {
      return formula(fnode::multop(o, f.ptr_->clone(), g.to_node_()));
    }
 
    static formula multop(op o, formula&& f, const formula& g)
    {
      return formula(fnode::multop(o, f.to_node_(), g.ptr_->clone()));
    }
 
    static formula multop(op o, formula&& f, formula&& g)
    {
      return formula(fnode::multop(o, f.to_node_(), g.to_node_()));
    }
#endif // !SWIG
 
#ifdef SWIG
#define SPOT_DEF_MULTOP(Name)                                           \
    static formula Name(const std::vector<formula>& l)                  \
    {                                                                   \
      return multop(op::Name, l);                                       \
    }                                                                   \
                                                                        \
    static formula Name(const formula& left, const formula& right)      \
    {                                                                   \
      return multop(op::Name, left, right);                             \
    }
#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));                            \
    }                                                                   \
                                                                        \
    static formula Name(const formula& left, const formula& right)      \
    {                                                                   \
      return multop(op::Name, left, right);                             \
    }
#endif // !SWIG
#ifdef SWIG
#define SPOT_DEF_MULTOP2(Name)                                          \
    static formula Name(const std::vector<formula>& l)                  \
    {                                                                   \
      return multop(op::Name, l);                                       \
    }                                                                   \
                                                                        \
    static formula Name(const formula& left, const formula& right)      \
    {                                                                   \
      return formula(fnode::multop_build_and_or<op::Name>               \
                     (left->ptr_->clone(), right->ptr_->clone());       \
    }
#else // !SWIG
#define SPOT_DEF_MULTOP2(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));                            \
    }                                                                   \
                                                                        \
    static formula Name(const formula& left, const formula& right)      \
    {                                                                   \
      return formula(fnode::multop_build_and_or<op::Name>               \
                     (left.ptr_->clone(), right.ptr_->clone()));        \
    }                                                                   \
    static formula Name(const formula& left, formula&& right)           \
    {                                                                   \
      return formula(fnode::multop_build_and_or<op::Name>               \
                     (left.ptr_->clone(), right.to_node_()));           \
    }                                                                   \
    static formula Name(formula&& left, const formula& right)           \
    {                                                                   \
      return formula(fnode::multop_build_and_or<op::Name>               \
                     (left.to_node_(), right.ptr_->clone()));           \
    }                                                                   \
    static formula Name(formula&& left, formula&& right)                \
    {                                                                   \
      return formula(fnode::multop_build_and_or<op::Name>               \
                     (left.to_node_(), right.to_node_()));              \
    }
#endif // !SWIG
    SPOT_DEF_MULTOP2(Or);

    SPOT_DEF_MULTOP(OrRat);

    SPOT_DEF_MULTOP2(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 formula quantify(op quantifier,
                            formula&& ap,
                            formula&& f)
    {
      return formula(fnode::quantify(quantifier,
                                     ap.to_node_(),
                                     f.to_node_()));
    }
 
    static formula quantify(op quantifier,
                            const formula& ap,
                            const formula& f)
    {
      return formula(fnode::quantify(quantifier,
                                     ap.ptr_->clone(),
                                     f.ptr_->clone()));
    }
 
    static formula quantify(op quantifier,
                            const std::vector<formula>& aps,
                            const formula& f)
    {
      std::vector<const fnode*> tmp;
      tmp.reserve(aps.size() + 1);
      for (auto a: aps)
        if (a.ptr_)
          tmp.emplace_back(a.to_node_());
      return formula(fnode::quantify(quantifier, std::move(tmp),
                                     f.ptr_->clone()));
    }
 
#ifndef SWIG
    static formula quantify(op quantifier,
                            std::vector<formula>&& aps,
                            const formula& f)
    {
      std::vector<const fnode*> tmp;
      tmp.reserve(aps.size() + 1);
      for (auto a: aps)
        if (a.ptr_)
          tmp.emplace_back(a.to_node_());
      return formula(fnode::quantify(quantifier, std::move(tmp),
                                     f.ptr_->clone()));
    }
#endif // !SWIG
 
#define SPOT_DEF_QUANTIFY(Name)                                         \
    static formula Name(const std::vector<formula>& aps, const formula& f) \
    {                                                                   \
      return quantify(op::Name, aps, f);                                \
    }                                                                   \
                                                                        \
    static formula Name(const formula& ap, const formula& f)            \
    {                                                                   \
      return quantify(op::Name, ap, f);                                 \
    }

    SPOT_DEF_QUANTIFY(exists);

    SPOT_DEF_QUANTIFY(forall);
#undef SPOT_DEF_QUANTIFY

    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();
    }

    unsigned apid() const
    {
      return ptr_->apid();
    }

    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);
    SPOT_DEF_PROP(is_quantified);
#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:
          {
            formula arg = (*this)[0];
            formula new_arg = trans(arg, std::forward<Args>(args)...);
            if (arg == new_arg)
              return *this;
            else
              return unop(o, new_arg);
          }
        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 left = (*this)[0];
            formula right = (*this)[1];
            formula new_left = trans(left, std::forward<Args>(args)...);
            formula new_right = trans(right, std::forward<Args>(args)...);
            if (left == new_left && right == new_right)
              return *this;
            else
              return binop(o, new_left, new_right);
          }
        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;
            bool changed = false;
            tmp.reserve(size());
            for (auto f: *this)
              {
                formula g = trans(f, std::forward<Args>(args)...);
                tmp.emplace_back(g);
                changed |= g != f;
              }
            if (!changed)
              return *this;
            else
              return multop(o, std::move(tmp));
          }
        case op::Star:
        case op::FStar:
          {
            formula arg = (*this)[0];
            formula new_arg = trans(arg, std::forward<Args>(args)...);
            if (arg == new_arg)
              return *this;
            else
              return bunop(o, new_arg, min(), max());
          }
        case op::exists:
        case op::forall:
          {
            std::vector<formula> tmp;
            unsigned sz = size();
            tmp.reserve(sz - 1);
            bool changed = false;
            for (unsigned i = 0; i < sz - 1; ++i)
              {
                formula c = (*this)[i];
                formula g = trans(c, std::forward<Args>(args)...);
                changed |= c != g;
                tmp.push_back(g);
              }
            formula c = (*this)[sz - 1];
            formula g = trans(c, std::forward<Args>(args)...);
            if (c == g && !changed)
              return *this;
            return quantify(o, std::move(tmp), g);
          }
        }
      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)...);
    }
 
#ifndef SWIG
    [[noreturn]] static void report_message(const char* message);
  private:
    [[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