Hom.cpp File Reference

#include <typeinfo>
#include <iostream>
#include <cassert>
#include <map>
#include <algorithm>
#include "ddd/util/set.hh"
#include "ddd/Hom.h"
#include "ddd/DDD.h"
#include "ddd/DED.h"
#include "ddd/UniqueTable.h"
#include "ddd/MLHom.h"
#include "ddd/util/hash_support.hh"
#include "ddd/util/configuration.hh"
#include "ddd/Cache.hh"
#include "ddd/MemoryManager.h"
#include "ddd/FixObserver.hh"

Include dependency graph for Hom.cpp:

Classes
struct	d3::util::equal< _GHom * >
class	Identity
class	Constant
class	Apply2k
class	DomExtract
	Extractor of variable domains for invert computations. More...
class	Mult
class	Inter
class	NotCond
class	Add
class	Monotonic
class	Compose
class	And
	A commutative composition of n homomorphisms. More...
class	LeftConcat
class	RightConcat
class	Minus
class	Fixpoint
class	MLHomAdapter

Namespaces
	d3
	d3::util

Typedefs
typedef Cache< GHom, GDDD, GDDD >	HomCache
typedef Cache< GHom, GDDD, GDDD, char >	ImgHomCache

Functions
bool	testWasInterrupt (bool can_garbage, const GDDD &d1, const GDDD &d2)
bool	testShouldInterrupt (bool can_garbage, const GDDD &d1, const GDDD &d2)
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. More...
static bool	notInRange (const GHom::range_t &h1r, const GHom &h2)
bool	commutative (const GHom &h1, const GHom &h2)
	return true if the provided operations are commutative More...
GHom	fixpoint (const GHom &h, bool is_top_level)
	Apply a homomorphism until fixpoint is reached. More...
GHom	monotonic (const d3::set< GHom >::type &set)
static void	printCondError (const GHom &cond)
GHom	ITE (const GHom &cond, const GHom &iftrue, const GHom &iffalse)
	An IF-THEN-ELSE construct. More...
GHom	operator! (const GHom &cond)
	A negation/complement constructor for selector homomophisms. More...
static void	addCompositionParameter (const GHom &h, And::parameters_t &args)
GHom	operator& (const GHom &h1, const GHom &h2)
	Composition by circ (rond) of homomorphisms. More...
GHom	operator+ (const GHom &h1, const GHom &h2)
	Composition by union of two homomorphisms. More...
GHom	operator* (const GDDD &d, const GHom &h)
	Intersection with a constant DDD. More...
GHom	operator* (const GHom &h, const GDDD &d)
	Intersection with a constant SDD. More...
GHom	operator* (const GHom &h, const GHom &cond)
	Intersection with a selector Hom. More...
GHom	operator^ (const GDDD &d, const GHom &h)
	Left Concatenation of a constant SDD. More...
GHom	operator^ (const GHom &h, const GDDD &d)
	Right Concatenation of a constant SDD. More...
GHom	operator- (const GHom &h, const GDDD &d)
	Set difference. More...
GHom	apply2k (const GDDD &d)
	Apply a 2 level DDD representing a transition relation to current variable. More...
std::ostream &	operator<< (std::ostream &os, const GHom &h)

Variables
static UniqueTable< _GHom >	canonical
static HomCache	cache
static ImgHomCache	imgcache

Typedef Documentation

HomCache

typedef Cache<GHom,GDDD,GDDD> HomCache

ImgHomCache

typedef Cache<GHom,GDDD,GDDD,char> ImgHomCache

Function Documentation

addCompositionParameter()

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

static

References commutative(), and _GHom::get_concret().

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.

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

monotonic()

GHom monotonic

(

const d3::set< GHom >::type &

set

)

Similar to the fixpoint, but we suppose here that the parameters are commutative And that any application order converges to the same result Typically this is the property of a base of monotonic< permutations.

Referenced by Monotonic::skip_variable().

notInRange()

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

static

References GHom::get_range().

Referenced by commutative().

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.

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

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

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

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.

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

operator<<()

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

operator^() [1/2]

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

Left Concatenation of a constant SDD.

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

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

printCondError()

static void printCondError ( const GHom &  cond )

static

Referenced by ITE().

testShouldInterrupt()

bool testShouldInterrupt	(	bool	can_garbage,
		const GDDD &	d1,
		const GDDD &	d2
	)

Referenced by Fixpoint::eval().

testWasInterrupt()

bool testWasInterrupt	(	bool	can_garbage,
		const GDDD &	d1,
		const GDDD &	d2
	)

References fobs::get_fixobserver(), fobs::FixObserver::should_interrupt(), and fobs::FixObserver::update().

Referenced by Fixpoint::eval().

Variable Documentation

cache

HomCache cache

static

Referenced by GHom::garbage(), GHom::operator()(), DED::pstats(), and GHom::pstats().

canonical

UniqueTable<_GHom> canonical

static

Referenced by GHom::add(), GHom::ccompose(), GHom::garbage(), GShom::garbage(), GShom::GShom(), GHom::pstats(), GShom::pstats(), GHom::statistics(), and GShom::statistics().

imgcache

ImgHomCache imgcache

static

Referenced by GHom::garbage(), and GHom::has_image().