Creates independent unfounded set checkers for all components of a program and automatically calls them appropriately. More...

#include <include/dlvhex2/UnfoundedSetChecker.h>

Collaboration diagram for UnfoundedSetCheckerManager:

[legend]

Public Types
typedef boost::shared_ptr < UnfoundedSetCheckerManager >	Ptr
Public Member Functions
	UnfoundedSetCheckerManager (BaseModelGenerator &mg, ProgramCtx &ctx, const AnnotatedGroundProgram &agp, bool choiceRuleCompatible=false, SimpleNogoodContainerPtr ngc=SimpleNogoodContainerPtr())
	Initializes the UFS checker with support for external atoms.
	UnfoundedSetCheckerManager (ProgramCtx &ctx, const AnnotatedGroundProgram &agp, bool choiceRuleCompatible=false)
	Initializes the UFS checker without support for external atoms (they are considered as ordinary ones).
std::vector< IDAddress >	getUnfoundedSet (InterpretationConstPtr interpretation, const std::set< ID > &skipProgram, SimpleNogoodContainerPtr ngc=SimpleNogoodContainerPtr())
	Tries to detect an unfounded set with the possibility to ignore rules and learn nogoods.
std::vector< IDAddress >	getUnfoundedSet (InterpretationConstPtr interpretation)
	Tries to detect an unfounded set, but does not skip program parts or learn nogoods.
void	initializeUnfoundedSetCheckers ()
	Initializes the unfounded set checkers for all program components.
void	learnNogoodsFromMainSearch (bool reset)
	Forces all unfounded set checker in this manager to learn nogoods from main search now.
Nogood	getLastUFSNogood () const
	Returns the UFS nogood for the most recent detected unfounded set.
Private Member Functions
void	computeChoiceRuleCompatibility (bool choiceRuleCompatible)
	Computes for all components if they intersect with non-HCF rules and stores the results in UnfoundedSetCheckerManager::intersectsWithNonHCFDisjunctiveRules.
void	computeChoiceRuleCompatibilityForComponent (bool choiceRuleCompatible, int comp)
	Computes for a given components if it intersects with non-HCF rules and stores the results in UnfoundedSetCheckerManager::intersectsWithNonHCFDisjunctiveRules.
UnfoundedSetCheckerPtr	instantiateUnfoundedSetChecker (ProgramCtx &ctx, const OrdinaryASPProgram &groundProgram, InterpretationConstPtr componentAtoms=InterpretationConstPtr(), SimpleNogoodContainerPtr ngc=SimpleNogoodContainerPtr())
	Initializes the UFS checker without support for external atoms (they are considered as ordinary ones).
UnfoundedSetCheckerPtr	instantiateUnfoundedSetChecker (BaseModelGenerator &mg, ProgramCtx &ctx, const OrdinaryASPProgram &groundProgram, const AnnotatedGroundProgram &agp, InterpretationConstPtr componentAtoms=InterpretationConstPtr(), SimpleNogoodContainerPtr ngc=SimpleNogoodContainerPtr())
	Initializes the UFS checker with support for external atoms.
Private Attributes
ProgramCtx &	ctx
	Program context.
BaseModelGenerator *	mg
	Reference to the model generator which shall be used for evaluating external atoms.
const AnnotatedGroundProgram &	agp
	UnfoundedSetChecker::groundProgram with additional meta information.
int	lastAGPComponentCount
	Used for detecting extensions of the AnnotatedGroundProgram.
Nogood	ufsnogood
	Temporary storage for the UFS nogood of the last detected unfounded set.
SimpleNogoodContainerPtr	ngc
	Pointer to a container with valid input-output relationships (EANogoods).
std::map< int, UnfoundedSetCheckerPtr >	preparedUnfoundedSetCheckers
	Unfounded set checkers for all components.
std::vector< bool >	intersectsWithNonHCFDisjunctiveRules
	Stores for each component if it intersects with non-head-cycle-free rules.
bool	choiceRuleCompatible
	Stores if the UFS checker should reduce optimization such that an implementation of non-HCF rules via choice rules is possible.

