cprover
mini_bddt Class Reference

#include <miniBDD.h>

Collaboration diagram for mini_bddt:
[legend]

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_bddtoperator= (const mini_bddt &)
 
bool is_constant () const
 
bool is_true () const
 
bool is_false () const
 
unsigned var () const
 
const mini_bddtlow () const
 
const mini_bddthigh () const
 
unsigned node_number () const
 
void clear ()
 
bool is_initialized () const
 
 mini_bddt (class mini_bdd_nodet *_node)
 

Public Attributes

class mini_bdd_nodetnode
 

Detailed Description

Definition at line 31 of file miniBDD.h.

Constructor & Destructor Documentation

◆ mini_bddt() [1/3]

mini_bddt::mini_bddt ( )

◆ mini_bddt() [2/3]

mini_bddt::mini_bddt ( const mini_bddt x)

◆ ~mini_bddt()

mini_bddt::~mini_bddt ( )

◆ mini_bddt() [3/3]

mini_bddt::mini_bddt ( class mini_bdd_nodet _node)
explicit

Member Function Documentation

◆ clear()

void mini_bddt::clear ( )

◆ high()

◆ is_constant()

bool mini_bddt::is_constant ( ) const

◆ is_false()

bool mini_bddt::is_false ( ) const

Referenced by cubes(), and OneSat().

◆ is_initialized()

bool mini_bddt::is_initialized ( ) const
inline

◆ is_true()

bool mini_bddt::is_true ( ) const

◆ low()

◆ node_number()

unsigned mini_bddt::node_number ( ) const

◆ operator &()

mini_bddt mini_bddt::operator& ( const mini_bddt ) const

◆ operator!()

mini_bddt mini_bddt::operator! ( ) const

Definition at line 379 of file miniBDD.cpp.

References is_initialized(), mini_bdd_nodet::mgr, node, and mini_bdd_mgrt::True().

◆ operator=()

mini_bddt& mini_bddt::operator= ( const mini_bddt )

◆ operator==()

mini_bddt mini_bddt::operator== ( const mini_bddt other) const

Definition at line 364 of file miniBDD.cpp.

References equal_fkt().

◆ operator^()

mini_bddt mini_bddt::operator^ ( const mini_bddt other) const

Definition at line 374 of file miniBDD.cpp.

References xor_fkt().

◆ operator|()

mini_bddt mini_bddt::operator| ( const mini_bddt other) const

Definition at line 401 of file miniBDD.cpp.

References or_fkt().

◆ var()

Member Data Documentation

◆ node


The documentation for this class was generated from the following files: