pbes_expression.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_PBES_PBES_EXPRESSION_H
#define MCRL2_PBES_PBES_EXPRESSION_H
 
#include "mcrl2/data/expression_traits.h"
#include "mcrl2/data/optimized_boolean_operators.h"
#include "mcrl2/pbes/propositional_variable.h"
 
namespace mcrl2
{
 
namespace pbes_system
{
 
//--- start generated classes ---//
class pbes_expression: public atermpp::aterm
{
  public:
    pbes_expression()
      : atermpp::aterm(core::detail::default_values::PBExpr)
    {}
 
    explicit pbes_expression(const atermpp::aterm& term)
      : atermpp::aterm(term)
    {
      assert(core::detail::check_rule_PBExpr(*this));
    }
 
    pbes_expression(const data::data_expression& x)
      : atermpp::aterm(x)
    {}
 
    pbes_expression(const data::variable& x)
      : atermpp::aterm(x)
    {}
 
    pbes_expression(const data::untyped_data_parameter& x)
      : atermpp::aterm(x)
    {}
 
    pbes_expression(const pbes_expression&) noexcept = default;
    pbes_expression(pbes_expression&&) noexcept = default;
    pbes_expression& operator=(const pbes_expression&) noexcept = default;
    pbes_expression& operator=(pbes_expression&&) noexcept = default;
};
 
typedef atermpp::term_list<pbes_expression> pbes_expression_list;
 
typedef std::vector<pbes_expression>    pbes_expression_vector;
 
// prototypes
inline bool is_propositional_variable_instantiation(const atermpp::aterm& x);
inline bool is_not(const atermpp::aterm& x);
inline bool is_and(const atermpp::aterm& x);
inline bool is_or(const atermpp::aterm& x);
inline bool is_imp(const atermpp::aterm& x);
inline bool is_forall(const atermpp::aterm& x);
inline bool is_exists(const atermpp::aterm& x);
 
inline
bool is_pbes_expression(const atermpp::aterm& x)
{
  return data::is_data_expression(x) ||
         data::is_variable(x) ||
         data::is_untyped_data_parameter(x) ||
         pbes_system::is_propositional_variable_instantiation(x) ||
         pbes_system::is_not(x) ||
         pbes_system::is_and(x) ||
         pbes_system::is_or(x) ||
         pbes_system::is_imp(x) ||
         pbes_system::is_forall(x) ||
         pbes_system::is_exists(x);
}
 
// prototype declaration
std::string pp(const pbes_expression& x);
 
inline
std::ostream& operator<<(std::ostream& out, const pbes_expression& x)
{
  return out << pbes_system::pp(x);
}
 
inline void swap(pbes_expression& t1, pbes_expression& t2)
{
  t1.swap(t2);
}
 
 
class propositional_variable_instantiation: public pbes_expression
{
  public:
 
 
    propositional_variable_instantiation(const propositional_variable_instantiation&) noexcept = default;
    propositional_variable_instantiation(propositional_variable_instantiation&&) noexcept = default;
    propositional_variable_instantiation& operator=(const propositional_variable_instantiation&) noexcept = default;
    propositional_variable_instantiation& operator=(propositional_variable_instantiation&&) noexcept = default;
 
    const core::identifier_string& name() const
    {
      return atermpp::down_cast<core::identifier_string>((*this)[0]);
    }
 
    const data::data_expression_list& parameters() const
    {
      return atermpp::down_cast<data::data_expression_list>((*this)[1]);
    }
//--- start user section propositional_variable_instantiation ---//
    propositional_variable_instantiation()
      : pbes_expression(core::detail::default_values::PropVarInst)
    {}
 
    explicit propositional_variable_instantiation(const atermpp::aterm& term)
      : pbes_expression(term)
    {
      assert(core::detail::check_term_PropVarInst(*this));
    }
 
