Main Page | Namespace List | Class Hierarchy | Class List | File List | Namespace Members | Class Members | File Members

gbdd::Space Class Reference

An abstract interface to BDD implementations. More...

#include <space.h>

Inheritance diagram for gbdd::Space:

gbdd::BuddySpace gbdd::GSpace gbdd::MutexSpace List of all members.

Public Types

typedef Domain::Var Var
typedef unsigned long int Bdd
typedef BinaryFunction< bool,
bool, bool > 
ProductFunction
typedef UnaryFunction< bool,
bool > 
UnaryProductFunction
typedef UnaryFunction< Var,
bool > 
VarPredicate
typedef Domain::VarMap VarMap

Public Member Functions

virtual ~Space ()
virtual void gc ()=0
 Garbage collect space.

virtual void lock_gc ()
 Prevent garbage collection.

virtual void unlock_gc ()
 Unprevent garbate collection.

virtual void bdd_ref (Bdd p)=0
 Reference BDD.

virtual void bdd_unref (Bdd p)=0
 Unreference BDD.

virtual bool bdd_is_leaf (Bdd p)=0
 Test for leaf.

virtual bool bdd_leaf_value (Bdd p)=0
 Get leaf value.

virtual Bdd bdd_then (Bdd p)=0
 Get then-branch.

virtual Bdd bdd_else (Bdd p)=0
 Get else-branch.

virtual Var bdd_var (Bdd p)=0
 Get variable of internal node.

virtual Bdd bdd_leaf (bool v)=0
 Construct leaf node.

Bdd bdd_true ()
 Construct true node.

Bdd bdd_false ()
 Construct false node.

virtual Bdd bdd_var_true (Var v)=0
 Construct Bdd node for a variable being true.

virtual Bdd bdd_var_false (Var v)=0
 Construct Bdd node for a variable being false.

virtual Bdd bdd_var_then_else (Var v, Bdd p_then, Bdd p_else)=0
 Construct an internal node.

virtual Var bdd_highest_var (Bdd p)
 Find highest variable in BDD.

virtual Bdd bdd_project (Bdd p, VarPredicate &fn_var, ProductFunction &fn_prod)=0
 Project BDD.

virtual Bdd bdd_rename (Bdd p, const VarMap &fn)=0
 Rename BDD.

virtual Bdd bdd_product (Bdd p, Bdd q, ProductFunction &fn)=0
 BDD product.

virtual Bdd bdd_product (Bdd p, UnaryProductFunction &fn)=0
 BDD unary product.

template<class _VarPredicate, class _ProductFunction> Bdd bdd_project (Bdd p, _VarPredicate fn_var, _ProductFunction fn_prod)
 Project BDD.

template<class _ProductFunction> Bdd bdd_product (Bdd p, Bdd q, _ProductFunction fn)
 BDD product.

template<class _UnaryProductFunction> Bdd bdd_product (Bdd p, _UnaryProductFunction fn)
 BDD unary product.

virtual void bdd_print (ostream &os, Bdd p)=0
virtual unsigned int get_n_nodes (void) const
 Get number of nodes in Space.


Static Public Member Functions

Spacecreate_default (bool diagnostics=false)

Detailed Description

An abstract interface to BDD implementations.


Member Typedef Documentation

typedef unsigned long int gbdd::Space::Bdd
 

An identity of a BDD

typedef BinaryFunction<bool, bool, bool> gbdd::Space::ProductFunction
 

typedef UnaryFunction<bool, bool> gbdd::Space::UnaryProductFunction
 

typedef Domain::Var gbdd::Space::Var
 

A variable in a BDD

typedef Domain::VarMap gbdd::Space::VarMap
 

typedef UnaryFunction<Var, bool> gbdd::Space::VarPredicate
 


Constructor & Destructor Documentation

virtual gbdd::Space::~Space  )  [inline, virtual]
 


Member Function Documentation

virtual Bdd gbdd::Space::bdd_else Bdd  p  )  [pure virtual]
 

Get else-branch.

Parameters:
p Bdd to get else-branch of
Returns:
Else-branch of p

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

Bdd gbdd::Space::bdd_false  )  [inline]
 

Construct false node.

Returns:
The leaf Bdd with value false

Space::Var gbdd::Space::bdd_highest_var Bdd  p  )  [virtual]
 

Find highest variable in BDD.

Parameters:
p Bdd to find highest variable of
Returns:
Highest variable in BDD, or 0 if none

Reimplemented in gbdd::BuddySpace, and gbdd::MutexSpace.

virtual bool gbdd::Space::bdd_is_leaf Bdd  p  )  [pure virtual]
 

Test for leaf.

Parameters:
p Bdd to test
Returns:
Whether p is a leaf

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

virtual Bdd gbdd::Space::bdd_leaf bool  v  )  [pure virtual]
 

Construct leaf node.

Parameters:
v Value of leaf node
Returns:
The leaf Bdd with value v

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

virtual bool gbdd::Space::bdd_leaf_value Bdd  p  )  [pure virtual]
 

