mCRL2
Loading...
Searching...
No Matches
Static Public Member Functions | Static Protected Member Functions | List of all members
mcrl2::data::detail::BDD_Info Class Reference

The class BDD_Info provides information about the structure of binary decision diagrams. More...

#include <bdd_info.h>

Static Public Member Functions

static const mcrl2::data::data_expression & get_guard (const mcrl2::data::data_expression &a_bdd)
 Method that returns the guard of a BDD.
 
static const mcrl2::data::data_expression & get_true_branch (const mcrl2::data::data_expression &a_bdd)
 Method that returns the true-branch of a BDD.
 
static const mcrl2::data::data_expression & get_false_branch (const mcrl2::data::data_expression &a_bdd)
 Method that returns the false-branch of a BDD.
 
static bool is_true (const data_expression &a_bdd)
 Method that indicates whether or not a BDD equals true.
 
static bool is_false (const data_expression &a_bdd)
 Method that indicates whether or not a BDD equals false.
 
static bool is_if_then_else (const data_expression &a_bdd)
 Method that indicates wether or not the root of a BDD is a guard node.
 

Static Protected Member Functions

static const mcrl2::data::data_expression & argument (const mcrl2::data::data_expression &x, std::size_t n)
 

Detailed Description

The class BDD_Info provides information about the structure of binary decision diagrams.

Definition at line 25 of file bdd_info.h.

Member Function Documentation

◆ argument()

static const mcrl2::data::data_expression & mcrl2::data::detail::BDD_Info::argument ( const mcrl2::data::data_expression &  x,
std::size_t  n 
)
inlinestaticprotected

Definition at line 28 of file bdd_info.h.

◆ get_false_branch()

static const mcrl2::data::data_expression & mcrl2::data::detail::BDD_Info::get_false_branch ( const mcrl2::data::data_expression &  a_bdd)
inlinestatic

Method that returns the false-branch of a BDD.

Parameters
[in]a_bddA binary decision diagram.
Returns
The false-branch of the BDD.

Definition at line 58 of file bdd_info.h.

◆ get_guard()

static const mcrl2::data::data_expression & mcrl2::data::detail::BDD_Info::get_guard ( const mcrl2::data::data_expression &  a_bdd)
inlinestatic

Method that returns the guard of a BDD.

Parameters
[in]a_bddA binary decision diagram.
Returns
The guard at the root of the BDD.

Definition at line 42 of file bdd_info.h.

◆ get_true_branch()

static const mcrl2::data::data_expression & mcrl2::data::detail::BDD_Info::get_true_branch ( const mcrl2::data::data_expression &  a_bdd)
inlinestatic

Method that returns the true-branch of a BDD.

Parameters
[in]a_bddA binary decision diagram.
Returns
The true-branch of the BDD.

Definition at line 50 of file bdd_info.h.

◆ is_false()

static bool mcrl2::data::detail::BDD_Info::is_false ( const data_expression &  a_bdd)
inlinestatic

Method that indicates whether or not a BDD equals false.

Parameters
[in]a_bddA binary decision diagram.
Returns
True, if the BDD equals false. False, if the BDD does not equal true.

Definition at line 76 of file bdd_info.h.

◆ is_if_then_else()

static bool mcrl2::data::detail::BDD_Info::is_if_then_else ( const data_expression &  a_bdd)
inlinestatic

Method that indicates wether or not the root of a BDD is a guard node.

Parameters
[in]a_bddA binary decision diagram.
Returns
True, if the root of the BDD is a guard node. False, if the BDD equals true or if the BDD equals false.

Definition at line 85 of file bdd_info.h.

◆ is_true()

static bool mcrl2::data::detail::BDD_Info::is_true ( const data_expression &  a_bdd)
inlinestatic

Method that indicates whether or not a BDD equals true.

Parameters
[in]a_bddA binary decision diagram.
Returns
True, if the BDD equals true. False, if the BDD does not equal true.

Definition at line 67 of file bdd_info.h.

The documentation for this class was generated from the following file: