LCOV - code coverage report
Current view: top level - data/include/mcrl2/data/detail/prover - bdd_info.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 4 17 23.5 %
Date: 2020-02-19 00:44:21 Functions: 2 7 28.6 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Luc Engelen
       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/utilities/bdd_info.h
      10             : /// \brief Interface to class BDD_Info
      11             : 
      12             : #ifndef MCRL2_DATA_DETAIL_PROVER_BDD_INFO_H
      13             : #define MCRL2_DATA_DETAIL_PROVER_BDD_INFO_H
      14             : 
      15             : #include "mcrl2/data/bool.h"
      16             : 
      17             : namespace mcrl2
      18             : {
      19             : namespace data
      20             : {
      21             : namespace detail
      22             : {
      23             : 
      24             : /// \brief The class BDD_Info provides information about the structure of binary decision diagrams.
      25             : class BDD_Info
      26             : {
      27             :   protected:
      28           0 :     static const mcrl2::data::data_expression& argument(const mcrl2::data::data_expression& x, std::size_t n)
      29             :     {
      30           0 :       const mcrl2::data::application& a = atermpp::down_cast<mcrl2::data::application>(x);
      31           0 :       mcrl2::data::application::const_iterator i = a.begin();
      32           0 :       std::advance(i, n);
      33           0 :       return *i;
      34             :     }
      35             : 
      36             :   public:
      37             : 
      38             :     /// \brief Method that returns the guard of a BDD.
      39             :     /// \param[in] a_bdd A binary decision diagram.
      40             :     /// \return The guard at the root of the BDD.
      41           0 :     static inline mcrl2::data::data_expression get_guard(const mcrl2::data::data_expression& a_bdd)
      42             :     {
      43           0 :       return argument(a_bdd,0);
      44             :     }
      45             : 
      46             :     /// \brief Method that returns the true-branch of a BDD.
      47             :     /// \param[in] a_bdd A binary decision diagram.
      48             :     /// \return The true-branch of the BDD.
      49           0 :     static inline mcrl2::data::data_expression get_true_branch(const mcrl2::data::data_expression&  a_bdd)
      50             :     {
      51           0 :       return argument(a_bdd,1);
      52             :     }
      53             : 
      54             :     /// \brief Method that returns the false-branch of a BDD.
      55             :     /// \param[in] a_bdd A binary decision diagram.
      56             :     /// \return The false-branch of the BDD.
      57           0 :     static inline mcrl2::data::data_expression get_false_branch(const mcrl2::data::data_expression& a_bdd)
      58             :     {
      59           0 :       return argument(a_bdd,2);
      60             :     }
      61             : 
      62             :     /// \brief Method that indicates whether or not a BDD equals true.
      63             :     /// \param[in] a_bdd A binary decision diagram.
      64             :     /// \return True, if the BDD equals true.
      65             :     ///         False, if the BDD does not equal true.
      66          81 :     static inline bool is_true(const data_expression& a_bdd)
      67             :     {
      68          81 :       return mcrl2::data::sort_bool::is_true_function_symbol(a_bdd);
      69             :     }
      70             : 
      71             :     /// \brief Method that indicates whether or not a BDD equals false.
      72             :     /// \param[in] a_bdd A binary decision diagram.
      73             :     /// \return True, if the BDD equals false.
      74             :     ///         False, if the BDD does not equal true.
      75          22 :     static inline bool is_false(const data_expression& a_bdd)
      76             :     {
      77          22 :       return mcrl2::data::sort_bool::is_false_function_symbol(a_bdd);
      78             :     }
      79             : 
      80             :     /// \brief Method that indicates wether or not the root of a BDD is a guard node.
      81             :     /// \param[in] a_bdd A binary decision diagram.
      82             :     /// \return True, if the root of the BDD is a guard node.
      83             :     ///         False, if the BDD equals true or if the BDD equals false.
      84           0 :     static inline bool is_if_then_else(const data_expression& a_bdd)
      85             :     {
      86           0 :       return mcrl2::data::is_if_application(a_bdd);
      87             :     }
      88             : };
      89             : 
      90             : } // namespace detail
      91             : } // namespace data
      92             : } // namespace mcrl2
      93             : 
      94             : #endif

Generated by: LCOV version 1.13