Generated on Mon Aug 25 11:35:49 2008 for Gecode by doxygen 1.5.6
Gecode::CpltSet::BddMgr

Gecode::CpltSet::BddMgr Class Reference

List of all members.

Detailed Description

Manager for CpltSetVars.

Used for initialization and destruction of the global lookup table for Bdd nodes and for keeping track between CpltSetVars and their corresponding indices in the lookup table.

Definition at line 61 of file bddmanager.icc.


Public Member Functions

 BddMgr (void)
 Default constructor.
GECODE_CPLTSET_EXPORT ~BddMgr (void)
 Destructor.
void init (int n, int c)
 Initialize manager with initial nodesize n and cachesize c.
bool leaf (const bdd &b) const
 Test whether bdd b is either constant true or constant false.
bool cfalse (const bdd &b) const
 Tests whether bdd b is constant false.
bool ctrue (const bdd &b) const
 Tests whether bdd b is constant true.
void setorder (int *hls)
 Sets the variable ordering in the bdd according to hls.
unsigned int bddsize (const bdd &b) const
 Return the size of bdd b.
unsigned int bddpath (const bdd &b) const
 Return the number of paths of bdd leading to a true nodeb.
GECODE_CPLTSET_EXPORT unsigned int numberOfPaths (bdd &b)
 Return the total number of paths of bdd b.
bdd bddpos (int i) const
 Return bdd at position i in bdd lookup table.
bdd negbddpos (int i) const
 Return negated bdd at position i in bdd lookup table.
int lbCard (const bdd &b)
 Get lower cardinality bound for breadth-first iteration.
int ubCard (const bdd &b)
 Get upper cardinality bound for breadth-first iteration.
void lbCard (const bdd &b, int l)
 Set lower cardinality bound for breadth-first iteration.
void ubCard (const bdd &b, int r)
 Set upper cardinality bound for breadth-first iteration.
bdd ite (const bdd &v, const bdd &t, const bdd &f)
 Construct the Bdd for $ \mbox{if} v \mbox{then} t \mbox{else} f$.
void mark (const bdd &b)
 Marks the bdd b.
void unmark (const bdd &b)
 Unmarks the bdd b.
bool marked (const bdd &b) const
 Check whether b is marked.
int node_level (const bdd &b) const
int bdd2var (int i)
 Returns the position of variable i in the current variable order.
int var2bdd (int i)
 Returns the variable at position i in the current variable order.
int dummy (void)
 Returns the offset of the first dummy var if there is any.
bdd iftrue (bdd &b)
 Return the true branch of a bdd b.
bdd iffalse (bdd &b)
 Return the false branch of a bdd b.
const unsigned int bddidx (const bdd &b)
 Returns the index of the variable labeling the bdd b.
void existquant (bdd &dom, bdd &d, int *var, int s)
 Set the bdd dom to $ \exists_{V(var)} \left(dom \wedge d\right)$.
void existquant (bdd &dom, bdd &d, int a, int b)
 Set the bdd dom to $ \exists_{V([x_a,\dots,x_b])} \left(dom \wedge d\right)$.
void existquant (bdd &dom, bdd &d, bdd &pr)
 Set the bdd dom to $ \exists_{V(pr)} \left(dom \wedge d\right)$.
bdd eliminate (bdd &d, int a, int b)
 Set the bdd d to $ \exists_{V([x_a,\dots,x_b])} d$.
bdd eliminate (bdd &d, bdd &e)
 Set the bdd d to $ \exists_{V(e)} d$.
bdd eliminate (bdd &d, int *var, int s)
 Set the bdd d to $ \exists_{V(var)} d$.
void markdummy (int a, int b)
 Marks in the table, whether dummy nodes have been allocated so far.
void dispose (void)
 Free the node table.
void dispose (int offset, int range, int freenodes=0)
 Free variable in the node table.
void dispose (bdd &d)
 Free nodes for bdd d in the table.
int allocate (int r)
 Subscribe a variable to the lookup table Returns the offset where the first node starts.
int varnum (void)
 return the number of used bdd variables
void bddntf (std::ostream &, bdd &b)
 Prints a bdd node b with its true edge and its false edge.
void bdd2dot (const bdd &b) const
 Prints dot-output of a bdd b.
