This class is the base class for Homomorphisms over SDD. More...

#include <SHom.h>

Inheritance diagram for GShom:

Collaboration diagram for GShom:

Friends
class	Shom
	Open access to concret for Shom class. More...

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

Memory Management routines.
enum	fixpointStrategy { BFS , DFS }

enum	saturationStrategy { ORDINARY , RECFIREANDSAT }

static fixpointStrategy	fixpointStrategy_ = BFS

static saturationStrategy	saturationStrategy_ = ORDINARY

void	mark () const
	Mark a concrete data as in use (forbids garbage collection of the data). More...

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

static unsigned int	statistics ()
	Return the current size of the unicity table for GShom. More...

static size_t	cache_size ()
	Return the current size of the cache for GShom. More...

static size_t	cache_peak ()
	Return the peak size of the cache for GShom. More...

static void	pstats (bool reinit=true)
	Print some usage statistics on Shom. More...

static void	garbage ()
	Collects and destroys unused homomorphisms. More...

static fixpointStrategy	getFixpointStrategy ()

static void	setFixpointStrategy (fixpointStrategy strat)

static saturationStrategy	getSaturationStrategy ()

static void	setSaturationStrategy (saturationStrategy strat)

Friendly hard coded composition operators.
Open full access for library implemented hard coded operations.
typedef GSDD	NodeType

GShom	fixpoint (const GShom &, bool is_top_level)
	Apply a homomorphism until fixpoint is reached. More...

GShom	localApply (const GHom &, int target)
	Apply a homomorphism on a target variable. More...

GShom	localApply (const GShom &, int target)

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

GShom	operator+ (const GShom &, const GShom &)
	Composition by union of two homomorphisms. More...

GShom	operator& (const GShom &, const GShom &)
	Composition by circ (rond) of homomorphisms. More...

GShom	operator* (const GSDD &, const GShom &)
	Intersection with a constant SDD. More...

GShom	operator* (const GShom &, const GSDD &)
	Intersection with a constant SDD. More...

GShom	operator^ (const GSDD &, const GShom &)
	Left Concatenation of a constant SDD. More...

GShom	operator^ (const GShom &, const GSDD &)
	Right Concatenation of a constant SDD. More...

GShom	operator- (const GShom &, const GSDD &)
	Set difference. More...

const _GShom *	concret
	Pointer to the data instance in the unicity table. More...

Comparisons between GShom.
Comparisons between GShom for unicity table. Both equality comparison and total ordering provided to allow hash and map storage of GShom
typedef d3::set< int >::type	range_t

typedef range_t::const_iterator	range_it

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

bool	operator== (const GShom &h) const

bool	operator!= (const GShom &h) const

bool	operator< (const GShom &h) const

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

bool	skip_variable (int) const
	This predicate is true if the homomorphism "skips" this variable. More...

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

Evaluation mechanism for homomorphisms.
std::ostream &	operator<< (std::ostream &os, const GShom &h)

GSDD	operator() (const GSDD &d) const
	Applying a homomorphism to a node returns a node. More...

GSDD	eval (const GSDD &d) const
	The full evaluation, this is the computational procedure, that is called when the computation cache yields a miss. More...

int	refCounter () const
	For debug and development purposes. Gives the reference count of the concrete data. More...

static GShom	add (const d3::set< GShom >::type &s)
	Compute an n-ary sum between homomorphisms. More...

Public Constructors
static const GShom	id
	Elementary SDD homomorphism identity. Applied to any SDD d, it returns d. More...

	GShom ()
	Default constructor builds identity homomorphism. More...

	GShom (const _GShom *_h)
	Pseudo-private constructor. More...

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

	GShom (const _GShom &_h)
	To build GShom from pointers to user homomomorphisms. More...

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

	GShom (const GSDD &d)
	Construct a constant homomorphism. More...

	GShom (int var, const DataSet &val, const GShom &h=GShom::id)
	Left concatenation of a single arc SDD. More...

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

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

GShom	compose (const GShom &) const

Detailed Description

This class is the base class for Homomorphisms over SDD.

Composition operators between homomorphisms are defined at this level, so this is the common ground between user-defined homomorphisms (i.e. derived classes of StrongShom) and hard-coded operations such as union, concatenation etc... Like GSDD, GShom implement a smart pointer behavior, the actual data (instance of hidden private class _GShom) linked to an instance of GShom has only one occurrence in memory, thanks to a unicity table.

User homomorphisms should be manipulated and instanciated using Shom, as GShom provide no reference counting and are thus likely to be collected in a MemoryManager::garbage() call. Shom provides reference counting.