    explicit propositional_variable_instantiation(const core::identifier_string& name, const data::data_expression_list& parameters)
    {
      atermpp::make_term_appl(*this,core::detail::function_symbol_PropVarInst(), name, parameters);
    }
 
    explicit propositional_variable_instantiation(const std::string& name, const data::data_expression_list& parameters)
      : propositional_variable_instantiation(core::identifier_string(name), parameters)
    {
    }
    
    explicit propositional_variable_instantiation(const core::identifier_string& name)
      : propositional_variable_instantiation(name, data::data_expression_list())
    {
    }
 
    explicit propositional_variable_instantiation(const std::string& name)
      : propositional_variable_instantiation(name, data::data_expression_list())
    {
    }
 
//--- end user section propositional_variable_instantiation ---//
};
 
template <class... ARGUMENTS>
inline void make_propositional_variable_instantiation(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_PropVarInst(), args...);
}
 
typedef atermpp::term_list<propositional_variable_instantiation> propositional_variable_instantiation_list;
 
typedef std::vector<propositional_variable_instantiation>    propositional_variable_instantiation_vector;
 
inline
bool is_propositional_variable_instantiation(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::PropVarInst;
}
 
// prototype declaration
std::string pp(const propositional_variable_instantiation& x);
 
inline
std::ostream& operator<<(std::ostream& out, const propositional_variable_instantiation& x)
{
  return out << pbes_system::pp(x);
}
 
inline void swap(propositional_variable_instantiation& t1, propositional_variable_instantiation& t2)
{
  t1.swap(t2);
}
 
 
class not_: public pbes_expression
{
  public:
    not_()
      : pbes_expression(core::detail::default_values::PBESNot)
    {}
 
    explicit not_(const atermpp::aterm& term)
      : pbes_expression(term)
    {
      assert(core::detail::check_term_PBESNot(*this));
    }
 
    explicit not_(const pbes_expression& operand)
      : pbes_expression(atermpp::aterm(core::detail::function_symbol_PBESNot(), operand))
    {}
 
    not_(const not_&) noexcept = default;
    not_(not_&&) noexcept = default;
    not_& operator=(const not_&) noexcept = default;
    not_& operator=(not_&&) noexcept = default;
 
    const pbes_expression& operand() const
    {
      return atermpp::down_cast<pbes_expression>((*this)[0]);
    }
};
 
template <class... ARGUMENTS>
inline void make_not_(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_PBESNot(), args...);
}
 
inline
bool is_not(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::PBESNot;
}
 
// prototype declaration
std::string pp(const not_& x);
 
inline
std::ostream& operator<<(std::ostream& out, const not_& x)
{
  return out << pbes_system::pp(x);
}
 
inline void swap(not_& t1, not_& t2)
{
  t1.swap(t2);
}
 
 
class and_: public pbes_expression
{
  public:
    and_()
      : pbes_expression(core::detail::default_values::PBESAnd)
    {}
 
    explicit and_(const atermpp::aterm& term)
      : pbes_expression(term)
    {
      assert(core::detail::check_term_PBESAnd(*this));
    }
 
    and_(const pbes_expression& left, const pbes_expression& right)
      : pbes_expression(atermpp::aterm(core::detail::function_symbol_PBESAnd(), left, right))
    {}
 
    and_(const and_&) noexcept = default;
    and_(and_&&) noexcept = default;
    and_& operator=(const and_&) noexcept = default;
    and_& operator=(and_&&) noexcept = default;
 
    const pbes_expression& left() const
    {
      return atermpp::down_cast<pbes_expression>((*this)[0]);
    }
 
    const pbes_expression& right() const
    {
      return atermpp::down_cast<pbes_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_and_(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_PBESAnd(), args...);
}
 
inline
bool is_and(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::PBESAnd;
}
 
// prototype declaration
std::string pp(const and_& x);
 
inline
std::ostream& operator<<(std::ostream& out, const and_& x)
{
  return out << pbes_system::pp(x);
}
 
inline void swap(and_& t1, and_& t2)
{
  t1.swap(t2);
}
 
 
class or_: public pbes_expression
{
  public:
    or_()
      : pbes_expression(core::detail::default_values::PBESOr)
    {}
 
