Base class for learnt constraints. More...

#include <constraint.h>

Inheritance diagram for Clasp::LearntConstraint:

Public Member Functions
virtual Activity	activity () const
	Returns the activity of the constraint.
virtual void	decreaseActivity ()
	Asks the constraint to decrease its activity.
virtual uint32	isOpen (const Solver &s, const TypeSet &t, LitVec &freeLits)=0
	Shall return 0 if either !t.inSet(type()) or this constraint is satisfied w.r.t the current assignment.
	LearntConstraint ()
virtual bool	locked (const Solver &s) const =0
virtual void	resetActivity (Activity hint)
	Asks the constraint to reset its activity.
ConstraintType	type () const
	Returns the type of this learnt constraint.
Protected Member Functions
	~LearntConstraint ()

Detailed Description

Base class for learnt constraints.

Base class for constraints that can be learnt during search. A learnt constraint is a constraint with the difference that it can be created and deleted dynamically during the search-process and is subject to nogood-deletion. Typical examples are conflict clauses which are created during conflict analysis and loop formulas which are created during unfounded-set checks.

A learnt constraint must additionally define the method locked in order to tell a solver if the constraint can be safely deleted or not. Furthermore whenever a solver needs to delete some learnt constraints it will first delete those with a low activity. A learnt constraint may therefore bump its activity whenever it sees fit in order to delay its deletion.

Definition at line 202 of file constraint.h.

Constructor & Destructor Documentation

Clasp::LearntConstraint::LearntConstraint ( )

Definition at line 37 of file constraint.cpp.

Clasp::LearntConstraint::~LearntConstraint ( ) [protected]

Definition at line 36 of file constraint.cpp.

Member Function Documentation

Activity Clasp::LearntConstraint::activity ( ) const [virtual]

Returns the activity of the constraint.

Note:: A solver uses the activity-value in order to establish an ordering of learnt constraints. Whenever a solver needs to delete some learnt constraints it selects from the unlocked ones those with a low activity-value.; The default-implementation always returns 0.

Reimplemented in Clasp::LoopFormula, and Clasp::ClauseHead.

Definition at line 38 of file constraint.cpp.

void Clasp::LearntConstraint::decreaseActivity ( ) [virtual]

Asks the constraint to decrease its activity.

Reimplemented in Clasp::LoopFormula, and Clasp::ClauseHead.

Definition at line 39 of file constraint.cpp.

virtual uint32 Clasp::LearntConstraint::isOpen	(	const Solver &	s,
		const TypeSet &	t,
		LitVec &	freeLits
	)		`[pure virtual]`

Shall return 0 if either !t.inSet(type()) or this constraint is satisfied w.r.t the current assignment.

If this constraint is currently not satisfied and t.inSet(type()), shall return type() and freeLits shall contain all currently unassigned literals of this constraint.

Implemented in Clasp::mt::SharedLitsClause, Clasp::LoopFormula, Clasp::Clause, and Clasp::Test::TestingConstraint.

virtual bool Clasp::LearntConstraint::locked ( const Solver & s ) const [pure virtual]