This class combines a grounder and a solver to support direct solving of nonground programs. More...

#include <include/dlvhex2/GenuineSolver.h>

Inheritance diagram for GenuineSolver:

Collaboration diagram for GenuineSolver:

Public Types
typedef boost::shared_ptr < GenuineSolver >	Ptr
typedef boost::shared_ptr < const GenuineSolver >	ConstPtr
Public Member Functions
const OrdinaryASPProgram &	getGroundProgram ()
	Getter for the internal ground program.
std::string	getStatistics ()
	Create solver statistics in a no further specified format (for debug purposes).
void	setOptimum (std::vector< int > &optimum)
	Sets the current optimum for optimization problems.
InterpretationPtr	getNextModel ()
	Returns the next model.
int	getModelCount ()
	Returns the number of models enumerated so far.
void	addNogood (Nogood ng)
	Adds a nogood to the container.
void	restartWithAssumptions (const std::vector< ID > &assumptions)
	Resets the search and assumes truth values for selected atoms.
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.
void	removePropagator (PropagatorCallback *pb)
	Removes a propagator callback.
void	addProgram (const AnnotatedGroundProgram &program, InterpretationConstPtr frozen=InterpretationConstPtr())
	Incrementally adds another program component to the solver.
Nogood	getInconsistencyCause (InterpretationConstPtr explanationAtoms)
	Returns an explanation for an inconsistency in terms of litervals over the atoms given in `explanationAtoms`.
void	addNogoodSet (const NogoodSet &ns, InterpretationConstPtr frozen=InterpretationConstPtr())
	Adds a set of nogoods to the solver.
GenuineGrounderPtr	getGenuineGrounder ()
	Returns a pointer to the internal grounder.
GenuineGroundSolverPtr	getGenuineGroundSolver ()
	Returns a pointer to the internal solver.
Static Public Member Functions
static Ptr	getInstance (ProgramCtx &ctx, const OrdinaryASPProgram &p, 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.
Private Member Functions
	GenuineSolver (GenuineGrounderPtr grounder, GenuineGroundSolverPtr solver, OrdinaryASPProgram gprog)
	Constructor.
Private Attributes
GenuineGrounderPtr	grounder
	Internal grounder.
GenuineGroundSolverPtr	solver
	Internal solver.
OrdinaryASPProgram	gprog
	Ground program produced by the grounder.

Detailed Description

This class combines a grounder and a solver to support direct solving of nonground programs.

Definition at line 236 of file GenuineSolver.h.

Member Typedef Documentation

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

Reimplemented from GenuineGrounder.

Definition at line 286 of file GenuineSolver.h.

typedef boost::shared_ptr<GenuineSolver> GenuineSolver::Ptr

Reimplemented from GenuineGrounder.

Definition at line 285 of file GenuineSolver.h.

Constructor & Destructor Documentation

GenuineSolver::GenuineSolver	(	GenuineGrounderPtr	grounder,
		GenuineGroundSolverPtr	solver,
		OrdinaryASPProgram	gprog
	)		`[inline, private]`

Constructor.

Parameters:

grounder	Grounder to be used.
solver	Solver to be used.
gprog	Ground program produced by `grounder`.

Definition at line 252 of file GenuineSolver.h.

Referenced by getInstance().

Member Function Documentation

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

Adds a nogood to the container.

Parameters:

ng	The nogood to add.

Implements NogoodContainer.

Definition at line 218 of file GenuineSolver.cpp.

References solver.

Referenced by DLVHEX_NAMESPACE_BEGIN::ExternalSolverHelper< GenuineSolver >::addNogood().

void GenuineSolver::addNogoodSet	(	const NogoodSet &	ns,
		InterpretationConstPtr	frozen = `InterpretationConstPtr()`
	)		`[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.

Implements GenuineGroundSolver.

Definition at line 251 of file GenuineSolver.cpp.

References solver.

void GenuineSolver::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 246 of file GenuineSolver.cpp.

References solver.

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

Parameters:

pb	The callback to be added.

Implements GenuineGroundSolver.

Definition at line 230 of file GenuineSolver.cpp.

References solver.

GenuineGrounderPtr GenuineSolver::getGenuineGrounder ( ) [inline]

Returns a pointer to the internal grounder.

Returns:: grounder.

Definition at line 277 of file GenuineSolver.h.

GenuineGroundSolverPtr GenuineSolver::getGenuineGroundSolver ( ) [inline]

Returns a pointer to the internal solver.

Returns:: solver.

Definition at line 283 of file GenuineSolver.h.

const OrdinaryASPProgram & GenuineSolver::getGroundProgram ( ) [virtual]

Getter for the internal ground program.

Returns:: Ground program gprog.

Implements GenuineGrounder.

Definition at line 193 of file GenuineSolver.cpp.

References gprog.

Nogood GenuineSolver::getInconsistencyCause ( InterpretationConstPtr explanationAtoms ) [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.

Implements GenuineGroundSolver.

Definition at line 241 of file GenuineSolver.cpp.

References solver.

GenuineSolverPtr GenuineSolver::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 from GenuineGroundSolver.

Definition at line 169 of file GenuineSolver.cpp.

References DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, GenuineSolver(), gprog, and grounder.

Referenced by GenuineWellfoundedModelGenerator::generateNextModel(), and GenuinePlainModelGenerator::GenuinePlainModelGenerator().

int GenuineSolver::getModelCount ( ) [virtual]

Returns the number of models enumerated so far.

Returns:: Model count.

Implements GenuineGroundSolver.

Definition at line 212 of file GenuineSolver.cpp.

References solver.

InterpretationPtr GenuineSolver::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 GenuineGroundSolver.

Definition at line 205 of file GenuineSolver.cpp.

References DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, and solver.

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

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

Returns:: Debug statistics.

Implements GenuineGroundSolver.

Definition at line 187 of file GenuineSolver.cpp.

References solver.

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

Removes a propagator callback.

Parameters:

pb	The callback to be removed.

Implements GenuineGroundSolver.

Definition at line 236 of file GenuineSolver.cpp.

References solver.

void GenuineSolver::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 GenuineGroundSolver.

Definition at line 224 of file GenuineSolver.cpp.

References solver.

void GenuineSolver::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 199 of file GenuineSolver.cpp.

References solver.