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

gbdd::Bdd Class Reference

A BDD in some space. More...

#include <bdd.h>

Inheritance diagram for gbdd::Bdd:

gbdd::BoolConstraint gbdd::StructureConstraint 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.

Spaceget_space () const
 Get space of BDD.

Factoryptr_factory () const
BoolConstraintptr_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.

Bddoperator= (const Bdd &p)
 Assignment operator.

Bddoperator|= (const Bdd &p)
 Assignment OR.

Bddoperator &= (const Bdd &p)
 Assignment AND.

Bddoperator-= (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< Bddwith_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< Bddnodes () 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 Bddptr_rename (VarMap map) const
 Rename variables.

virtual Bddptr_project (Domain vs) const
 Project variables.

virtual Bddptr_constrain_value (Var v, bool value) const
 Constrain variable.

virtual Bddptr_product (const StructureConstraint &b2, bool(*fn)(bool v1, bool v2)) const
 Product.

virtual Bddptr_negate () const
 Negation.

virtual Bddptr_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:
Generated on Thu Aug 12 13:21:42 2004 for gbdd by doxygen 1.3.6