#include <include/dlvhex2/UnfoundedSetChecker.h>

Inheritance diagram for AssumptionBasedUnfoundedSetChecker:

Collaboration diagram for AssumptionBasedUnfoundedSetChecker:

Public Member Functions
	AssumptionBasedUnfoundedSetChecker (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).
	AssumptionBasedUnfoundedSetChecker (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 the unfounded set checker 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	constructDomain ()
	Goes through EDB and IDB and sets all facts in domain.
void	constructUFSDetectionProblemFacts (NogoodSet &ns)
	Encodes that facts cannot be in the unfounded set.
void	constructUFSDetectionProblemCreateAuxAtoms ()
	Sets up interpretationShadow and residualShadow.
void	constructUFSDetectionProblemDefineAuxiliaries (NogoodSet &ns)
	Defines the auxiliary variables.
void	constructUFSDetectionProblemRule (NogoodSet &ns, ID ruleID)
	Encodes a given program rule.
void	constructUFSDetectionProblemNonempty (NogoodSet &ns)
	Encodes that we are looking for a nonempty unfounded set.
void	constructUFSDetectionProblemRestrictToSCC (NogoodSet &ns)
	Restricts the search to the current strongly connected component.
void	constructUFSDetectionProblemBasicEABehavior (NogoodSet &ns)
	Optimization: Basic behavior of external atoms.
void	constructUFSDetectionProblemAndInstantiateSolver ()
	Constructs the nogood set used for unfounded set detection and instantiates the solver.
void	expandUFSDetectionProblemAndReinstantiateSolver ()
	Extends the nogood set used for unfounded set detection and reinstantiates the solver.
void	setAssumptions (InterpretationConstPtr compatibleSet, const std::set< ID > &skipProgram)
	Prepares the list of assumptions for an unfounded set search over a given compatible set.
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.
Private Attributes
boost::unordered_map < IDAddress, IDAddress >	interpretationShadow
	A special atom "a_i" for each atom "a" in the program, representing the truth value of "a" in the compatible set.
boost::unordered_map < IDAddress, IDAddress >	residualShadow
	A special atom "a_j" for each atom "a" in the program, representing the truth value of "a" in I u -X.
boost::unordered_map < IDAddress, IDAddress >	becomeFalse
	A special atom "a_f" for each atom "a" in the program, representing a change from of the truth value of a from true in I to false in I u -X.
boost::unordered_map < IDAddress, IDAddress >	IandU
	A special atom "a_{IandU}" for each atom "a" in the program, representing that a is true in I and member of U.
boost::unordered_map < IDAddress, IDAddress >	nIorU
	A special atom "a_{\overline{I}orU}" for each atom "a" in the program, representing that a is false in I or member of U.
int	atomcnt
	Counter for auxiliary atoms.
int	problemRuleCount
	Number of program rules respected in the encoding (allows for incremental addition of further rules).
ID	hookAtom
	Allows for extension of the problem encoding when additional rules are added.
int	learnedNogoodsFromMainSearch

Detailed Description

Definition at line 454 of file UnfoundedSetChecker.h.

Constructor & Destructor Documentation

AssumptionBasedUnfoundedSetChecker::AssumptionBasedUnfoundedSetChecker	(	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 1826 of file UnfoundedSetChecker.cpp.

References constructUFSDetectionProblemAndInstantiateSolver(), DBGLOG, OrdinaryASPProgram::edb, OrdinaryASPProgram::idb, learnedNogoodsFromMainSearch, RawPrinter::print(), UnfoundedSetChecker::reg, and ProgramCtx::registry().

AssumptionBasedUnfoundedSetChecker::AssumptionBasedUnfoundedSetChecker	(	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 1854 of file UnfoundedSetChecker.cpp.

References constructUFSDetectionProblemAndInstantiateSolver(), DBGLOG, OrdinaryASPProgram::edb, OrdinaryASPProgram::idb, learnedNogoodsFromMainSearch, RawPrinter::print(), UnfoundedSetChecker::reg, and ProgramCtx::registry().

Member Function Documentation

void AssumptionBasedUnfoundedSetChecker::constructDomain ( ) [private]

Goes through EDB and IDB and sets all facts in domain.

Definition at line 1242 of file UnfoundedSetChecker.cpp.

References ID::address, UnfoundedSetChecker::agp, Rule::body, UnfoundedSetChecker::domain, OrdinaryASPProgram::edb, AnnotatedGroundProgram::getAuxToEA(), UnfoundedSetChecker::groundProgram, Rule::head, OrdinaryASPProgram::idb, Rule::isEAGuessingRule(), ID::isExternalAuxiliary(), AnnotatedGroundProgram::mapsAux(), UnfoundedSetChecker::mg, UnfoundedSetChecker::mode, UnfoundedSetChecker::reg, and UnfoundedSetChecker::WithExt.

Referenced by constructUFSDetectionProblemAndInstantiateSolver(), and expandUFSDetectionProblemAndReinstantiateSolver().

void AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemAndInstantiateSolver ( ) [private]

Constructs the nogood set used for unfounded set detection and instantiates the solver.

Definition at line 1665 of file UnfoundedSetChecker.cpp.

References atomcnt, constructDomain(), constructUFSDetectionProblemBasicEABehavior(), constructUFSDetectionProblemCreateAuxAtoms(), constructUFSDetectionProblemDefineAuxiliaries(), constructUFSDetectionProblemFacts(), constructUFSDetectionProblemNonempty(), constructUFSDetectionProblemRestrictToSCC(), constructUFSDetectionProblemRule(), UnfoundedSetChecker::ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, UnfoundedSetChecker::domain, SATSolver::getInstance(), UnfoundedSetChecker::groundProgram, hookAtom, OrdinaryASPProgram::idb, interpretationShadow, ID::MAINKIND_ATOM, problemRuleCount, ID::PROPERTY_ATOM_HIDDEN, ID::PROPERTY_AUX, UnfoundedSetChecker::reg, UnfoundedSetChecker::solver, ID::SUBKIND_ATOM_ORDINARYG, and Atom::tuple.

Referenced by AssumptionBasedUnfoundedSetChecker().

void AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemBasicEABehavior ( NogoodSet & ns ) [private]

Optimization: Basic behavior of external atoms.

Parameters:

ns	The nogood set to add the nogodos to.

Definition at line 1615 of file UnfoundedSetChecker.cpp.

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

Referenced by constructUFSDetectionProblemAndInstantiateSolver(), and expandUFSDetectionProblemAndReinstantiateSolver().

void AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemCreateAuxAtoms ( ) [private]

Sets up interpretationShadow and residualShadow.

Definition at line 1291 of file UnfoundedSetChecker.cpp.

References atomcnt, becomeFalse, UnfoundedSetChecker::domain, IandU, interpretationShadow, ID::MAINKIND_ATOM, UnfoundedSetChecker::mode, nIorU, UnfoundedSetChecker::Ordinary, ID::PROPERTY_ATOM_HIDDEN, ID::PROPERTY_AUX, UnfoundedSetChecker::reg, residualShadow, ID::SUBKIND_ATOM_ORDINARYG, and Atom::tuple.

Referenced by constructUFSDetectionProblemAndInstantiateSolver(), and expandUFSDetectionProblemAndReinstantiateSolver().

void AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemDefineAuxiliaries ( NogoodSet & ns ) [private]

Defines the auxiliary variables.

Parameters:

ns	The nogood set to add the nogodos to.

Definition at line 1426 of file UnfoundedSetChecker.cpp.

References NogoodSet::addNogood(), ID::address, becomeFalse, NogoodContainer::createLiteral(), DBGLOG, UnfoundedSetChecker::domain, IandU, Nogood::insert(), interpretationShadow, UnfoundedSetChecker::mode, nIorU, UnfoundedSetChecker::Ordinary, UnfoundedSetChecker::reg, and residualShadow.

Referenced by constructUFSDetectionProblemAndInstantiateSolver(), and expandUFSDetectionProblemAndReinstantiateSolver().

void AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemFacts ( NogoodSet & ns ) [private]

Encodes that facts cannot be in the unfounded set.

Definition at line 1274 of file UnfoundedSetChecker.cpp.

References NogoodSet::addNogood(), NogoodContainer::createLiteral(), DBGLOG, OrdinaryASPProgram::edb, UnfoundedSetChecker::groundProgram, and Nogood::insert().

Referenced by constructUFSDetectionProblemAndInstantiateSolver(), and expandUFSDetectionProblemAndReinstantiateSolver().

void AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemNonempty ( NogoodSet & ns ) [private]

Encodes that we are looking for a nonempty unfounded set.

Parameters:

ns	The nogood set to add the nogodos to.

Definition at line 1572 of file UnfoundedSetChecker.cpp.

References NogoodSet::addNogood(), ID::address, NogoodContainer::createLiteral(), DBGLOG, UnfoundedSetChecker::domain, hookAtom, Nogood::insert(), UnfoundedSetChecker::mode, UnfoundedSetChecker::Ordinary, and UnfoundedSetChecker::reg.

Referenced by constructUFSDetectionProblemAndInstantiateSolver(), and expandUFSDetectionProblemAndReinstantiateSolver().

void AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemRestrictToSCC ( NogoodSet & ns ) [private]

Restricts the search to the current strongly connected component.

Parameters:

ns	The nogood set to add the nogodos to.

Definition at line 1592 of file UnfoundedSetChecker.cpp.

References NogoodSet::addNogood(), ID::address, UnfoundedSetChecker::componentAtoms, NogoodContainer::createLiteral(), DBGLOG, UnfoundedSetChecker::domain, hookAtom, Nogood::insert(), UnfoundedSetChecker::mode, UnfoundedSetChecker::Ordinary, and UnfoundedSetChecker::reg.

Referenced by constructUFSDetectionProblemAndInstantiateSolver(), and expandUFSDetectionProblemAndReinstantiateSolver().

void AssumptionBasedUnfoundedSetChecker::constructUFSDetectionProblemRule	(	NogoodSet &	ns,
		ID	ruleID
	)		`[private]`

Encodes a given program rule.

Parameters:

ns	The nogood set to add the nogodos to.
ruleID	Rule to encode.

Definition at line 1324 of file UnfoundedSetChecker.cpp.

References NogoodSet::addNogood(), ID::address, atomcnt, Rule::body, ProgramCtx::config, NogoodContainer::createLiteral(), UnfoundedSetChecker::ctx, DBGLOG, Configuration::getOption(), Rule::head, IandU, Nogood::insert(), interpretationShadow, Rule::isEAGuessingRule(), ID::isExternalAuxiliary(), ID::isNaf(), ID::isWeightRule(), LOG, ID::MAINKIND_ATOM, UnfoundedSetChecker::mg, UnfoundedSetChecker::mode, nIorU, UnfoundedSetChecker::Ordinary, RawPrinter::print(), ID::PROPERTY_ATOM_HIDDEN, ID::PROPERTY_AUX, UnfoundedSetChecker::reg, ID::SUBKIND_ATOM_ORDINARYG, Atom::tuple, and WARNING().

Referenced by constructUFSDetectionProblemAndInstantiateSolver(), and expandUFSDetectionProblemAndReinstantiateSolver().

void AssumptionBasedUnfoundedSetChecker::expandUFSDetectionProblemAndReinstantiateSolver ( ) [private]

Extends the nogood set used for unfounded set detection and reinstantiates the solver.

Definition at line 1725 of file UnfoundedSetChecker.cpp.

References atomcnt, constructDomain(), constructUFSDetectionProblemBasicEABehavior(), constructUFSDetectionProblemCreateAuxAtoms(), constructUFSDetectionProblemDefineAuxiliaries(), constructUFSDetectionProblemFacts(), constructUFSDetectionProblemNonempty(), constructUFSDetectionProblemRestrictToSCC(), constructUFSDetectionProblemRule(), DBGLOG, UnfoundedSetChecker::domain, UnfoundedSetChecker::groundProgram, hookAtom, OrdinaryASPProgram::idb, ID::MAINKIND_ATOM, problemRuleCount, ID::PROPERTY_ATOM_HIDDEN, ID::PROPERTY_AUX, UnfoundedSetChecker::reg, UnfoundedSetChecker::solver, ID::SUBKIND_ATOM_ORDINARYG, and Atom::tuple.

Referenced by getUnfoundedSet().

std::vector< IDAddress > AssumptionBasedUnfoundedSetChecker::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 1980 of file UnfoundedSetChecker.cpp.

References DBGLOG, DLVHEX_BENCHMARK_REGISTER, DLVHEX_BENCHMARK_REGISTER_AND_COUNT, DLVHEX_BENCHMARK_START, DLVHEX_BENCHMARK_STOP, UnfoundedSetChecker::domain, expandUFSDetectionProblemAndReinstantiateSolver(), UnfoundedSetChecker::groundProgram, OrdinaryASPProgram::idb, UnfoundedSetChecker::isUnfoundedSet(), learnNogoodsFromMainSearch(), UnfoundedSetChecker::mode, UnfoundedSetChecker::Ordinary, problemRuleCount, setAssumptions(), UnfoundedSetChecker::solver, and UnfoundedSetChecker::WithExt.

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

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

Implements UnfoundedSetChecker.

Definition at line 1951 of file UnfoundedSetChecker.cpp.

References ExternalAtomVerificationTree::addNogood(), ProgramCtx::config, UnfoundedSetChecker::ctx, DBGLOG, UnfoundedSetChecker::eavTree, Configuration::getOption(), Nogood::getStringRepresentation(), Nogood::isGround(), learnedNogoodsFromMainSearch, UnfoundedSetChecker::ngc, nogoodTransformation(), UnfoundedSetChecker::reg, and UnfoundedSetChecker::solver.

Referenced by getUnfoundedSet().

std::pair< bool, Nogood > AssumptionBasedUnfoundedSetChecker::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 1884 of file UnfoundedSetChecker.cpp.

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

Referenced by learnNogoodsFromMainSearch().

void AssumptionBasedUnfoundedSetChecker::setAssumptions	(	InterpretationConstPtr	compatibleSet,
		const std::set< ID > &	skipProgram
	)		`[private]`

Prepares the list of assumptions for an unfounded set search over a given compatible set.

Parameters:

compatibleSet	The compatible set over which we do the UFS search
skipProgram	The set of rules ignored in the UFS check

Definition at line 1770 of file UnfoundedSetChecker.cpp.

References ID::address, DBGLOG, UnfoundedSetChecker::domain, Rule::head, hookAtom, interpretationShadow, ID::isNaf(), UnfoundedSetChecker::mode, ID::NAF_MASK, ID::nafLiteralFromAtom(), UnfoundedSetChecker::Ordinary, ID::posLiteralFromAtom(), UnfoundedSetChecker::reg, and UnfoundedSetChecker::solver.

Referenced by getUnfoundedSet().

Field Documentation

int AssumptionBasedUnfoundedSetChecker::atomcnt [private]

Counter for auxiliary atoms.

Definition at line 469 of file UnfoundedSetChecker.h.

Referenced by constructUFSDetectionProblemAndInstantiateSolver(), constructUFSDetectionProblemCreateAuxAtoms(), constructUFSDetectionProblemRule(), and expandUFSDetectionProblemAndReinstantiateSolver().

boost::unordered_map<IDAddress, IDAddress> AssumptionBasedUnfoundedSetChecker::becomeFalse [private]

A special atom "a_f" for each atom "a" in the program, representing a change from of the truth value of a from true in I to false in I u -X.

Definition at line 462 of file UnfoundedSetChecker.h.

Referenced by constructUFSDetectionProblemBasicEABehavior(), constructUFSDetectionProblemCreateAuxAtoms(), and constructUFSDetectionProblemDefineAuxiliaries().

ID AssumptionBasedUnfoundedSetChecker::hookAtom [private]

Allows for extension of the problem encoding when additional rules are added.

Definition at line 475 of file UnfoundedSetChecker.h.

Referenced by constructUFSDetectionProblemAndInstantiateSolver(), constructUFSDetectionProblemBasicEABehavior(), constructUFSDetectionProblemNonempty(), constructUFSDetectionProblemRestrictToSCC(), expandUFSDetectionProblemAndReinstantiateSolver(), and setAssumptions().

boost::unordered_map<IDAddress, IDAddress> AssumptionBasedUnfoundedSetChecker::IandU [private]

A special atom "a_{IandU}" for each atom "a" in the program, representing that a is true in I and member of U.

Definition at line 464 of file UnfoundedSetChecker.h.

Referenced by constructUFSDetectionProblemCreateAuxAtoms(), constructUFSDetectionProblemDefineAuxiliaries(), and constructUFSDetectionProblemRule().

boost::unordered_map<IDAddress, IDAddress> AssumptionBasedUnfoundedSetChecker::interpretationShadow [private]

A special atom "a_i" for each atom "a" in the program, representing the truth value of "a" in the compatible set.

Definition at line 458 of file UnfoundedSetChecker.h.

Referenced by constructUFSDetectionProblemAndInstantiateSolver(), constructUFSDetectionProblemBasicEABehavior(), constructUFSDetectionProblemCreateAuxAtoms(), constructUFSDetectionProblemDefineAuxiliaries(), constructUFSDetectionProblemRule(), nogoodTransformation(), and setAssumptions().

int AssumptionBasedUnfoundedSetChecker::learnedNogoodsFromMainSearch [private]

Definition at line 478 of file UnfoundedSetChecker.h.

Referenced by AssumptionBasedUnfoundedSetChecker(), and learnNogoodsFromMainSearch().

boost::unordered_map<IDAddress, IDAddress> AssumptionBasedUnfoundedSetChecker::nIorU [private]

A special atom "a_{\overline{I}orU}" for each atom "a" in the program, representing that a is false in I or member of U.

Definition at line 466 of file UnfoundedSetChecker.h.

Referenced by constructUFSDetectionProblemCreateAuxAtoms(), constructUFSDetectionProblemDefineAuxiliaries(), and constructUFSDetectionProblemRule().

int AssumptionBasedUnfoundedSetChecker::problemRuleCount [private]

Number of program rules respected in the encoding (allows for incremental addition of further rules).

Definition at line 472 of file UnfoundedSetChecker.h.

Referenced by constructUFSDetectionProblemAndInstantiateSolver(), expandUFSDetectionProblemAndReinstantiateSolver(), and getUnfoundedSet().

boost::unordered_map<IDAddress, IDAddress> AssumptionBasedUnfoundedSetChecker::residualShadow [private]

A special atom "a_j" for each atom "a" in the program, representing the truth value of "a" in I u -X.

Definition at line 460 of file UnfoundedSetChecker.h.

Referenced by constructUFSDetectionProblemCreateAuxAtoms(), constructUFSDetectionProblemDefineAuxiliaries(), and nogoodTransformation().

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

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

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Field Documentation