cprover
|
A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes. More...
Go to the source code of this file.
Classes | |
class | mini_bdd_applyt |
class | restrictt |
Macros | |
#define | forall_nodes(it) |
Functions | |
bool | equal_fkt (bool x, bool y) |
bool | xor_fkt (bool x, bool y) |
bool | and_fkt (bool x, bool y) |
bool | or_fkt (bool x, bool y) |
mini_bddt | restrict (const mini_bddt &u, unsigned var, const bool value) |
mini_bddt | exists (const mini_bddt &u, const unsigned var) |
mini_bddt | substitute (const mini_bddt &t, unsigned var, const mini_bddt &tp) |
void | cubes (const mini_bddt &u, const std::string &path, std::string &result) |
std::string | cubes (const mini_bddt &u) |
bool | OneSat (const mini_bddt &v, std::map< unsigned, bool > &assignment) |
A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes.
Definition in file miniBDD.cpp.
#define forall_nodes | ( | it | ) |
Definition at line 20 of file miniBDD.cpp.
Referenced by mini_bdd_mgrt::DumpDot(), mini_bdd_mgrt::DumpTable(), and mini_bdd_mgrt::DumpTikZ().
bool and_fkt | ( | bool | x, |
bool | y | ||
) |
Definition at line 386 of file miniBDD.cpp.
void cubes | ( | const mini_bddt & | u, |
const std::string & | path, | ||
std::string & | result | ||
) |
Definition at line 566 of file miniBDD.cpp.
References mini_bddt::high(), mini_bddt::is_false(), mini_bddt::is_true(), mini_bddt::low(), mini_bdd_nodet::mgr, mini_bddt::node, mini_bddt::var(), and mini_bdd_mgrt::var_table.
Referenced by cubes().
std::string cubes | ( | const mini_bddt & | u | ) |
Definition at line 591 of file miniBDD.cpp.
References cubes(), mini_bddt::is_false(), and mini_bddt::is_true().
bool equal_fkt | ( | bool | x, |
bool | y | ||
) |
Definition at line 359 of file miniBDD.cpp.
Referenced by mini_bddt::operator==().
Definition at line 549 of file miniBDD.cpp.
References restrict().
bool OneSat | ( | const mini_bddt & | v, |
std::map< unsigned, bool > & | assignment | ||
) |
Definition at line 605 of file miniBDD.cpp.
References mini_bddt::high(), mini_bddt::is_false(), mini_bddt::is_true(), mini_bddt::low(), OneSat(), and mini_bddt::var().
Referenced by OneSat().
bool or_fkt | ( | bool | x, |
bool | y | ||
) |
Definition at line 396 of file miniBDD.cpp.
Referenced by mini_bddt::operator|().
Definition at line 544 of file miniBDD.cpp.
Referenced by exists(), main(), and substitute().
Definition at line 556 of file miniBDD.cpp.
References restrict().
bool xor_fkt | ( | bool | x, |
bool | y | ||
) |
Definition at line 369 of file miniBDD.cpp.
Referenced by mini_bddt::operator^().