#include <include/dlvhex2/CDNLSolver.h>

Inheritance diagram for CDNLSolver:

Collaboration diagram for CDNLSolver:

Data Structures
struct	SimpleHashID
	Allows for hashing ID. More...
struct	SimpleHashIDAddress
	Allows for hashing IDAddress. More...
Public Types
typedef boost::shared_ptr < CDNLSolver >	Ptr
typedef boost::shared_ptr < const CDNLSolver >	ConstPtr
Public Member Functions
	CDNLSolver (ProgramCtx &ctx, NogoodSet ns)
	Constructor.
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 InterpretationPtr	getNextModel ()
	Returns the next model.
virtual Nogood	getInconsistencyCause (InterpretationConstPtr explanationAtoms)
	Returns an explanation for an inconsistency in terms of litervals over the atoms given in `explanationAtoms`.
virtual void	addNogoodSet (const NogoodSet &ns, InterpretationConstPtr frozen=InterpretationConstPtr())
	Adds a set of additional nogoods to the solver instance.
virtual void	addNogood (Nogood ng)
	Adds a nogood to the container.
virtual std::string	getStatistics ()
	Delivers solver statistics in human-readable format.
Protected Member Functions
bool	assigned (IDAddress litadr)
	Checks if an atom is assigned.
bool	satisfied (ID lit)
	Checks if a literal is satisfied.
bool	falsified (ID lit)
	Checks if a literal is falsified.
ID	negation (ID lit)
	Negates a literal ID.
bool	complete ()
	Checks if the assignment is currently complete.
bool	unitPropagation (Nogood &violatedNogood)
void	loadAddedNogoods ()
void	analysis (Nogood &violatedNogood, Nogood &learnedNogood, int &backtrackDL)
Nogood	resolve (Nogood &ng1, Nogood &ng2, IDAddress litadr)
virtual void	setFact (ID fact, int dl, int cause)
virtual void	clearFact (IDAddress litadr)
void	backtrack (int dl)
ID	getGuess ()
bool	handlePreviousModel ()
void	flipDecisionLiteral ()
void	initWatchingStructures ()
	Performs unit propagation.
void	updateWatchingStructuresAfterAddNogood (int index)
	Updates all data structures after a nogood was added.
void	updateWatchingStructuresAfterRemoveNogood (int index)
	Updates all data structures after a nogood was removed.
void	updateWatchingStructuresAfterSetFact (ID lit)
	Updates all data structures after a literal was assigned to true.
void	updateWatchingStructuresAfterClearFact (ID lit)
	Updates all data structures after a literal was unassigned.
void	inactivateNogood (int nogoodNr)
	Removed all watches for a nogood.
void	stopWatching (int nogoodNr, ID lit)
	Removed a single watche for a nogood.
void	startWatching (int nogoodNr, ID lit)
	Adds a single watche for a nogood.
void	touchVarsInNogood (Nogood &ng)
	Increses the usage counter for all variables in a nogood.
void	initListOfAllAtoms ()
	Harvests all atoms in the instance.
virtual void	resizeVectors ()
	Resizes the internal solver vectors according to the total number of ground atoms in the registry.
template<typename T >
bool	contains (const std::vector< T > &s, T el)
	Checks if a vector contains an element.
template<typename T >
std::vector< T >	intersect (const std::vector< T > &a, const std::vector< T > &b)
	Checks if two vectors intersect.
long	getAssignmentOrderIndex (IDAddress adr)
	Retrieves for an atom the index in the assignment list in chronological order.
int	addNogoodAndUpdateWatchingStructures (Nogood ng)
	Adds a nogood and updates all internal data structures.
std::vector< Nogood >	getContradictoryNogoods ()
	Retrieves all nogoods which are currently conflicting.
bool	isDecisionLiteral (IDAddress litaddr)
	Checks if a given atom is used as decision literal.
Nogood	getCause (IDAddress adr)
	Retrieves for an atom the nogood which implied it.
Static Protected Member Functions
static std::string	litToString (ID lit)
	Encodes a literal in a string.
Protected Attributes
NogoodSet	nogoodset
	Instance.
Set< IDAddress >	allAtoms
	Atoms of the instance as Set.
ProgramCtx &	ctx
	ProgramCtx.
SimpleNogoodContainer	nogoodsToAdd
	Nogoods scheduled for adding but not added yet.
InterpretationPtr	interpretation
	Current (partial) interpretation.
InterpretationPtr	assignedAtoms
	Set of assigned atoms.
DynamicVector< IDAddress, int >	decisionlevel
	Decision level for each atom; undefined if unassigned.
DynamicVector< IDAddress, int >	flipped
	Stores for decision literals if they have already been flipped.
boost::unordered_map < IDAddress, int, SimpleHashIDAddress >	cause
	Stores for each atom the index and hash of the clause which implied it; undefined if unassigned or guessed.
int	currentDL
	Current decision level >= 0.
OrderedSet< IDAddress, SimpleHashIDAddress >	assignmentOrder
	Stores the current assignment in chronoligical order.
DynamicVector< int, std::vector< IDAddress > >	factsOnDecisionLevel
	Stores for each decision level the facts assigned on that level.
int	exhaustedDL
	Maximum decision level such that the search space above was exhausted (used for eliminating duplicate models without explicitly adding them as nogoods).
DynamicVector< int, ID >	decisionLiteralOfDecisionLevel
	Stores for each decision level the guessed literal (=decision literal).
boost::unordered_map < IDAddress, Set< int > , SimpleHashIDAddress >	nogoodsOfPosLiteral
	Stores for each positive literal the nogoods which contain.
boost::unordered_map < IDAddress, Set< int > , SimpleHashIDAddress >	nogoodsOfNegLiteral
	Stores for each negative literal the nogoods which contain.
boost::unordered_map < IDAddress, Set< int > , SimpleHashIDAddress >	watchingNogoodsOfPosLiteral
	Stores for each positive literal the nogoods which watch it (i.e., which might fire once the literal becomes true).
boost::unordered_map < IDAddress, Set< int > , SimpleHashIDAddress >	watchingNogoodsOfNegLiteral
	Stores for each negative literal the nogoods which watch it (i.e., which might fire once the literal becomes true).
std::vector< Set< ID > >	watchedLiteralsOfNogood
	Stores for each nogood the set of watched literals.
Set< int >	unitNogoods
	Stores the nogoods which are currently unit (i.e., all literals but one are satisfied).
Set< int >	contradictoryNogoods
	Stores the nogoods which are currently contradictory (i.e., all literals are satisfied).
int	conflicts
	Counter for total number of conflicts so far (periodic reset).
boost::unordered_map < IDAddress, int, SimpleHashIDAddress >	varCounterPos
	Counts for each positive literal the number of conflicts it was involved in (periodic reset).
boost::unordered_map < IDAddress, int, SimpleHashIDAddress >	varCounterNeg
	Counts for each negative literal the number of conflicts it was involved in (periodic reset).
std::vector< int >	recentConflicts
	Stores the indexes of the clauses which were recently contradictory in chronological order.
long	cntAssignments
	Number of assignments so far.
long	cntGuesses
	Number of guesses so far.
long	cntBacktracks
	Number of backtracks so far.
long	cntResSteps
	Number of resolution steps so far.
long	cntDetectedConflicts
	Number of conflicts so far.
Set< ID >	tmpWatched
	Temporary objects (they are just class members in order to make them reuseable without reallocation).
InterpretationPtr	changedAtoms
	Set of atoms which (possibly) changes since last call of external learners because they have been reassigned.
Set< PropagatorCallback * >	propagator
	Set of external propagators.

Detailed Description

Definition at line 57 of file CDNLSolver.h.

Member Typedef Documentation

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

Reimplemented from NogoodContainer.

Reimplemented in InternalGroundASPSolver, and InternalGroundDASPSolver.

Definition at line 334 of file CDNLSolver.h.

typedef boost::shared_ptr<CDNLSolver> CDNLSolver::Ptr

Reimplemented from NogoodContainer.

Reimplemented in InternalGroundASPSolver, and InternalGroundDASPSolver.

Definition at line 333 of file CDNLSolver.h.

Constructor & Destructor Documentation

CDNLSolver::CDNLSolver	(	ProgramCtx &	ctx,
		NogoodSet	ns
	)

Constructor.

Initializes the solver.

Parameters:

ctx	ProgramCtx.
ns	Instance as NogoodSet.

Definition at line 719 of file CDNLSolver.cpp.

References assignedAtoms, changedAtoms, ctx, currentDL, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, exhaustedDL, initListOfAllAtoms(), initWatchingStructures(), interpretation, ProgramCtx::registry(), and resizeVectors().

Member Function Documentation

void CDNLSolver::addNogood ( Nogood ng ) [virtual]

Adds a nogood to the container.

Parameters:

ng	The nogood to add.

Implements NogoodContainer.

Definition at line 920 of file CDNLSolver.cpp.

References SimpleNogoodContainer::addNogood(), and nogoodsToAdd.

Referenced by InternalGroundDASPSolver::getNextModel().

int CDNLSolver::addNogoodAndUpdateWatchingStructures ( Nogood ng ) [protected]

Adds a nogood and updates all internal data structures.

Parameters:

ng	Nogood to add.

Returns:: Index of the new nogood.

Definition at line 673 of file CDNLSolver.cpp.

References NogoodSet::addNogood(), ID::address, allAtoms, Set< T >::contains(), DBGLOG, Nogood::insert(), Nogood::isGround(), ID::isNaf(), nogoodset, updateWatchingStructuresAfterAddNogood(), and watchedLiteralsOfNogood.

Referenced by InternalGroundASPSolver::getNextModel(), getNextModel(), handlePreviousModel(), and loadAddedNogoods().

void CDNLSolver::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).

Implements SATSolver.

Reimplemented in InternalGroundASPSolver.

Definition at line 915 of file CDNLSolver.cpp.

void CDNLSolver::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.

Implements SATSolver.

Reimplemented in InternalGroundASPSolver.

Definition at line 764 of file CDNLSolver.cpp.

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

