Inheritance diagram for sns::Add:

Collaboration diagram for sns::Add:

Classes
struct	partition

Public Types
typedef std::vector< GShom >	Gset_t

typedef Gset_t::const_iterator	Gset_it

typedef hash_map< int, partition >::type	partition_cache_type

typedef std::vector< GShom >	parameters_t

typedef parameters_t::const_iterator	parameters_it

Public Member Functions
	Add (const d3::set< GShom >::type &p, bool have_id)

bool	get_have_id () const

bool	operator== (const _GShom &h) const
	Comparator. More...

size_t	hash () const
	Hash key computation. More...

_GShom *	clone () const

GSDD	has_image (const GSDD &d) const

bool	is_selector () const
	The isSelector predicate indicates a homomorphism that only selects paths in the SDD (no modifications, no additions) Tagging with isSelector() allows to enable optimizations and makes the homomorphism eligible as "condition" in ITE construct. More...

GShom	invert (const GSDD &pot) const

bool	skip_variable (int var) const
	The skip_variable predicate indicates which variables are "don't care" with respect to this SHom. More...

const GShom::range_t	get_range () const
	The range returns the dual of skip_variable, default implem considers that all variables are affected by this homomorphism. More...

partition	get_partition (int var) const

GSDD	eval (const GSDD &d) const
	The computation function responsible for evaluation over a node. More...

void	mark () const
	For garbage collection. Used in first phase of garbage collection. More...

void	print (std::ostream &os) const

GSDD	has_image_skip (const GSDD &) const

virtual GShom	compose (const GShom &) const

void	mark_if_refd () const

void	ref () const

void	deref () const

unsigned long int	refCounter () const

bool	is_marked () const

void	set_mark (bool val) const

Static Public Member Functions
static const _GShom *	get_concret (const GShom &gshom)
	TODO : this is a dirty trick to allow us to do terms rewriting in Add, Fixpoint etc... More...

Public Attributes
parameters_t	parameters

Private Member Functions
void	factorizeByLevel (Gset_t &G, int target) const
	apply factorization rules adapted to g = l & f More...

GSDD	eval_skip (const GSDD &) const
	The procedure responsible for propagating efficiently across "skipped" variable nodes. More...

virtual bool	immediat () const
	For operation cache management. More...

Private Attributes
partition_cache_type	partition_cache

bool	have_id

int	_refCounter
	For garbage collection. More...

Member Typedef Documentation

◆ Gset_it

typedef Gset_t::const_iterator sns::Add::Gset_it

◆ Gset_t

typedef std::vector<GShom> sns::Add::Gset_t

◆ parameters_it

typedef parameters_t::const_iterator sns::Add::parameters_it

◆ parameters_t

typedef std::vector<GShom> sns::Add::parameters_t

◆ partition_cache_type

typedef hash_map<int, partition>::type sns::Add::partition_cache_type

Constructor & Destructor Documentation

◆ Add()

sns::Add::Add	(	const d3::set< GShom >::type &	p,
		bool	have_id
	)

inline

Referenced by clone().

Member Function Documentation

◆ clone()

_GShom* sns::Add::clone ( ) const

inlinevirtual

Implements _GShom.

References Add().

◆ compose()

GShom _GShom::compose ( const GShom & r ) const

virtualinherited

References GShom::id, and GSDD::null.

Referenced by GShom::compose().

◆ deref()

void _GShom::deref ( ) const

inlineinherited

References _GShom::_refCounter.

Referenced by Shom::operator=(), and Shom::~Shom().

◆ eval()

GSDD sns::Add::eval ( const GSDD & ) const

inlinevirtual

The computation function responsible for evaluation over a node.

Users should not directly use this. Normal behavior is to use GShom::operator() that encapsulates this call with operation caching.

Implements _GShom.

References SDED::add(), _GShom::GShom, GSDD::null, GSDD::one, parameters, partition_cache, skip_variable(), GSDD::top, and GSDD::variable().

◆ eval_skip()

