cprover
|
#include <miniBDD.h>
Public Member Functions | |
mini_bddt () | |
mini_bddt (const mini_bddt &x) | |
~mini_bddt () | |
mini_bddt | operator! () const |
mini_bddt | operator^ (const mini_bddt &) const |
mini_bddt | operator== (const mini_bddt &) const |
mini_bddt | operator & (const mini_bddt &) const |
mini_bddt | operator| (const mini_bddt &) const |
mini_bddt & | operator= (const mini_bddt &) |
bool | is_constant () const |
bool | is_true () const |
bool | is_false () const |
unsigned | var () const |
const mini_bddt & | low () const |
const mini_bddt & | high () const |
unsigned | node_number () const |
void | clear () |
bool | is_initialized () const |
mini_bddt (class mini_bdd_nodet *_node) | |
Public Attributes | |
class mini_bdd_nodet * | node |
mini_bddt::mini_bddt | ( | ) |
Referenced by is_initialized().
mini_bddt::mini_bddt | ( | const mini_bddt & | x | ) |
mini_bddt::~mini_bddt | ( | ) |
|
explicit |
void mini_bddt::clear | ( | ) |
Referenced by mini_bdd_nodet::remove_reference().
const mini_bddt& mini_bddt::high | ( | ) | const |
Referenced by mini_bdd_applyt::APP_non_rec(), mini_bdd_applyt::APP_rec(), bdd_exprt::as_expr(), cubes(), OneSat(), and restrictt::RES().
bool mini_bddt::is_constant | ( | ) | const |
Referenced by mini_bdd_applyt::APP_non_rec(), mini_bdd_applyt::APP_rec(), and bdd_exprt::as_expr().
bool mini_bddt::is_false | ( | ) | const |
Referenced by bdd_exprt::as_expr(), cubes(), and OneSat().
|
inline |
Definition at line 58 of file miniBDD.h.
References mini_bddt(), and node.
Referenced by mini_bdd_applyt::APP_non_rec(), mini_bdd_applyt::APP_rec(), bdd_exprt::as_expr(), and restrictt::RES().
bool mini_bddt::is_true | ( | ) | const |
Referenced by mini_bdd_applyt::APP_non_rec(), mini_bdd_applyt::APP_rec(), bdd_exprt::as_expr(), cubes(), and OneSat().
const mini_bddt& mini_bddt::low | ( | ) | const |
Referenced by mini_bdd_applyt::APP_non_rec(), mini_bdd_applyt::APP_rec(), bdd_exprt::as_expr(), cubes(), OneSat(), and restrictt::RES().
unsigned mini_bddt::node_number | ( | ) | const |
Referenced by mini_bdd_applyt::APP_rec(), and mini_bdd_mgrt::mk().
mini_bddt mini_bddt::operator! | ( | ) | const |
Definition at line 379 of file miniBDD.cpp.
Definition at line 364 of file miniBDD.cpp.
References equal_fkt().
Definition at line 374 of file miniBDD.cpp.
References xor_fkt().
Definition at line 401 of file miniBDD.cpp.
References or_fkt().
unsigned mini_bddt::var | ( | ) | const |
class mini_bdd_nodet* mini_bddt::node |
Definition at line 62 of file miniBDD.h.
Referenced by mini_bdd_applyt::APP_non_rec(), mini_bdd_applyt::APP_rec(), cubes(), is_initialized(), restrictt::RES(), and mini_bdd_mgrt::Var().