Stores meta information about a ground program, including mappings of external atom auxiliaries to external atoms. More...

#include <include/dlvhex2/AnnotatedGroundProgram.h>

Collaboration diagram for AnnotatedGroundProgram:

[legend]

Data Structures
struct	ProgramComponent
	Stores a strongly connected component of the ground program according to its atom dependencies. More...
Public Types
typedef std::pair< IDAddress, std::vector< ID > >	AuxToExternalAtoms
Public Member Functions
	AnnotatedGroundProgram ()
	Constructor.
	AnnotatedGroundProgram (ProgramCtx &ctx, const OrdinaryASPProgram &groundProgram, std::vector< ID > indexedEatoms=std::vector< ID >(), std::vector< ID > dependencyIDB=std::vector< ID >())
	Analyzes a ground program and stored meta information.
	AnnotatedGroundProgram (ProgramCtx &ctx, std::vector< ID > indexedEatoms)
	Analyzes a ground program and stored meta information.
void	addProgram (const AnnotatedGroundProgram &other)
	Allows for incremental extension of a program.
const AnnotatedGroundProgram &	operator= (const AnnotatedGroundProgram &other)
	Assignment operator.
void	setIndexEAtoms (std::vector< ID > indexedEatoms)
	Set the external atoms to track.
bool	containsHeadCycles (ID ruleID) const
	Checks for a given rule if it has at least to cyclically depending atoms in its head.
int	getComponentCount () const
	Returns the number of components of this program.
const OrdinaryASPProgram &	getProgramOfComponent (int compNr) const
	Retrieves a component as OrdinaryASPProgram.
InterpretationConstPtr	getAtomsOfComponent (int compNr) const
	Returns the set of atoms of a component.
bool	hasHeadCycles (int compNr) const
	Checks a given component for head cycles.
bool	hasECycles (int compNr) const
	Checks a given component for cycles through external atoms.
bool	hasECycles (int compNr, InterpretationConstPtr intr) const
	Checks a given component for head cycles when the atom dependency graph is restricted to `intr`.
bool	hasHeadCycles () const
	Checks the program has head cycles.
bool	hasECycles () const
	Checks the program has cycles through external atoms.
bool	hasECycles (InterpretationConstPtr intr) const
	Checks thr program for cycles through external atoms when the atom dependency graph is restricted to `intr`.
bool	mapsAux (IDAddress ida) const
	Checks if `ida` is contained in the ground program and mapped back to an external atom in indexEAtoms.
const boost::unordered_map < IDAddress, std::vector< ID > > &	getAuxToEA () const
	Returns all pairs of external auxiliary atoms and their associated external atoms they stem from.
const std::vector< ID > &	getAuxToEA (IDAddress ida) const
	Returns for a given external auxiliary atom the associated external atoms it stem from.
const boost::shared_ptr < ExternalAtomMask >	getEAMask (int eaIndex) const
	Returns the the mask of a tracked external atom with a given index.
const OrdinaryASPProgram &	getGroundProgram () const
	Returns the (not annotated) underlying ground program.
const std::vector< ID > &	getIndexedEAtoms () const
	Returns the external atoms indexed by this AnnotatedGroundProgram.
ID	getIndexedEAtom (int index) const
	Returns a single external atom identified by its index.
int	getIndexOfEAtom (ID eatomID) const
	Returns the index of an external atom identified by its ID.
InterpretationConstPtr	getProgramMask () const
	Returns the mask of the overall program.
void	setCompleteSupportSetsForVerification (SimpleNogoodContainerPtr supportSets)
	Sets support sets for verification.
bool	allowsForVerificationUsingCompleteSupportSets () const
	Returns if complete support sets have been defined.
SimpleNogoodContainerPtr	getCompleteSupportSetsForVerification ()
	Returns the complete support sets added for verification.
bool	verifyExternalAtomsUsingCompleteSupportSets (int eaIndex, InterpretationConstPtr interpretation, InterpretationConstPtr auxiliariesToVerify) const
	Tries to verify an external atom which allows for verification using support sets and returns the result of this check.
Private Types
typedef ProgramComponent::Ptr	ProgramComponentPtr
typedef boost::adjacency_list < boost::vecS, boost::vecS, boost::bidirectionalS, IDAddress >	Graph
typedef Graph::vertex_descriptor	Node
Private Member Functions
void	createProgramMask ()
	Initializes programMask.
void	createEAMasks ()
	Initializes eaMasks.
void	mapAuxToEAtoms ()
	Initializes auxToEA.