GSDD _GShom::eval_skip ( const GSDD & d ) const

privateinherited

The procedure responsible for propagating efficiently across "skipped" variable nodes.

References GSDD::begin(), GSDD::end(), _GShom::eval(), GShom::id, _GShom::immediat(), GSDD::nbsons(), GSDD::null, GSDD::one, _GShom::skip_variable(), square_union(), GSDD::top, and GSDD::variable().

Referenced by GShom::eval().

◆ factorizeByLevel()

void sns::Add::factorizeByLevel	(	Gset_t &	G,
		int	target
	)		const

inlineprivate

apply factorization rules adapted to g = l & f

First step : for any g1 = l1 & f1 and any g2 = l2 & f2, if l1 == l2 then rewrite into g' = g1 + g2 = l1 & (f1+f2)

load the map

We have now obtained a partition of G into the terms of the form l & f, stored by l key in the map_ltof, and the "normal" or default g terms, that are still in G.

Now apply second factorization wrt. the f value

look if the term exists

Finally reinsert into the G set

References GShom::add, and _GShom::get_concret().

Referenced by skip_variable().

◆ get_concret()

static const _GShom* _GShom::get_concret ( const GShom & gshom )

inlinestaticinherited

TODO : this is a dirty trick to allow us to do terms rewriting in Add, Fixpoint etc...

A more elegant architecture would be nice.

References GShom::concret.

Referenced by addCompositionParameter(), addParameter(), buildUnionParameters(), sns::RecFireSat::eval(), sns::Fixpoint::eval(), factorizeByLevel(), GShom::GShom(), sns::Fixpoint::has_image(), operator!(), operator*(), sns::recFireSat(), sns::Inter::skip_variable(), skip_variable(), and sns::RightConcat::skip_variable().

◆ get_have_id()

bool sns::Add::get_have_id ( ) const

inline

References have_id.

◆ get_partition()

partition sns::Add::get_partition ( int var ) const

inline

References partition_cache, and skip_variable().

◆ get_range()

const GShom::range_t sns::Add::get_range ( ) const

inlinevirtual

The range returns the dual of skip_variable, default implem considers that all variables are affected by this homomorphism.

Reimplemented from _GShom.

References parameters.

◆ has_image()

GSDD sns::Add::has_image ( const GSDD & d ) const

inlinevirtual

Reimplemented from _GShom.

References GSDD::null, and parameters.

◆ has_image_skip()

GSDD _GShom::has_image_skip ( const GSDD & d ) const

inherited

References GSDD::begin(), GSDD::end(), GShom::has_image(), _GShom::has_image(), GShom::id, GSDD::null, GSDD::one, _GShom::skip_variable(), GSDD::top, and GSDD::variable().

◆ hash()

size_t sns::Add::hash ( ) const

inlinevirtual

Hash key computation.

It is essential for good hash table operation that the spread of the keys be as good as possible. Also, fast hash key computation is a good design goal. Note that bad hash functions will yield more collisions, thus equality comparisons which may be quite costly.

Implements _GShom.

References parameters.

◆ immediat()

virtual bool _GShom::immediat ( ) const

inlineprivatevirtualinherited

For operation cache management.

If immediat==true, eval is called without attempting a cache hit. Currently only the constant homomorphism has this attribute set to true. Overload and return true for immediate computations.

Reimplemented in sns::Constant, and sns::Identity.

Referenced by _GShom::eval_skip(), and GShom::operator()().

◆ invert()

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

inlinevirtual

Reimplemented from _GShom.

References GShom::add, and parameters.

◆ is_marked()

bool _GShom::is_marked ( ) const

inlineinherited

References _GShom::_refCounter.

Referenced by _GShom::set_mark().

◆ is_selector()

bool sns::Add::is_selector ( ) const

inlinevirtual

The isSelector predicate indicates a homomorphism that only selects paths in the SDD (no modifications, no additions) Tagging with isSelector() allows to enable optimizations and makes the homomorphism eligible as "condition" in ITE construct.

Reimplemented from _GShom.