void CDNLSolver::analysis	(	Nogood &	violatedNogood,
		Nogood &	learnedNogood,
		int &	backtrackDL
	)		`[protected]`

Definition at line 100 of file CDNLSolver.cpp.

References ID::address, ID::ALL_ONES, allAtoms, cause, cntDetectedConflicts, cntResSteps, conflicts, DBGLOG, decisionlevel, getAssignmentOrderIndex(), NogoodSet::getNogood(), ID_FAIL(), isDecisionLiteral(), nogoodset, resolve(), touchVarsInNogood(), varCounterNeg, and varCounterPos.

Referenced by InternalGroundASPSolver::getNextModel(), getNextModel(), and handlePreviousModel().

bool CDNLSolver::assigned ( IDAddress litadr ) [inline, protected]

Checks if an atom is assigned.

Parameters:

litadr Atom IDAddress.

Returns:: True if litadr is assigned and false otherwise.

Definition at line 157 of file CDNLSolver.h.

References assignedAtoms.

Referenced by falsified(), getAssignmentOrderIndex(), getGuess(), satisfied(), unitPropagation(), updateWatchingStructuresAfterAddNogood(), updateWatchingStructuresAfterClearFact(), updateWatchingStructuresAfterSetFact(), and InternalGroundASPSolver::useAsNewSourceForHeadAtom().

void CDNLSolver::backtrack ( int dl ) [protected]

Definition at line 260 of file CDNLSolver.cpp.

References clearFact(), cntBacktracks, and factsOnDecisionLevel.

Referenced by flipDecisionLiteral(), InternalGroundASPSolver::getNextModel(), getNextModel(), and handlePreviousModel().

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

Reimplemented in InternalGroundASPSolver.

Definition at line 246 of file CDNLSolver.cpp.

References assignedAtoms, assignmentOrder, cause, changedAtoms, NogoodContainer::createLiteral(), DBGLOG, decisionlevel, OrderedSet< T, H >::erase(), interpretation, and updateWatchingStructuresAfterClearFact().

Referenced by backtrack().

bool CDNLSolver::complete ( ) [inline, protected]

Checks if the assignment is currently complete.

Returns:: True if complete and false otherwise.

Definition at line 190 of file CDNLSolver.h.

References allAtoms, assignedAtoms, and Set< T >::size().

Referenced by getGuess(), InternalGroundASPSolver::getNextModel(), getNextModel(), and handlePreviousModel().

template<typename T >

bool CDNLSolver::contains	(	const std::vector< T > &	s,
		T	el
	)		`[inline, protected]`

Checks if a vector contains an element.

Parameters:

s	Vector.
el	Element.

Returns:: True if el is in s and false otherwise.

Definition at line 260 of file CDNLSolver.h.

Referenced by InternalGroundASPSolver::createSingularLoopNogoods(), InternalGroundASPSolver::doesRuleExternallySupportLiteral(), InternalGroundASPSolver::intersect(), and intersect().

bool CDNLSolver::falsified ( ID lit ) [inline, protected]

Checks if a literal is falsified.

Parameters:

litlitadr Literal ID.

Returns:: True if lit is falsified and false otherwise.

Definition at line 174 of file CDNLSolver.h.

References ID::address, assigned(), interpretation, and ID::isNaf().

Referenced by InternalGroundASPSolver::updateUnfoundedSetStructuresAfterSetFact(), updateWatchingStructuresAfterAddNogood(), updateWatchingStructuresAfterClearFact(), and updateWatchingStructuresAfterSetFact().

void CDNLSolver::flipDecisionLiteral ( ) [protected]

Definition at line 809 of file CDNLSolver.cpp.

References ID::address, backtrack(), currentDL, DBGLOG, decisionLiteralOfDecisionLevel, exhaustedDL, flipped, litToString(), negation(), and setFact().

Referenced by InternalGroundASPSolver::getNextModel(), and getNextModel().

long CDNLSolver::getAssignmentOrderIndex ( IDAddress adr ) [inline, protected]

Retrieves for an atom the index in the assignment list in chronological order.

Parameters:

adr	Atom IDAddress.

Returns:: -1 if adr is unassigned and its assignment index otherwise (larger means more recent).

Definition at line 279 of file CDNLSolver.h.

References assigned(), assignmentOrder, and OrderedSet< T, H >::getInsertionIndex().

Referenced by analysis(), InternalGroundASPSolver::getInitialNewlyUnfoundedAtomsAfterSetFact(), and InternalGroundASPSolver::useAsNewSourceForHeadAtom().

Nogood CDNLSolver::getCause ( IDAddress adr ) [protected]

Retrieves for an atom the nogood which implied it.

Parameters:

adr	Address of an assigned and not guessed atom.

Returns:: Nogood which implied adr.

Definition at line 937 of file CDNLSolver.cpp.

References cause, NogoodSet::getNogood(), and nogoodset.

std::vector< Nogood > CDNLSolver::getContradictoryNogoods ( ) [protected]

Retrieves all nogoods which are currently conflicting.

Returns:: Set of conflicting nogoods.

Definition at line 926 of file CDNLSolver.cpp.

References contradictoryNogoods, NogoodSet::getNogood(), and nogoodset.