    explicit or_(const atermpp::aterm& term)
      : pbes_expression(term)
    {
      assert(core::detail::check_term_PBESOr(*this));
    }
 
    or_(const pbes_expression& left, const pbes_expression& right)
      : pbes_expression(atermpp::aterm(core::detail::function_symbol_PBESOr(), left, right))
    {}
 
    or_(const or_&) noexcept = default;
    or_(or_&&) noexcept = default;
    or_& operator=(const or_&) noexcept = default;
    or_& operator=(or_&&) noexcept = default;
 
    const pbes_expression& left() const
    {
      return atermpp::down_cast<pbes_expression>((*this)[0]);
    }
 
    const pbes_expression& right() const
    {
      return atermpp::down_cast<pbes_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_or_(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_PBESOr(), args...);
}
 
inline
bool is_or(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::PBESOr;
}
 
// prototype declaration
std::string pp(const or_& x);
 
inline
std::ostream& operator<<(std::ostream& out, const or_& x)
{
  return out << pbes_system::pp(x);
}
 
inline void swap(or_& t1, or_& t2)
{
  t1.swap(t2);
}
 
 
class imp: public pbes_expression
{
  public:
    imp()
      : pbes_expression(core::detail::default_values::PBESImp)
    {}
 
    explicit imp(const atermpp::aterm& term)
      : pbes_expression(term)
    {
      assert(core::detail::check_term_PBESImp(*this));
    }
 
    imp(const pbes_expression& left, const pbes_expression& right)
      : pbes_expression(atermpp::aterm(core::detail::function_symbol_PBESImp(), left, right))
    {}
 
    imp(const imp&) noexcept = default;
    imp(imp&&) noexcept = default;
    imp& operator=(const imp&) noexcept = default;
    imp& operator=(imp&&) noexcept = default;
 
    const pbes_expression& left() const
    {
      return atermpp::down_cast<pbes_expression>((*this)[0]);
    }
 
    const pbes_expression& right() const
    {
      return atermpp::down_cast<pbes_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_imp(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_PBESImp(), args...);
}
 
inline
bool is_imp(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::PBESImp;
}
 
// prototype declaration
std::string pp(const imp& x);
 
inline
std::ostream& operator<<(std::ostream& out, const imp& x)
{
  return out << pbes_system::pp(x);
}
 
inline void swap(imp& t1, imp& t2)
{
  t1.swap(t2);
}
 
 
class forall: public pbes_expression
{
  public:
    forall()
      : pbes_expression(core::detail::default_values::PBESForall)
    {}
 
    explicit forall(const atermpp::aterm& term)
      : pbes_expression(term)
    {
      assert(core::detail::check_term_PBESForall(*this));
    }
 
    forall(const data::variable_list& variables, const pbes_expression& body)
      : pbes_expression(atermpp::aterm(core::detail::function_symbol_PBESForall(), variables, body))
    {}
 
    forall(const forall&) noexcept = default;
    forall(forall&&) noexcept = default;
    forall& operator=(const forall&) noexcept = default;
    forall& operator=(forall&&) noexcept = default;
 
    const data::variable_list& variables() const
    {
      return atermpp::down_cast<data::variable_list>((*this)[0]);
    }
 
    const pbes_expression& body() const
    {
      return atermpp::down_cast<pbes_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_forall(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_PBESForall(), args...);
}
 
inline
bool is_forall(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::PBESForall;
}
 
// prototype declaration
std::string pp(const forall& x);
 
inline
std::ostream& operator<<(std::ostream& out, const forall& x)
{
  return out << pbes_system::pp(x);
}
 
inline void swap(forall& t1, forall& t2)
{
  t1.swap(t2);
}
 
 
class exists: public pbes_expression
{
  public:
    exists()
      : pbes_expression(core::detail::default_values::PBESExists)
    {}
 
