SDD Class Reference

This class is the public interface for manipulating Data Decision Diagrams. More...

#include <SDD.h>

Inheritance diagram for SDD:

Collaboration diagram for SDD:

Public Member Functions
	SDD (const SDD &)
	Copy constructor. More...
	SDD (const GSDD &g=GSDD::null)
	Copy constructor from base class GDDD, also default DDD constructor to empty set. More...
	SDD (int var, const DataSet &val, const GSDD &d=one)
	The most common way for the user of creating DDD. More...
	SDD (int var, const GSDD &val, const GSDD &d=one)
	SDD (int var, const SDD &val, const GSDD &d=one)
virtual	~SDD ()
	Destructor, maintains refCount. More...
Assignment operators.
SDD &	operator= (const GSDD &)
	Overloaded behavior for assignment operator, maintains reference counting. More...
SDD &	operator= (const SDD &)
	Overloaded behavior for assignment operator, maintains reference counting. More...
Comparisons for hash and map storage
bool	operator== (const GSDD &g) const
	Comparison between DDD. More...
bool	operator!= (const GSDD &g) const
	Comparison between DDD. More...
bool	operator< (const GSDD &g) const
	Total ordering function between DDD. More...
unsigned int	refCounter () const
	Returns current reference count of a node. More...
unsigned long int	size () const
	Returns the size in number of nodes of a SDD structure. More...
std::pair< unsigned long int, unsigned long int >	node_size () const
size_t	nbsons () const
	Returns the number of successors of a given node. This is the size of the arc array of the node. More...
long double	nbStates () const
	Returns the number of states or paths represented by a given node. More...
DataSet implementation interface
This is the implementation of the DataSet class interface used in SDD context. These functions allow to reference SDD from SDD arcs. IMPORTANT Remember to delete returned values after use. Note these functions are not resistant to incompatible DataSet types. When these functions have a parameter "b", it should be a reference to a SDD from proper behavior.
DataSet *	newcopy () const
	Return a new copy of a SDD. More...
DataSet *	set_intersect (const DataSet &b) const
	Compute intersection of two SDD. More...
DataSet *	set_union (const DataSet &b) const
	Compute union of two SDD. More...
DataSet *	set_minus (const DataSet &b) const
	Compute set difference of two SDD. More...
bool	empty () const
	Return true if this is the empty set. More...
DataSet *	empty_set () const
	Returns a pointer to GSDD::null. More...
bool	set_equal (const DataSet &b) const
	Compares to DataSet for equality. More...
bool	set_less_than (const DataSet &b) const
	Compares two sets with a total order. More...
long double	set_size () const
	Compares to DataSet for equality. More...
size_t	set_hash () const
	Returns a hash key for the SDD. More...
void	set_print (std::ostream &os) const
	Textual (human readable) output of a SDD. More...

Static Public Attributes
Terminal nodes defined as constants
static const GSDD	one
	The accepting terminal. This is the basic leaf for accepted sequences. More...
static const GSDD	null
	The non-accepting terminal. More...
static const GSDD	top
	The approximation terminal. More...

Private Member Functions
void	print (std::ostream &os, std::string s) const
	Internal function used in recursion for textual printing of GDDD. More...

Private Attributes
const _GSDD *	concret
	The real implementation class. More...

Public Accessors
int	variable () const
	Returns a node's variable. More...
const_iterator	begin () const
	API for iterating over the arcs of a DDD manually. More...
const_iterator	end () const
	API for iterating over the arcs of a DDD manually. More...
typedef std::vector< std::pair< DataSet *, GSDD > >	Valuation
	To hide how arcs are actually stored. Use GSDD::Valuation to refer to arcs type. More...
typedef Valuation::const_iterator	const_iterator
	To hide how arcs are stored. More...

Memory Management
Broken right now, dont use me or fixme first Returns the number of nodes that would be used to represent a SDD if no unicity table was used.
void	mark () const
	For garbage collection internals. More...
size_t	hash () const
	For storage in a hash table. More...
static unsigned int	statistics ()
	Returns unicity table current size. Gives the number of different nodes created and not yet destroyed. More...
static void	garbage ()
	For garbage collection, do not call this directly, use MemoryManager::garbage() instead. More...