void	initialize ()
	Calls all other initialization methods.
void	computeAtomDependencyGraph ()
	Creates depGraph.
void	computeAdditionalDependencies ()
	Adds dependencies defined via dependencyIDB (see constructor AnnotatedGroundProgram::AnnotatedGroundProgram).
void	computeStronglyConnectedComponents ()
	Computes strongly connected components in depSCC.
void	computeHeadCycles ()
	Analyzes all components and the overall program for head cycles.
void	computeECycles ()
	Analyzes all components and the overall program for cycles through external atoms.
Private Attributes
ProgramCtx *	ctx
	ProgramCtx.
RegistryPtr	reg
	Registry to be used for interpretation of IDs.
OrdinaryASPProgram	groundProgram
	Underlying ground program without annotations.
std::vector< ID >	dependencyIDB
	Subset of nonground rules used for computing additional dependencies (see constructor AnnotatedGroundProgram::AnnotatedGroundProgram).
bool	haveGrounding
	True if groundProgram is initialized, otherwise false (then we have only information about ground external atoms in the program but not about the entire program).
std::vector< ID >	indexedEatoms
	Set of external atoms in the original program whose ground instances shall be tracked.
std::vector< boost::shared_ptr < ExternalAtomMask > >	eaMasks
	Stores for each external atom in indexedEatoms its mask, i.e., set of ground atoms stemming from this external atom.
boost::unordered_map < IDAddress, std::vector< ID > >	auxToEA
	Stores for each external atom auxiliary in groundProgram the set of (nonground) external atoms it stems from (this external atom is in general not unique).
SimpleNogoodContainerPtr	supportSets
	Set of complete support sets for the external atoms in this ground program (can be used for compatibility checking without actual external calls).
InterpretationPtr	programMask
	Set of all atoms in the program.
boost::unordered_map < IDAddress, Node >	depNodes
	Stores for each ground atom IDAddress the according node in the atom dependency graph.
Graph	depGraph
	Atom dependency graph.
std::vector< std::set < IDAddress > >	depSCC
	Strongly connected components (of atoms) of depGraph.
boost::unordered_map < IDAddress, int >	componentOfAtom
	Stores for each ground atom the index of the component in depSCC where the atom is contained.
std::vector< std::pair < IDAddress, IDAddress > >	externalEdges
	Stores edges (a,b) between ground atoms a,b such that atom a externally depends on b.
std::vector< bool >	headCycles
	Stores for each component in depSCC whether it contains head cycles.
InterpretationPtr	headCyclicRules
	Stores the set of rules which contain at least two cyclically depending atoms in their heads.
std::vector< bool >	eCycles
	Stores for each component in depSCC whether it contains cycles through external atoms.
std::vector< ProgramComponentPtr >	programComponents
	Vector of all program components.
bool	headCyclesTotal
	Stores if the overall program contains head cycles.
bool	eCyclesTotal
	Stores if the overall program contains cycles through external atoms.

Detailed Description

Stores meta information about a ground program, including mappings of external atom auxiliaries to external atoms.

Definition at line 63 of file AnnotatedGroundProgram.h.

Member Typedef Documentation

typedef std::pair<IDAddress, std::vector<ID> > AnnotatedGroundProgram::AuxToExternalAtoms

Definition at line 274 of file AnnotatedGroundProgram.h.

typedef boost::adjacency_list<boost::vecS, boost::vecS, boost::bidirectionalS, IDAddress> AnnotatedGroundProgram::Graph [private]

Definition at line 108 of file AnnotatedGroundProgram.h.

typedef Graph::vertex_descriptor AnnotatedGroundProgram::Node [private]

Definition at line 109 of file AnnotatedGroundProgram.h.

typedef ProgramComponent::Ptr AnnotatedGroundProgram::ProgramComponentPtr [private]

Definition at line 107 of file AnnotatedGroundProgram.h.

Constructor & Destructor Documentation

DLVHEX_NAMESPACE_BEGIN AnnotatedGroundProgram::AnnotatedGroundProgram ( )

Constructor.

Definition at line 56 of file AnnotatedGroundProgram.cpp.

AnnotatedGroundProgram::AnnotatedGroundProgram	(	ProgramCtx &	ctx,
		const OrdinaryASPProgram &	groundProgram,
		std::vector< ID >	indexedEatoms = `std::vector<ID>()`,
		std::vector< ID >	dependencyIDB = `std::vector<ID>()`
	)

Analyzes a ground program and stored meta information.

