Unfounded set checker for HEX programs (with external atoms). More...

#include <include/dlvhex2/UnfoundedSetChecker.h>

Inheritance diagram for UnfoundedSetChecker:

Collaboration diagram for UnfoundedSetChecker:

Data Structures
struct	UnfoundedSetVerificationStatus
	Defines data structures used for verification of UFS candidates. More...
Public Types
typedef boost::shared_ptr < UnfoundedSetChecker >	Ptr
typedef boost::shared_ptr < const UnfoundedSetChecker >	ConstPtr
Public Member Functions
	UnfoundedSetChecker (ProgramCtx &ctx, const OrdinaryASPProgram &groundProgram, InterpretationConstPtr componentAtoms=InterpretationConstPtr(), SimpleNogoodContainerPtr ngc=SimpleNogoodContainerPtr())
	Initialization for UFS search considering external atoms as ordinary ones.
	UnfoundedSetChecker (BaseModelGenerator *mg, ProgramCtx &ctx, const OrdinaryASPProgram &groundProgram, const AnnotatedGroundProgram &agp, InterpretationConstPtr componentAtoms=InterpretationConstPtr(), SimpleNogoodContainerPtr ngc=SimpleNogoodContainerPtr())
	Initialization for UFS search under consideration of the semantics of external atoms.
virtual	~UnfoundedSetChecker ()
virtual std::vector< IDAddress >	getUnfoundedSet (InterpretationConstPtr compatibleSet, const std::set< ID > &skipProgram)=0
	Returns an unfounded set of groundProgram with respect to a compatibleSet; If the empty set is returned, then there does not exist a greater (nonempty) unfounded set.
virtual void	learnNogoodsFromMainSearch (bool reset)=0
	Forces the unfounded set checker to learn nogoods from main search now.
Nogood	getUFSNogood (const std::vector< IDAddress > &ufs, InterpretationConstPtr interpretation)
	Constructs a nogood which encodes the essence of an unfounded set using one of the overloaded versions of the method.
Nogood	getUFSNogoodReductBased (const std::vector< IDAddress > &ufs, InterpretationConstPtr interpretation)
	Constructs a nogood which encodes the essence of an unfounded set based on the reduct.
Nogood	getUFSNogoodUFSBased (const std::vector< IDAddress > &ufs, InterpretationConstPtr interpretation)
	Constructs a nogood which encodes the essence of an unfounded set based on the UFS itself.
Protected Types
enum	Mode { Ordinary, WithExt }
Protected Member Functions
bool	isUnfoundedSet (InterpretationConstPtr compatibleSet, InterpretationConstPtr compatibleSetWithoutAux, InterpretationConstPtr ufsCandidate)
	Checks if an UFS candidate is actually an unfounded set.
virtual std::pair< bool, Nogood >	nogoodTransformation (Nogood ng, InterpretationConstPtr compatibleSet)=0
	Transforms a nogood (valid input-output relationship of some external atom) learned in the main search for being used in the UFS search.
Protected Attributes
BaseModelGenerator *	mg
	Reference to the model generator which shall be used for evaluating external atoms.
Mode	mode
	Defines the mode of the UFS checker (ordinary or WithExt).
ProgramCtx &	ctx
	Program context.
RegistryPtr	reg
	Registry.
const OrdinaryASPProgram &	groundProgram
	The ground program for which the UFS checker is used.
AnnotatedGroundProgram	emptyagp
	Empty AnnotatedGroundProgram.
const AnnotatedGroundProgram &	agp
	UnfoundedSetChecker::groundProgram with additional meta information.
InterpretationConstPtr	componentAtoms
	Set of all atoms in the component of the UFS checker.
ExternalAtomVerificationTree	eavTree
	Tree representation of GenuineGuessAndCheckModelGenerator::learnedEANogoods for verification purposes.
SimpleNogoodContainerPtr	ngc
	Set of nogoods to be learned during UFS detection.
InterpretationPtr	domain
	Domain of all problem variables.
SATSolverPtr	solver
	Satisfiability solver for evaluating the UFS detection problem.
Private Member Functions
bool	verifyExternalAtomByEvaluation (ID eaID, InterpretationConstPtr ufsCandidate, InterpretationConstPtr compatibleSet, UnfoundedSetVerificationStatus &ufsVerStatus)
	Explicitly evaluates an external atom and verifies or falsifies the auxiliaries which depend on it.

Detailed Description

Unfounded set checker for HEX programs (with external atoms).

Definition at line 54 of file UnfoundedSetChecker.h.

Member Typedef Documentation

typedef boost::shared_ptr<const UnfoundedSetChecker> UnfoundedSetChecker::ConstPtr

Definition at line 257 of file UnfoundedSetChecker.h.

typedef boost::shared_ptr<UnfoundedSetChecker> UnfoundedSetChecker::Ptr

Definition at line 256 of file UnfoundedSetChecker.h.

Member Enumeration Documentation

enum UnfoundedSetChecker::Mode [protected]

Enumerator:

Ordinary	Consider external atoms as ordinary ones.
WithExt	Consider external atoms as such (requires ggncmg to be set).

Definition at line 60 of file UnfoundedSetChecker.h.

Constructor & Destructor Documentation

DLVHEX_NAMESPACE_BEGIN UnfoundedSetChecker::UnfoundedSetChecker	(	ProgramCtx &	ctx,
		const OrdinaryASPProgram &	groundProgram,
		InterpretationConstPtr	componentAtoms = `InterpretationConstPtr()`,
		SimpleNogoodContainerPtr	ngc = `SimpleNogoodContainerPtr()`
	)

Initialization for UFS search considering external atoms as ordinary ones.

Parameters:

groundProgram	Ground program over which the ufs check is done.
componentAtoms	The atoms in the strongly connected component in the atom dependency graph; if NULL, then all atoms in groundProgram are considered to be in the SCC.
ngc	Set of valid input-output relationships learned in the main search (to be extended by this UFS checker).

Definition at line 61 of file UnfoundedSetChecker.cpp.

References DBGLOG, OrdinaryASPProgram::idb, mode, Ordinary, reg, and ProgramCtx::registry().

UnfoundedSetChecker::UnfoundedSetChecker	(	BaseModelGenerator *	mg,
		ProgramCtx &	ctx,
		const OrdinaryASPProgram &	groundProgram,
		const AnnotatedGroundProgram &	agp,
		InterpretationConstPtr	componentAtoms = `InterpretationConstPtr()`,
		SimpleNogoodContainerPtr	ngc = `SimpleNogoodContainerPtr()`
	)

Initialization for UFS search under consideration of the semantics of external atoms.

Parameters:

ggncmg	Reference to the G&C model generator for which this UnfoundedSetChecker runs.
ctx	ProgramCtx.
groundProgram	Ground program over which the ufs check is done.
agp	Annotated version of the ground program; may be a superset of groundProgram, but must contain meta information about all external atoms in groundProgram.
componentAtoms	The atoms in the strongly connected component in the atom dependency graph; if 0, then all atoms in groundProgram are considered to be in the SCC.
ngc	Set of valid input-output relationships learned in the main search (to be extended by this UFS checker).

Definition at line 82 of file UnfoundedSetChecker.cpp.

References DBGLOG, OrdinaryASPProgram::idb, mode, reg, ProgramCtx::registry(), and WithExt.

virtual UnfoundedSetChecker::~UnfoundedSetChecker ( ) [inline, virtual]

Definition at line 202 of file UnfoundedSetChecker.h.

Member Function Documentation

Nogood UnfoundedSetChecker::getUFSNogood	(	const std::vector< IDAddress > &	ufs,
		InterpretationConstPtr	interpretation
	)

Constructs a nogood which encodes the essence of an unfounded set using one of the overloaded versions of the method.

Parameters:

ufs	The unfounded set to construct the nogood for.
interpretation	The interpretation which was used to compute the unfounded set for.

