gbdd::Space Class Reference

An abstract interface to BDD implementations. More...

#include <space.h>

Inheritance diagram for gbdd::Space:

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
Space *	create_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:

• space.h
• space.cc

---