Inheritance diagram for Clasp::Restricted:

Public Types
typedef ConstraintType	con_t
typedef LitVec::size_type	size_t
Public Member Functions
bool	bump (const Solver &s, const WeightLitVec &w, double d)
	Shall bump the activity of literals in lits by lits.second * adj.
Literal	doSelect (Solver &s)
	Implements the actual selection process.
void	endInit (Solver &s)
void	newConstraint (const Solver &s, const Literal *p, size_t sz, con_t t)
bool	notify (Solver &s)
void	restoreOther (Solver &s)
	Restricted (const Lookahead::Params &p, uint32 numOps, DecisionHeuristic *other)
Literal	selectRange (Solver &s, const Literal f, const Literal l)
void	simplify (const Solver &s, size_t st)
void	startInit (const Solver &s)
void	undoUntil (const Solver &s, size_t st)
void	updateReason (const Solver &s, const LitVec &x, Literal r)
void	updateVar (const Solver &s, Var v, uint32 n)
Private Types
typedef SingleOwnerPtr < DecisionHeuristic >	HeuPtr
Private Attributes
uint32	numOps_
HeuPtr	other_

Detailed Description

Definition at line 390 of file lookahead.cpp.

Member Typedef Documentation

typedef ConstraintType Clasp::Restricted::con_t

Definition at line 393 of file lookahead.cpp.

typedef SingleOwnerPtr<DecisionHeuristic> Clasp::Restricted::HeuPtr [private]

Definition at line 429 of file lookahead.cpp.

typedef LitVec::size_type Clasp::Restricted::size_t

Definition at line 392 of file lookahead.cpp.

Constructor & Destructor Documentation

Clasp::Restricted::Restricted	(	const Lookahead::Params &	p,
		uint32	numOps,
		DecisionHeuristic *	other
	)		`[inline]`

Definition at line 394 of file lookahead.cpp.

Member Function Documentation

bool Clasp::Restricted::bump	(	const Solver &	,
		const WeightLitVec &	,
		double
	)		`[inline, virtual]`

Shall bump the activity of literals in lits by lits.second * adj.

The default-implementation is a noop and always returns false.

Returns:: true if heuristic supports activities, false otherwise.

Reimplemented from Clasp::DecisionHeuristic.

Definition at line 425 of file lookahead.cpp.

Literal Clasp::Restricted::doSelect ( Solver & ) [inline, virtual]

Implements the actual selection process.

Precondition:: s.numFreeVars() > 0, i.e. there is at least one variable to branch on.

Returns:

a literal that is currently free or
a sentinel literal. In that case, the heuristic shall have asserted a literal!

Reimplemented from Clasp::UnitHeuristic.

Definition at line 415 of file lookahead.cpp.

void Clasp::Restricted::endInit ( Solver & ) [inline, virtual]

Called once after all problem constraints are known to the solver and the problem was simplified. The default-implementation is a noop.

Parameters:

s	The solver in which this heuristic is used.

Reimplemented from Clasp::UnitHeuristic.

Definition at line 409 of file lookahead.cpp.

void Clasp::Restricted::newConstraint	(	const Solver &	,
		const Literal *	,
		size_t	,
		con_t
	)		`[inline, virtual]`

Called whenever a new constraint is added to the solver s. The default-implementation is a noop.

Parameters:

s	The solver to which the constraint is added.
first	First literal of the new constraint.
size	Size of the new constraint.
t	Type of the new constraint.

Note:: first points to an array of size size.

Reimplemented from Clasp::DecisionHeuristic.

Definition at line 426 of file lookahead.cpp.

bool Clasp::Restricted::notify ( Solver & s ) [inline, virtual]

Reimplemented from Clasp::UnitHeuristic.

Definition at line 403 of file lookahead.cpp.

void Clasp::Restricted::restoreOther ( Solver & s ) [inline]

Definition at line 399 of file lookahead.cpp.

Literal Clasp::Restricted::selectRange	(	Solver &	,
		const Literal *	first,
		const Literal *
	)		`[inline, virtual]`

Shall select one of the literals in the range [first, last).

Parameters:

s	The solver that needs a new decision variable.
first	Pointer to first literal in range.
last	Pointer to the end of the range.

Precondition:: [first, last) is not empty and all literals in the range are currently unassigned.

Note:: The default implementation returns *first.

Reimplemented from Clasp::DecisionHeuristic.

Definition at line 427 of file lookahead.cpp.

void Clasp::Restricted::simplify	(	const Solver &	,
		size_t
	)		`[inline, virtual]`

Called on decision level 0. Variables that are assigned on this level may be removed from any decision heuristic.

Note:: Whenever the solver returns to dl 0, simplify is only called again if the solver learnt new facts since the last call to simplify.

Parameters:

s	The solver that reached decision level 0.
st	The position in the trail of the first new learnt fact.

Reimplemented from Clasp::DecisionHeuristic.

Definition at line 422 of file lookahead.cpp.

void Clasp::Restricted::startInit ( const Solver & ) [inline, virtual]

Called once after all problem variables are known to the solver. The default-implementation is a noop.

Parameters:

s	The solver in which this heuristic is used.

Reimplemented from Clasp::DecisionHeuristic.

Definition at line 421 of file lookahead.cpp.

void Clasp::Restricted::undoUntil	(	const Solver &	,
		size_t
	)		`[inline, virtual]`

Called whenever the solver backracks. Literals in the range [s.trail()[st], s.trail().size()) are subject to backtracking. The default-implementation is a noop.

Parameters:

s	The solver that is about to backtrack.
st	Position in the trail of the first literal that will be backtracked.

Reimplemented from Clasp::DecisionHeuristic.

Definition at line 423 of file lookahead.cpp.

void Clasp::Restricted::updateReason	(	const Solver &	,
		const LitVec &	,
		Literal
	)		`[inline, virtual]`

Called for each new reason-set that is traversed during conflict analysis. The default-implementation is a noop.

Parameters:

s	The solver in which the conflict is analyzed.
lits	The current reason-set under inspection.
resolveLit	The literal that is currently resolved.

Note:: When a conflict is detected, the solver passes the conflicting literals in lits during the first call to updateReason. On that first call resolveLit is the sentinel-literal.

Reimplemented from Clasp::DecisionHeuristic.

Definition at line 424 of file lookahead.cpp.