Returns:: The UFS-nogood.

Definition at line 341 of file UnfoundedSetChecker.cpp.

References ProgramCtx::config, ctx, DBGLOG, Configuration::getOption(), getUFSNogoodReductBased(), getUFSNogoodUFSBased(), and reg.

Nogood UnfoundedSetChecker::getUFSNogoodReductBased	(	const std::vector< IDAddress > &	ufs,
		InterpretationConstPtr	interpretation
	)

Constructs a nogood which encodes the essence of an unfounded set based on the reduct.

Parameters:

ufs	The unfounded set to construct the nogood for.
interpretation	The interpretation which was used to compute the unfounded set for.

Returns:: The UFS-nogood.

Definition at line 362 of file UnfoundedSetChecker.cpp.

References ID::address, Rule::body, NogoodContainer::createLiteral(), DBGLOG, groundProgram, OrdinaryASPProgram::idb, Nogood::insert(), ID::isNaf(), and reg.

Referenced by getUFSNogood().

Nogood UnfoundedSetChecker::getUFSNogoodUFSBased	(	const std::vector< IDAddress > &	ufs,
		InterpretationConstPtr	interpretation
	)

Constructs a nogood which encodes the essence of an unfounded set based on the UFS itself.

Parameters:

ufs	The unfounded set to construct the nogood for.
interpretation	The interpretation which was used to compute the unfounded set for.

Returns:: The UFS-nogood.

Definition at line 424 of file UnfoundedSetChecker.cpp.

References ID::address, agp, Rule::body, NogoodContainer::createLiteral(), DBGLOG, domain, AnnotatedGroundProgram::getAuxToEA(), AnnotatedGroundProgram::getProgramMask(), Nogood::getStringRepresentation(), groundProgram, Rule::head, OrdinaryASPProgram::idb, Nogood::insert(), Rule::isEAGuessingRule(), ID::isExternalAuxiliary(), ID::isNaf(), AnnotatedGroundProgram::mapsAux(), mg, mode, Ordinary, reg, and RawPrinter::toString().

Referenced by getUFSNogood().

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

Returns an unfounded set of groundProgram with respect to a compatibleSet; If the empty set is returned, then there does not exist a greater (nonempty) unfounded set.

The method supports also unfounded set detection over partial interpretations. For this purpose, skipProgram specifies all rules which shall be ignored in the search. The interpretation must be complete and compatible over the non-ignored part. Each detected unfounded set will remain an unfounded set for all possible completions of the interpretation.

Parameters:

compatibleSet	The interpretation for which we want to compute an unfounded set.
skipProgram	The set of rules which shall be ignored in the UFS check (because the assignment might be incomplete wrt. these rules).

Returns:: An unfounded set (might be of size 0).

Implemented in AssumptionBasedUnfoundedSetChecker, and EncodingBasedUnfoundedSetChecker.

bool UnfoundedSetChecker::isUnfoundedSet	(	InterpretationConstPtr	compatibleSet,
		InterpretationConstPtr	compatibleSetWithoutAux,
		InterpretationConstPtr	ufsCandidate
	)		`[protected]`

Checks if an UFS candidate is actually an unfounded set.

Parameters:

compatibleSet	The interpretation over which we compute UFSs.
compatibleSetWithoutAux	The interpretation over which we compute UFSs (without EA replacements).
ufsCandidate	A candidate unfounded set (solution to the nogood set created by getUFSDetectionProblem).

Returns:: True if ufsCandidate is an unfounded set and false otherwise.

Definition at line 105 of file UnfoundedSetChecker.cpp.

References ID::address, agp, AnnotatedGroundProgram::allowsForVerificationUsingCompleteSupportSets(), UnfoundedSetChecker::UnfoundedSetVerificationStatus::auxiliariesToVerify, ProgramCtx::config, ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, domain, UnfoundedSetChecker::UnfoundedSetVerificationStatus::externalAtomAddressToAuxIndices, ExternalAtom::getExtSourceProperties(), AnnotatedGroundProgram::getIndexedEAtom(), AnnotatedGroundProgram::getIndexedEAtoms(), Configuration::getOption(), mode, ExtSourceProperties::providesCompleteNegativeSupportSets(), ExtSourceProperties::providesCompletePositiveSupportSets(), reg, verifyExternalAtomByEvaluation(), AnnotatedGroundProgram::verifyExternalAtomsUsingCompleteSupportSets(), and WithExt.

