Implements a tree representation of IO-nogoods. More...

#include <include/dlvhex2/ExternalAtomVerificationTree.h>

Data Structures
struct	Node
	Node of GenuineGuessAndCheckModelGenerator::ExternalAtomVerificationTree. More...
Public Types
typedef Node::Ptr	NodePtr
Public Member Functions
	ExternalAtomVerificationTree ()
	Default constructor.
void	addNogood (const Nogood &iong, RegistryPtr reg, bool includeNegated)
	Adds a nogood to the tree.
std::string	toString (RegistryPtr reg, int indent=0, NodePtr root=NodePtr())
	Gets a string representation of the tree.
InterpretationConstPtr	getVerifiedAuxiliaries (InterpretationConstPtr partialInterpretation, InterpretationConstPtr assigned, RegistryPtr reg)
	Returns the set of all external atom auxiliaries verified under a certain partial interpretation.
Data Fields
NodePtr	root
Private Member Functions
void	getVerifiedAuxiliaries (NodePtr current, InterpretationPtr output, InterpretationConstPtr partialInterpretation, InterpretationConstPtr assigned, RegistryPtr reg)
	Returns the set of all external atom auxiliaries verified under a certain partial interpretation beginning from a certain node (helper function).

Detailed Description

Implements a tree representation of IO-nogoods.

Both inner and leave nodes contain auxiliary atoms which are verified if an interpretation matches from the root until this node. Note that this is *not* a search tree: interpretations may match multiple pathes since nogoods may not depend on all atoms. The tree has a size of up to 3^n, where n is the number of atoms in the program, but may be much smaller if nogood minimization is used. Matching an interpretation is O(2^n), but may be also much lower if nogoods are minimized.

Definition at line 56 of file ExternalAtomVerificationTree.h.

Member Typedef Documentation

typedef Node::Ptr ExternalAtomVerificationTree::NodePtr

Definition at line 68 of file ExternalAtomVerificationTree.h.

Constructor & Destructor Documentation

DLVHEX_NAMESPACE_BEGIN ExternalAtomVerificationTree::ExternalAtomVerificationTree ( )

Default constructor.

Definition at line 60 of file ExternalAtomVerificationTree.cpp.

Member Function Documentation

void ExternalAtomVerificationTree::addNogood	(	const Nogood &	iong,
		RegistryPtr	reg,
		bool	includeNegated
	)

Adds a nogood to the tree.

Parameters:

ng	IO-Nogood to add.
reg	RegistryPtr.
includeNegated	Include 'n' atom for each 'p' atom and vice versa.

Definition at line 63 of file ExternalAtomVerificationTree.cpp.

References ID::address, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, ID_FAIL(), ID::isExternalAuxiliary(), ID::isNaf(), ID::kind, ID::NAF_MASK, and root.

Referenced by AssumptionBasedUnfoundedSetChecker::learnNogoodsFromMainSearch(), GenuineGuessAndCheckModelGenerator::updateEANogoods(), and UnfoundedSetChecker::verifyExternalAtomByEvaluation().

InterpretationConstPtr ExternalAtomVerificationTree::getVerifiedAuxiliaries	(	InterpretationConstPtr	partialInterpretation,
		InterpretationConstPtr	assigned,
		RegistryPtr	reg
	)

Returns the set of all external atom auxiliaries verified under a certain partial interpretation.

Parameters:

partialInterpretation	Current partial interpretation.
assigned	Currently assigned atoms.
reg	RegistryPtr.

Returns:: Set of all verified external atom auxiliaries.

Definition at line 140 of file ExternalAtomVerificationTree.cpp.

References DBGLOG, and root.

Referenced by getVerifiedAuxiliaries(), UnfoundedSetChecker::verifyExternalAtomByEvaluation(), and GenuineGuessAndCheckModelGenerator::verifyExternalAtomByEvaluation().

void ExternalAtomVerificationTree::getVerifiedAuxiliaries	(	NodePtr	current,
		InterpretationPtr	output,
		InterpretationConstPtr	partialInterpretation,
		InterpretationConstPtr	assigned,
		RegistryPtr	reg
	)		`[private]`

Returns the set of all external atom auxiliaries verified under a certain partial interpretation beginning from a certain node (helper function).

Parameters:

current	Current Node in the search.
output	Interpretation to write the result to.
partialInterpretation	Current partial interpretation.
assigned	Currently assigned atoms.
reg	RegistryPtr.