LCOV - code coverage report
Current view: top level - bes/include/mcrl2/bes - bdd_expression.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 44 49 89.8 %
Date: 2020-10-20 00:45:57 Functions: 19 20 95.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/bes/bdd_expression.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_BES_BDD_EXPRESSION_H
      13             : #define MCRL2_BES_BDD_EXPRESSION_H
      14             : 
      15             : #include "mcrl2/core/detail/default_values.h"
      16             : #include "mcrl2/core/detail/soundness_checks.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace bdd {
      21             : 
      22             : //--- start generated classes ---//
      23             : /// \brief A bdd expression
      24           6 : class bdd_expression: public atermpp::aterm_appl
      25             : {
      26             :   public:
      27             :     /// \brief Default constructor.
      28             :     bdd_expression()
      29             :       : atermpp::aterm_appl(core::detail::default_values::BddExpression)
      30             :     {}
      31             : 
      32             :     /// \brief Constructor.
      33             :     /// \param term A term
      34           6 :     explicit bdd_expression(const atermpp::aterm& term)
      35           6 :       : atermpp::aterm_appl(term)
      36             :     {
      37           6 :       assert(core::detail::check_rule_BddExpression(*this));
      38           6 :     }
      39             : 
      40             :     /// Move semantics
      41             :     bdd_expression(const bdd_expression&) noexcept = default;
      42             :     bdd_expression(bdd_expression&&) noexcept = default;
      43             :     bdd_expression& operator=(const bdd_expression&) noexcept = default;
      44             :     bdd_expression& operator=(bdd_expression&&) noexcept = default;
      45             : };
      46             : 
      47             : /// \brief list of bdd_expressions
      48             : typedef atermpp::term_list<bdd_expression> bdd_expression_list;
      49             : 
      50             : /// \brief vector of bdd_expressions
      51             : typedef std::vector<bdd_expression>    bdd_expression_vector;
      52             : 
      53             : // prototypes
      54             : inline bool is_true(const atermpp::aterm_appl& x);
      55             : inline bool is_false(const atermpp::aterm_appl& x);
      56             : inline bool is_if(const atermpp::aterm_appl& x);
      57             : 
      58             : /// \brief Test for a bdd_expression expression
      59             : /// \param x A term
      60             : /// \return True if \a x is a bdd_expression expression
      61             : inline
      62             : bool is_bdd_expression(const atermpp::aterm_appl& x)
      63             : {
      64             :   return bdd::is_true(x) ||
      65             :          bdd::is_false(x) ||
      66             :          bdd::is_if(x);
      67             : }
      68             : 
      69             : // prototype declaration
      70             : std::string pp(const bdd_expression& x);
      71             : 
      72             : /// \brief Outputs the object to a stream
      73             : /// \param out An output stream
      74             : /// \param x Object x
      75             : /// \return The output stream
      76             : inline
      77           0 : std::ostream& operator<<(std::ostream& out, const bdd_expression& x)
      78             : {
      79           0 :   return out << bdd::pp(x);
      80             : }
      81             : 
      82             : /// \brief swap overload
      83             : inline void swap(bdd_expression& t1, bdd_expression& t2)
      84             : {
      85             :   t1.swap(t2);
      86             : }
      87             : 
      88             : 
      89             : /// \brief The value true for bdd expressions
      90           2 : class true_: public bdd_expression
      91             : {
      92             :   public:
      93             :     /// \brief Default constructor.
      94           2 :     true_()
      95           2 :       : bdd_expression(core::detail::default_values::BddTrue)
      96           2 :     {}
      97             : 
      98             :     /// \brief Constructor.
      99             :     /// \param term A term
     100             :     explicit true_(const atermpp::aterm& term)
     101             :       : bdd_expression(term)
     102             :     {
     103             :       assert(core::detail::check_term_BddTrue(*this));
     104             :     }
     105             : 
     106             :     /// Move semantics
     107             :     true_(const true_&) noexcept = default;
     108             :     true_(true_&&) noexcept = default;
     109             :     true_& operator=(const true_&) noexcept = default;
     110             :     true_& operator=(true_&&) noexcept = default;
     111             : };
     112             : 
     113             : /// \brief Test for a true expression
     114             : /// \param x A term
     115             : /// \return True if \a x is a true expression
     116             : inline
     117          24 : bool is_true(const atermpp::aterm_appl& x)
     118             : {
     119          24 :   return x.function() == core::detail::function_symbols::BddTrue;
     120             : }
     121             : 
     122             : // prototype declaration
     123             : std::string pp(const true_& x);
     124             : 
     125             : /// \brief Outputs the object to a stream
     126             : /// \param out An output stream
     127             : /// \param x Object x
     128             : /// \return The output stream
     129             : inline
     130             : std::ostream& operator<<(std::ostream& out, const true_& x)
     131             : {
     132             :   return out << bdd::pp(x);
     133             : }
     134             : 
     135             : /// \brief swap overload
     136             : inline void swap(true_& t1, true_& t2)
     137             : {
     138             :   t1.swap(t2);
     139             : }
     140             : 
     141             : 
     142             : /// \brief The value false for bdd expressions
     143           1 : class false_: public bdd_expression
     144             : {
     145             :   public:
     146             :     /// \brief Default constructor.
     147           1 :     false_()
     148           1 :       : bdd_expression(core::detail::default_values::BddFalse)
     149           1 :     {}
     150             : 
     151             :     /// \brief Constructor.
     152             :     /// \param term A term
     153             :     explicit false_(const atermpp::aterm& term)
     154             :       : bdd_expression(term)
     155             :     {
     156             :       assert(core::detail::check_term_BddFalse(*this));
     157             :     }
     158             : 
     159             :     /// Move semantics
     160             :     false_(const false_&) noexcept = default;
     161             :     false_(false_&&) noexcept = default;
     162             :     false_& operator=(const false_&) noexcept = default;
     163             :     false_& operator=(false_&&) noexcept = default;
     164             : };
     165             : 
     166             : /// \brief Test for a false expression
     167             : /// \param x A term
     168             : /// \return True if \a x is a false expression
     169             : inline
     170          36 : bool is_false(const atermpp::aterm_appl& x)
     171             : {
     172          36 :   return x.function() == core::detail::function_symbols::BddFalse;
     173             : }
     174             : 
     175             : // prototype declaration
     176             : std::string pp(const false_& x);
     177             : 
     178             : /// \brief Outputs the object to a stream
     179             : /// \param out An output stream
     180             : /// \param x Object x
     181             : /// \return The output stream
     182             : inline
     183             : std::ostream& operator<<(std::ostream& out, const false_& x)
     184             : {
     185             :   return out << bdd::pp(x);
     186             : }
     187             : 
     188             : /// \brief swap overload
     189             : inline void swap(false_& t1, false_& t2)
     190             : {
     191             :   t1.swap(t2);
     192             : }
     193             : 
     194             : 
     195             : /// \brief The if operator for bdd expressions
     196           3 : class if_: public bdd_expression
     197             : {
     198             :   public:
     199             :     /// \brief Default constructor.
     200             :     if_()
     201             :       : bdd_expression(core::detail::default_values::BddIf)
     202             :     {}
     203             : 
     204             :     /// \brief Constructor.
     205             :     /// \param term A term
     206             :     explicit if_(const atermpp::aterm& term)
     207             :       : bdd_expression(term)
     208             :     {
     209             :       assert(core::detail::check_term_BddIf(*this));
     210             :     }
     211             : 
     212             :     /// \brief Constructor.
     213             :     if_(const core::identifier_string& name, const bdd_expression& left, const bdd_expression& right)
     214             :       : bdd_expression(atermpp::aterm_appl(core::detail::function_symbol_BddIf(), name, left, right))
     215             :     {}
     216             : 
     217             :     /// \brief Constructor.
     218           3 :     if_(const std::string& name, const bdd_expression& left, const bdd_expression& right)
     219           3 :       : bdd_expression(atermpp::aterm_appl(core::detail::function_symbol_BddIf(), core::identifier_string(name), left, right))
     220           3 :     {}
     221             : 
     222             :     /// Move semantics
     223             :     if_(const if_&) noexcept = default;
     224             :     if_(if_&&) noexcept = default;
     225             :     if_& operator=(const if_&) noexcept = default;
     226             :     if_& operator=(if_&&) noexcept = default;
     227             : 
     228           3 :     const core::identifier_string& name() const
     229             :     {
     230           3 :       return atermpp::down_cast<core::identifier_string>((*this)[0]);
     231             :     }
     232             : 
     233          20 :     const bdd_expression& left() const
     234             :     {
     235          20 :       return atermpp::down_cast<bdd_expression>((*this)[1]);
     236             :     }
     237             : 
     238          20 :     const bdd_expression& right() const
     239             :     {
     240          20 :       return atermpp::down_cast<bdd_expression>((*this)[2]);
     241             :     }
     242             : };
     243             : 
     244             : /// \brief Test for a if expression
     245             : /// \param x A term
     246             : /// \return True if \a x is a if expression
     247             : inline
     248          13 : bool is_if(const atermpp::aterm_appl& x)
     249             : {
     250          13 :   return x.function() == core::detail::function_symbols::BddIf;
     251             : }
     252             : 
     253             : // prototype declaration
     254             : std::string pp(const if_& x);
     255             : 
     256             : /// \brief Outputs the object to a stream
     257             : /// \param out An output stream
     258             : /// \param x Object x
     259             : /// \return The output stream
     260             : inline
     261           3 : std::ostream& operator<<(std::ostream& out, const if_& x)
     262             : {
     263           3 :   return out << bdd::pp(x);
     264             : }
     265             : 
     266             : /// \brief swap overload
     267             : inline void swap(if_& t1, if_& t2)
     268             : {
     269             :   t1.swap(t2);
     270             : }
     271             : //--- end generated classes ---//
     272             : 
     273             : inline
     274          12 : std::string pp(const bdd::false_&)
     275             : {
     276          12 :   return "false";
     277             : }
     278             : 
     279             : inline
     280          13 : std::string pp(const bdd::true_&)
     281             : {
     282          13 :   return "true";
     283             : }
     284             : 
     285             : inline
     286          18 : std::string pp(const bdd::if_& x)
     287             : {
     288          18 :   return "if(" + pp(x.left()) + ", " + pp(x.right()) + ")";
     289             : }
     290             : 
     291             : inline
     292          36 : std::string pp(const bdd::bdd_expression& x)
     293             : {
     294          36 :   if (is_false(x))
     295             :   {
     296          12 :     return pp(atermpp::down_cast<false_>(x));
     297             :   }
     298          24 :   else if (is_true(x))
     299             :   {
     300          12 :     return pp(atermpp::down_cast<true_>(x));
     301             :   }
     302          12 :   else if (is_if(x))
     303             :   {
     304          12 :     return pp(atermpp::down_cast<if_>(x));
     305             :   }
     306           0 :   std::ostringstream out;
     307           0 :   out << x;
     308           0 :   throw mcrl2::runtime_error("unknown bdd expression " + out.str());
     309             : }
     310             : 
     311             : } // namespace bdd
     312             : 
     313             : } // namespace mcrl2
     314             : 
     315             : #endif // MCRL2_BES_BDD_EXPRESSION_H

Generated by: LCOV version 1.13