Detailed Description

Creates independent unfounded set checkers for all components of a program and automatically calls them appropriately.

Depending on the settings, the class keeps one UFS checker for the program or a separate one for all components. During UFS checker, the single components are checked until a UFS is found. The class further exploits decision criteria which allows for skipping the UFS check for the overall program or single components.

Definition at line 594 of file UnfoundedSetChecker.h.

Member Typedef Documentation

typedef boost::shared_ptr<UnfoundedSetCheckerManager> UnfoundedSetCheckerManager::Ptr

Definition at line 739 of file UnfoundedSetChecker.h.

Constructor & Destructor Documentation

UnfoundedSetCheckerManager::UnfoundedSetCheckerManager	(	BaseModelGenerator &	mg,
		ProgramCtx &	ctx,
		const AnnotatedGroundProgram &	agp,
		bool	choiceRuleCompatible = `false`,
		SimpleNogoodContainerPtr	ngc = `SimpleNogoodContainerPtr()`
	)

Initializes the UFS checker with support for external atoms.

Parameters:

mg	Reference to a model generator (used to evaluate the external atoms)
ctx	ProgramCtx
agp	Ground program with meta information used for optimized UFS checking
choiceRuleCompatible	This parameter is necessary for the clasp backend, which implements non-head cycle free disjunctive rules using choice rules. However, this transformation must be regarded in the optimization of UFS checking. More specifically, the UFS check MUST NOT BE SKIPPED for HFC-free components if they contain such choice rules. For more information, see examples/trickyufs.hex.
ngc	Pointer to a container with valid input-output relationships (EANogoods)

Definition at line 2090 of file UnfoundedSetChecker.cpp.

References computeChoiceRuleCompatibility(), ProgramCtx::config, Configuration::getOption(), and initializeUnfoundedSetCheckers().

UnfoundedSetCheckerManager::UnfoundedSetCheckerManager	(	ProgramCtx &	ctx,
		const AnnotatedGroundProgram &	agp,
		bool	choiceRuleCompatible = `false`
	)

Initializes the UFS checker without support for external atoms (they are considered as ordinary ones).

Parameters:

ctx	ProgramCtx
agp	Ground program with meta information used for optimized UFS checking
choiceRuleCompatible	This parameter is necessary for the clasp backend, which implements non-head cycle free disjunctive rules using choice rules. However, this transformation must be regarded in the optimization of UFS checking. More specifically, the UFS check MUST NOT BE SKIPPED for HFC-free components if they contain such choice rules. For more information, see examples/trickyufs.hex.

Definition at line 2157 of file UnfoundedSetChecker.cpp.

References computeChoiceRuleCompatibility(), ProgramCtx::config, Configuration::getOption(), and initializeUnfoundedSetCheckers().

Member Function Documentation

void UnfoundedSetCheckerManager::computeChoiceRuleCompatibility ( bool choiceRuleCompatible ) [private]

Computes for all components if they intersect with non-HCF rules and stores the results in UnfoundedSetCheckerManager::intersectsWithNonHCFDisjunctiveRules.

Parameters:

choiceRuleCompatible See UnfoundedSetCheckerManager::choiceRuleCompatible.

Definition at line 2209 of file UnfoundedSetChecker.cpp.

References agp, computeChoiceRuleCompatibilityForComponent(), and AnnotatedGroundProgram::getComponentCount().

Referenced by UnfoundedSetCheckerManager().

void UnfoundedSetCheckerManager::computeChoiceRuleCompatibilityForComponent	(	bool	choiceRuleCompatible,
		int	comp
	)		`[private]`

Computes for a given components if it intersects with non-HCF rules and stores the results in UnfoundedSetCheckerManager::intersectsWithNonHCFDisjunctiveRules.

Parameters:

choiceRuleCompatible	See UnfoundedSetCheckerManager::choiceRuleCompatible.
comp	Component index.

Definition at line 2218 of file UnfoundedSetChecker.cpp.