ID CDNLSolver::getGuess ( ) [protected]

Definition at line 276 of file CDNLSolver.cpp.

References ID::address, allAtoms, assigned(), assignedAtoms, cntGuesses, complete(), NogoodContainer::createLiteral(), DBGLOG, NogoodSet::getNogood(), ID_FAIL(), litToString(), negation(), nogoodset, recentConflicts, Set< T >::size(), varCounterNeg, varCounterPos, and watchedLiteralsOfNogood.

Referenced by InternalGroundASPSolver::getNextModel(), and getNextModel().

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

Returns an explanation for an inconsistency in terms of litervals over the atoms given in explanationAtoms.

Details (definition of explanations) are specified in subclasses.

The method may only be called after getNextModel() has returned a NULL-pointer after first call.

Parameters:

explanationAtoms The atoms which serve as explanation.

Returns:: An explanation for the inconsistency depending on the atoms in explanationAtoms.

Implements SATSolver.

Reimplemented in InternalGroundASPSolver.

Definition at line 911 of file CDNLSolver.cpp.

InterpretationPtr CDNLSolver::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.

Implements SATSolver.

Reimplemented in InternalGroundASPSolver, and InternalGroundDASPSolver.

Definition at line 828 of file CDNLSolver.cpp.

References addNogoodAndUpdateWatchingStructures(), ID::address, analysis(), assignedAtoms, backtrack(), changedAtoms, complete(), currentDL, DBGLOG, decisionLiteralOfDecisionLevel, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, exhaustedDL, flipDecisionLiteral(), flipped, getGuess(), NogoodSet::getNogoodCount(), interpretation, litToString(), loadAddedNogoods(), nogoodset, PropagatorCallback::propagate(), propagator, recentConflicts, setFact(), and unitPropagation().

std::string CDNLSolver::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 in InternalGroundASPSolver.

Definition at line 700 of file CDNLSolver.cpp.

References cntAssignments, cntBacktracks, cntDetectedConflicts, cntGuesses, and cntResSteps.

bool CDNLSolver::handlePreviousModel ( ) [protected]

Definition at line 776 of file CDNLSolver.cpp.

References addNogoodAndUpdateWatchingStructures(), allAtoms, analysis(), backtrack(), complete(), NogoodContainer::createLiteral(), currentDL, DBGLOG, NogoodSet::getNogoodCount(), Nogood::insert(), interpretation, isDecisionLiteral(), nogoodset, and recentConflicts.

void CDNLSolver::inactivateNogood ( int nogoodNr ) [protected]

Removed all watches for a nogood.

Parameters:

nogoodNr Index of the nogood to remove all watches for.

Definition at line 586 of file CDNLSolver.cpp.

References ID::address, contradictoryNogoods, DBGLOGD, Set< T >::erase(), unitNogoods, watchedLiteralsOfNogood, watchingNogoodsOfNegLiteral, and watchingNogoodsOfPosLiteral.

Referenced by updateWatchingStructuresAfterSetFact().

void CDNLSolver::initListOfAllAtoms ( ) [protected]

Harvests all atoms in the instance.

Definition at line 640 of file CDNLSolver.cpp.

References allAtoms, Set< T >::begin(), Set< T >::end(), NogoodSet::getNogood(), NogoodSet::getNogoodCount(), Set< T >::insert(), and nogoodset.

Referenced by CDNLSolver().

void CDNLSolver::initWatchingStructures ( ) [protected]

Performs unit propagation.

Definition at line 350 of file CDNLSolver.cpp.

References Set< T >::clear(), contradictoryNogoods, NogoodSet::getNogoodCount(), nogoodset, nogoodsOfNegLiteral, nogoodsOfPosLiteral, unitNogoods, updateWatchingStructuresAfterAddNogood(), watchedLiteralsOfNogood, watchingNogoodsOfNegLiteral, and watchingNogoodsOfPosLiteral.

Referenced by CDNLSolver(), InternalGroundASPSolver::InternalGroundASPSolver(), and restartWithAssumptions().

template<typename T >

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

Checks if two vectors intersect.

Parameters:

a	First vector.
b	Second vector.

Returns:: True if a and b intersect and false otherwise.

Definition at line 268 of file CDNLSolver.h.

References contains().

bool CDNLSolver::isDecisionLiteral ( IDAddress litaddr ) [inline, protected]

Checks if a given atom is used as decision literal.

Parameters:

litaddr Atom address.

Returns:: True if litaddr is a decision literal and false otherwise.

Definition at line 295 of file CDNLSolver.h.

References cause.

Referenced by analysis(), and handlePreviousModel().

std::string CDNLSolver::litToString ( ID lit ) [static, protected]

Encodes a literal in a string.

Parameters:

lit	Literal to encode.

Returns:: String representation of lit.

Definition at line 665 of file CDNLSolver.cpp.

References ID::address, and ID::isNaf().

Referenced by flipDecisionLiteral(), getGuess(), InternalGroundASPSolver::getNextModel(), getNextModel(), InternalGroundASPSolver::getUnfoundedSet(), setFact(), startWatching(), stopWatching(), updateWatchingStructuresAfterClearFact(), and updateWatchingStructuresAfterSetFact().

