This class is the base class representing a homomorphism over DDD. More...

#include <Hom.h>

Inheritance diagram for GHom:

Collaboration diagram for GHom:

Public Types
typedef GDDD	NodeType

Public Member Functions
	GHom (const _GHom *_h)
	A uncontrolled constructor used in internals. More...

	GHom (_GHom *_h)
	THIS VERSION IS DELIBERATELY UNIMPLEMENTED OTHERWISE bad calls like GShom(new myHom()) would promote to const _GShom *_h and bypass unicity. More...

	GHom (const _GHom &_h)
	build a GHom from user provided homomorphisms such as StrongHom. More...

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

Friends
class	Hom
	Open access to Hom derived class. More...

class	_GHom
	Open access to _GHom based homomophisms. More...

GHom	fixpoint (const GHom &, bool)
	This operator applies its argument to a node until a fixpoint is reached. More...

GHom	monotonic (const d3::set< GHom >::type &set)
	This operator applies its arguments to a node until a fixpoint is reached. More...

GHom	operator+ (const GHom &, const GHom &)
	This operator creates an operation that is the union of two operations. More...

GHom	operator& (const GHom &, const GHom &)
	This operator creates an operation that is the composition of two operations. More...

GHom	operator* (const GDDD &, const GHom &)
	This operator creates an operation that is the intersection of an operation and a constant DDD. More...

GHom	operator* (const GHom &, const GDDD &)
	This operator creates an operation that is the intersection of an operation and a constant DDD. More...

GHom	operator^ (const GDDD &, const GHom &)
	This is the left concatenantion operator, that adds a constant DDD above the operation. More...

GHom	operator^ (const GHom &, const GDDD &)
	This is the right concatenantion operator, that adds a constant DDD below the operation. More...

GHom	operator- (const GHom &, const GDDD &)
	This is a set difference constructor, only available for (hom - ddd), not hom - hom as that might not preserve linearity. More...

Comparisons for hash and map storage
typedef d3::set< int >::type	range_t

typedef range_t::const_iterator	range_it

std::ostream &	operator<< (std::ostream &os, const GHom &h)

static const range_t	full_range = GHom::range_t()
	The full_range : that targets everyone. More...

bool	operator== (const GHom &h) const
	Comparison between Homomorphisms. More...

bool	operator!= (const GHom &h) const
	Comparison between Homomorphisms. More...

bool	operator< (const GHom &h) const
	Total ordering function between Hom. More...

bool	is_selector () const
	This predicate is true if the homomorphism global behavior is only to prune some paths. More...

const range_t	get_range () const
	Returns the range for this homomorphism, i.e. the dual of skip_variable. More...

GHom	invert (const GDDD &pot) const
	returns the predescessor homomorphism, using pot to determine variable domains More...

GDDD	has_image (const GDDD &d) const
	returns true if and only if h(d) != SDD::null More...

GHom	negate () const
	returns a negation of a selector homomorphism h, such that h.negate() (d) = d - h(d) More...

GDDD	operator() (const GDDD &d) const
	Evaluation operator. More...

GDDD	eval (const GDDD &d) const
	Evaluation function : users should use operator() instead of this. More...

bool	skip_variable (int var) const

GHom	compose (const GHom &r) const

int	refCounter () const
	Accessor to visualize the reference count of the concret instance. More...

static GHom	add (const d3::set< GHom >::type &set)
	A constructor for a union of several homomorphisms. More...

static GHom	ccompose (const d3::set< GHom >::type &set)
	A constructor for a commutative composition of several homomorphisms. More...

Public Constructors
static const GHom	id
	Elementary homomorphism Identity, defined as a constant. More...

	GHom ()
	Default public constructor. More...

	GHom (const MLHom &)
	Encapsulate an MLHom, by setting a stop level for the upstream homomorphisms. More...

	GHom (const GDDD &d)
	Create a constant DDD homomorphism. More...

	GHom (int var, int val, const GHom &h=GHom::id)
	Create variable/value pair and left concatenate to a homomorphism. More...

Memory Management
void	mark () const
	For garbage collection internals. Marks a GHom as in use in garbage collection phase. 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 _GHom created and not yet destroyed. More...

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