References agp, choiceRuleCompatible, AnnotatedGroundProgram::containsHeadCycles(), AnnotatedGroundProgram::getProgramOfComponent(), AnnotatedGroundProgram::hasHeadCycles(), OrdinaryASPProgram::idb, and intersectsWithNonHCFDisjunctiveRules.

Referenced by computeChoiceRuleCompatibility(), and getUnfoundedSet().

Nogood UnfoundedSetCheckerManager::getLastUFSNogood ( ) const

Returns the UFS nogood for the most recent detected unfounded set.

Returns:: UFS nogood, see UnfoundedSetChecker::getUFSNogood.

Definition at line 2438 of file UnfoundedSetChecker.cpp.

References ufsnogood.

Referenced by InternalGroundDASPSolver::getNextModel().

std::vector< IDAddress > UnfoundedSetCheckerManager::getUnfoundedSet	(	InterpretationConstPtr	interpretation,
		const std::set< ID > &	skipProgram,
		SimpleNogoodContainerPtr	ngc = `SimpleNogoodContainerPtr()`
	)

Tries to detect an unfounded set with the possibility to ignore rules and learn nogoods.

Parameters:

interpretation	The compatible set the UFS check shall be performed form. Must be complete over all non-ignored rules (`skipProgram`).
skipProgram	Set of rule IDs to ignore during the check.
ngc	NogoodContainer to add learned nogoods to (can be NULL).

Returns:: Unfounded set as set of ground atoms, or the empty set of no unfounded set exists.

Definition at line 2313 of file UnfoundedSetChecker.cpp.

References agp, choiceRuleCompatible, computeChoiceRuleCompatibilityForComponent(), ProgramCtx::config, ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, AnnotatedGroundProgram::getAtomsOfComponent(), AnnotatedGroundProgram::getComponentCount(), AnnotatedGroundProgram::getGroundProgram(), Configuration::getOption(), AnnotatedGroundProgram::getProgramOfComponent(), AnnotatedGroundProgram::hasECycles(), AnnotatedGroundProgram::hasHeadCycles(), instantiateUnfoundedSetChecker(), intersectsWithNonHCFDisjunctiveRules, lastAGPComponentCount, mg, ngc, preparedUnfoundedSetCheckers, and ufsnogood.

Referenced by InternalGroundDASPSolver::getNextModel(), and getUnfoundedSet().

std::vector< IDAddress > UnfoundedSetCheckerManager::getUnfoundedSet ( InterpretationConstPtr interpretation )

Tries to detect an unfounded set, but does not skip program parts or learn nogoods.

Parameters:

interpretation The compatible set the UFS check shall be performed form. Must be complete over all non-ignored rules (skipProgram).

Returns:: Unfounded set as set of ground atoms, or the empty set of no unfounded set exists.

Definition at line 2431 of file UnfoundedSetChecker.cpp.

References getUnfoundedSet().

void UnfoundedSetCheckerManager::initializeUnfoundedSetCheckers ( )

Initializes the unfounded set checkers for all program components.

Definition at line 2169 of file UnfoundedSetChecker.cpp.

References agp, ProgramCtx::config, ctx, DBGLOG, AnnotatedGroundProgram::getAtomsOfComponent(), AnnotatedGroundProgram::getComponentCount(), AnnotatedGroundProgram::getGroundProgram(), Configuration::getOption(), AnnotatedGroundProgram::getProgramOfComponent(), AnnotatedGroundProgram::hasECycles(), AnnotatedGroundProgram::hasHeadCycles(), instantiateUnfoundedSetChecker(), intersectsWithNonHCFDisjunctiveRules, mg, ngc, and preparedUnfoundedSetCheckers.

Referenced by UnfoundedSetCheckerManager().

UnfoundedSetCheckerPtr UnfoundedSetCheckerManager::instantiateUnfoundedSetChecker	(	ProgramCtx &	ctx,
		const OrdinaryASPProgram &	groundProgram,
		InterpretationConstPtr	componentAtoms = `InterpretationConstPtr()`,
		SimpleNogoodContainerPtr	ngc = `SimpleNogoodContainerPtr()`
	)		`[private]`

