gbdd::Bdd Class Reference

A BDD in some space. More...

#include <bdd.h>

Inheritance diagram for gbdd::Bdd:

List of all members.

Public Types
typedef Space::Var	Var
typedef Space::VarMap	VarMap
Public Member Functions
	Bdd ()
	Create undefined BDD.
	Bdd (Space *space, bool v=false)
	Constructs a leaf BDD.
	~Bdd ()
	Destructor.
	Bdd (const Bdd &p)
	Copy constructor.
Space *	get_space () const
	Get space of BDD.
Factory *	ptr_factory () const
BoolConstraint *	ptr_convert (const BoolConstraint::Factory &f) const
Bdd	operator! () const
	Negates BDD.
Bdd	operator| (const Bdd &p2) const
	OR operator.
Bdd	operator & (const Bdd &p2) const
	AND operator.
Bdd	operator- (const Bdd &p2) const
	Set difference.
Bdd &	operator= (const Bdd &p)
	Assignment operator.
Bdd &	operator|= (const Bdd &p)
	Assignment OR.
Bdd &	operator &= (const Bdd &p)
	Assignment AND.
Bdd &	operator-= (const Bdd &p)
	Assignment Set minus.
virtual bool	operator== (const StructureConstraint &b2) const
	Equality.
bool	bdd_is_leaf () const
	Test if BDD is a leaf.
bool	bdd_leaf_value () const
	Get leaf value of BDD.
Bdd	bdd_then () const
	Get then-branch of BDD.
Bdd	bdd_else () const
	Get else-branch of BDD.
Var	bdd_var () const
	Get variable of this node.
bool	value_member (const Domain &vs, unsigned int v) const
	Membership of value.
Bdd	value_follow (const Domain &vs, unsigned int v) const
	Membership of value.
template<class Product> Bdd	product (Product fn) const
	Product.
template<class VarPredicate, class Product> Bdd	project (VarPredicate fn_var, Product fn_prod) const
	Projection.
template<class VarPredicate> Bdd	project (VarPredicate fn_var) const
	OR projection.
template<class VarPredicate> Bdd	exists (VarPredicate fn_var) const
	Synonym for OR projection.
template<class VarPredicate> Bdd	forall (VarPredicate fn_var) const
	Forall projection.
Bdd	rename (const VarMap &map) const
	Rename according to map.
Bdd	rename (const Domain &vs1, const Domain &vs2) const
	Renaming between variable sets.
unsigned int	n_assignments (const Domain &vs) const
	Get number of possible assignments.
set< unsigned int >	assignments_value (const Domain &vs) const
	Get all assignments interpreted as values.
hash_set< Bdd >	with_geq_var (Var v) const
	Get subtrees with variable over some threshold.
Bdd	with_image_geq_var (Bdd im, Var v) const
	Construct BDD representing the set of assignments leading to a subtree.
hash_set< Bdd >	nodes () const
	Return all reachable nodes in this BDD.
Var	highest_var () const
	Get highest variable.
Var	lowest_var () const
	Get lowest variable.
Domain	vars () const
	Get set of variables in BDD.
bool	is_false () const
	Test for false BDD.
bool	is_true () const
	Test for true BDD.
unsigned long int	hash (void) const
	Hash value of this BDD.
ostream &	print_dot (ostream &os) const
	Print a dot representation of the BDD.
virtual Bdd *	ptr_rename (VarMap map) const
	Rename variables.
virtual Bdd *	ptr_project (Domain vs) const
	Project variables.
virtual Bdd *	ptr_constrain_value (Var v, bool value) const
	Constrain variable.
virtual Bdd *	ptr_product (const StructureConstraint &b2, bool(*fn)(bool v1, bool v2)) const
	Product.
virtual Bdd *	ptr_negate () const
	Negation.
virtual Bdd *	ptr_clone () const
	Cloning.
Static Public Member Functions
template<class Product> Bdd	var_product (Space *space, Var v1, Var v2, Product fn)
	Product of two variables.
Bdd	var_equal (Space *space, Var v1, Var v2)
	Equality of two variables.
Bdd	var_true (Space *space, Var v)
	Construct BDD that tests for variable.
Bdd	var_false (Space *space, Var v)
	Construct BDD that tests for variable.
Bdd	var_then_else (Space *space, Var v, Bdd p_then, Bdd p_else)
	Construct BDD.
unsigned int	n_vars_needed (unsigned int n_values)
	Get number of variables needed for encoding of values.
Bdd	value (Space *space, const Domain &vs, unsigned int v)
	Encodes a value as a BDD using a binary representation.
Bdd	value_range (Space *space, const Domain &vs, unsigned int from_v, unsigned int to_v)
	Encodes a value range as a BDD.
