Implements liberal safety extensible by LiberalSafetyPlugin. More...

#include <include/dlvhex2/LiberalSafetyChecker.h>

Collaboration diagram for LiberalSafetyChecker:

Data Structures
struct	Attribute
	Stores an ordinary or external (input or output) attribute. More...
struct	NodeInfoTag
struct	NodeMappingInfo
	See boost::graph. More...
Public Types
typedef boost::adjacency_list < boost::setS, boost::vecS, boost::bidirectionalS, Attribute >	Graph
typedef boost::graph_traits < Graph >	Traits
typedef Graph::vertex_descriptor	Node
typedef Graph::edge_descriptor	Dependency
typedef Traits::vertex_iterator	NodeIterator
typedef Traits::edge_iterator	DependencyIterator
typedef Traits::out_edge_iterator	PredecessorIterator
typedef Traits::in_edge_iterator	SuccessorIterator
typedef std::pair< ID, ID >	VariableLocation
typedef std::pair< ID, ID >	AtomLocation
Public Member Functions
Attribute	getAttribute (ID eatomID, ID predicate, std::vector< ID > inputList, ID ruleID, bool inputAttribute, int argumentIndex)
	Constructs an external attribute.
Attribute	getAttribute (ID predicate, int argumentIndex)
	Constructs an ordinary attribute.
void	addExternallyBoundedVariable (ID extAtom, VariableLocation vl)
	Called for adding variables bounded by external atoms.
void	addBoundedVariable (VariableLocation vl)
	Called after a new variable has become bounded to trigger further actions.
void	addDomainExpansionSafeAttribute (Attribute at)
	Called after an attribute has become safe to trigger further actions.
const std::vector< ID > &	getIdb ()
	Retrieves the IDB for which the checker was instantiated.
const Graph &	getAttributeGraph ()
	Retrieves the internal attribute dependency graph.
const std::vector< std::vector < Attribute > > &	getDepSCC ()
	Retrieves the strongly connected components of the internal attribute dependency graph.
const boost::unordered_set < Attribute > &	getDomainExpansionSafeAttributes ()
	Retrieves the attributes which are liberally domain-expansion safe.
const boost::unordered_set < VariableLocation > &	getBoundedVariables ()
	Retrieves the set of variables which have been shown to be bounded.
void	getReachableAttributes (Attribute start, std::set< Node > &output)
int	getPredicateArity (ID predicate) const
	Retrieves the arity of an ordinary predicate.
	LiberalSafetyChecker (RegistryPtr reg, const std::vector< ID > &idb, std::vector< LiberalSafetyPluginFactoryPtr > customSafetyPlugins)
	Constructor.
bool	isDomainExpansionSafe () const
	Checks if the program is liberally domain-expansion safe.
bool	isExternalAtomNecessaryForDomainExpansionSafety (ID eatomID) const
	Checks if a given external atom is necessary for establishing liberal domain-expansion safety.
virtual void	writeGraphViz (std::ostream &o, bool verbose) const
	Output the attribute dependency graph as graphviz source (dot file).
Data Fields
RegistryPtr	reg
	Registry.
const std::vector< ID > &	idb
	IDB of the program.
Private Types
typedef boost::multi_index_container < NodeMappingInfo, boost::multi_index::indexed_by < boost::multi_index::hashed_unique < boost::multi_index::tag < NodeInfoTag >, > > >	NodeMapping
typedef NodeMapping::index < NodeInfoTag >::type	NodeNodeInfoIndex
typedef std::pair< std::set < VariableLocation > , boost::unordered_set < Attribute > >	SafetyPreconditions
	Stores which variables still need to be bounded.
Private Member Functions
Node	getNode (Attribute at)
	Retrieves the internal node from the attribute dependency graph corresponding to an attribute.
bool	hasInformationFlow (boost::unordered_map< ID, boost::unordered_set< ID > > &builtinflow, ID from, ID to)
	Checks if there is flow of information from one builtin atom to another.
bool	isNewlySafe (Attribute at)
	Checks if `at` has recently been declared safe.
