Inheritance diagram for Clasp::ModelEnumerator::BacktrackFinder:

Public Member Functions
	BacktrackFinder (Solver &s, MinimizeConstraint min, VarVec project, uint32 projOpts)
Constraint *	cloneAttach (Solver &s)
	Returns a clone of this and adds necessary watches to the given solver.
void	doCommitModel (Enumerator &ctx, Solver &s)
bool	doUpdate (Solver &s)
bool	hasModel () const
PropResult	propagate (Solver &, Literal, uint32 &)
void	reason (Solver &s, Literal p, LitVec &x)
Public Attributes
uint32	opts
LitVec	solution

Detailed Description

Definition at line 138 of file model_enumerators.cpp.

Constructor & Destructor Documentation

Clasp::ModelEnumerator::BacktrackFinder::BacktrackFinder	(	Solver &	s,
		MinimizeConstraint *	min,
		VarVec *	project,
		uint32	projOpts
	)		`[inline]`

Definition at line 140 of file model_enumerators.cpp.

Member Function Documentation

Constraint* Clasp::ModelEnumerator::BacktrackFinder::cloneAttach ( Solver & other ) [inline, virtual]

Returns a clone of this and adds necessary watches to the given solver.

The function shall create and return a copy of this constraint to be used in the given solver. Furthermore, it shall add necessary watches to the given solver.

Note:: Return 0 to indicate that cloning is not supported.

Implements Clasp::Constraint.

Definition at line 147 of file model_enumerators.cpp.

void Clasp::ModelEnumerator::BacktrackFinder::doCommitModel	(	Enumerator &	ctx,
		Solver &	s
	)		`[virtual]`

Reimplemented from Clasp::EnumerationConstraint.

Definition at line 210 of file model_enumerators.cpp.

bool Clasp::ModelEnumerator::BacktrackFinder::doUpdate ( Solver & s ) [virtual]

Implements Clasp::EnumerationConstraint.

Definition at line 170 of file model_enumerators.cpp.

bool Clasp::ModelEnumerator::BacktrackFinder::hasModel ( ) const [inline]

Definition at line 141 of file model_enumerators.cpp.

Constraint::PropResult Clasp::ModelEnumerator::BacktrackFinder::propagate	(	Solver &	s,
		Literal	p,
		uint32 &	data
	)		`[virtual]`

Propagate is called for each constraint that watches p. It shall enqueue all consequences of p becoming true.

Precondition:: p is true in s

Parameters:

s	The solver in which p became true.
p	A literal watched by this constraint that recently became true.
data	The data-blob that this constraint passed when the watch for p was registered.

Reimplemented from Clasp::EnumerationConstraint.

Definition at line 158 of file model_enumerators.cpp.