void CDNLSolver::loadAddedNogoods ( ) [protected]

Definition at line 90 of file CDNLSolver.cpp.

References addNogoodAndUpdateWatchingStructures(), SimpleNogoodContainer::clear(), SimpleNogoodContainer::getNogood(), SimpleNogoodContainer::getNogoodCount(), and nogoodsToAdd.

Referenced by InternalGroundASPSolver::getInconsistencyCause(), InternalGroundASPSolver::getNextModel(), and getNextModel().

ID CDNLSolver::negation ( ID lit ) [inline, protected]

Negates a literal ID.

Parameters:

lit	Literal ID.

Returns:: Negated literal ID.

Definition at line 184 of file CDNLSolver.h.

References ID::address, ID::kind, and ID::NAF_MASK.

Referenced by InternalGroundASPSolver::createNogoodsForRuleBody(), InternalGroundASPSolver::createShiftedProgram(), InternalGroundASPSolver::createSingularLoopNogoods(), flipDecisionLiteral(), getGuess(), resolve(), and unitPropagation().

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

Removes a propagator callback.

Parameters:

pb	The callback to be removed.

Implements SATSolver.

Reimplemented in InternalGroundASPSolver.

Definition at line 770 of file CDNLSolver.cpp.

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

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

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

Reimplemented in InternalGroundASPSolver.

Definition at line 656 of file CDNLSolver.cpp.

References assignmentOrder, ctx, DBGLOG, ProgramCtx::registry(), and OrderedSet< T, H >::resize().

Referenced by CDNLSolver().

Nogood CDNLSolver::resolve	(	Nogood &	ng1,
		Nogood &	ng2,
		IDAddress	litadr
	)		`[protected]`

Definition at line 197 of file CDNLSolver.cpp.

References Set< T >::begin(), cntResSteps, NogoodContainer::createLiteral(), DBGLOG, Set< T >::end(), Set< T >::erase(), Nogood::insert(), and negation().

Referenced by analysis(), and InternalGroundASPSolver::getInconsistencyCause().

void CDNLSolver::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.

Implements SATSolver.

Reimplemented in InternalGroundASPSolver.

Definition at line 736 of file CDNLSolver.cpp.

References ID::address, assignedAtoms, assignmentOrder, cause, changedAtoms, conflicts, NogoodContainer::createLiteral(), ctx, currentDL, DBGLOG, decisionLiteralOfDecisionLevel, exhaustedDL, factsOnDecisionLevel, initWatchingStructures(), interpretation, ID::isNaf(), ProgramCtx::registry(), and setFact().

bool CDNLSolver::satisfied ( ID lit ) [inline, protected]

Checks if a literal is satisfied.

Parameters:

lit	Literal ID.

Returns:: True if lit is satisfied and false otherwise.

Definition at line 164 of file CDNLSolver.h.

References ID::address, assigned(), interpretation, and ID::isNaf().

Referenced by InternalGroundASPSolver::getInitialNewlyUnfoundedAtomsAfterSetFact(), InternalGroundASPSolver::getLoopNogood(), InternalGroundASPSolver::getPossibleSourceRule(), and InternalGroundASPSolver::useAsNewSourceForHeadAtom().

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

Reimplemented in InternalGroundASPSolver.

Definition at line 213 of file CDNLSolver.cpp.

References ID::address, assignedAtoms, assignmentOrder, cause, changedAtoms, cntAssignments, DBGLOG, decisionlevel, factsOnDecisionLevel, NogoodSet::getNogood(), OrderedSet< T, H >::insert(), interpretation, ID::isNaf(), litToString(), nogoodset, and updateWatchingStructuresAfterSetFact().

Referenced by flipDecisionLiteral(), getNextModel(), restartWithAssumptions(), and unitPropagation().

void CDNLSolver::startWatching	(	int	nogoodNr,
		ID	lit
	)		`[protected]`

Adds a single watche for a nogood.

Parameters:

nogoodNr	Index of the nogood to add the watche for.
lit	The literal which shall now be watched.

Definition at line 614 of file CDNLSolver.cpp.

References ID::address, NogoodContainer::createLiteral(), DBGLOGD, ID::isNaf(), litToString(), watchedLiteralsOfNogood, watchingNogoodsOfNegLiteral, and watchingNogoodsOfPosLiteral.

Referenced by updateWatchingStructuresAfterAddNogood(), updateWatchingStructuresAfterClearFact(), and updateWatchingStructuresAfterSetFact().

void CDNLSolver::stopWatching	(	int	nogoodNr,
		ID	lit
	)		`[protected]`

Removed a single watche for a nogood.

Parameters:

nogoodNr	Index of the nogood to remove the watche for.
lit	The literal which shall not be watched any longer.

Definition at line 601 of file CDNLSolver.cpp.

References ID::address, NogoodContainer::createLiteral(), DBGLOGD, ID::isNaf(), litToString(), watchedLiteralsOfNogood, watchingNogoodsOfNegLiteral, and watchingNogoodsOfPosLiteral.

Referenced by updateWatchingStructuresAfterRemoveNogood(), and updateWatchingStructuresAfterSetFact().

void CDNLSolver::touchVarsInNogood ( Nogood & ng ) [protected]

Increses the usage counter for all variables in a nogood.

Parameters:

ng	The nogood whose variables shall be touched.

Definition at line 627 of file CDNLSolver.cpp.

References ID::address, ID::isNaf(), varCounterNeg, and varCounterPos.

Referenced by analysis().

bool CDNLSolver::unitPropagation ( Nogood & violatedNogood ) [protected]

Definition at line 55 of file CDNLSolver.cpp.

References ID::address, assigned(), Set< T >::begin(), contradictoryNogoods, DBGLOG, decisionlevel, Set< T >::erase(), NogoodSet::getNogood(), negation(), nogoodset, setFact(), Set< T >::size(), unitNogoods, and watchedLiteralsOfNogood.

Referenced by InternalGroundASPSolver::getNextModel(), and getNextModel().

void CDNLSolver::updateWatchingStructuresAfterAddNogood ( int index ) [protected]

Updates all data structures after a nogood was added.

Parameters:

index Index of added nogood.

Definition at line 371 of file CDNLSolver.cpp.

References ID::address, assigned(), Set< T >::clear(), contradictoryNogoods, NogoodContainer::createLiteral(), DBGLOGD, falsified(), NogoodSet::getNogood(), Set< T >::insert(), ID::isNaf(), nogoodset, nogoodsOfNegLiteral, nogoodsOfPosLiteral, Set< T >::size(), startWatching(), tmpWatched, and unitNogoods.

Referenced by addNogoodAndUpdateWatchingStructures(), and initWatchingStructures().

void CDNLSolver::updateWatchingStructuresAfterClearFact ( ID lit ) [protected]

Updates all data structures after a literal was unassigned.

Parameters:

lit	Literal which is now unassigned.

Definition at line 507 of file CDNLSolver.cpp.

References ID::address, assigned(), Set< T >::clear(), contradictoryNogoods, NogoodContainer::createLiteral(), DBGLOG, DBGLOGD, Set< T >::erase(), falsified(), NogoodSet::getNogood(), Set< T >::insert(), litToString(), nogoodset, nogoodsOfNegLiteral, nogoodsOfPosLiteral, Set< T >::size(), startWatching(), tmpWatched, unitNogoods, and watchedLiteralsOfNogood.

Referenced by clearFact().

void CDNLSolver::updateWatchingStructuresAfterRemoveNogood ( int index ) [protected]

Updates all data structures after a nogood was removed.

Parameters:

index Former index of removed nogood.

Definition at line 420 of file CDNLSolver.cpp.

References ID::address, NogoodSet::getNogood(), nogoodset, nogoodsOfNegLiteral, nogoodsOfPosLiteral, stopWatching(), and watchedLiteralsOfNogood.

void CDNLSolver::updateWatchingStructuresAfterSetFact ( ID lit ) [protected]

Updates all data structures after a literal was assigned to true.

Parameters:

lit	Literal which is now true.

Definition at line 438 of file CDNLSolver.cpp.

References ID::address, assigned(), contradictoryNogoods, NogoodContainer::createLiteral(), DBGLOGD, Set< T >::erase(), falsified(), NogoodSet::getNogood(), inactivateNogood(), Set< T >::insert(), ID::isNaf(), litToString(), nogoodset, startWatching(), stopWatching(), unitNogoods, watchedLiteralsOfNogood, watchingNogoodsOfNegLiteral, and watchingNogoodsOfPosLiteral.

Referenced by setFact().

Field Documentation

Set<IDAddress> CDNLSolver::allAtoms [protected]

Atoms of the instance as Set.

Definition at line 82 of file CDNLSolver.h.

Referenced by addNogoodAndUpdateWatchingStructures(), analysis(), complete(), InternalGroundASPSolver::computeStronglyConnectedComponents(), InternalGroundASPSolver::createNewBodyAtom(), getGuess(), InternalGroundASPSolver::getImplicationGraphAsDotString(), InternalGroundASPSolver::getNextModel(), handlePreviousModel(), InternalGroundASPSolver::initializeLists(), initListOfAllAtoms(), and InternalGroundASPSolver::restartWithAssumptions().

InterpretationPtr CDNLSolver::assignedAtoms [protected]

Set of assigned atoms.

Definition at line 92 of file CDNLSolver.h.

Referenced by assigned(), CDNLSolver(), clearFact(), complete(), getGuess(), InternalGroundASPSolver::getImplicationGraphAsDotString(), InternalGroundASPSolver::getNextModel(), getNextModel(), InternalGroundASPSolver::restartWithAssumptions(), restartWithAssumptions(), and setFact().

OrderedSet<IDAddress, SimpleHashIDAddress> CDNLSolver::assignmentOrder [protected]

Stores the current assignment in chronoligical order.

Definition at line 102 of file CDNLSolver.h.

Referenced by clearFact(), getAssignmentOrderIndex(), resizeVectors(), restartWithAssumptions(), and setFact().

