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

#include <DDD.h>

Inheritance diagram for DDD:

Collaboration diagram for DDD:

Public Types
typedef unsigned int	id_t

Public Member Functions
	DDD (const DDD &)
	Copy constructor. More...

	DDD (const GDDD &g=GDDD::null)
	Copy constructor from base class GDDD, also default DDD constructor to empty set. More...

	DDD (int var, val_t val, const GDDD &d=one)
	The most common way for the user of creating DDD. More...

	DDD (int var, val_t val1, val_t val2, const GDDD &d=one)
	To create a DDD with arcs covering a range of values. More...

	~DDD ()
	Destructor, maintains refCount. More...

Assignment operators.
DDD &	operator= (const GDDD &)
	Overloaded behavior for assignment operator, maintains reference counting. More...

DDD &	operator= (const DDD &)
	Overloaded behavior for assignment operator, maintains reference counting. More...

DataSet implementation interface
This is the implementation of the DataSet class interface used in SDD context. These functions allow to reference DDD 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 DDD from proper behavior.
DataSet *	newcopy () const
	Return a new copy of a DDD. More...

DataSet *	set_intersect (const DataSet &b) const
	Compute intersection of two DDD. More...

DataSet *	set_union (const DataSet &b) const
	Compute union of two DDD. More...

DataSet *	set_minus (const DataSet &b) const
	Compute set difference of two DDD. More...

bool	empty () const
	Return true if this is the empty set. More...

DataSet *	empty_set () const
	Returns a pointer to GDDD::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 DDD. More...

void	set_print (std::ostream &os) const
	Textual (human readable) output of a DDD. More...

void	mark () const
	mark() from DataSet interface More...

Comparisons for hash and map storage
bool	operator== (const GDDD &g) const
	Comparison between DDD. More...

bool	operator!= (const GDDD &g) const
	Comparison between DDD. More...