template<class Product> Bdd	vars_product (Space *space, const Domain &vs1, const Domain &vs2, Product fn)
Bdd	vars_equal (Space *space, const Domain &vs1, const Domain &vs2)
	Construct BDD representing equality between variables.
template<class Product> Bdd	bdd_product (const Bdd &p1, const Bdd &p2, Product fn)
	Product.
void	gc (Space *space)
	Garbage collect BDD space.
Friends
struct	hash< Bdd >
bool	operator== (const Bdd &p1, const Bdd &p2)
	Equality.
ostream &	operator<< (ostream &s, const Bdd &p)
	Print a textual representation on a stream.

---

Detailed Description

A BDD in some space.

The following code illustrates the typical use of BDDs in gbdd. It creates a domain vs containing the variables 0, 1, 2 and 3. Using this set of variables, it encodes integer values using a binary encoding, creating two BDDs. The first BDD p represents the set {2,3} and the second BDD q represents the set {3,4}. The it tests whether p intersected with q gives the set {3}.

See also gbdd::Bdd::Vars, a simplified way to create BDDs.

Space *space = Space::create_default();

Domain vs(0,4);

Bdd p = Bdd::value(space, vs, 2) | Bdd::value(space, vs, 3);

Bdd q = Bdd::value(space, vs, 3) | Bdd::value(space, vs, 4);

return (p & q) == Bdd::value(space, vs, 3);

---

Member Typedef Documentation

typedef Space::Var gbdd::Bdd::Var

Variable in a BDD Reimplemented from gbdd::StructureConstraint.

typedef Space::VarMap gbdd::Bdd::VarMap

Mapping from variables to variables Reimplemented from gbdd::StructureConstraint.

---

Constructor & Destructor Documentation

gbdd::Bdd::Bdd (   )

Create undefined BDD.

gbdd::Bdd::Bdd (  Space *  space, bool  v = false )

Constructs a leaf BDD. Parameters: space  Space to create leaf BDD in v  Value of leaf

gbdd::Bdd::~Bdd (   )

Destructor.

gbdd::Bdd::Bdd (  const Bdd &  p  )

Copy constructor.

---

Member Function Documentation

set< unsigned int > gbdd::Bdd::assignments_value (  const Domain &  vs  )  const

Get all assignments interpreted as values. Calculates assignments to variables in vs that makes the BDD true. All variables in BDD must be in vs. Parameters: vs  Variable to assign values to Returns: The set of values where the encoding in vs is an assignment

Bdd gbdd::Bdd::bdd_else (   )  const

Get else-branch of BDD. Returns: else-branch of this BDD

bool gbdd::Bdd::bdd_is_leaf (   )  const

Test if BDD is a leaf. Returns: True if this BDD is a leaf

bool gbdd::Bdd::bdd_leaf_value (   )  const

Get leaf value of BDD. Returns: Leaf value of this BDD

template<class Product> Bdd gbdd::Bdd::bdd_product (  const Bdd &  p1, const Bdd &  p2, Product  fn )  [static]

Product. Parameters: p1  First BDD p2  Second BDD fn  Product function Returns: Product of p1 and p2 with respect to fn

Bdd gbdd::Bdd::bdd_then (   )  const

Get then-branch of BDD. Returns: then-branch of this BDD

Bdd::Var gbdd::Bdd::bdd_var (   )  const

Get variable of this node. Returns: Variable of this node

template<class VarPredicate> Bdd gbdd::Bdd::exists (  VarPredicate  fn_var  )  const [inline]

Synonym for OR projection. Parameters: fn_var  Predicate describing variables to project Returns: Projection of this BDD with OR with respect to all variables v such that fn_var(v)

template<class VarPredicate> Bdd gbdd::Bdd::forall (  VarPredicate  fn_var  )  const [inline]

Forall projection. Parameters: fn_var  Predicate describing variables to project Returns: !((!p).exists(fn_var)) for p as this BDD

void gbdd::Bdd::gc (  Space *  space  )  [static]

Garbage collect BDD space.

Space* gbdd::Bdd::get_space (   )  const [inline]

Get space of BDD. Returns: The implementation space of this BDD

unsigned long int gbdd::Bdd::hash (  void   )  const

Hash value of this BDD. Returns: Hash value for BDD

Space::Var gbdd::Bdd::highest_var (   )  const [virtual]

Get highest variable. Returns: The highest variable in this BDD Implements gbdd::StructureConstraint.

bool gbdd::Bdd::is_false (   )  const

Test for false BDD. Returns: true if BDD is false

bool gbdd::Bdd::is_true (   )  const

Test for true BDD. Returns: true if BDD is true

Space::Var gbdd::Bdd::lowest_var (   )  const [virtual]

Get lowest variable. Returns: The lowest variable in this BDD Implements gbdd::StructureConstraint.

