Lookahead extends propagation with failed-literal detection. More...

#include <lookahead.h>

Inheritance diagram for Clasp::Lookahead:

Classes
struct	LitNode
struct	Params
Public Types
enum	Type { no_lookahead = 0, atom_lookahead, body_lookahead, hybrid_lookahead }
	Defines the supported lookahead-types. More...
Public Member Functions
void	append (Literal p, bool testBoth)
	Adds literal p to the lookahead list.
void	clear ()
	Clears the lookahead list.
void	destroy (Solver *s, bool detach)
	Default is to call delete this.
bool	empty () const
	Returns true if lookahead list is empty.
Literal	heuristic (Solver &s)
	Returns "best" literal w.r.t scoring of last lookahead or posLit(0) if no such literal exists.
bool	init (Solver &s)
	Called during initialization of s.
	Lookahead (const Params &p)
uint32	priority () const
	Returns PostPropagator::priority_reserved_look.
bool	propagateFixpoint (Solver &s, PostPropagator *)
	Single-step lookahead on all vars in the loookahead list.
void	setLimit (UnitHeuristic *n)
	~Lookahead ()
Static Public Member Functions
static bool	isType (uint32 t)
Public Attributes
ScoreLook	score
	Updates state with lookahead result.
Protected Member Functions
bool	propagateLevel (Solver &s)
bool	test (Solver &s, Literal p)
void	undoLevel (Solver &s)
	Called when the solver undid a decision level watched by this constraint.
Private Types
enum	{ head_id = NodeId(0), undo_id = NodeId(1) }
typedef UnitHeuristic *	HeuPtr
typedef PodVector< LitNode >::type	LookList
typedef uint32	NodeId
typedef PodVector< NodeId >::type	UndoStack
Private Member Functions
bool	checkImps (Solver &s, Literal p)
LitNode *	head ()
const LitNode *	head () const
LitNode *	node (NodeId n)
void	splice (NodeId n)
LitNode *	undo ()
Private Attributes
LitVec	imps_
NodeId	last_
HeuPtr	limit_
LookList	nodes_
NodeId	pos_
UndoStack	saved_
uint32	top_

Detailed Description

Lookahead extends propagation with failed-literal detection.

The class provides different kinds of one-step lookahead. Atom- and body-lookahead are uniform lookahead types, where either only atoms or bodies are tested. Hybrid-lookahead tests both types of vars but each only in a single phase. I.e. atoms are only tested negatively while bodies are tested positively.

Definition at line 138 of file lookahead.h.

Member Typedef Documentation

typedef UnitHeuristic* Clasp::Lookahead::HeuPtr [private]

Definition at line 195 of file lookahead.h.

typedef PodVector<LitNode>::type Clasp::Lookahead::LookList [private]

Definition at line 194 of file lookahead.h.

typedef uint32 Clasp::Lookahead::NodeId [private]

Definition at line 186 of file lookahead.h.

typedef PodVector<NodeId>::type Clasp::Lookahead::UndoStack [private]

Definition at line 193 of file lookahead.h.

Member Enumeration Documentation

anonymous enum [private]

Enumerator:

head_id
undo_id

Definition at line 187 of file lookahead.h.

enum Clasp::Lookahead::Type

Defines the supported lookahead-types.

Enumerator:

no_lookahead	Dummy value
atom_lookahead	Test only atoms in both phases
body_lookahead	Test only bodies in both phases
hybrid_lookahead	Test atoms and bodies but only their preferred decision literal

Definition at line 141 of file lookahead.h.

Constructor & Destructor Documentation

Clasp::Lookahead::Lookahead ( const Params & p ) [explicit]

Parameters:

t	Lookahead-type to use.

Definition at line 68 of file lookahead.cpp.

Clasp::Lookahead::~Lookahead ( )

Definition at line 90 of file lookahead.cpp.

Member Function Documentation

void Clasp::Lookahead::append	(	Literal	p,
		bool	testBoth
	)

Adds literal p to the lookahead list.

Definition at line 147 of file lookahead.cpp.