static void	garbage ()
	For garbage collection. More...

Detailed Description

This class is the base class representing a homomorphism over DDD.

A DDD homomorphism is a linear application that respects the better-defined relation (see ICATPN'2002 paper by Couvreur et al.). It comes with composition &, union +, and intersection * operators to construct complex operations from two homomorphisms. It also comes with the fixpoint() unary operator, that allows to implement saturation (see FORTE'05 paper by Couvreur & Thierry-Mieg) This class does not implement reference counting : GHom are destroyed on MemoryManager::Garbage unless they are also referenced as Hom. 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 _GHom) that contains the data and has a single memory occurrence thanks to the unicity table.

Member Typedef Documentation

◆ NodeType

typedef GDDD GHom::NodeType

◆ range_it

typedef range_t::const_iterator GHom::range_it

◆ range_t

typedef d3::set<int>::type GHom::range_t

Constructor & Destructor Documentation

◆ GHom() [1/7]

GHom::GHom ( const _GHom * _h )

inline

A uncontrolled constructor used in internals.

Made public for calls like return GHom(this) in StrongHom::phi definitions.

Parameters

_h	The pointer provided should point into the unicity table

◆ GHom() [2/7]

GHom::GHom ( _GHom * _h )

THIS VERSION IS DELIBERATELY UNIMPLEMENTED OTHERWISE bad calls like GShom(new myHom()) would promote to const _GShom *_h and bypass unicity.

User code prior to 20/05/08 would use this in the form : return new myHom(xx); This is now illegal as we take up memory allocation now, so the user should stack alloc and pass a reference as in GShom(const _GShom &_h). Exceptionally, for efficiency, return this; in a phi user function is permitted hence public visibility of above GShom(const _GShom *_h); This signature is here to ensure link errors in old user code.

◆ GHom() [3/7]

GHom::GHom ( const _GHom & _h )

build a GHom from user provided homomorphisms such as StrongHom.

This call ensures canonization of h

◆ GHom() [4/7]

GHom::GHom ( )

inline

Default public constructor.

Builds Identity homomorphism : forall d in DDD, id(d) = d

Referenced by add().

◆ GHom() [5/7]

GHom::GHom ( const MLHom & h )

Encapsulate an MLHom, by setting a stop level for the upstream homomorphisms.

◆ GHom() [6/7]

GHom::GHom ( const GDDD & d )

Create a constant DDD homomorphism.

These are the basic building bricks of more complex operations. h(d1) (d2) = d1 Where d1 is a DDD, h(d1) a constant homomorphism and d2 an arbitrary DDD.

◆ GHom() [7/7]

GHom::GHom	(	int	var,
		int	val,
		const GHom &	h = `GHom::id`
	)

Create variable/value pair and left concatenate to a homomorphism.

h(var,val,g) (d) = DDD(var,val) ^ g(d). In other words : var – val -> g

Parameters

var	the variable index
val	the value associated to the variable
h	the homomorphism to apply on successor node. Default is identity, so is equivalent to a left concatenation of a DDD(var,val).

Member Function Documentation

◆ add()

GHom GHom::add ( const d3::set< GHom >::type & set )

static

A constructor for a union of several homomorphisms.

Note that for canonisation and optimization reasons, union is an n-ary and commutative composition operator. Use of this constructor may be slightly more efficient than using operator+ multiple times. H({h1,h2, ..hn}) (d) = sum_i h_i (d).

Parameters

set	the set of homomorphisms to put in the union.

Todo:: std::set not very efficient for storage, replace by a sorted vector ?

References canonical, GHom(), and GDDD::null.

Referenced by Add::invert(), _setVarConst::invert(), And::negate(), and Add::skip_variable().

◆ ccompose()

GHom GHom::ccompose ( const d3::set< GHom >::type & set )

static

A constructor for a commutative composition of several homomorphisms.

It's up to user to ensure pairwise commutatitivity off all arguments in the set

Parameters

set	the set of homomorphisms to put in the composition.

Todo:: std::set not very efficient for storage, replace by a sorted vector ?

References canonical, and id.

Referenced by Add::negate().

◆ compose()

GHom GHom::compose ( const GHom & r ) const

References _GHom::compose(), and concret.