Parameters:

ctx	ProgramCtx
groundProgram	The ground program to analyze
indexedEatoms	The set of relevant external atoms, i.e., the external atoms meta information shall be generated for
dependencyIDB	A (possibly nonground) IDB whose rules define possible additional dependencies if the set of facts is extended. The class will consider atoms as dependent if they might become dependent with future domain expansions. Thus allows for extended the AnnotatedGroundProgram without rearranging SCCs.

Example: The program p(1) v x. q(1) :- p(1). stemming from the nonground program p(1) v x. p(X) :- q(X), d(X). q(1) :- p(1). has the dependency q(1) -> p(1) (and thus might put p(1) and q(1) in different SCCs). But when the element d(1) is added, a newly added rule (p(1) :- q(1), d(1)) introduces the dependency { p(1) -> q(1) }. In contrast, the dependency x -> p(1) will never hold, even if the domain is expanded.

Definition at line 61 of file AnnotatedGroundProgram.cpp.

References initialize().

AnnotatedGroundProgram::AnnotatedGroundProgram	(	ProgramCtx &	ctx,
		std::vector< ID >	indexedEatoms
	)

Analyzes a ground program and stored meta information.

Parameters:

ctx	ProgramCtx
indexedEatoms	The set of relevant external atoms, i.e., the external atoms meta information shall be generated for

Definition at line 69 of file AnnotatedGroundProgram.cpp.

References initialize().

Member Function Documentation

void AnnotatedGroundProgram::addProgram ( const AnnotatedGroundProgram & other )

Allows for incremental extension of a program.

Note: This operation is only allowed if for all cyclically depending atoms a,b in the merged program, for each of the input programs either (i) The cyclic dependency of a and b is already contained in the input program; or (ii) None of the atoms a,b occurs in the input program. It is allowed that one of the input programs fulfills (i) and the other one (ii), but it is also allowed that they fulfill the same condition. Informally, the condition guarantees that no previously existing strongly connected components need no be merged, but the addition of a program only amounts to an extension of existing SCCs or the addition of new SCCs. If both input programs stem from the same nonground program (but with different domains of constants), then it can be guaranteed by passing the nonground program as parameter dependencyIDB to the constructor.

Parameters:

other The program to add.

Definition at line 79 of file AnnotatedGroundProgram.cpp.

References auxToEA, componentOfAtom, createEAMasks(), DBGLOG, depSCC, eaMasks, eCycles, eCyclesTotal, OrdinaryASPProgram::edb, groundProgram, haveGrounding, headCycles, headCyclesTotal, headCyclicRules, OrdinaryASPProgram::idb, indexedEatoms, OrdinaryASPProgram::mask, OrdinaryASPProgram::maxint, programComponents, programMask, reg, OrdinaryASPProgram::registry, and supportSets.

bool AnnotatedGroundProgram::allowsForVerificationUsingCompleteSupportSets ( ) const

Returns if complete support sets have been defined.

Returns:: True if complete support sets have been defined and false otherwise.

Definition at line 1150 of file AnnotatedGroundProgram.cpp.

References supportSets.

Referenced by UnfoundedSetChecker::isUnfoundedSet(), and GenuineGuessAndCheckModelGenerator::verifyExternalAtom().

void AnnotatedGroundProgram::computeAdditionalDependencies ( ) [private]

Adds dependencies defined via dependencyIDB (see constructor AnnotatedGroundProgram::AnnotatedGroundProgram).

Definition at line 479 of file AnnotatedGroundProgram.cpp.

References ID::atomFromLiteral(), Rule::body, ProgramCtx::config, ctx, DBGLOG, dependencyIDB, depGraph, depNodes, DLVHEX_BENCHMARK_REGISTER_AND_COUNT, OrdinaryASPProgram::edb, bm::bvector< Alloc >::end(), externalEdges, bm::bvector< Alloc >::first(), ExternalAtom::getExtSourceProperties(), PluginAtom::getInputType(), Configuration::getOption(), groundProgram, Rule::head, ExternalAtom::inputs, ExtSourceProperties::isAntimonotonic(), ID::isExternalAtom(), ExtSourceProperties::isMonotonic(), ID::isNaf(), ID::isOrdinaryAtom(), ID::isWeightRule(), ExternalAtom::pluginAtom, PluginAtom::PREDICATE, programMask, reg, Atom::tuple, OrdinaryAtom::unifiesWith(), and ExternalAtom::updatePredicateInputMask().

Referenced by initialize().

void AnnotatedGroundProgram::computeAtomDependencyGraph ( ) [private]

void AnnotatedGroundProgram::computeECycles ( ) [private]

Analyzes all components and the overall program for cycles through external atoms.

Definition at line 824 of file AnnotatedGroundProgram.cpp.

References componentOfAtom, ProgramCtx::config, ctx, DBGLOG, depGraph, depNodes, depSCC, eCycles, eCyclesTotal, externalEdges, Configuration::getOption(), programComponents, and reg.

Referenced by initialize().

void AnnotatedGroundProgram::computeHeadCycles ( ) [private]

Analyzes all components and the overall program for head cycles.

Definition at line 787 of file AnnotatedGroundProgram.cpp.

References ID::address, DBGLOG, depSCC, Rule::head, headCycles, headCyclesTotal, headCyclicRules, programComponents, and reg.

Referenced by initialize().

void AnnotatedGroundProgram::computeStronglyConnectedComponents ( ) [private]

Computes strongly connected components in depSCC.

Definition at line 715 of file AnnotatedGroundProgram.cpp.

References ID::address, componentOfAtom, DBGLOG, depGraph, depNodes, depSCC, OrdinaryASPProgram::edb, groundProgram, Rule::head, OrdinaryASPProgram::idb, RawPrinter::print(), programComponents, and reg.

Referenced by initialize().

bool AnnotatedGroundProgram::containsHeadCycles ( ID ruleID ) const

Checks for a given rule if it has at least to cyclically depending atoms in its head.

Parameters:

ruleID ID of a rule in this program.

Returns:: True if rule ruleID is involved in head cycles.

Definition at line 899 of file AnnotatedGroundProgram.cpp.

References ID::address, and headCyclicRules.

Referenced by UnfoundedSetCheckerManager::computeChoiceRuleCompatibilityForComponent().

void AnnotatedGroundProgram::createEAMasks ( ) [private]

Initializes eaMasks.

Definition at line 299 of file AnnotatedGroundProgram.cpp.

References ctx, eaMasks, groundProgram, OrdinaryASPProgram::idb, indexedEatoms, and reg.

Referenced by addProgram(), and initialize().

void AnnotatedGroundProgram::createProgramMask ( ) [private]

Initializes programMask.

Definition at line 285 of file AnnotatedGroundProgram.cpp.

References ID::address, Rule::body, OrdinaryASPProgram::edb, groundProgram, Rule::head, OrdinaryASPProgram::idb, ID::isExternalAuxiliary(), programMask, and reg.

Referenced by initialize().

InterpretationConstPtr AnnotatedGroundProgram::getAtomsOfComponent ( int compNr ) const

Returns the set of atoms of a component.

Parameters:

compNr A component index from 0 to getComponentCount()-1.

Returns:: Set of atoms.

Definition at line 918 of file AnnotatedGroundProgram.cpp.

References depSCC, and programComponents.

Referenced by UnfoundedSetCheckerManager::getUnfoundedSet(), and UnfoundedSetCheckerManager::initializeUnfoundedSetCheckers().

const boost::unordered_map< IDAddress, std::vector< ID > > & AnnotatedGroundProgram::getAuxToEA ( ) const

Returns all pairs of external auxiliary atoms and their associated external atoms they stem from.

Returns:: Pairs of external atom auxiliaries (IDAddress) and the set of external atoms (IDs) they stem from.

Definition at line 1091 of file AnnotatedGroundProgram.cpp.

References auxToEA.

Referenced by AssumptionBasedUnfoundedSetChecker::constructDomain(), EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemNecessaryPart(), GenuineGuessAndCheckModelGenerator::generalizeNogood(), UnfoundedSetChecker::getUFSNogoodUFSBased(), GenuineGuessAndCheckModelGenerator::inlineExternalAtoms(), GenuineGuessAndCheckModelGenerator::learnSupportSets(), and UnfoundedSetChecker::UnfoundedSetVerificationStatus::UnfoundedSetVerificationStatus().

const std::vector< ID > & AnnotatedGroundProgram::getAuxToEA ( IDAddress ida ) const

Returns for a given external auxiliary atom the associated external atoms it stem from.

Returns:: The set of external atoms (IDs) the auxiliary ida stems from.

Definition at line 1097 of file AnnotatedGroundProgram.cpp.

References auxToEA.

SimpleNogoodContainerPtr AnnotatedGroundProgram::getCompleteSupportSetsForVerification ( )

Returns the complete support sets added for verification.

Returns:: Support sets encoded as nogoods.

