#include <include/dlvhex2/UnfoundedSetChecker.h>

Inheritance diagram for EncodingBasedUnfoundedSetChecker:

Collaboration diagram for EncodingBasedUnfoundedSetChecker:

Public Member Functions
	EncodingBasedUnfoundedSetChecker (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).
	EncodingBasedUnfoundedSetChecker (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.
void	learnNogoodsFromMainSearch (bool reset)
	Forces all unfounded set checker in this manager to learn nogoods from main search now.
std::vector< IDAddress >	getUnfoundedSet (InterpretationConstPtr compatibleSet, const std::set< ID > &skipProgram)
	Transforms a nogood from the main search to the UFS search.
Private Member Functions
void	constructUFSDetectionProblem (NogoodSet &ufsDetectionProblem, InterpretationConstPtr compatibleSet, InterpretationConstPtr compatibleSetWithoutAux, const std::set< ID > &skipProgram, std::vector< ID > &ufsProgram)
	Constructs the nogood set used for unfounded set detection.
void	constructUFSDetectionProblemNecessaryPart (NogoodSet &ufsDetectionProblem, int &auxatomcnt, InterpretationConstPtr compatibleSet, InterpretationConstPtr compatibleSetWithoutAux, const std::set< ID > &skipProgram, std::vector< ID > &ufsProgram)
	Constructs the necessary part of the nogood set used for unfounded set detection.
void	constructUFSDetectionProblemOptimizationPart (NogoodSet &ufsDetectionProblem, int &auxatomcnt, InterpretationConstPtr compatibleSet, InterpretationConstPtr compatibleSetWithoutAux, const std::set< ID > &skipProgram, std::vector< ID > &ufsProgram)
	Constructs the optional optimization part of the nogood set used for unfounded set detection.
void	constructUFSDetectionProblemOptimizationPartRestrictToCompatibleSet (NogoodSet &ufsDetectionProblem, int &auxatomcnt, InterpretationConstPtr compatibleSet, InterpretationConstPtr compatibleSetWithoutAux, const std::set< ID > &skipProgram, std::vector< ID > &ufsProgram)
	Constructs the optional optimization part of the nogood set used for unfounded set detection such that the search is restricted to atoms which are true in the compatible set.
void	constructUFSDetectionProblemOptimizationPartBasicEAKnowledge (NogoodSet &ufsDetectionProblem, int &auxatomcnt, InterpretationConstPtr compatibleSet, InterpretationConstPtr compatibleSetWithoutAux, const std::set< ID > &skipProgram, std::vector< ID > &ufsProgram)
	Constructs the optional optimization part of the nogood set used for unfounded set detection, exploiting the fact that the truth value of external atoms cannot change if no input atom is unfounded.
void	constructUFSDetectionProblemOptimizationPartLearnedFromMainSearch (NogoodSet &ufsDetectionProblem, int &auxatomcnt, InterpretationConstPtr compatibleSet, InterpretationConstPtr compatibleSetWithoutAux, const std::set< ID > &skipProgram, std::vector< ID > &ufsProgram)
	Constructs the optional optimization part of the nogood set used for unfounded set detection using learned nogoods from the main search.
void	constructUFSDetectionProblemOptimizationPartEAEnforement (NogoodSet &ufsDetectionProblem, int &auxatomcnt, InterpretationConstPtr compatibleSet, InterpretationConstPtr compatibleSetWithoutAux, const std::set< ID > &skipProgram, std::vector< ID > &ufsProgram)
	Constructs the optional optimization part of the nogood set used for unfounded set detection which tries to keep the truth values of external atoms unchanged.
std::pair< bool, Nogood >	nogoodTransformation (Nogood ng, InterpretationConstPtr compatibleSet)
	Transforms a nogood (valid input-output relationship of some external atom) learned in the main search for being used in the UFS search.

Detailed Description

Definition at line 263 of file UnfoundedSetChecker.h.

Constructor & Destructor Documentation

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

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 557 of file UnfoundedSetChecker.cpp.

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

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 567 of file UnfoundedSetChecker.cpp.

Member Function Documentation

void EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblem	(	NogoodSet &	ufsDetectionProblem,
		InterpretationConstPtr	compatibleSet,
		InterpretationConstPtr	compatibleSetWithoutAux,
		const std::set< ID > &	skipProgram,
		std::vector< ID > &	ufsProgram
	)		`[private]`

Constructs the nogood set used for unfounded set detection.

The construction depends on the interpretation (encoding-based UFS detection). The constructed UFS detection problem is written to ufsDetectionProblem

Parameters:

compatibleSet	The compatible set to create the UFS check for.
compatibleSetWithoutAux	The compatible set without external atom auxiliaries.
skipProgram	The set of rules considered in the UFS search.
ufsProgram	the set of rules in the program but ignored in the UFS search.

Definition at line 579 of file UnfoundedSetChecker.cpp.

References constructUFSDetectionProblemNecessaryPart(), and constructUFSDetectionProblemOptimizationPart().

Referenced by getUnfoundedSet().

void EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemNecessaryPart	(	NogoodSet &	ufsDetectionProblem,
		int &	auxatomcnt,
		InterpretationConstPtr	compatibleSet,
		InterpretationConstPtr	compatibleSetWithoutAux,
		const std::set< ID > &	skipProgram,
		std::vector< ID > &	ufsProgram
	)		`[private]`

Constructs the necessary part of the nogood set used for unfounded set detection.

The construction depends on the interpretation (encoding-based UFS detection). The constructed UFS detection problem is written to ufsDetectionProblem

Parameters:

compatibleSet	The compatible set to create the UFS check for.
compatibleSetWithoutAux	The compatible set without external atom auxiliaries.
skipProgram	The set of rules considered in the UFS search.
ufsProgram	the set of rules in the program but ignored in the UFS search.

Definition at line 593 of file UnfoundedSetChecker.cpp.

Referenced by constructUFSDetectionProblem().

void EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemOptimizationPart	(	NogoodSet &	ufsDetectionProblem,
		int &	auxatomcnt,
		InterpretationConstPtr	compatibleSet,
		InterpretationConstPtr	compatibleSetWithoutAux,
		const std::set< ID > &	skipProgram,
		std::vector< ID > &	ufsProgram
	)		`[private]`

Constructs the optional optimization part of the nogood set used for unfounded set detection.

The construction depends on the interpretation (encoding-based UFS detection). The constructed UFS detection problem is written to ufsDetectionProblem

Parameters:

compatibleSet	The compatible set to create the UFS check for.
compatibleSetWithoutAux	The compatible set without external atom auxiliaries.
skipProgram	The set of rules considered in the UFS search.
ufsProgram	the set of rules in the program but ignored in the UFS search.

Definition at line 776 of file UnfoundedSetChecker.cpp.

References constructUFSDetectionProblemOptimizationPartBasicEAKnowledge(), constructUFSDetectionProblemOptimizationPartEAEnforement(), constructUFSDetectionProblemOptimizationPartLearnedFromMainSearch(), constructUFSDetectionProblemOptimizationPartRestrictToCompatibleSet(), DBGLOG, UnfoundedSetChecker::mode, UnfoundedSetChecker::ngc, and UnfoundedSetChecker::WithExt.

Referenced by constructUFSDetectionProblem().

void EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemOptimizationPartBasicEAKnowledge	(	NogoodSet &	ufsDetectionProblem,
		int &	auxatomcnt,
		InterpretationConstPtr	compatibleSet,
		InterpretationConstPtr	compatibleSetWithoutAux,
		const std::set< ID > &	skipProgram,
		std::vector< ID > &	ufsProgram
	)		`[private]`

Constructs the optional optimization part of the nogood set used for unfounded set detection, exploiting the fact that the truth value of external atoms cannot change if no input atom is unfounded.

The construction depends on the interpretation (encoding-based UFS detection). The constructed UFS detection problem is written to ufsDetectionProblem

Parameters:

compatibleSet	The compatible set to create the UFS check for.
compatibleSetWithoutAux	The compatible set without external atom auxiliaries.
skipProgram	The set of rules considered in the UFS search.
ufsProgram	the set of rules in the program but ignored in the UFS search.

Definition at line 828 of file UnfoundedSetChecker.cpp.

References NogoodSet::addNogood(), UnfoundedSetChecker::agp, NogoodContainer::createLiteral(), DBGLOG, UnfoundedSetChecker::domain, AnnotatedGroundProgram::getEAMask(), AnnotatedGroundProgram::getIndexedEAtom(), AnnotatedGroundProgram::getIndexedEAtoms(), ExternalAtom::getPredicateInputMask(), Nogood::insert(), UnfoundedSetChecker::reg, and ExternalAtom::updatePredicateInputMask().

Referenced by constructUFSDetectionProblemOptimizationPart().

void EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemOptimizationPartEAEnforement	(	NogoodSet &	ufsDetectionProblem,
		int &	auxatomcnt,
		InterpretationConstPtr	compatibleSet,
		InterpretationConstPtr	compatibleSetWithoutAux,
		const std::set< ID > &	skipProgram,
		std::vector< ID > &	ufsProgram
	)		`[private]`

Constructs the optional optimization part of the nogood set used for unfounded set detection which tries to keep the truth values of external atoms unchanged.

The construction depends on the interpretation (encoding-based UFS detection). The constructed UFS detection problem is written to ufsDetectionProblem

Parameters:

compatibleSet	The compatible set to create the UFS check for.
compatibleSetWithoutAux	The compatible set without external atom auxiliaries.
skipProgram	The set of rules considered in the UFS search.
ufsProgram	the set of rules in the program but ignored in the UFS search.

Definition at line 914 of file UnfoundedSetChecker.cpp.

References NogoodSet::addNogood(), ID::address, Rule::body, NogoodContainer::createLiteral(), DBGLOG, Rule::head, Nogood::insert(), ID::isExternalAuxiliary(), ID::isNaf(), ID::MAINKIND_ATOM, ID::PROPERTY_ATOM_HIDDEN, ID::PROPERTY_AUX, UnfoundedSetChecker::reg, ID::SUBKIND_ATOM_ORDINARYG, and Atom::tuple.

Referenced by constructUFSDetectionProblemOptimizationPart().

void EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemOptimizationPartLearnedFromMainSearch	(	NogoodSet &	ufsDetectionProblem,
		int &	auxatomcnt,
		InterpretationConstPtr	compatibleSet,
		InterpretationConstPtr	compatibleSetWithoutAux,
		const std::set< ID > &	skipProgram,
		std::vector< ID > &	ufsProgram
	)		`[private]`

Constructs the optional optimization part of the nogood set used for unfounded set detection using learned nogoods from the main search.

The construction depends on the interpretation (encoding-based UFS detection). The constructed UFS detection problem is written to ufsDetectionProblem

Parameters:

compatibleSet	The compatible set to create the UFS check for.
compatibleSetWithoutAux	The compatible set without external atom auxiliaries.
skipProgram	The set of rules considered in the UFS search.
ufsProgram	the set of rules in the program but ignored in the UFS search.

Definition at line 887 of file UnfoundedSetChecker.cpp.

References NogoodSet::addNogood(), DBGLOG, Nogood::getStringRepresentation(), Nogood::isGround(), UnfoundedSetChecker::ngc, nogoodTransformation(), and UnfoundedSetChecker::reg.

Referenced by constructUFSDetectionProblemOptimizationPart().

void EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemOptimizationPartRestrictToCompatibleSet	(	NogoodSet &	ufsDetectionProblem,
		int &	auxatomcnt,
		InterpretationConstPtr	compatibleSet,
		InterpretationConstPtr	compatibleSetWithoutAux,
		const std::set< ID > &	skipProgram,
		std::vector< ID > &	ufsProgram
	)		`[private]`

Constructs the optional optimization part of the nogood set used for unfounded set detection such that the search is restricted to atoms which are true in the compatible set.

The construction depends on the interpretation (encoding-based UFS detection). The constructed UFS detection problem is written to ufsDetectionProblem

Parameters:

compatibleSet	The compatible set to create the UFS check for.
compatibleSetWithoutAux	The compatible set without external atom auxiliaries.
skipProgram	The set of rules considered in the UFS search.
ufsProgram	the set of rules in the program but ignored in the UFS search.

Definition at line 797 of file UnfoundedSetChecker.cpp.

References NogoodSet::addNogood(), ID::address, Rule::body, NogoodContainer::createLiteral(), DBGLOG, Rule::head, Nogood::insert(), ID::isExternalAuxiliary(), UnfoundedSetChecker::mode, UnfoundedSetChecker::Ordinary, and UnfoundedSetChecker::reg.

Referenced by constructUFSDetectionProblemOptimizationPart().

std::vector< IDAddress > EncodingBasedUnfoundedSetChecker::getUnfoundedSet	(	InterpretationConstPtr	compatibleSet,
		const std::set< ID > &	skipProgram
	)		`[virtual]`

Transforms a nogood from the main search to the UFS search.

Parameters:

ng	Nogodo to transform.
compatibleSet	Compatible set for which the UFS check shall be performed.

Returns:: A set of nogoods which can be used in the unfounded set search.

Implements UnfoundedSetChecker.

Definition at line 1101 of file UnfoundedSetChecker.cpp.

void EncodingBasedUnfoundedSetChecker::learnNogoodsFromMainSearch ( bool reset ) [virtual]

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

Implements UnfoundedSetChecker.

Definition at line 1094 of file UnfoundedSetChecker.cpp.

std::pair< bool, Nogood > EncodingBasedUnfoundedSetChecker::nogoodTransformation	(	Nogood	ng,
		InterpretationConstPtr	compatibleSet
	)		`[private, virtual]`

Transforms a nogood (valid input-output relationship of some external atom) learned in the main search for being used in the UFS search.

Parameters:

ng	The nogood from the main search.
compatibleSet	The current compatible set we do the unfounded set search with respect to. Note: For AssumptionBasedUnfoundedSetChecker it is essential that the nogood transformation is independent of the compatible set.

Returns:: A pair of a boolean, which denotes if the transformation yielded a nogood, an the transformed nogood in this case.

Implements UnfoundedSetChecker.

Definition at line 1007 of file UnfoundedSetChecker.cpp.

References ID::address, NogoodContainer::createLiteral(), DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, UnfoundedSetChecker::domain, Nogood::insert(), ID::isNaf(), ID::kind, ID::NAF_MASK, UnfoundedSetChecker::reg, and Atom::tuple.

Referenced by constructUFSDetectionProblemOptimizationPartLearnedFromMainSearch().

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

include/dlvhex2/UnfoundedSetChecker.h
src/UnfoundedSetChecker.cpp

Public Member Functions

Private Member Functions

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation