LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes - pbes_expression.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 237 260 91.2 %
Date: 2020-02-19 00:44:21 Functions: 103 112 92.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/pbes/pbes_expression.h
      10             : /// \brief The class pbes_expression.
      11             : 
      12             : #ifndef MCRL2_PBES_PBES_EXPRESSION_H
      13             : #define MCRL2_PBES_PBES_EXPRESSION_H
      14             : 
      15             : #include "mcrl2/data/expression_traits.h"
      16             : #include "mcrl2/data/optimized_boolean_operators.h"
      17             : #include "mcrl2/pbes/propositional_variable.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace pbes_system
      23             : {
      24             : 
      25             : typedef std::pair<core::identifier_string, data::data_expression_list> propositional_variable_key_type;
      26             : 
      27             : //--- start generated classes ---//
      28             : /// \brief A pbes expression
      29      637835 : class pbes_expression: public atermpp::aterm_appl
      30             : {
      31             :   public:
      32             :     /// \brief Default constructor.
      33      140902 :     pbes_expression()
      34      140902 :       : atermpp::aterm_appl(core::detail::default_values::PBExpr)
      35      140902 :     {}
      36             : 
      37             :     /// \brief Constructor.
      38             :     /// \param term A term
      39       56898 :     explicit pbes_expression(const atermpp::aterm& term)
      40       56898 :       : atermpp::aterm_appl(term)
      41             :     {
      42       56898 :       assert(core::detail::check_rule_PBExpr(*this));
      43       56898 :     }
      44             : 
      45             :     /// \brief Constructor.
      46       94224 :     pbes_expression(const data::data_expression& x)
      47       94224 :       : atermpp::aterm_appl(x)
      48       94224 :     {}
      49             : 
      50             :     /// \brief Constructor.
      51           9 :     pbes_expression(const data::variable& x)
      52           9 :       : atermpp::aterm_appl(x)
      53           9 :     {}
      54             : 
      55             :     /// \brief Constructor.
      56        1650 :     pbes_expression(const data::untyped_data_parameter& x)
      57        1650 :       : atermpp::aterm_appl(x)
      58        1650 :     {}
      59             : 
      60             :     /// Move semantics
      61      128542 :     pbes_expression(const pbes_expression&) noexcept = default;
      62       50346 :     pbes_expression(pbes_expression&&) noexcept = default;
      63             :     pbes_expression& operator=(const pbes_expression&) noexcept = default;
      64             :     pbes_expression& operator=(pbes_expression&&) noexcept = default;
      65             : };
      66             : 
      67             : /// \brief list of pbes_expressions
      68             : typedef atermpp::term_list<pbes_expression> pbes_expression_list;
      69             : 
      70             : /// \brief vector of pbes_expressions
      71             : typedef std::vector<pbes_expression>    pbes_expression_vector;
      72             : 
      73             : // prototypes
      74             : inline bool is_propositional_variable_instantiation(const atermpp::aterm_appl& x);
      75             : inline bool is_not(const atermpp::aterm_appl& x);
      76             : inline bool is_and(const atermpp::aterm_appl& x);
      77             : inline bool is_or(const atermpp::aterm_appl& x);
      78             : inline bool is_imp(const atermpp::aterm_appl& x);
      79             : inline bool is_forall(const atermpp::aterm_appl& x);
      80             : inline bool is_exists(const atermpp::aterm_appl& x);
      81             : 
      82             : /// \brief Test for a pbes_expression expression
      83             : /// \param x A term
      84             : /// \return True if \a x is a pbes_expression expression
      85             : inline
      86             : bool is_pbes_expression(const atermpp::aterm_appl& x)
      87             : {
      88             :   return data::is_data_expression(x) ||
      89             :          pbes_system::is_propositional_variable_instantiation(x) ||
      90             :          pbes_system::is_not(x) ||
      91             :          pbes_system::is_and(x) ||
      92             :          pbes_system::is_or(x) ||
      93             :          pbes_system::is_imp(x) ||
      94             :          pbes_system::is_forall(x) ||
      95             :          pbes_system::is_exists(x) ||
      96             :          data::is_variable(x) ||
      97             :          data::is_untyped_data_parameter(x);
      98             : }
      99             : 
     100             : // prototype declaration
     101             : std::string pp(const pbes_expression& x);
     102             : 
     103             : /// \brief Outputs the object to a stream
     104             : /// \param out An output stream
     105             : /// \param x Object x
     106             : /// \return The output stream
     107             : inline
     108        6503 : std::ostream& operator<<(std::ostream& out, const pbes_expression& x)
     109             : {
     110        6503 :   return out << pbes_system::pp(x);
     111             : }
     112             : 
     113             : /// \brief swap overload
     114             : inline void swap(pbes_expression& t1, pbes_expression& t2)
     115             : {
     116             :   t1.swap(t2);
     117             : }
     118             : 
     119             : 
     120             : /// \brief A propositional variable instantiation
     121       64427 : class propositional_variable_instantiation: public pbes_expression
     122             : {
     123             :   public:
     124             : 
     125             : 
     126             :     /// Move semantics
     127       27278 :     propositional_variable_instantiation(const propositional_variable_instantiation&) noexcept = default;
     128        3821 :     propositional_variable_instantiation(propositional_variable_instantiation&&) noexcept = default;
     129             :     propositional_variable_instantiation& operator=(const propositional_variable_instantiation&) noexcept = default;
     130             :     propositional_variable_instantiation& operator=(propositional_variable_instantiation&&) noexcept = default;
     131             : 
     132       71846 :     const core::identifier_string& name() const
     133             :     {
     134       71846 :       return atermpp::down_cast<core::identifier_string>((*this)[0]);
     135             :     }
     136             : 
     137       49090 :     const data::data_expression_list& parameters() const
     138             :     {
     139       49090 :       return atermpp::down_cast<data::data_expression_list>((*this)[1]);
     140             :     }
     141             : //--- start user section propositional_variable_instantiation ---//
     142             :     /// \brief Default constructor.
     143        6748 :     propositional_variable_instantiation()
     144        6748 :       : pbes_expression(core::detail::default_values::PropVarInst)
     145        6748 :     {}
     146             : 
     147             :     /// \brief Constructor.
     148             :     /// \param term A term
     149           8 :     explicit propositional_variable_instantiation(const atermpp::aterm& term)
     150           8 :       : pbes_expression(term)
     151             :     {
     152           8 :       assert(core::detail::check_term_PropVarInst(*this));
     153           8 :     }
     154             : 
     155             :     /// \brief Constructor.
     156       21686 :     propositional_variable_instantiation(const core::identifier_string& name, const data::data_expression_list& parameters)
     157       65058 :       : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PropVarInst(),
     158             :           name,
     159             :           parameters,
     160       43372 :           atermpp::aterm_int(core::index_traits<propositional_variable_instantiation, propositional_variable_key_type, 2>::insert(std::make_pair(name, parameters)))
     161       43372 :        ))
     162       21686 :     {}
     163             : 
     164             :     /// \brief Constructor.
     165        1732 :     propositional_variable_instantiation(const std::string& name, const data::data_expression_list& parameters)
     166        5196 :       : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PropVarInst(),
     167        3464 :           core::identifier_string(name),
     168             :           parameters,
     169        3464 :           atermpp::aterm_int(core::index_traits<propositional_variable_instantiation, propositional_variable_key_type, 2>::insert(std::make_pair(name, parameters)))
     170        3464 :         ))
     171        1732 :     {}
     172             : 
     173             : //--- end user section propositional_variable_instantiation ---//
     174             : };
     175             : 
     176             : /// \brief list of propositional_variable_instantiations
     177             : typedef atermpp::term_list<propositional_variable_instantiation> propositional_variable_instantiation_list;
     178             : 
     179             : /// \brief vector of propositional_variable_instantiations
     180             : typedef std::vector<propositional_variable_instantiation>    propositional_variable_instantiation_vector;
     181             : 
     182             : /// \brief Test for a propositional_variable_instantiation expression
     183             : /// \param x A term
     184             : /// \return True if \a x is a propositional_variable_instantiation expression
     185             : inline
     186      184667 : bool is_propositional_variable_instantiation(const atermpp::aterm_appl& x)
     187             : {
     188      184667 :   return x.function() == core::detail::function_symbols::PropVarInst;
     189             : }
     190             : 
     191             : // prototype declaration
     192             : std::string pp(const propositional_variable_instantiation& x);
     193             : 
     194             : /// \brief Outputs the object to a stream
     195             : /// \param out An output stream
     196             : /// \param x Object x
     197             : /// \return The output stream
     198             : inline
     199          74 : std::ostream& operator<<(std::ostream& out, const propositional_variable_instantiation& x)
     200             : {
     201          74 :   return out << pbes_system::pp(x);
     202             : }
     203             : 
     204             : /// \brief swap overload
     205             : inline void swap(propositional_variable_instantiation& t1, propositional_variable_instantiation& t2)
     206             : {
     207             :   t1.swap(t2);
     208             : }
     209             : 
     210             : 
     211             : /// \brief The not operator for pbes expressions
     212         898 : class not_: public pbes_expression
     213             : {
     214             :   public:
     215             :     /// \brief Default constructor.
     216             :     not_()
     217             :       : pbes_expression(core::detail::default_values::PBESNot)
     218             :     {}
     219             : 
     220             :     /// \brief Constructor.
     221             :     /// \param term A term
     222           0 :     explicit not_(const atermpp::aterm& term)
     223           0 :       : pbes_expression(term)
     224             :     {
     225           0 :       assert(core::detail::check_term_PBESNot(*this));
     226           0 :     }
     227             : 
     228             :     /// \brief Constructor.
     229         898 :     not_(const pbes_expression& operand)
     230         898 :       : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESNot(), operand))
     231         898 :     {}
     232             : 
     233             :     /// Move semantics
     234             :     not_(const not_&) noexcept = default;
     235             :     not_(not_&&) noexcept = default;
     236             :     not_& operator=(const not_&) noexcept = default;
     237             :     not_& operator=(not_&&) noexcept = default;
     238             : 
     239        1447 :     const pbes_expression& operand() const
     240             :     {
     241        1447 :       return atermpp::down_cast<pbes_expression>((*this)[0]);
     242             :     }
     243             : };
     244             : 
     245             : /// \brief Test for a not expression
     246             : /// \param x A term
     247             : /// \return True if \a x is a not expression
     248             : inline
     249      117560 : bool is_not(const atermpp::aterm_appl& x)
     250             : {
     251      117560 :   return x.function() == core::detail::function_symbols::PBESNot;
     252             : }
     253             : 
     254             : // prototype declaration
     255             : std::string pp(const not_& x);
     256             : 
     257             : /// \brief Outputs the object to a stream
     258             : /// \param out An output stream
     259             : /// \param x Object x
     260             : /// \return The output stream
     261             : inline
     262             : std::ostream& operator<<(std::ostream& out, const not_& x)
     263             : {
     264             :   return out << pbes_system::pp(x);
     265             : }
     266             : 
     267             : /// \brief swap overload
     268             : inline void swap(not_& t1, not_& t2)
     269             : {
     270             :   t1.swap(t2);
     271             : }
     272             : 
     273             : 
     274             : /// \brief The and operator for pbes expressions
     275        6309 : class and_: public pbes_expression
     276             : {
     277             :   public:
     278             :     /// \brief Default constructor.
     279             :     and_()
     280             :       : pbes_expression(core::detail::default_values::PBESAnd)
     281             :     {}
     282             : 
     283             :     /// \brief Constructor.
     284             :     /// \param term A term
     285             :     explicit and_(const atermpp::aterm& term)
     286             :       : pbes_expression(term)
     287             :     {
     288             :       assert(core::detail::check_term_PBESAnd(*this));
     289             :     }
     290             : 
     291             :     /// \brief Constructor.
     292        6309 :     and_(const pbes_expression& left, const pbes_expression& right)
     293        6309 :       : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESAnd(), left, right))
     294        6309 :     {}
     295             : 
     296             :     /// Move semantics
     297             :     and_(const and_&) noexcept = default;
     298             :     and_(and_&&) noexcept = default;
     299             :     and_& operator=(const and_&) noexcept = default;
     300             :     and_& operator=(and_&&) noexcept = default;
     301             : 
     302       48200 :     const pbes_expression& left() const
     303             :     {
     304       48200 :       return atermpp::down_cast<pbes_expression>((*this)[0]);
     305             :     }
     306             : 
     307       44924 :     const pbes_expression& right() const
     308             :     {
     309       44924 :       return atermpp::down_cast<pbes_expression>((*this)[1]);
     310             :     }
     311             : };
     312             : 
     313             : /// \brief Test for a and expression
     314             : /// \param x A term
     315             : /// \return True if \a x is a and expression
     316             : inline
     317      139710 : bool is_and(const atermpp::aterm_appl& x)
     318             : {
     319      139710 :   return x.function() == core::detail::function_symbols::PBESAnd;
     320             : }
     321             : 
     322             : // prototype declaration
     323             : std::string pp(const and_& x);
     324             : 
     325             : /// \brief Outputs the object to a stream
     326             : /// \param out An output stream
     327             : /// \param x Object x
     328             : /// \return The output stream
     329             : inline
     330             : std::ostream& operator<<(std::ostream& out, const and_& x)
     331             : {
     332             :   return out << pbes_system::pp(x);
     333             : }
     334             : 
     335             : /// \brief swap overload
     336             : inline void swap(and_& t1, and_& t2)
     337             : {
     338             :   t1.swap(t2);
     339             : }
     340             : 
     341             : 
     342             : /// \brief The or operator for pbes expressions
     343        4985 : class or_: public pbes_expression
     344             : {
     345             :   public:
     346             :     /// \brief Default constructor.
     347             :     or_()
     348             :       : pbes_expression(core::detail::default_values::PBESOr)
     349             :     {}
     350             : 
     351             :     /// \brief Constructor.
     352             :     /// \param term A term
     353         220 :     explicit or_(const atermpp::aterm& term)
     354         220 :       : pbes_expression(term)
     355             :     {
     356         220 :       assert(core::detail::check_term_PBESOr(*this));
     357         220 :     }
     358             : 
     359             :     /// \brief Constructor.
     360        4765 :     or_(const pbes_expression& left, const pbes_expression& right)
     361        4765 :       : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESOr(), left, right))
     362        4765 :     {}
     363             : 
     364             :     /// Move semantics
     365             :     or_(const or_&) noexcept = default;
     366             :     or_(or_&&) noexcept = default;
     367             :     or_& operator=(const or_&) noexcept = default;
     368             :     or_& operator=(or_&&) noexcept = default;
     369             : 
     370       42747 :     const pbes_expression& left() const
     371             :     {
     372       42747 :       return atermpp::down_cast<pbes_expression>((*this)[0]);
     373             :     }
     374             : 
     375       25361 :     const pbes_expression& right() const
     376             :     {
     377       25361 :       return atermpp::down_cast<pbes_expression>((*this)[1]);
     378             :     }
     379             : };
     380             : 
     381             : /// \brief Test for a or expression
     382             : /// \param x A term
     383             : /// \return True if \a x is a or expression
     384             : inline
     385       79172 : bool is_or(const atermpp::aterm_appl& x)
     386             : {
     387       79172 :   return x.function() == core::detail::function_symbols::PBESOr;
     388             : }
     389             : 
     390             : // prototype declaration
     391             : std::string pp(const or_& x);
     392             : 
     393             : /// \brief Outputs the object to a stream
     394             : /// \param out An output stream
     395             : /// \param x Object x
     396             : /// \return The output stream
     397             : inline
     398             : std::ostream& operator<<(std::ostream& out, const or_& x)
     399             : {
     400             :   return out << pbes_system::pp(x);
     401             : }
     402             : 
     403             : /// \brief swap overload
     404             : inline void swap(or_& t1, or_& t2)
     405             : {
     406             :   t1.swap(t2);
     407             : }
     408             : 
     409             : 
     410             : /// \brief The implication operator for pbes expressions
     411         899 : class imp: public pbes_expression
     412             : {
     413             :   public:
     414             :     /// \brief Default constructor.
     415             :     imp()
     416             :       : pbes_expression(core::detail::default_values::PBESImp)
     417             :     {}
     418             : 
     419             :     /// \brief Constructor.
     420             :     /// \param term A term
     421         182 :     explicit imp(const atermpp::aterm& term)
     422         182 :       : pbes_expression(term)
     423             :     {
     424         182 :       assert(core::detail::check_term_PBESImp(*this));
     425         182 :     }
     426             : 
     427             :     /// \brief Constructor.
     428         717 :     imp(const pbes_expression& left, const pbes_expression& right)
     429         717 :       : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESImp(), left, right))
     430         717 :     {}
     431             : 
     432             :     /// Move semantics
     433             :     imp(const imp&) noexcept = default;
     434             :     imp(imp&&) noexcept = default;
     435             :     imp& operator=(const imp&) noexcept = default;
     436             :     imp& operator=(imp&&) noexcept = default;
     437             : 
     438        3294 :     const pbes_expression& left() const
     439             :     {
     440        3294 :       return atermpp::down_cast<pbes_expression>((*this)[0]);
     441             :     }
     442             : 
     443        3289 :     const pbes_expression& right() const
     444             :     {
     445        3289 :       return atermpp::down_cast<pbes_expression>((*this)[1]);
     446             :     }
     447             : };
     448             : 
     449             : /// \brief Test for a imp expression
     450             : /// \param x A term
     451             : /// \return True if \a x is a imp expression
     452             : inline
     453       30959 : bool is_imp(const atermpp::aterm_appl& x)
     454             : {
     455       30959 :   return x.function() == core::detail::function_symbols::PBESImp;
     456             : }
     457             : 
     458             : // prototype declaration
     459             : std::string pp(const imp& x);
     460             : 
     461             : /// \brief Outputs the object to a stream
     462             : /// \param out An output stream
     463             : /// \param x Object x
     464             : /// \return The output stream
     465             : inline
     466             : std::ostream& operator<<(std::ostream& out, const imp& x)
     467             : {
     468             :   return out << pbes_system::pp(x);
     469             : }
     470             : 
     471             : /// \brief swap overload
     472             : inline void swap(imp& t1, imp& t2)
     473             : {
     474             :   t1.swap(t2);
     475             : }
     476             : 
     477             : 
     478             : /// \brief The universal quantification operator for pbes expressions
     479        1204 : class forall: public pbes_expression
     480             : {
     481             :   public:
     482             :     /// \brief Default constructor.
     483             :     forall()
     484             :       : pbes_expression(core::detail::default_values::PBESForall)
     485             :     {}
     486             : 
     487             :     /// \brief Constructor.
     488             :     /// \param term A term
     489          15 :     explicit forall(const atermpp::aterm& term)
     490          15 :       : pbes_expression(term)
     491             :     {
     492          15 :       assert(core::detail::check_term_PBESForall(*this));
     493          15 :     }
     494             : 
     495             :     /// \brief Constructor.
     496        1080 :     forall(const data::variable_list& variables, const pbes_expression& body)
     497        1080 :       : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESForall(), variables, body))
     498        1080 :     {}
     499             : 
     500             :     /// Move semantics
     501         109 :     forall(const forall&) noexcept = default;
     502             :     forall(forall&&) noexcept = default;
     503             :     forall& operator=(const forall&) noexcept = default;
     504             :     forall& operator=(forall&&) noexcept = default;
     505             : 
     506        5221 :     const data::variable_list& variables() const
     507             :     {
     508        5221 :       return atermpp::down_cast<data::variable_list>((*this)[0]);
     509             :     }
     510             : 
     511        5128 :     const pbes_expression& body() const
     512             :     {
     513        5128 :       return atermpp::down_cast<pbes_expression>((*this)[1]);
     514             :     }
     515             : };
     516             : 
     517             : /// \brief Test for a forall expression
     518             : /// \param x A term
     519             : /// \return True if \a x is a forall expression
     520             : inline
     521       28470 : bool is_forall(const atermpp::aterm_appl& x)
     522             : {
     523       28470 :   return x.function() == core::detail::function_symbols::PBESForall;
     524             : }
     525             : 
     526             : // prototype declaration
     527             : std::string pp(const forall& x);
     528             : 
     529             : /// \brief Outputs the object to a stream
     530             : /// \param out An output stream
     531             : /// \param x Object x
     532             : /// \return The output stream
     533             : inline
     534           0 : std::ostream& operator<<(std::ostream& out, const forall& x)
     535             : {
     536           0 :   return out << pbes_system::pp(x);
     537             : }
     538             : 
     539             : /// \brief swap overload
     540             : inline void swap(forall& t1, forall& t2)
     541             : {
     542             :   t1.swap(t2);
     543             : }
     544             : 
     545             : 
     546             : /// \brief The existential quantification operator for pbes expressions
     547         696 : class exists: public pbes_expression
     548             : {
     549             :   public:
     550             :     /// \brief Default constructor.
     551             :     exists()
     552             :       : pbes_expression(core::detail::default_values::PBESExists)
     553             :     {}
     554             : 
     555             :     /// \brief Constructor.
     556             :     /// \param term A term
     557           1 :     explicit exists(const atermpp::aterm& term)
     558           1 :       : pbes_expression(term)
     559             :     {
     560           1 :       assert(core::detail::check_term_PBESExists(*this));
     561           1 :     }
     562             : 
     563             :     /// \brief Constructor.
     564         580 :     exists(const data::variable_list& variables, const pbes_expression& body)
     565         580 :       : pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESExists(), variables, body))
     566         580 :     {}
     567             : 
     568             :     /// Move semantics
     569         115 :     exists(const exists&) noexcept = default;
     570             :     exists(exists&&) noexcept = default;
     571             :     exists& operator=(const exists&) noexcept = default;
     572             :     exists& operator=(exists&&) noexcept = default;
     573             : 
     574        3737 :     const data::variable_list& variables() const
     575             :     {
     576        3737 :       return atermpp::down_cast<data::variable_list>((*this)[0]);
     577             :     }
     578             : 
     579        3609 :     const pbes_expression& body() const
     580             :     {
     581        3609 :       return atermpp::down_cast<pbes_expression>((*this)[1]);
     582             :     }
     583             : };
     584             : 
     585             : /// \brief Test for a exists expression
     586             : /// \param x A term
     587             : /// \return True if \a x is a exists expression
     588             : inline
     589       22742 : bool is_exists(const atermpp::aterm_appl& x)
     590             : {
     591       22742 :   return x.function() == core::detail::function_symbols::PBESExists;
     592             : }
     593             : 
     594             : // prototype declaration
     595             : std::string pp(const exists& x);
     596             : 
     597             : /// \brief Outputs the object to a stream
     598             : /// \param out An output stream
     599             : /// \param x Object x
     600             : /// \return The output stream
     601             : inline
     602           0 : std::ostream& operator<<(std::ostream& out, const exists& x)
     603             : {
     604           0 :   return out << pbes_system::pp(x);
     605             : }
     606             : 
     607             : /// \brief swap overload
     608             : inline void swap(exists& t1, exists& t2)
     609             : {
     610             :   t1.swap(t2);
     611             : }
     612             : //--- end generated classes ---//
     613             : 
     614             : // template function overloads
     615             : std::string pp(const pbes_expression_list& x);
     616             : std::string pp(const pbes_expression_vector& x);
     617             : std::string pp(const propositional_variable_instantiation_list& x);
     618             : std::string pp(const propositional_variable_instantiation_vector& x);
     619             : std::set<pbes_system::propositional_variable_instantiation> find_propositional_variable_instantiations(const pbes_system::pbes_expression& x);
     620             : std::set<core::identifier_string> find_identifiers(const pbes_system::pbes_expression& x);
     621             : std::set<data::variable> find_free_variables(const pbes_system::pbes_expression& x);
     622             : bool search_variable(const pbes_system::pbes_expression& x, const data::variable& v);
     623             : pbes_system::pbes_expression normalize_sorts(const pbes_system::pbes_expression& x, const data::sort_specification& sortspec);
     624             : pbes_system::pbes_expression translate_user_notation(const pbes_system::pbes_expression& x);
     625             : 
     626             : /// \return Returns the value true
     627             : inline
     628       23526 : pbes_expression true_()
     629             : {
     630       23526 :   return data::sort_bool::true_();
     631             : }
     632             : 
     633             : /// \return Returns the value false
     634             : inline
     635       10029 : pbes_expression false_()
     636             : {
     637       10029 :   return data::sort_bool::false_();
     638             : }
     639             : 
     640             : /// \brief Test for the value true
     641             : /// \param t A PBES expression
     642             : /// \return True if it is the value \p true
     643       48873 : inline bool is_true(const pbes_expression& t)
     644             : {
     645       48873 :   return data::sort_bool::is_true_function_symbol(t);
     646             : }
     647             : 
     648             : /// \brief Test for the value false
     649             : /// \param t A PBES expression
     650             : /// \return True if it is the value \p false
     651       48762 : inline bool is_false(const pbes_expression& t)
     652             : {
     653       48762 :   return data::sort_bool::is_false_function_symbol(t);
     654             : }
     655             : 
     656             : /// \brief Returns true if the term t is a not expression
     657             : /// \param t A PBES expression
     658             : /// \return True if the term t is a not expression
     659         496 : inline bool is_pbes_not(const pbes_expression& t)
     660             : {
     661         496 :   return pbes_system::is_not(t);
     662             : }
     663             : 
     664             : /// \brief Returns true if the term t is an and expression
     665             : /// \param t A PBES expression
     666             : /// \return True if the term t is an and expression
     667       10458 : inline bool is_pbes_and(const pbes_expression& t)
     668             : {
     669       10458 :   return pbes_system::is_and(t);
     670             : }
     671             : 
     672             : /// \brief Returns true if the term t is an or expression
     673             : /// \param t A PBES expression
     674             : /// \return True if the term t is an or expression
     675        1889 : inline bool is_pbes_or(const pbes_expression& t)
     676             : {
     677        1889 :   return pbes_system::is_or(t);
     678             : }
     679             : 
     680             : /// \brief Returns true if the term t is an imp expression
     681             : /// \param t A PBES expression
     682             : /// \return True if the term t is an imp expression
     683             : inline bool is_pbes_imp(const pbes_expression& t)
     684             : {
     685             :   return pbes_system::is_imp(t);
     686             : }
     687             : 
     688             : /// \brief Returns true if the term t is a universal quantification
     689             : /// \param t A PBES expression
     690             : /// \return True if the term t is a universal quantification
     691             : inline bool is_pbes_forall(const pbes_expression& t)
     692             : {
     693             :   return pbes_system::is_forall(t);
     694             : }
     695             : 
     696             : /// \brief Returns true if the term t is an existential quantification
     697             : /// \param t A PBES expression
     698             : /// \return True if the term t is an existential quantification
     699             : inline bool is_pbes_exists(const pbes_expression& t)
     700             : {
     701             :   return pbes_system::is_exists(t);
     702             : }
     703             : 
     704             : /// \brief Test for a conjunction
     705             : /// \param t A PBES expression or a data expression
     706             : /// \return True if it is a conjunction
     707         110 : inline bool is_universal_not(const pbes_expression& t)
     708             : {
     709         110 :   return is_pbes_not(t) || data::sort_bool::is_not_application(t);
     710             : }
     711             : 
     712             : /// \brief Test for a conjunction
     713             : /// \param t A PBES expression or a data expression
     714             : /// \return True if it is a conjunction
     715           0 : inline bool is_universal_and(const pbes_expression& t)
     716             : {
     717           0 :   return is_pbes_and(t) || data::sort_bool::is_and_application(t);
     718             : }
     719             : 
     720             : /// \brief Test for a disjunction
     721             : /// \param t A PBES expression or a data expression
     722             : /// \return True if it is a disjunction
     723           0 : inline bool is_universal_or(const pbes_expression& t)
     724             : {
     725           0 :   return is_pbes_or(t) || data::sort_bool::is_or_application(t);
     726             : }
     727             : 
     728             : /// \brief Returns true if the term t is a data expression
     729             : /// \param t A PBES expression
     730             : /// \return True if the term t is a data expression
     731       17056 : inline bool is_data(const pbes_expression& t)
     732             : {
     733       17056 :   return data::is_data_expression(t);
     734             : }
     735             : 
     736             : /// \brief The namespace for accessor functions on pbes expressions.
     737             : namespace accessors
     738             : {
     739             : 
     740             : /// \brief Returns the pbes expression argument of expressions of type not, exists and forall.
     741             : /// \param t A PBES expression
     742             : /// \return The pbes expression argument of expressions of type not, exists and forall.
     743             : inline
     744         235 : const pbes_expression& arg(const pbes_expression& t)
     745             : {
     746         235 :   if (is_pbes_not(t))
     747             :   {
     748           3 :     return atermpp::down_cast<const pbes_expression>(t[0]);
     749             :   }
     750             :   else
     751             :   {
     752         232 :     assert(is_forall(t) || is_exists(t));
     753         232 :     return atermpp::down_cast<const pbes_expression>(t[1]);
     754             :   }
     755             : }
     756             : 
     757             : /// \brief Returns the pbes expression argument of expressions of type not, exists and forall.
     758             : /// \param t A PBES expression or a data expression
     759             : /// \return The pbes expression argument of expressions of type not, exists and forall.
     760             : inline
     761             : pbes_expression data_arg(const pbes_expression& t)
     762             : {
     763             :   if (data::is_data_expression(t))
     764             :   {
     765             :     assert(data::is_application(t));
     766             :     const auto& a = atermpp::down_cast<const data::application>(t);
     767             :     return *(a.begin());
     768             :   }
     769             :   else
     770             :   {
     771             :     return arg(t);
     772             :   }
     773             : }
     774             : 
     775             : /// \brief Returns the left hand side of an expression of type and, or or imp.
     776             : /// \param t A PBES expression
     777             : /// \return The left hand side of an expression of type and, or or imp.
     778             : inline
     779        5756 : const pbes_expression& left(const pbes_expression& t)
     780             : {
     781        5756 :   assert(is_and(t) || is_or(t) || is_imp(t));
     782        5756 :   return atermpp::down_cast<pbes_expression>(t[0]);
     783             : }
     784             : 
     785             : /// \brief Returns the left hand side of an expression of type and, or or imp.
     786             : /// \param x A PBES expression or a data expression
     787             : /// \return The left hand side of an expression of type and, or or imp.
     788             : inline
     789           3 : pbes_expression data_left(const pbes_expression& x)
     790             : {
     791           3 :   if (data::is_data_expression(x))
     792             :   {
     793           2 :     return data::binary_left(atermpp::down_cast<data::application>(x));
     794             :   }
     795             :   else
     796             :   {
     797           1 :     return left(x);
     798             :   }
     799             : }
     800             : 
     801             : /// \brief Returns the right hand side of an expression of type and, or or imp.
     802             : /// \param t A PBES expression
     803             : /// \return The right hand side of an expression of type and, or or imp.
     804             : inline
     805        5736 : const pbes_expression& right(const pbes_expression& t)
     806             : {
     807        5736 :   return atermpp::down_cast<pbes_expression>(t[1]);
     808             : }
     809             : 
     810             : /// \brief Returns the left hand side of an expression of type and, or or imp.
     811             : /// \param x A PBES expression or a data expression
     812             : /// \return The left hand side of an expression of type and, or or imp.
     813             : inline
     814           3 : pbes_expression data_right(const pbes_expression& x)
     815             : {
     816           3 :   if (data::is_data_expression(x))
     817             :   {
     818           2 :     return data::binary_right(atermpp::down_cast<data::application>(x));
     819             :   }
     820             :   else
     821             :   {
     822           1 :     return right(x);
     823             :   }
     824             : }
     825             : 
     826             : /// \brief Returns the variables of a quantification expression
     827             : /// \param t A PBES expression
     828             : /// \return The variables of a quantification expression
     829             : inline
     830           2 : const data::variable_list& var(const pbes_expression& t)
     831             : {
     832           2 :   assert(is_forall(t) || is_exists(t));
     833           2 :   return atermpp::down_cast<data::variable_list>(t[0]);
     834             : }
     835             : 
     836             : /// \brief Returns the name of a propositional variable expression
     837             : /// \param t A PBES expression
     838             : /// \return The name of a propositional variable expression
     839             : inline
     840           2 : const core::identifier_string& name(const pbes_expression& t)
     841             : {
     842           2 :   assert(is_propositional_variable_instantiation(t));
     843           2 :   return atermpp::down_cast<core::identifier_string>(t[0]);
     844             : }
     845             : 
     846             : /// \brief Returns the parameters of a propositional variable instantiation.
     847             : /// \param t A PBES expression
     848             : /// \return The parameters of a propositional variable instantiation.
     849             : inline
     850           2 : const data::data_expression_list& param(const pbes_expression& t)
     851             : {
     852           2 :   assert(is_propositional_variable_instantiation(t));
     853           2 :   return atermpp::down_cast<data::data_expression_list>(t[1]);
     854             : }
     855             : } // namespace accessors
     856             : 
     857             : /// \brief Make a universal quantification. It checks for an empty variable list,
     858             : /// which is not allowed.
     859             : /// \param l A sequence of data variables
     860             : /// \param p A PBES expression
     861             : /// \return The value <tt>forall l.p</tt>
     862             : inline
     863         720 : pbes_expression make_forall(const data::variable_list& l, const pbes_expression& p)
     864             : {
     865         720 :   if (l.empty())
     866             :   {
     867         240 :     return p;
     868             :   }
     869         480 :   return pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESForall(), l, p));
     870             : }
     871             : 
     872             : /// \brief Make an existential quantification. It checks for an empty variable list,
     873             : /// which is not allowed.
     874             : /// \param l A sequence of data variables
     875             : /// \param p A PBES expression
     876             : /// \return The value <tt>exists l.p</tt>
     877             : inline
     878        2875 : pbes_expression make_exists(const data::variable_list& l, const pbes_expression& p)
     879             : {
     880        2875 :   if (l.empty())
     881             :   {
     882        2174 :     return p;
     883             :   }
     884         701 :   return pbes_expression(atermpp::aterm_appl(core::detail::function_symbol_PBESExists(), l, p));
     885             : }
     886             : 
     887             : /// \brief Make a negation
     888             : /// \param p A PBES expression
     889             : /// \return The value <tt>!p</tt>
     890             : inline
     891             : pbes_expression optimized_not(const pbes_expression& p)
     892             : {
     893             :   return data::optimized_not(p);
     894             : }
     895             : 
     896             : /// \brief Make a conjunction
     897             : /// \param p A PBES expression
     898             : /// \param q A PBES expression
     899             : /// \return The value <tt>p && q</tt>
     900             : inline
     901        4790 : pbes_expression optimized_and(const pbes_expression& p, const pbes_expression& q)
     902             : {
     903        4790 :   return data::optimized_and(p, q);
     904             : }
     905             : 
     906             : /// \brief Make a disjunction
     907             : /// \param p A PBES expression
     908             : /// \param q A PBES expression
     909             : /// \return The value <tt>p || q</tt>
     910             : inline
     911         864 : pbes_expression optimized_or(const pbes_expression& p, const pbes_expression& q)
     912             : {
     913         864 :   return data::optimized_or(p, q);
     914             : }
     915             : 
     916             : /// \brief Make an implication
     917             : /// \param p A PBES expression
     918             : /// \param q A PBES expression
     919             : /// \return The value <tt>p => q</tt>
     920             : inline
     921         288 : pbes_expression optimized_imp(const pbes_expression& p, const pbes_expression& q)
     922             : {
     923         288 :   return data::optimized_imp(p, q);
     924             : }
     925             : 
     926             : /// \brief Make a universal quantification
     927             : /// If l is empty, p is returned.
     928             : /// \param l A sequence of data variables
     929             : /// \param p A PBES expression
     930             : /// \return The value <tt>forall l.p</tt>
     931             : inline
     932             : pbes_expression optimized_forall(const data::variable_list& l, const pbes_expression& p)
     933             : {
     934             :   if (l.empty())
     935             :   {
     936             :     return p;
     937             :   }
     938             :   if (is_false(p))
     939             :   {
     940             :     // N.B. Here we use the fact that mCRL2 data types are never empty.
     941             :     return data::sort_bool::false_();
     942             :   }
     943             :   if (is_true(p))
     944             :   {
     945             :     return true_();
     946             :   }
     947             :   return forall(l, p);
     948             : }
     949             : 
     950             : /// \brief Make an existential quantification
     951             : /// If l is empty, p is returned.
     952             : /// \param l A sequence of data variables
     953             : /// \param p A PBES expression
     954             : /// \return The value <tt>exists l.p</tt>
     955             : inline
     956             : pbes_expression optimized_exists(const data::variable_list& l, const pbes_expression& p)
     957             : {
     958             :   if (l.empty())
     959             :   {
     960             :     return p;
     961             :   }
     962             :   if (is_false(p))
     963             :   {
     964             :     return data::sort_bool::false_();
     965             :   }
     966             :   if (is_true(p))
     967             :   {
     968             :     // N.B. Here we use the fact that mCRL2 data types are never empty.
     969             :     return data::sort_bool::true_();
     970             :   }
     971             :   return exists(l, p);
     972             : }
     973             : 
     974             : inline
     975             : bool is_constant(const pbes_expression& x)
     976             : {
     977             :   return find_free_variables(x).empty();
     978             : }
     979             : 
     980             : inline
     981         165 : const data::variable_list& quantifier_variables(const pbes_expression& x)
     982             : {
     983         165 :   assert(is_exists(x) || is_forall(x));
     984         165 :   if (is_exists(x))
     985             :   {
     986           0 :     return atermpp::down_cast<exists>(x).variables();
     987             :   }
     988             :   else
     989             :   {
     990         165 :     return atermpp::down_cast<forall>(x).variables();
     991             :   }
     992             : }
     993             : 
     994             : inline
     995         486 : data::variable_list free_variables(const pbes_expression& x)
     996             : {
     997         972 :   std::set<data::variable> v = find_free_variables(x);
     998         972 :   return data::variable_list(v.begin(), v.end());
     999             : }
    1000             : 
    1001             : } // namespace pbes_system
    1002             : 
    1003             : } // namespace mcrl2
    1004             : 
    1005             : namespace mcrl2
    1006             : {
    1007             : 
    1008             : namespace core
    1009             : {
    1010             : 
    1011             : /// \brief Contains type information for pbes expressions.
    1012             : template <>
    1013             : struct term_traits<pbes_system::pbes_expression>
    1014             : {
    1015             :   /// \brief The term type
    1016             :   typedef pbes_system::pbes_expression term_type;
    1017             : 
    1018             :   /// \brief The data term type
    1019             :   typedef data::data_expression data_term_type;
    1020             : 
    1021             :   /// \brief The data term sequence type
    1022             :   typedef data::data_expression_list data_term_sequence_type;
    1023             : 
    1024             :   /// \brief The variable type
    1025             :   typedef data::variable variable_type;
    1026             : 
    1027             :   /// \brief The variable sequence type
    1028             :   typedef data::variable_list variable_sequence_type;
    1029             : 
    1030             :   /// \brief The propositional variable declaration type
    1031             :   typedef pbes_system::propositional_variable propositional_variable_decl_type;
    1032             : 
    1033             :   /// \brief The propositional variable instantiation type
    1034             :   typedef pbes_system::propositional_variable_instantiation propositional_variable_type;
    1035             : 
    1036             :   /// \brief The string type
    1037             :   typedef core::identifier_string string_type;
    1038             : 
    1039             :   /// \brief Make the value true
    1040             :   /// \return The value \p true
    1041             :   static inline
    1042        1006 :   term_type true_()
    1043             :   {
    1044        1006 :     return pbes_system::true_();
    1045             :   }
    1046             : 
    1047             :   /// \brief Make the value false
    1048             :   /// \return The value \p false
    1049             :   static inline
    1050        4839 :   term_type false_()
    1051             :   {
    1052        4839 :     return pbes_system::false_();
    1053             :   }
    1054             : 
    1055             :   /// \brief Make a negation
    1056             :   /// \param p A term
    1057             :   /// \return The value <tt>!p</tt>
    1058             :   static inline
    1059         256 :   term_type not_(const term_type& p)
    1060             :   {
    1061         256 :     return term_type(atermpp::aterm_appl(core::detail::function_symbol_PBESNot(), p));
    1062             :   }
    1063             : 
    1064             :   /// \brief Make a conjunction
    1065             :   /// \param p A term
    1066             :   /// \param q A term
    1067             :   /// \return The value <tt>p && q</tt>
    1068             :   static inline
    1069        6770 :   term_type and_(const term_type& p, const term_type& q)
    1070             :   {
    1071        6770 :     return term_type(atermpp::aterm_appl(core::detail::function_symbol_PBESAnd(), p,q));
    1072             :   }
    1073             : 
    1074             :   /// \brief Make a disjunction
    1075             :   /// \param p A term
    1076             :   /// \param q A term
    1077             :   /// \return The value <tt>p || q</tt>
    1078             :   static inline
    1079        2467 :   term_type or_(const term_type& p, const term_type& q)
    1080             :   {
    1081        2467 :     return term_type(atermpp::aterm_appl(core::detail::function_symbol_PBESOr(), p,q));
    1082             :   }
    1083             : 
    1084             :   template <typename FwdIt>
    1085             :   static inline
    1086           0 :   term_type join_or(FwdIt first, FwdIt last)
    1087             :   {
    1088           0 :     return utilities::detail::join(first, last, or_, false_());
    1089             :   }
    1090             : 
    1091             :   template <typename FwdIt>
    1092             :   static inline
    1093           0 :   term_type join_and(FwdIt first, FwdIt last)
    1094             :   {
    1095           0 :     return utilities::detail::join(first, last, and_, true_());
    1096             :   }
    1097             : 
    1098             :   /// \brief Make an implication
    1099             :   /// \param p A term
    1100             :   /// \param q A term
    1101             :   /// \return The value <tt>p => q</tt>
    1102             :   static inline
    1103         537 :   term_type imp(const term_type& p, const term_type& q)
    1104             :   {
    1105         537 :     return term_type(atermpp::aterm_appl(core::detail::function_symbol_PBESImp(), p, q));
    1106             :   }
    1107             : 
    1108             :   /// \brief Make a universal quantification
    1109             :   /// \param l A sequence of variables
    1110             :   /// \param p A term
    1111             :   /// \return The value <tt>forall l.p</tt>
    1112             :   static inline
    1113         206 :   term_type forall(const variable_sequence_type& l, const term_type& p)
    1114             :   {
    1115         206 :     if (l.empty())
    1116             :     {
    1117           0 :       return p;
    1118             :     }
    1119         206 :     return term_type(atermpp::aterm_appl(core::detail::function_symbol_PBESForall(), l, p));
    1120             :   }
    1121             : 
    1122             :   /// \brief Make an existential quantification
    1123             :   /// \param l A sequence of variables
    1124             :   /// \param p A term
    1125             :   /// \return The value <tt>exists l.p</tt>
    1126             :   static inline
    1127         185 :   term_type exists(const variable_sequence_type& l, const term_type& p)
    1128             :   {
    1129         185 :     if (l.empty())
    1130             :     {
    1131           0 :       return p;
    1132             :     }
    1133         185 :     return term_type(atermpp::aterm_appl(core::detail::function_symbol_PBESExists(), l, p));
    1134             :   }
    1135             : 
    1136             :   /// \brief Test for the value true
    1137             :   /// \param t A term
    1138             :   /// \return True if it is the value \p true
    1139             :   static inline
    1140       71836 :   bool is_true(const term_type& t)
    1141             :   {
    1142       71836 :     return data::sort_bool::is_true_function_symbol(t);
    1143             :   }
    1144             : 
    1145             :   /// \brief Test for the value false
    1146             :   /// \param t A term
    1147             :   /// \return True if it is the value \p false
    1148             :   static inline
    1149       49426 :   bool is_false(const term_type& t)
    1150             :   {
    1151       49426 :     return data::sort_bool::is_false_function_symbol(t);
    1152             :   }
    1153             : 
    1154             :   /// \brief Test for a negation
    1155             :   /// \param t A term
    1156             :   /// \return True if it is a negation
    1157             :   static inline
    1158         354 :   bool is_not(const term_type& t)
    1159             :   {
    1160         354 :     return pbes_system::is_not(t);
    1161             :   }
    1162             : 
    1163             :   /// \brief Test for a conjunction
    1164             :   /// \param t A term
    1165             :   /// \return True if it is a conjunction
    1166             :   static inline
    1167           1 :   bool is_and(const term_type& t)
    1168             :   {
    1169           1 :     return pbes_system::is_and(t);
    1170             :   }
    1171             : 
    1172             :   /// \brief Test for a disjunction
    1173             :   /// \param t A term
    1174             :   /// \return True if it is a disjunction
    1175             :   static inline
    1176           1 :   bool is_or(const term_type& t)
    1177             :   {
    1178           1 :     return pbes_system::is_or(t);
    1179             :   }
    1180             : 
    1181             :   /// \brief Test for an implication
    1182             :   /// \param t A term
    1183             :   /// \return True if it is an implication
    1184             :   static inline
    1185           1 :   bool is_imp(const term_type& t)
    1186             :   {
    1187           1 :     return pbes_system::is_imp(t);
    1188             :   }
    1189             : 
    1190             :   /// \brief Test for an universal quantification
    1191             :   /// \param t A term
    1192             :   /// \return True if it is a universal quantification
    1193             :   static inline
    1194           1 :   bool is_forall(const term_type& t)
    1195             :   {
    1196           1 :     return pbes_system::is_forall(t);
    1197             :   }
    1198             : 
    1199             :   /// \brief Test for an existential quantification
    1200             :   /// \param t A term
    1201             :   /// \return True if it is an existential quantification
    1202             :   static inline
    1203           2 :   bool is_exists(const term_type& t)
    1204             :   {
    1205           2 :     return pbes_system::is_exists(t);
    1206             :   }
    1207             : 
    1208             :   /// \brief Test for data term
    1209             :   /// \param t A term
    1210             :   /// \return True if the term is a data term
    1211             :   static inline
    1212             :   bool is_data(const term_type& t)
    1213             :   {
    1214             :     return data::is_data_expression(t);
    1215             :   }
    1216             : 
    1217             :   /// \brief Test for propositional variable instantiation
    1218             :   /// \param t A term
    1219             :   /// \return True if the term is a propositional variable instantiation
    1220             :   static inline
    1221             :   bool is_prop_var(const term_type& t)
    1222             :   {
    1223             :     return pbes_system::is_propositional_variable_instantiation(t);
    1224             :   }
    1225             : 
    1226             :   /// \brief Returns the left argument of a term of type and, or or imp
    1227             :   /// \param t A term
    1228             :   /// \return The left argument of the term. Also works for data terms
    1229             :   static inline
    1230           0 :   term_type left(const term_type& t)
    1231             :   {
    1232           0 :     return pbes_system::accessors::left(t);
    1233             :   }
    1234             : 
    1235             :   /// \brief Returns the right argument of a term of type and, or or imp
    1236             :   /// \param t A term
    1237             :   /// \return The right argument of the term. Also works for data terms
    1238             :   static inline
    1239           0 :   term_type right(const term_type& t)
    1240             :   {
    1241           0 :     return pbes_system::accessors::right(t);
    1242             :   }
    1243             : 
    1244             :   /// \brief Returns the argument of a term of type not
    1245             :   /// \param t A term
    1246             :   static inline
    1247         151 :   const term_type& not_arg(const term_type& t)
    1248             :   {
    1249         151 :     assert(is_pbes_not(t));
    1250         151 :     return atermpp::down_cast<term_type>(t[0]);
    1251             :   }
    1252             : 
    1253             :   /// \brief Returns the quantifier variables of a quantifier expression
    1254             :   /// \param t A term
    1255             :   /// \return The requested argument. Doesn't work for data terms
    1256             :   static inline
    1257           2 :   const variable_sequence_type& var(const term_type& t)
    1258             :   {
    1259             :     // Forall and exists are not fully supported by the data library
    1260           2 :     assert(!data::is_data_expression(t) || (!data::is_abstraction(t)
    1261             :                                             || (!data::is_forall(data::abstraction(t)) && !data::is_exists(data::abstraction(t)))));
    1262           2 :     assert(is_exists(t) || is_forall(t));
    1263             : 
    1264           2 :     return atermpp::down_cast<variable_sequence_type>(t[0]);
    1265             :   }
    1266             : 
    1267             :   /// \brief Returns the name of a propositional variable instantiation
    1268             :   /// \param t A term
    1269             :   /// \return The name of the propositional variable instantiation
    1270             :   static inline
    1271             :   const string_type &name(const term_type& t)
    1272             :   {
    1273             :     assert(is_prop_var(t));
    1274             :     return atermpp::down_cast<string_type>(t[0]);
    1275             :   }
    1276             : 
    1277             :   /// \brief Returns the parameter list of a propositional variable instantiation
    1278             :   /// \param t A term
    1279             :   /// \return The parameter list of the propositional variable instantiation
    1280             :   static inline
    1281             :   const data_term_sequence_type &param(const term_type& t)
    1282             :   {
    1283             :     assert(is_prop_var(t));
    1284             :     return atermpp::down_cast<data_term_sequence_type>(t[1]);
    1285             :   }
    1286             : 
    1287             :   /// \brief Conversion from variable to term
    1288             :   /// \param v A variable
    1289             :   /// \return The converted variable
    1290             :   static inline
    1291             :   const term_type& variable2term(const variable_type& v)
    1292             :   {
    1293             :     return atermpp::down_cast<term_type>(v);
    1294             :   }
    1295             : 
    1296             :   /// \brief Test if a term is a variable
    1297             :   /// \param t A term
    1298             :   /// \return True if the term is a variable
    1299             :   static inline
    1300             :   bool is_variable(const term_type& t)
    1301             :   {
    1302             :     return data::is_variable(t);
    1303             :   }
    1304             : 
    1305             :   /// \brief Pretty print function
    1306             :   /// \param t A term
    1307             :   /// \return Returns a pretty print representation of the term
    1308             :   static inline
    1309             :   std::string pp(const term_type& t)
    1310             :   {
    1311             :     return pbes_system::pp(t);
    1312             :   }
    1313             : };
    1314             : 
    1315             : } // namespace core
    1316             : 
    1317             : } // namespace mcrl2
    1318             : 
    1319             : namespace std
    1320             : {
    1321             : 
    1322             :   template <>
    1323             :   struct hash<mcrl2::pbes_system::pbes_expression>
    1324             :   {
    1325       17017 :     std::size_t operator()(const mcrl2::pbes_system::pbes_expression& x) const
    1326             :     {
    1327       17017 :       return hash<atermpp::aterm>()(x);
    1328             :     }
    1329             :   };
    1330             : 
    1331             :   template <>
    1332             :   struct hash<mcrl2::pbes_system::propositional_variable_instantiation>
    1333             :   {
    1334       17158 :     std::size_t operator()(const mcrl2::pbes_system::propositional_variable_instantiation& x) const
    1335             :     {
    1336       17158 :       return hash<atermpp::aterm>()(x);
    1337             :     }
    1338             :   };
    1339             : 
    1340             : } // namespace std
    1341             : 
    1342             : #include "mcrl2/pbes/index_traits.h"
    1343             : 
    1344             : #endif // MCRL2_PBES_PBES_EXPRESSION_H

Generated by: LCOV version 1.13