|
CBMC
|
Include dependency graph for miniBDD.cpp: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.
| bool and_fkt | ( | bool | x, |
| bool | y | ||
| ) |
Definition at line 391 of file miniBDD.cpp.
| std::string cubes | ( | const mini_bddt & | u | ) |
Definition at line 596 of file miniBDD.cpp.
| void cubes | ( | const mini_bddt & | u, |
| const std::string & | path, | ||
| std::string & | result | ||
| ) |
Definition at line 571 of file miniBDD.cpp.
| bool equal_fkt | ( | bool | x, |
| bool | y | ||
| ) |
Definition at line 364 of file miniBDD.cpp.
Definition at line 556 of file miniBDD.cpp.
| bool OneSat | ( | const mini_bddt & | v, |
| std::map< unsigned, bool > & | assignment | ||
| ) |
Definition at line 610 of file miniBDD.cpp.
| bool or_fkt | ( | bool | x, |
| bool | y | ||
| ) |
Definition at line 401 of file miniBDD.cpp.
Definition at line 551 of file miniBDD.cpp.
Definition at line 562 of file miniBDD.cpp.
| bool xor_fkt | ( | bool | x, |
| bool | y | ||
| ) |
Definition at line 374 of file miniBDD.cpp.