    explicit exists(const atermpp::aterm& term)
      : pbes_expression(term)
    {
      assert(core::detail::check_term_PBESExists(*this));
    }
 
    exists(const data::variable_list& variables, const pbes_expression& body)
      : pbes_expression(atermpp::aterm(core::detail::function_symbol_PBESExists(), variables, body))
    {}
 
    exists(const exists&) noexcept = default;
    exists(exists&&) noexcept = default;
    exists& operator=(const exists&) noexcept = default;
    exists& operator=(exists&&) noexcept = default;
 
    const data::variable_list& variables() const
    {
      return atermpp::down_cast<data::variable_list>((*this)[0]);
    }
 
    const pbes_expression& body() const
    {
      return atermpp::down_cast<pbes_expression>((*this)[1]);
    }
};
 
template <class... ARGUMENTS>
inline void make_exists(atermpp::aterm& t, const ARGUMENTS&... args)
{
  atermpp::make_term_appl(t, core::detail::function_symbol_PBESExists(), args...);
}
 
inline
bool is_exists(const atermpp::aterm& x)
{
  return x.function() == core::detail::function_symbols::PBESExists;
}
 
// prototype declaration
std::string pp(const exists& x);
 
inline
std::ostream& operator<<(std::ostream& out, const exists& x)
{
  return out << pbes_system::pp(x);
}
 
inline void swap(exists& t1, exists& t2)
{
  t1.swap(t2);
}
//--- end generated classes ---//
 
// template function overloads
std::string pp(const pbes_expression_list& x);
std::string pp(const pbes_expression_vector& x);
std::string pp(const propositional_variable_instantiation_list& x);
std::string pp(const propositional_variable_instantiation_vector& x);
std::set<pbes_system::propositional_variable_instantiation> find_propositional_variable_instantiations(const pbes_system::pbes_expression& x);
std::set<core::identifier_string> find_identifiers(const pbes_system::pbes_expression& x);
std::set<data::variable> find_free_variables(const pbes_system::pbes_expression& x);
bool search_variable(const pbes_system::pbes_expression& x, const data::variable& v);
pbes_system::pbes_expression normalize_sorts(const pbes_system::pbes_expression& x, const data::sort_specification& sortspec);
pbes_system::pbes_expression translate_user_notation(const pbes_system::pbes_expression& x);
 
inline
const pbes_expression& true_()
{
  /* The dynamic cast is required, to prevent copying the data term true to
     a local term on the stack. */
  return reinterpret_cast<const pbes_expression&>(data::sort_bool::true_());
}
 
inline
const pbes_expression& false_()
{
  /* The dynamic cast is required, to prevent copying the data term false to
     a local term on the stack. */
  return reinterpret_cast<const pbes_expression&>(data::sort_bool::false_());
}
 
inline bool is_true(const pbes_expression& t)
{
  return data::sort_bool::is_true_function_symbol(t);
}
 
inline bool is_false(const pbes_expression& t)
{
  return data::sort_bool::is_false_function_symbol(t);
}
 
inline bool is_pbes_not(const pbes_expression& t)
{
  return pbes_system::is_not(t);
}
 
inline bool is_pbes_and(const pbes_expression& t)
{
  return pbes_system::is_and(t);
}
 
inline bool is_pbes_or(const pbes_expression& t)
{
  return pbes_system::is_or(t);
}
 
inline bool is_pbes_imp(const pbes_expression& t)
{
  return pbes_system::is_imp(t);
}
 
inline bool is_pbes_forall(const pbes_expression& t)
{
  return pbes_system::is_forall(t);
}
 
inline bool is_pbes_exists(const pbes_expression& t)
{
  return pbes_system::is_exists(t);
}
 
inline bool is_universal_not(const pbes_expression& t)
{
  return is_pbes_not(t) || data::sort_bool::is_not_application(t);
}
 
inline bool is_universal_and(const pbes_expression& t)
{
  return is_pbes_and(t) || data::sort_bool::is_and_application(t);
}
 
inline bool is_universal_or(const pbes_expression& t)
{
  return is_pbes_or(t) || data::sort_bool::is_or_application(t);
}
 
inline bool is_data(const pbes_expression& t)
{
  return data::is_data_expression(t);
}
 
namespace accessors
{
 
inline
const pbes_expression& arg(const pbes_expression& t)
{
  if (is_pbes_not(t))
  {
    return atermpp::down_cast<const pbes_expression>(t[0]);
  }
  else
  {
    assert(is_forall(t) || is_exists(t));
    return atermpp::down_cast<const pbes_expression>(t[1]);
  }
}
 
inline
pbes_expression data_arg(const pbes_expression& t)
{
  if (data::is_data_expression(t))
  {
    assert(data::is_application(t));
    const auto& a = atermpp::down_cast<const data::application>(t);
    return *(a.begin());
  }
  else
  {
    return arg(t);
  }
}
 
inline
const pbes_expression& left(const pbes_expression& t)
{
  assert(is_and(t) || is_or(t) || is_imp(t));
  return atermpp::down_cast<pbes_expression>(t[0]);
}
 
inline
pbes_expression data_left(const pbes_expression& x)
{
  if (data::is_data_expression(x))
  {
    return data::binary_left(atermpp::down_cast<data::application>(x));
  }
  else
  {
    return left(x);
  }
}
 
inline
const pbes_expression& right(const pbes_expression& t)
{
  return atermpp::down_cast<pbes_expression>(t[1]);
}
 
inline
pbes_expression data_right(const pbes_expression& x)
{
  if (data::is_data_expression(x))
  {
    return data::binary_right(atermpp::down_cast<data::application>(x));
  }
  else
  {
    return right(x);
  }
}
 
inline
const data::variable_list& var(const pbes_expression& t)
{
  assert(is_forall(t) || is_exists(t));
  return atermpp::down_cast<data::variable_list>(t[0]);
}
 
inline
const core::identifier_string& name(const pbes_expression& t)
{
  assert(is_propositional_variable_instantiation(t));
  return atermpp::down_cast<core::identifier_string>(t[0]);
}
 
inline
const data::data_expression_list& param(const pbes_expression& t)
{
  assert(is_propositional_variable_instantiation(t));
  return atermpp::down_cast<data::data_expression_list>(t[1]);
}
} // namespace accessors
 
inline
pbes_expression make_forall_(const data::variable_list& l, const pbes_expression& p)
{
  if (l.empty())
  {
    return p;
  }
  return pbes_expression(atermpp::aterm(core::detail::function_symbol_PBESForall(), l, p));
}
 
inline
pbes_expression make_exists_(const data::variable_list& l, const pbes_expression& p)
{
  if (l.empty())
  {
    return p;
  }
  return pbes_expression(atermpp::aterm(core::detail::function_symbol_PBESExists(), l, p));
}
 
inline
void optimized_not(pbes_expression& result, const pbes_expression& p)
{
  data::optimized_not(result, p);
}
 
inline
void optimized_and(pbes_expression& result, const pbes_expression& p, const pbes_expression& q)
{
  data::optimized_and(result, p, q);
}
 
inline
void optimized_or(pbes_expression& result, const pbes_expression& p, const pbes_expression& q)
{
  data::optimized_or(result, p, q);
}
 
inline
void optimized_imp(pbes_expression& result, const pbes_expression& p, const pbes_expression& q)
{
  data::optimized_imp(result, p, q);
}
 
inline
void optimized_forall(pbes_expression& result, const data::variable_list& l, const pbes_expression& p)
{
  if (l.empty())
  {
    result = p;
    return;
  }
  if (is_false(p))
  {
    // N.B. Here we use the fact that mCRL2 data types are never empty.
    result = data::sort_bool::false_();
    return;
  }
  if (is_true(p))
  {
    result = true_();
    return;
  }
  pbes_system::make_forall(result, l, p);
  return;
}
 
inline
void optimized_exists(pbes_expression& result, const data::variable_list& l, const pbes_expression& p)
{
  if (l.empty())
  {
    result = p;
    return;
  }
  if (is_false(p))
  {
    result = data::sort_bool::false_();
    return;
  }
  if (is_true(p))
  {
    // N.B. Here we use the fact that mCRL2 data types are never empty.
    result = data::sort_bool::true_();
    return;
  }
  pbes_system::make_exists(result, l, p);
  return;
}
 
inline
bool is_constant(const pbes_expression& x)
{
  return find_free_variables(x).empty();
}
 
inline
const data::variable_list& quantifier_variables(const pbes_expression& x)
{
  assert(is_exists(x) || is_forall(x));
  if (is_exists(x))
  {
    return atermpp::down_cast<exists>(x).variables();
  }
  else
  {
    return atermpp::down_cast<forall>(x).variables();
  }
}
 
inline
data::variable_list free_variables(const pbes_expression& x)
{
  std::set<data::variable> v = find_free_variables(x);
  return data::variable_list(v.begin(), v.end());
}
 
} // namespace pbes_system
 
} // namespace mcrl2
 
namespace mcrl2
{
 
namespace core
{
 
template <>
struct term_traits<pbes_system::pbes_expression>
{
  typedef pbes_system::pbes_expression term_type;
 
