(Abstract) base class for clause types. More...

#include <solver_types.h>

Inheritance diagram for Clasp::ClauseHead:

Classes
union	Data
union	Info
Public Types
enum	{ HEAD_LITS = 3, MAX_SHORT_LEN = 5, MAX_LBD = (1<<5)-1, TAGGED_CLAUSE = 1023, MAX_ACTIVITY = (1<<15)-1 }
typedef std::pair< bool, bool >	BoolPair
Public Member Functions
Activity	activity () const
	Returns the activity of this clause.
void	attach (Solver &s)
	Adds watches for first two literals in head to solver.
void	bumpActivity ()
	Increases activity.
ClauseHead *	clause ()
	Downcast from LearntConstraint.
	ClauseHead (const ClauseInfo &init)
void	decreaseActivity ()
	Halves the activity of this clause.
virtual void	detach (Solver &s)
	Removes watches from s.
virtual bool	isReverseReason (const Solver &s, Literal p, uint32 maxL, uint32 maxN)=0
	Returns true if this clause is a valid "reverse antecedent" for p.
uint32	lbd () const
void	lbd (uint32 x)
bool	learnt () const
bool	locked (const Solver &s) const
	True if this clause currently is the antecedent of an assignment.
PropResult	propagate (Solver &s, Literal, uint32 &data)
	Propagates the head and calls updateWatch() if necessary.
void	resetActivity (Activity a)
	Asks the constraint to reset its activity.
bool	satisfied (const Solver &s)
	Returns true if head is satisfied w.r.t current assignment in s.
virtual uint32	size () const =0
	Returns the size of this clause.
virtual BoolPair	strengthen (Solver &s, Literal p, bool allowToShort=true)=0
	Removes p from clause if possible.
bool	tagged () const
	Conditional clause?
virtual void	toLits (LitVec &out) const =0
	Returns the literals of this clause in out.
ConstraintType	type () const
	Type of clause.
Protected Member Functions
void	clearTagged ()
bool	hasLbd () const
void	setLbd (uint32 x)
bool	toImplication (Solver &s)
virtual bool	updateWatch (Solver &s, uint32 pos)=0
	Shall replace the watched literal at position pos with a non-false literal.
Protected Attributes
union Clasp::ClauseHead::Data	data_
Literal	head_ [HEAD_LITS]
union Clasp::ClauseHead::Info	info_
Friends
struct	ClauseWatch

Detailed Description

(Abstract) base class for clause types.

ClauseHead is used to enforce a common memory-layout for all clauses. It contains the two watched literals and a cache literal to improve propagation performance. A virtual call to Constraint::propagate() is only needed if the other watch is not true and the cache literal is false.

Definition at line 407 of file solver_types.h.

Member Typedef Documentation

typedef std::pair<bool, bool> Clasp::ClauseHead::BoolPair

Definition at line 427 of file solver_types.h.

Member Enumeration Documentation

anonymous enum

Enumerator:

HEAD_LITS
MAX_SHORT_LEN
MAX_LBD
TAGGED_CLAUSE
MAX_ACTIVITY

Definition at line 409 of file solver_types.h.

Constructor & Destructor Documentation

Clasp::ClauseHead::ClauseHead ( const ClauseInfo & init ) [explicit]

Definition at line 88 of file solver_types.cpp.

Member Function Documentation

Activity Clasp::ClauseHead::activity ( ) const [inline, virtual]

Returns the activity of this clause.

Reimplemented from Clasp::LearntConstraint.

Definition at line 419 of file solver_types.h.

void Clasp::ClauseHead::attach ( Solver & s )

Adds watches for first two literals in head to solver.

Definition at line 93 of file solver_types.cpp.

void Clasp::ClauseHead::bumpActivity ( ) [inline]

Increases activity.

Definition at line 429 of file solver_types.h.

ClauseHead* Clasp::ClauseHead::clause ( ) [inline, virtual]

Downcast from LearntConstraint.

Reimplemented from Clasp::Constraint.

Definition at line 424 of file solver_types.h.

void Clasp::ClauseHead::clearTagged ( ) [inline, protected]

Definition at line 459 of file solver_types.h.

void Clasp::ClauseHead::decreaseActivity ( ) [inline, virtual]

Halves the activity of this clause.

Reimplemented from Clasp::LearntConstraint.

Definition at line 421 of file solver_types.h.

void Clasp::ClauseHead::detach ( Solver & s ) [virtual]

Removes watches from s.

Reimplemented in Clasp::Clause.

Definition at line 99 of file solver_types.cpp.

bool Clasp::ClauseHead::hasLbd ( ) const [inline, protected]

Definition at line 461 of file solver_types.h.

virtual bool Clasp::ClauseHead::isReverseReason	(	const Solver &	s,
		Literal	p,
		uint32	maxL,
		uint32	maxN
	)		`[pure virtual]`

Returns true if this clause is a valid "reverse antecedent" for p.

Implemented in Clasp::mt::SharedLitsClause, and Clasp::Clause.

uint32 Clasp::ClauseHead::lbd ( ) const [inline]

Definition at line 437 of file solver_types.h.

void Clasp::ClauseHead::lbd ( uint32 x ) [inline]

Definition at line 438 of file solver_types.h.

bool Clasp::ClauseHead::learnt ( ) const [inline]

Definition at line 436 of file solver_types.h.

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

True if this clause currently is the antecedent of an assignment.

Implements Clasp::LearntConstraint.

Definition at line 104 of file solver_types.cpp.

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

Propagates the head and calls updateWatch() if necessary.

Implements Clasp::Constraint.

Definition at line 672 of file solver.cpp.

void Clasp::ClauseHead::resetActivity ( Activity hint ) [inline, virtual]

Asks the constraint to reset its activity.

Reimplemented from Clasp::LearntConstraint.

Definition at line 422 of file solver_types.h.

bool Clasp::ClauseHead::satisfied ( const Solver & s )

Returns true if head is satisfied w.r.t current assignment in s.

Definition at line 109 of file solver_types.cpp.

void Clasp::ClauseHead::setLbd ( uint32 x ) [inline, protected]

Definition at line 460 of file solver_types.h.

virtual uint32 Clasp::ClauseHead::size ( ) const [pure virtual]

Returns the size of this clause.

Implemented in Clasp::mt::SharedLitsClause, and Clasp::Clause.

virtual BoolPair Clasp::ClauseHead::strengthen	(	Solver &	s,
		Literal	p,
		bool	allowToShort = `true`
	)		`[pure virtual]`

Removes p from clause if possible.

Returns:: The first component of the returned pair specifies whether or not p was removed from the clause. The second component of the returned pair specifies whether the clause should be kept (false) or removed (true).

Implemented in Clasp::mt::SharedLitsClause, and Clasp::Clause.

bool Clasp::ClauseHead::tagged ( ) const [inline]

Conditional clause?

Definition at line 435 of file solver_types.h.

bool Clasp::ClauseHead::toImplication ( Solver & s ) [protected]

Definition at line 113 of file solver_types.cpp.

virtual void Clasp::ClauseHead::toLits ( LitVec & out ) const [pure virtual]

Returns the literals of this clause in out.

Implemented in Clasp::mt::SharedLitsClause, and Clasp::Clause.

ConstraintType Clasp::ClauseHead::type ( ) const [inline, virtual]

Type of clause.

Reimplemented from Clasp::LearntConstraint.