unsigned int gbdd::Bdd::n_assignments (  const Domain &  vs  )  const

Get number of possible assignments. Calculates the number of assignments to variables in vs that makes the BDD true. All variables in BDD must be in vs. Parameters: vs  Variable to assign values to Returns: The number of possible assignments

unsigned int gbdd::Bdd::n_vars_needed (  unsigned int  n_values  )  [static]

Get number of variables needed for encoding of values. Parameters: n_values  Number of values to represent Returns: Minimum number of variables needed to encode 0..n_values - 1

hash_set< Bdd > gbdd::Bdd::nodes (   )  const

Return all reachable nodes in this BDD. Returns: All nodes reachable from this BDD using bdd_then and bdd_else

Bdd gbdd::Bdd::operator & (  const Bdd &  p2  )  const

AND operator. Parameters: p2  BDD to and with Returns: This BDD and'ed with p2

Bdd & gbdd::Bdd::operator &= (  const Bdd &  p  )

Assignment AND.

Bdd gbdd::Bdd::operator! (   )  const

Negates BDD. Returns: The negated BDD

Bdd gbdd::Bdd::operator- (  const Bdd &  p2  )  const

Set difference. Parameters: p2  BDD to minus with Returns: This BDD minus'ed with p2

Bdd & gbdd::Bdd::operator-= (  const Bdd &  p  )

Assignment Set minus.

Bdd & gbdd::Bdd::operator= (  const Bdd &  p  )

Assignment operator.

bool gbdd::Bdd::operator== (  const StructureConstraint &  b2  )  const [virtual]

Equality. Parameters: b2  structure constraint object to compare with Returns: Whether this object and b2 are equivalent Implements gbdd::StructureConstraint.

Bdd gbdd::Bdd::operator| (  const Bdd &  p2  )  const

OR operator. Parameters: p2  BDD to or with Returns: This BDD or'ed with p2

Bdd & gbdd::Bdd::operator|= (  const Bdd &  p  )

Assignment OR.

ostream & gbdd::Bdd::print_dot (  ostream &  os  )  const

Print a dot representation of the BDD. Code inspired by the Cudd_DumpDot function in the CUDD package by Fabio Somenzi Parameters: os  Stream to write to Returns: The stream os

template<class Product> Bdd gbdd::Bdd::product (  Product  fn  )  const

Product. Parameters: fn  Product function Returns: Product of this BDD with respect to fn

template<class VarPredicate> Bdd gbdd::Bdd::project (  VarPredicate  fn_var  )  const [inline]

OR projection. Parameters: fn_var  Predicate describing variables to project Returns: Projection of this BDD with OR with respect to all variables v such that fn_var(v)

template<class VarPredicate, class Product> Bdd gbdd::Bdd::project (  VarPredicate  fn_var, Product  fn_prod )  const

Projection. Parameters: fn_var  Predicate describing variables to project fn_prod  Product function to use for projection Returns: Projection of this BDD with fn_prod with respect to all variables v such that fn_var(v)

Bdd * gbdd::Bdd::ptr_clone (   )  const [virtual]

Cloning. Returns: A copy of this object Implements gbdd::StructureConstraint.

Bdd * gbdd::Bdd::ptr_constrain_value (  Var  v, bool  value )  const [virtual]

Constrain variable. Parameters: v  Variable to constrain value  Value to constrain v with Returns: The structure constraint object with set to value Implements gbdd::StructureConstraint.

BoolConstraint * gbdd::Bdd::ptr_convert (  const BoolConstraint::Factory &  f  )  const

Factory* gbdd::Bdd::ptr_factory (   )  const [inline, virtual]

Implements gbdd::BoolConstraint.

Bdd * gbdd::Bdd::ptr_negate (   )  const [virtual]

Negation. Returns: Negation of this object Implements gbdd::StructureConstraint.

Bdd * gbdd::Bdd::ptr_product (  const StructureConstraint &  b2, bool(*  fn)(bool v1, bool v2) )  const [virtual]

Product. Parameters: b2  structure constraint object to take product with fn  Product function Returns: Product of this object and b2 with respect to fn Implements gbdd::StructureConstraint.

Bdd * gbdd::Bdd::ptr_project (  Domain  vs  )  const [virtual]

Project variables. Parameters: vs  Domain to project Returns: The structure constraint object with the variables in vs projected away Implements gbdd::StructureConstraint.

Bdd * gbdd::Bdd::ptr_rename (  VarMap  map  )  const [virtual]

Rename variables. Parameters: map  Renaming Returns: The structure constraint object renamed with map Implements gbdd::StructureConstraint.

Bdd gbdd::Bdd::rename (  const Domain &  vs1, const Domain &  vs2 )  const [inline]

Renaming between variable sets. Parameters: vs1  Current set of variables vs2  New set of variables Returns: The renamed BDD such that vs1[i] is renamed to vs2[i]

