Stores a set of signed literals which cannot be simultanously true. More...

#include <include/dlvhex2/Nogood.h>

Inheritance diagram for Nogood:

Collaboration diagram for Nogood:

Public Member Functions
	Nogood ()
	Constructs an empty nogood.
	Nogood (InterpretationConstPtr assigned, InterpretationConstPtr interpretation)
	Constructs a nogood from an interpretation.
void	recomputeHash ()
	Recomputes the hash after literals were added.
size_t	getHash ()
	Returns the hash of the nogood.
const Nogood &	operator= (const Nogood &other)
	Overwrites the contents of the nogood with a new one.
bool	operator== (const Nogood &ng2) const
	Compares the nogood to another one.
bool	operator!= (const Nogood &ng2) const
	Compares the nogood to another one.
std::ostream &	print (std::ostream &o) const
	Prints the nogood in numeric format.
std::string	getStringRepresentation (RegistryPtr reg) const
	Prints the nogood in string format.
Nogood	resolve (const Nogood &ng2, IDAddress groundlitadr)
	Performs resolution on this nogood with another one using a given ground literal.
Nogood	resolve (const Nogood &ng2, ID lit)
	Performs resolution on this nogood with another one using a given literal ID.
void	applyVariableSubstitution (RegistryPtr reg, const std::map< ID, ID > &subst)
	Substitutes variables in this (nonground) nogood.
void	heuristicNormalization (RegistryPtr reg)
	Renames variables in this nogoods.
void	insert (ID lit)
	Adds a literal to this nogood.
template<class InputIterator >
void	insert (InputIterator begin, InputIterator end)
bool	isGround () const
	Checks groundness of this nogood.
bool	match (RegistryPtr reg, ID atomID, Nogood &instance) const
	Checks if there is a substitution of variables in this nogood such that `atomID` occurs in the substitution and computes the instance of the nogood in that case.
std::string	dbgsave () const
void	dbgload (std::string str)
Private Attributes
std::size_t	hashValue
	Hash value of the nogood for indexing purposes.
bool	ground
	True if the nogood is ground and false otherwise.

Detailed Description

Stores a set of signed literals which cannot be simultanously true.

A nogood is used to restrict the search space. To this end, they contain signed literals (that is, positive or negative atoms) which cannot be simultanously true in a compatible set.

In dlvhex, they are mainly used to encode conditions which contradict the semantics of external atoms. For instance, the nogood { p(a), -q(a), -&diff[p,q](a) } encodes that whenever the atom p(a) is true and the atom q(a) is false, then the atom &diff[p,q](a) must be true (i.e. must not be false) since constant a will be in the output of the set difference of p and q.

Note: For constructing external source output atoms (such as &diff[p,q](a)), use the method ExternalLearningHelper::getOutputAtom.

Nogoods can be added to the reasoner in the method PluginAtom::retrieve. When adding dlvhex IDs to a nogood, they need to be passed through NogoodContainer::createLiteral to strip off property flags (Nogood::insert performs this step automatically).

Definition at line 72 of file Nogood.h.

Constructor & Destructor Documentation

Nogood::Nogood ( )

Constructs an empty nogood.

Definition at line 69 of file Nogood.cpp.

Nogood::Nogood	(	InterpretationConstPtr	assigned,
		InterpretationConstPtr	interpretation
	)

Constructs a nogood from an interpretation.

Parameters:

assigned	Set of atoms to respect.
interpretation	Truth values of the atoms in `assigned`.

Definition at line 73 of file Nogood.cpp.

References NogoodContainer::createLiteral(), and insert().

Member Function Documentation

void Nogood::applyVariableSubstitution	(	RegistryPtr	reg,
		const std::map< ID, ID > &	subst
	)

Substitutes variables in this (nonground) nogood.

Parameters:

reg	Registry used to resolve literal IDs.
subst	Variable substitution of pairs (X,Y) to replace variable X by Y.

Definition at line 203 of file Nogood.cpp.

References ID::address, NogoodContainer::createLiteral(), DBGLOG, getStringRepresentation(), insert(), and Atom::tuple.

Referenced by SimpleNogoodContainer::addAllResolvents(), and heuristicNormalization().

void Nogood::dbgload ( std::string str )

Definition at line 367 of file Nogood.cpp.

References NogoodContainer::createLiteral(), and insert().

std::string Nogood::dbgsave ( ) const

Definition at line 357 of file Nogood.cpp.

size_t Nogood::getHash ( )

Returns the hash of the nogood.

Returns:: Hash of the nogood.

Definition at line 94 of file Nogood.cpp.

References hashValue.

