Hom.h File Reference

#include "ddd/DDD.h"
#include "ddd/util/hash_support.hh"
#include "ddd/util/set.hh"
#include <map>
#include <cassert>
#include <iostream>

Include dependency graph for Hom.h:

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

Go to the source code of this file.

Classes
class	GHom
	This class is the base class representing a homomorphism over DDD. More...
class	Hom
	This is the user interface class to manipulate homomorphisms. More...
struct	std::less< GHom >
	Compares two GHom in hash tables. More...
class	_GHom
	The concrete data class for Homomorphisms. More...
class	StrongHom
	The abstract base class for user defined operations. More...
class	MyGHom
	Unknown function for this class. More...

Namespaces
	std

Functions
Composition operators between DDD homomorphisms.
GHom	fixpoint (const GHom &, bool is_top_level=false)
	Apply a homomorphism until fixpoint is reached. More...
GHom	operator! (const GHom &cond)
	A negation/complement constructor for selector homomophisms. More...
GHom	ITE (const GHom &cond, const GHom &iftrue, const GHom &iffalse)
	An IF-THEN-ELSE construct. More...
GHom	operator+ (const GHom &, const GHom &)
	Composition by union of two homomorphisms. More...
GHom	operator& (const GHom &, const GHom &)
	Composition by circ (rond) of homomorphisms. More...
GHom	operator* (const GDDD &, const GHom &)
	Intersection with a constant DDD. More...
GHom	operator* (const GHom &, const GDDD &)
	Intersection with a constant SDD. More...
GHom	operator* (const GHom &, const GHom &)
	Intersection with a selector Hom. More...
GHom	operator^ (const GDDD &, const GHom &)
	Left Concatenation of a constant SDD. More...
GHom	operator^ (const GHom &, const GDDD &)
	Right Concatenation of a constant SDD. More...
GHom	operator- (const GHom &, const GDDD &)
	Set difference. More...
GHom	apply2k (const GDDD &)
	Apply a 2 level DDD representing a transition relation to current variable. More...
GDDD	computeDomain (int var, const GDDD &)
	Return the domain of the first variable bearing the provided index in the provided DDD Useful for invert computations. More...
bool	commutative (const GHom &h1, const GHom &h2)
	return true if the provided operations are commutative More...

Function Documentation

apply2k()

GHom apply2k

(

const GDDD &

d

)

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

References GDDD::null, GDDD::one, and GDDD::top.

commutative()

bool commutative	(	const GHom &	h1,
		const GHom &	h2
	)

return true if the provided operations are commutative

References GHom::get_range(), GHom::is_selector(), and notInRange().

Referenced by addCompositionParameter().

computeDomain()

GDDD computeDomain	(	int	var,
		const GDDD &	d
	)

Return the domain of the first variable bearing the provided index in the provided DDD Useful for invert computations.

Referenced by _setVarConst::invert(), and _incVar::invert().

fixpoint()

GHom fixpoint	(	const GHom &	h,
		bool	is_top_level
	)

Apply a homomorphism until fixpoint is reached.

This operator applies its argument to a node until a 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 )

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

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

ITE()

GHom ITE	(	const GHom &	cond,
		const GHom &	iftrue,
		const GHom &	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 GHom::is_selector(), and printCondError().

operator!()

GHom operator!

(

const GHom &

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 !

operator&()

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

Composition by circ (rond) of homomorphisms.

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

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

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

operator*() [1/3]

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

Intersection with a constant DDD.

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

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

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

operator*() [2/3]

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

Intersection with a constant SDD.

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

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

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

operator*() [3/3]

GHom operator*	(	const GHom &	h,
		const GHom &	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 GHom::is_selector(), and GDDD::null.

operator+()

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

Composition by union of two homomorphisms.

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

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

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

operator-()

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

Set difference.

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

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

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

operator^() [1/2]

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

Left Concatenation of a constant SDD.

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

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)

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

operator^() [2/2]

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

Right Concatenation of a constant SDD.

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

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

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

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