Implements an internal ASP solver without using third-party software. More...

#include <include/dlvhex2/InternalGroundASPSolver.h>

Inheritance diagram for InternalGroundASPSolver:

Collaboration diagram for InternalGroundASPSolver:

Public Types
typedef boost::shared_ptr < InternalGroundASPSolver >	Ptr
typedef boost::shared_ptr < const InternalGroundASPSolver >	ConstPtr
Public Member Functions
	InternalGroundASPSolver (ProgramCtx &ctx, const AnnotatedGroundProgram &p, InterpretationConstPtr frozen=InterpretationConstPtr())
	Constructor.
virtual void	addProgram (const AnnotatedGroundProgram &p, InterpretationConstPtr frozen=InterpretationConstPtr())
	Incrementally adds another program component to the solver.
virtual Nogood	getInconsistencyCause (InterpretationConstPtr explanationAtoms)
	In order to compute an inconsistency reason the program must be inconsistent.
virtual void	addNogoodSet (const NogoodSet &ns, InterpretationConstPtr frozen=InterpretationConstPtr())
	Adds a set of additional nogoods to the solver instance.
virtual void	restartWithAssumptions (const std::vector< ID > &assumptions)
	Resets the search and assumes truth values for selected atoms.
virtual void	addPropagator (PropagatorCallback *pb)
	Adds a propagator callback which is to be called by the SAT solver whenever it cannot propagate by other means or when a model is complete but before getNextModel returns it.
virtual void	removePropagator (PropagatorCallback *pb)
	Removes a propagator callback.
virtual void	setOptimum (std::vector< int > &optimum)
	Sets the current optimum for optimization problems.
virtual InterpretationPtr	getNextModel ()
	Returns the next model.
virtual int	getModelCount ()
	Returns the number of models enumerated so far.
virtual std::string	getStatistics ()
	Delivers solver statistics in human-readable format.
std::string	getImplicationGraphAsDotString ()
	Returns a string representation of the current implication graph in dot format.
Protected Types
typedef boost::adjacency_list < boost::vecS, boost::vecS, boost::bidirectionalS, IDAddress >	Graph
typedef Graph::vertex_descriptor	Node
Protected Member Functions
void	createNogoodsForRule (ID ruleBodyAtomID, ID ruleID)
	Adds nogoods for a rule.
void	createNogoodsForRuleBody (ID ruleBodyAtomID, const Tuple &ruleBody)
	Adds nogoods for a rule.
Set< std::pair< ID, ID > >	createShiftedProgram ()
	Creates the shifted program.
void	computeClarkCompletion ()
	Computes Clark's completion of the input program and adds it to the internal instance.
void	createSingularLoopNogoods (InterpretationConstPtr frozen)
	Computes loop nogoods for singular components of the input program and adds it to the internal instance.
virtual void	resizeVectors ()
	Resizes the internal solver vectors according to the total number of ground atoms in the registry.
void	setEDB ()
	Assigns all atoms from the EDB in the interpretation.
void	computeDepGraph ()
	Computes the positive atom dependency graph of the input program.
void	computeStronglyConnectedComponents ()
	Computes the strongly connected components of the positive atom dependency graph of the input program.
void	initSourcePointers ()
	Initializes the source pointer data structures for unfounded set detection.
void	initializeLists (InterpretationConstPtr frozen)
	Initializes all lists of atoms and facts.
virtual void	setFact (ID fact, int dl, int cause)
virtual void	clearFact (IDAddress litadr)
void	removeSourceFromAtom (IDAddress litadr)
	Removes a source pointer from an atom.
void	addSourceToAtom (IDAddress litadr, ID rule)
	Adds a rule as a possible source for deriving an atom.
Set< IDAddress >	getDependingAtoms (IDAddress litadr)
	Retrieves a list of all atoms which might transitively depend on `litadr`.
void	getInitialNewlyUnfoundedAtomsAfterSetFact (ID fact, Set< IDAddress > &newlyUnfoundedAtoms)
	Get the set of atoms which become unfounded after a literal was assigned.
void	updateUnfoundedSetStructuresAfterSetFact (ID fact)
	Bookkeeping for internal data structures after a literal became true.