Referenced by nsMLHom::ConstantUp::eval().

◆ eval()

GDDD GHom::eval ( const GDDD & d ) const

Evaluation function : users should use operator() instead of this.

This evaluation function does not use the cache, it is called in case of cache miss in the call to operator().

Parameters

d	the argument DDD

Returns: h(d)

References concret, and _GHom::eval_skip().

Referenced by _DED_Hom::eval().

◆ garbage()

void GHom::garbage ( )

static

For garbage collection.

WARNING Do not use this function directly !! Use MemoryManager::garbage() to ensure proper reference counting and cache cleanup. Garbage collection algorithm is a simple two phase mark and sweep : in phase mark, all nodes with positive reference counts are marked, as well as their descendants, recursively. In phase sweep, all nodes which are unmarked are destroyed. This avoids maintaining reference counts during operation : only external references made through the DDD class are counted, and no recursive reference counting is needed.

References cache, canonical, Cache< FuncType, ParamType, ResType, EvalFunc >::clear(), imgcache, and _GHom::marking.

Referenced by MemoryManager::garbage().

◆ get_range()

const GHom::range_t GHom::get_range ( ) const

Returns the range for this homomorphism, i.e. the dual of skip_variable.

References concret, and _GHom::get_range().

Referenced by commutative(), NotCond::get_range(), Compose::get_range(), Fixpoint::get_range(), and notInRange().

◆ has_image()

GDDD GHom::has_image ( const GDDD & d ) const

returns true if and only if h(d) != SDD::null

References imgcache, Cache< FuncType, ParamType, ResType, EvalFunc >::insert(), and GDDD::null.

Referenced by Inter::has_image(), NotCond::has_image(), Add::has_image(), LeftConcat::has_image(), RightConcat::has_image(), Fixpoint::has_image(), sns::LocalApply::has_image(), and _GHom::has_image_skip().

◆ hash()

size_t GHom::hash ( ) const

inline

For storage in a hash table.

References concret, and ddd::knuth32_hash().

Referenced by _DED_Hom::hash(), Mult::hash(), Inter::hash(), NotCond::hash(), Compose::hash(), LeftConcat::hash(), RightConcat::hash(), Minus::hash(), Fixpoint::hash(), nsMLHom::GHomAdapter::hash(), nsMLHom::ConstantUp::hash(), and sns::LocalApply::hash().

◆ invert()

GHom GHom::invert ( const GDDD & pot ) const

returns the predescessor homomorphism, using pot to determine variable domains

References concret, and _GHom::invert().

Referenced by Mult::invert(), Inter::invert(), Compose::invert(), Minus::invert(), Fixpoint::invert(), and sns::LocalApply::invert().

◆ is_selector()

bool GHom::is_selector ( ) const

This predicate is true if the homomorphism global behavior is only to prune some paths.

References concret, and _GHom::is_selector().

Referenced by commutative(), Mult::is_selector(), Inter::is_selector(), Compose::is_selector(), Minus::is_selector(), Fixpoint::is_selector(), sns::LocalApply::is_selector(), ITE(), and operator*().

◆ mark()

void GHom::mark ( ) const

For garbage collection internals. Marks a GHom as in use in garbage collection phase.

References concret, _GHom::mark(), and _GHom::marking.

Referenced by Fixpoint::eval(), Mult::mark(), Inter::mark(), NotCond::mark(), Compose::mark(), LeftConcat::mark(), RightConcat::mark(), Minus::mark(), Fixpoint::mark(), sns::LocalApply::mark(), and MemoryManager::mark().

◆ negate()

GHom GHom::negate ( ) const

returns a negation of a selector homomorphism h, such that h.negate() (d) = d - h(d)

References concret, and _GHom::negate().

Referenced by NotCond::has_image(), and Inter::negate().

◆ operator!=()

bool GHom::operator!= ( const GHom & h ) const

inline

Comparison between Homomorphisms.

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

Parameters

h	the hom to compare to

Returns: true if the nodes are NOT equal.

References concret.

◆ operator()()

GDDD GHom::operator() ( const GDDD & d ) const

Evaluation operator.

Homomorphisms overload operator(), so they can be directly applied to DDD nodes. Note that evaluation through this operator uses and updates a cache.