Get leaf value.

Parameters:
p Bdd to get leaf of
Returns:
The value of p

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

virtual void gbdd::Space::bdd_print ostream &  os,
Bdd  p
[pure virtual]
 

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

template<class _UnaryProductFunction>
Space::Bdd gbdd::Space::bdd_product Bdd  p,
_UnaryProductFunction  fn
 

BDD unary product.

Parameters:
p BDD
fn Product function
Returns:
The BDD representing fn(p)

template<class _ProductFunction>
Space::Bdd gbdd::Space::bdd_product Bdd  p,
Bdd  q,
_ProductFunction  fn
 

BDD product.

Parameters:
p First BDD
q Second BDD
fn Product function
Returns:
The BDD representing fn(p, q)

virtual Bdd gbdd::Space::bdd_product Bdd  p,
UnaryProductFunction fn
[pure virtual]
 

BDD unary product.

Parameters:
p BDD
fn Product function
Returns:
The BDD representing fn(p)

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

virtual Bdd gbdd::Space::bdd_product Bdd  p,
Bdd  q,
ProductFunction fn
[pure virtual]
 

BDD product.

Parameters:
p First BDD
q Second BDD
fn Product function
Returns:
The BDD representing fn(p, q)

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

template<class _VarPredicate, class _ProductFunction>
Space::Bdd gbdd::Space::bdd_project Bdd  p,
_VarPredicate  fn_var,
_ProductFunction  fn_prod
 

Project BDD.

Parameters:
p BDD to project
fn_var Predicate describing variables to project
fn_prod Product function
Returns:
The projected BDD on variables v with fn_var (v) using product function fn_prod

virtual Bdd gbdd::Space::bdd_project Bdd  p,
VarPredicate fn_var,
ProductFunction fn_prod
[pure virtual]
 

Project BDD.

Parameters:
p BDD to project
fn_var Predicate describing variables to project
fn_prod Product function
Returns:
The projected BDD on variables v with fn_var (v) using product function fn_prod

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

virtual void gbdd::Space::bdd_ref Bdd  p  )  [pure virtual]
 

Reference BDD.

Increases reference count of p

Parameters:
p Bdd to reference

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

virtual Bdd gbdd::Space::bdd_rename Bdd  p,
const VarMap fn
[pure virtual]
 

Rename BDD.

Parameters:
p BDD to project
fn Renaming map
Returns:
The renamed BDD such that variables v are renamed to fn(v)

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

virtual Bdd gbdd::Space::bdd_then Bdd  p  )  [pure virtual]
 

Get then-branch.

Parameters:
p Bdd to get then-branch of
Returns:
Then-branch of p

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

Bdd gbdd::Space::bdd_true  )  [inline]
 

Construct true node.

Returns:
The leaf Bdd with value true

virtual void gbdd::Space::bdd_unref Bdd  p  )  [pure virtual]
 

Unreference BDD.

Decreases reference count of p

Parameters:
p Bdd to unreference

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

virtual Var gbdd::Space::bdd_var Bdd  p  )  [pure virtual]
 

Get variable of internal node.

Parameters:
p Bdd to get variable of
Returns:
Variable of internal node p

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

virtual Bdd gbdd::Space::bdd_var_false Var  v  )  [pure virtual]
 

Construct Bdd node for a variable being false.

Parameters:
v Variable of node
Returns:
A Bdd representing that v is false

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

virtual Bdd gbdd::Space::bdd_var_then_else Var  v,
Bdd  p_then,
Bdd  p_else
[pure virtual]
 

Construct an internal node.

Parameters:
v Variable of internal node
p_then Then-branch of node
p_else Else-branch of node
Returns:
The BDD representing (v => p_then ) AND ( v => p_else )

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

virtual Bdd gbdd::Space::bdd_var_true Var  v  )  [pure virtual]
 

Construct Bdd node for a variable being true.

Parameters:
v Variable of node
Returns:
A Bdd representing that v is true

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

Space * gbdd::Space::create_default bool  diagnostics = false  )  [static]
 

virtual void gbdd::Space::gc  )  [pure virtual]
 

Garbage collect space.

Implemented in gbdd::BuddySpace, gbdd::GSpace, and gbdd::MutexSpace.

unsigned int gbdd::Space::get_n_nodes void   )  const [virtual]
 

Get number of nodes in Space.

To be sure not to get dead nodes in the count, you have to lock the space and do a garbage collection before calling this

Returns:
Number of nodes

Reimplemented in gbdd::BuddySpace, and gbdd::MutexSpace.

void gbdd::Space::lock_gc  )  [virtual]
 

Prevent garbage collection.

Reimplemented in gbdd::MutexSpace.

void gbdd::Space::unlock_gc  )  [virtual]
 

Unprevent garbate collection.

Reimplemented in gbdd::MutexSpace.


The documentation for this class was generated from the following files:
Generated on Mon Aug 1 04:04:44 2005 for gbdd by doxygen 1.3.6