Base class for ground ASP solvers. More...

#include <include/dlvhex2/GenuineSolver.h>

Inheritance diagram for GenuineGroundSolver:

Collaboration diagram for GenuineGroundSolver:

Public Types
typedef boost::shared_ptr < GenuineGroundSolver >	Ptr
typedef boost::shared_ptr < const GenuineGroundSolver >	ConstPtr
Public Member Functions
virtual std::string	getStatistics ()=0
	Create solver statistics in a no further specified format (for debug purposes).
virtual void	setOptimum (std::vector< int > &optimum)=0
	Sets the current optimum for optimization problems.
virtual InterpretationPtr	getNextModel ()=0
	Returns the next model.
virtual int	getModelCount ()=0
	Returns the number of models enumerated so far.
virtual void	restartWithAssumptions (const std::vector< ID > &assumptions)=0
	Resets the search and assumes truth values for selected atoms.
virtual void	addPropagator (PropagatorCallback *pb)=0
	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)=0
	Removes a propagator callback.
virtual void	addProgram (const AnnotatedGroundProgram &program, InterpretationConstPtr frozen=InterpretationConstPtr())=0
	Incrementally adds another program component to the solver.
virtual Nogood	getInconsistencyCause (InterpretationConstPtr explanationAtoms)=0
	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())=0
	Adds a set of nogoods to the solver.
Static Public Member Functions
static Ptr	getInstance (ProgramCtx &ctx, const OrdinaryASPProgram &program, InterpretationConstPtr frozen=InterpretationConstPtr(), bool minCheck=true)
	Interprets the settings in `ctx` and creates an instance of a concrete subclass of this class, which implements a specific ground program solver.
static Ptr	getInstance (ProgramCtx &ctx, const AnnotatedGroundProgram &program, InterpretationConstPtr frozen=InterpretationConstPtr(), bool minCheck=true)
	Interprets the settings in `ctx` and creates an instance of a concrete subclass of this class, which implements a specific ground program solver.

Detailed Description

Base class for ground ASP solvers.

Definition at line 103 of file GenuineSolver.h.

Member Typedef Documentation

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

Reimplemented from NogoodContainer.

Reimplemented in InternalGroundASPSolver, GenuineSolver, and InternalGroundDASPSolver.

Definition at line 199 of file GenuineSolver.h.

typedef boost::shared_ptr<GenuineGroundSolver> GenuineGroundSolver::Ptr

Reimplemented from NogoodContainer.

Reimplemented in InternalGroundASPSolver, GenuineSolver, and InternalGroundDASPSolver.

Definition at line 198 of file GenuineSolver.h.

Member Function Documentation

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

Adds a set of nogoods to the solver.

Parameters:

ns	Encoding of the SAT instance as a set of nogoods.
frozen	A set of atoms which occur in `ns` and are saved from being optimized away (e.g. because their truth values are relevant). if NULL, then all variables are frozen.

Implemented in InternalGroundASPSolver, and GenuineSolver.

virtual void GenuineGroundSolver::addProgram	(	const AnnotatedGroundProgram &	program,
		InterpretationConstPtr	frozen = `InterpretationConstPtr()`
	)		`[pure 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).

Implemented in InternalGroundASPSolver, and GenuineSolver.

virtual void GenuineGroundSolver::addPropagator ( PropagatorCallback * pb ) [pure 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.

Parameters:

pb	The callback to be added.

Implemented in InternalGroundASPSolver, and GenuineSolver.

virtual Nogood GenuineGroundSolver::getInconsistencyCause ( InterpretationConstPtr explanationAtoms ) [pure virtual]

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

Let A be the set of explanationAtoms. Let further P be the program with IDB I and EDB E. A proto-explanation X is a subset of A such that for any program P' with IDB I and EDB E', where E' coincides with E on all atoms which are (i) not in A or (ii) in X, is inconsistent. That is, X guarantees the inconsistency all programs with the same IDB I and the same EDB over atoms other than A, while facts over atoms in A but not in X are not relevant for inconsistency. (Note that set A itself is always a proto-explanation for an inconsistent program P because then the only possible P' is P itself.)

Example: A proto-explanation of the Program

 a. b.
 :- a, not c.

wrt. A={a,b,c} is X={a,c} because any program with the same IDB, fact a and c not being a fact is inconsistent (while b might be removed as a fact and the program is still inconsistent).

An explanation is a proto-explanation X if all atoms in X are turned into signed literals, where the sign is positive if it is a fact in P and negative otherwise.

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.

Implemented in InternalGroundASPSolver, and GenuineSolver.

GenuineGroundSolverPtr GenuineGroundSolver::getInstance	(	ProgramCtx &	ctx,
		const OrdinaryASPProgram &	program,
		InterpretationConstPtr	frozen = `InterpretationConstPtr()`,
		bool	minCheck = `true`
	)		`[static]`

Interprets the settings in ctx and creates an instance of a concrete subclass of this class, which implements a specific ground program solver.

Parameters:

ctx	ProgramCtx.
program	Ground program to be solved; will automatically be wrapped in an AnnotatedGroundProgram.
frozen	A set of atoms which occur in `ns` and are saved from being optimized away (e.g. because their trutz values are relevant). if NULL, then all variables are frozen.
minCheck	True to force a minimality check for detecting unfounded sets due to disjunctions before returning a model. False leaves the decision open to the implementer of this class and might be more efficient. This might be useful to avoid redundancy if the caller performs an extended unfounded set check anyway (e.g. for detecting unfounded sets due to external atoms).

Returns:: Pointer to the new grounder instance.

Reimplemented in GenuineSolver.

Definition at line 138 of file GenuineSolver.cpp.

References ProgramCtx::config, DBGLOG, and Configuration::getOption().

Referenced by GenuineGuessAndCheckModelGenerator::GenuineGuessAndCheckModelGenerator(), and GenuinePlainModelGenerator::GenuinePlainModelGenerator().

GenuineGroundSolverPtr GenuineGroundSolver::getInstance	(	ProgramCtx &	ctx,
		const AnnotatedGroundProgram &	program,
		InterpretationConstPtr	frozen = `InterpretationConstPtr()`,
		bool	minCheck = `true`
	)		`[static]`

Interprets the settings in ctx and creates an instance of a concrete subclass of this class, which implements a specific ground program solver.

Parameters:

ctx	ProgramCtx.
program	Ground program to be solved.
frozen	A set of atoms which occur in `ns` and are saved from being optimized away (e.g. because their trutz values are relevant); if NULL, then all variables are frozen.
minCheck	True to force a minimality check for detecting unfounded sets due to disjunctions before returning a model. False leaves the decision open to the implementer of this class and might be more efficient. This might be useful to avoid redundancy if the caller performs an extended unfounded set check anyway (e.g. for detecting unfounded sets due to external atoms).

Returns:: Pointer to the new grounder instance.

Definition at line 108 of file GenuineSolver.cpp.

References ProgramCtx::config, DBGLOG, and Configuration::getOption().

virtual int GenuineGroundSolver::getModelCount ( ) [pure virtual]

Returns the number of models enumerated so far.

Returns:: Model count.

Implemented in InternalGroundASPSolver, and GenuineSolver.

virtual InterpretationPtr GenuineGroundSolver::getNextModel ( ) [pure 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 OrdinaryASPSolver.

Implemented in InternalGroundASPSolver, GenuineSolver, and InternalGroundDASPSolver.

virtual std::string GenuineGroundSolver::getStatistics ( ) [pure virtual]

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

Returns:: Debug statistics.

Implemented in InternalGroundASPSolver, and GenuineSolver.

virtual void GenuineGroundSolver::removePropagator ( PropagatorCallback * pb ) [pure virtual]

Removes a propagator callback.

Parameters:

pb	The callback to be removed.

Implemented in InternalGroundASPSolver, and GenuineSolver.

virtual void GenuineGroundSolver::restartWithAssumptions ( const std::vector< ID > & assumptions ) [pure 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.

Implemented in InternalGroundASPSolver, and GenuineSolver.

virtual void GenuineGroundSolver::setOptimum ( std::vector< int > & optimum ) [pure 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).

Implemented in InternalGroundASPSolver, and GenuineSolver.

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

include/dlvhex2/GenuineSolver.h
src/GenuineSolver.cpp

Public Types

Public Member Functions

Static Public Member Functions

Detailed Description

Member Typedef Documentation

Member Function Documentation