CBMC
|
A minimalistic BDD library, following Bryant's original paper and Andersen's lecture notes. More...
#include <list>
#include <map>
#include <stack>
#include <string>
#include <vector>
#include "miniBDD.inc"
Go to the source code of this file.
Classes | |
class | mini_bddt |
class | mini_bdd_nodet |
class | mini_bdd_mgrt |
struct | mini_bdd_mgrt::var_table_entryt |
struct | mini_bdd_mgrt::reverse_keyt |
Functions | |
mini_bddt | restrict (const mini_bddt &u, unsigned var, const bool value) |
mini_bddt | exists (const mini_bddt &u, unsigned var) |
mini_bddt | substitute (const mini_bddt &where, unsigned var, const mini_bddt &by_what) |
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.
Small BDD implementation.
Definition in file miniBDD.h.
Definition at line 596 of file miniBDD.cpp.
Definition at line 610 of file miniBDD.cpp.
Definition at line 551 of file miniBDD.cpp.