void	computeBuiltinInformationFlow (const Rule &rule, boost::unordered_map< ID, boost::unordered_set< ID > > &builtinflow)
	Computes for a given rule the information exchange between variables through builtins.
void	createDependencyGraph ()
	Create dependency graph of ordinary and external predicates.
void	createPreconditionsAndLocationIndices ()
	The indices stored in the class members.
void	computeCyclicAttributes ()
	Compute attributes which occur in or depend on cycles.
void	ensureOrdinarySafety ()
	Restricts the optimization of necessary to keep ordinary safety.
void	computeDomainExpansionSafety ()
	Calls the previous methods until no more safe attributes can be derived.
Private Attributes
Graph	ag
	Attribute graph.
boost::unordered_map< ID, std::vector< Attribute > >	attributesOfPredicate
	Stores for each ordinary predicate its attributes.
NodeMapping	nm
	See boost::graph.
std::vector< std::vector < Attribute > >	depSCC
	Strongly connected components in LiberalSafetyChecker::ag.
boost::unordered_map < Attribute, SafetyPreconditions >	safetyPreconditions
	Stores for each attributes the preconditios for becoming safe.
boost::unordered_map < VariableLocation, boost::unordered_set < Attribute > >	attributesSafeByVariable
	Stores for each variable the attributes whose safety depends on this variable.
boost::unordered_map < Attribute, boost::unordered_set < Attribute > >	attributesSafeByAttribute
	Stores for each attribute the attributes whose safety depends on this attribute.
boost::unordered_map < Attribute, std::set < AtomLocation > >	attributeOccursIn
	Stores for each attribute the atoms where it occurs.
boost::unordered_map < VariableLocation, std::set < AtomLocation > >	variableOccursIn
	Stores for each variable the atoms where it occurs.
boost::unordered_map< ID, int >	predicateArity
	Arity of a given (ordinary) predciate.
std::set< Node >	cyclicAttributes
	Stores all attributes which occur in cycles.
boost::unordered_set < VariableLocation >	boundedVariables
	Currently bounded variables.
boost::unordered_set< Attribute >	domainExpansionSafeAttributes
	Current domain-expansion safe attributes.
boost::unordered_set< IDAddress >	necessaryExternalAtoms
	External atoms which are necessary to establish domain-expansion safety.
boost::unordered_set < std::pair< ID, VariableLocation > >	boundedByExternals
	Variables bounded by externals, but not (yet) by ordinary atoms.
std::vector < LiberalSafetyPluginPtr >	safetyPlugins
	List of loaded LiberalSafetyPlugins.

Detailed Description

Implements liberal safety extensible by LiberalSafetyPlugin.

Definition at line 94 of file LiberalSafetyChecker.h.

Member Typedef Documentation

typedef std::pair<ID, ID> LiberalSafetyChecker::AtomLocation

Definition at line 152 of file LiberalSafetyChecker.h.

typedef Graph::edge_descriptor LiberalSafetyChecker::Dependency

Definition at line 143 of file LiberalSafetyChecker.h.

typedef Traits::edge_iterator LiberalSafetyChecker::DependencyIterator

Definition at line 145 of file LiberalSafetyChecker.h.

typedef boost::adjacency_list<boost::setS, boost::vecS, boost::bidirectionalS, Attribute > LiberalSafetyChecker::Graph

Definition at line 139 of file LiberalSafetyChecker.h.

typedef Graph::vertex_descriptor LiberalSafetyChecker::Node

Definition at line 142 of file LiberalSafetyChecker.h.

typedef Traits::vertex_iterator LiberalSafetyChecker::NodeIterator

Definition at line 144 of file LiberalSafetyChecker.h.

typedef boost::multi_index_container< NodeMappingInfo, boost::multi_index::indexed_by< boost::multi_index::hashed_unique< boost::multi_index::tag<NodeInfoTag>, > > > LiberalSafetyChecker::NodeMapping [private]

Definition at line 180 of file LiberalSafetyChecker.h.

typedef NodeMapping::index<NodeInfoTag>::type LiberalSafetyChecker::NodeNodeInfoIndex [private]

Definition at line 183 of file LiberalSafetyChecker.h.

typedef Traits::out_edge_iterator LiberalSafetyChecker::PredecessorIterator

Definition at line 146 of file LiberalSafetyChecker.h.

typedef std::pair<std::set<VariableLocation>, boost::unordered_set<Attribute> > LiberalSafetyChecker::SafetyPreconditions [private]

Stores which variables still need to be bounded.

Also stores which attributes need to become safe in order to make another attribute safe.

Definition at line 191 of file LiberalSafetyChecker.h.

typedef Traits::in_edge_iterator LiberalSafetyChecker::SuccessorIterator

Definition at line 147 of file LiberalSafetyChecker.h.

typedef boost::graph_traits<Graph> LiberalSafetyChecker::Traits

Definition at line 140 of file LiberalSafetyChecker.h.

typedef std::pair<ID, ID> LiberalSafetyChecker::VariableLocation

Definition at line 150 of file LiberalSafetyChecker.h.

Constructor & Destructor Documentation

LiberalSafetyChecker::LiberalSafetyChecker	(	RegistryPtr	reg,
		const std::vector< ID > &	idb,
		std::vector< LiberalSafetyPluginFactoryPtr >	customSafetyPlugins
	)

Constructor.

Parameters:

reg	See LiberalSafetyChecker::reg.
idb	See LiberalSafetyChecker::idb.
customSafetyPlugins	See LiberalSafetyChecker::safetyPlugins.

Definition at line 1108 of file LiberalSafetyChecker.cpp.

References computeDomainExpansionSafety(), createDependencyGraph(), createPreconditionsAndLocationIndices(), cyclicAttributes, and safetyPlugins.

Member Function Documentation

void LiberalSafetyChecker::addBoundedVariable ( VariableLocation vl )

Called after a new variable has become bounded to trigger further actions.

Definition at line 472 of file LiberalSafetyChecker.cpp.

References addDomainExpansionSafeAttribute(), addExternallyBoundedVariable(), attributesSafeByVariable, boundedVariables, DBGLOG, domainExpansionSafeAttributes, getAttribute(), ExternalAtom::getExtSourceProperties(), ExtSourceProperties::hasFiniteFiber(), ExternalAtom::inputs, isNewlySafe(), ExternalAtom::predicate, RawPrinter::print(), reg, safetyPreconditions, ID::TERM_BUILTIN_EQ, Atom::tuple, and variableOccursIn.

Referenced by addDomainExpansionSafeAttribute(), and computeDomainExpansionSafety().

void LiberalSafetyChecker::addDomainExpansionSafeAttribute ( Attribute at )

Called after an attribute has become safe to trigger further actions.

Definition at line 560 of file LiberalSafetyChecker.cpp.

References addBoundedVariable(), addExternallyBoundedVariable(), attributeOccursIn, attributesSafeByAttribute, DBGLOG, domainExpansionSafeAttributes, getAttribute(), ExternalAtom::inputs, isNewlySafe(), ExternalAtom::predicate, reg, safetyPreconditions, and Atom::tuple.

Referenced by addBoundedVariable().

void LiberalSafetyChecker::addExternallyBoundedVariable	(	ID	extAtom,
		VariableLocation	vl
	)

Called for adding variables bounded by external atoms.

Definition at line 466 of file LiberalSafetyChecker.cpp.

References boundedByExternals.

Referenced by addBoundedVariable(), and addDomainExpansionSafeAttribute().

void LiberalSafetyChecker::computeBuiltinInformationFlow	(	const Rule &	rule,
		boost::unordered_map< ID, boost::unordered_set< ID > > &	builtinflow
	)		`[private]`

Computes for a given rule the information exchange between variables through builtins.

Parameters:

rule	Rule to compute the information for.
builtinflow	See LiberalSafetyChecker::hasInformationFlow.

Definition at line 660 of file LiberalSafetyChecker.cpp.

References Rule::body, DBGLOG, ID::isBuiltinAtom(), ID::isNaf(), reg, ID::TERM_BUILTIN_ADD, ID::TERM_BUILTIN_DIV, ID::TERM_BUILTIN_EQ, ID::TERM_BUILTIN_MOD, ID::TERM_BUILTIN_MUL, ID::TERM_BUILTIN_SUB, ID::TERM_BUILTIN_SUCC, and Atom::tuple.