Member Typedef Documentation

◆ NodeType

typedef GSDD GShom::NodeType

◆ range_it

typedef range_t::const_iterator GShom::range_it

◆ range_t

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

Member Enumeration Documentation

◆ fixpointStrategy

enum GShom::fixpointStrategy

Enumerator
BFS
DFS

◆ saturationStrategy

enum GShom::saturationStrategy

Enumerator
ORDINARY
RECFIREANDSAT

Constructor & Destructor Documentation

◆ GShom() [1/7]

GShom::GShom ( )

inline

Default constructor builds identity homomorphism.

◆ GShom() [2/7]

GShom::GShom ( const _GShom * _h )

Pseudo-private constructor.

This should only be called with pointers into the unicity table. For example return this in a StrongHom phi() body is legal.

Parameters

_h	pointer into the unicity table

◆ GShom() [3/7]

GShom::GShom ( _GShom * _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.

◆ GShom() [4/7]

GShom::GShom ( const _GShom & _h )

To build GShom from pointers to user homomomorphisms.

This call ensures unicity of representation.

◆ GShom() [5/7]

GShom::GShom ( const MLShom & h )

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

◆ GShom() [6/7]

GShom::GShom ( const GSDD & d )

Construct a constant homomorphism.

Applied to any SDD this homomorphism will return the value it was initialized with.

◆ GShom() [7/7]

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

Left concatenation of a single arc SDD.

This is provided as a convenience and to avoid the inefficiency if we build a node pointing to GSDD::one and then concatenate something to it. Applied to a SDD d, this homomorphism will return var–val->h(d).

Parameters

var	the variable labeling the node to left concat
val	the set of values labeling the arc
h	the homomorphism to apply on the argument d. This defaults to GSHom::id.

References canonical, concret, DataSet::empty(), _GShom::get_concret(), and Shom::null.

Member Function Documentation

◆ add()

static GShom GShom::add ( const d3::set< GShom >::type & s )

static

Compute an n-ary sum between homomorphisms.

This should be slightly more efficient in evaluation than a composition of binary sums constructed using the friend operator+.

Todo:: : move this to friend status not static member for more homogeneity with other operators.

◆ cache_peak()

size_t GShom::cache_peak ( )

static

Return the peak size of the cache for GShom.

References sns::cache, and Cache< FuncType, ParamType, ResType, EvalFunc >::peak().

◆ cache_size()

size_t GShom::cache_size ( )

static

Return the current size of the cache for GShom.

References sns::cache, and Cache< FuncType, ParamType, ResType, EvalFunc >::size().

Referenced by Statistic::load().

◆ compose()

GShom GShom::compose ( const GShom & o ) const

References _GShom::compose(), and concret.

◆ eval()

GSDD GShom::eval ( const GSDD & d ) const

The full evaluation, this is the computational procedure, that is called when the computation cache yields a miss.

Users should not use this function directly, but only through GSDD::operator().

References concret, and _GShom::eval_skip().

Referenced by operator()().

◆ garbage()

void GShom::garbage ( )

static

Collects and destroys unused homomorphisms.

Do not call this directly but through MemoryManager::garbage() as order of calls (among GSDD::garbage(), GShom::garbage(), SDED::garbage()) is important.

References addCache, sns::cache, canonical, Cache< FuncType, ParamType, ResType, EvalFunc >::clear(), sns::imgcache, and _GShom::set_mark().

Referenced by MemoryManager::garbage().

◆ get_range()

const GShom::range_t GShom::get_range ( ) const

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

References concret, and _GShom::get_range().

Referenced by commutative(), sns::SNotCond::get_range(), sns::RecFireSat::get_range(), sns::Compose::get_range(), sns::Fixpoint::get_range(), and notInRange().

◆ getFixpointStrategy()

static fixpointStrategy GShom::getFixpointStrategy ( )

inlinestatic

References fixpointStrategy_.

Referenced by sns::Fixpoint::eval().

◆ getSaturationStrategy()

static saturationStrategy GShom::getSaturationStrategy ( )

inlinestatic

References saturationStrategy_.

Referenced by sns::Fixpoint::eval().

◆ has_image()

GSDD GShom::has_image ( const GSDD & d ) const

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

References sns::imgcache, and GSDD::null.

Referenced by sns::RecFireSat::eval(), sns::Inter::has_image(), sns::SLocalApply::has_image(), sns::SNotCond::has_image(), sns::And::has_image(), sns::Compose::has_image(), sns::LeftConcat::has_image(), sns::RightConcat::has_image(), sns::Fixpoint::has_image(), and _GShom::has_image_skip().

◆ hash()

size_t GShom::hash ( ) const

inline

For storage in a hash table.

References concret, and ddd::knuth32_hash().

Referenced by nsMLShom::GShomAdapter::hash(), nsMLShom::ConstantUp::hash(), sns::Mult::hash(), sns::Inter::hash(), sns::SLocalApply::hash(), sns::SNotCond::hash(), sns::RecFireSat::hash(), sns::Compose::hash(), sns::LeftConcat::hash(), sns::RightConcat::hash(), sns::Minus::hash(), sns::HomMinus::hash(), and sns::Fixpoint::hash().

◆ invert()

GShom GShom::invert ( const GSDD & pot ) const

returns the predescessor homomorphism, using pot to determine variable domains

References concret, and _GShom::invert().

Referenced by sns::Mult::invert(), sns::Inter::invert(), sns::SLocalApply::invert(), sns::RecFireSat::invert(), sns::Compose::invert(), sns::Minus::invert(), sns::HomMinus::invert(), and sns::Fixpoint::invert().

◆ is_selector()

bool GShom::is_selector ( ) const

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

References concret, and _GShom::is_selector().

Referenced by commutative(), sns::Mult::is_selector(), sns::Inter::is_selector(), sns::SLocalApply::is_selector(), sns::RecFireSat::is_selector(), sns::Compose::is_selector(), sns::Minus::is_selector(), sns::HomMinus::is_selector(), sns::Fixpoint::is_selector(), ITE(), operator!(), and operator*().

◆ mark()

void GShom::mark ( ) const

Mark a concrete data as in use (forbids garbage collection of the data).

References concret, and _GShom::set_mark().

Referenced by sns::Fixpoint::eval(), sns::Mult::mark(), sns::Inter::mark(), sns::SLocalApply::mark(), sns::SNotCond::mark(), sns::RecFireSat::mark(), sns::Compose::mark(), sns::LeftConcat::mark(), sns::RightConcat::mark(), sns::Minus::mark(), sns::HomMinus::mark(), and sns::Fixpoint::mark().

◆ operator!=()

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

inline

References concret.

◆ operator()()

GSDD GShom::operator() ( const GSDD & d ) const

Applying a homomorphism to a node returns a node.

This is the normal way for users of computing the application of a homomorphism.

References sns::cache, concret, eval(), _GShom::immediat(), and GSDD::null.

◆ operator<()

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

inline

References concret.

◆ operator==()

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

inline

References concret.

◆ pstats()

void GShom::pstats ( bool reinit = true )

static

Print some usage statistics on Shom.

Mostly used for development and debug.

Todo:: Allow output not in std::cout.

References _GShom, sns::cache, and canonical.

Referenced by MemoryManager::pstats().

◆ refCounter()

int GShom::refCounter ( ) const

For debug and development purposes. Gives the reference count of the concrete data.

References concret, and _GShom::refCounter().

◆ setFixpointStrategy()

static void GShom::setFixpointStrategy ( fixpointStrategy strat )

inlinestatic

References fixpointStrategy_.

◆ setSaturationStrategy()

static void GShom::setSaturationStrategy ( saturationStrategy strat )

inlinestatic

References saturationStrategy_.

◆ skip_variable()

bool GShom::skip_variable ( int var ) const

This predicate is true if the homomorphism "skips" this variable.

References concret, and _GShom::skip_variable().

Referenced by sns::Mult::eval(), nsMLShom::GShomAdapter::skip_variable(), sns::SNotCond::skip_variable(), sns::RecFireSat::skip_variable(), sns::Compose::skip_variable(), and sns::Fixpoint::skip_variable().

◆ statistics()

unsigned int GShom::statistics ( )

static

Return the current size of the unicity table for GShom.

References canonical.

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

Friends And Related Function Documentation

◆ _GShom

friend class _GShom

friend

Open access to _GShom based homomophisms.

Referenced by pstats().

◆ add

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

friend

Referenced by sns::Fixpoint::eval(), sns::Add::factorizeByLevel(), sns::Add::invert(), and sns::Add::skip_variable().

◆ fixpoint

GShom fixpoint	(	const GShom &	,
		bool	is_top_level
	)

friend

Apply a homomorphism until fixpoint is reached.

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 )

