This is the user interface class to manipulate homomorphisms. More...

#include <SHom.h>

Inheritance diagram for Shom:

Collaboration diagram for Shom:

Public Member Functions
Assignment operators.
Shom &	operator= (const GShom &)
	Overloaded behavior for assignment operator, maintains reference counting. More...

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

Public Constructors.
Default constructor builds identity homomorphism.
static const Shom	null = GSDD::null

	Shom (const GShom &h=GShom::id)
	Build an Shom from a GShom. More...

	Shom (const Shom &h)
	Copy constructor. Maintains reference count. More...

	Shom (const GSDD &d)
	Constructs a constant homomorphism. More...

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

	~Shom ()
	Destructor maintains reference counting. More...

Public Constructors
static const GShom	id
	Elementary SDD homomorphism identity. Applied to any SDD d, it returns d. 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

Comparisons between GShom.
Comparisons between GShom for unicity table. Both equality comparison and total ordering provided to allow hash and map storage of GShom
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...

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

typedef range_t::const_iterator	range_it

Evaluation mechanism for homomorphisms.
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...

Memory Management routines.
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...

enum	fixpointStrategy { BFS , DFS }

enum	saturationStrategy { ORDINARY , RECFIREANDSAT }

static fixpointStrategy	fixpointStrategy_ = BFS

static saturationStrategy	saturationStrategy_ = ORDINARY

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

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

Detailed Description

This is the user interface class to manipulate homomorphisms.

The only difference with GShom is that it implements reference counting so that instances of Shom are not collected upon MemoryManager::garbage().

Member Typedef Documentation

◆ NodeType

typedef GSDD GShom::NodeType

inherited

◆ range_it

typedef range_t::const_iterator GShom::range_it

inherited

◆ range_t

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

inherited

Member Enumeration Documentation

◆ fixpointStrategy

enum GShom::fixpointStrategy

inherited

Enumerator
BFS
DFS

◆ saturationStrategy

enum GShom::saturationStrategy

inherited

Enumerator
ORDINARY
RECFIREANDSAT

Constructor & Destructor Documentation

◆ Shom() [1/4]

Shom::Shom ( const GShom & h = GShom::id )

Build an Shom from a GShom.

References GShom::concret, and _GShom::ref().

◆ Shom() [2/4]

Shom::Shom ( const Shom & h )

Copy constructor. Maintains reference count.

References GShom::concret, and _GShom::ref().

◆ Shom() [3/4]

Shom::Shom ( const GSDD & d )

Constructs a constant homomorphism.

References GShom::concret, and _GShom::ref().

◆ Shom() [4/4]

Shom::Shom	(	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 GShom::concret, and _GShom::ref().

◆ ~Shom()

Shom::~Shom ( )

Destructor maintains reference counting.

Note that the destructor does not truly reclaim memory, MemoryManager::garbage() does that.

References GShom::concret, _GShom::deref(), and _GShom::refCounter().

Member Function Documentation

◆ add()

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

staticinherited

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

staticinherited

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

staticinherited

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

inherited

References _GShom::compose(), and GShom::concret.

◆ eval()

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

inherited

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 GShom::concret, and _GShom::eval_skip().

Referenced by GShom::operator()().

◆ garbage()

void GShom::garbage ( )

staticinherited

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

inherited

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

References GShom::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 ( )

inlinestaticinherited

References GShom::fixpointStrategy_.

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

◆ getSaturationStrategy()

static saturationStrategy GShom::getSaturationStrategy ( )

inlinestaticinherited

References GShom::saturationStrategy_.

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

◆ has_image()

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

inherited

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

inlineinherited

For storage in a hash table.

References GShom::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

inherited

returns the predescessor homomorphism, using pot to determine variable domains

References GShom::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

inherited

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

References GShom::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

inherited

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

References GShom::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

inlineinherited

References GShom::concret.

◆ operator()()

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

inherited

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, GShom::concret, GShom::eval(), _GShom::immediat(), and GSDD::null.

◆ operator<()

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

inlineinherited

References GShom::concret.

◆ operator=() [1/2]

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

Overloaded behavior for assignment operator, maintains reference counting.

References GShom::concret, _GShom::deref(), _GShom::ref(), and _GShom::refCounter().

◆ operator=() [2/2]

Shom & Shom::operator= ( const Shom & h )

Overloaded behavior for assignment operator, maintains reference counting.

References GShom::concret, _GShom::deref(), _GShom::ref(), and _GShom::refCounter().

◆ operator==()

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

inlineinherited

References GShom::concret.

◆ pstats()

void GShom::pstats ( bool reinit = true )

staticinherited

Print some usage statistics on Shom.

Mostly used for development and debug.

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

References GShom::_GShom, sns::cache, and canonical.

Referenced by MemoryManager::pstats().

◆ refCounter()

int GShom::refCounter ( ) const

inherited

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

References GShom::concret, and _GShom::refCounter().

◆ setFixpointStrategy()

static void GShom::setFixpointStrategy ( fixpointStrategy strat )

inlinestaticinherited

References GShom::fixpointStrategy_.

◆ setSaturationStrategy()

static void GShom::setSaturationStrategy ( saturationStrategy strat )

inlinestaticinherited

References GShom::saturationStrategy_.

◆ skip_variable()

bool GShom::skip_variable ( int var ) const

inherited

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

References GShom::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 ( )

staticinherited

Return the current size of the unicity table for GShom.

References canonical.

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

Member Data Documentation

◆ concret

const _GShom* GShom::concret

privateinherited

Pointer to the data instance in the unicity table.

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

◆ fixpointStrategy_

GShom::fixpointStrategy GShom::fixpointStrategy_ = BFS

staticprivateinherited

Referenced by GShom::getFixpointStrategy(), and GShom::setFixpointStrategy().

◆ full_range

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

staticinherited

The full_range : that targets everyone.

Referenced by _GShom::get_range().

◆ id

const GShom GShom::id

staticinherited

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

◆ null

const Shom Shom::null = GSDD::null

static

Referenced by GShom::GShom(), _GShom::invert(), operator!(), and operator*().

◆ saturationStrategy_

GShom::saturationStrategy GShom::saturationStrategy_ = ORDINARY

staticprivateinherited

Referenced by GShom::getSaturationStrategy(), and GShom::setSaturationStrategy().

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

Public Member Functions

Public Constructors.

Public Constructors

Comparisons between GShom.

Evaluation mechanism for homomorphisms.

Memory Management routines.

Friendly hard coded composition operators.

Detailed Description

Member Typedef Documentation

◆ NodeType

◆ range_it

◆ range_t

Member Enumeration Documentation

◆ fixpointStrategy

◆ saturationStrategy

Constructor & Destructor Documentation

◆ Shom() [1/4]

◆ Shom() [2/4]

◆ Shom() [3/4]

◆ Shom() [4/4]

◆ ~Shom()

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=() [1/2]

◆ operator=() [2/2]

◆ operator==()

◆ pstats()

◆ refCounter()

◆ setFixpointStrategy()

◆ setSaturationStrategy()

◆ skip_variable()

◆ statistics()

Member Data Documentation

◆ concret

◆ fixpointStrategy_

◆ full_range

◆ id

◆ null

◆ saturationStrategy_