Referenced by EncodingBasedUnfoundedSetChecker::getUnfoundedSet(), and AssumptionBasedUnfoundedSetChecker::getUnfoundedSet().

virtual void UnfoundedSetChecker::learnNogoodsFromMainSearch ( bool reset ) [pure virtual]

Forces the unfounded set checker to learn nogoods from main search now.

Implemented in AssumptionBasedUnfoundedSetChecker, and EncodingBasedUnfoundedSetChecker.

virtual std::pair<bool, Nogood> UnfoundedSetChecker::nogoodTransformation	(	Nogood	ng,
		InterpretationConstPtr	compatibleSet
	)		`[protected, pure 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.

Implemented in AssumptionBasedUnfoundedSetChecker, and EncodingBasedUnfoundedSetChecker.

Referenced by verifyExternalAtomByEvaluation().

bool UnfoundedSetChecker::verifyExternalAtomByEvaluation	(	ID	eaID,
		InterpretationConstPtr	ufsCandidate,
		InterpretationConstPtr	compatibleSet,
		UnfoundedSetVerificationStatus &	ufsVerStatus
	)		`[private]`

Explicitly evaluates an external atom and verifies or falsifies the auxiliaries which depend on it.

Parameters:

ufsCandidate	Representation of the UFS candidate.
compatibleSet	Compatible Set.
ufsVerStatus	Represents the current verification status (to be prepared by indexEatomsForUfsVerification).

Returns:: True if verification succeeded and false otherwise.

Definition at line 236 of file UnfoundedSetChecker.cpp.

References ExternalAtomVerificationTree::addNogood(), ID::address, UnfoundedSetChecker::UnfoundedSetVerificationStatus::auxiliariesToVerify, UnfoundedSetChecker::UnfoundedSetVerificationStatus::auxIndexToRemainingExternalAtoms, ProgramCtx::config, ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_COUNT, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, UnfoundedSetChecker::UnfoundedSetVerificationStatus::eaInput, eavTree, BaseModelGenerator::evaluateExternalAtom(), UnfoundedSetChecker::UnfoundedSetVerificationStatus::externalAtomAddressToAuxIndices, Configuration::getOption(), Nogood::getStringRepresentation(), ExternalAtomVerificationTree::getVerifiedAuxiliaries(), Nogood::isGround(), mg, ngc, nogoodTransformation(), reg, ProgramCtx::registry(), and solver.

Referenced by isUnfoundedSet().

Field Documentation

const AnnotatedGroundProgram& UnfoundedSetChecker::agp [protected]

UnfoundedSetChecker::groundProgram with additional meta information.

Definition at line 81 of file UnfoundedSetChecker.h.

Referenced by AssumptionBasedUnfoundedSetChecker::constructDomain(), AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemBasicEABehavior(), EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemNecessaryPart(), EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemOptimizationPartBasicEAKnowledge(), getUFSNogoodUFSBased(), and isUnfoundedSet().

InterpretationConstPtr UnfoundedSetChecker::componentAtoms [protected]

Set of all atoms in the component of the UFS checker.

Definition at line 83 of file UnfoundedSetChecker.h.

Referenced by EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemNecessaryPart(), and AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemRestrictToSCC().

ProgramCtx& UnfoundedSetChecker::ctx [protected]

Program context.

Definition at line 71 of file UnfoundedSetChecker.h.

Referenced by AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemAndInstantiateSolver(), EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemNecessaryPart(), AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemRule(), getUFSNogood(), EncodingBasedUnfoundedSetChecker::getUnfoundedSet(), isUnfoundedSet(), AssumptionBasedUnfoundedSetChecker::learnNogoodsFromMainSearch(), and verifyExternalAtomByEvaluation().

InterpretationPtr UnfoundedSetChecker::domain [protected]

Domain of all problem variables.

Definition at line 89 of file UnfoundedSetChecker.h.

ExternalAtomVerificationTree UnfoundedSetChecker::eavTree [protected]

Tree representation of GenuineGuessAndCheckModelGenerator::learnedEANogoods for verification purposes.

Definition at line 85 of file UnfoundedSetChecker.h.

Referenced by AssumptionBasedUnfoundedSetChecker::learnNogoodsFromMainSearch(), and verifyExternalAtomByEvaluation().

AnnotatedGroundProgram UnfoundedSetChecker::emptyagp [protected]

Empty AnnotatedGroundProgram.

Definition at line 79 of file UnfoundedSetChecker.h.

const OrdinaryASPProgram& UnfoundedSetChecker::groundProgram [protected]

The ground program for which the UFS checker is used.

Definition at line 77 of file UnfoundedSetChecker.h.

Referenced by AssumptionBasedUnfoundedSetChecker::constructDomain(), AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemAndInstantiateSolver(), AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemFacts(), EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemNecessaryPart(), AssumptionBasedUnfoundedSetChecker::expandUFSDetectionProblemAndReinstantiateSolver(), getUFSNogoodReductBased(), getUFSNogoodUFSBased(), EncodingBasedUnfoundedSetChecker::getUnfoundedSet(), and AssumptionBasedUnfoundedSetChecker::getUnfoundedSet().

BaseModelGenerator* UnfoundedSetChecker::mg [protected]

Reference to the model generator which shall be used for evaluating external atoms.

Can be NULL if the UFS checker runs in ordinary mode.

Definition at line 58 of file UnfoundedSetChecker.h.

Referenced by AssumptionBasedUnfoundedSetChecker::constructDomain(), AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemRule(), getUFSNogoodUFSBased(), EncodingBasedUnfoundedSetChecker::getUnfoundedSet(), and verifyExternalAtomByEvaluation().

Mode UnfoundedSetChecker::mode [protected]

Defines the mode of the UFS checker (ordinary or WithExt).

Definition at line 68 of file UnfoundedSetChecker.h.

SimpleNogoodContainerPtr UnfoundedSetChecker::ngc [protected]

Set of nogoods to be learned during UFS detection.

Definition at line 87 of file UnfoundedSetChecker.h.

Referenced by EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemOptimizationPart(), EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemOptimizationPartLearnedFromMainSearch(), AssumptionBasedUnfoundedSetChecker::learnNogoodsFromMainSearch(), and verifyExternalAtomByEvaluation().

RegistryPtr UnfoundedSetChecker::reg [protected]

Registry.

Definition at line 73 of file UnfoundedSetChecker.h.

SATSolverPtr UnfoundedSetChecker::solver [protected]

Satisfiability solver for evaluating the UFS detection problem.

AssumptionBasedUnfoundedSetChecker, solver is defined during the whole lifetime of the object. An EncodingBasedUnfoundedSetChecker, solver is only defined while getUnfoundedSet runs.

Definition at line 97 of file UnfoundedSetChecker.h.

Referenced by AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemAndInstantiateSolver(), AssumptionBasedUnfoundedSetChecker::expandUFSDetectionProblemAndReinstantiateSolver(), EncodingBasedUnfoundedSetChecker::getUnfoundedSet(), AssumptionBasedUnfoundedSetChecker::getUnfoundedSet(), AssumptionBasedUnfoundedSetChecker::learnNogoodsFromMainSearch(), AssumptionBasedUnfoundedSetChecker::setAssumptions(), and verifyExternalAtomByEvaluation().

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

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

Data Structures

Public Types

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Private Member Functions

Detailed Description

Member Typedef Documentation

Member Enumeration Documentation

Constructor & Destructor Documentation

Member Function Documentation

Field Documentation