Referenced by NogoodSet::addNogood(), ExternalLearningHelper::learnFromInputOutputBehavior(), ExternalLearningHelper::learnFromNegativeAtoms(), and NogoodSet::removeNogood().

std::string Nogood::getStringRepresentation ( RegistryPtr reg ) const

Prints the nogood in string format.

Parameters:

reg	Registry used to resolve atom IDs.

Returns:: String representation of the nogood.

Definition at line 152 of file Nogood.cpp.

References ID::address, ID::isNaf(), ID::isOrdinaryGroundAtom(), and RawPrinter::print().

Referenced by SimpleNogoodContainer::addAllResolvents(), GenuineGuessAndCheckModelGeneratorFactory::addInconsistencyCauseFromSuccessor(), GenuineGuessAndCheckModelGenerator::addNogood(), applyVariableSubstitution(), EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemOptimizationPartLearnedFromMainSearch(), GenuineGuessAndCheckModelGenerator::generalizeNogood(), PluginAtom::generalizeNogood(), GenuineGuessAndCheckModelGenerator::generateNextModel(), InternalGroundASPSolver::getImplicationGraphAsDotString(), InternalGroundASPSolver::getInconsistencyCause(), NogoodSet::getStringRepresentation(), UnfoundedSetChecker::getUFSNogoodUFSBased(), heuristicNormalization(), GenuineGuessAndCheckModelGenerator::identifyInconsistencyCause(), GenuineGuessAndCheckModelGenerator::inlineExternalAtoms(), ExternalLearningHelper::learnFromFunctionality(), ExternalLearningHelper::learnFromGroundRule(), ExternalLearningHelper::learnFromInputOutputBehavior(), ExternalLearningHelper::learnFromNegativeAtoms(), AssumptionBasedUnfoundedSetChecker::learnNogoodsFromMainSearch(), GenuineGuessAndCheckModelGenerator::learnSupportSets(), ExternalLearningHelper::DefaultInputNogoodProvider::operator()(), TestASPQueryAtom::retrieveOrLearnSupportSets(), ImmediateNogoodGrounder::update(), LazyNogoodGrounder::update(), GenuineGuessAndCheckModelGenerator::updateEANogoods(), UnfoundedSetChecker::verifyExternalAtomByEvaluation(), and AnnotatedGroundProgram::verifyExternalAtomsUsingCompleteSupportSets().

void Nogood::heuristicNormalization ( RegistryPtr reg )

Renames variables in this nogoods.

Parameters:

reg	Registry used to resolve literal IDs.

Definition at line 226 of file Nogood.cpp.

References applyVariableSubstitution(), DBGLOG, getStringRepresentation(), isGround(), and Atom::tuple.

void Nogood::insert ( ID lit )

Adds a literal to this nogood.

Note: Before adding, the literal is passed through NogoodContainer::createLiteral to translate it into a uniform form (strip off property flags from the ID).

Parameters:

lit	ID of the literal to add.

Reimplemented from Set< ID >.

Definition at line 280 of file Nogood.cpp.

References NogoodContainer::createLiteral(), ground, and ID::isOrdinaryGroundAtom().

template<class InputIterator >

void Nogood::insert	(	InputIterator	begin,
		InputIterator	end
	)		`[inline]`

Definition at line 178 of file Nogood.h.

References Set< T >::end(), and Set< T >::insert().

bool Nogood::isGround ( ) const

Checks groundness of this nogood.

Returns:: True if all literals in this nogood are ground and false otherwise.

Definition at line 291 of file Nogood.cpp.

References ground.

Referenced by CDNLSolver::addNogoodAndUpdateWatchingStructures(), EncodingBasedUnfoundedSetChecker::constructUFSDetectionProblemOptimizationPartLearnedFromMainSearch(), GenuineGuessAndCheckModelGenerator::generalizeNogood(), PluginAtom::generalizeNogood(), PluginAtom::guardSupportSet(), heuristicNormalization(), GenuineGuessAndCheckModelGenerator::inlineExternalAtoms(), AssumptionBasedUnfoundedSetChecker::learnNogoodsFromMainSearch(), GenuineGuessAndCheckModelGenerator::learnSupportSets(), match(), ImmediateNogoodGrounder::update(), LazyNogoodGrounder::update(), GenuineGuessAndCheckModelGenerator::updateEANogoods(), UnfoundedSetChecker::verifyExternalAtomByEvaluation(), and AnnotatedGroundProgram::verifyExternalAtomsUsingCompleteSupportSets().

bool Nogood::match	(	RegistryPtr	reg,
		ID	atomID,
		Nogood &	instance
	)		const

Checks if there is a substitution of variables in this nogood such that atomID occurs in the substitution and computes the instance of the nogood in that case.

Parameters: