#include <include/dlvhex2/FLPModelGeneratorBase.h>

Inheritance diagram for FLPModelGeneratorBase:

Collaboration diagram for FLPModelGeneratorBase:

Public Member Functions
	FLPModelGeneratorBase (FLPModelGeneratorFactoryBase &factory, InterpretationConstPtr input)
	Constructor.
virtual	~FLPModelGeneratorBase ()
	Destructor.
Protected Member Functions
virtual bool	isCompatibleSet (InterpretationConstPtr candidateCompatibleSet, InterpretationConstPtr postprocessedInput, ProgramCtx &ctx, SimpleNogoodContainerPtr nc)
	Checks whether guessed external atom truth values and external atom computations coincide.
template<typename OrdinaryASPSolverT >
bool	isSubsetMinimalFLPModel (InterpretationConstPtr compatibleSet, InterpretationConstPtr postprocessedInput, ProgramCtx &ctx, SimpleNogoodContainerPtr ngc=SimpleNogoodContainerPtr())
	Checks whether a given model is subset-minimal OrdinaryASPSolverT must implement the OrdinaryASPSolver interface (e.g., GenuineSolver).
Nogood	getFLPNogood (ProgramCtx &ctx, const OrdinaryASPProgram &groundProgram, InterpretationConstPtr compatibleSet, InterpretationConstPtr projectedCompatibleSet, InterpretationConstPtr smallerFLPModel)
	Constructs a nogood which describes the essence of a failed FLP check.
void	computeShadowAndUnfoundedPredicates (RegistryPtr reg, InterpretationConstPtr edb, const std::vector< ID > &idb, std::map< ID, std::pair< int, ID > > &shadowPredicates, std::map< ID, std::pair< int, ID > > &unfoundedPredicates, std::string &shadowPostfix, std::string &unfoundedPostfix)
	Computes for each predicate p in IDB/EDB a "shadow predicate" and an "unfounded predicate" (two new predicates) which does not yet occur.
void	addShadowInterpretation (RegistryPtr reg, std::map< ID, std::pair< int, ID > > &shadowPredicates, InterpretationConstPtr input, InterpretationPtr output)
	Transforms an EDB into its shadowed version, i.e., each predicate is replaced by its shadow predicate.
void	createMinimalityRules (RegistryPtr reg, std::map< ID, std::pair< int, ID > > &shadowPredicates, std::string &shadowPostfix, std::vector< ID > &idb)
	Computes for each pair of predicate p and shadow predicate sp of arity n rules: :- p(X1, ..., Xn), not sp(X1, ..., Xn).
void	createFoundingRules (RegistryPtr reg, std::map< ID, std::pair< int, ID > > &shadowPredicates, std::map< ID, std::pair< int, ID > > &unfoundedPredicates, std::vector< ID > &idb)
	Creates rules which provide additional support for atoms in the program.
Protected Attributes
FLPModelGeneratorFactoryBase &	factory
	Reference to the factory which created this model generator.
AnnotatedGroundProgram	annotatedGroundProgram
	Meta information about the ground program of this model generator.

Detailed Description

Definition at line 138 of file FLPModelGeneratorBase.h.

Constructor & Destructor Documentation

FLPModelGeneratorBase::FLPModelGeneratorBase	(	FLPModelGeneratorFactoryBase &	factory,
		InterpretationConstPtr	input
	)

Constructor.

Parameters:

factory	Reference to the factory which created this model generator.
input	Input interpretation to this model generator.

Definition at line 420 of file FLPModelGeneratorBase.cpp.

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

Destructor.

Definition at line 150 of file FLPModelGeneratorBase.h.

Member Function Documentation

void FLPModelGeneratorBase::addShadowInterpretation	(	RegistryPtr	reg,
		std::map< ID, std::pair< int, ID > > &	shadowPredicates,
		InterpretationConstPtr	input,
		InterpretationPtr	output
	)		`[protected]`

Transforms an EDB into its shadowed version, i.e., each predicate is replaced by its shadow predicate.