  typedef data::data_expression data_term_type;
 
  typedef data::data_expression_list data_term_sequence_type;
 
  typedef data::variable variable_type;
 
  typedef data::variable_list variable_sequence_type;
 
  typedef pbes_system::propositional_variable propositional_variable_decl_type;
 
  typedef pbes_system::propositional_variable_instantiation propositional_variable_type;
 
  typedef core::identifier_string string_type;
 
  static inline
  term_type true_()
  {
    return pbes_system::true_();
  }
 
  static inline
  term_type false_()
  {
    return pbes_system::false_();
  }
 
  static inline
  term_type not_(const term_type& p)
  {
    return pbes_system::not_(p);
  }
 
  static inline
  void make_not_(term_type& result, const term_type& p)
  {
    pbes_system::make_not_(result, p);
  }
 
  static inline
  term_type and_(const term_type& p, const term_type& q)
  {
    return pbes_system::and_(p, q);
  }
 
  static inline
  void make_and_(term_type& result, const term_type& p, const term_type& q)
  {
    pbes_system::make_and_(result, p, q);
  }
 
  static inline
  term_type or_(const term_type& p, const term_type& q)
  {
    return pbes_system::or_(p, q);
  }
 
  static inline
  void make_or_(term_type& result, const term_type& p, const term_type& q)
  {
    pbes_system::make_or_(result, p,q);
  }
 