Initializes the UFS checker without support for external atoms (they are considered as ordinary ones).

Parameters:

ctx	ProgramCtx
groundProgram	Ground program used for UFS checking.
componentAtoms	Atoms in the component the UFS checker is initialized for.
ngc	Pointer to a container with valid input-output relationships (EANogoods)

Definition at line 2264 of file UnfoundedSetChecker.cpp.

References ProgramCtx::config, DBGLOG, and Configuration::getOption().

Referenced by getUnfoundedSet(), and initializeUnfoundedSetCheckers().

UnfoundedSetCheckerPtr UnfoundedSetCheckerManager::instantiateUnfoundedSetChecker	(	BaseModelGenerator &	mg,
		ProgramCtx &	ctx,
		const OrdinaryASPProgram &	groundProgram,
		const AnnotatedGroundProgram &	agp,
		InterpretationConstPtr	componentAtoms = `InterpretationConstPtr()`,
		SimpleNogoodContainerPtr	ngc = `SimpleNogoodContainerPtr()`
	)		`[private]`

Initializes the UFS checker with support for external atoms.

Parameters:

mg	Reference to a model generator (used to evaluate the external atoms).
ctx	ProgramCtx.
groundProgram	Ground program used for UFS checking.
agp	Ground program with meta information used for optimized UFS checking.
choiceRuleCompatible	This parameter is necessary for the clasp backend, which implements non-head cycle free disjunctive rules using choice rules. However, this transformation must be regarded in the optimization of UFS checking. More specifically, the UFS check MUST NOT BE SKIPPED for HFC-free components if they contain such choice rules. For more information, see examples/trickyufs.hex.
ngc	Pointer to a container with valid input-output relationships (EANogoods)

Definition at line 2282 of file UnfoundedSetChecker.cpp.

References ProgramCtx::config, DBGLOG, and Configuration::getOption().

void UnfoundedSetCheckerManager::learnNogoodsFromMainSearch ( bool reset )

Forces all unfounded set checker in this manager to learn nogoods from main search now.

Parameters:

reset Specifies if the nogood container from the main search shall be scanned from the beginning (otherwise only nogoods added at the back will be recognized).

Definition at line 2302 of file UnfoundedSetChecker.cpp.

References preparedUnfoundedSetCheckers.

Field Documentation

const AnnotatedGroundProgram& UnfoundedSetCheckerManager::agp [private]

UnfoundedSetChecker::groundProgram with additional meta information.

Definition at line 603 of file UnfoundedSetChecker.h.

Referenced by computeChoiceRuleCompatibility(), computeChoiceRuleCompatibilityForComponent(), getUnfoundedSet(), and initializeUnfoundedSetCheckers().

bool UnfoundedSetCheckerManager::choiceRuleCompatible [private]

Stores if the UFS checker should reduce optimization such that an implementation of non-HCF rules via choice rules is possible.

This parameter is necessary for the clasp backend, which implements non-head cycle free disjunctive rules using choice rules. However, this transformation must be regarded in the optimization of UFS checking. More specifically, the UFS check MUST NOT BE SKIPPED for HFC-free components if they contain such choice rules. For more information, see examples/trickyufs.hex.

Definition at line 624 of file UnfoundedSetChecker.h.

Referenced by computeChoiceRuleCompatibilityForComponent(), and getUnfoundedSet().

ProgramCtx& UnfoundedSetCheckerManager::ctx [private]

Program context.

Definition at line 598 of file UnfoundedSetChecker.h.

Referenced by getUnfoundedSet(), and initializeUnfoundedSetCheckers().

std::vector<bool> UnfoundedSetCheckerManager::intersectsWithNonHCFDisjunctiveRules [private]

Stores for each component if it intersects with non-head-cycle-free rules.

Definition at line 615 of file UnfoundedSetChecker.h.

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

int UnfoundedSetCheckerManager::lastAGPComponentCount [private]

Used for detecting extensions of the AnnotatedGroundProgram.