LCOV - code coverage report
Current view: top level - bes/include/mcrl2/bes - boolean_expression.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 117 126 92.9 %
Date: 2020-10-20 00:45:57 Functions: 59 63 93.7 %
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/bes/boolean_expression.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_BES_BOOLEAN_EXPRESSION_H
      13             : #define MCRL2_BES_BOOLEAN_EXPRESSION_H
      14             : 
      15             : #include "mcrl2/core/detail/default_values.h"
      16             : #include "mcrl2/core/detail/soundness_checks.h"
      17             : #include "mcrl2/core/index_traits.h"
      18             : #include "mcrl2/core/print.h"
      19             : #include "mcrl2/core/term_traits.h"
      20             : 
      21             : namespace mcrl2
      22             : {
      23             : 
      24             : namespace bes
      25             : {
      26             : 
      27             : typedef core::identifier_string boolean_variable_key_type;
      28             : 
      29             : template <typename T> std::string pp(const T& x);
      30             : 
      31             : //--- start generated classes ---//
      32             : /// \brief A boolean expression
      33        4577 : class boolean_expression: public atermpp::aterm_appl
      34             : {
      35             :   public:
      36             :     /// \brief Default constructor.
      37          79 :     boolean_expression()
      38          79 :       : atermpp::aterm_appl(core::detail::default_values::BooleanExpression)
      39          79 :     {}
      40             : 
      41             :     /// \brief Constructor.
      42             :     /// \param term A term
      43         908 :     explicit boolean_expression(const atermpp::aterm& term)
      44         908 :       : atermpp::aterm_appl(term)
      45             :     {
      46         908 :       assert(core::detail::check_rule_BooleanExpression(*this));
      47         908 :     }
      48             : 
      49             :     /// Move semantics
      50        2065 :     boolean_expression(const boolean_expression&) noexcept = default;
      51        1278 :     boolean_expression(boolean_expression&&) noexcept = default;
      52             :     boolean_expression& operator=(const boolean_expression&) noexcept = default;
      53             :     boolean_expression& operator=(boolean_expression&&) noexcept = default;
      54             : };
      55             : 
      56             : /// \brief list of boolean_expressions
      57             : typedef atermpp::term_list<boolean_expression> boolean_expression_list;
      58             : 
      59             : /// \brief vector of boolean_expressions
      60             : typedef std::vector<boolean_expression>    boolean_expression_vector;
      61             : 
      62             : // prototypes
      63             : inline bool is_true(const atermpp::aterm_appl& x);
      64             : inline bool is_false(const atermpp::aterm_appl& x);
      65             : inline bool is_not(const atermpp::aterm_appl& x);
      66             : inline bool is_and(const atermpp::aterm_appl& x);
      67             : inline bool is_or(const atermpp::aterm_appl& x);
      68             : inline bool is_imp(const atermpp::aterm_appl& x);
      69             : inline bool is_boolean_variable(const atermpp::aterm_appl& x);
      70             : 
      71             : /// \brief Test for a boolean_expression expression
      72             : /// \param x A term
      73             : /// \return True if \a x is a boolean_expression expression
      74             : inline
      75             : bool is_boolean_expression(const atermpp::aterm_appl& x)
      76             : {
      77             :   return bes::is_true(x) ||
      78             :          bes::is_false(x) ||
      79             :          bes::is_not(x) ||
      80             :          bes::is_and(x) ||
      81             :          bes::is_or(x) ||
      82             :          bes::is_imp(x) ||
      83             :          bes::is_boolean_variable(x);
      84             : }
      85             : 
      86             : // prototype declaration
      87             : std::string pp(const boolean_expression& x);
      88             : 
      89             : /// \brief Outputs the object to a stream
      90             : /// \param out An output stream
      91             : /// \param x Object x
      92             : /// \return The output stream
      93             : inline
      94           0 : std::ostream& operator<<(std::ostream& out, const boolean_expression& x)
      95             : {
      96           0 :   return out << bes::pp(x);
      97             : }
      98             : 
      99             : /// \brief swap overload
     100             : inline void swap(boolean_expression& t1, boolean_expression& t2)
     101             : {
     102             :   t1.swap(t2);
     103             : }
     104             : 
     105             : 
     106             : /// \brief The value true for boolean expressions
     107         131 : class true_: public boolean_expression
     108             : {
     109             :   public:
     110             :     /// \brief Default constructor.
     111         125 :     true_()
     112         125 :       : boolean_expression(core::detail::default_values::BooleanTrue)
     113         125 :     {}
     114             : 
     115             :     /// \brief Constructor.
     116             :     /// \param term A term
     117             :     explicit true_(const atermpp::aterm& term)
     118             :       : boolean_expression(term)
     119             :     {
     120             :       assert(core::detail::check_term_BooleanTrue(*this));
     121             :     }
     122             : 
     123             :     /// Move semantics
     124           6 :     true_(const true_&) noexcept = default;
     125             :     true_(true_&&) noexcept = default;
     126             :     true_& operator=(const true_&) noexcept = default;
     127             :     true_& operator=(true_&&) noexcept = default;
     128             : };
     129             : 
     130             : /// \brief Test for a true expression
     131             : /// \param x A term
     132             : /// \return True if \a x is a true expression
     133             : inline
     134         406 : bool is_true(const atermpp::aterm_appl& x)
     135             : {
     136         406 :   return x.function() == core::detail::function_symbols::BooleanTrue;
     137             : }
     138             : 
     139             : // prototype declaration
     140             : std::string pp(const true_& x);
     141             : 
     142             : /// \brief Outputs the object to a stream
     143             : /// \param out An output stream
     144             : /// \param x Object x
     145             : /// \return The output stream
     146             : inline
     147             : std::ostream& operator<<(std::ostream& out, const true_& x)
     148             : {
     149             :   return out << bes::pp(x);
     150             : }
     151             : 
     152             : /// \brief swap overload
     153             : inline void swap(true_& t1, true_& t2)
     154             : {
     155             :   t1.swap(t2);
     156             : }
     157             : 
     158             : 
     159             : /// \brief The value false for boolean expressions
     160          56 : class false_: public boolean_expression
     161             : {
     162             :   public:
     163             :     /// \brief Default constructor.
     164          52 :     false_()
     165          52 :       : boolean_expression(core::detail::default_values::BooleanFalse)
     166          52 :     {}
     167             : 
     168             :     /// \brief Constructor.
     169             :     /// \param term A term
     170             :     explicit false_(const atermpp::aterm& term)
     171             :       : boolean_expression(term)
     172             :     {
     173             :       assert(core::detail::check_term_BooleanFalse(*this));
     174             :     }
     175             : 
     176             :     /// Move semantics
     177           4 :     false_(const false_&) noexcept = default;
     178             :     false_(false_&&) noexcept = default;
     179             :     false_& operator=(const false_&) noexcept = default;
     180             :     false_& operator=(false_&&) noexcept = default;
     181             : };
     182             : 
     183             : /// \brief Test for a false expression
     184             : /// \param x A term
     185             : /// \return True if \a x is a false expression
     186             : inline
     187         391 : bool is_false(const atermpp::aterm_appl& x)
     188             : {
     189         391 :   return x.function() == core::detail::function_symbols::BooleanFalse;
     190             : }
     191             : 
     192             : // prototype declaration
     193             : std::string pp(const false_& x);
     194             : 
     195             : /// \brief Outputs the object to a stream
     196             : /// \param out An output stream
     197             : /// \param x Object x
     198             : /// \return The output stream
     199             : inline
     200             : std::ostream& operator<<(std::ostream& out, const false_& x)
     201             : {
     202             :   return out << bes::pp(x);
     203             : }
     204             : 
     205             : /// \brief swap overload
     206             : inline void swap(false_& t1, false_& t2)
     207             : {
     208             :   t1.swap(t2);
     209             : }
     210             : 
     211             : 
     212             : /// \brief The not operator for boolean expressions
     213           1 : class not_: public boolean_expression
     214             : {
     215             :   public:
     216             :     /// \brief Default constructor.
     217             :     not_()
     218             :       : boolean_expression(core::detail::default_values::BooleanNot)
     219             :     {}
     220             : 
     221             :     /// \brief Constructor.
     222             :     /// \param term A term
     223             :     explicit not_(const atermpp::aterm& term)
     224             :       : boolean_expression(term)
     225             :     {
     226             :       assert(core::detail::check_term_BooleanNot(*this));
     227             :     }
     228             : 
     229             :     /// \brief Constructor.
     230           1 :     not_(const boolean_expression& operand)
     231           1 :       : boolean_expression(atermpp::aterm_appl(core::detail::function_symbol_BooleanNot(), operand))
     232           1 :     {}
     233             : 
     234             :     /// Move semantics
     235             :     not_(const not_&) noexcept = default;
     236             :     not_(not_&&) noexcept = default;
     237             :     not_& operator=(const not_&) noexcept = default;
     238             :     not_& operator=(not_&&) noexcept = default;
     239             : 
     240           0 :     const boolean_expression& operand() const
     241             :     {
     242           0 :       return atermpp::down_cast<boolean_expression>((*this)[0]);
     243             :     }
     244             : };
     245             : 
     246             : /// \brief Test for a not expression
     247             : /// \param x A term
     248             : /// \return True if \a x is a not expression
     249             : inline
     250         451 : bool is_not(const atermpp::aterm_appl& x)
     251             : {
     252         451 :   return x.function() == core::detail::function_symbols::BooleanNot;
     253             : }
     254             : 
     255             : // prototype declaration
     256             : std::string pp(const not_& x);
     257             : 
     258             : /// \brief Outputs the object to a stream
     259             : /// \param out An output stream
     260             : /// \param x Object x
     261             : /// \return The output stream
     262             : inline
     263             : std::ostream& operator<<(std::ostream& out, const not_& x)
     264             : {
     265             :   return out << bes::pp(x);
     266             : }
     267             : 
     268             : /// \brief swap overload
     269             : inline void swap(not_& t1, not_& t2)
     270             : {
     271             :   t1.swap(t2);
     272             : }
     273             : 
     274             : 
     275             : /// \brief The and operator for boolean expressions
     276         134 : class and_: public boolean_expression
     277             : {
     278             :   public:
     279             :     /// \brief Default constructor.
     280             :     and_()
     281             :       : boolean_expression(core::detail::default_values::BooleanAnd)
     282             :     {}
     283             : 
     284             :     /// \brief Constructor.
     285             :     /// \param term A term
     286             :     explicit and_(const atermpp::aterm& term)
     287             :       : boolean_expression(term)
     288             :     {
     289             :       assert(core::detail::check_term_BooleanAnd(*this));
     290             :     }
     291             : 
     292             :     /// \brief Constructor.
     293         134 :     and_(const boolean_expression& left, const boolean_expression& right)
     294         134 :       : boolean_expression(atermpp::aterm_appl(core::detail::function_symbol_BooleanAnd(), left, right))
     295         134 :     {}
     296             : 
     297             :     /// Move semantics
     298             :     and_(const and_&) noexcept = default;
     299             :     and_(and_&&) noexcept = default;
     300             :     and_& operator=(const and_&) noexcept = default;
     301             :     and_& operator=(and_&&) noexcept = default;
     302             : 
     303          57 :     const boolean_expression& left() const
     304             :     {
     305          57 :       return atermpp::down_cast<boolean_expression>((*this)[0]);
     306             :     }
     307             : 
     308          57 :     const boolean_expression& right() const
     309             :     {
     310          57 :       return atermpp::down_cast<boolean_expression>((*this)[1]);
     311             :     }
     312             : };
     313             : 
     314             : /// \brief Test for a and expression
     315             : /// \param x A term
     316             : /// \return True if \a x is a and expression
     317             : inline
     318         467 : bool is_and(const atermpp::aterm_appl& x)
     319             : {
     320         467 :   return x.function() == core::detail::function_symbols::BooleanAnd;
     321             : }
     322             : 
     323             : // prototype declaration
     324             : std::string pp(const and_& x);
     325             : 
     326             : /// \brief Outputs the object to a stream
     327             : /// \param out An output stream
     328             : /// \param x Object x
     329             : /// \return The output stream
     330             : inline
     331             : std::ostream& operator<<(std::ostream& out, const and_& x)
     332             : {
     333             :   return out << bes::pp(x);
     334             : }
     335             : 
     336             : /// \brief swap overload
     337             : inline void swap(and_& t1, and_& t2)
     338             : {
     339             :   t1.swap(t2);
     340             : }
     341             : 
     342             : 
     343             : /// \brief The or operator for boolean expressions
     344          33 : class or_: public boolean_expression
     345             : {
     346             :   public:
     347             :     /// \brief Default constructor.
     348             :     or_()
     349             :       : boolean_expression(core::detail::default_values::BooleanOr)
     350             :     {}
     351             : 
     352             :     /// \brief Constructor.
     353             :     /// \param term A term
     354             :     explicit or_(const atermpp::aterm& term)
     355             :       : boolean_expression(term)
     356             :     {
     357             :       assert(core::detail::check_term_BooleanOr(*this));
     358             :     }
     359             : 
     360             :     /// \brief Constructor.
     361          33 :     or_(const boolean_expression& left, const boolean_expression& right)
     362          33 :       : boolean_expression(atermpp::aterm_appl(core::detail::function_symbol_BooleanOr(), left, right))
     363          33 :     {}
     364             : 
     365             :     /// Move semantics
     366             :     or_(const or_&) noexcept = default;
     367             :     or_(or_&&) noexcept = default;
     368             :     or_& operator=(const or_&) noexcept = default;
     369             :     or_& operator=(or_&&) noexcept = default;
     370             : 
     371          44 :     const boolean_expression& left() const
     372             :     {
     373          44 :       return atermpp::down_cast<boolean_expression>((*this)[0]);
     374             :     }
     375             : 
     376          44 :     const boolean_expression& right() const
     377             :     {
     378          44 :       return atermpp::down_cast<boolean_expression>((*this)[1]);
     379             :     }
     380             : };
     381             : 
     382             : /// \brief Test for a or expression
     383             : /// \param x A term
     384             : /// \return True if \a x is a or expression
     385             : inline
     386         411 : bool is_or(const atermpp::aterm_appl& x)
     387             : {
     388         411 :   return x.function() == core::detail::function_symbols::BooleanOr;
     389             : }
     390             : 
     391             : // prototype declaration
     392             : std::string pp(const or_& x);
     393             : 
     394             : /// \brief Outputs the object to a stream
     395             : /// \param out An output stream
     396             : /// \param x Object x
     397             : /// \return The output stream
     398             : inline
     399             : std::ostream& operator<<(std::ostream& out, const or_& x)
     400             : {
     401             :   return out << bes::pp(x);
     402             : }
     403             : 
     404             : /// \brief swap overload
     405             : inline void swap(or_& t1, or_& t2)
     406             : {
     407             :   t1.swap(t2);
     408             : }
     409             : 
     410             : 
     411             : /// \brief The implication operator for boolean expressions
     412           3 : class imp: public boolean_expression
     413             : {
     414             :   public:
     415             :     /// \brief Default constructor.
     416             :     imp()
     417             :       : boolean_expression(core::detail::default_values::BooleanImp)
     418             :     {}
     419             : 
     420             :     /// \brief Constructor.
     421             :     /// \param term A term
     422             :     explicit imp(const atermpp::aterm& term)
     423             :       : boolean_expression(term)
     424             :     {
     425             :       assert(core::detail::check_term_BooleanImp(*this));
     426             :     }
     427             : 
     428             :     /// \brief Constructor.
     429           3 :     imp(const boolean_expression& left, const boolean_expression& right)
     430           3 :       : boolean_expression(atermpp::aterm_appl(core::detail::function_symbol_BooleanImp(), left, right))
     431           3 :     {}
     432             : 
     433             :     /// Move semantics
     434             :     imp(const imp&) noexcept = default;
     435             :     imp(imp&&) noexcept = default;
     436             :     imp& operator=(const imp&) noexcept = default;
     437             :     imp& operator=(imp&&) noexcept = default;
     438             : 
     439           5 :     const boolean_expression& left() const
     440             :     {
     441           5 :       return atermpp::down_cast<boolean_expression>((*this)[0]);
     442             :     }
     443             : 
     444           5 :     const boolean_expression& right() const
     445             :     {
     446           5 :       return atermpp::down_cast<boolean_expression>((*this)[1]);
     447             :     }
     448             : };
     449             : 
     450             : /// \brief Test for a imp expression
     451             : /// \param x A term
     452             : /// \return True if \a x is a imp expression
     453             : inline
     454         353 : bool is_imp(const atermpp::aterm_appl& x)
     455             : {
     456         353 :   return x.function() == core::detail::function_symbols::BooleanImp;
     457             : }
     458             : 
     459             : // prototype declaration
     460             : std::string pp(const imp& x);
     461             : 
     462             : /// \brief Outputs the object to a stream
     463             : /// \param out An output stream
     464             : /// \param x Object x
     465             : /// \return The output stream
     466             : inline
     467             : std::ostream& operator<<(std::ostream& out, const imp& x)
     468             : {
     469             :   return out << bes::pp(x);
     470             : }
     471             : 
     472             : /// \brief swap overload
     473             : inline void swap(imp& t1, imp& t2)
     474             : {
     475             :   t1.swap(t2);
     476             : }
     477             : 
     478             : 
     479             : /// \brief A boolean variable
     480        1624 : class boolean_variable: public boolean_expression
     481             : {
     482             :   public:
     483             : 
     484             : 
     485             :     /// Move semantics
     486         796 :     boolean_variable(const boolean_variable&) noexcept = default;
     487         251 :     boolean_variable(boolean_variable&&) noexcept = default;
     488             :     boolean_variable& operator=(const boolean_variable&) noexcept = default;
     489             :     boolean_variable& operator=(boolean_variable&&) noexcept = default;
     490             : 
     491         261 :     const core::identifier_string& name() const
     492             :     {
     493         261 :       return atermpp::down_cast<core::identifier_string>((*this)[0]);
     494             :     }
     495             : //--- start user section boolean_variable ---//
     496             :     /// \brief Default constructor.
     497           8 :     boolean_variable()
     498           8 :       : boolean_expression(core::detail::default_values::BooleanVariable)
     499           8 :     {}
     500             : 
     501             :     /// \brief Constructor.
     502             :     /// \param term A term
     503          18 :     explicit boolean_variable(const atermpp::aterm& term)
     504          18 :       : boolean_expression(term)
     505             :     {
     506          18 :       assert(core::detail::check_term_BooleanVariable(*this));
     507          18 :     }
     508             : 
     509             :     /// \brief Constructor.
     510         132 :     boolean_variable(const core::identifier_string& name)
     511         396 :       : boolean_expression(atermpp::aterm_appl(core::detail::function_symbol_BooleanVariable(),
     512             :           name,
     513         264 :           atermpp::aterm_int(core::index_traits<boolean_variable, boolean_variable_key_type, 1>::insert(name)
     514         264 :         )))
     515         132 :     {}
     516             : 
     517             :     /// \brief Constructor.
     518         402 :     boolean_variable(const std::string& name)
     519        1206 :       : boolean_expression(atermpp::aterm_appl(core::detail::function_symbol_BooleanVariable(),
     520         804 :           core::identifier_string(name),
     521         804 :           atermpp::aterm_int(core::index_traits<boolean_variable, boolean_variable_key_type, 1>::insert(name)
     522         804 :         )))
     523         402 :     {}
     524             : //--- end user section boolean_variable ---//
     525             : };
     526             : 
     527             : /// \brief Test for a boolean_variable expression
     528             : /// \param x A term
     529             : /// \return True if \a x is a boolean_variable expression
     530             : inline
     531         278 : bool is_boolean_variable(const atermpp::aterm_appl& x)
     532             : {
     533         278 :   return x.function() == core::detail::function_symbols::BooleanVariable;
     534             : }
     535             : 
     536             : // prototype declaration
     537             : std::string pp(const boolean_variable& x);
     538             : 
     539             : /// \brief Outputs the object to a stream
     540             : /// \param out An output stream
     541             : /// \param x Object x
     542             : /// \return The output stream
     543             : inline
     544           0 : std::ostream& operator<<(std::ostream& out, const boolean_variable& x)
     545             : {
     546           0 :   return out << bes::pp(x);
     547             : }
     548             : 
     549             : /// \brief swap overload
     550             : inline void swap(boolean_variable& t1, boolean_variable& t2)
     551             : {
     552             :   t1.swap(t2);
     553             : }
     554             : //--- end generated classes ---//
     555             : 
     556             : namespace accessors
     557             : {
     558             : inline
     559           2 : const boolean_expression& left(boolean_expression const& e)
     560             : {
     561           2 :   assert(is_and(e) || is_or(e) || is_imp(e));
     562           2 :   return atermpp::down_cast<boolean_expression>(e[0]);
     563             : }
     564             : 
     565             : inline
     566           2 : const boolean_expression& right(boolean_expression const& e)
     567             : {
     568           2 :   assert(is_and(e) || is_or(e) || is_imp(e));
     569           2 :   return atermpp::down_cast<boolean_expression>(e[1]);
     570             : }
     571             : 
     572             : } // namespace accessors
     573             : 
     574             : } // namespace bes
     575             : 
     576             : } // namespace mcrl2
     577             : 
     578             : namespace mcrl2
     579             : {
     580             : 
     581             : namespace core
     582             : {
     583             : 
     584             : /// \brief Contains type information for boolean expressions
     585             : template <>
     586             : struct term_traits<bes::boolean_expression>
     587             : {
     588             :   /// The term type
     589             :   typedef bes::boolean_expression term_type;
     590             : 
     591             :   /// \brief The variable type
     592             :   typedef bes::boolean_variable variable_type;
     593             : 
     594             :   /// \brief The string type
     595             :   typedef core::identifier_string string_type;
     596             : 
     597             :   /// \brief The value true
     598             :   /// \return The value true
     599             :   static inline
     600         122 :   bes::boolean_expression true_()
     601             :   {
     602         122 :     return bes::true_();
     603             :   }
     604             : 
     605             :   /// \brief The value false
     606             :   /// \return The value false
     607             :   static inline
     608          50 :   bes::boolean_expression false_()
     609             :   {
     610          50 :     return bes::false_();
     611             :   }
     612             : 
     613             :   /// \brief Operator not
     614             :   /// \param x A term
     615             :   /// \return Operator not applied to
     616             :   static inline
     617           1 :   bes::boolean_expression not_(const bes::boolean_expression& x)
     618             :   {
     619           1 :     return bes::not_(x);
     620             :   }
     621             : 
     622             :   /// \brief Operator and
     623             :   /// \param p A term
     624             :   /// \param q A term
     625             :   /// \return Operator and applied to p and q
     626             :   static inline
     627         123 :   bes::boolean_expression and_(const bes::boolean_expression& p, const bes::boolean_expression& q)
     628             :   {
     629         123 :     return bes::and_(p, q);
     630             :   }
     631             : 
     632             :   /// \brief Operator or
     633             :   /// \param p A term
     634             :   /// \param q A term
     635             :   /// \return Operator or applied to p and q
     636             :   static inline
     637          22 :   bes::boolean_expression or_(const bes::boolean_expression& p, const bes::boolean_expression& q)
     638             :   {
     639          22 :     return bes::or_(p, q);
     640             :   }
     641             : 
     642             :   /// \brief Implication
     643             :   /// \param p A term
     644             :   /// \param q A term
     645             :   /// \return Implication applied to p and q
     646             :   static inline
     647           3 :   bes::boolean_expression imp(const bes::boolean_expression& p, const bes::boolean_expression& q)
     648             :   {
     649           3 :     return bes::imp(p, q);
     650             :   }
     651             : 
     652             :   /// \brief Test for value true
     653             :   /// \param t A term
     654             :   /// \return True if the term has the value true
     655             :   static inline
     656          16 :   bool is_true(const bes::boolean_expression& t)
     657             :   {
     658          16 :     return bes::is_true(t);
     659             :   }
     660             : 
     661             :   /// \brief Test for value false
     662             :   /// \param t A term
     663             :   /// \return True if the term has the value false
     664             :   static inline
     665          17 :   bool is_false(const bes::boolean_expression& t)
     666             :   {
     667          17 :     return bes::is_false(t);
     668             :   }
     669             : 
     670             :   /// \brief Test for operator not
     671             :   /// \param t A term
     672             :   /// \return True if the term is of type and
     673             :   static inline
     674           6 :   bool is_not(const bes::boolean_expression& t)
     675             :   {
     676           6 :     return bes::is_not(t);
     677             :   }
     678             : 
     679             :   /// \brief Test for operator and
     680             :   /// \param t A term
     681             :   /// \return True if the term is of type and
     682             :   static inline
     683           6 :   bool is_and(const bes::boolean_expression& t)
     684             :   {
     685           6 :     return bes::is_and(t);
     686             :   }
     687             : 
     688             :   /// \brief Test for operator or
     689             :   /// \param t A term
     690             :   /// \return True if the term is of type or
     691             :   static inline
     692           6 :   bool is_or(const bes::boolean_expression& t)
     693             :   {
     694           6 :     return bes::is_or(t);
     695             :   }
     696             : 
     697             :   /// \brief Test for implication
     698             :   /// \param t A term
     699             :   /// \return True if the term is an implication
     700             :   static inline
     701           6 :   bool is_imp(const bes::boolean_expression& t)
     702             :   {
     703           6 :     return bes::is_imp(t);
     704             :   }
     705             : 
     706             :   /// \brief Test for propositional variable
     707             :   /// \param t A term
     708             :   /// \return True if the term is a propositional variable
     709             :   static inline
     710           2 :   bool is_prop_var(const bes::boolean_expression& t)
     711             :   {
     712           2 :     return bes::is_boolean_variable(t);
     713             :   }
     714             : 
     715             :   /// \brief Returns the left argument of a term of type and, or or imp
     716             :   /// \param t A term
     717             :   /// \return The left argument of the term
     718             :   static inline
     719             :   const bes::boolean_expression& left(const bes::boolean_expression& t)
     720             :   {
     721             :     assert(is_and(t) || is_or(t) || is_imp(t));
     722             :     return atermpp::down_cast<const bes::boolean_expression>(t[0]);
     723             :   }
     724             : 
     725             :   /// \brief Returns the right argument of a term of type and, or or imp
     726             :   /// \param t A term
     727             :   /// \return The right argument of the term
     728             :   static inline
     729             :   const bes::boolean_expression& right(const bes::boolean_expression& t)
     730             :   {
     731             :     assert(is_and(t) || is_or(t) || is_imp(t));
     732             :     return atermpp::down_cast<const bes::boolean_expression>(t[1]);
     733             :   }
     734             : 
     735             :   /// \brief Returns the argument of a term of type not
     736             :   /// \param t A term
     737             :   static inline
     738           0 :   const bes::boolean_expression& not_arg(const bes::boolean_expression& t)
     739             :   {
     740           0 :     assert(is_not(t));
     741           0 :     return atermpp::down_cast<bes::not_>(t).operand();
     742             :   }
     743             : 
     744             :   /// \brief Returns the name of a boolean variable
     745             :   /// \param t A term
     746             :   /// \return The name of the boolean variable
     747             :   static inline
     748             :   const core::identifier_string& name(const bes::boolean_expression& t)
     749             :   {
     750             :     assert(bes::is_boolean_variable(t));
     751             :     return atermpp::down_cast<bes::boolean_variable>(t).name();
     752             :   }
     753             : 
     754             :   /// \brief Conversion from variable to term
     755             :   /// \param v A variable
     756             :   /// \returns The converted variable
     757             :   static inline
     758             :   const bes::boolean_expression& variable2term(const bes::boolean_variable& v)
     759             :   {
     760             :     return v;
     761             :   }
     762             : 
     763             :   /// \brief Conversion from term to variable
     764             :   /// \param t a term
     765             :   /// \returns The converted term
     766             :   static inline
     767             :   const bes::boolean_variable& term2variable(const bes::boolean_expression& t)
     768             :   {
     769             :     return atermpp::down_cast<bes::boolean_variable>(t);
     770             :   }
     771             : 
     772             :   /// \brief Pretty print function
     773             :   /// \param t A term
     774             :   /// \return Returns a pretty print representation of the term
     775             :   static inline
     776             :   std::string pp(const bes::boolean_expression& t)
     777             :   {
     778             :     return bes::pp(t);
     779             :   }
     780             : };
     781             : 
     782             : } // namespace core
     783             : 
     784             : } // namespace mcrl2
     785             : 
     786             : #endif // MCRL2_BES_BOOLEAN_EXPRESSION_H

Generated by: LCOV version 1.13