  template <typename FwdIt>
  static inline
  term_type join_or(FwdIt first, FwdIt last)
  {
    return utilities::detail::join(first, last, or_, false_());
  }
 
  template <typename FwdIt>
  static inline
  term_type join_and(FwdIt first, FwdIt last)
  {
    return utilities::detail::join(first, last, and_, true_());
  }
 
  static inline
  term_type imp(const term_type& p, const term_type& q)
  {
    return pbes_system::imp(p, q);
  }
 
  static inline
  void make_imp(term_type& result, const term_type& p, const term_type& q)
  {
    pbes_system::make_imp(result, p, q);
  }
 
  static inline
  term_type forall(const variable_sequence_type& l, const term_type& p)
  {
    if (l.empty())
    {
      return p;
    }
    return pbes_system::forall(l, p);
  }
 
  static inline
  void make_forall(term_type& result, const variable_sequence_type& l, const term_type& p)
  {
    if (l.empty())
    {
      result = p;
      return;
    }
    pbes_system::make_forall(result, l, p);
  }
 
  static inline
  term_type exists(const variable_sequence_type& l, const term_type& p)
  {
    if (l.empty())
    {
      return p;
    }
    return pbes_system::exists(l, p);
  }
 
  static inline
  void make_exists(term_type& result, const variable_sequence_type& l, const term_type& p)
  {
    if (l.empty())
    {
      result = p;
      return;
    }
    pbes_system::make_exists(result, l, p);
  }
 
