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 : return a[n]; 32 : // mcrl2::data::application::const_iterator i = a.begin(); 33 : // std::advance(i, n); 34 : // return *i; 35 : } 36 : 37 : public: 38 : 39 : /// \brief Method that returns the guard of a BDD. 40 : /// \param[in] a_bdd A binary decision diagram. 41 : /// \return The guard at the root of the BDD. 42 0 : static inline const mcrl2::data::data_expression& get_guard(const mcrl2::data::data_expression& a_bdd) 43 : { 44 0 : return argument(a_bdd,0); 45 : } 46 : 47 : /// \brief Method that returns the true-branch of a BDD. 48 : /// \param[in] a_bdd A binary decision diagram. 49 : /// \return The true-branch of the BDD. 50 0 : static inline const mcrl2::data::data_expression& get_true_branch(const mcrl2::data::data_expression& a_bdd) 51 : { 52 0 : return argument(a_bdd,1); 53 : } 54 : 55 : /// \brief Method that returns the false-branch of a BDD. 56 : /// \param[in] a_bdd A binary decision diagram. 57 : /// \return The false-branch of the BDD. 58 0 : static inline const mcrl2::data::data_expression& get_false_branch(const mcrl2::data::data_expression& a_bdd) 59 : { 60 0 : return argument(a_bdd,2); 61 : } 62 : 63 : /// \brief Method that indicates whether or not a BDD equals true. 64 : /// \param[in] a_bdd A binary decision diagram. 65 : /// \return True, if the BDD equals true. 66 : /// False, if the BDD does not equal true. 67 81 : static inline bool is_true(const data_expression& a_bdd) 68 : { 69 81 : return mcrl2::data::sort_bool::is_true_function_symbol(a_bdd); 70 : } 71 : 72 : /// \brief Method that indicates whether or not a BDD equals false. 73 : /// \param[in] a_bdd A binary decision diagram. 74 : /// \return True, if the BDD equals false. 75 : /// False, if the BDD does not equal true. 76 22 : static inline bool is_false(const data_expression& a_bdd) 77 : { 78 22 : return mcrl2::data::sort_bool::is_false_function_symbol(a_bdd); 79 : } 80 : 81 : /// \brief Method that indicates wether or not the root of a BDD is a guard node. 82 : /// \param[in] a_bdd A binary decision diagram. 83 : /// \return True, if the root of the BDD is a guard node. 84 : /// False, if the BDD equals true or if the BDD equals false. 85 0 : static inline bool is_if_then_else(const data_expression& a_bdd) 86 : { 87 0 : return mcrl2::data::is_if_application(a_bdd); 88 : } 89 : }; 90 : 91 : } // namespace detail 92 : } // namespace data 93 : } // namespace mcrl2 94 : 95 : #endif