boost::unordered_map<IDAddress, int, SimpleHashIDAddress> CDNLSolver::cause [protected]

Stores for each atom the index and hash of the clause which implied it; undefined if unassigned or guessed.

Definition at line 98 of file CDNLSolver.h.

Referenced by analysis(), clearFact(), getCause(), InternalGroundASPSolver::getImplicationGraphAsDotString(), InternalGroundASPSolver::getInconsistencyCause(), isDecisionLiteral(), restartWithAssumptions(), InternalGroundASPSolver::setFact(), and setFact().

InterpretationPtr CDNLSolver::changedAtoms [protected]

Set of atoms which (possibly) changes since last call of external learners because they have been reassigned.

Definition at line 240 of file CDNLSolver.h.

Referenced by CDNLSolver(), clearFact(), InternalGroundASPSolver::getNextModel(), getNextModel(), restartWithAssumptions(), and setFact().

long CDNLSolver::cntAssignments [protected]

Number of assignments so far.

Definition at line 140 of file CDNLSolver.h.

Referenced by getStatistics(), and setFact().

long CDNLSolver::cntBacktracks [protected]

Number of backtracks so far.

Definition at line 144 of file CDNLSolver.h.

Referenced by backtrack(), and getStatistics().

long CDNLSolver::cntDetectedConflicts [protected]

Number of conflicts so far.

Definition at line 148 of file CDNLSolver.h.

Referenced by analysis(), and getStatistics().

long CDNLSolver::cntGuesses [protected]

Number of guesses so far.

Definition at line 142 of file CDNLSolver.h.

Referenced by getGuess(), and getStatistics().

long CDNLSolver::cntResSteps [protected]

Number of resolution steps so far.

Definition at line 146 of file CDNLSolver.h.

Referenced by analysis(), getStatistics(), and resolve().

int CDNLSolver::conflicts [protected]

Counter for total number of conflicts so far (periodic reset).

Definition at line 130 of file CDNLSolver.h.

Referenced by analysis(), and restartWithAssumptions().

Set<int> CDNLSolver::contradictoryNogoods [protected]

Stores the nogoods which are currently contradictory (i.e., all literals are satisfied).

Definition at line 126 of file CDNLSolver.h.

Referenced by getContradictoryNogoods(), InternalGroundASPSolver::getImplicationGraphAsDotString(), InternalGroundASPSolver::getInconsistencyCause(), inactivateNogood(), initWatchingStructures(), unitPropagation(), updateWatchingStructuresAfterAddNogood(), updateWatchingStructuresAfterClearFact(), and updateWatchingStructuresAfterSetFact().

ProgramCtx& CDNLSolver::ctx [protected]

ProgramCtx.

Definition at line 84 of file CDNLSolver.h.

Referenced by CDNLSolver(), InternalGroundASPSolver::InternalGroundASPSolver(), resizeVectors(), and restartWithAssumptions().

int CDNLSolver::currentDL [protected]

Current decision level >= 0.

Definition at line 100 of file CDNLSolver.h.

Referenced by CDNLSolver(), flipDecisionLiteral(), InternalGroundASPSolver::getNextModel(), getNextModel(), handlePreviousModel(), and restartWithAssumptions().

DynamicVector<IDAddress, int> CDNLSolver::decisionlevel [protected]

Decision level for each atom; undefined if unassigned.

Definition at line 94 of file CDNLSolver.h.

Referenced by analysis(), clearFact(), InternalGroundASPSolver::getImplicationGraphAsDotString(), InternalGroundASPSolver::getInconsistencyCause(), setFact(), unitPropagation(), and InternalGroundASPSolver::useAsNewSourceForHeadAtom().

DynamicVector<int, ID> CDNLSolver::decisionLiteralOfDecisionLevel [protected]

Stores for each decision level the guessed literal (=decision literal).

Definition at line 110 of file CDNLSolver.h.

Referenced by flipDecisionLiteral(), InternalGroundASPSolver::getNextModel(), getNextModel(), and restartWithAssumptions().

int CDNLSolver::exhaustedDL [protected]

Maximum decision level such that the search space above was exhausted (used for eliminating duplicate models without explicitly adding them as nogoods).

Definition at line 108 of file CDNLSolver.h.

Referenced by CDNLSolver(), flipDecisionLiteral(), InternalGroundASPSolver::getNextModel(), getNextModel(), and restartWithAssumptions().

DynamicVector<int, std::vector<IDAddress> > CDNLSolver::factsOnDecisionLevel [protected]

Stores for each decision level the facts assigned on that level.

Definition at line 104 of file CDNLSolver.h.

Referenced by backtrack(), restartWithAssumptions(), and setFact().

DynamicVector<IDAddress, int> CDNLSolver::flipped [protected]

Stores for decision literals if they have already been flipped.

Definition at line 96 of file CDNLSolver.h.

Referenced by flipDecisionLiteral(), InternalGroundASPSolver::getImplicationGraphAsDotString(), and getNextModel().

InterpretationPtr CDNLSolver::interpretation [protected]

Current (partial) interpretation.

Definition at line 90 of file CDNLSolver.h.

