Clasp::BasicSolve Class Reference

#include <solve_algorithms.h>

List of all members.

Classes
struct	State
Public Member Functions
bool	assume (const LitVec &assumptions)
	Enables solving under the given assumptions.
	BasicSolve (Solver &s, const SolveParams &p, SolveLimits *lim=0)
	Creates a new object for solving with the given solver using the given solving options.
	BasicSolve (Solver &s, SolveLimits *lim=0)
void	reset (bool reinit=false)
	Resets the internal solving state while keeping the solver and the solving options.
void	reset (Solver &s, const SolveParams &p, SolveLimits *lim=0)
	Replaces *this with BasicSolve(s, p).
bool	satisfiable (const LitVec &assumptions, bool init)
	Returns whether the given problem is satisfiable under the given assumptions.
ValueRep	solve ()
	Solves the path stored in the given solver using the given solving options.
Solver &	solver ()
	~BasicSolve ()
Private Types
typedef SolveLimits	Limits
typedef const SolveParams	Params
Private Member Functions
	BasicSolve (const BasicSolve &)
BasicSolve &	operator= (const BasicSolve &)
Private Attributes
Limits *	limits_
Params *	params_
Solver *	solver_
State *	state_

---

Detailed Description

Basic (sequential) solving using given solving options.

Definition at line 50 of file solve_algorithms.h.

---

Member Typedef Documentation

typedef SolveLimits Clasp::BasicSolve::Limits [private]

Definition at line 99 of file solve_algorithms.h.

typedef const SolveParams Clasp::BasicSolve::Params [private]

Definition at line 98 of file solve_algorithms.h.

---

Constructor & Destructor Documentation

Clasp::BasicSolve::BasicSolve	(	Solver &	s,
		const SolveParams &	p,
		SolveLimits *	lim = 0
	)

Creates a new object for solving with the given solver using the given solving options.

Precondition:

s is attached to a problem (SharedContext).

Parameters:

lim	Solving limits to apply (in/out parameter).

Definition at line 46 of file solve_algorithms.cpp.

Clasp::BasicSolve::BasicSolve	(	Solver &	s,
		SolveLimits *	lim = 0
	)

Definition at line 45 of file solve_algorithms.cpp.

Clasp::BasicSolve::~BasicSolve

(

)

Definition at line 53 of file solve_algorithms.cpp.

Clasp::BasicSolve::BasicSolve

(

const BasicSolve &

)

[private]

---

Member Function Documentation

bool Clasp::BasicSolve::assume

(

const LitVec &

assumptions

)

Enables solving under the given assumptions.

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

Parameters:

assumptions

A list of unit assumptions to be assumed true.

Returns:

false if assumptions are conflicting.

Definition at line 85 of file solve_algorithms.cpp.

BasicSolve& Clasp::BasicSolve::operator=

(

const BasicSolve &

)

[private]

void Clasp::BasicSolve::reset

(

bool

reinit = false

)

Resets the internal solving state while keeping the solver and the solving options.

Definition at line 54 of file solve_algorithms.cpp.

void Clasp::BasicSolve::reset	(	Solver &	s,
		const SolveParams &	p,
		SolveLimits *	lim = 0
	)

Replaces *this with BasicSolve(s, p).

Definition at line 64 of file solve_algorithms.cpp.

bool Clasp::BasicSolve::satisfiable	(	const LitVec &	assumptions,
		bool	init
	)

Returns whether the given problem is satisfiable under the given assumptions.

Calls assume(assumptions) followed by solve() but does not maintain any solving state.

Parameters:

init	Call InitParams::randomize() before starting search?

Definition at line 78 of file solve_algorithms.cpp.

ValueRep Clasp::BasicSolve::solve

(

)

Solves the path stored in the given solver using the given solving options.

Returns:

• value_true if search stopped on a model.
• value_false if the search-space was completely examined.
• value_free if the given solve limit was hit.

Note:

The function maintains the current solving state (number of restarts, learnt limits, ...) between calls.

Definition at line 71 of file solve_algorithms.cpp.

Solver& Clasp::BasicSolve::solver

(

)

[inline]

Definition at line 94 of file solve_algorithms.h.

---

Member Data Documentation

Limits* Clasp::BasicSolve::limits_ [private]

Definition at line 103 of file solve_algorithms.h.

Params* Clasp::BasicSolve::params_ [private]

Definition at line 102 of file solve_algorithms.h.

Solver* Clasp::BasicSolve::solver_ [private]

Definition at line 100 of file solve_algorithms.h.

State* Clasp::BasicSolve::state_ [private]

Definition at line 104 of file solve_algorithms.h.

---

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

• solve_algorithms.h
• solve_algorithms.cpp