unsigned int allocated (void)
 Return the number of allocated bdd variables for the set elements in the table.
void print_set (const bdd &b)
 Set print of a bdd.
int offset (void) const
 Return the current offset of the manager.
void setmaxinc (int max)
 Memory Management.
bool available (void)
 Check whether the buddy library has already been initialized.

Constructor & Destructor Documentation

Gecode::CpltSet::BddMgr::BddMgr ( void   )  [inline]

Default constructor.

Definition at line 188 of file bddmanager.icc.

Gecode::CpltSet::BddMgr::~BddMgr ( void   ) 

Destructor.

Definition at line 51 of file bddmanager.cc.

Member Function Documentation

void Gecode::CpltSet::BddMgr::init ( int  n,
int  c 
) [inline]

Initialize manager with initial nodesize n and cachesize c.

Definition at line 203 of file bddmanager.icc.

bool Gecode::CpltSet::BddMgr::leaf ( const bdd &  b  )  const [inline]

Test whether bdd b is either constant true or constant false.

Definition at line 179 of file bddmanager.icc.

bool Gecode::CpltSet::BddMgr::cfalse ( const bdd &  b  )  const [inline]

Tests whether bdd b is constant false.

Definition at line 182 of file bddmanager.icc.

bool Gecode::CpltSet::BddMgr::ctrue ( const bdd &  b  )  const [inline]

Tests whether bdd b is constant true.

Definition at line 185 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::setorder ( int *  hls  )  [inline]

Sets the variable ordering in the bdd according to hls.

Definition at line 307 of file bddmanager.icc.

unsigned int Gecode::CpltSet::BddMgr::bddsize ( const bdd &  b  )  const [inline]

Return the size of bdd b.

Definition at line 313 of file bddmanager.icc.

unsigned int Gecode::CpltSet::BddMgr::bddpath ( const bdd &  b  )  const [inline]

Return the number of paths of bdd leading to a true nodeb.

Definition at line 316 of file bddmanager.icc.

unsigned int Gecode::CpltSet::BddMgr::numberOfPaths ( bdd &  b  ) 

Return the total number of paths of bdd b.

Definition at line 44 of file bddmanager.cc.

bdd Gecode::CpltSet::BddMgr::bddpos ( int  i  )  const [inline]

Return bdd at position i in bdd lookup table.

Definition at line 226 of file bddmanager.icc.

bdd Gecode::CpltSet::BddMgr::negbddpos ( int  i  )  const [inline]

Return negated bdd at position i in bdd lookup table.

Definition at line 266 of file bddmanager.icc.

int Gecode::CpltSet::BddMgr::lbCard ( const bdd &  b  )  [inline]

Get lower cardinality bound for breadth-first iteration.

Definition at line 281 of file bddmanager.icc.

int Gecode::CpltSet::BddMgr::ubCard ( const bdd &  b  )  [inline]

Get upper cardinality bound for breadth-first iteration.

Definition at line 284 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::lbCard ( const bdd &  b,
int  l 
) [inline]

Set lower cardinality bound for breadth-first iteration.

Definition at line 287 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::ubCard ( const bdd &  b,
int  r 
) [inline]

Set upper cardinality bound for breadth-first iteration.

Definition at line 290 of file bddmanager.icc.

bdd Gecode::CpltSet::BddMgr::ite ( const bdd &  v,
const bdd &  t,
const bdd &  f 
) [inline]

Construct the Bdd for $ \mbox{if} v \mbox{then} t \mbox{else} f$.

Definition at line 293 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::mark ( const bdd &  b  )  [inline]

Marks the bdd b.

Definition at line 269 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::unmark ( const bdd &  b  )  [inline]

Unmarks the bdd b.

Definition at line 272 of file bddmanager.icc.

bool Gecode::CpltSet::BddMgr::marked ( const bdd &  b  )  const [inline]

Check whether b is marked.

Definition at line 275 of file bddmanager.icc.

int Gecode::CpltSet::BddMgr::node_level ( const bdd &  b  )  const [inline]

Definition at line 278 of file bddmanager.icc.

int Gecode::CpltSet::BddMgr::bdd2var ( int  i  )  [inline]

Returns the position of variable i in the current variable order.

Definition at line 298 of file bddmanager.icc.