void	updateUnfoundedSetStructuresAfterClearFact (IDAddress litadr)
	Bookkeeping for internal data structures after a literal became unassigned.
ID	getPossibleSourceRule (const Set< ID > &ufs)
bool	useAsNewSourceForHeadAtom (IDAddress headAtom, ID sourceRule)
	Checks if a head atom uses the rule as source.
Set< ID >	getUnfoundedSet ()
	Finds an unfounded set.
bool	doesRuleExternallySupportLiteral (ID ruleID, ID lit, const Set< ID > &s)
	Checks for a rule if it supports a literal externally to a set `s`.
Set< ID >	getExternalSupport (const Set< ID > &s)
	Finds all rules which support some atom from `s` externally wrt.
Set< ID >	satisfiesIndependently (ID ruleID, const Set< ID > &y)
	Compute all literals which satisfy the rule independently of set `y`.
Nogood	getLoopNogood (const Set< ID > &ufs)
	Constructs a loop nogood for an unfouneded set.
ID	createNewAtom (ID predID)
	Adds a new propositional atom.
ID	createNewBodyAtom ()
	Adds a new atom used for representing a rule body.
std::string	toString (const Set< ID > &lits)
	Returns a string representation of a set of literals.
std::string	toString (const Set< IDAddress > &lits)
	Returns a string representation of a set of atoms.
std::string	toString (const std::vector< IDAddress > &lits)
	Returns a string representation of a vector of atoms.
template<typename T >
std::vector< T >	intersect (const Set< T > &a, const std::vector< T > &b)
	Intersects two sets.
template<typename T >
Set< T >	intersect (const Set< T > &a, const Set< T > &b)
	Intersects two sets.
InterpretationPtr	outputProjection (InterpretationConstPtr intr)
	Projects dummy atoms for rule bodies away.
Protected Attributes
bool	firstmodel
	True before the first model was found and false otherwise.
int	modelCount
	Number of models found so far.
AnnotatedGroundProgram	program
	Problem instance, i.e., ASP program.
RegistryPtr	reg
	RegistryPtr.
Set< IDAddress >	ordinaryFacts
	Set of facts in the program as Set.
InterpretationPtr	ordinaryFactsInt
	Set of facts in the program as Interpretation.
Set< IDAddress >	nonSingularFacts
	Set of facts which occur in non-singular strongly connected components in the positive atom dependency graph.
boost::unordered_map < IDAddress, Node, SimpleHashIDAddress >	depNodes
	Nodes in the positive atom dependency graph.
Graph	depGraph
	Positive atom dependency graph.
std::vector< Set< IDAddress > >	depSCC
	Stores for each component the contained atoms.
boost::unordered_map < IDAddress, int, SimpleHashIDAddress >	componentOfAtom
	Stores for each atom its component number.
boost::unordered_map < IDAddress, IDAddress, SimpleHashIDAddress >	bodyAtomOfRule
	Store for each rule the body atom.
Set< IDAddress >	unfoundedAtoms
	Currently unfounded atoms.
boost::unordered_map < IDAddress, Set< ID > , SimpleHashIDAddress >	rulesWithPosBodyLiteral
	Stores for each literal the rules which contain it positively in their body.
boost::unordered_map < IDAddress, Set< ID > , SimpleHashIDAddress >	rulesWithNegBodyLiteral
	Stores for each literal the rules which contain it negatively in their body.
boost::unordered_map < IDAddress, Set< ID > , SimpleHashIDAddress >	rulesWithPosHeadLiteral
	Stores for each literal the rules which contain it (positively) in their head.
boost::unordered_map < IDAddress, Set< IDAddress > , SimpleHashIDAddress >	foundedAtomsOfBodyAtom
	Stores for each body atom the set of atoms which use the corresponding rule as source.
boost::unordered_map < IDAddress, ID, SimpleHashIDAddress >	sourceRule
	Stores for each atom a source rule (if available); for facts, ID_FAIL will be stored.
long	cntDetectedUnfoundedSets
	Number of unfounded sets detected so far.
Private Attributes
std::string	bodyAtomPrefix
	Prefix added to variables introduced to represent rule bodies.
int	bodyAtomNumber
	Counter for variables introduced for rule bodies so far.

