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 deserialize(std::size_t index) 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

std::string hash(const bdd_type &x) 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

std::size_t node_count(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

void print(const std::string &msg, const bdd_type &x, const bdd_variable_set &context) const

void print(const std::string &msg, const std::map<std::uint32_t, bdd_sylvan::bdd_type> &m, const bdd_variable_set &context) const

void print(const std::string &msg, const std::vector<bdd_type> &x, const bdd_variable_set &context) const

bdd_type quantify(const bdd_type &body, const bdd_variable_set &variables, bool is_forall) const

bdd_type relation_backward(const bdd_type &R, const bdd_type &x, const bdd_variable_set &next_variables, const bdd_substitution &next_substitution, bool optimized = false) const

bdd_type relation_forward(const bdd_type &R, const bdd_type &x, const bdd_variable_set &variables, const bdd_substitution &prev_substitution, bool optimized = false) const

std::size_t serialize(const bdd_type &x) 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