SHom.h File Reference

#include "ddd/SDD.h"
#include "ddd/Hom.h"
#include "ddd/Cache.hh"
#include "ddd/util/set.hh"

Include dependency graph for SHom.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	GShom
	This class is the base class for Homomorphisms over SDD. More...
class	Shom
	This is the user interface class to manipulate homomorphisms. More...
struct	std::less< GShom >
	Compares two GShom in hash tables. More...
class	_GShom
	The concrete data class for Homomorphisms. More...
class	StrongShom
	The abstract base class for user defined operations. More...
class	MyGShom

Namespaces
	std

Functions
Composition operators between SDD homomorphisms.
GShom	fixpoint (const GShom &, bool is_top_level=false)
	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	extractPotential (int var)
	Extract the domain of a given variable. More...
GShom	ITE (const GShom &cond, const GShom &iftrue, const GShom &iffalse)
	An IF-THEN-ELSE construct. More...
GShom	operator! (const GShom &cond)
	A negation/complement constructor for selector homomophisms. More...
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 GShom &, const GShom &)
	Intersection with a selector Hom. 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...
GShom	operator- (const GShom &, const GShom &)
	Set difference (generalized). More...
GShom	apply2k (const GSDD &)
	Apply a 2 level DDD representing a transition relation to current variable. More...

Function Documentation

apply2k()

GShom apply2k

(

const GSDD &

d

)

Apply a 2 level DDD representing a transition relation to current variable.

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

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

extractPotential()

GShom extractPotential

(

int

var

)

Extract the domain of a given variable.

Returns the union of the first nodes encountered that bear this variable, with 1 as signle successor. In other words, an SDD of a single var, with an edge value that is the union of all Datasets in the reachable SDD.

Referenced by sns::LocalApply::invert(), and sns::SLocalApply::invert().

fixpoint()

GShom fixpoint	(	const GShom &	h,
		bool	is_top_level = false
	)

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 )

Referenced by sns::RecFireSat::eval(), sns::Fixpoint::eval(), sns::Fixpoint::has_image(), and sns::Fixpoint::invert().

ITE()

GShom ITE	(	const GShom &	cond,
		const GShom &	iftrue,
		const GShom &	iffalse
	)

An IF-THEN-ELSE construct.

The behavior of the condition must be a selection, as indicated by its isSelector() flag. PITFALL : Otherwise an assertion violation will be raised (with an explicit stderr message)

Semantics : ITE ( cond, iftrue, iffalse) (d) = (iftrue & cond(d)) + (iffalse & !cond(d))

References GShom::is_selector(), and printCondError().

localApply() [1/2]

GShom localApply	(	const GHom &	h,
		int	target
	)

Apply a homomorphism on a target variable.

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

Referenced by addCompositionParameter(), buildUnionParameters(), sns::Fixpoint::eval(), sns::Fixpoint::has_image(), sns::LocalApply::invert(), sns::SLocalApply::invert(), operator!(), and operator*().

localApply() [2/2]

GShom localApply	(	const GShom &	h,
		int	target
	)

operator!()

GShom operator!

(

const GShom &

cond

)

A negation/complement constructor for selector homomophisms.

Let cond be a selector, !cond(d) = d - cond(d) PITFALL : Raises an assert violation if is_selector() returns false !

References _GShom::get_concret(), GShom::id, GShom::is_selector(), localApply(), Shom::null, and printCondError().

operator&()

GShom operator&	(	const GShom &	h1,
		const GShom &	h2
	)

Composition by circ (rond) of homomorphisms.

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

operator*() [1/3]

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

Intersection with a constant SDD.

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

operator*() [2/3]

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

Intersection with a constant SDD.

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

operator*() [3/3]

GShom operator*	(	const GShom &	h,
		const GShom &	cond
	)

Intersection with a selector Hom.

Semantics : (d1 * sel) (d) = d1 (d) * sel (d) WARNING : assert failure if 2nd argument is not a selector.

References _GShom::get_concret(), GHom::id, GShom::id, GShom::is_selector(), localApply(), Shom::null, and printCondError().

operator+()

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

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

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

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

GShom operator-	(	const GShom &	h1,
		const GShom &	h2
	)

Set difference (generalized).

Note that this operation is not commutative, nor is it linear. This means the operation a priori cannot "skip", and it could be incorrect to apply it at an arbitrary level of the structure. However, in some cases it is still useful and it can be applied directly at the top node of the structure yielding correct results.

Semantics : (h1 - h2) (d) = h1(d) - h2(d)

operator^() [1/2]

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

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 &	h,
		const GSDD &	d
	)

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