Detailed Description

Implements an internal ASP solver without using third-party software.

Definition at line 62 of file InternalGroundASPSolver.h.

Member Typedef Documentation

typedef boost::shared_ptr<const InternalGroundASPSolver> InternalGroundASPSolver::ConstPtr

Reimplemented from CDNLSolver.

Reimplemented in InternalGroundDASPSolver.

Definition at line 296 of file InternalGroundASPSolver.h.

typedef boost::adjacency_list<boost::vecS, boost::vecS, boost::bidirectionalS, IDAddress> InternalGroundASPSolver::Graph [protected]

Definition at line 91 of file InternalGroundASPSolver.h.

typedef Graph::vertex_descriptor InternalGroundASPSolver::Node [protected]

Definition at line 92 of file InternalGroundASPSolver.h.

typedef boost::shared_ptr<InternalGroundASPSolver> InternalGroundASPSolver::Ptr

Reimplemented from CDNLSolver.

Reimplemented in InternalGroundDASPSolver.

Definition at line 295 of file InternalGroundASPSolver.h.

Constructor & Destructor Documentation

InternalGroundASPSolver::InternalGroundASPSolver	(	ProgramCtx &	ctx,
		const AnnotatedGroundProgram &	p,
		InterpretationConstPtr	frozen = `InterpretationConstPtr()`
	)

Constructor.

Initializes the solver.

Parameters:

ctx	ProgramCtx.
ns	Instance as NogoodSet.
frozen	Atoms which shall not be optimized away since they might be defined by assumptions.

Definition at line 931 of file InternalGroundASPSolver.cpp.

References computeClarkCompletion(), computeDepGraph(), computeStronglyConnectedComponents(), createSingularLoopNogoods(), CDNLSolver::ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, initializeLists(), initSourcePointers(), CDNLSolver::initWatchingStructures(), reg, ProgramCtx::registry(), resizeVectors(), and setEDB().

Member Function Documentation

void InternalGroundASPSolver::addNogoodSet	(	const NogoodSet &	ns,
		InterpretationConstPtr	frozen = `InterpretationConstPtr()`
	)		`[virtual]`

Adds a set of additional nogoods to the solver instance.

Parameters:

ns	The set of nogoods to add.
frozen	A set of atoms which occur in `ns` and are saved from being optimized away (e.g. because their truth values are relevant).

Reimplemented from CDNLSolver.

Definition at line 1040 of file InternalGroundASPSolver.cpp.

void InternalGroundASPSolver::addProgram	(	const AnnotatedGroundProgram &	program,
		InterpretationConstPtr	frozen = `InterpretationConstPtr()`
	)		`[virtual]`

Incrementally adds another program component to the solver.

Note that modularity conditions do not allow for closing cycles over multiple incremental step (the conditions are as in gringo and clasp).

Parameters:

program	The program component to be added.
frozen	A set of atoms which occur in `ns` and are saved from being optimized away (e.g. because their truth values are relevant).

Implements GenuineGroundSolver.

Definition at line 951 of file InternalGroundASPSolver.cpp.

void InternalGroundASPSolver::addPropagator ( PropagatorCallback * pb ) [virtual]

Adds a propagator callback which is to be called by the SAT solver whenever it cannot propagate by other means or when a model is complete but before getNextModel returns it.

The propagator can add additional nogoods by calling NogoodContainer::addNogood inherited from the base class.

Parameters:

pb	The callback to be added.

Reimplemented from CDNLSolver.

Definition at line 1081 of file InternalGroundASPSolver.cpp.

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

void InternalGroundASPSolver::addSourceToAtom	(	IDAddress	litadr,
		ID	rule
	)		`[protected]`

Adds a rule as a possible source for deriving an atom.

Parameters:

litadr	Atom IDAddress.
rule	ID of a rule which may derive `litadr`.

Definition at line 432 of file InternalGroundASPSolver.cpp.

References ID::address, bodyAtomOfRule, DBGLOG, foundedAtomsOfBodyAtom, and sourceRule.

Referenced by getUnfoundedSet().

void InternalGroundASPSolver::clearFact ( IDAddress litadr ) [protected, virtual]

Reimplemented from CDNLSolver.