◆ localApply [1/2]

GShom localApply	(	const GHom &	,
		int	target
	)

friend

Apply a homomorphism on a target variable.

This ensures that the operation is local to this variable, and is used to implement auto-saturation.

◆ localApply [2/2]

GShom localApply	(	const GShom &	,
		int	target
	)

friend

◆ operator&

GShom operator&	(	const GShom &	,
		const GShom &
	)

friend

Composition by circ (rond) of homomorphisms.

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

◆ operator* [1/2]

GShom operator*	(	const GSDD &	,
		const GShom &
	)

friend

Intersection with a constant SDD.

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

◆ operator* [2/2]

GShom operator*	(	const GShom &	,
		const GSDD &
	)

friend

Intersection with a constant SDD.

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

◆ operator+

GShom operator+	(	const GShom &	,
		const GShom &
	)

friend

Composition by union of two homomorphisms.

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-

GShom operator-	(	const GShom &	,
		const GSDD &
	)

friend

Set difference.

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 GShom &	h
	)

friend

◆ operator^ [1/2]

GShom operator^	(	const GSDD &	,
		const GShom &
	)

friend

Left Concatenation of a constant SDD.

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]

GShom operator^	(	const GShom &	,
		const GSDD &
	)

friend

Right Concatenation of a constant SDD.

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

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

