CBMC
|
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 |
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.
Definition at line 391 of file miniBDD.cpp.
Definition at line 596 of file miniBDD.cpp.
Definition at line 571 of file miniBDD.cpp.
Definition at line 364 of file miniBDD.cpp.
Definition at line 556 of file miniBDD.cpp.
Definition at line 610 of file miniBDD.cpp.
Definition at line 401 of file miniBDD.cpp.
Definition at line 551 of file miniBDD.cpp.
Definition at line 562 of file miniBDD.cpp.
Definition at line 374 of file miniBDD.cpp.