Definition at line 410 of file InternalGroundASPSolver.cpp.

References updateUnfoundedSetStructuresAfterClearFact().

Referenced by restartWithAssumptions().

void InternalGroundASPSolver::computeClarkCompletion ( ) [protected]

Computes Clark's completion of the input program and adds it to the internal instance.

Definition at line 217 of file InternalGroundASPSolver.cpp.

References ID::address, bodyAtomOfRule, createNewBodyAtom(), createNogoodsForRule(), DBGLOG, AnnotatedGroundProgram::getGroundProgram(), OrdinaryASPProgram::idb, ID::isWeakConstraint(), CDNLSolver::nogoodset, and program.

Referenced by InternalGroundASPSolver().

void InternalGroundASPSolver::computeDepGraph ( ) [protected]

Computes the positive atom dependency graph of the input program.

Definition at line 251 of file InternalGroundASPSolver.cpp.

References ID::address, Rule::body, depGraph, depNodes, AnnotatedGroundProgram::getGroundProgram(), Rule::head, OrdinaryASPProgram::idb, ID::isNaf(), ordinaryFacts, program, and reg.

Referenced by InternalGroundASPSolver().

void InternalGroundASPSolver::computeStronglyConnectedComponents ( ) [protected]

Computes the strongly connected components of the positive atom dependency graph of the input program.

Definition at line 275 of file InternalGroundASPSolver.cpp.

References CDNLSolver::allAtoms, componentOfAtom, DBGLOG, depGraph, depNodes, depSCC, Set< T >::insert(), nonSingularFacts, ordinaryFacts, and toString().

Referenced by InternalGroundASPSolver().

ID InternalGroundASPSolver::createNewAtom ( ID predID ) [protected]

Adds a new propositional atom.

Parameters:

predID Predicate used for the new atom.

Returns:: ID of the new atom.

Definition at line 849 of file InternalGroundASPSolver.cpp.

References NogoodContainer::createLiteral(), ID::MAINKIND_ATOM, reg, ID::SUBKIND_ATOM_ORDINARYG, and Atom::tuple.

Referenced by createNewBodyAtom().

ID InternalGroundASPSolver::createNewBodyAtom ( ) [protected]

Adds a new atom used for representing a rule body.

Returns:: ID of the new atom.

Definition at line 857 of file InternalGroundASPSolver.cpp.

References ID::address, CDNLSolver::allAtoms, bodyAtomNumber, bodyAtomPrefix, createNewAtom(), DBGLOG, Set< T >::insert(), and reg.

Referenced by computeClarkCompletion(), and createShiftedProgram().

void InternalGroundASPSolver::createNogoodsForRule	(	ID	ruleBodyAtomID,
		ID	ruleID
	)		`[protected]`

Adds nogoods for a rule.

Parameters:

ruleBodyAtomID	Atom used for representing the rule body.
ruleID	ID of the rule to encode.

Definition at line 59 of file InternalGroundASPSolver.cpp.

References NogoodSet::addNogood(), ID::address, Rule::body, NogoodContainer::createLiteral(), createNogoodsForRuleBody(), Rule::head, Nogood::insert(), ID::isWeightRule(), CDNLSolver::nogoodset, and reg.

Referenced by computeClarkCompletion().

void InternalGroundASPSolver::createNogoodsForRuleBody	(	ID	ruleBodyAtomID,
		const Tuple &	ruleBody
	)		`[protected]`

Adds nogoods for a rule.

Parameters:

ruleBodyAtomID	Atom used for representing the rule body.
ruleBody	Rule body to encode.

Definition at line 80 of file InternalGroundASPSolver.cpp.

References NogoodSet::addNogood(), NogoodContainer::createLiteral(), Nogood::insert(), ID::isAggregateAtom(), CDNLSolver::negation(), and CDNLSolver::nogoodset.

Referenced by createNogoodsForRule(), and createSingularLoopNogoods().

Set< std::pair< ID, ID > > InternalGroundASPSolver::createShiftedProgram ( ) [protected]

Creates the shifted program.

For each rule of kind h1 v ... hn :- b1, ..., bm the shifted program contains all shifted rules of kind hi :- b1, ..., bm, not h1, ..., not h{i-1}, not h{i+1}, ..., not hn.