Referenced by CDNLSolver(), clearFact(), falsified(), InternalGroundASPSolver::getImplicationGraphAsDotString(), InternalGroundASPSolver::getNextModel(), getNextModel(), handlePreviousModel(), restartWithAssumptions(), satisfied(), and setFact().

NogoodSet CDNLSolver::nogoodset [protected]

boost::unordered_map<IDAddress, Set<int>, SimpleHashIDAddress > CDNLSolver::nogoodsOfNegLiteral [protected]

Stores for each negative literal the nogoods which contain.

Definition at line 116 of file CDNLSolver.h.

Referenced by initWatchingStructures(), updateWatchingStructuresAfterAddNogood(), updateWatchingStructuresAfterClearFact(), and updateWatchingStructuresAfterRemoveNogood().

boost::unordered_map<IDAddress, Set<int>, SimpleHashIDAddress > CDNLSolver::nogoodsOfPosLiteral [protected]

Stores for each positive literal the nogoods which contain.

Definition at line 114 of file CDNLSolver.h.

Referenced by initWatchingStructures(), updateWatchingStructuresAfterAddNogood(), updateWatchingStructuresAfterClearFact(), and updateWatchingStructuresAfterRemoveNogood().

SimpleNogoodContainer CDNLSolver::nogoodsToAdd [protected]

Nogoods scheduled for adding but not added yet.

Definition at line 86 of file CDNLSolver.h.

Referenced by addNogood(), and loadAddedNogoods().

Set<PropagatorCallback*> CDNLSolver::propagator [protected]

Set of external propagators.

Definition at line 242 of file CDNLSolver.h.

Referenced by InternalGroundASPSolver::addPropagator(), addPropagator(), InternalGroundASPSolver::getNextModel(), getNextModel(), InternalGroundASPSolver::removePropagator(), and removePropagator().

std::vector<int> CDNLSolver::recentConflicts [protected]

Stores the indexes of the clauses which were recently contradictory in chronological order.

Definition at line 136 of file CDNLSolver.h.

Referenced by getGuess(), InternalGroundASPSolver::getNextModel(), getNextModel(), and handlePreviousModel().

Set<ID> CDNLSolver::tmpWatched [protected]

Temporary objects (they are just class members in order to make them reuseable without reallocation).

Definition at line 151 of file CDNLSolver.h.

Referenced by updateWatchingStructuresAfterAddNogood(), and updateWatchingStructuresAfterClearFact().

Set<int> CDNLSolver::unitNogoods [protected]

Stores the nogoods which are currently unit (i.e., all literals but one are satisfied).

Definition at line 124 of file CDNLSolver.h.

Referenced by inactivateNogood(), initWatchingStructures(), unitPropagation(), updateWatchingStructuresAfterAddNogood(), updateWatchingStructuresAfterClearFact(), and updateWatchingStructuresAfterSetFact().

boost::unordered_map<IDAddress, int, SimpleHashIDAddress> CDNLSolver::varCounterNeg [protected]

Counts for each negative literal the number of conflicts it was involved in (periodic reset).

Definition at line 134 of file CDNLSolver.h.

Referenced by analysis(), getGuess(), and touchVarsInNogood().

boost::unordered_map<IDAddress, int, SimpleHashIDAddress> CDNLSolver::varCounterPos [protected]

Counts for each positive literal the number of conflicts it was involved in (periodic reset).

Definition at line 132 of file CDNLSolver.h.

Referenced by analysis(), getGuess(), and touchVarsInNogood().

std::vector<Set<ID> > CDNLSolver::watchedLiteralsOfNogood [protected]

Stores for each nogood the set of watched literals.

Definition at line 122 of file CDNLSolver.h.

Referenced by addNogoodAndUpdateWatchingStructures(), getGuess(), inactivateNogood(), initWatchingStructures(), startWatching(), stopWatching(), unitPropagation(), updateWatchingStructuresAfterClearFact(), updateWatchingStructuresAfterRemoveNogood(), and updateWatchingStructuresAfterSetFact().

boost::unordered_map<IDAddress, Set<int>, SimpleHashIDAddress > CDNLSolver::watchingNogoodsOfNegLiteral [protected]

Stores for each negative literal the nogoods which watch it (i.e., which might fire once the literal becomes true).

Definition at line 120 of file CDNLSolver.h.

Referenced by inactivateNogood(), initWatchingStructures(), startWatching(), stopWatching(), and updateWatchingStructuresAfterSetFact().

boost::unordered_map<IDAddress, Set<int>, SimpleHashIDAddress > CDNLSolver::watchingNogoodsOfPosLiteral [protected]

Stores for each positive literal the nogoods which watch it (i.e., which might fire once the literal becomes true).

Definition at line 118 of file CDNLSolver.h.

Referenced by inactivateNogood(), initWatchingStructures(), startWatching(), stopWatching(), and updateWatchingStructuresAfterSetFact().

The documentation for this class was generated from the following files:

include/dlvhex2/CDNLSolver.h
src/CDNLSolver.cpp

Data Structures

Public Types

Public Member Functions

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

Constructor & Destructor Documentation

Member Function Documentation

Field Documentation