This class is the base class representing a Data Decision Diagram. More...

#include <DDD.h>

Inheritance diagram for GDDD:

Collaboration diagram for GDDD:

Public Types
typedef unsigned int	id_t

Public Member Functions
Public Constructors
	GDDD (int variable, const Valuation &value)
	Construct a GDDD with arguments given.

	GDDD ()
	Default constructor creates the empty set DDD.

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

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

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

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

bool	operator< (const GDDD &g) const
	Total ordering function between DDD.

unsigned int	refCounter () const
	Returns current reference count of a node.

unsigned long int	size () const
	Returns the size in number of nodes of a DDD structure.

size_t	nbsons () const
	Returns the number of successors of a given node. This is the size of the arc array of the node.

long double	nbStates () const
	Returns the number of states or paths represented by a given node.

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

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

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

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

static const GDDD	null
	The non-accepting terminal.

static const GDDD	top
	The approximation terminal.

Private Member Functions
	GDDD (const id_t &_g)
	A private constructor used in internals.

	GDDD (_GDDD *_g)
	UNIMPLEMENTED DELIBERATELY: see SHom.h for details.

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

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

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

Private Attributes
id_t	concret
	The real implementation class.

Friends
class	DDD
	Open access to concret for reference counting in DDD.

std::ostream &	operator<< (std::ostream &os, const GDDD &g)
	A textual output.

Serialization functions.
void	saveDDD (std::ostream &, std::vector< DDD >)
	Function for serialization. Save a set of DDD to a stream.

void	loadDDD (std::istream &, std::vector< DDD > &)
	Function for deserialization. Load a set of DDD from a stream.

Public Accessors
typedef short	val_t
	The type used as values of variables in a DDD.

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.

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

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

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

int	variable () const
	Returns a node's variable.

const_iterator	begin () const
	API for iterating over the arcs of a DDD manually.

const_iterator	end () const
	API for iterating over the arcs of a DDD manually.

Memory Management
void	mark () const
	For garbage collection internals.

size_t	hash () const
	For storage in a hash table.

static unsigned int	statistics ()
	Returns unicity table current size. Gives the number of different nodes created and not yet destroyed.

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

static void	pstats (bool reinit=true)
	Prints some statistics to std::cout.

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

Detailed Description

This class is the base class representing a Data Decision Diagram.

It is composed of a set of arcs labeled by integers that point to successor GDDD nodes. This class does not implement reference counting : GDDD are destroyed on MemoryManager::Garbage unless they are also referenced as DDD. Note that this class is in fact a kind of smart pointer : operations are delegated on "concret" the true implementation class (of private hidden type _GDDD) that contains the data and has a single memory occurrence thanks to the unicity table.

Member Typedef Documentation

◆ const_iterator

typedef const edge_t* GDDD::const_iterator

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

An edge is a pair <value,child node>

◆ id_t

typedef unsigned int GDDD::id_t

◆ val_t

typedef short GDDD::val_t

The type used as values of variables in a DDD.

◆ valsz_t

typedef unsigned short GDDD::valsz_t

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

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

Constructor & Destructor Documentation

◆ GDDD() [1/6]

GDDD::GDDD ( const id_t & _g )

private

A private constructor used in internals.

Parameters

_g	The pointer provided should point into the unicity table

◆ GDDD() [2/6]

GDDD::GDDD ( _GDDD * _g )

private

UNIMPLEMENTED DELIBERATELY: see SHom.h for details.

user should use version above const & or below const * into unique storage.

◆ GDDD() [3/6]

GDDD::GDDD	(	int	variable,
		const Valuation &	value
	)

Construct a GDDD with arguments given.

Todo:: why is this public ??? WARNING Valuation should be sorted according to arc values

Parameters

variable	the variable labeling the node
value	the set of arcs of the node

References concret, _GDDD::create_unique_GDDD(), GDDD(), null, and variable().

◆ GDDD() [4/6]

GDDD::GDDD ( )

inline

Default constructor creates the empty set DDD.

Referenced by GDDD().

◆ GDDD() [5/6]