Returns:: For each rule the set of shifted rules.

Definition at line 104 of file InternalGroundASPSolver.cpp.

References ID::address, Rule::body, bodyAtomOfRule, NogoodContainer::createLiteral(), createNewBodyAtom(), DBGLOG, AnnotatedGroundProgram::getGroundProgram(), Rule::head, ID_FAIL(), OrdinaryASPProgram::idb, Set< T >::insert(), ID::MAINKIND_RULE, CDNLSolver::negation(), program, reg, and ID::SUBKIND_RULE_REGULAR.

Referenced by createSingularLoopNogoods().

void InternalGroundASPSolver::createSingularLoopNogoods ( InterpretationConstPtr frozen ) [protected]

Computes loop nogoods for singular components of the input program and adds it to the internal instance.

Parameters:

frozen Atoms which shall not be optimized away since they might be defined by assumptions.

Definition at line 160 of file InternalGroundASPSolver.cpp.

References NogoodSet::addNogood(), Rule::body, CDNLSolver::contains(), NogoodContainer::createLiteral(), createNogoodsForRuleBody(), createShiftedProgram(), DBGLOG, OrdinaryASPProgram::edb, AnnotatedGroundProgram::getGroundProgram(), Rule::head, OrdinaryASPProgram::idb, Nogood::insert(), CDNLSolver::negation(), CDNLSolver::nogoodset, ordinaryFacts, program, and reg.

Referenced by InternalGroundASPSolver().

bool InternalGroundASPSolver::doesRuleExternallySupportLiteral	(	ID	ruleID,
		ID	lit,
		const Set< ID > &	s
	)		`[protected]`

Checks for a rule if it supports a literal externally to a set s.

External support means that the rule may be used to derive the atom but does not depend on an atom in s.

Parameters:

ruleID	ID of a rule.
lit	Literal ID.
s	Set of literals.

Returns:: True if the rule supports lit externally wrt. s and false otherwise.

Definition at line 742 of file InternalGroundASPSolver.cpp.

References ID::address, Rule::body, CDNLSolver::contains(), Rule::head, and reg.

Referenced by getExternalSupport().

Set< IDAddress > InternalGroundASPSolver::getDependingAtoms ( IDAddress litadr ) [protected]

Retrieves a list of all atoms which might transitively depend on litadr.

Parameters:

litadr IDAddress of an atom.

Returns:: List of all atoms which might transitively depend on litadr.

Definition at line 440 of file InternalGroundASPSolver.cpp.

References ID::address, bodyAtomOfRule, foundedAtomsOfBodyAtom, Set< T >::insert(), and rulesWithPosBodyLiteral.

Referenced by updateUnfoundedSetStructuresAfterSetFact().

Set< ID > InternalGroundASPSolver::getExternalSupport ( const Set< ID > & s ) [protected]

Finds all rules which support some atom from s externally wrt.

s.

Parameters:

s	Set of literals.

Returns:: Set of all rules which support some atom from s externally wrt. s.

Definition at line 768 of file InternalGroundASPSolver.cpp.

References ID::address, DBGLOG, DBGLOGD, doesRuleExternallySupportLiteral(), Set< T >::insert(), rulesWithPosHeadLiteral, and toString().

Referenced by getLoopNogood(), and getPossibleSourceRule().

std::string InternalGroundASPSolver::getImplicationGraphAsDotString ( )

Returns a string representation of the current implication graph in dot format.

Returns:: String representation of the current implication graph in dot format.

Definition at line 1228 of file InternalGroundASPSolver.cpp.

References CDNLSolver::allAtoms, CDNLSolver::assignedAtoms, Set< T >::begin(), CDNLSolver::cause, CDNLSolver::contradictoryNogoods, CDNLSolver::decisionlevel, CDNLSolver::flipped, NogoodSet::getNogood(), Nogood::getStringRepresentation(), CDNLSolver::interpretation, CDNLSolver::nogoodset, reg, and Set< T >::size().

Referenced by getInconsistencyCause(), and getNextModel().

Nogood InternalGroundASPSolver::getInconsistencyCause ( InterpretationConstPtr explanationAtoms ) [virtual]

