Model generator for arbitrary components. More...

#include <include/dlvhex2/GenuineGuessAndCheckModelGenerator.h>

Inheritance diagram for GenuineGuessAndCheckModelGenerator:

Collaboration diagram for GenuineGuessAndCheckModelGenerator:

Public Types
typedef GenuineGuessAndCheckModelGeneratorFactory	Factory
Public Member Functions
	GenuineGuessAndCheckModelGenerator (Factory &factory, InterpretationConstPtr input)
	Constructor.
virtual	~GenuineGuessAndCheckModelGenerator ()
	Destuctor.
virtual InterpretationPtr	generateNextModel ()
	Generate and return next model, return NULL after last model.
void	identifyInconsistencyCause ()
	Identifies a reason for an inconsistency in this unit.
virtual const Nogood *	getInconsistencyCause ()
	Returns a reason for inconsistency in this instance wrt.
virtual void	addNogood (const Nogood *cause)
	Adds a nogood to the model generator.
Protected Member Functions
void	inlineExternalAtoms (OrdinaryASPProgram &program, GenuineGrounderPtr &grounder, AnnotatedGroundProgram &annotatedGroundProgram, std::vector< ID > &activeInnerEatoms)
	Inlines selected external atoms which provide support sets.
ID	replacePredForInlinedEAs (ID atomID, InterpretationConstPtr eliminatedExtAuxes)
	If the atom represented by `atomID` uses is an external auxiliary from `eliminatedExtAuxes`, then 'r' is replaced by 'R' and 'n' by 'N'.
void	initializeExplanationAtoms (OrdinaryASPProgram &program)
	Identifies the set of atoms used to explain inconsistencies in this unit.
void	initializeInconsistencyAnalysis ()
	Initializes a non-optimized solver for inconsistency analysis in this unit.
void	initializeHeuristics ()
	Initializes heuristics for external atom evaluation and UFS checking over partial assignments.
void	initializeVerificationWatchLists ()
	Adds watches to all external auxilies for incremental verification and unverification of external atoms.
void	generalizeNogood (Nogood ng)
	Learns related nonground nogoods.
void	learnSupportSets ()
	Learns all support sets provided by external sources and adds them to supportSets.
void	updateEANogoods (InterpretationConstPtr compatibleSet, InterpretationConstPtr assigned=InterpretationConstPtr(), InterpretationConstPtr changed=InterpretationConstPtr())
	Triggern nonground nogood learning and instantiation.
bool	finalCompatibilityCheck (InterpretationConstPtr modelCandidate)
	Checks after completion of an assignment if it is compatible.
bool	isModel (InterpretationConstPtr compatibleSet)
	Checks if a compatible set is a model, i.e., it does the FLP check.
bool	unfoundedSetCheck (InterpretationConstPtr partialInterpretation, InterpretationConstPtr assigned=InterpretationConstPtr(), InterpretationConstPtr changed=InterpretationConstPtr(), bool partial=false)
	Makes an unfounded set check over a (possibly) partial interpretation if useful.
IDAddress	getWatchedLiteral (int eaIndex, InterpretationConstPtr search, bool truthValue)
	Finds a new atom in the scope of an external atom which shall be watched wrt.
void	unverifyExternalAtoms (InterpretationConstPtr changed)
	Removes verification results for external atoms if relevant parts of the input have changed.
bool	verifyExternalAtoms (InterpretationConstPtr partialInterpretation, InterpretationConstPtr assigned, InterpretationConstPtr changed)
	Heuristically decides if and which external atoms we evaluate.
bool	verifyExternalAtom (int eaIndex, InterpretationConstPtr partialInterpretation, InterpretationConstPtr assigned=InterpretationConstPtr(), InterpretationConstPtr changed=InterpretationConstPtr(), bool *answeredFromCacheOrSupportSets=0)
	Evaluates the inner external atom with index eaIndex (if possible, i.e., if the input is complete).
bool	verifyExternalAtomByEvaluation (int eaIndex, InterpretationConstPtr partialInterpretation, InterpretationConstPtr assigned=InterpretationConstPtr(), InterpretationConstPtr changed=InterpretationConstPtr(), bool *answeredFromCache=0)
	Evaluates the inner external atom with index eaIndex (if possible, i.e., if the input is complete) using explicit evaluation.
bool	verifyExternalAtomBySupportSets (int eaIndex, InterpretationConstPtr partialInterpretation, InterpretationConstPtr assigned=InterpretationConstPtr(), InterpretationConstPtr changed=InterpretationConstPtr())
	Evaluates the inner external atom with index eaIndex (if possible, i.e., if the input is complete) using complete support sets.
const OrdinaryASPProgram &	getGroundProgram ()
	Returns the ground program in this component.
void	propagate (InterpretationConstPtr partialInterpretation, InterpretationConstPtr assigned, InterpretationConstPtr changed)
	Is called by the ASP solver in its propagation method to trigger fruther learning methods.
Protected Attributes
Factory &	factory
	Reference to the factory which created this model generator.
RegistryPtr	reg
	RegistryPtr.
std::vector< ID >	activeInnerEatoms
	The set of inner external atoms which were not inlined.
boost::unordered_map < IDAddress, std::vector< int > >	verifyWatchList
	Stores for each replacement atom the set of external atoms which shall be verified when the replacement atom is (re-)assigned.
boost::unordered_map < IDAddress, std::vector< int > >	unverifyWatchList
	Stores for each replacement atom the set of external atoms which shall be unverified when the replacement atom is (re-)assigned.
std::vector< bool >	eaEvaluated
	Stores for each external atom guess if it already was checked against the semantics (i.e., it is either verified or falsified).
std::vector< bool >	eaVerified
	Stores for each external atom guess if it already was checked against the semantics and this check succeeded.
InterpretationPtr	verifiedAuxes
	The set of currently verified external atom auxiliaries.
std::vector< InterpretationPtr >	changedAtomsPerExternalAtom
	Stores for each inner external atom the cumulative atoms which potentially changes since last evaluation.
ExternalAtomEvaluationHeuristicsPtr	defaultExternalAtomEvalHeuristics
	Heuristics to be used for evaluating external atoms for which no dedicated heuristics is provided.
std::vector < ExternalAtomEvaluationHeuristicsPtr >	eaEvalHeuristics
	Stores for each external atom its evaluation heuristics; is either defaultExternalAtomEvalHeuristics or a dedicated one.
UnfoundedSetCheckHeuristicsPtr	ufsCheckHeuristics
InterpretationConstPtr	postprocessedInput
	EDB + original (input) interpretation plus auxiliary atoms for evaluated external atoms.
InterpretationPtr	mask
	Non-external fact input, i.e., postprocessedInput before evaluating outer eatoms.
NogoodGrounderPtr	nogoodGrounder
	Grounder for nonground nogoods.
SimpleNogoodContainerPtr	learnedEANogoods
	All nogoods learned from EA evaluations.
ExternalAtomVerificationTree	eavTree
	Tree representation of GenuineGuessAndCheckModelGenerator::learnedEANogoods for verification purposes.
int	learnedEANogoodsTransferredIndex
	The highest index in learnedEANogoods which has already been transferred to the solver.
GenuineGrounderPtr	grounder
	Grounder instance.
GenuineGroundSolverPtr	solver
	Solver instance.
int	cmModelCount
	Number of models of this model generate (only compatible and minimal ones).
InterpretationPtr	explAtoms
	Set of atoms used for inconsistency analysis (only defined if inconsistency analysis is used).
InternalGroundDASPSolverPtr	analysissolver
	Second solver instance (non-optimized solver!) for inconsistency analysis.
bool	haveInconsistencyCause
	Stores if an inconsistency cause has been identified.
Nogood	inconsistencyCause
	Stores the inconsistency cause as a nogood if GenuineGuessAndCheckModelGenerator::haveInconsistencyCause is set to true.
UnfoundedSetCheckerManagerPtr	ufscm
	Manager for unfounded set checking.
InterpretationPtr	programMask
	All atoms in the program.

Detailed Description

Model generator for arbitrary components.

Definition at line 59 of file GenuineGuessAndCheckModelGenerator.h.

Member Typedef Documentation

typedef GenuineGuessAndCheckModelGeneratorFactory GenuineGuessAndCheckModelGenerator::Factory

Definition at line 66 of file GenuineGuessAndCheckModelGenerator.h.

Constructor & Destructor Documentation