int Gecode::CpltSet::BddMgr::var2bdd ( int  i  )  [inline]

Returns the variable at position i in the current variable order.

Definition at line 301 of file bddmanager.icc.

int Gecode::CpltSet::BddMgr::dummy ( void   )  [inline]

Returns the offset of the first dummy var if there is any.

Definition at line 304 of file bddmanager.icc.

bdd Gecode::CpltSet::BddMgr::iftrue ( bdd &  b  )  [inline]

Return the true branch of a bdd b.

Definition at line 321 of file bddmanager.icc.

bdd Gecode::CpltSet::BddMgr::iffalse ( bdd &  b  )  [inline]

Return the false branch of a bdd b.

Definition at line 324 of file bddmanager.icc.

const unsigned int Gecode::CpltSet::BddMgr::bddidx ( const bdd &  b  )  [inline]

Returns the index of the variable labeling the bdd b.

Definition at line 327 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::existquant ( bdd &  dom,
bdd &  d,
int *  var,
int  s 
) [inline]

Set the bdd dom to $ \exists_{V(var)} \left(dom \wedge d\right)$.

Definition at line 342 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::existquant ( bdd &  dom,
bdd &  d,
int  a,
int  b 
) [inline]

Set the bdd dom to $ \exists_{V([x_a,\dots,x_b])} \left(dom \wedge d\right)$.

Definition at line 349 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::existquant ( bdd &  dom,
bdd &  d,
bdd &  pr 
) [inline]

Set the bdd dom to $ \exists_{V(pr)} \left(dom \wedge d\right)$.

Definition at line 362 of file bddmanager.icc.

bdd Gecode::CpltSet::BddMgr::eliminate ( bdd &  d,
int  a,
int  b 
) [inline]

Set the bdd d to $ \exists_{V([x_a,\dots,x_b])} d$.

Definition at line 367 of file bddmanager.icc.

bdd Gecode::CpltSet::BddMgr::eliminate ( bdd &  d,
bdd &  e 
) [inline]

Set the bdd d to $ \exists_{V(e)} d$.

Definition at line 378 of file bddmanager.icc.

bdd Gecode::CpltSet::BddMgr::eliminate ( bdd &  d,
int *  var,
int  s 
) [inline]

Set the bdd d to $ \exists_{V(var)} d$.

Definition at line 383 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::markdummy ( int  a,
int  b 
) [inline]

Marks in the table, whether dummy nodes have been allocated so far.

Definition at line 389 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::dispose ( void   )  [inline]

Free the node table.

Definition at line 192 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::dispose ( int  offset,
int  range,
int  freenodes = 0 
) [inline]

Free variable in the node table.

Definition at line 396 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::dispose ( bdd &  d  )  [inline]

Free nodes for bdd d in the table.

Definition at line 410 of file bddmanager.icc.

int Gecode::CpltSet::BddMgr::allocate ( int  r  )  [inline]

Subscribe a variable to the lookup table Returns the offset where the first node starts.

Definition at line 229 of file bddmanager.icc.

int Gecode::CpltSet::BddMgr::varnum ( void   )  [inline]

return the number of used bdd variables

Definition at line 427 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::bddntf ( std::ostream &  os,
bdd &  b 
) [inline]

Prints a bdd node b with its true edge and its false edge.

Definition at line 419 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::bdd2dot ( const bdd &  b  )  const [inline]

Prints dot-output of a bdd b.

Definition at line 339 of file bddmanager.icc.

unsigned int Gecode::CpltSet::BddMgr::allocated ( void   )  [inline]

Return the number of allocated bdd variables for the set elements in the table.

Definition at line 259 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::print_set ( const bdd &  b  )  [inline]

Set print of a bdd.

Definition at line 221 of file bddmanager.icc.

int Gecode::CpltSet::BddMgr::offset ( void   )  const [inline]

Return the current offset of the manager.

Definition at line 433 of file bddmanager.icc.

void Gecode::CpltSet::BddMgr::setmaxinc ( int  max  )  [inline]

Memory Management.

Definition at line 439 of file bddmanager.icc.

bool Gecode::CpltSet::BddMgr::available ( void   )  [inline]

Check whether the buddy library has already been initialized.

Definition at line 176 of file bddmanager.icc.

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