BranchingHeuristic Class Reference

Branching heurstic for a quantified space. Branching heuristic using a score attribuer to give the next variable. This branching heuristic keeps trace of the variables on which we have branched, and so requires a backtrack signal (send by the solver using its backtrack method). The next variable musi be (and is) chosen respect to the variables partial order in the prefix. Heaps are used to provide the next variable in logarithmic time. Variables declared as subsumed are ignored by the branching heuristic. More...

#include <qecore.hh>

Collaboration diagram for BranchingHeuristic:

[legend]List of all members.


Public Member Functions
void	updateVar (int pos, QSpace *qs)
	BranchingHeuristic (QSpace qs, ScoreAttribuer ev)
	Constructor for a branching heuristic. constructor for a branching heuristic on a quantified space, using a score attribuer.
int	nextVar (QSpace *qs)
void	backtrack (QSpace *qs)
void	vartouched (int pos, QSpace *qs)
Private Attributes
int	size
int	blocks
int *	bloc
stackint	treated
cheap *	heaps
stackint	touched
int *	score
int	curHeap
ScoreAttribuer *	eval

Detailed Description

Definition at line 157 of file qecore.hh.

Constructor & Destructor Documentation

BranchingHeuristic::BranchingHeuristic	(	QSpace *	qs,
		ScoreAttribuer *	ev
	)

Constructor for a branching heuristic. constructor for a branching heuristic on a quantified space, using a score attribuer.

Parameters:

	qs	The quantified space the branching heuristic is for.
	ev	the score attribuer this branching heuristic will use to determine the next variable

Definition at line 41 of file qecore.cc.

References bloc, blocks, curHeap, eval, heaps, Heap< C >::insert(), MARKER, QSpace::nv(), QSpace::quantification(), ScoreAttribuer::score(), score, Heap< C >::setBounds(), size, touched, and treated.

Member Function Documentation

void BranchingHeuristic::updateVar	(	int	pos,
		QSpace *	qs
	)

Definition at line 108 of file qecore.cc.

References bloc, Heap< C >::decrease(), eval, heaps, Heap< C >::increase(), score, and ScoreAttribuer::score().

Referenced by backtrack(), and vartouched().

int BranchingHeuristic::nextVar ( QSpace * qs )

Returns the next variable to branch on.

Parameters:

The current quantified space on which we are searching (must be a clone, possibly cloned, propagated and assigned multiple times of the quantified space given at the construction.)

Definition at line 85 of file qecore.cc.

References blocks, curHeap, Heap< C >::getmin(), Heap< C >::getminwopop(), heaps, MARKER, QSpace::subsumed(), touched, and treated.

Referenced by QSolver::rSolve().

void BranchingHeuristic::backtrack ( QSpace * qs )

Used by the solver to indicate it backtracked.

Parameters:

The current quantified space on which we are searching, i.e. the one on which the solver just backtracked (must be a clone, possibly cloned, propagated and assigned multiple times of the quantified space given at the construction).

Definition at line 128 of file qecore.cc.

References bloc, curHeap, heaps, Heap< C >::insert(), MARKER, touched, treated, and updateVar().

Referenced by QSolver::rSolve().

void BranchingHeuristic::vartouched	(	int	pos,
		QSpace *	qs
	)

Used by the solver to indicate that a variable has been touched, and so thai its scors have possibly changed.

Parameters:

The current quantified space on which we are searching (must be a clone, possibly cloned, propagated and assigned multiple times of the quantified space given at the construction).

Definition at line 123 of file qecore.cc.

References touched, and updateVar().

Referenced by Warner::warn().