Class for representing a clause in a solver. More...

#include <clause.h>

Inheritance diagram for Clasp::Clause:

Public Types
enum	{ MAX_SHORT_LEN = 5 }
typedef Constraint::PropResult	PropResult
Public Member Functions
Constraint *	cloneAttach (Solver &other)
	Returns a clone of this and adds necessary watches to the given solver.
uint32	computeAllocSize () const
bool	contracted () const
void	destroy (Solver *s=0, bool detach=false)
	Destroys the clause and frees its memory.
void	detach (Solver &)
	Removes watches from s.
uint32	isOpen (const Solver &s, const TypeSet &t, LitVec &freeLits)
	Returns type() if the clause is currently not satisfied and t.inSet(type()).
bool	isReverseReason (const Solver &s, Literal p, uint32 maxL, uint32 maxN)
	Returns true if this clause is a valid "reverse antecedent" for p.
bool	isSmall () const
bool	minimize (Solver &m, Literal p, CCMinRecursive *r)
void	reason (Solver &s, Literal p, LitVec &lits)
bool	simplify (Solver &s, bool=false)
	Returns true if clause is SAT.
uint32	size () const
	Returns the size of this clause.
BoolPair	strengthen (Solver &s, Literal p, bool allowToShort)
	Removes p from clause if possible.
bool	strengthened () const
void	toLits (LitVec &out) const
	Returns the literals of this clause in out.
Static Public Member Functions
static void *	alloc (Solver &s, uint32 mLits, bool learnt)
	Allocates memory for storing a (learnt) clause with nLits literals.
static ClauseHead *	newClause (Solver &s, const ClauseRep &rep)
	Creates a new clause from the clause given in rep.
static ClauseHead *	newClause (void *mem, Solver &s, const ClauseRep &rep)
	Creates a new clause object in mem.
static ClauseHead *	newContractedClause (Solver &s, const ClauseRep &rep, uint32 tailPos, bool extend)
	Creates a new contracted clause from the clause given in rep.
static ClauseHead *	newShared (Solver &s, SharedLiterals *lits, const ClauseInfo &e, const Literal head[3], bool addRef=true)
	Creates a new local surrogate for shared_lits to be used in the given solver.
Private Types
typedef std::pair< Literal , Literal >	LitRange
Private Member Functions
	Clause (Solver &s, const ClauseRep &rep, uint32 tail=UINT32_MAX, bool extend=false)
	Clause (Solver &s, const Clause &other)
Literal *	longEnd ()
Literal *	removeFromTail (Solver &s, Literal it, Literal end)
LitRange	tail ()
void	undoLevel (Solver &s)
	Called when the solver undid a decision level watched by this constraint.
bool	updateWatch (Solver &s, uint32 pos)
	Shall replace the watched literal at position pos with a non-false literal.

Detailed Description

Class for representing a clause in a solver.

Definition at line 291 of file clause.h.

Member Typedef Documentation

typedef std::pair<Literal*, Literal*> Clasp::Clause::LitRange [private]

Definition at line 382 of file clause.h.

typedef Constraint::PropResult Clasp::Clause::PropResult

Definition at line 293 of file clause.h.

Member Enumeration Documentation

anonymous enum

Enumerator:

MAX_SHORT_LEN

Definition at line 294 of file clause.h.

Constructor & Destructor Documentation

Clasp::Clause::Clause	(	Solver &	s,
		const ClauseRep &	rep,
		uint32	tail = `UINT32_MAX`,
		bool	extend = `false`
	)		`[private]`

Definition at line 386 of file clause.cpp.

Clasp::Clause::Clause	(	Solver &	s,
		const Clause &	other
	)		`[private]`

Definition at line 415 of file clause.cpp.

Member Function Documentation

void * Clasp::Clause::alloc	(	Solver &	s,
		uint32	mLits,
		bool	learnt
	)		`[static]`

Allocates memory for storing a (learnt) clause with nLits literals.

Definition at line 360 of file clause.cpp.