Parameters:

reg	RegistryPtr.
shadowPredicates	Map containing for each predicate a shadow predicate and its arity.
input	EDB.
output	Interpretation to receive the output.

Definition at line 642 of file FLPModelGeneratorBase.cpp.

References ID::MAINKIND_ATOM, ID::SUBKIND_ATOM_ORDINARYG, and Atom::tuple.

Referenced by isSubsetMinimalFLPModel().

void FLPModelGeneratorBase::computeShadowAndUnfoundedPredicates	(	RegistryPtr	reg,
		InterpretationConstPtr	edb,
		const std::vector< ID > &	idb,
		std::map< ID, std::pair< int, ID > > &	shadowPredicates,
		std::map< ID, std::pair< int, ID > > &	unfoundedPredicates,
		std::string &	shadowPostfix,
		std::string &	unfoundedPostfix
	)		`[protected]`

Computes for each predicate p in IDB/EDB a "shadow predicate" and an "unfounded predicate" (two new predicates) which does not yet occur.

Parameters:

reg	RegistryPtr.
edb	Program EDB.
idb	Program IDB.
shadowPredicates	Map where for each predicate a shadow predicate and its arity will be added.
unfoundedPredicates	Map where for each predicate an unfoundedPredicates predicate and its arity will be added.
shadowPostfix	String to append to shadow predicates.
unfoundedPostfix	String to append to unfounded predicates.

Definition at line 533 of file FLPModelGeneratorBase.cpp.

References Rule::body, DBGLOG, Rule::head, ID::isExternalAuxiliary(), ID::isFLPAuxiliary(), ID::isOrdinaryAtom(), ID::isOrdinaryGroundAtom(), ID::MAINKIND_TERM, ID::SUBKIND_TERM_CONSTANT, and Atom::tuple.

Referenced by isSubsetMinimalFLPModel().

void FLPModelGeneratorBase::createFoundingRules	(	RegistryPtr	reg,
		std::map< ID, std::pair< int, ID > > &	shadowPredicates,
		std::map< ID, std::pair< int, ID > > &	unfoundedPredicates,
		std::vector< ID > &	idb
	)		`[protected]`

Creates rules which provide additional support for atoms in the program.

We want to compute a _model_ of the reduct rather than an _answer set_, i.e., atoms are allowed to be _not_ founded. For this we introduce for each n-ary shadow predicate ps(X1, ..., Xn) a rule p(X1, ..., Xn) v p_unfounded(X1, ..., Xn) :- ps(X1, ..., Xn) which can be used to found an atom. (p_unfounded(X1, ..., Xn) encodes that the atom is not artificially founded)

Parameters:

reg	RegistryPtr.
shadowPredicates	Map where for each predicate a shadow predicate and its arity will be added.
unfoundedPredicates	Map where for each predicate an unfoundedPredicates predicate and its arity will be added.
idb	Program IDB.

Definition at line 744 of file FLPModelGeneratorBase.cpp.

References Rule::body, DBGLOG, Rule::head, Atom::kind, ID::MAINKIND_ATOM, ID::MAINKIND_RULE, ID::PROPERTY_AUX, ID::PROPERTY_RULE_DISJ, ID::SUBKIND_ATOM_ORDINARYG, ID::SUBKIND_ATOM_ORDINARYN, ID::SUBKIND_RULE_REGULAR, and Atom::tuple.

Referenced by isSubsetMinimalFLPModel().

void FLPModelGeneratorBase::createMinimalityRules	(	RegistryPtr	reg,
		std::map< ID, std::pair< int, ID > > &	shadowPredicates,
		std::string &	shadowPostfix,
		std::vector< ID > &	idb
	)		`[protected]`

Computes for each pair of predicate p and shadow predicate sp of arity n rules: :- p(X1, ..., Xn), not sp(X1, ..., Xn).

smaller :- not p(X1, ..., Xn), sp(X1, ..., Xn). and one rule :- not smaller

Parameters:

reg	RegistryPtr.
shadowPredicates	Map containing for each predicate a shadow predicate and its arity.
shadowPostfix	String to append to shadow predicates.
idb	Original program IDB.

Definition at line 662 of file FLPModelGeneratorBase.cpp.

References ID::address, Rule::body, DBGLOG, Rule::head, Atom::kind, ID::kind, ID::MAINKIND_ATOM, ID::MAINKIND_LITERAL, ID::MAINKIND_RULE, ID::MAINKIND_TERM, ID::NAF_MASK, ID::PROPERTY_AUX, ID::SUBKIND_ATOM_ORDINARYG, ID::SUBKIND_ATOM_ORDINARYN, ID::SUBKIND_MASK, ID::SUBKIND_RULE_CONSTRAINT, ID::SUBKIND_RULE_REGULAR, ID::SUBKIND_TERM_CONSTANT, and Atom::tuple.

Referenced by isSubsetMinimalFLPModel().

Nogood FLPModelGeneratorBase::getFLPNogood	(	ProgramCtx &	ctx,
		const OrdinaryASPProgram &	groundProgram,
		InterpretationConstPtr	compatibleSet,
		InterpretationConstPtr	projectedCompatibleSet,
		InterpretationConstPtr	smallerFLPModel
	)		`[protected]`

Constructs a nogood which describes the essence of a failed FLP check.

Parameters:

ctx	ProgramCtx.
groundProgram	Original ground program.
compatibleSet	A model of the ordinary ASP program which is compatible with the external atom semantics, i.e., it passed isCompatibleSet.
projectedCompatibleSet	Interpretation `compatibleSet` without replacement atoms.
smallerFLPModel	A proper subset of `projectedCompatibleSet`.

Returns:: A nogood which describes the essence of a failed FLP check and can be used for search space pruning.

Definition at line 482 of file FLPModelGeneratorBase.cpp.

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

bool FLPModelGeneratorBase::isCompatibleSet	(	InterpretationConstPtr	candidateCompatibleSet,
		InterpretationConstPtr	postprocessedInput,
		ProgramCtx &	ctx,
		SimpleNogoodContainerPtr	nc
	)		`[protected, virtual]`

Checks whether guessed external atom truth values and external atom computations coincide.

Parameters:

candidateCompatibleSet	Model of the ordinary ASP program to be checked for compatibility.
postprocessedInput	Facts and auxiliaries for outer external atoms.
ctx	ProgramCtx.
nc	NogoodContainer to add learned nogoods to; can be NULL.

Returns:: True if candidateCompatibleSet is compatible with the external atom semantics and false otherwise.

Definition at line 429 of file FLPModelGeneratorBase.cpp.

References ProgramCtx::config, DBGLOG, BaseModelGenerator::evaluateExternalAtoms(), factory, Configuration::getOption(), FLPModelGeneratorFactoryBase::gnMask, FLPModelGeneratorFactoryBase::gpMask, FLPModelGeneratorFactoryBase::innerEatoms, PredicateMask::mask(), FLPModelGeneratorFactoryBase::reg, and PredicateMask::updateMask().

Referenced by GuessAndCheckModelGenerator::generateNextModel(), and isSubsetMinimalFLPModel().

template<typename OrdinaryASPSolverT >

bool FLPModelGeneratorBase::isSubsetMinimalFLPModel	(	InterpretationConstPtr	compatibleSet,
		InterpretationConstPtr	postprocessedInput,
		ProgramCtx &	ctx,
		SimpleNogoodContainerPtr	ngc = `SimpleNogoodContainerPtr()`
	)		`[protected]`

Checks whether a given model is subset-minimal OrdinaryASPSolverT must implement the OrdinaryASPSolver interface (e.g., GenuineSolver).

Parameters:

compatibleSet	A model of the ordinary ASP program which is compatible with the external atom semantics, i.e., it passed isCompatibleSet.
postprocessedInput	Facts and auxiliaries for outer external atoms.
ctx	ProgramCtx.
snc	NogoodContainer to add learned nogoods to; can be NULL.