Referenced by createDependencyGraph().

void LiberalSafetyChecker::computeCyclicAttributes ( ) [private]

Compute attributes which occur in or depend on cycles.

Definition at line 930 of file LiberalSafetyChecker.cpp.

References ag, cyclicAttributes, DBGLOG, depSCC, domainExpansionSafeAttributes, LiberalSafetyChecker::Attribute::External, LiberalSafetyChecker::Attribute::input, nm, LiberalSafetyChecker::Attribute::predicate, and LiberalSafetyChecker::Attribute::type.

void LiberalSafetyChecker::computeDomainExpansionSafety ( ) [private]

Calls the previous methods until no more safe attributes can be derived.

Definition at line 1050 of file LiberalSafetyChecker.cpp.

References addBoundedVariable(), ID::address, ag, boundedByExternals, boundedVariables, DBGLOG, domainExpansionSafeAttributes, ensureOrdinarySafety(), isDomainExpansionSafe(), necessaryExternalAtoms, and safetyPlugins.

Referenced by LiberalSafetyChecker().

void LiberalSafetyChecker::createDependencyGraph ( ) [private]

Create dependency graph of ordinary and external predicates.

Definition at line 691 of file LiberalSafetyChecker.cpp.

References ag, attributesOfPredicate, Rule::body, computeBuiltinInformationFlow(), DBGLOG, depSCC, getAttribute(), PluginAtom::getInputType(), getNode(), hasInformationFlow(), Rule::head, idb, ExternalAtom::inputs, ID::isExternalAtom(), ID::isNaf(), ID::isOrdinaryAtom(), ExternalAtom::pluginAtom, ExternalAtom::predicate, PluginAtom::PREDICATE, reg, and Atom::tuple.

Referenced by LiberalSafetyChecker().

void LiberalSafetyChecker::createPreconditionsAndLocationIndices ( ) [private]

The indices stored in the class members.

Definition at line 846 of file LiberalSafetyChecker.cpp.

References attributeOccursIn, attributesSafeByAttribute, attributesSafeByVariable, Rule::body, getAttribute(), PluginAtom::getInputType(), Rule::head, idb, ExternalAtom::inputs, ID::isBuiltinAtom(), ID::isExternalAtom(), ID::isNaf(), ID::isOrdinaryAtom(), ExternalAtom::pluginAtom, ExternalAtom::predicate, PluginAtom::PREDICATE, predicateArity, reg, safetyPreconditions, Atom::tuple, and variableOccursIn.

Referenced by LiberalSafetyChecker().

void LiberalSafetyChecker::ensureOrdinarySafety ( ) [private]

Restricts the optimization of necessary to keep ordinary safety.

Definition at line 973 of file LiberalSafetyChecker.cpp.

References ID::address, Rule::body, SafetyChecker::checkSafety(), DBGLOG, Rule::head, Rule::headGuard, ID_FAIL(), ProgramCtx::idb, idb, ID::isExternalAtom(), ID::isNaf(), Rule::kind, necessaryExternalAtoms, reg, ProgramCtx::setupRegistry(), and Atom::tuple.

Referenced by computeDomainExpansionSafety().

LiberalSafetyChecker::Attribute LiberalSafetyChecker::getAttribute	(	ID	eatomID,
		ID	predicate,
		std::vector< ID >	inputList,
		ID	ruleID,
		bool	inputAttribute,
		int	argumentIndex
	)

Constructs an external attribute.

Parameters:

eatomID	External atom.
inputList	Input parameters.
ruleID	Rule where `eatomID` occurs.
inputAttribute	True to generate an input attribute and false to generate an output attribute.
argumentIndex	Index of the attribute in the input or output list, depending on `inputAttribute`.

Returns:: External input or output attribute.

Definition at line 402 of file LiberalSafetyChecker.cpp.

References LiberalSafetyChecker::Attribute::argIndex, LiberalSafetyChecker::Attribute::eatomID, LiberalSafetyChecker::Attribute::External, LiberalSafetyChecker::Attribute::input, LiberalSafetyChecker::Attribute::inputList, LiberalSafetyChecker::Attribute::predicate, LiberalSafetyChecker::Attribute::reg, reg, LiberalSafetyChecker::Attribute::ruleID, and LiberalSafetyChecker::Attribute::type.