◆ Shom

friend class Shom

friend

Open access to concret for Shom class.

Member Data Documentation

◆ concret

const _GShom* GShom::concret

private

Pointer to the data instance in the unicity table.

Referenced by compose(), eval(), _GShom::get_concret(), get_range(), GShom(), hash(), invert(), is_selector(), mark(), operator!=(), operator()(), operator<(), Shom::operator=(), operator==(), refCounter(), Shom::Shom(), skip_variable(), and Shom::~Shom().

◆ fixpointStrategy_

GShom::fixpointStrategy GShom::fixpointStrategy_ = BFS

staticprivate

Referenced by getFixpointStrategy(), and setFixpointStrategy().

◆ full_range

const GShom::range_t GShom::full_range = GShom::range_t()

static

The full_range : that targets everyone.

Referenced by _GShom::get_range().

◆ id

const GShom GShom::id

static

Elementary SDD homomorphism identity. Applied to any SDD d, it returns d.

Referenced by apply2k(), buildUnionParameters(), _GShom::compose(), StrongMLShom::eval(), nsMLShom::Identity::eval(), nsMLShom::GShomAdapter::eval(), sns::Mult::eval(), sns::And::eval(), sns::Fixpoint::eval(), _GShom::eval_skip(), sns::And::has_image(), sns::Fixpoint::has_image(), _GShom::has_image_skip(), sns::Mult::invert(), sns::And::invert(), sns::Minus::invert(), sns::HomMinus::invert(), sns::Fixpoint::invert(), operator!(), and operator*().

◆ saturationStrategy_

GShom::saturationStrategy GShom::saturationStrategy_ = ORDINARY

staticprivate

Referenced by getSaturationStrategy(), and setSaturationStrategy().

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

Friends

Memory Management routines.

Friendly hard coded composition operators.

Comparisons between GShom.

Evaluation mechanism for homomorphisms.

Public Constructors

Detailed Description

Member Typedef Documentation

◆ NodeType

◆ range_it

◆ range_t

Member Enumeration Documentation

◆ fixpointStrategy

◆ saturationStrategy

Constructor & Destructor Documentation

◆ GShom() [1/7]

◆ GShom() [2/7]

◆ GShom() [3/7]

◆ GShom() [4/7]

◆ GShom() [5/7]

◆ GShom() [6/7]

◆ GShom() [7/7]

Member Function Documentation

◆ add()

◆ cache_peak()

◆ cache_size()

◆ compose()

◆ eval()

◆ garbage()

◆ get_range()

◆ getFixpointStrategy()

◆ getSaturationStrategy()

◆ has_image()

◆ hash()

◆ invert()

◆ is_selector()

◆ mark()

◆ operator!=()

◆ operator()()

◆ operator<()

◆ operator==()

◆ pstats()

◆ refCounter()

◆ setFixpointStrategy()

◆ setSaturationStrategy()

◆ skip_variable()

◆ statistics()

Friends And Related Function Documentation

◆ _GShom

◆ add

◆ fixpoint

◆ localApply [1/2]

◆ localApply [2/2]

◆ operator&

◆ operator* [1/2]

◆ operator* [2/2]

◆ operator+

◆ operator-

◆ operator<<

◆ operator^ [1/2]

◆ operator^ [2/2]

◆ Shom

Member Data Documentation

◆ concret

◆ fixpointStrategy_

◆ full_range

◆ id

◆ saturationStrategy_