bool	operator< (const GDDD &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 DDD structure. More...

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...

long double	noSharedSize () const
	Returns the number of nodes that would be used to represent a DDD if no unicity table was used. More...

Static Public Member Functions
Variable naming.
static void	varName (int var, const std::string &name)
	Sets a variable's name. More...

static const std::string	getvarName (int var)
	Gets a variable's name. More...

Static Public Attributes
Terminal nodes defined as constants
static const GDDD	one
	The accepting terminal. This is the basic leaf for accepted sequences. More...

static const GDDD	null
	The non-accepting terminal. More...

static const GDDD	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...

void	saveNode (std::ostream &, std::vector< id_t > &) const
	A function for DDD serialization (beta). More...

unsigned long int	nodeIndex (const std::vector< id_t > &) const
	Another function used in serialization. More...

Private Attributes
id_t	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 short	val_t
	The type used as values of variables in a DDD. More...

typedef unsigned short	valsz_t
	A type wide enough to count how many outgoing edges a DDD node has, should be congruent to val_t. More...

typedef std::pair< val_t, GDDD >	edge_t
	An edge is a pair <value,child node> More...

typedef std::vector< edge_t >	Valuation
	To hide how arcs are actually stored. Use GDDD::Valuation to refer to arcs type. More...

typedef const edge_t *	const_iterator
	To hide how arcs are stored. More...

Memory Management
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 DDD, not GDDD. Reference counting is enabled for DDD, so they will not be destroyed if they are still in use upon garbage collection.

Member Typedef Documentation

◆ const_iterator

typedef const edge_t* GDDD::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

◆ edge_t

typedef std::pair<val_t,GDDD> GDDD::edge_t

inherited

An edge is a pair <value,child node>

◆ id_t

typedef unsigned int GDDD::id_t

inherited

◆ val_t

typedef short GDDD::val_t

inherited

The type used as values of variables in a DDD.

◆ valsz_t

typedef unsigned short GDDD::valsz_t

inherited

A type wide enough to count how many outgoing edges a DDD node has, should be congruent to val_t.

◆ Valuation

typedef std::vector<edge_t > GDDD::Valuation

inherited

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

Constructor & Destructor Documentation

◆ DDD() [1/4]

DDD::DDD ( const DDD & g )

Copy constructor.

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

References GDDD::concret, UniqueTableId< T, ID >::instance(), and UniqueTableId< T, ID >::ref().

◆ DDD() [2/4]

DDD::DDD ( const GDDD & g = GDDD::null )

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

Increments refCounter of g.concret.

References GDDD::concret, UniqueTableId< T, ID >::instance(), and UniqueTableId< T, ID >::ref().

◆ DDD() [3/4]

DDD::DDD	(	int	var,
		val_t	val,
		const GDDD &	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 DDD(var1, val1, DDD( var2, val2 )). Then compose them using +, -, *, ^ ... See also GDDD(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 GDDD::concret, UniqueTableId< T, ID >::instance(), and UniqueTableId< T, ID >::ref().

◆ DDD() [4/4]

DDD::DDD	(	int	var,
		val_t	val1,
		val_t	val2,
		const GDDD &	d = `one`
	)

To create a DDD with arcs covering a range of values.

This interface creates nodes with a set of arcs bearing the values in the interval [val1,var2] that point to the same successor node d.

Parameters

var	the variable labeling the node
val1	lowest value labeling an arc
val2	highest value labeling an arc
d	the successor node or defaults to terminal GDDD::one if none provided

References GDDD::concret, UniqueTableId< T, ID >::instance(), and UniqueTableId< T, ID >::ref().

◆ ~DDD()

DDD::~DDD ( )

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 GDDD::concret, UniqueTableId< T, ID >::deref(), and UniqueTableId< T, ID >::instance().

Member Function Documentation

◆ begin()

GDDD::const_iterator GDDD::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 _GDDD::begin(), GDDD::concret, and _GDDD::resolve().

Referenced by DED::add(), dotExporter::collect(), _DED_Mult::eval(), _DED_Minus::eval(), _DED_Concat::eval(), StrongHom::eval(), StrongMLHom::eval(), Apply2k::eval(), DomExtract::eval(), _GHom::eval_skip(), StrongHom::has_image(), _GHom::has_image_skip(), _setVarConst::invert(), _incVar::invert(), MySize::mysize(), MyNbStates::nbStates(), GDDD::print(), GDDD::saveNode(), and SddSize::sddsize().

◆ empty()

bool DDD::empty ( ) const

virtual

Return true if this is the empty set.

Implements DataSet.

References GDDD::null, and GDDD::operator==().

◆ empty_set()

DataSet * DDD::empty_set ( ) const

virtual

Returns a pointer to GDDD::null.

Implements DataSet.

References GDDD::DDD.

◆ end()

GDDD::const_iterator GDDD::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 GDDD::concret, _GDDD::end(), and _GDDD::resolve().

Referenced by dotExporter::collect(), _DED_Mult::eval(), _DED_Minus::eval(), _DED_Concat::eval(), StrongHom::eval(), StrongMLHom::eval(), Apply2k::eval(), DomExtract::eval(), _GHom::eval_skip(), StrongHom::has_image(), _GHom::has_image_skip(), _setVarConst::invert(), MySize::mysize(), MyNbStates::nbStates(), GDDD::print(), GDDD::saveNode(), and SddSize::sddsize().

◆ garbage()

void GDDD::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 MyNbStates::clear(), UniqueTableId< T, ID >::garbage(), UniqueTableId< T, ID >::instance(), GDDD::mark(), GDDD::one, and GDDD::top.

Referenced by MemoryManager::garbage().

◆ getvarName()

const std::string GDDD::getvarName ( int var )

staticinherited

Gets a variable's name.

Todo:: This function should be implemented in a name manager somewhere so that it is common to DDD and SDD variables.

Parameters

var	the index of the variable to be named

Returns: the name attached to this variable index

References mapVarName.

Referenced by dotExporter::collect(), _VarCompState::print(), _setVarConst::print(), _incVar::print(), _VarCompVar::print(), and GDDD::print().

◆ hash()

size_t GDDD::hash ( ) const

inlineinherited

For storage in a hash table.

References GDDD::concret, and ddd::int32_hash().

Referenced by _DED_Mult::create(), _DED_Mult::hash(), _DED_Minus::hash(), _DED_Concat::hash(), _DED_Hom::hash(), Constant::hash(), Apply2k::hash(), Mult::hash(), LeftConcat::hash(), RightConcat::hash(), Minus::hash(), nsMLHom::LeftConcat::hash(), and set_hash().

◆ mark()

void DDD::mark ( ) const

inlinevirtual

mark() from DataSet interface

Implements DataSet.

References GDDD::mark().

◆ nbsons()

size_t GDDD::nbsons ( ) const

inherited

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

References GDDD::concret, _GDDD::resolve(), and _GDDD::valuation_size.

Referenced by _DED_Mult::eval(), _DED_Minus::eval(), and _incVar::invert().

◆ nbStates()

long double GDDD::nbStates ( ) const

inherited

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

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

◆ newcopy()

DataSet* DDD::newcopy ( ) const

inlinevirtual

Return a new copy of a DDD.

Implements DataSet.

References GDDD::DDD.

◆ nodeIndex()

unsigned long int GDDD::nodeIndex ( const std::vector< id_t > & ) const

privateinherited

Another function used in serialization.

References GDDD::concret.

Referenced by GDDD::saveNode().

◆ noSharedSize()

long double GDDD::noSharedSize ( ) const

inherited

Returns the number of nodes that would be used to represent a DDD if no unicity table was used.

◆ operator!=()

bool GDDD::operator!= ( const GDDD & 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 GDDD::concret.

◆ operator<()

bool GDDD::operator< ( const GDDD & 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 GDDD::concret.

◆ operator=() [1/2]

DDD & DDD::operator= ( const DDD & g )

Overloaded behavior for assignment operator, maintains reference counting.

References GDDD::concret, UniqueTableId< T, ID >::deref(), UniqueTableId< T, ID >::instance(), and UniqueTableId< T, ID >::ref().

◆ operator=() [2/2]

DDD & DDD::operator= ( const GDDD & g )

Overloaded behavior for assignment operator, maintains reference counting.

References GDDD::concret, UniqueTableId< T, ID >::deref(), UniqueTableId< T, ID >::instance(), and UniqueTableId< T, ID >::ref().

◆ operator==()

bool GDDD::operator== ( const GDDD & 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.

Referenced by empty().

◆ peak()

size_t GDDD::peak ( )

staticinherited

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

References UniqueTableId< T, ID >::instance(), and UniqueTableId< T, ID >::peak_size().

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

◆ print()

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

privateinherited

Internal function used in recursion for textual printing of GDDD.

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

◆ pstats()

void GDDD::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 UniqueTableId< T, ID >::instance(), and GDDD::peak().

Referenced by MemoryManager::pstats().

◆ refCounter()

unsigned int GDDD::refCounter ( ) const

inherited

Returns current reference count of a node.

Reference count corresponds to the number of DDD 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.

◆ saveNode()

void GDDD::saveNode	(	std::ostream &	,
		std::vector< id_t > &
	)		const

privateinherited

A function for DDD serialization (beta).

References GDDD::begin(), GDDD::concret, GDDD::end(), GDDD::nodeIndex(), GDDD::one, and GDDD::top.

◆ set_equal()

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

virtual

Compares to DataSet for equality.

Implements DataSet.

◆ set_hash()

size_t DDD::set_hash ( ) const

virtual

Returns a hash key for the DDD.

Implements DataSet.

References GDDD::hash().

◆ set_intersect()

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

virtual

Compute intersection of two DDD.

Implements DataSet.

References GDDD::DDD.

◆ set_less_than()

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

virtual

Compares two sets with a total order.

Implements DataSet.

◆ set_minus()

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

virtual

Compute set difference of two DDD.

Implements DataSet.

References GDDD::DDD.

◆ set_print()

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

inlinevirtual

Textual (human readable) output of a DDD.

Implements DataSet.

◆ set_size()

long double DDD::set_size ( ) const

virtual

Compares to DataSet for equality.

Implements DataSet.

References GDDD::nbStates().

◆ set_union()

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

virtual

Compute union of two DDD.

Implements DataSet.

References GDDD::DDD.

◆ size()

unsigned long int GDDD::size ( ) const

inherited

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

Referenced by Statistic::load().

◆ statistics()

unsigned int GDDD::statistics ( )

staticinherited

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

References UniqueTableId< T, ID >::instance(), and UniqueTableId< T, ID >::size().

Referenced by MemoryManager::nbDDD().

◆ variable()

int GDDD::variable ( ) const

inherited

Returns a node's variable.

References GDDD::concret, _GDDD::resolve(), and _GDDD::variable.

Referenced by dotExporter::collect(), _DED_Mult::create(), _DED_Minus::create(), _DED_Mult::eval(), _DED_Minus::eval(), _DED_Concat::eval(), StrongHom::eval(), StrongMLHom::eval(), Apply2k::eval(), DomExtract::eval(), Add::eval(), Monotonic::eval(), And::eval(), Fixpoint::eval(), _GHom::eval_skip(), GDDD::GDDD(), StrongHom::has_image(), Add::has_image(), Fixpoint::has_image(), _GHom::has_image_skip(), and GDDD::print().

◆ varName()

void GDDD::varName	(	int	var,
		const std::string &	name
	)

staticinherited

Sets a variable's name.

Todo:: This function should be implemented in a name manager somewhere so that it is common to DDD and SDD variables.

Parameters

var	the index of the variable to be named
name	the name to attach to this variable index

References mapVarName.

Member Data Documentation

◆ concret

id_t GDDD::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 GDDD::begin(), DDD(), GDDD::end(), GDDD::GDDD(), GDDD::hash(), GDDD::mark(), GDDD::nbsons(), GDDD::nodeIndex(), GDDD::operator!=(), GDDD::operator<(), operator=(), GDDD::saveNode(), GDDD::variable(), and ~DDD().

◆ null

const GDDD GDDD::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 GHom::add(), DED::add(), apply2k(), dotExporter::collect(), _VarCompState::compose(), _VarCompVar::compose(), _GHom::compose(), _DED_Mult::create(), _DED_Minus::create(), _DED_Concat::create(), _DED_Hom::create(), _DED_Add::create(), empty(), _DED_Mult::eval(), _DED_Minus::eval(), StrongHom::eval(), StrongMLHom::eval(), Constant::eval(), Apply2k::eval(), DomExtract::eval(), NotCond::eval(), Add::eval(), Monotonic::eval(), And::eval(), Fixpoint::eval(), sns::SApply2k::eval(), sns::LocalApply::eval(), sns::RecFireSat::eval(), _GHom::eval_skip(), StrongHom::has_image(), Inter::has_image(), NotCond::has_image(), Add::has_image(), And::has_image(), Fixpoint::has_image(), GHom::has_image(), sns::LocalApply::has_image(), _GHom::has_image_skip(), _GHom::invert(), Compose::invert(), Constant::is_selector(), iterateDDD(), MyNbStates::nbStates(), Identity::negate(), Constant::negate(), GHom::operator()(), operator*(), _VarCompState::phi(), varGtVar(), varLtVar(), and varNeqVar().

◆ one

const GDDD GDDD::one

staticinherited

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

Referenced by apply2k(), dotExporter::collect(), _DED_Mult::create(), _DED_Minus::create(), _DED_Concat::create(), _DED_Add::create(), StrongHom::eval(), StrongMLHom::eval(), DomExtract::eval(), NotCond::eval(), Add::eval(), Monotonic::eval(), And::eval(), Fixpoint::eval(), _GHom::eval_skip(), GDDD::garbage(), StrongHom::has_image(), Add::has_image(), Fixpoint::has_image(), _GHom::has_image_skip(), iterateDDD(), MyNbStates::nbStates(), _VarCompState::phiOne(), _setVarConst::phiOne(), _incVar::phiOne(), _VarCompVar::phiOne(), GDDD::print(), and GDDD::saveNode().

◆ top

const GDDD GDDD::top

staticinherited

The approximation terminal.

This represents any finite set of assignment sequences. In a "normal" usage pattern, top terminals should not be produced.

Referenced by apply2k(), dotExporter::collect(), _DED_Mult::create(), _DED_Minus::create(), _DED_Concat::create(), _DED_Add::create(), StrongHom::eval(), StrongMLHom::eval(), DomExtract::eval(), NotCond::eval(), Add::eval(), Monotonic::eval(), And::eval(), Fixpoint::eval(), _GHom::eval_skip(), GDDD::garbage(), StrongHom::has_image(), Add::has_image(), Fixpoint::has_image(), _GHom::has_image_skip(), iterateDDD(), MyNbStates::nbStates(), StrongHom::phiOne(), GDDD::print(), and GDDD::saveNode().

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

Public Types

Public Member Functions

Static Public Member Functions

Static Public Attributes

Private Member Functions

Private Attributes

Public Accessors

Memory Management

Detailed Description

Member Typedef Documentation

◆ const_iterator

◆ edge_t

◆ id_t

◆ val_t

◆ valsz_t

◆ Valuation

Constructor & Destructor Documentation

◆ DDD() [1/4]

◆ DDD() [2/4]

◆ DDD() [3/4]

◆ DDD() [4/4]

◆ ~DDD()

Member Function Documentation

◆ begin()

◆ empty()

◆ empty_set()

◆ end()

◆ garbage()

◆ getvarName()

◆ hash()

◆ mark()

◆ nbsons()

◆ nbStates()

◆ newcopy()

◆ nodeIndex()

◆ noSharedSize()

◆ operator!=()

◆ operator<()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator==()

◆ peak()

◆ print()

◆ pstats()

◆ refCounter()

◆ saveNode()

◆ set_equal()

◆ set_hash()

◆ set_intersect()

◆ set_less_than()

◆ set_minus()

◆ set_print()

◆ set_size()

◆ set_union()

◆ size()

◆ statistics()

◆ variable()

◆ varName()

Member Data Documentation

◆ concret

◆ null

◆ one

◆ top