SHom.cpp File Reference

#include <typeinfo>
#include <cassert>
#include <iostream>
#include "ddd/MemoryManager.h"
#include "ddd/util/configuration.hh"
#include "ddd/util/hash_support.hh"
#include "ddd/util/ext_hash_map.hh"
#include "ddd/Cache.hh"
#include "ddd/MLSHom.h"
#include "ddd/FixObserver.hh"

Include dependency graph for SHom.cpp:

Classes
struct	d3::util::equal< _GShom * >
class	sns::Identity
class	sns::Constant
class	sns::SApply2k
class	sns::Mult
class	sns::Inter
class	sns::SDomExtract
	Extractor of variable domains for invert computations. More...
class	sns::LocalApply
class	sns::SLocalApply
class	sns::SNotCond
class	sns::And
	A commutative composition of n homomorphisms. More...
class	sns::Add
struct	sns::Add::partition
class	sns::RecFireSat
class	sns::Compose
class	sns::LeftConcat
class	sns::RightConcat
class	sns::Minus
class	sns::HomMinus
class	sns::Fixpoint
class	sns::MLShomAdapter

Namespaces
	d3
	d3::util
	sns

Macros
#define	trace   while(0) std::cerr

Typedefs
typedef std::map< GSDD, DataSet * >	GSDD_DataSet_map
typedef Cache< GShom, GSDD, GSDD >	ShomCache
typedef Cache< GShom, GSDD, GSDD, char >	ImgShomCache
typedef ext_hash_map< d3::set< GShom >::type, const _GShom * >::internal_hash_map	addCache_t

Functions
bool	sns::testWasInterrupt (bool can_garbage, const GSDD &d1, const GSDD &d2)
bool	sns::testShouldInterrupt (bool can_garbage, const GSDD &d1, const GSDD &d2)
const _GShom *	sns::getIdentity ()
GShom	sns::recFireSat (const GShom &sat, const GShom &lf)
static bool	notInRange (const GShom::range_t &h1r, const GShom &h2)
GShom	fixpoint (const GShom &h, bool is_top_level)
	Apply a homomorphism until fixpoint is reached. More...
GShom	localApply (const GHom &h, int target)
	Apply a homomorphism on a target variable. More...
GShom	localApply (const GShom &h, int target)
static void	addParameter (const GShom &hh, std::map< int, GHom > &local_homs, std::map< int, GShom > &local_shoms, d3::set< GShom >::type &parameters, bool &have_id)
static void	buildUnionParameters (d3::set< GShom >::type &p, d3::set< GShom >::type &parameters, bool &have_id)
static bool	commutative (const GShom &h1, const GShom &h2)
static void	addCompositionParameter (const GShom &h, sns::And::parameters_t &args)
GShom	operator& (const GShom &h1, const GShom &h2)
	Composition by circ (rond) of homomorphisms. More...
GShom	operator+ (const GShom &h1, const GShom &h2)
	Composition by union of two homomorphisms. More...
GShom	operator* (const GSDD &d, const GShom &h)
	Intersection with a constant SDD. More...
GShom	operator* (const GShom &h, const GSDD &d)
	Intersection with a constant SDD. More...
GShom	operator^ (const GSDD &d, const GShom &h)
	Left Concatenation of a constant SDD. More...
GShom	operator^ (const GShom &h, const GSDD &d)
	Right Concatenation of a constant SDD. More...
GShom	operator- (const GShom &h, const GSDD &d)
	Set difference. More...
GShom	operator- (const GShom &h1, const GShom &h2)
	Set difference (generalized). More...
static void	printCondError (const GShom &cond)
	An IF-THEN-ELSE construct. 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	apply2k (const GSDD &d)
	Apply a 2 level DDD representing a transition relation to current variable. More...
GShom	extractPotential (int var)
	Extract the domain of a given variable. More...
GShom	operator* (const GShom &h, const GShom &cond)
	Intersection with a selector Hom. More...
std::ostream &	operator<< (std::ostream &os, const GShom &h)

Variables
static ShomCache	sns::cache
static ImgShomCache	sns::imgcache
static addCache_t	addCache

Macro Definition Documentation

trace

#define trace   while(0) std::cerr

Typedef Documentation

addCache_t

typedef ext_hash_map<d3::set<GShom>::type, const _GShom*>::internal_hash_map addCache_t

GSDD_DataSet_map

typedef std::map<GSDD, DataSet*> GSDD_DataSet_map

ImgShomCache

typedef Cache<GShom, GSDD, GSDD, char> ImgShomCache

ShomCache

typedef Cache<GShom, GSDD, GSDD> ShomCache

Function Documentation

addCompositionParameter()

static void addCompositionParameter ( const GShom &  h, sns::And::parameters_t &  args  )

static

References commutative(), _GShom::get_concret(), and localApply().

addParameter()

static void addParameter ( const GShom &  hh, std::map< int, GHom > &  local_homs, std::map< int, GShom > &  local_shoms, d3::set< GShom >::type &  parameters, bool &  have_id  )

static

References _GShom::get_concret(), sns::LocalApply::h, sns::SLocalApply::h, sns::LocalApply::target, and sns::SLocalApply::target.

Referenced by buildUnionParameters().

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

buildUnionParameters()

static void buildUnionParameters ( d3::set< GShom >::type &  p, d3::set< GShom >::type &  parameters, bool &  have_id  )

static

References addParameter(), _GShom::get_concret(), GHom::id, GShom::id, and localApply().

commutative()

static bool commutative ( const GShom &  h1, const GShom &  h2  )

static

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

Referenced by addCompositionParameter().

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
	)

notInRange()

static bool notInRange ( const GShom::range_t &  h1r, const GShom &  h2  )

static

References GShom::get_range().

Referenced by commutative().

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

std::ostream& operator<<	(	std::ostream &	os,
		const GShom &	h
	)

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

printCondError()

static void printCondError ( const GShom &  cond )

static

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

Referenced by ITE(), operator!(), and operator*().

Variable Documentation

addCache

addCache_t addCache

static

Referenced by GShom::garbage().