Parameters

d	the DDD to apply this h to.

Returns: h(d), the result of applying this h to d.

References cache, concret, _GHom::eval(), _GHom::immediat, Cache< FuncType, ParamType, ResType, EvalFunc >::insert(), and GDDD::null.

◆ operator<()

bool GHom::operator< ( const GHom & h ) const

Total ordering function between Hom.

Note that comparison is based on chronological ordering of creation, and delegated to "concret". Unlike comparison on addresses in unicity table, this ensures reproductible results. This ordering is necessary for hash and map storage of GHom.

Parameters

h	the node to compare to

Returns: true if argument h is greater than "this".

References concret.

◆ operator==()

bool GHom::operator== ( const GHom & h ) const

inline

Comparison between Homomorphisms.

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

Parameters

h	the hom to compare to

Returns: true if the nodes are equal.

◆ pstats()

void GHom::pstats ( bool reinit = true )

static

Prints some statistics to std::cout.

Mostly used in debug and development phase.

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

References _GHom, cache, and canonical.

Referenced by MemoryManager::pstats().

◆ refCounter()

int GHom::refCounter ( ) const

Accessor to visualize the reference count of the concret instance.

See _GHom::refCounter for details.

References concret, and _GHom::refCounter.

◆ skip_variable()

bool GHom::skip_variable ( int var ) const

References concret, and _GHom::skip_variable().

Referenced by nsMLHom::GHomAdapter::skip_variable().

◆ statistics()

unsigned int GHom::statistics ( )

static

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

References canonical.

Referenced by Statistic::load(), and MemoryManager::nbHom().

Friends And Related Function Documentation

◆ _GHom

friend class _GHom

friend

Open access to _GHom based homomophisms.

Referenced by pstats().

◆ fixpoint

GHom fixpoint	(	const GHom &	,
		bool
	)

friend

This operator applies its argument to a node until a fixpoint is reached.

Application consists in : while ( h(d) != d ) d = h(d); Where d is a DDD and h a homomorphism.

This new unary operator is introduced to implement local saturation in transition relation evaluation. Proper use of fixpoint allows to effectively tackle the intermediate size problem of decision diagram based representations. Note that evaluation simply iterates until a fixpoint is reached, thus to cumulate new states with previously reached it should be combined with GShom::id as in

fixpoint ( h + GShom::id )

◆ Hom

friend class Hom

friend

Open access to Hom derived class.

◆ monotonic

GHom monotonic ( const d3::set< GHom >::type & set )

friend

This operator applies its arguments to a node until a fixpoint is reached.

Similar to the fixpoint, but we suppose here that the parameters are commutative And that any application order converges to the same result Typically this is the property of a base of monotonic< permutations.

◆ operator&

GHom operator&	(	const GHom &	,
		const GHom &
	)

friend

This operator creates an operation that is the composition of two operations.

(h & g) (d) = h( g(d) ) ; Where g,h are homomorphisms and d is a DDD.

Semantics : (h1 & h2) (d) = h1( h2(d) ).

◆ operator* [1/2]

GHom operator*	(	const GDDD &	,
		const GHom &
	)

friend

This operator creates an operation that is the intersection of an operation and a constant DDD.

(d1 * h) (d2) = d1 * h(d2) ; Where h is a homomorphism and d1, d2 are DDD.

Semantics : (h * d1) (d) = h(d) * d1

◆ operator* [2/2]

GHom operator*	(	const GHom &	,
		const GDDD &
	)

friend

This operator creates an operation that is the intersection of an operation and a constant DDD.

(h * d1) (d2) = h(d2) * d1 ; Where h is a homomorphism and d1, d2 are DDD.

Semantics : (d1 * h) (d) = d1 * h(d)

◆ operator+

GHom operator+	(	const GHom &	,
		const GHom &
	)

friend

This operator creates an operation that is the union of two operations.

By definition, as homomorphism are linear, (h+g) (d) = h(d) + g(d) ; Where g,h are homomorphisms and d is a DDD.

See also GShom::add(). This commutative operation computes a homomorphism that evaluates as the sum of two homomorphism.

Semantics : (h1 + h2) (d) = h1(d) + h2(d).