In order to compute an inconsistency reason the program must be inconsistent.

This condition is stronger than the condition of getNextModel() returning NULL: getNextModel() might also return if there are _no more_ models, while for inconsistent programs it would return NULL even after a restart.

: FOR TESTIGN PURPOSES ONLY If (for whatever reason) there is a contradictory nogood after getNextModel() returns NULL, we can compute a reason why there is no *further* model (flipping all decision literals leads to this conflict); if all previous models have been rejected due to incompatibility (which needs to be checked by the caller), then this is also a reason for inconsistency.

Reimplemented from CDNLSolver.

Definition at line 961 of file InternalGroundASPSolver.cpp.

References ID::address, Set< T >::begin(), CDNLSolver::cause, CDNLSolver::contradictoryNogoods, DBGLOG, CDNLSolver::decisionlevel, getImplicationGraphAsDotString(), getNextModel(), NogoodSet::getNogood(), Nogood::getStringRepresentation(), ID_FAIL(), Nogood::insert(), CDNLSolver::loadAddedNogoods(), modelCount, CDNLSolver::nogoodset, reg, CDNLSolver::resolve(), and Set< T >::size().

void InternalGroundASPSolver::getInitialNewlyUnfoundedAtomsAfterSetFact	(	ID	fact,
		Set< IDAddress > &	newlyUnfoundedAtoms
	)		`[protected]`

Get the set of atoms which become unfounded after a literal was assigned.

Parameters:

fact	Literal which is now true (either a positive or a negated atom).
newlyUnfoundedAtoms	Set of atoms which are unfounded after `fact` was assigned.

Definition at line 461 of file InternalGroundASPSolver.cpp.

References ID::address, componentOfAtom, NogoodContainer::createLiteral(), DBGLOGD, foundedAtomsOfBodyAtom, CDNLSolver::getAssignmentOrderIndex(), Rule::head, Set< T >::insert(), ID::isNaf(), reg, rulesWithPosHeadLiteral, CDNLSolver::satisfied(), sourceRule, and toString().

Referenced by updateUnfoundedSetStructuresAfterSetFact().

Nogood InternalGroundASPSolver::getLoopNogood ( const Set< ID > & ufs ) [protected]

Constructs a loop nogood for an unfouneded set.

Parameters:

ufs	Unfounded set.
Nogood	which tries to avoid the same unfounded set in the future search.

Definition at line 817 of file InternalGroundASPSolver.cpp.

References Set< T >::begin(), NogoodContainer::createLiteral(), DBGLOG, getExternalSupport(), Nogood::insert(), CDNLSolver::satisfied(), satisfiesIndependently(), and toString().

Referenced by getNextModel().

int InternalGroundASPSolver::getModelCount ( ) [virtual]

Returns the number of models enumerated so far.

Returns:: Model count.

Implements GenuineGroundSolver.

Definition at line 1206 of file InternalGroundASPSolver.cpp.

References modelCount.

InterpretationPtr InternalGroundASPSolver::getNextModel ( ) [virtual]

Returns the next model.

This will also trigger callbacks to the propagators, see addPropagator.

Returns:: The next model or a NULL-pointer of no more models exist.

Reimplemented from CDNLSolver.

Reimplemented in InternalGroundDASPSolver.

Definition at line 1100 of file InternalGroundASPSolver.cpp.

References CDNLSolver::addNogoodAndUpdateWatchingStructures(), CDNLSolver::allAtoms, CDNLSolver::analysis(), CDNLSolver::assignedAtoms, CDNLSolver::backtrack(), CDNLSolver::changedAtoms, cntDetectedUnfoundedSets, CDNLSolver::complete(), CDNLSolver::currentDL, DBGLOG, CDNLSolver::decisionLiteralOfDecisionLevel, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, CDNLSolver::exhaustedDL, firstmodel, CDNLSolver::flipDecisionLiteral(), CDNLSolver::getGuess(), getImplicationGraphAsDotString(), getLoopNogood(), NogoodSet::getNogoodCount(), getUnfoundedSet(), CDNLSolver::interpretation, CDNLSolver::litToString(), CDNLSolver::loadAddedNogoods(), modelCount, CDNLSolver::nogoodset, outputProjection(), PropagatorCallback::propagate(), CDNLSolver::propagator, CDNLSolver::recentConflicts, reg, setFact(), Set< T >::size(), toString(), and CDNLSolver::unitPropagation().