GDDD::GDDD	(	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 GDDD(var1, val1, GDDD( var2, val2 )). Then compose them using +, -, *, ^ ...

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 concret, _GDDD::create_unique_GDDD(), and null.

◆ GDDD() [6/6]

GDDD::GDDD	(	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 concret, _GDDD::create_unique_GDDD(), and null.

Member Function Documentation

◆ begin()

GDDD::const_iterator GDDD::begin ( ) const

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

Referenced by DED::add(), dotExporter::collect(), dotExporter::collect(), _DED_Add::create(), _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(), print(), saveNode(), and SddSize::sddsize().

◆ end()

GDDD::const_iterator GDDD::end ( ) const

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

Referenced by dotExporter::collect(), 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(), print(), saveNode(), and SddSize::sddsize().

◆ garbage()

void GDDD::garbage ( )

static

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(), mark(), null, one, and top.

Referenced by MemoryManager::garbage().

◆ getvarName()

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

static

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 print().

◆ hash()

size_t GDDD::hash ( ) const

inline

For storage in a hash table.

References 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 DDD::set_hash().

◆ mark()

void GDDD::mark ( ) const

For garbage collection internals.

Marks a GDDD as in use in garbage collection phase.

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

Referenced by Fixpoint::eval(), garbage(), DDD::mark(), Constant::mark(), Apply2k::mark(), Mult::mark(), LeftConcat::mark(), RightConcat::mark(), Minus::mark(), and MemoryManager::mark().

◆ nbsons()

size_t GDDD::nbsons ( ) const

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

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

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

◆ nbStates()

long double GDDD::nbStates ( ) const

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

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

◆ nodeIndex()

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

private

Another function used in serialization.

References concret.

Referenced by saveNode().

◆ noSharedSize()

long double GDDD::noSharedSize ( ) const

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

inline

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

◆ operator<()

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

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

◆ operator==()

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

inline

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.

References concret.

Referenced by DDD::empty().

◆ peak()

size_t GDDD::peak ( )

static

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(), Statistic::load(), and pstats().

◆ print()

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

private

Internal function used in recursion for textual printing of GDDD.

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

◆ pstats()

void GDDD::pstats ( bool reinit = true )

static

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 peak().

Referenced by MemoryManager::pstats().

◆ refCounter()

unsigned int GDDD::refCounter ( ) const

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

private

A function for DDD serialization (beta).

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

◆ size()

unsigned long int GDDD::size ( ) const

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

Referenced by Statistic::load().

◆ statistics()

unsigned int GDDD::statistics ( )

static

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

Returns a node's variable.

References 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(), StrongHom::has_image(), Add::has_image(), Fixpoint::has_image(), _GHom::has_image_skip(), and print().

◆ varName()

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

static

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.

Friends And Related Symbol Documentation

◆ DDD

friend class DDD

friend

Open access to concret for reference counting in DDD.

Referenced by DDD::empty_set(), DDD::newcopy(), DDD::set_intersect(), DDD::set_minus(), and DDD::set_union().

◆ loadDDD

void loadDDD	(	std::istream &	is,
		std::vector< DDD > &	list
	)

friend

Function for deserialization. Load a set of DDD from a stream.

◆ operator<<

std::ostream & operator<<	(	std::ostream &	os,
		const GDDD &	g
	)

friend

A textual output.

Don't use it with large number of paths as each element is printed on a different line

◆ saveDDD

void saveDDD	(	std::ostream &	os,
		std::vector< DDD >	list
	)

friend

Function for serialization. Save a set of DDD to a stream.

Member Data Documentation

◆ concret

id_t GDDD::concret

private

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

◆ null

const GDDD GDDD::null

static

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(), DDD::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(), garbage(), GDDD(), GDDD(), GDDD(), 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(), print(), saveNode(), varGtVar(), varLtVar(), and varNeqVar().

◆ one

const GDDD GDDD::one

static

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

Referenced by apply2k(), dotExporter::collect(), 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(), 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(), print(), and saveNode().

◆ top

const GDDD GDDD::top

static

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(), garbage(), StrongHom::has_image(), Add::has_image(), Fixpoint::has_image(), _GHom::has_image_skip(), iterateDDD(), MyNbStates::nbStates(), StrongHom::phiOne(), print(), and 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

Friends

Public Accessors

Memory Management

Detailed Description

Member Typedef Documentation

◆ const_iterator

◆ edge_t

◆ id_t

◆ val_t

◆ valsz_t

◆ Valuation

Constructor & Destructor Documentation

◆ GDDD() [1/6]

◆ GDDD() [2/6]

◆ GDDD() [3/6]

◆ GDDD() [4/6]

◆ GDDD() [5/6]

◆ GDDD() [6/6]

Member Function Documentation

◆ begin()

◆ end()

◆ garbage()

◆ getvarName()

◆ hash()

◆ mark()

◆ nbsons()

◆ nbStates()

◆ nodeIndex()

◆ noSharedSize()

◆ operator!=()

◆ operator<()

◆ operator==()

◆ peak()

◆ print()

◆ pstats()

◆ refCounter()

◆ saveNode()

◆ size()

◆ statistics()

◆ variable()

◆ varName()

Friends And Related Symbol Documentation

◆ DDD

◆ loadDDD

◆ operator<<

◆ saveDDD

Member Data Documentation

◆ concret

◆ null

◆ one

◆ top