◆ operator-

GHom operator-	(	const GHom &	,
		const GDDD &
	)

friend

This is a set difference constructor, only available for (hom - ddd), not hom - hom as that might not preserve linearity.

(h - d1) (d2) = h(d2) - d1 Where h is a homomorphism and d1, d2 are DDD.

Note that this operation is not commutative, nor is it linear. This means the difference of two linear homomorphisms is not necessarily linear; (h1 - h2) (d) is not necessarily equal to h1(d) - h2(d). Therefore this operator is not defined for composition of two homomorphisms, only for a constant and a homomorphism.

Semantics : (h - d1) (d) = h(d) - d1

◆ operator<<

std::ostream& operator<<	(	std::ostream &	os,
		const GHom &	h
	)

friend

◆ operator^ [1/2]

GHom operator^	(	const GDDD &	,
		const GHom &
	)

friend

This is the left concatenantion operator, that adds a constant DDD above the operation.

(d1 ^ h) (d2) = d1 ^ h(d2) Where h is a homomorphism and d1, d2 are DDD.

Note that this is inherently inefficient, the nodes of d1 are constructed, but the result a priori will not contain them, unless h(d) == GSDD::one.

Semantics : (d1 ^ h) (d) = d1 ^ h(d)

◆ operator^ [2/2]

GHom operator^	(	const GHom &	,
		const GDDD &
	)

friend

This is the right concatenantion operator, that adds a constant DDD below the operation.

(h ^ d1) (d2) = h(d1) ^ d2 Where h is a homomorphism and d1, d2 are DDD.

This is used to construct new nodes, and has the same efficiency issue as left concatenation.

Semantics : (h ^ d1) (d) = h(d) ^ d1

Member Data Documentation

◆ concret

const _GHom* GHom::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 compose(), eval(), _GHom::get_concret(), get_range(), hash(), Hom::Hom(), invert(), is_selector(), mark(), negate(), operator!=(), operator()(), operator<(), Hom::operator=(), refCounter(), skip_variable(), and Hom::~Hom().

◆ full_range

const GHom::range_t GHom::full_range = GHom::range_t()

static

The full_range : that targets everyone.

Referenced by _GHom::get_range().

◆ id

const GHom GHom::id

static

Elementary homomorphism Identity, defined as a constant.

id(d) = d

Referenced by buildUnionParameters(), ccompose(), _GHom::compose(), StrongMLHom::eval(), And::eval(), nsMLHom::Identity::eval(), nsMLHom::GHomAdapter::eval(), _GHom::eval_skip(), Add::get_have_id(), Fixpoint::has_image(), sns::Fixpoint::has_image(), _GHom::has_image_skip(), Mult::invert(), And::invert(), Minus::invert(), Fixpoint::invert(), Constant::negate(), operator*(), _VarCompState::phi(), _setVarConst::phi(), varEqVar(), varGeqVar(), and varLeqVar().

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

Public Types

Public Member Functions

Private Attributes

Friends

Comparisons for hash and map storage

Public Constructors

Memory Management

Detailed Description

Member Typedef Documentation

◆ NodeType

◆ range_it

◆ range_t

Constructor & Destructor Documentation

◆ GHom() [1/7]

◆ GHom() [2/7]

◆ GHom() [3/7]

◆ GHom() [4/7]

◆ GHom() [5/7]

◆ GHom() [6/7]

◆ GHom() [7/7]

Member Function Documentation

◆ add()

◆ ccompose()

◆ compose()

◆ eval()

◆ garbage()

◆ get_range()

◆ has_image()

◆ hash()

◆ invert()

◆ is_selector()

◆ mark()

◆ negate()

◆ operator!=()

◆ operator()()

◆ operator<()

◆ operator==()

◆ pstats()

◆ refCounter()

◆ skip_variable()

◆ statistics()

Friends And Related Function Documentation

◆ _GHom

◆ fixpoint

◆ Hom

◆ monotonic

◆ operator&

◆ operator* [1/2]

◆ operator* [2/2]

◆ operator+

◆ operator-

◆ operator<<

◆ operator^ [1/2]

◆ operator^ [2/2]

Member Data Documentation

◆ concret

◆ full_range

◆ id