Referenced by getInconsistencyCause().

ID InternalGroundASPSolver::getPossibleSourceRule ( const Set< ID > & ufs ) [protected]

Definition at line 593 of file InternalGroundASPSolver.cpp.

References ID::address, DBGLOG, getExternalSupport(), ID_FAIL(), CDNLSolver::satisfied(), satisfiesIndependently(), and toString().

Referenced by getUnfoundedSet().

std::string InternalGroundASPSolver::getStatistics ( ) [virtual]

Delivers solver statistics in human-readable format.

Create solver statistics in a no further specified format (for debug purposes).

Returns:: Debug statistics.

Reimplemented from CDNLSolver.

Definition at line 1212 of file InternalGroundASPSolver.cpp.

References cntDetectedUnfoundedSets.

Set< ID > InternalGroundASPSolver::getUnfoundedSet ( ) [protected]

Finds an unfounded set.

Returns:: A non-empty unfounded set if there is any, and an empty set otherwise.

Definition at line 688 of file InternalGroundASPSolver.cpp.

References ID::address, addSourceToAtom(), Set< T >::begin(), Rule::body, Set< T >::clear(), componentOfAtom, Set< T >::count(), NogoodContainer::createLiteral(), DBGLOG, depSCC, Set< T >::erase(), getPossibleSourceRule(), Rule::head, ID_FAIL(), Set< T >::insert(), ID::isNaf(), CDNLSolver::litToString(), reg, Set< T >::size(), toString(), unfoundedAtoms, and useAsNewSourceForHeadAtom().

Referenced by getNextModel().

void InternalGroundASPSolver::initializeLists ( InterpretationConstPtr frozen ) [protected]

Initializes all lists of atoms and facts.

Parameters:

frozen Atoms which shall not be optimized away since they might be defined by assumptions.

Definition at line 344 of file InternalGroundASPSolver.cpp.

References CDNLSolver::allAtoms, Rule::body, OrdinaryASPProgram::edb, AnnotatedGroundProgram::getGroundProgram(), Rule::head, OrdinaryASPProgram::idb, Set< T >::insert(), ordinaryFacts, ordinaryFactsInt, program, reg, rulesWithNegBodyLiteral, rulesWithPosBodyLiteral, and rulesWithPosHeadLiteral.

Referenced by InternalGroundASPSolver().

void InternalGroundASPSolver::initSourcePointers ( ) [protected]

Initializes the source pointer data structures for unfounded set detection.

Definition at line 321 of file InternalGroundASPSolver.cpp.

References Set< T >::count(), DBGLOG, OrdinaryASPProgram::edb, AnnotatedGroundProgram::getGroundProgram(), ID_FAIL(), Set< T >::insert(), nonSingularFacts, ordinaryFacts, program, sourceRule, toString(), and unfoundedAtoms.

Referenced by InternalGroundASPSolver().

template<typename T >

std::vector<T> InternalGroundASPSolver::intersect	(	const Set< T > &	a,
		const std::vector< T > &	b
	)		`[inline, protected]`

Intersects two sets.

Parameters:

a	First Set.
b	Second Set.

Returns:: Intersection of a and b as std::vector.

Definition at line 244 of file InternalGroundASPSolver.h.

References CDNLSolver::contains().

Referenced by updateUnfoundedSetStructuresAfterSetFact().

template<typename T >

Set<T> InternalGroundASPSolver::intersect	(	const Set< T > &	a,
		const Set< T > &	b
	)		`[inline, protected]`

Intersects two sets.

Parameters:

a	First Set.
b	Second Set.

Returns:: Intersection of a and b as Set.

Definition at line 257 of file InternalGroundASPSolver.h.

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

InterpretationPtr InternalGroundASPSolver::outputProjection ( InterpretationConstPtr intr ) [protected]

Projects dummy atoms for rule bodies away.

Parameters:

intr	Interpretation to project.

Returns:: Projection of intr.

Definition at line 913 of file InternalGroundASPSolver.cpp.