GenuineGuessAndCheckModelGenerator::GenuineGuessAndCheckModelGenerator	(	Factory &	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 190 of file GenuineGuessAndCheckModelGenerator.cpp.

References activeInnerEatoms, FLPModelGeneratorBase::annotatedGroundProgram, GenuineGuessAndCheckModelGeneratorFactory::ci, BaseModelGenerator::computeExtensionOfDomainPredicates(), ProgramCtx::config, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, FLPModelGeneratorFactoryBase::deidb, FLPModelGeneratorFactoryBase::deidbInnerEatoms, ComponentGraph::ComponentInfo::disjunctiveHeads, DLVHEX_BENCHMARK_COUNT, DLVHEX_BENCHMARK_REGISTER, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, ProgramCtx::edb, BaseModelGenerator::evaluateExternalAtoms(), explAtoms, GenuineGrounder::getInstance(), GenuineGroundSolver::getInstance(), Configuration::getOption(), FLPModelGeneratorFactoryBase::gidb, grounder, OrdinaryASPProgram::idb, initializeExplanationAtoms(), initializeHeuristics(), initializeInconsistencyAnalysis(), initializeVerificationWatchLists(), inlineExternalAtoms(), FLPModelGeneratorFactoryBase::innerEatoms, learnedEANogoods, learnedEANogoodsTransferredIndex, learnSupportSets(), OrdinaryASPProgram::mask, mask, ProgramCtx::maxint, nogoodGrounder, GenuineGuessAndCheckModelGeneratorFactory::outerEatoms, postprocessedInput, FLPModelGeneratorFactoryBase::reg, reg, ProgramCtx::registry(), solver, ufscm, WARNING(), and FLPModelGeneratorFactoryBase::xidb.

GenuineGuessAndCheckModelGenerator::~GenuineGuessAndCheckModelGenerator ( ) [virtual]

Destuctor.

Definition at line 309 of file GenuineGuessAndCheckModelGenerator.cpp.

References DBGLOG, and solver.

Member Function Documentation

void GenuineGuessAndCheckModelGenerator::addNogood ( const Nogood * ng ) [virtual]

Adds a nogood to the model generator.

This nogood can be, for instance, an inconsistency cause in successor units.

Parameters:

cause Pointer to the nogood to be added.

Reimplemented from ModelGeneratorBase< Interpretation >.

Definition at line 824 of file GenuineGuessAndCheckModelGenerator.cpp.

References analysissolver, ProgramCtx::config, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_COUNT, factory, Configuration::getOption(), Nogood::getStringRepresentation(), ProgramCtx::registry(), and solver.

Referenced by initializeInconsistencyAnalysis().

bool GenuineGuessAndCheckModelGenerator::finalCompatibilityCheck ( InterpretationConstPtr modelCandidate ) [protected]

Checks after completion of an assignment if it is compatible.

Depending on the eaVerificationMode, the compatibility is either directly checked in this function, of previously recorded verfication results are used to compute the return value.

Parameters:

modelCandidate The model candidate to check for compatibility

Returns:: True if compatibel and false otherwise.

Definition at line 1015 of file GenuineGuessAndCheckModelGenerator.cpp.

References activeInnerEatoms, ProgramCtx::config, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, eaEvaluated, eaVerified, factory, Configuration::getOption(), and verifyExternalAtom().

Referenced by generateNextModel().

void GenuineGuessAndCheckModelGenerator::generalizeNogood ( Nogood ng ) [protected]

Learns related nonground nogoods.

Parameters:

ng	The nogood to generalize.

Definition at line 833 of file GenuineGuessAndCheckModelGenerator.cpp.

References ID::address, FLPModelGeneratorBase::annotatedGroundProgram, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, factory, AnnotatedGroundProgram::getAuxToEA(), Nogood::getStringRepresentation(), ID_FAIL(), Nogood::isGround(), learnedEANogoods, AnnotatedGroundProgram::mapsAux(), and reg.

Referenced by updateEANogoods().

InterpretationPtr GenuineGuessAndCheckModelGenerator::generateNextModel ( ) [virtual]

Generate and return next model, return NULL after last model.

Returns:: Next model if any and NULL after last model.

Implements ModelGeneratorBase< Interpretation >.

Definition at line 733 of file GenuineGuessAndCheckModelGenerator.cpp.

References analysissolver, FLPModelGeneratorBase::annotatedGroundProgram, cmModelCount, ProgramCtx::config, GenuineGuessAndCheckModelGeneratorFactory::ctx, ProgramCtx::currentOptimum, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_COUNT, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, explAtoms, factory, finalCompatibilityCheck(), Configuration::getOption(), AnnotatedGroundProgram::getProgramMask(), Nogood::getStringRepresentation(), FLPModelGeneratorFactoryBase::gnMask, FLPModelGeneratorFactoryBase::gpMask, identifyInconsistencyCause(), isModel(), LOG, LOG_SCOPE, PredicateMask::mask(), mask, postprocessedInput, ProgramCtx::registry(), and solver.

const OrdinaryASPProgram & GenuineGuessAndCheckModelGenerator::getGroundProgram ( ) [protected]

Returns the ground program in this component.

Returns:: const std::vector<ID>& Reference to the ground program in this component

Definition at line 1473 of file GenuineGuessAndCheckModelGenerator.cpp.

References FLPModelGeneratorBase::annotatedGroundProgram, and AnnotatedGroundProgram::getGroundProgram().

const Nogood * GenuineGuessAndCheckModelGenerator::getInconsistencyCause ( ) [virtual]

Returns a reason for inconsistency in this instance wrt.

the input atoms*

Returns:: Pointer to a nogood instance to contain the reason for the inconsistency, or false if no such reason cound be determined.

Reimplemented from ModelGeneratorBase< Interpretation >.

Definition at line 818 of file GenuineGuessAndCheckModelGenerator.cpp.

References ProgramCtx::config, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_COUNT, factory, Configuration::getOption(), haveInconsistencyCause, and inconsistencyCause.

IDAddress GenuineGuessAndCheckModelGenerator::getWatchedLiteral	(	int	eaIndex,
		InterpretationConstPtr	search,
		bool	truthValue
	)		`[protected]`

Finds a new atom in the scope of an external atom which shall be watched wrt.

an interpretation.

Precondition:: Some atom in the scope of the external atom is yet unassigned.

Parameters:

eaIndex	The index of the inner external atom.
search	Search interpretation; can be 0 to indicate that all atoms of the EA's mask are eligable.
truthValue	Indicates whether to search for a true or a false atom in search.

Returns:: Address of an atom to watch or ALL_ONES if none exists.

Definition at line 1214 of file GenuineGuessAndCheckModelGenerator.cpp.

References activeInnerEatoms, ID::ALL_ONES, FLPModelGeneratorBase::annotatedGroundProgram, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, and AnnotatedGroundProgram::getEAMask().

Referenced by verifyExternalAtoms().

void GenuineGuessAndCheckModelGenerator::identifyInconsistencyCause ( )

Identifies a reason for an inconsistency in this unit.

The method may only be called after generateNextModel() has returned NULL after first call.

Definition at line 805 of file GenuineGuessAndCheckModelGenerator.cpp.

References analysissolver, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, explAtoms, factory, Nogood::getStringRepresentation(), haveInconsistencyCause, inconsistencyCause, and ProgramCtx::registry().

Referenced by generateNextModel().

void GenuineGuessAndCheckModelGenerator::initializeExplanationAtoms ( OrdinaryASPProgram & program ) [protected]

Identifies the set of atoms used to explain inconsistencies in this unit.

Parameters:

program The program whose EDB needs to be modified for inconsistency analysis (explanation atoms are removed as facts and assumed instead).

Definition at line 597 of file GenuineGuessAndCheckModelGenerator.cpp.

References GenuineGuessAndCheckModelGeneratorFactory::ci, ProgramCtx::config, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, OrdinaryASPProgram::edb, explAtoms, factory, Configuration::getOption(), postprocessedInput, ComponentGraph::ComponentInfo::predicatesDefinedInComponent, ComponentGraph::ComponentInfo::predicatesOccurringInComponent, ProgramCtx::registry(), and GenuineGuessAndCheckModelGeneratorFactory::succNogoods.

Referenced by GenuineGuessAndCheckModelGenerator().

void GenuineGuessAndCheckModelGenerator::initializeHeuristics ( ) [protected]

Initializes heuristics for external atom evaluation and UFS checking over partial assignments.

Definition at line 677 of file GenuineGuessAndCheckModelGenerator.cpp.

References activeInnerEatoms, FLPModelGeneratorBase::annotatedGroundProgram, changedAtomsPerExternalAtom, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, defaultExternalAtomEvalHeuristics, ProgramCtx::defaultExternalAtomEvaluationHeuristicsFactory, ExtSourceProperties::doesCareAboutChanged(), eaEvalHeuristics, eaEvaluated, eaVerified, factory, PluginAtom::getCustomExternalAtomEvaluationHeuristicsFactory(), ExternalAtom::getExtSourceProperties(), ExternalAtom::pluginAtom, PluginAtom::providesCustomExternalAtomEvaluationHeuristicsFactory(), reg, ufsCheckHeuristics, ProgramCtx::unfoundedSetCheckHeuristicsFactory, and verifiedAuxes.

Referenced by GenuineGuessAndCheckModelGenerator().

void GenuineGuessAndCheckModelGenerator::initializeInconsistencyAnalysis ( ) [protected]

Initializes a non-optimized solver for inconsistency analysis in this unit.

Definition at line 643 of file GenuineGuessAndCheckModelGenerator.cpp.

References addNogood(), analysissolver, FLPModelGeneratorBase::annotatedGroundProgram, ProgramCtx::config, NogoodContainer::createLiteral(), GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, explAtoms, factory, Configuration::getOption(), AnnotatedGroundProgram::getProgramMask(), ID::nafLiteralFromAtom(), ID::posLiteralFromAtom(), postprocessedInput, ProgramCtx::registry(), solver, and GenuineGuessAndCheckModelGeneratorFactory::succNogoods.

Referenced by GenuineGuessAndCheckModelGenerator().

void GenuineGuessAndCheckModelGenerator::initializeVerificationWatchLists ( ) [protected]

Adds watches to all external auxilies for incremental verification and unverification of external atoms.

Definition at line 707 of file GenuineGuessAndCheckModelGenerator.cpp.

References activeInnerEatoms, FLPModelGeneratorBase::annotatedGroundProgram, AnnotatedGroundProgram::getEAMask(), unverifyWatchList, and verifyWatchList.

Referenced by GenuineGuessAndCheckModelGenerator().

void GenuineGuessAndCheckModelGenerator::inlineExternalAtoms	(	OrdinaryASPProgram &	program,
		GenuineGrounderPtr &	grounder,
		AnnotatedGroundProgram &	annotatedGroundProgram,
		std::vector< ID > &	activeInnerEatoms
	)		`[protected]`

Inlines selected external atoms which provide support sets.

Parameters:

program	The input non-ground program whose external atoms are to be inlined (if possible).
grounder	The grounder used to ground `program`.
annotatedGroundProgram	The current annotations of `program` before the inlining, i.e., considering external atoms as external.
activeInnerEatoms	After the call this vector contains the external atoms which were not inlined.
Parameters	`program`, `grounder`, `annotatedGroundProgram` and `activeInnerEatoms` are updated.

Definition at line 316 of file GenuineGuessAndCheckModelGenerator.cpp.

References ID::address, ID::ALL_ONES, FLPModelGeneratorBase::annotatedGroundProgram, Rule::body, Set< T >::count(), GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, OrdinaryASPProgram::edb, explAtoms, factory, AnnotatedGroundProgram::getAuxToEA(), AnnotatedGroundProgram::getEAMask(), ExternalAtom::getExtSourceProperties(), AnnotatedGroundProgram::getIndexOfEAtom(), GenuineGrounder::getInstance(), Nogood::getStringRepresentation(), Rule::head, ID_FAIL(), OrdinaryASPProgram::idb, FLPModelGeneratorFactoryBase::innerEatoms, ID::isAuxiliary(), Rule::isEAGuessingRule(), ID::isExternalAuxiliary(), Nogood::isGround(), ID::isNaf(), ID::isOrdinaryGroundAtom(), ID::kind, BaseModelGenerator::learnSupportSetsForExternalAtom(), ID::MAINKIND_ATOM, ID::MAINKIND_RULE, AnnotatedGroundProgram::mapsAux(), OrdinaryASPProgram::mask, mask, ProgramCtx::maxint, ID::NAF_MASK, ID::nafLiteralFromAtom(), ID::posLiteralFromAtom(), ID::PROPERTY_AUX, ID::PROPERTY_RULE_DISJ, ExtSourceProperties::providesOnlySafeSupportSets(), ExtSourceProperties::providesSupportSets(), reg, ProgramCtx::registry(), replacePredForInlinedEAs(), ID::SUBKIND_ATOM_ORDINARYG, ID::SUBKIND_RULE_REGULAR, and Atom::tuple.

Referenced by GenuineGuessAndCheckModelGenerator().

bool GenuineGuessAndCheckModelGenerator::isModel ( InterpretationConstPtr compatibleSet ) [protected]

Checks if a compatible set is a model, i.e., it does the FLP check.

The details depend on the selected semantics (well-justified FLP or FLP) and the selected algorithm (explicit or ufs-based). Depending on the eaVerificationMode, the compatibility is either directly checked in this function, of previously recorded verfication results are used to compute the return value.

Parameters:

compatibleSet The model candidate to check for minimality.

Returns:: True if compatibleSet is an answer set and false otherwise.

Definition at line 1051 of file GenuineGuessAndCheckModelGenerator.cpp.

References FLPModelGeneratorBase::annotatedGroundProgram, ProgramCtx::config, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, factory, Configuration::getOption(), AnnotatedGroundProgram::hasECycles(), AnnotatedGroundProgram::hasHeadCycles(), learnedEANogoods, postprocessedInput, unfoundedSetCheck(), and updateEANogoods().

Referenced by generateNextModel().

void GenuineGuessAndCheckModelGenerator::learnSupportSets ( ) [protected]

Learns all support sets provided by external sources and adds them to supportSets.

Definition at line 860 of file GenuineGuessAndCheckModelGenerator.cpp.

References activeInnerEatoms, ID::address, FLPModelGeneratorBase::annotatedGroundProgram, ProgramCtx::config, Set< T >::count(), GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, DLVHEX_BENCHMARK_COUNT, DLVHEX_BENCHMARK_REGISTER, factory, AnnotatedGroundProgram::getAuxToEA(), ExternalAtom::getExtSourceProperties(), Configuration::getOption(), Nogood::getStringRepresentation(), ID_FAIL(), Nogood::isGround(), learnedEANogoods, BaseModelGenerator::learnSupportSetsForExternalAtom(), AnnotatedGroundProgram::mapsAux(), ExtSourceProperties::providesSupportSets(), reg, ProgramCtx::registry(), and AnnotatedGroundProgram::setCompleteSupportSetsForVerification().

Referenced by GenuineGuessAndCheckModelGenerator().

void GenuineGuessAndCheckModelGenerator::propagate	(	InterpretationConstPtr	partialInterpretation,
		InterpretationConstPtr	assigned,
		InterpretationConstPtr	changed
	)		`[protected, virtual]`

Is called by the ASP solver in its propagation method to trigger fruther learning methods.

This function can add additional (learned) nogoods to the solver to force implications or tell the solver that the current assignment is conflicting.

Parameters:

partialInterpretation	The current assignment.
assigned	Currently assigned atoms.
changed	The set of atoms with modified truth value since the last call.

Implements PropagatorCallback.

Definition at line 1479 of file GenuineGuessAndCheckModelGenerator.cpp.

References FLPModelGeneratorBase::annotatedGroundProgram, ProgramCtx::config, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, factory, Configuration::getOption(), AnnotatedGroundProgram::hasECycles(), AnnotatedGroundProgram::hasHeadCycles(), ufsCheckHeuristics, unfoundedSetCheck(), unverifyExternalAtoms(), verifiedAuxes, and verifyExternalAtoms().

ID GenuineGuessAndCheckModelGenerator::replacePredForInlinedEAs	(	ID	atomID,
		InterpretationConstPtr	eliminatedExtAuxes
	)		`[protected]`

If the atom represented by atomID uses is an external auxiliary from eliminatedExtAuxes, then 'r' is replaced by 'R' and 'n' by 'N'.

Parameters:

atomID	The atom whose predicate is to be replaced.
eliminatedExtPreds	The external predicates whose auxiliaries are to be replaced.

Returns:: The ID of the new atom.

Definition at line 571 of file GenuineGuessAndCheckModelGenerator.cpp.

References ID::address, ID::ALL_ONES, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, factory, ID::isExternalAuxiliary(), Atom::kind, ID::PROPERTY_EXTERNALAUX, reg, ProgramCtx::registry(), and Atom::tuple.

Referenced by inlineExternalAtoms().

bool GenuineGuessAndCheckModelGenerator::unfoundedSetCheck	(	InterpretationConstPtr	partialInterpretation,
		InterpretationConstPtr	assigned = `InterpretationConstPtr()`,
		InterpretationConstPtr	changed = `InterpretationConstPtr()`,
		bool	partial = `false`
	)		`[protected]`

Makes an unfounded set check over a (possibly) partial interpretation if useful.

Parameters:

partialInterpretation	The current assignment.
assigned	Currently assigned atoms (can be 0 if partial=false).
changed	The set of atoms with modified truth value since the last call (can be 0 if partial=false).
partial	True if the assignment is (potentially) partial; in this case the check is driven by a heuristic.

Returns:: bool True if the check is passed, i.e., if there is *no* unfounded set. False if the check is failed, i.e., there *is* an unfounded set.

Definition at line 1136 of file GenuineGuessAndCheckModelGenerator.cpp.

References ID::address, analysissolver, ProgramCtx::config, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, factory, Configuration::getOption(), learnedEANogoods, LOG, solver, ufsCheckHeuristics, ufscm, verifiedAuxes, and WARNING().

Referenced by isModel(), and propagate().

void GenuineGuessAndCheckModelGenerator::unverifyExternalAtoms ( InterpretationConstPtr changed ) [protected]

Removes verification results for external atoms if relevant parts of the input have changed.

Parameters:

changed The set of atoms with modified truth value since the last call.

Definition at line 1237 of file GenuineGuessAndCheckModelGenerator.cpp.

References FLPModelGeneratorBase::annotatedGroundProgram, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, eaEvaluated, eaVerified, AnnotatedGroundProgram::getEAMask(), unverifyWatchList, verifiedAuxes, and verifyWatchList.

Referenced by propagate().

void GenuineGuessAndCheckModelGenerator::updateEANogoods	(	InterpretationConstPtr	compatibleSet,
		InterpretationConstPtr	assigned = `InterpretationConstPtr()`,
		InterpretationConstPtr	changed = `InterpretationConstPtr()`
	)		`[protected]`

Triggern nonground nogood learning and instantiation.

Parameters:

compatibleSet	Current compatible set.
assigned	Set of currently assigned atoms or NULL to represent a complete assignment (optimization).
changed	Set of atoms which possibly changes since the previous call (optimization)

Transferes new nogoods from learnedEANogoods to the solver and updates learnedEANogoodsTransferredIndex accordingly.

Definition at line 944 of file GenuineGuessAndCheckModelGenerator.cpp.

References ExternalAtomVerificationTree::addNogood(), analysissolver, FLPModelGeneratorBase::annotatedGroundProgram, ProgramCtx::config, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_COUNT, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, eavTree, factory, generalizeNogood(), Configuration::getOption(), Configuration::getStringOption(), Nogood::getStringRepresentation(), AnnotatedGroundProgram::hasECycles(), Nogood::isGround(), learnedEANogoods, learnedEANogoodsTransferredIndex, LOG, nogoodGrounder, reg, Set< T >::size(), solver, ExternalAtomVerificationTree::toString(), and ufscm.

Referenced by isModel(), and verifyExternalAtomByEvaluation().

bool GenuineGuessAndCheckModelGenerator::verifyExternalAtom	(	int	eaIndex,
		InterpretationConstPtr	partialInterpretation,
		InterpretationConstPtr	assigned = `InterpretationConstPtr()`,
		InterpretationConstPtr	changed = `InterpretationConstPtr()`,
		bool *	answeredFromCacheOrSupportSets = `0`
	)		`[protected]`

Evaluates the inner external atom with index eaIndex (if possible, i.e., if the input is complete).

Learns nogoods if external learning is activated. Sets eaVerified and eaEvaluated if eaVerificationMode == mixed.

Parameters:

eaIndex	The index of the external atom to verify.
partialInterpretation	The current assignment.
assigned	Currently assigned atoms (if 0, then the assignment is assumed to be complete).
changed	The set of atoms with modified truth value since the last call (if 0, then all atoms are assumed to have changed).
answeredFromCacheOrSupportSets	Optional pointer to a boolean where it is to be stored whether the query was answered from cache or support sets (true) or the external source was actually called (false).

Returns:: bool True if the assignment is conflicting wrt. this external atom, otherwise false.

Definition at line 1352 of file GenuineGuessAndCheckModelGenerator.cpp.

References activeInnerEatoms, AnnotatedGroundProgram::allowsForVerificationUsingCompleteSupportSets(), FLPModelGeneratorBase::annotatedGroundProgram, ProgramCtx::config, GenuineGuessAndCheckModelGeneratorFactory::ctx, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, factory, ExternalAtom::getExtSourceProperties(), Configuration::getOption(), ExtSourceProperties::providesCompleteNegativeSupportSets(), ExtSourceProperties::providesCompletePositiveSupportSets(), reg, verifyExternalAtomByEvaluation(), and verifyExternalAtomBySupportSets().

Referenced by finalCompatibilityCheck(), and verifyExternalAtoms().

bool GenuineGuessAndCheckModelGenerator::verifyExternalAtomByEvaluation	(	int	eaIndex,
		InterpretationConstPtr	partialInterpretation,
		InterpretationConstPtr	assigned = `InterpretationConstPtr()`,
		InterpretationConstPtr	changed = `InterpretationConstPtr()`,
		bool *	answeredFromCache = `0`
	)		`[protected]`

Evaluates the inner external atom with index eaIndex (if possible, i.e., if the input is complete) using explicit evaluation.

Learns nogoods if external learning is activated. Sets eaVerified and eaEvaluated if eaVerificationMode == mixed.

Parameters:

eaIndex	The index of the external atom to verify.
partialInterpretation	The current assignment.
assigned	Currently assigned atoms (if 0, then the assignment is assumed to be complete).
changed	The set of atoms with modified truth value since the last call (if 0, then all atoms are assumed to have changed).
answeredFromCache	Optional pointer to a boolean where it is to be stored whether the query was answered from cache (true) or the external source was actually called (false).

Returns:: bool True if the assignment is conflicting wrt. this external atom, otherwise false.

Definition at line 1372 of file GenuineGuessAndCheckModelGenerator.cpp.

References activeInnerEatoms, FLPModelGeneratorBase::annotatedGroundProgram, ProgramCtx::config, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_COUNT, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, eaEvaluated, eaVerified, eavTree, BaseModelGenerator::evaluateExternalAtom(), factory, AnnotatedGroundProgram::getEAMask(), Configuration::getOption(), AnnotatedGroundProgram::getProgramMask(), ExternalAtomVerificationTree::getVerifiedAuxiliaries(), learnedEANogoods, mask, ProgramCtx::registry(), updateEANogoods(), verifiedAuxes, and BaseModelGenerator::VerifyExternalAtomCB::verify().

Referenced by verifyExternalAtom().

bool GenuineGuessAndCheckModelGenerator::verifyExternalAtomBySupportSets	(	int	eaIndex,
		InterpretationConstPtr	partialInterpretation,
		InterpretationConstPtr	assigned = `InterpretationConstPtr()`,
		InterpretationConstPtr	changed = `InterpretationConstPtr()`
	)		`[protected]`

Evaluates the inner external atom with index eaIndex (if possible, i.e., if the input is complete) using complete support sets.

Learns nogoods if external learning is activated. Sets eaVerified and eaEvaluated if eaVerificationMode == mixed.

Parameters:

eaIndex	The index of the external atom to verify.
partialInterpretation	The current assignment.
assigned	Currently assigned atoms (if 0, then the assignment is assumed to be complete).
changed	The set of atoms with modified truth value since the last call (if 0, then all atoms are assumed to have changed).

Returns:: bool True if the assignment is conflicting wrt. this external atom, otherwise false.

Definition at line 1454 of file GenuineGuessAndCheckModelGenerator.cpp.

References FLPModelGeneratorBase::annotatedGroundProgram, ProgramCtx::config, GenuineGuessAndCheckModelGeneratorFactory::ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, eaEvaluated, eaVerified, factory, AnnotatedGroundProgram::getEAMask(), Configuration::getOption(), verifiedAuxes, and AnnotatedGroundProgram::verifyExternalAtomsUsingCompleteSupportSets().

Referenced by verifyExternalAtom().

bool GenuineGuessAndCheckModelGenerator::verifyExternalAtoms	(	InterpretationConstPtr	partialInterpretation,
		InterpretationConstPtr	assigned,
		InterpretationConstPtr	changed
	)		`[protected]`