Definition at line 1156 of file AnnotatedGroundProgram.cpp.

References supportSets.

int AnnotatedGroundProgram::getComponentCount ( ) const

Returns the number of components of this program.

Returns:: Number of components of this program.

Definition at line 905 of file AnnotatedGroundProgram.cpp.

References programComponents.

Referenced by UnfoundedSetCheckerManager::computeChoiceRuleCompatibility(), UnfoundedSetCheckerManager::getUnfoundedSet(), and UnfoundedSetCheckerManager::initializeUnfoundedSetCheckers().

const boost::shared_ptr< ExternalAtomMask > AnnotatedGroundProgram::getEAMask ( int eaIndex ) const

Returns the the mask of a tracked external atom with a given index.

Parameters:

eaIndex Index of an external atom in indexedEatoms.

Returns:: Mask of the external atom identified by eaIndex.

Definition at line 1104 of file AnnotatedGroundProgram.cpp.

References eaMasks, and indexedEatoms.

Referenced by AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemBasicEABehavior(), EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemOptimizationPartBasicEAKnowledge(), GenuineGuessAndCheckModelGenerator::getWatchedLiteral(), GenuineGuessAndCheckModelGenerator::initializeVerificationWatchLists(), GenuineGuessAndCheckModelGenerator::inlineExternalAtoms(), GenuineGuessAndCheckModelGenerator::unverifyExternalAtoms(), GenuineGuessAndCheckModelGenerator::verifyExternalAtomByEvaluation(), GenuineGuessAndCheckModelGenerator::verifyExternalAtomBySupportSets(), GenuineGuessAndCheckModelGenerator::verifyExternalAtoms(), and verifyExternalAtomsUsingCompleteSupportSets().

const OrdinaryASPProgram & AnnotatedGroundProgram::getGroundProgram ( ) const

Returns the (not annotated) underlying ground program.

Returns:: Ground program.

Definition at line 1112 of file AnnotatedGroundProgram.cpp.

References groundProgram.

Referenced by InternalGroundASPSolver::computeClarkCompletion(), InternalGroundASPSolver::computeDepGraph(), InternalGroundASPSolver::createShiftedProgram(), InternalGroundASPSolver::createSingularLoopNogoods(), GenuineGuessAndCheckModelGenerator::getGroundProgram(), UnfoundedSetCheckerManager::getUnfoundedSet(), InternalGroundASPSolver::initializeLists(), UnfoundedSetCheckerManager::initializeUnfoundedSetCheckers(), InternalGroundASPSolver::initSourcePointers(), InternalGroundASPSolver::outputProjection(), InternalGroundASPSolver::setEDB(), UnfoundedSetCheckHeuristics::UnfoundedSetCheckHeuristics(), and UnfoundedSetCheckHeuristics::updateSkipProgram().

ID AnnotatedGroundProgram::getIndexedEAtom ( int index ) const

Returns a single external atom identified by its index.

Parameters:

index Identifies the external atom.

Returns:: ID of external atom associated with index.

Definition at line 1124 of file AnnotatedGroundProgram.cpp.

References indexedEatoms.

Referenced by AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemBasicEABehavior(), EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemOptimizationPartBasicEAKnowledge(), and UnfoundedSetChecker::isUnfoundedSet().

const std::vector< ID > & AnnotatedGroundProgram::getIndexedEAtoms ( ) const

Returns the external atoms indexed by this AnnotatedGroundProgram.

Returns:: Set of indexed external atoms.

Definition at line 1118 of file AnnotatedGroundProgram.cpp.

References indexedEatoms.

Referenced by AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemBasicEABehavior(), EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemOptimizationPartBasicEAKnowledge(), and UnfoundedSetChecker::isUnfoundedSet().

int AnnotatedGroundProgram::getIndexOfEAtom ( ID eatomID ) const

Returns the index of an external atom identified by its ID.

Parameters:

eatomID ID of the external atom to retrieve.

Returns:: Index of eatomID or -1 if it not indexed.

Definition at line 1130 of file AnnotatedGroundProgram.cpp.

References indexedEatoms.

Referenced by GenuineGuessAndCheckModelGenerator::inlineExternalAtoms().

InterpretationConstPtr AnnotatedGroundProgram::getProgramMask ( ) const

Returns the mask of the overall program.

Returns:: Program mask.

Definition at line 1137 of file AnnotatedGroundProgram.cpp.

References programMask.