Referenced by addBoundedVariable(), addDomainExpansionSafeAttribute(), createDependencyGraph(), and createPreconditionsAndLocationIndices().

LiberalSafetyChecker::Attribute LiberalSafetyChecker::getAttribute	(	ID	predicate,
		int	argumentIndex
	)

Constructs an ordinary attribute.

Parameters:

predicate	Predicate ID.
argumentIndex	Argument position of `predicate`.

Returns:: Ordinary attribute.

Definition at line 418 of file LiberalSafetyChecker.cpp.

References LiberalSafetyChecker::Attribute::argIndex, LiberalSafetyChecker::Attribute::eatomID, ID_FAIL(), LiberalSafetyChecker::Attribute::input, LiberalSafetyChecker::Attribute::Ordinary, LiberalSafetyChecker::Attribute::predicate, predicateArity, LiberalSafetyChecker::Attribute::reg, reg, LiberalSafetyChecker::Attribute::ruleID, and LiberalSafetyChecker::Attribute::type.

const LiberalSafetyChecker::Graph & LiberalSafetyChecker::getAttributeGraph ( )

Retrieves the internal attribute dependency graph.

Returns:: Attribute dependency graph.

Definition at line 616 of file LiberalSafetyChecker.cpp.

References ag.

const boost::unordered_set< LiberalSafetyChecker::VariableLocation > & LiberalSafetyChecker::getBoundedVariables ( )

Retrieves the set of variables which have been shown to be bounded.

Returns:: Set of variables consisting of the rule ID and the variable term.

Definition at line 634 of file LiberalSafetyChecker.cpp.

References boundedVariables.

const std::vector< std::vector< LiberalSafetyChecker::Attribute > > & LiberalSafetyChecker::getDepSCC ( )

Retrieves the strongly connected components of the internal attribute dependency graph.

Returns:: Strongly connected components of the attribute dependency graph.

Definition at line 622 of file LiberalSafetyChecker.cpp.

References depSCC.

const boost::unordered_set< LiberalSafetyChecker::Attribute > & LiberalSafetyChecker::getDomainExpansionSafeAttributes ( )

Retrieves the attributes which are liberally domain-expansion safe.

Returns:: Set of attributes.

Definition at line 628 of file LiberalSafetyChecker.cpp.

References domainExpansionSafeAttributes.

const std::vector< ID > & LiberalSafetyChecker::getIdb ( )

Retrieves the IDB for which the checker was instantiated.

Returns:: IDB.

Definition at line 610 of file LiberalSafetyChecker.cpp.

References idb.

LiberalSafetyChecker::Node LiberalSafetyChecker::getNode ( Attribute at ) [private]

Retrieves the internal node from the attribute dependency graph corresponding to an attribute.

Parameters:

at	Attribute.

Returns:: Node.

Definition at line 434 of file LiberalSafetyChecker.cpp.

References ag, attributesOfPredicate, nm, LiberalSafetyChecker::Attribute::Ordinary, LiberalSafetyChecker::Attribute::predicate, and LiberalSafetyChecker::Attribute::type.

Referenced by createDependencyGraph().

int LiberalSafetyChecker::getPredicateArity ( ID predicate ) const

Retrieves the arity of an ordinary predicate.

Parameters:

predicate Ordinary predicate.

Returns:: Arity of predicate.

Definition at line 654 of file LiberalSafetyChecker.cpp.

References predicateArity.

void LiberalSafetyChecker::getReachableAttributes	(	Attribute	start,
		std::set< Node > &	output
	)

Definition at line 640 of file LiberalSafetyChecker.cpp.

References ag, and nm.

bool LiberalSafetyChecker::hasInformationFlow	(	boost::unordered_map< ID, boost::unordered_set< ID > > &	builtinflow,
		ID	from,
		ID	to
	)		`[private]`

Checks if there is flow of information from one builtin atom to another.

Parameters:

builtinflow	Detected information flow.
from	First builtin.
to	Second builtin.

