mcrl2::pbes_system::bdd::bdd_sylvan

Include file:

#include "mcrl2/pbes/pbesbddsolve.h
class mcrl2::pbes_system::bdd::bdd_sylvan

Public types

type mcrl2::pbes_system::bdd::bdd_sylvan::bdd_substitution

typedef for sylvan::BddMap

type mcrl2::pbes_system::bdd::bdd_sylvan::bdd_type

typedef for sylvan::Bdd

type mcrl2::pbes_system::bdd::bdd_sylvan::bdd_variable_set

typedef for sylvan::BddSet

Private attributes

std::map<std::string, std::size_t> mcrl2::pbes_system::bdd::bdd_sylvan::m_variable_index
std::vector<std::string> mcrl2::pbes_system::bdd::bdd_sylvan::m_variable_names
std::vector<bdd_type> mcrl2::pbes_system::bdd::bdd_sylvan::m_variables

Public member functions

std::pair<bdd_type, std::size_t> add_variable(const std::string &name)
bdd_type all(const std::vector<bdd_type> &v) const
bdd_type and_(const bdd_type &x, const bdd_type &y) const
bdd_type any(const std::vector<bdd_type> &v) const
std::size_t count(const bdd_type &x, const bdd_variable_set &variables) const
bdd_type equiv(const bdd_type &x, const bdd_type &y) const
bdd_type exists(const bdd_variable_set &variables, const bdd_type &body) const
bdd_type false_() const
bdd_type forall(const bdd_variable_set &variables, const bdd_type &body) const
bdd_type implies(const bdd_type &x, const bdd_type &y) const
bdd_type ite(const bdd_type &x, const bdd_type &y, const bdd_type &z) const
bdd_type let(const bdd_substitution &sigma, const bdd_type &x) const
bdd_type not_(const bdd_type &x) const
bdd_type or_(const bdd_type &x, const bdd_type &y) const
std::string pick_one_solution(const bdd_type &x, const bdd_variable_set &variables) const
bdd_type quantify(const bdd_type &body, const bdd_variable_set &variables, bool is_forall) const
bdd_type true_() const
const bdd_type &variable_bdd(const std::string &name) const
std::size_t variable_index(const std::string &name) const