Referenced by GenuineGuessAndCheckModelGenerator::generateNextModel(), UnfoundedSetChecker::getUFSNogoodUFSBased(), GenuineGuessAndCheckModelGenerator::initializeInconsistencyAnalysis(), ImmediateNogoodGrounder::update(), GenuineGuessAndCheckModelGenerator::verifyExternalAtomByEvaluation(), and GenuineGuessAndCheckModelGenerator::verifyExternalAtoms().

const OrdinaryASPProgram & AnnotatedGroundProgram::getProgramOfComponent ( int compNr ) const

Retrieves a component as OrdinaryASPProgram.

Parameters:

compNr A component index from 0 to getComponentCount()-1.

Returns:: Underlying (not annotated) ground program.

Definition at line 911 of file AnnotatedGroundProgram.cpp.

References depSCC, and programComponents.

Referenced by UnfoundedSetCheckerManager::computeChoiceRuleCompatibilityForComponent(), UnfoundedSetCheckerManager::getUnfoundedSet(), and UnfoundedSetCheckerManager::initializeUnfoundedSetCheckers().

bool AnnotatedGroundProgram::hasECycles ( int compNr ) const

Checks a given component for cycles through external atoms.

Parameters:

compNr A component index from 0 to getComponentCount()-1.

Returns:: True if component compNr has cycles through external atoms and false otherwise.

Definition at line 932 of file AnnotatedGroundProgram.cpp.

References depSCC, and eCycles.

Referenced by UnfoundedSetCheckerManager::getUnfoundedSet(), UnfoundedSetCheckerManager::initializeUnfoundedSetCheckers(), GenuineGuessAndCheckModelGenerator::isModel(), GenuineGuessAndCheckModelGenerator::propagate(), and GenuineGuessAndCheckModelGenerator::updateEANogoods().

bool AnnotatedGroundProgram::hasECycles	(	int	compNr,
		InterpretationConstPtr	intr
	)		const

Checks a given component for head cycles when the atom dependency graph is restricted to intr.

Parameters:

compNr	A component index from 0 to getComponentCount()-1.
intr	A set of atoms; the atom dependency graph will be reduced to these atoms for answering the request.

Returns:: True if component compNr has head cycles when restricted to intr and false otherwise.

Definition at line 973 of file AnnotatedGroundProgram.cpp.

References ctx, DBGLOG, depGraph, depNodes, depSCC, DLVHEX_BENCHMARK_REGISTER_AND_COUNT, externalEdges, hasECycles(), and ProgramCtx::registry().

bool AnnotatedGroundProgram::hasECycles ( ) const

Checks the program has cycles through external atoms.

Returns:: True if it has cycles through external atoms and false otherwise.

Definition at line 1079 of file AnnotatedGroundProgram.cpp.

References eCyclesTotal.

Referenced by hasECycles().

bool AnnotatedGroundProgram::hasECycles ( InterpretationConstPtr intr ) const

Checks thr program for cycles through external atoms when the atom dependency graph is restricted to intr.

Parameters:

intr	A set of atoms; the atom dependency graph will be reduced to these atoms for answering the request.

Returns:: True if the program cycles through external atoms when restricted to intr and false otherwise.

Definition at line 1065 of file AnnotatedGroundProgram.cpp.

References DBGLOG, depSCC, and hasECycles().

bool AnnotatedGroundProgram::hasHeadCycles ( int compNr ) const

Checks a given component for head cycles.

Parameters:

compNr A component index from 0 to getComponentCount()-1.

Returns:: True if component compNr has head cycles and false otherwise.

Definition at line 925 of file AnnotatedGroundProgram.cpp.

References depSCC, and headCycles.

Referenced by UnfoundedSetCheckerManager::computeChoiceRuleCompatibilityForComponent(), UnfoundedSetCheckerManager::getUnfoundedSet(), UnfoundedSetCheckerManager::initializeUnfoundedSetCheckers(), GenuineGuessAndCheckModelGenerator::isModel(), and GenuineGuessAndCheckModelGenerator::propagate().

bool AnnotatedGroundProgram::hasHeadCycles ( ) const

Checks the program has head cycles.

Returns:: True if it has head cycles and false otherwise.

Definition at line 1059 of file AnnotatedGroundProgram.cpp.

References headCyclesTotal.

void AnnotatedGroundProgram::initialize ( ) [private]

Calls all other initialization methods.

Definition at line 348 of file AnnotatedGroundProgram.cpp.