Constraint * Clasp::Clause::cloneAttach ( Solver & other ) [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 428 of file clause.cpp.

uint32 Clasp::Clause::computeAllocSize ( ) const

Definition at line 455 of file clause.cpp.

bool Clasp::Clause::contracted ( ) const [inline]

Definition at line 375 of file clause.h.

void Clasp::Clause::destroy	(	Solver *	s = `0`,
		bool	detach = `false`
	)		`[virtual]`

Destroys the clause and frees its memory.

Reimplemented from Clasp::Constraint.

Definition at line 433 of file clause.cpp.

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

Removes watches from s.

Reimplemented from Clasp::ClauseHead.

Definition at line 445 of file clause.cpp.

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

Returns type() if the clause is currently not satisfied and t.inSet(type()).

Implements Clasp::LearntConstraint.

Definition at line 584 of file clause.cpp.

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

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

Implements Clasp::ClauseHead.

Definition at line 527 of file clause.cpp.

bool Clasp::Clause::isSmall ( ) const [inline]

Definition at line 376 of file clause.h.

Literal* Clasp::Clause::longEnd ( ) [inline, private]

Definition at line 386 of file clause.h.

bool Clasp::Clause::minimize	(	Solver &	s,
		Literal	p,
		CCMinRecursive *	rec
	)		`[virtual]`

Called during minimization of learnt clauses.

Precondition:: This constraint is the reason for p being true in s.

Returns:: true if p can be removed from the current learnt clause, false otherwise.

Note:

The default implementation uses the following inefficient algorithm

   LitVec temp;
   reason(s, p, temp);
   for each x in temp 
     if (!s.ccMinimize(p, rec)) return false;
   return true;

Reimplemented from Clasp::Constraint.

Definition at line 511 of file clause.cpp.

static ClauseHead* Clasp::Clause::newClause	(	Solver &	s,
		const ClauseRep &	rep
	)		`[inline, static]`

Creates a new clause from the clause given in rep.

Parameters:

s	Solver in which the new clause is to be used.
rep	The raw representation of the clause.

Precondition:: The clause given in lits is prepared and contains at least two literals.

Note:: The clause must be destroyed using Clause::destroy.

See also:: ClauseCreator::prepare()

Definition at line 308 of file clause.h.

ClauseHead * Clasp::Clause::newClause	(	void *	mem,
		Solver &	s,
		const ClauseRep &	rep
	)		`[static]`

Creates a new clause object in mem.

Precondition:: mem points to a memory block that was allocated via Clause::alloc().

Definition at line 371 of file clause.cpp.

ClauseHead * Clasp::Clause::newContractedClause	(	Solver &	s,
		const ClauseRep &	rep,
		uint32	tailPos,
		bool	extend
	)		`[static]`

Creates a new contracted clause from the clause given in rep.

A contracted clause consists of an active head and a tail of false literals. Propagation is restricted to the head. The tail is only needed to compute reasons from assignments.

Parameters:

s	Solver in which the new clause is to be used.
rep	The raw representation of the clause.
tail	The starting index of the tail (first literal that should be temporarily removed from the clause).
exten	Extend head part of clause as tail literals become free?

Definition at line 380 of file clause.cpp.

ClauseHead * Clasp::Clause::newShared	(	Solver &	s,
		SharedLiterals *	lits,
		const ClauseInfo &	e,
		const Literal	head[3],
		bool	addRef = `true`
	)		`[static]`

Creates a new local surrogate for shared_lits to be used in the given solver.

Parameters:

s	The solver in which this clause will be used.
lits	The shared literals of this clause.
e	Initial data for the new (local) clause.
head	Watches and cache literal for the new (local) clause.
addRef	Increment ref count of lits.

Definition at line 376 of file clause.cpp.

void Clasp::Clause::reason	(	Solver &	s,
		Literal	p,
		LitVec &	lits
	)		`[virtual]`

For a clause [x y p] the reason for p is ~x and ~y.

Precondition:: *this previously asserted p

Note:: if the clause is a learnt clause, calling reason increases the clause's activity.

Implements Clasp::Constraint.

Definition at line 491 of file clause.cpp.

Literal * Clasp::Clause::removeFromTail	(	Solver &	s,
		Literal *	it,
		Literal *	end
	)		`[private]`

Definition at line 674 of file clause.cpp.

bool Clasp::Clause::simplify	(	Solver &	s,
		bool	reinit = `false`
	)		`[virtual]`

Returns true if clause is SAT.

Removes from the clause all literals that are false.

Reimplemented from Clasp::Constraint.

Definition at line 543 of file clause.cpp.

uint32 Clasp::Clause::size ( ) const [virtual]

Returns the size of this clause.

Implements Clasp::ClauseHead.

Definition at line 703 of file clause.cpp.

ClauseHead::BoolPair Clasp::Clause::strengthen	(	Solver &	s,
		Literal	p,
		bool	allowToShort
	)		`[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).

Implements Clasp::ClauseHead.

Definition at line 632 of file clause.cpp.

bool Clasp::Clause::strengthened ( ) const [inline]

Definition at line 377 of file clause.h.

LitRange Clasp::Clause::tail ( ) [inline, private]

Definition at line 387 of file clause.h.

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

Returns the literals of this clause in out.

Implements Clasp::ClauseHead.

Definition at line 625 of file clause.cpp.

void Clasp::Clause::undoLevel ( Solver & s ) [private, 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 606 of file clause.cpp.

bool Clasp::Clause::updateWatch	(	Solver &	s,
		uint32	pos
	)		`[private, virtual]`

Shall replace the watched literal at position pos with a non-false literal.

Precondition:: pos in [0,1]; s.isFalse(head_[pos]) && s.isFalse(head_[2]); head_[pos^1] is the other watched literal

Implements Clasp::ClauseHead.

Definition at line 468 of file clause.cpp.

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

Public Types

Public Member Functions

Static Public Member Functions

Private Types

Private Member Functions

Detailed Description

Member Typedef Documentation

Member Enumeration Documentation

Constructor & Destructor Documentation

Member Function Documentation