bdd_info.h

Go to the documentation of this file.

// Author(s): Luc Engelen
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_DATA_DETAIL_PROVER_BDD_INFO_H
#define MCRL2_DATA_DETAIL_PROVER_BDD_INFO_H
 
#include "mcrl2/data/bool.h"
 
namespace mcrl2
{
namespace data
{
namespace detail
{
 
class BDD_Info
{
  protected:
    static const mcrl2::data::data_expression& argument(const mcrl2::data::data_expression& x, std::size_t n)
    {
      const mcrl2::data::application& a = atermpp::down_cast<mcrl2::data::application>(x);
      return a[n]; 
      // mcrl2::data::application::const_iterator i = a.begin();
      // std::advance(i, n);
      // return *i;
    }
 
  public:
 
    static inline const mcrl2::data::data_expression& get_guard(const mcrl2::data::data_expression& a_bdd)
    {
      return argument(a_bdd,0);
    }
 
    static inline const mcrl2::data::data_expression& get_true_branch(const mcrl2::data::data_expression&  a_bdd)
    {
      return argument(a_bdd,1);
    }
 
    static inline const mcrl2::data::data_expression& get_false_branch(const mcrl2::data::data_expression& a_bdd)
    {
      return argument(a_bdd,2);
    }
 
    static inline bool is_true(const data_expression& a_bdd)
    {
      return mcrl2::data::sort_bool::is_true_function_symbol(a_bdd);
    }
 
    static inline bool is_false(const data_expression& a_bdd)
    {
      return mcrl2::data::sort_bool::is_false_function_symbol(a_bdd);
    }
 
    static inline bool is_if_then_else(const data_expression& a_bdd)
    {
      return mcrl2::data::is_if_application(a_bdd);
    }
};
 
} // namespace detail
} // namespace data
} // namespace mcrl2
 
#endif