References computeAdditionalDependencies(), computeAtomDependencyGraph(), computeECycles(), computeHeadCycles(), computeStronglyConnectedComponents(), createEAMasks(), createProgramMask(), DBGLOG, depSCC, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, eaMasks, eCycles, OrdinaryASPProgram::edb, groundProgram, haveGrounding, headCycles, headCyclicRules, OrdinaryASPProgram::idb, mapAuxToEAtoms(), RawPrinter::print(), and reg.

Referenced by AnnotatedGroundProgram(), and setIndexEAtoms().

void AnnotatedGroundProgram::mapAuxToEAtoms ( ) [private]

Initializes auxToEA.

Definition at line 314 of file AnnotatedGroundProgram.cpp.

References auxToEA, DBGLOG, eaMasks, indexedEatoms, PredicateMask::mask(), and reg.

Referenced by initialize().

bool AnnotatedGroundProgram::mapsAux ( IDAddress ida ) const

Checks if ida is contained in the ground program and mapped back to an external atom in indexEAtoms.

Returns:: True if ida is contained in the ground program and mapped back to an external atom in indexEAtoms.

Definition at line 1085 of file AnnotatedGroundProgram.cpp.

References auxToEA.

Referenced by AssumptionBasedUnfoundedSetChecker::constructDomain(), EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemNecessaryPart(), GenuineGuessAndCheckModelGenerator::generalizeNogood(), UnfoundedSetChecker::getUFSNogoodUFSBased(), GenuineGuessAndCheckModelGenerator::inlineExternalAtoms(), and GenuineGuessAndCheckModelGenerator::learnSupportSets().

const AnnotatedGroundProgram & AnnotatedGroundProgram::operator= ( const AnnotatedGroundProgram & other )

Assignment operator.

Parameters:

other Assign another AnnotatedGroundProgram and overwrite the contents.

Definition at line 259 of file AnnotatedGroundProgram.cpp.

References auxToEA, componentOfAtom, depGraph, depNodes, depSCC, eaMasks, eCycles, eCyclesTotal, externalEdges, groundProgram, haveGrounding, headCycles, headCyclesTotal, headCyclicRules, indexedEatoms, programComponents, programMask, reg, and supportSets.

void AnnotatedGroundProgram::setCompleteSupportSetsForVerification ( SimpleNogoodContainerPtr supportSets )

Sets support sets for verification.

Parameters:

supportSets Support sets encoded as nogoods.

Definition at line 1144 of file AnnotatedGroundProgram.cpp.

References supportSets.

Referenced by GenuineGuessAndCheckModelGenerator::learnSupportSets().

void AnnotatedGroundProgram::setIndexEAtoms ( std::vector< ID > indexedEatoms )

Set the external atoms to track.

Parameters:

indexedEatoms Set of (possibly nonground) external atoms.

Definition at line 340 of file AnnotatedGroundProgram.cpp.

References indexedEatoms, and initialize().

bool AnnotatedGroundProgram::verifyExternalAtomsUsingCompleteSupportSets	(	int	eaIndex,
		InterpretationConstPtr	interpretation,
		InterpretationConstPtr	auxiliariesToVerify
	)		const

Tries to verify an external atom which allows for verification using support sets and returns the result of this check.

(only supported if support sets have been defined).

Parameters:

eaIndex	Identifies an external atom by its index.
interpretation	An interpretation which is complete for the given ground program (including external atom auxilies).
auxiliariesToVerify	The set of external atoms to verify.

Returns:: Verification result.

Definition at line 1162 of file AnnotatedGroundProgram.cpp.

References ID::address, DBGLOG, getEAMask(), ExternalAtom::getExtSourceProperties(), Nogood::getStringRepresentation(), ID_FAIL(), IDKind, indexedEatoms, Nogood::isGround(), ID::isNaf(), ID::NAF_MASK, RawPrinter::print(), ID::PROPERTY_EXTERNALAUX, ExtSourceProperties::providesCompletePositiveSupportSets(), reg, and supportSets.

Referenced by UnfoundedSetChecker::isUnfoundedSet(), and GenuineGuessAndCheckModelGenerator::verifyExternalAtomBySupportSets().

Field Documentation

boost::unordered_map<IDAddress, std::vector<ID> > AnnotatedGroundProgram::auxToEA [private]

Stores for each external atom auxiliary in groundProgram the set of (nonground) external atoms it stems from (this external atom is in general not unique).

Definition at line 83 of file AnnotatedGroundProgram.h.

Referenced by addProgram(), computeAtomDependencyGraph(), getAuxToEA(), mapAuxToEAtoms(), mapsAux(), and operator=().

