Clasp::SolveAlgorithm Class Reference

Interface for complex solve algorithms. More...

#include <solve_algorithms.h>

Inheritance diagram for Clasp::SolveAlgorithm:

List of all members.

Public Member Functions
virtual void	enableInterrupts ()=0
	Prepares the algorithm for handling (asynchronous) calls to SolveAlgorithm::terminate(int).
const Enumerator *	enumerator () const
bool	interrupt ()
	Tries to terminate the current solve process.
virtual bool	interrupted () const =0
const SolveLimits &	limits () const
virtual void	resetSolve ()=0
	Resets solving state and sticky messages like terminate.
void	setEnumerator (Enumerator &e)
void	setEnumLimit (uint64 m)
void	setLimits (const SolveLimits &x)
bool	solve (SharedContext &ctx, const LitVec &assume=LitVec(), EventHandler *modelHandler=0)
	Runs the solve algorithm.
	SolveAlgorithm (Enumerator *enumerator=0, const SolveLimits &limit=SolveLimits())
virtual	~SolveAlgorithm ()
Protected Member Functions
virtual bool	doInterrupt ()=0
	Shall return true if termination is supported, otherwise false.
virtual bool	doSolve (SharedContext &ctx, const LitVec &assume)=0
	The actual solve algorithm.
Enumerator &	enumerator ()
SolveAlgorithm &	operator= (const SolveAlgorithm &)
bool	reportModel (Solver &s) const
	SolveAlgorithm (const SolveAlgorithm &)
Private Attributes
Enumerator *	enum_
uint64	enumLimit_
SolveLimits	limits_
EventHandler *	onModel_

---

Detailed Description

Interface for complex solve algorithms.

SolveAlgorithms implement complex algorithms like enumeration or optimization.

Definition at line 125 of file solve_algorithms.h.

---

Constructor & Destructor Documentation

Clasp::SolveAlgorithm::SolveAlgorithm	(	Enumerator *	enumerator = 0,
		const SolveLimits &	limit = SolveLimits()
	)		[explicit]

Parameters:

lim	An optional solve limit applied in solve().

Definition at line 227 of file solve_algorithms.cpp.

Clasp::SolveAlgorithm::~SolveAlgorithm

(

)

[virtual]

Definition at line 228 of file solve_algorithms.cpp.

Clasp::SolveAlgorithm::SolveAlgorithm

(

const SolveAlgorithm &

)

[protected]

---

Member Function Documentation

virtual bool Clasp::SolveAlgorithm::doInterrupt

(

)

[protected, pure virtual]

Shall return true if termination is supported, otherwise false.

Implemented in Clasp::SequentialSolve.

virtual bool Clasp::SolveAlgorithm::doSolve	(	SharedContext &	ctx,
		const LitVec &	assume
	)		[protected, pure virtual]

The actual solve algorithm.

Implemented in Clasp::SequentialSolve.

virtual void Clasp::SolveAlgorithm::enableInterrupts

(

)

[pure virtual]

Prepares the algorithm for handling (asynchronous) calls to SolveAlgorithm::terminate(int).

Implemented in Clasp::SequentialSolve.

const Enumerator* Clasp::SolveAlgorithm::enumerator

(

)

const [inline]

Definition at line 133 of file solve_algorithms.h.

Enumerator& Clasp::SolveAlgorithm::enumerator

(

)

[inline, protected]

Definition at line 179 of file solve_algorithms.h.

bool Clasp::SolveAlgorithm::interrupt

(

)

Tries to terminate the current solve process.

Note:

If enableInterrupts() was not called, SolveAlgorithm::interrupt() may return false to signal that (asynchronous) termination is not supported.

Definition at line 230 of file solve_algorithms.cpp.

virtual bool Clasp::SolveAlgorithm::interrupted

(

)

const [pure virtual]

Implemented in Clasp::SequentialSolve.

const SolveLimits& Clasp::SolveAlgorithm::limits

(

)

const [inline]

Definition at line 134 of file solve_algorithms.h.

SolveAlgorithm& Clasp::SolveAlgorithm::operator=

(

const SolveAlgorithm &

)

[protected]

bool Clasp::SolveAlgorithm::reportModel

(

Solver &

s

)

const [protected]

Definition at line 258 of file solve_algorithms.cpp.

virtual void Clasp::SolveAlgorithm::resetSolve

(

)

[pure virtual]

Resets solving state and sticky messages like terminate.

Note:

The function must be called between successive calls to solve().

Implemented in Clasp::SequentialSolve.

void Clasp::SolveAlgorithm::setEnumerator

(

Enumerator &

e

)

[inline]

Definition at line 137 of file solve_algorithms.h.

void Clasp::SolveAlgorithm::setEnumLimit

(

uint64

m

)

[inline]

Definition at line 138 of file solve_algorithms.h.

void Clasp::SolveAlgorithm::setLimits

(

const SolveLimits &

x

)

[inline]

Definition at line 139 of file solve_algorithms.h.

bool Clasp::SolveAlgorithm::solve	(	SharedContext &	ctx,
		const LitVec &	assume = LitVec(),
		EventHandler *	modelHandler = 0
	)

Runs the solve algorithm.

Parameters:

ctx	A context object containing the problem.
assume	A list of initial unit-assumptions.

Returns:

• true: if the search stopped before the search-space was exceeded.
• false: if the search-space was completely examined.

Note:

The use of assumptions allows for incremental solving. Literals contained in assumptions are assumed to be true during search but are undone before solve returns.

Definition at line 233 of file solve_algorithms.cpp.

---

Member Data Documentation

Enumerator* Clasp::SolveAlgorithm::enum_ [private]

Definition at line 182 of file solve_algorithms.h.

uint64 Clasp::SolveAlgorithm::enumLimit_ [private]

Definition at line 184 of file solve_algorithms.h.

SolveLimits Clasp::SolveAlgorithm::limits_ [private]

Definition at line 181 of file solve_algorithms.h.

EventHandler* Clasp::SolveAlgorithm::onModel_ [private]

Definition at line 183 of file solve_algorithms.h.

---

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

• solve_algorithms.h
• solve_algorithms.cpp