Returns:: True if information flows from from to to, and false otherwise.

Definition at line 454 of file LiberalSafetyChecker.cpp.

Referenced by createDependencyGraph().

bool LiberalSafetyChecker::isDomainExpansionSafe ( ) const

Checks if the program is liberally domain-expansion safe.

Returns:: True if the program is liberally domain-expansion safe and false otherwise.

Definition at line 1122 of file LiberalSafetyChecker.cpp.

References ag, and domainExpansionSafeAttributes.

Referenced by computeDomainExpansionSafety(), and isExternalAtomNecessaryForDomainExpansionSafety().

bool LiberalSafetyChecker::isExternalAtomNecessaryForDomainExpansionSafety ( ID eatomID ) const

Checks if a given external atom is necessary for establishing liberal domain-expansion safety.

Parameters:

eaomID The external atom whose relevance shall be checked.

Returns:: True if eatomID is necessary for establishing liberal domain-expansion safety and false otherwise.

Definition at line 1128 of file LiberalSafetyChecker.cpp.

References ID::address, isDomainExpansionSafe(), and necessaryExternalAtoms.

bool LiberalSafetyChecker::isNewlySafe ( Attribute at ) [private]

Checks if at has recently been declared safe.

Parameters:

at	Attribute to check.

Returns:: True if at has recently been declared safe and false otherwise.

Definition at line 460 of file LiberalSafetyChecker.cpp.

References safetyPreconditions.

Referenced by addBoundedVariable(), and addDomainExpansionSafeAttribute().

void LiberalSafetyChecker::writeGraphViz	(	std::ostream &	o,
		bool	verbose
	)		const `[virtual]`

Output the attribute dependency graph as graphviz source (dot file).

Parameters:

o	Stream to write the graph to.
verbose	True to include more detailed information.

Definition at line 1145 of file LiberalSafetyChecker.cpp.

References ag, cyclicAttributes, DBGLOG, domainExpansionSafeAttributes, graphviz::escape(), LiberalSafetyChecker::Attribute::External, and necessaryExternalAtoms.

Field Documentation

Graph LiberalSafetyChecker::ag [private]

Attribute graph.

Definition at line 161 of file LiberalSafetyChecker.h.

Referenced by computeCyclicAttributes(), computeDomainExpansionSafety(), createDependencyGraph(), getAttributeGraph(), getNode(), getReachableAttributes(), isDomainExpansionSafe(), and writeGraphViz().

boost::unordered_map<Attribute, std::set<AtomLocation> > LiberalSafetyChecker::attributeOccursIn [private]

Stores for each attribute the atoms where it occurs.

Definition at line 202 of file LiberalSafetyChecker.h.

Referenced by addDomainExpansionSafeAttribute(), and createPreconditionsAndLocationIndices().

boost::unordered_map<ID, std::vector<Attribute> > LiberalSafetyChecker::attributesOfPredicate [private]

Stores for each ordinary predicate its attributes.

Definition at line 163 of file LiberalSafetyChecker.h.

Referenced by createDependencyGraph(), and getNode().

boost::unordered_map<Attribute, boost::unordered_set<Attribute> > LiberalSafetyChecker::attributesSafeByAttribute [private]

Stores for each attribute the attributes whose safety depends on this attribute.

Definition at line 199 of file LiberalSafetyChecker.h.

Referenced by addDomainExpansionSafeAttribute(), and createPreconditionsAndLocationIndices().

boost::unordered_map<VariableLocation, boost::unordered_set<Attribute> > LiberalSafetyChecker::attributesSafeByVariable [private]

Stores for each variable the attributes whose safety depends on this variable.

Definition at line 197 of file LiberalSafetyChecker.h.

Referenced by addBoundedVariable(), and createPreconditionsAndLocationIndices().

boost::unordered_set<std::pair<ID, VariableLocation> > LiberalSafetyChecker::boundedByExternals [private]

Variables bounded by externals, but not (yet) by ordinary atoms.

Definition at line 218 of file LiberalSafetyChecker.h.

Referenced by addExternallyBoundedVariable(), and computeDomainExpansionSafety().