boost::unordered_map<IDAddress, int> AnnotatedGroundProgram::componentOfAtom [private]

Stores for each ground atom the index of the component in depSCC where the atom is contained.

Definition at line 117 of file AnnotatedGroundProgram.h.

Referenced by addProgram(), computeECycles(), computeStronglyConnectedComponents(), and operator=().

ProgramCtx* AnnotatedGroundProgram::ctx [private]

ProgramCtx.

Definition at line 67 of file AnnotatedGroundProgram.h.

Referenced by computeAdditionalDependencies(), computeAtomDependencyGraph(), computeECycles(), createEAMasks(), and hasECycles().

std::vector<ID> AnnotatedGroundProgram::dependencyIDB [private]

Subset of nonground rules used for computing additional dependencies (see constructor AnnotatedGroundProgram::AnnotatedGroundProgram).

Definition at line 73 of file AnnotatedGroundProgram.h.

Referenced by computeAdditionalDependencies().

Graph AnnotatedGroundProgram::depGraph [private]

Atom dependency graph.

Definition at line 113 of file AnnotatedGroundProgram.h.

Referenced by computeAdditionalDependencies(), computeAtomDependencyGraph(), computeECycles(), computeStronglyConnectedComponents(), hasECycles(), and operator=().

boost::unordered_map<IDAddress, Node> AnnotatedGroundProgram::depNodes [private]

Stores for each ground atom IDAddress the according node in the atom dependency graph.

Definition at line 111 of file AnnotatedGroundProgram.h.

Referenced by computeAdditionalDependencies(), computeAtomDependencyGraph(), computeECycles(), computeStronglyConnectedComponents(), hasECycles(), and operator=().

std::vector<std::set<IDAddress> > AnnotatedGroundProgram::depSCC [private]

Strongly connected components (of atoms) of depGraph.

Definition at line 115 of file AnnotatedGroundProgram.h.

Referenced by addProgram(), computeECycles(), computeHeadCycles(), computeStronglyConnectedComponents(), getAtomsOfComponent(), getProgramOfComponent(), hasECycles(), hasHeadCycles(), initialize(), and operator=().

std::vector<boost::shared_ptr<ExternalAtomMask> > AnnotatedGroundProgram::eaMasks [private]

Stores for each external atom in indexedEatoms its mask, i.e., set of ground atoms stemming from this external atom.

Definition at line 81 of file AnnotatedGroundProgram.h.

Referenced by addProgram(), createEAMasks(), getEAMask(), initialize(), mapAuxToEAtoms(), and operator=().

std::vector<bool> AnnotatedGroundProgram::eCycles [private]

Stores for each component in depSCC whether it contains cycles through external atoms.

Definition at line 125 of file AnnotatedGroundProgram.h.

Referenced by addProgram(), computeECycles(), hasECycles(), initialize(), and operator=().

bool AnnotatedGroundProgram::eCyclesTotal [private]

Stores if the overall program contains cycles through external atoms.

Definition at line 132 of file AnnotatedGroundProgram.h.

Referenced by addProgram(), computeECycles(), hasECycles(), and operator=().

std::vector<std::pair<IDAddress, IDAddress> > AnnotatedGroundProgram::externalEdges [private]

Stores edges (a,b) between ground atoms a,b such that atom a externally depends on b.

Definition at line 119 of file AnnotatedGroundProgram.h.

Referenced by computeAdditionalDependencies(), computeAtomDependencyGraph(), computeECycles(), hasECycles(), and operator=().

OrdinaryASPProgram AnnotatedGroundProgram::groundProgram [private]

Underlying ground program without annotations.

Definition at line 71 of file AnnotatedGroundProgram.h.

Referenced by addProgram(), computeAdditionalDependencies(), computeAtomDependencyGraph(), computeStronglyConnectedComponents(), createEAMasks(), createProgramMask(), getGroundProgram(), initialize(), and operator=().

bool AnnotatedGroundProgram::haveGrounding [private]

True if groundProgram is initialized, otherwise false (then we have only information about ground external atoms in the program but not about the entire program).

Definition at line 75 of file AnnotatedGroundProgram.h.

Referenced by addProgram(), initialize(), and operator=().

std::vector<bool> AnnotatedGroundProgram::headCycles [private]

Stores for each component in depSCC whether it contains head cycles.

Definition at line 121 of file AnnotatedGroundProgram.h.

Referenced by addProgram(), computeHeadCycles(), hasHeadCycles(), initialize(), and operator=().