References AnnotatedGroundProgram::getGroundProgram(), OrdinaryASPProgram::mask, ordinaryFactsInt, program, and reg.

Referenced by getNextModel().

void InternalGroundASPSolver::removePropagator ( PropagatorCallback * pb ) [virtual]

Removes a propagator callback.

Parameters:

pb	The callback to be removed.

Reimplemented from CDNLSolver.

Definition at line 1087 of file InternalGroundASPSolver.cpp.

References Set< T >::erase(), and CDNLSolver::propagator.

void InternalGroundASPSolver::removeSourceFromAtom ( IDAddress litadr ) [protected]

Removes a source pointer from an atom.

Parameters:

litadr Atom to remove the source pointer from.

Definition at line 417 of file InternalGroundASPSolver.cpp.

References ID::address, bodyAtomOfRule, DBGLOG, foundedAtomsOfBodyAtom, ID_FAIL(), and sourceRule.

Referenced by updateUnfoundedSetStructuresAfterSetFact().

void InternalGroundASPSolver::resizeVectors ( ) [protected, virtual]

Resizes the internal solver vectors according to the total number of ground atoms in the registry.

Reimplemented from CDNLSolver.

Definition at line 199 of file InternalGroundASPSolver.cpp.

References reg.

Referenced by InternalGroundASPSolver().

void InternalGroundASPSolver::restartWithAssumptions ( const std::vector< ID > & assumptions ) [virtual]

Resets the search and assumes truth values for selected atoms.

Parameters:

assumptions Vector of positive or negated (using ID::NAF_MASK) atoms which are temporarily assumed to hold (until the next reset); ID::NAF_MASK is used to represent that the according atom is assumed to be false.

Reimplemented from CDNLSolver.

Definition at line 1046 of file InternalGroundASPSolver.cpp.

References ID::address, CDNLSolver::allAtoms, CDNLSolver::assignedAtoms, clearFact(), Set< T >::contains(), DBGLOG, setEDB(), and setFact().

Set< ID > InternalGroundASPSolver::satisfiesIndependently	(	ID	ruleID,
		const Set< ID > &	y
	)		`[protected]`

Compute all literals which satisfy the rule independently of set y.

This is the case if either the body of rule ruleID is false or some head literal, which is not in y, is true.

Parameters:

ruleID	ID of some rule.
y	Some set of literals.

Returns:: All literals which satisfy the rule independently of set y.

Definition at line 795 of file InternalGroundASPSolver.cpp.

References ID::address, bodyAtomOfRule, Set< T >::count(), NogoodContainer::createLiteral(), DBGLOG, Rule::head, Set< T >::insert(), reg, and toString().

Referenced by getLoopNogood(), and getPossibleSourceRule().

void InternalGroundASPSolver::setEDB ( ) [protected]

Assigns all atoms from the EDB in the interpretation.

Definition at line 233 of file InternalGroundASPSolver.cpp.

References Set< T >::count(), NogoodContainer::createLiteral(), DBGLOG, OrdinaryASPProgram::edb, AnnotatedGroundProgram::getGroundProgram(), ordinaryFacts, program, and setFact().

Referenced by InternalGroundASPSolver(), and restartWithAssumptions().

void InternalGroundASPSolver::setFact	(	ID	fact,
		int	dl,
		int	cause = `-1`
	)		`[protected, virtual]`

Reimplemented from CDNLSolver.

Definition at line 403 of file InternalGroundASPSolver.cpp.

References CDNLSolver::cause, and updateUnfoundedSetStructuresAfterSetFact().

Referenced by getNextModel(), restartWithAssumptions(), and setEDB().

void InternalGroundASPSolver::setOptimum ( std::vector< int > & optimum ) [virtual]

Sets the current optimum for optimization problems.

The solver may (or may not) use this value to prune the search space and not return less optimal models.

Parameters:

optimum The optimum in form of current costs for each level, migh levels with greater index are considered more important (see AnswerSet::costVector).

Implements GenuineGroundSolver.

Definition at line 1093 of file InternalGroundASPSolver.cpp.

References LOG.

std::string InternalGroundASPSolver::toString ( const Set< ID > & lits ) [protected]