boost::unordered_set<VariableLocation> LiberalSafetyChecker::boundedVariables [private]

Currently bounded variables.

Definition at line 212 of file LiberalSafetyChecker.h.

Referenced by addBoundedVariable(), computeDomainExpansionSafety(), and getBoundedVariables().

std::set<Node> LiberalSafetyChecker::cyclicAttributes [private]

Stores all attributes which occur in cycles.

Definition at line 210 of file LiberalSafetyChecker.h.

Referenced by computeCyclicAttributes(), LiberalSafetyChecker(), and writeGraphViz().

std::vector<std::vector<Attribute> > LiberalSafetyChecker::depSCC [private]

Strongly connected components in LiberalSafetyChecker::ag.

Definition at line 185 of file LiberalSafetyChecker.h.

Referenced by computeCyclicAttributes(), createDependencyGraph(), and getDepSCC().

boost::unordered_set<Attribute> LiberalSafetyChecker::domainExpansionSafeAttributes [private]

Current domain-expansion safe attributes.

Definition at line 214 of file LiberalSafetyChecker.h.

Referenced by addBoundedVariable(), addDomainExpansionSafeAttribute(), computeCyclicAttributes(), computeDomainExpansionSafety(), getDomainExpansionSafeAttributes(), isDomainExpansionSafe(), and writeGraphViz().

const std::vector<ID>& LiberalSafetyChecker::idb

IDB of the program.

Definition at line 157 of file LiberalSafetyChecker.h.

Referenced by createDependencyGraph(), createPreconditionsAndLocationIndices(), ensureOrdinarySafety(), and getIdb().

boost::unordered_set<IDAddress> LiberalSafetyChecker::necessaryExternalAtoms [private]

External atoms which are necessary to establish domain-expansion safety.

Definition at line 216 of file LiberalSafetyChecker.h.

Referenced by computeDomainExpansionSafety(), ensureOrdinarySafety(), isExternalAtomNecessaryForDomainExpansionSafety(), and writeGraphViz().

NodeMapping LiberalSafetyChecker::nm [private]

See boost::graph.

Definition at line 182 of file LiberalSafetyChecker.h.

Referenced by computeCyclicAttributes(), getNode(), and getReachableAttributes().

boost::unordered_map<ID, int> LiberalSafetyChecker::predicateArity [private]

Arity of a given (ordinary) predciate.

Definition at line 208 of file LiberalSafetyChecker.h.

Referenced by createPreconditionsAndLocationIndices(), getAttribute(), and getPredicateArity().

RegistryPtr LiberalSafetyChecker::reg

Registry.

Definition at line 155 of file LiberalSafetyChecker.h.

Referenced by addBoundedVariable(), addDomainExpansionSafeAttribute(), computeBuiltinInformationFlow(), createDependencyGraph(), createPreconditionsAndLocationIndices(), ensureOrdinarySafety(), getAttribute(), and LiberalSafetyChecker::Attribute::print().

std::vector<LiberalSafetyPluginPtr> LiberalSafetyChecker::safetyPlugins [private]

List of loaded LiberalSafetyPlugins.

Definition at line 305 of file LiberalSafetyChecker.h.

Referenced by computeDomainExpansionSafety(), and LiberalSafetyChecker().

boost::unordered_map<Attribute, SafetyPreconditions> LiberalSafetyChecker::safetyPreconditions [private]

Stores for each attributes the preconditios for becoming safe.

Definition at line 194 of file LiberalSafetyChecker.h.

Referenced by addBoundedVariable(), addDomainExpansionSafeAttribute(), createPreconditionsAndLocationIndices(), and isNewlySafe().

boost::unordered_map<VariableLocation, std::set<AtomLocation> > LiberalSafetyChecker::variableOccursIn [private]

Stores for each variable the atoms where it occurs.

Definition at line 204 of file LiberalSafetyChecker.h.

Referenced by addBoundedVariable(), and createPreconditionsAndLocationIndices().

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

include/dlvhex2/LiberalSafetyChecker.h
src/LiberalSafetyChecker.cpp

Data Structures

Public Types

Public Member Functions

Data Fields

Private Types

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Field Documentation