static void	pstats (bool reinit=true)
	Prints some statistics to std::cout. More...
static size_t	peak ()
	Returns the peak size of the DDD unicity table. This value is maintained up to date upon GarbageCollection. More...

Detailed Description

This class is the public interface for manipulating Data Decision Diagrams.

Except when defining new homomorphisms, a user of the library should only manipulate SDD, not GSDD. Reference counting is enabled for SDD, so they will not be destroyed if they are still in use upon garbage collection.

Member Typedef Documentation

const_iterator

typedef Valuation::const_iterator GSDD::const_iterator

inherited

To hide how arcs are stored.

Also for more compact expressions : use GDDD::const_iterator to iterate over the arcs of a DDD

Valuation

typedef std::vector<std::pair<DataSet *,GSDD> > GSDD::Valuation

inherited

To hide how arcs are actually stored. Use GSDD::Valuation to refer to arcs type.

Constructor & Destructor Documentation

SDD() [1/5]

SDD::SDD

(

const SDD &

g

)

Copy constructor.

Constructs a copy, actual data (concret) is not copied. RefCounter is updated however.

References GSDD::concret, and _GSDD::ref().

SDD() [2/5]

SDD::SDD

(

const GSDD &

g = GSDD::null

)

Copy constructor from base class GDDD, also default DDD constructor to empty set.

Increments refCounter of g.concret.

References GSDD::concret, and _GSDD::ref().

SDD() [3/5]

SDD::SDD	(	int	var,
		const DataSet &	val,
		const GSDD &	d = one
	)

The most common way for the user of creating DDD.

This constructor builds a node with a single arc of the form var-val->d. Usually a user will create these single path DDD, possibly by imbrication as in SDD(var1, val1, SDD( var2, val2 )). Then compose them using +, -, *, ^ ... See also GSDD(var,val,d).

Parameters

var	the variable labeling the node
val	the value labeling the arc
d	the successor node or defaults to terminal GDDD::one if none provided

References GSDD::concret, and _GSDD::ref().

SDD() [4/5]

SDD::SDD	(	int	var,
		const GSDD &	val,
		const GSDD &	d = one
	)

References GSDD::concret, and _GSDD::ref().

SDD() [5/5]

SDD::SDD	(	int	var,
		const SDD &	val,
		const GSDD &	d = one
	)

References GSDD::concret, and _GSDD::ref().

~SDD()

SDD::~SDD ( )

virtual

Destructor, maintains refCount.

Note that destroying a DDD does not actually destroy any data, it decrements reference count, so that subsequent MemoryManager::garbage call may truly clear the data.

References GSDD::concret, _GSDD::deref(), and _GSDD::refCounter().

Member Function Documentation

begin()

GSDD::const_iterator GSDD::begin ( ) const

inherited

API for iterating over the arcs of a DDD manually.

i.e. not using a predefined evaluation mechanism such as StrongHom

