mcrl2/pbes/bdd.h¶

Include file:

#include "mcrl2/pbes/bdd.h"

add your file description here.

Classes¶

Typedefs¶

type mcrl2::pbes_system::bdd::bdd_node¶: typedef for std::shared_ptr< term >

Functions¶

std::vector<std::string> mcrl2::pbes_system::bdd::add_parens(const std::vector<std::string> &v)¶

std::vector<std::string> mcrl2::pbes_system::bdd::add_single_quotes(const std::vector<std::string> &v)¶

bdd_node mcrl2::pbes_system::bdd::all(const std::vector<bdd_node> &v)¶

bdd_node mcrl2::pbes_system::bdd::any(const std::vector<bdd_node> &v)¶

bdd_node mcrl2::pbes_system::bdd::at_least_one_equation(const std::map<pbes_system::propositional_variable, bdd_node> &equation_map)¶

std::vector<bdd_node> mcrl2::pbes_system::bdd::equation_identifiers(std::size_t equation_count, const std::vector<bdd_node> &id_variables, bool unary_encoding)¶

std::vector<bdd_node> mcrl2::pbes_system::bdd::even_ids(const std::vector<bdd_equation> &equations)¶

std::vector<bdd_node> mcrl2::pbes_system::bdd::id_variables(std::size_t n, bool unary_encoding)¶

bool mcrl2::pbes_system::bdd::is_degenerate_and(const pbes_system::pbes_expression &x)¶

bool mcrl2::pbes_system::bdd::is_degenerate_or(const pbes_system::pbes_expression &x)¶

std::size_t log2_rounded_up(std::size_t n)¶

bdd_node mcrl2::pbes_system::bdd::make_and(bdd_node left, bdd_node right)¶

bdd_node mcrl2::pbes_system::bdd::make_eq(bdd_node left, bdd_node right)¶

bdd_node mcrl2::pbes_system::bdd::make_false()¶

bdd_node mcrl2::pbes_system::bdd::make_imp(bdd_node left, bdd_node right)¶

bdd_node mcrl2::pbes_system::bdd::make_ite(bdd_node condition, bdd_node then_, bdd_node else_)¶

bdd_node mcrl2::pbes_system::bdd::make_not(bdd_node x)¶

bdd_node mcrl2::pbes_system::bdd::make_or(bdd_node left, bdd_node right)¶

bdd_node mcrl2::pbes_system::bdd::make_true()¶

bdd_node mcrl2::pbes_system::bdd::make_variable(const std::string &name)¶

std::vector<bdd_node> mcrl2::pbes_system::bdd::odd_ids(const std::vector<bdd_equation> &equations)¶

std::vector<bdd_node> mcrl2::pbes_system::bdd::operator+(const std::vector<bdd_node> &x, const std::vector<bdd_node> &y)¶

std::ostream &mcrl2::pbes_system::bdd::operator<<(std::ostream &out, const bdd_equation &eqn)¶

std::vector<bdd_node> mcrl2::pbes_system::bdd::param_variables(const pbes_system::propositional_variable &X)¶

std::string mcrl2::pbes_system::bdd::pbes2bdd(const pbes_system::pbes &p, bool unary_encoding = false)¶

std::map<std::size_t, std::vector<bdd_node>> mcrl2::pbes_system::bdd::priority_map(const std::vector<bdd_equation> &equations)¶

std::pair<propositional_variable_instantiation, data::data_expression> mcrl2::pbes_system::bdd::split_expression(const pbes_expression &x, Split split, Join join)¶

std::vector<bdd_equation> mcrl2::pbes_system::bdd::split_pbes(const pbes &p, const pbes_equation_index &eqn_index, const std::vector<bdd_node> &ids)¶

bdd_equation mcrl2::pbes_system::bdd::split_pbes_equation(const pbes_equation &eqn, std::size_t rank, const bdd_node &id)¶

std::string mcrl2::pbes_system::bdd::string_join(const std::vector<std::string> &v, const std::string &sep = ", ")¶

std::string mcrl2::pbes_system::bdd::string_join(InputIt first, InputIt last, const std::string &sep = ", ")¶

bdd_node mcrl2::pbes_system::bdd::to_bdd(const data::data_expression &x)¶

std::vector<bdd_node> mcrl2::pbes_system::bdd::to_bdd(const data::data_expression_list &v)¶

std::vector<bdd_node> mcrl2::pbes_system::bdd::to_bdd(const data::variable_list &v)¶

std::vector<std::string> mcrl2::pbes_system::bdd::to_string(const BddNodeContainer &nodes, bool after = false)¶

std::string mcrl2::pbes_system::bdd::unchanged_variables(const std::vector<bdd_node> &variables)¶