bool Clasp::Lookahead::checkImps	(	Solver &	s,
		Literal	p
	)		`[private]`

Definition at line 163 of file lookahead.cpp.

void Clasp::Lookahead::clear ( )

Clears the lookahead list.

Definition at line 105 of file lookahead.cpp.

void Clasp::Lookahead::destroy	(	Solver *	s,
		bool	detach
	)		`[virtual]`

Default is to call delete this.

Reimplemented from Clasp::Constraint.

Definition at line 92 of file lookahead.cpp.

bool Clasp::Lookahead::empty ( ) const [inline]

Returns true if lookahead list is empty.

Definition at line 167 of file lookahead.h.

LitNode* Clasp::Lookahead::head ( ) [inline, private]

Definition at line 198 of file lookahead.h.

const LitNode* Clasp::Lookahead::head ( ) const [inline, private]

Definition at line 201 of file lookahead.h.

Literal Clasp::Lookahead::heuristic ( Solver & s )

Returns "best" literal w.r.t scoring of last lookahead or posLit(0) if no such literal exists.

Definition at line 288 of file lookahead.cpp.

bool Clasp::Lookahead::init ( Solver & s ) [virtual]

Called during initialization of s.

Note:: During initialization a post propagator may assign variables but it must not yet propagate them.

Reimplemented from Clasp::PostPropagator.

Definition at line 120 of file lookahead.cpp.

static bool Clasp::Lookahead::isType ( uint32 t ) [inline, static]

Definition at line 156 of file lookahead.h.

LitNode* Clasp::Lookahead::node ( NodeId n ) [inline, private]

Definition at line 197 of file lookahead.h.

uint32 Clasp::Lookahead::priority ( ) const [virtual]

Returns PostPropagator::priority_reserved_look.

Implements Clasp::PostPropagator.

Definition at line 103 of file lookahead.cpp.

bool Clasp::Lookahead::propagateFixpoint	(	Solver &	s,
		PostPropagator *
	)		`[virtual]`

Single-step lookahead on all vars in the loookahead list.

Implements Clasp::PostPropagator.

Definition at line 212 of file lookahead.cpp.

bool Clasp::Lookahead::propagateLevel ( Solver & s ) [protected]

Definition at line 176 of file lookahead.cpp.

void Clasp::Lookahead::setLimit ( UnitHeuristic * n )

Definition at line 338 of file lookahead.cpp.

void Clasp::Lookahead::splice ( NodeId n ) [private]

Definition at line 241 of file lookahead.cpp.

bool Clasp::Lookahead::test	(	Solver &	s,
		Literal	p
	)		`[protected]`

Definition at line 157 of file lookahead.cpp.

LitNode* Clasp::Lookahead::undo ( ) [inline, private]

Definition at line 199 of file lookahead.h.

void Clasp::Lookahead::undoLevel ( Solver & s ) [protected, virtual]

Called when the solver undid a decision level watched by this constraint.

Parameters:

s	the solver in which the decision level is undone.

Reimplemented from Clasp::Constraint.

Definition at line 255 of file lookahead.cpp.

Member Data Documentation

LitVec Clasp::Lookahead::imps_ [private]

Definition at line 204 of file lookahead.h.

NodeId Clasp::Lookahead::last_ [private]

Definition at line 205 of file lookahead.h.

HeuPtr Clasp::Lookahead::limit_ [private]

Definition at line 208 of file lookahead.h.

LookList Clasp::Lookahead::nodes_ [private]

Definition at line 202 of file lookahead.h.

NodeId Clasp::Lookahead::pos_ [private]

Definition at line 206 of file lookahead.h.

UndoStack Clasp::Lookahead::saved_ [private]

Definition at line 203 of file lookahead.h.

ScoreLook Clasp::Lookahead::score

Updates state with lookahead result.

Definition at line 176 of file lookahead.h.

uint32 Clasp::Lookahead::top_ [private]

Definition at line 207 of file lookahead.h.

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

Classes

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Member Functions

Private Types