for (GDDD::const_iterator it = a_gddd.begin() ; it != a_gddd.end() ; it++ ) { // do something }

returns the first arc

References GSDD::concret, and _GSDD::valuation.

Referenced by dotExporter::collect(), hDotExporter::collect(), _SDED_Mult::eval(), _SDED_Minus::eval(), _SDED_Concat::eval(), StrongMLShom::eval(), StrongShom::eval(), sns::SApply2k::eval(), sns::Mult::eval(), sns::SDomExtract::eval(), sns::LocalApply::eval(), sns::SLocalApply::eval(), sns::RecFireSat::eval(), _GShom::eval_skip(), sns::LocalApply::has_image(), sns::SLocalApply::has_image(), StrongShom::has_image(), _GShom::has_image_skip(), sns::LocalApply::invert(), sns::SLocalApply::invert(), MySDDNbStates::nbStates(), GSDD::print(), dotExporter::printColor(), and SddSize::sddsize().

empty()

bool GSDD::empty ( ) const

virtualinherited

Return true if this is the empty set.

Implements DataSet.

References GSDD::null.

Referenced by GSDD::GSDD().

empty_set()

DataSet * GSDD::empty_set ( ) const

virtualinherited

Returns a pointer to GSDD::null.

Implements DataSet.

References GSDD::GSDD().

end()

GSDD::const_iterator GSDD::end ( ) const

inherited

API for iterating over the arcs of a DDD manually.

i.e. not using a predefined evaluation mechanism such as StrongHom

for (GDDD::const_iterator it = a_gddd.begin() ; it != a_gddd.end() ; it++ ) { // do something }

returns a past the end iterator

References GSDD::concret, and _GSDD::valuation.

Referenced by dotExporter::collect(), hDotExporter::collect(), _SDED_Mult::eval(), _SDED_Minus::eval(), _SDED_Concat::eval(), StrongMLShom::eval(), StrongShom::eval(), sns::SApply2k::eval(), sns::Mult::eval(), sns::SDomExtract::eval(), sns::LocalApply::eval(), sns::SLocalApply::eval(), sns::RecFireSat::eval(), _GShom::eval_skip(), sns::LocalApply::has_image(), sns::SLocalApply::has_image(), StrongShom::has_image(), _GShom::has_image_skip(), MySDDNbStates::nbStates(), GSDD::print(), dotExporter::printColor(), and SddSize::sddsize().

garbage()

void GSDD::garbage ( )

staticinherited

For garbage collection, do not call this directly, use MemoryManager::garbage() instead.

Todo:

describe garbage collection algorithm(s) + mark usage homogeneously in one place.

References canonical, MySDDNbStates::clear(), Max_SDD, and _GSDD::set_mark().

Referenced by MemoryManager::garbage().

hash()

size_t GSDD::hash ( ) const

inlineinherited

For storage in a hash table.

References GSDD::concret, and ddd::knuth32_hash().

Referenced by _SDED_Mult::create(), nsMLShom::LeftConcat::hash(), _SDED_Mult::hash(), _SDED_Minus::hash(), _SDED_Concat::hash(), sns::Constant::hash(), sns::SApply2k::hash(), sns::Mult::hash(), sns::LeftConcat::hash(), sns::RightConcat::hash(), and sns::Minus::hash().

mark()

void GSDD::mark ( ) const

virtualinherited

For garbage collection internals.

Marks a GSDD as in use in garbage collection phase.

Implements DataSet.

References GSDD::concret, and _GSDD::mark().

Referenced by sns::Fixpoint::eval(), sns::Constant::mark(), sns::SApply2k::mark(), sns::Mult::mark(), sns::LeftConcat::mark(), sns::RightConcat::mark(), and sns::Minus::mark().

nbsons()

size_t GSDD::nbsons ( ) const

inherited

Returns the number of successors of a given node. This is the size of the arc array of the node.

References GSDD::concret, and _GSDD::valuation.

Referenced by _GShom::eval_skip().

nbStates()

long double GSDD::nbStates ( ) const

inherited

Returns the number of states or paths represented by a given node.

Referenced by Statistic::load(), and GSDD::set_size().

newcopy()

DataSet* GSDD::newcopy ( ) const

inlinevirtualinherited

Return a new copy of a SDD.

Implements DataSet.

References GSDD::GSDD().

Referenced by GSDD::GSDD().

node_size()

std::pair< unsigned long int, unsigned long int > GSDD::node_size ( ) const

inherited

References SddSize::d3res, and SddSize::res.

Referenced by Statistic::load().

operator!=()

bool GSDD::operator!= ( const GSDD &  g ) const

inlineinherited

Comparison between DDD.

Note that comparison is based on "concret" address in unicity table.

Parameters

g	the node to compare to

Returns

true if the nodes are not equal.

References GSDD::concret.

operator<()

bool GSDD::operator< ( const GSDD &  g ) const

inherited

Total ordering function between DDD.

Note that comparison is based on "concret" address in unicity table. This ordering is necessary for hash and map storage of GDDD.

Parameters

g	the node to compare to

Returns

true if argument g is greater than "this" node.

References GSDD::concret.

operator=() [1/2]

SDD & SDD::operator=

(

const GSDD &

g

)

Overloaded behavior for assignment operator, maintains reference counting.

References GSDD::concret, _GSDD::deref(), and _GSDD::ref().

operator=() [2/2]

SDD & SDD::operator=

(

const SDD &

g

)

Overloaded behavior for assignment operator, maintains reference counting.

References GSDD::concret, _GSDD::deref(), and _GSDD::ref().

operator==()

bool GSDD::operator== ( const GSDD &  g ) const

inlineinherited

Comparison between DDD.

Note that comparison is based on "concret" address in unicity table.

Parameters

g	the node to compare to

Returns

true if the nodes are equal.

peak()

size_t GSDD::peak ( )

staticinherited

Returns the peak size of the DDD unicity table. This value is maintained up to date upon GarbageCollection.

References canonical, and Max_SDD.

Referenced by Statistic::load(), and GSDD::pstats().

print()

void GSDD::print ( std::ostream &  os, std::string  s  ) const

privateinherited

Internal function used in recursion for textual printing of GDDD.

References GSDD::begin(), GSDD::end(), GSDD::one, GSDD::top, and GSDD::variable().

pstats()

void GSDD::pstats ( bool  reinit = true )

staticinherited

Prints some statistics to std::cout.

Mostly used in debug and development phase. See also MemoryManager::pstats().

Todo:

allow output in other place than cout. Clean up output.

References GSDD::_GSDD, canonical, and GSDD::peak().

Referenced by MemoryManager::pstats().

refCounter()

unsigned int GSDD::refCounter ( ) const

inherited

Returns current reference count of a node.

Reference count corresponds to the number of SDD that use a given concrete node. No recursive reference counting is used : son nodes may have refCount=0 even if this node has a positive refCounter.

References GSDD::concret, and _GSDD::refCounter().

Referenced by dotExporter::collect().

set_equal()

bool GSDD::set_equal ( const DataSet &  b ) const

virtualinherited

Compares to DataSet for equality.

Implements DataSet.

set_hash()

size_t GSDD::set_hash ( ) const

virtualinherited

Returns a hash key for the SDD.

Implements DataSet.

References GSDD::concret.

set_intersect()

DataSet * GSDD::set_intersect ( const DataSet &  b ) const

virtualinherited

Compute intersection of two SDD.

Implements DataSet.

References GSDD::GSDD().

set_less_than()

bool GSDD::set_less_than ( const DataSet &  b ) const

virtualinherited

Compares two sets with a total order.

Implements DataSet.

set_minus()

DataSet * GSDD::set_minus ( const DataSet &  b ) const

virtualinherited

Compute set difference of two SDD.

Implements DataSet.

References GSDD::GSDD().

set_print()

void GSDD::set_print ( std::ostream &  os ) const

inlinevirtualinherited

Textual (human readable) output of a SDD.

Implements DataSet.

set_size()

long double GSDD::set_size ( ) const

virtualinherited

Compares to DataSet for equality.

Implements DataSet.

References GSDD::nbStates().

set_union()

DataSet * GSDD::set_union ( const DataSet &  b ) const

virtualinherited

Compute union of two SDD.

Implements DataSet.

References GSDD::GSDD().

size()

unsigned long int GSDD::size ( ) const

inherited

Returns the size in number of nodes of a SDD structure.

statistics()

unsigned int GSDD::statistics ( )

staticinherited

Returns unicity table current size. Gives the number of different nodes created and not yet destroyed.

References canonical.

Referenced by MemoryManager::nbSDD().

variable()

int GSDD::variable ( ) const

inherited

Returns a node's variable.

References GSDD::concret, and _GSDD::variable.

Referenced by dotExporter::collect(), hDotExporter::collect(), _SDED_Add::create(), _SDED_Mult::create(), _SDED_Minus::create(), _SDED_Mult::eval(), _SDED_Minus::eval(), _SDED_Concat::eval(), StrongMLShom::eval(), StrongShom::eval(), sns::SApply2k::eval(), sns::Mult::eval(), sns::SDomExtract::eval(), sns::LocalApply::eval(), sns::SLocalApply::eval(), sns::And::eval(), sns::Add::eval(), sns::RecFireSat::eval(), sns::Fixpoint::eval(), _GShom::eval_skip(), GSDD::GSDD(), sns::LocalApply::has_image(), sns::SLocalApply::has_image(), sns::And::has_image(), sns::Fixpoint::has_image(), StrongShom::has_image(), _GShom::has_image_skip(), GSDD::print(), and sns::SApply2k::skip_variable().

Member Data Documentation

concret

const _GSDD* GSDD::concret

privateinherited

The real implementation class.

All true operations are delagated on this pointer. Construction/destruction take care of ensuring concret is only instantiated once in memory.

Referenced by GSDD::begin(), GSDD::end(), GSDD::GSDD(), GSDD::hash(), GSDD::mark(), GSDD::nbsons(), GSDD::operator!=(), GSDD::operator<(), operator=(), GSDD::refCounter(), SDD(), GSDD::set_hash(), GSDD::variable(), and ~SDD().

null

const GSDD GSDD::null

staticinherited

The non-accepting terminal.

As DDD are a zero-suppressed variant of decision diagrams, paths leading to null are suppressed. Only the empty set is represented by null.

Referenced by SDED::add(), apply2k(), _GShom::compose(), _SDED_Add::create(), _SDED_Mult::create(), _SDED_Minus::create(), _SDED_Concat::create(), GSDD::empty(), _SDED_Add::eval(), _SDED_Mult::eval(), _SDED_Minus::eval(), _SDED_Concat::eval(), StrongMLShom::eval(), StrongShom::eval(), sns::Constant::eval(), sns::SApply2k::eval(), sns::Mult::eval(), sns::SDomExtract::eval(), sns::LocalApply::eval(), sns::SLocalApply::eval(), sns::SNotCond::eval(), sns::And::eval(), sns::Add::eval(), sns::RecFireSat::eval(), sns::Fixpoint::eval(), _GShom::eval_skip(), sns::Inter::has_image(), sns::LocalApply::has_image(), sns::SLocalApply::has_image(), sns::SNotCond::has_image(), sns::And::has_image(), sns::Add::has_image(), sns::Compose::has_image(), sns::Fixpoint::has_image(), GShom::has_image(), StrongShom::has_image(), _GShom::has_image_skip(), sns::Compose::invert(), sns::Constant::is_selector(), sns::SApply2k::is_selector(), iterateSDD(), MySDDNbStates::nbStates(), GShom::operator()(), and dotExporter::printLevels().

one

const GSDD GSDD::one

staticinherited

The accepting terminal. This is the basic leaf for accepted sequences.

Referenced by apply2k(), dotExporter::collect(), hDotExporter::collect(), _SDED_Add::create(), _SDED_Mult::create(), _SDED_Minus::create(), _SDED_Concat::create(), StrongMLShom::eval(), StrongShom::eval(), sns::SDomExtract::eval(), sns::LocalApply::eval(), sns::SLocalApply::eval(), sns::SNotCond::eval(), sns::And::eval(), sns::Add::eval(), sns::RecFireSat::eval(), sns::Fixpoint::eval(), _GShom::eval_skip(), sns::LocalApply::has_image(), sns::SLocalApply::has_image(), sns::And::has_image(), sns::Fixpoint::has_image(), StrongShom::has_image(), _GShom::has_image_skip(), iterateSDD(), MySDDNbStates::nbStates(), GSDD::print(), and dotExporter::printLevels().

top

const GSDD GSDD::top

staticinherited

The approximation terminal.

This represents any finite set of assignment sequences. In a "normal" usage pattern, top terminals should not be produced. In fact the result may be incorrect if Top is encountered at any but the highest level.

Referenced by apply2k(), dotExporter::collect(), hDotExporter::collect(), _SDED_Add::create(), _SDED_Mult::create(), _SDED_Minus::create(), _SDED_Concat::create(), StrongMLShom::eval(), StrongShom::eval(), sns::SDomExtract::eval(), sns::LocalApply::eval(), sns::SLocalApply::eval(), sns::SNotCond::eval(), sns::And::eval(), sns::Add::eval(), sns::RecFireSat::eval(), sns::Fixpoint::eval(), _GShom::eval_skip(), sns::LocalApply::has_image(), sns::SLocalApply::has_image(), sns::And::has_image(), sns::Fixpoint::has_image(), StrongShom::has_image(), _GShom::has_image_skip(), iterateSDD(), MySDDNbStates::nbStates(), StrongShom::phiOne(), GSDD::print(), and dotExporter::printLevels().

---

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

• SDD.h
• SDD.cpp