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

#include <clause.h>

Inheritance diagram for Clasp::mt::SharedLitsClause:

Collaboration diagram for Clasp::mt::SharedLitsClause:

Public Member Functions
Constraint *	cloneAttach (Solver &other)
	Returns a clone of this and adds necessary watches to the given solver. More...

void	reason (Solver &s, Literal p, LitVec &out)

bool	minimize (Solver &s, Literal p, CCMinRecursive *rec)

bool	isReverseReason (const Solver &s, Literal p, uint32 maxL, uint32 maxN)
	Returns true if this clause is a valid "reverse antecedent" for p. More...

bool	simplify (Solver &s, bool)

void	destroy (Solver *s, bool detach)
	Default is to call delete this. More...

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. More...

uint32	size () const
	Returns the size of this clause. More...

void	toLits (LitVec &out) const
	Returns the literals of this clause in out. More...

Public Member Functions inherited from Clasp::ClauseHead
	ClauseHead (const ClauseInfo &init)

PropResult	propagate (Solver &s, Literal, uint32 &data)
	Propagates the head and calls updateWatch() if necessary. More...

ConstraintType	type () const
	Type of clause. More...

bool	locked (const Solver &s) const
	True if this clause currently is the antecedent of an assignment. More...

Activity	activity () const
	Returns the activity of this clause. More...

void	decreaseActivity ()
	Halves the activity of this clause. More...

void	resetActivity (Activity a)
	Asks the constraint to reset its activity. More...

ClauseHead *	clause ()
	Downcast from LearntConstraint. More...

void	bumpActivity ()
	Increases activity. More...

void	attach (Solver &s)
	Adds watches for first two literals in head to solver. More...

bool	satisfied (const Solver &s)
	Returns true if head is satisfied w.r.t current assignment in s. More...

bool	tagged () const
	Conditional clause? More...

bool	learnt () const

uint32	lbd () const

void	lbd (uint32 x)

virtual void	detach (Solver &s)
	Removes watches from s. More...

Public Member Functions inherited from Clasp::LearntConstraint
	LearntConstraint ()

Public Member Functions inherited from Clasp::Constraint
	Constraint ()

virtual void	undoLevel (Solver &s)
	Called when the solver undid a decision level watched by this constraint. More...

virtual uint32	estimateComplexity (const Solver &s) const
	Returns an estimate of the constraint's complexity relative to a clause (complexity = 1). More...

virtual bool	valid (Solver &s)
	Shall return whether the constraint is valid (i.e. not conflicting) w.r.t the current assignment in s. More...

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. More...

Additional Inherited Members
Public Types inherited from Clasp::ClauseHead
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

Protected Member Functions inherited from Clasp::ClauseHead
bool	toImplication (Solver &s)

void	clearTagged ()

void	setLbd (uint32 x)

bool	hasLbd () const

Protected Member Functions inherited from Clasp::LearntConstraint
	~LearntConstraint ()

Protected Member Functions inherited from Clasp::Constraint
virtual	~Constraint ()

Protected Attributes inherited from Clasp::ClauseHead
union Clasp::ClauseHead::Data	data_

union Clasp::ClauseHead::Info	info_

Literal	head_ [HEAD_LITS]

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.

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.

Here is the call graph for this function:

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

virtual

Default is to call delete this.

Reimplemented from Clasp::Constraint.

Here is the call graph for this function:

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.

Here is the call graph for this function:

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.

Here is the call graph for this function:

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.

Here is the call graph for this function:

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.

Here is the call graph for this function:

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.

Here is the call graph for this function:

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.

Here is the call graph for this function:

uint32 Clasp::mt::SharedLitsClause::size ( ) const

virtual

Returns the size of this clause.

Implements Clasp::ClauseHead.

Here is the call graph for this function:

void Clasp::mt::SharedLitsClause::toLits ( LitVec & out ) const

virtual

Returns the literals of this clause in out.

Implements Clasp::ClauseHead.

Here is the call graph for this function:

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

/Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/clasp/clause.h
/Users/danielbaeck/Dropbox/Uni Klagenfurt/Diplomarbeit/gringo44/libclasp/src/clause.cpp

Public Member Functions

Static Public Member Functions

Additional Inherited Members

Detailed Description

Member Function Documentation