Clasp::mt::SharedLitsClause Class Reference

Stores the local part of a shared clause. More...

#include <clause.h>

Inheritance diagram for Clasp::mt::SharedLitsClause:

List of all members.

Public Member Functions
Constraint *	cloneAttach (Solver &other)
	Returns a clone of this and adds necessary watches to the given solver.
void	destroy (Solver *s, bool detach)
	Default is to call delete this.
uint32	isOpen (const Solver &s, const TypeSet &t, LitVec &freeLits)
	Shall return 0 if either !t.inSet(type()) or this constraint is satisfied w.r.t the current assignment.
bool	isReverseReason (const Solver &s, Literal p, uint32 maxL, uint32 maxN)
	Returns true if this clause is a valid "reverse antecedent" for p.
bool	minimize (Solver &s, Literal p, CCMinRecursive *rec)
void	reason (Solver &s, Literal p, LitVec &out)
bool	simplify (Solver &s, bool)
uint32	size () const
	Returns the size of this clause.
void	toLits (LitVec &out) const
	Returns the literals of this clause in out.
Static Public Member Functions
static ClauseHead *	newClause (Solver &s, SharedLiterals *shared_lits, const ClauseInfo &e, const Literal *lits, bool addRef=true)
	Creates a new SharedLitsClause to be used in the given solver.
Private Member Functions
	SharedLitsClause (Solver &s, SharedLiterals *x, const Literal *lits, const ClauseInfo &, bool addRef)
BoolPair	strengthen (Solver &s, Literal p, bool allowToShort)
	Removes p from clause if possible.
bool	updateWatch (Solver &s, uint32 pos)
	Shall replace the watched literal at position pos with a non-false literal.

---

Detailed Description

Stores the local part of a shared clause.

The local part of a shared clause consists of a clause head and and a pointer to the shared literals. Since the local part is owned by a particular solver it can be safely modified. Destroying a SharedLitsClause means destroying the local part and decreasing the shared literals' reference count.

Definition at line 496 of file clause.h.

---

Constructor & Destructor Documentation

Clasp::mt::SharedLitsClause::SharedLitsClause	(	Solver &	s,
		SharedLiterals *	x,
		const Literal *	lits,
		const ClauseInfo &	e,
		bool	addRef
	)		[private]

Definition at line 717 of file clause.cpp.

---

Member Function Documentation

Constraint * Clasp::mt::SharedLitsClause::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 726 of file clause.cpp.

void Clasp::mt::SharedLitsClause::destroy	(	Solver *	s,
		bool	detach
	)		[virtual]

Default is to call delete this.

Reimplemented from Clasp::Constraint.

Definition at line 821 of file clause.cpp.

uint32 Clasp::mt::SharedLitsClause::isOpen	(	const Solver &	s,
		const TypeSet &	t,
		LitVec &	freeLits
	)		[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.

Implements Clasp::LearntConstraint.

Definition at line 832 of file clause.cpp.

bool Clasp::mt::SharedLitsClause::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 773 of file clause.cpp.

bool Clasp::mt::SharedLitsClause::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 765 of file clause.cpp.

ClauseHead * Clasp::mt::SharedLitsClause::newClause	(	Solver &	s,
		SharedLiterals *	shared_lits,
		const ClauseInfo &	e,
		const Literal *	lits,
		bool	addRef = true
	)		[static]

Creates a new SharedLitsClause to be used in the given solver.

Parameters:

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

Definition at line 713 of file clause.cpp.

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

Precondition:

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

Postcondition:

The literals implying p were added to lits.

Implements Clasp::Constraint.

Definition at line 753 of file clause.cpp.

bool Clasp::mt::SharedLitsClause::simplify	(	Solver &	s,
		bool	reinit
	)		[virtual]

Simplify this constraint.

Precondition:

s.decisionLevel() == 0 and the current assignment is fully propagated.

Returns:

true if this constraint can be ignored (e.g. is satisfied), false otherwise.

Postcondition:

If simplify returned true, this constraint has previously removed all its watches from the solver.

Note:

The default implementation is a noop and returns false.

Reimplemented from Clasp::Constraint.

Definition at line 783 of file clause.cpp.

uint32 Clasp::mt::SharedLitsClause::size

(

)

const [virtual]

Returns the size of this clause.

Implements Clasp::ClauseHead.

Definition at line 858 of file clause.cpp.

ClauseHead::BoolPair Clasp::mt::SharedLitsClause::strengthen	(	Solver &	s,
		Literal	p,
		bool	allowToShort
	)		[private, 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 854 of file clause.cpp.

void Clasp::mt::SharedLitsClause::toLits

(

LitVec &

out

)

const [virtual]

Returns the literals of this clause in out.

Implements Clasp::ClauseHead.

Definition at line 850 of file clause.cpp.

bool Clasp::mt::SharedLitsClause::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 730 of file clause.cpp.

---

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

• clause.h
• clause.cpp