  static inline
  bool is_true(const term_type& t)
  {
    return data::sort_bool::is_true_function_symbol(t);
  }
 
  static inline
  bool is_false(const term_type& t)
  {
    return data::sort_bool::is_false_function_symbol(t);
  }
 
  static inline
  bool is_not(const term_type& t)
  {
    return pbes_system::is_not(t);
  }
 
  static inline
  bool is_and(const term_type& t)
  {
    return pbes_system::is_and(t);
  }
 
  static inline
  bool is_or(const term_type& t)
  {
    return pbes_system::is_or(t);
  }
 
  static inline
  bool is_imp(const term_type& t)
  {
    return pbes_system::is_imp(t);
  }
 
  static inline
  bool is_forall(const term_type& t)
  {
    return pbes_system::is_forall(t);
  }
 
  static inline
  bool is_exists(const term_type& t)
  {
    return pbes_system::is_exists(t);
  }
 
  static inline
  bool is_data(const term_type& t)
  {
    return data::is_data_expression(t);
  }
 
  static inline
  bool is_prop_var(const term_type& t)
  {
    return pbes_system::is_propositional_variable_instantiation(t);
  }
 
  static inline
  term_type left(const term_type& t)
  {
    return pbes_system::accessors::left(t);
  }
 
  static inline
  term_type right(const term_type& t)
  {
    return pbes_system::accessors::right(t);
  }
 
  static inline
  const term_type& not_arg(const term_type& t)
  {
    assert(is_pbes_not(t));
    return atermpp::down_cast<term_type>(t[0]);
  }
 
  static inline
  const variable_sequence_type& var(const term_type& t)
  {
    // Forall and exists are not fully supported by the data library
    assert(!data::is_data_expression(t) || (!data::is_abstraction(t)
                                            || (!data::is_forall(data::abstraction(t)) && !data::is_exists(data::abstraction(t)))));
    assert(is_exists(t) || is_forall(t));
 
    return atermpp::down_cast<variable_sequence_type>(t[0]);
  }
 
  static inline
  const string_type &name(const term_type& t)
  {
    assert(is_prop_var(t));
    return atermpp::down_cast<string_type>(t[0]);
  }
 
  static inline
  const data_term_sequence_type &param(const term_type& t)
  {
    assert(is_prop_var(t));
    return atermpp::down_cast<data_term_sequence_type>(t[1]);
  }
 
  static inline
  const term_type& variable2term(const variable_type& v)
  {
    return atermpp::down_cast<term_type>(v);
  }
 
  static inline
  bool is_variable(const term_type& t)
  {
    return data::is_variable(t);
  }
 
  static inline
  std::string pp(const term_type& t)
  {
    return pbes_system::pp(t);
  }
};
 
} // namespace core
 
} // namespace mcrl2
 
namespace std
{
 
  template <>
  struct hash<mcrl2::pbes_system::pbes_expression>
  {
    std::size_t operator()(const mcrl2::pbes_system::pbes_expression& x) const
    {
      return hash<atermpp::aterm>()(x);
    }
  };
 
  template <>
  struct hash<mcrl2::pbes_system::propositional_variable_instantiation>
  {
    std::size_t operator()(const mcrl2::pbes_system::propositional_variable_instantiation& x) const
    {
      return hash<atermpp::aterm>()(x);
    }
  };
 
} // namespace std
 
#endif // MCRL2_PBES_PBES_EXPRESSION_H