References parameters.

◆ mark()

void sns::Add::mark ( ) const

inlinevirtual

For garbage collection. Used in first phase of garbage collection.

Reimplemented from _GShom.

References parameters, and partition_cache.

◆ mark_if_refd()

void _GShom::mark_if_refd ( ) const

inlineinherited

References _GShom::refCounter(), and _GShom::set_mark().

◆ operator==()

bool sns::Add::operator== ( const _GShom & h ) const

inlinevirtual

Comparator.

Used in case of hash collision. Should be appropriately defined in derived classes, in particular in user defined homomorphisms.

Implements _GShom.

References parameters.

◆ print()

void sns::Add::print ( std::ostream & os ) const

inlinevirtual

Implements _GShom.

References parameters.

◆ ref()

void _GShom::ref ( ) const

inlineinherited

References _GShom::_refCounter.

Referenced by Shom::operator=(), and Shom::Shom().

◆ refCounter()

unsigned long int _GShom::refCounter ( ) const

inlineinherited

References _GShom::_refCounter.

Referenced by _GShom::mark_if_refd(), Shom::operator=(), GShom::refCounter(), and Shom::~Shom().

◆ set_mark()

void _GShom::set_mark ( bool val ) const

inlineinherited

References _GShom::_refCounter, _GShom::is_marked(), and _GShom::mark().

Referenced by GShom::garbage(), GShom::mark(), and _GShom::mark_if_refd().

◆ skip_variable()

bool sns::Add::skip_variable ( int ) const

inlinevirtual

The skip_variable predicate indicates which variables are "don't care" with respect to this SHom.

This is defined as a StrongHom with : phi(var,val) { if ( skip_variable(var) ) return GShom( var, val, this ); else { real behavior } }

Reimplemented from _GShom.

References GShom::add, sns::Add::partition::F, factorizeByLevel(), sns::Add::partition::G, _GShom::get_concret(), sns::Add::partition::has_local, sns::Add::partition::L, parameters, partition_cache, and _GShom::skip_variable().

Referenced by eval(), and get_partition().

Member Data Documentation

◆ _refCounter

int _GShom::_refCounter

mutableprivateinherited

For garbage collection.

Counts the number of times a _GShom is referenced from the context of an Shom. For garbage collection: lowest bit of refCounter gives marking value for mark&sweep. Used in the two phase garbage collection process. A Shom that is not marked after the first pass over the unicity table, will be sweeped in the second phase. Outside of garbage collection routine, marking should always bear the value false.

Referenced by _GShom::deref(), _GShom::is_marked(), _GShom::ref(), _GShom::refCounter(), and _GShom::set_mark().

◆ have_id

bool sns::Add::have_id

private

Referenced by get_have_id().

◆ parameters

parameters_t sns::Add::parameters

Referenced by eval(), get_range(), has_image(), hash(), invert(), is_selector(), mark(), operator==(), print(), and skip_variable().

◆ partition_cache

partition_cache_type sns::Add::partition_cache

mutableprivate

Referenced by eval(), get_partition(), mark(), and skip_variable().

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

SHom.cpp

Classes

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Private Member Functions

Private Attributes

Member Typedef Documentation

◆ Gset_it

◆ Gset_t

◆ parameters_it

◆ parameters_t

◆ partition_cache_type

Constructor & Destructor Documentation

◆ Add()

Member Function Documentation

◆ clone()

◆ compose()

◆ deref()

◆ eval()

◆ eval_skip()

◆ factorizeByLevel()

◆ get_concret()

◆ get_have_id()

◆ get_partition()

◆ get_range()

◆ has_image()

◆ has_image_skip()

◆ hash()

◆ immediat()

◆ invert()

◆ is_marked()

◆ is_selector()

◆ mark()

◆ mark_if_refd()

◆ operator==()

◆ print()

◆ ref()

◆ refCounter()

◆ set_mark()

◆ skip_variable()

Member Data Documentation

◆ _refCounter

◆ have_id

◆ parameters

◆ partition_cache