Bdd gbdd::Bdd::rename (  const VarMap &  map  )  const [inline]

Rename according to map. Parameters: map  Map describing renaming Returns: The BDD renamed with map

Bdd gbdd::Bdd::value (  Space *  space, const Domain &  vs, unsigned int  v )  [static]

Encodes a value as a BDD using a binary representation. Parameters: space  BDD space vs  Variables to use for encoding v  Value to encode Returns: A BDD using the variables vs to encode the value v

Bdd gbdd::Bdd::value_follow (  const Domain &  vs, unsigned int  v )  const

Membership of value. Follows a value encoded in the variables that must be lowest in the BDD (i.e. at the top) Parameters: vs  Variables to encode value in v  Value to encode Returns: The BDD gain by following v encoded with vs

bool gbdd::Bdd::value_member (  const Domain &  vs, unsigned int  v )  const

Membership of value. Tests the assignment of vs by encoding v is a valid assignment in the BDD Parameters: vs  Variables to encode value in v  Value to encode Returns: True if v encoded in vs is a member.

Bdd gbdd::Bdd::value_range (  Space *  space, const Domain &  vs, unsigned int  from_v, unsigned int  to_v )  [static]

Encodes a value range as a BDD. Parameters: space  BDD space vs  Variables to use for encoding from_v  Beginning of interval to encode to_v  End of interval to encode Returns: A BDD using the variable vs to encode the value range [from_v ..to_v]

Bdd gbdd::Bdd::var_equal (  Space *  space, Var  v1, Var  v2 )  [inline, static]

Equality of two variables. Parameters: space  Space of returned BDD v1  First variable v2  Second variable Returns: The BDD representing v1 == v2

Bdd gbdd::Bdd::var_false (  Space *  space, Var  v )  [static]

Construct BDD that tests for variable. Parameters: space  Space that BDD should reside in v  Variable to test Returns: The BDD testing if v is false

template<class Product> Bdd gbdd::Bdd::var_product (  Space *  space, Var  v1, Var  v2, Product  fn )  [static]

Product of two variables. Parameters: space  Space of returned BDD v1  First variable v2  Second variable fn  Product function Returns: The BDD representing fn(v1,v2)

Bdd gbdd::Bdd::var_then_else (  Space *  space, Var  v, Bdd  p_then, Bdd  p_else )  [static]

Construct BDD. Parameters: space  Space that BDD should reside in v  Variable to test p_then  then-branch i v is true p_else  else-branch i v is false Returns: The BDD testing variable v taking p_then if v is true and p_else if v is false

Bdd gbdd::Bdd::var_true (  Space *  space, Var  v )  [static]

Construct BDD that tests for variable. Parameters: space  Space that BDD should reside in v  Variable to test Returns: The BDD testing if v is true

Domain gbdd::Bdd::vars (   )  const

Get set of variables in BDD. Returns: The set of variables that exist in any node in this BDD

Bdd gbdd::Bdd::vars_equal (  Space *  space, const Domain &  vs1, const Domain &  vs2 )  [static]

Construct BDD representing equality between variables. Parameters: space  Space for resulting BDD vs1  Domain for one set of variables vs2  Domain for another set of variables Returns: A BDD representing assignments where the variables in vs1 are equal to the correspondning variable in vs2

template<class Product> Bdd gbdd::Bdd::vars_product (  Space *  space, const Domain &  vs1, const Domain &  vs2, Product  fn )  [static]

vars_product: Parameters: space  Space of BDD returned vs1  First set of variables vs2  Second set of variables fn  Product function Product of several variables Returns: The BDD representing product between variables in vs1 and vs2. The i'th variable in vs1 if related with fn to the i'th variable in vs2.

hash_set< Bdd > gbdd::Bdd::with_geq_var (  Var  v  )  const

Get subtrees with variable over some threshold. Parameters: v  Threshold value Returns: The set of subtrees of this BDD that has a variable node with a variable greater or equal to v and do not contain such subtree.

Bdd gbdd::Bdd::with_image_geq_var (  Bdd  im, Var  v )  const

Construct BDD representing the set of assignments leading to a subtree. Parameters: im  Subtree to check v  Threshold value Returns: The set of assignments of variables less than a leadning to the subtree im.

---

Friends And Related Function Documentation

friend struct hash< Bdd > [friend]

ostream& operator<< (  ostream &  s, const Bdd &  p )  [friend]

Print a textual representation on a stream. Parameters: s  Stream p  BDD to print Prints BDD p on s

bool operator== (  const Bdd &  p1, const Bdd &  p2 )  [friend]

Equality. Parameters: p1  BDD to compare p2  BDD to compare with Returns: Whether p1 is equal to p2

---

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

• bdd.h
• bdd.cc

---