A helper-class for creating/adding clauses. More...

#include <clause.h>

Classes
struct	Result
	A type for storing the result of a clause insertion operation. More...
Public Types
enum	Status { status_open = 0, status_sat = 1, status_unsat = 2, status_unit = 4, status_sat_asserting = 5, status_asserting = 6, status_subsumed = 9, status_empty = 10 }
	Status of a clause. More...
Public Member Functions
ClauseCreator &	add (const Literal &p)
	Adds the literal p to the clause under construction.
void	addDefaultFlags (uint32 f)
	Adds additional flags to be applied in end().
	ClauseCreator (Solver *s=0)
	Creates a new ClauseCreator object.
void	clear ()
	Discards the current clause.
Result	end (uint32 flags=clause_not_sat\|clause_not_conflict)
	Creates a new clause object for the clause under construction.
ClauseInfo	info () const
	Returns the aux info of the clause under construction.
const LitVec &	lits () const
	Returns the literals of the clause under construction.
LitVec &	lits ()
Literal &	operator[] (uint32 i)
	Returns the literal at the given idx.
Literal	operator[] (uint32 i) const
ClauseRep	prepare (bool fullSimplify)
	Removes subsumed lits and orders first lits w.r.t watch order.
void	reserve (LitVec::size_type s)
	Reserve space for a clause of size s.
ClauseCreator &	setActivity (uint32 a)
	Sets the initial activity of the clause under construction.
ClauseCreator &	setLbd (uint32 lbd)
	Sets the initial literal block distance of the clause under construction.
void	setSolver (Solver &s)
	Sets the solver in which created clauses are stored.
uint32	size () const
	Returns the current size of the clause under construction.
ClauseCreator &	start (ConstraintType t=Constraint_t::static_constraint)
	Starts the creation of a new clause.
ConstraintType	type () const
	Returns the clause's type.
Static Private Member Functions
static Result	create_prepared (Solver &s, const ClauseRep &pc, uint32 flags)
static bool	ignoreClause (const Solver &s, const ClauseRep &cl, Status st, uint32 modeFlags)
static ClauseHead *	newLearntClause (Solver &s, const ClauseRep &clause, uint32 flags)
static ClauseHead *	newProblemClause (Solver &s, const ClauseRep &clause, uint32 flags)
static ClauseHead *	newUnshared (Solver &s, SharedLiterals clause, const Literal w, const ClauseInfo &e)
static ClauseRep	prepare (Solver &s, const Literal in, uint32 inSize, const ClauseInfo &e, uint32 flags, Literal out, uint32 outMax=UINT32_MAX)
Private Attributes
ClauseInfo	extra_
uint32	flags_
LitVec	literals_
Solver *	solver_
factory functions
Functions for creating and integrating clauses
enum	CreateFlag { clause_no_add = 1, clause_explicit = 2, clause_not_sat = 4, clause_not_root_sat = 8, clause_not_conflict = 16, clause_no_release = 32, clause_int_lbd = 64, clause_no_prepare = 128, clause_force_simplify = 256, clause_no_heuristic = 512 }
	Flags controlling clause creation and integration. More...
static Status	status (const Solver &s, const Literal clause_begin, const Literal clause_end)
	Returns the status of the given clause w.r.t s.
static Status	status (const Solver &s, const ClauseRep &c)
static uint32	watchOrder (const Solver &s, Literal p)
	Returns an abstraction of p's decision level that can be used to order literals.
static ClauseRep	prepare (Solver &s, LitVec &lits, uint32 flags, const ClauseInfo &info=ClauseInfo())
	Prepares the clause given in lits.
static Result	create (Solver &s, LitVec &lits, uint32 flags, const ClauseInfo &info=ClauseInfo())
	Creates a clause from the literals given in lits.
static Result	create (Solver &s, const ClauseRep &rep, uint32 flags)
static Result	integrate (Solver &s, SharedLiterals *clause, uint32 flags, ConstraintType t)
	Integrates the given clause into the current search of s.
static Result	integrate (Solver &s, SharedLiterals *clause, uint32 flags)

Detailed Description

A helper-class for creating/adding clauses.

This class simplifies clause creation. It hides the special handling of short, and shared clauses. It also makes sure that learnt clauses watch the literals from the highest decision levels.

Definition at line 82 of file clause.h.

Member Enumeration Documentation

enum Clasp::ClauseCreator::CreateFlag

Flags controlling clause creation and integration.

Enumerator:

clause_no_add	Do not add clause to solver db.
clause_explicit	Force creation of explicit clause even if size <= 3.
clause_not_sat	Do not add clause if it is satisfied (but not asserting) w.r.t current assignment.
clause_not_root_sat	Do not add clause if it is satisfied w.r.t the root assignment.
clause_not_conflict	Do not add clause if it is conflicting w.r.t the current assignment.
clause_no_release	Do not call release on shared literals.
clause_int_lbd	Compute lbd when integrating asserting clauses.
clause_no_prepare	Assume clause is already ordered w.r.t watches.
clause_force_simplify	Call simplify() on create.
clause_no_heuristic	Do not notify heuristic about new clause.

Definition at line 168 of file clause.h.

enum Clasp::ClauseCreator::Status

Status of a clause.

For a clause with literals [l1,...,ln], status is one of:

Enumerator:

status_open	Clause is neither sat, unsat, or unit.
status_sat	At least one literal is true.
status_unsat	All literals are false.
status_unit	All but one literal false.
status_sat_asserting	Sat but literal is implied on lower dl.
status_asserting	Unsat but literal is implied on second highest dl.
status_subsumed	Sat and one literal is true on level 0.
status_empty	Unsat and all literals are false on level 0.

Definition at line 102 of file clause.h.

Constructor & Destructor Documentation

Clasp::ClauseCreator::ClauseCreator ( Solver * s = 0 ) [explicit]

Creates a new ClauseCreator object.

Parameters:

s	the Solver in which to store created clauses.

Definition at line 103 of file clause.cpp.

Member Function Documentation

ClauseCreator& Clasp::ClauseCreator::add ( const Literal & p ) [inline]

Adds the literal p to the clause under construction.

Definition at line 137 of file clause.h.

void Clasp::ClauseCreator::addDefaultFlags ( uint32 f ) [inline]

Adds additional flags to be applied in end().

Definition at line 92 of file clause.h.

void Clasp::ClauseCreator::clear ( ) [inline]

Discards the current clause.

Definition at line 96 of file clause.h.

ClauseCreator::Result Clasp::ClauseCreator::create	(	Solver &	s,
		LitVec &	lits,
		uint32	flags,
		const ClauseInfo &	info = `ClauseInfo()`
	)		`[static]`

Creates a clause from the literals given in lits.

Parameters:

s	The solver to which the clause should be added.
lits	The literals of the clause.
flags	Flag set controlling creation (see CreateFlag).
info	Initial information (e.g. type) for the new clause.

Precondition:: !s.hasConflict() and s.decisionLevel() == 0 or extra.learnt(); lits is fully prepared or flags contains suitable prepare flags.

Note:: If the given clause is unit (or asserting), the unit-resulting literal is asserted on the (numerical) lowest level possible but the new information is not immediately propagated, i.e. on return queueSize() may be greater than 0.; The local representation of the clause is always attached to the solver but only added to the solver if clause_no_add is not contained in flags. Otherwise, the returned clause is owned by the caller and it is the caller's responsibility to manage it. Furthermore, learnt statistics are *not* updated automatically in that case.

See also:: prepare()

Definition at line 306 of file clause.cpp.

ClauseCreator::Result Clasp::ClauseCreator::create	(	Solver &	s,
		const ClauseRep &	rep,
		uint32	flags
	)		`[static]`

Definition at line 310 of file clause.cpp.

ClauseCreator::Result Clasp::ClauseCreator::create_prepared	(	Solver &	s,
		const ClauseRep &	pc,
		uint32	flags
	)		`[static, private]`

Definition at line 276 of file clause.cpp.

ClauseCreator::Result Clasp::ClauseCreator::end ( uint32 flags = clause_not_sat | clause_not_conflict )

Creates a new clause object for the clause under construction.

Precondition:: The clause does not contain duplicate/complementary literals or flags contains clause_force_simplify.

Note:: If the clause to be added is empty, end() fails and s.hasConflict() is set to true.

See also:: Result ClauseCreator::create(Solver& s, LitVec& lits, uint32 flags, const ClauseInfo& info);

Definition at line 202 of file clause.cpp.

bool Clasp::ClauseCreator::ignoreClause	(	const Solver &	s,
		const ClauseRep &	cl,
		Status	st,
		uint32	modeFlags
	)		`[static, private]`

Definition at line 195 of file clause.cpp.

ClauseInfo Clasp::ClauseCreator::info ( ) const [inline]

Returns the aux info of the clause under construction.

Definition at line 151 of file clause.h.

ClauseCreator::Result Clasp::ClauseCreator::integrate	(	Solver &	s,
		SharedLiterals *	clause,
		uint32	flags,
		ConstraintType	t
	)		`[static]`

Integrates the given clause into the current search of s.

Precondition:: the assignment in s is not conflicting

Parameters:

s	The solver in which the clause should be integrated.
clause	The clause to be integrated.
flags	A set of flags controlling integration (see CreateFlag).
t	Constraint type to use for the local representation.

Note:

The function behaves similar to ClauseCreator::create() with the exception that it does not add local representations for implicit clauses (i.e. size <= 3) unless flags contains clause_explicit. In that case, an explicit representation is created. Implicit representations can only be created via ClauseCreator::create().

The function acts as a sink for the given clause (i.e. it decreases its reference count) unless flags contains clause_no_release.

integrate() is intended to be called in a post propagator. To integrate a set of clauses F, one would use a loop like this:

   bool MyPostProp::propagate(Solver& s) {
     bool r = true;
     while (!F.empty() && r) {
       SharedLiterals* C = f.pop();
       r = integrate(s, C, ...).ok;
     }
     return r;

This is an overloaded member function, provided for convenience. It differs from the above function only in what argument(s) it accepts.

Definition at line 316 of file clause.cpp.

ClauseCreator::Result Clasp::ClauseCreator::integrate	(	Solver &	s,
		SharedLiterals *	clause,
		uint32	flags
	)		`[static]`

Definition at line 354 of file clause.cpp.

const LitVec& Clasp::ClauseCreator::lits ( ) const [inline]

Returns the literals of the clause under construction.

Definition at line 146 of file clause.h.

LitVec& Clasp::ClauseCreator::lits ( ) [inline]

Definition at line 147 of file clause.h.

ClauseHead * Clasp::ClauseCreator::newLearntClause	(	Solver &	s,
		const ClauseRep &	clause,
		uint32	flags
	)		`[static, private]`

Definition at line 243 of file clause.cpp.

ClauseHead * Clasp::ClauseCreator::newProblemClause	(	Solver &	s,
		const ClauseRep &	clause,
		uint32	flags
	)		`[static, private]`

Definition at line 208 of file clause.cpp.

ClauseHead * Clasp::ClauseCreator::newUnshared	(	Solver &	s,
		SharedLiterals *	clause,
		const Literal *	w,
		const ClauseInfo &	e
	)		`[static, private]`

Definition at line 265 of file clause.cpp.

Literal& Clasp::ClauseCreator::operator[] ( uint32 i ) [inline]

Returns the literal at the given idx.

Definition at line 143 of file clause.h.

Literal Clasp::ClauseCreator::operator[] ( uint32 i ) const [inline]

Definition at line 144 of file clause.h.

ClauseRep Clasp::ClauseCreator::prepare ( bool fullSimplify )

Removes subsumed lits and orders first lits w.r.t watch order.

Definition at line 172 of file clause.cpp.

ClauseRep Clasp::ClauseCreator::prepare	(	Solver &	s,
		LitVec &	lits,
		uint32	flags,
		const ClauseInfo &	info = `ClauseInfo()`
	)		`[static]`

Prepares the clause given in lits.

A prepared clause [l1...ln] with n >= 2 is a clause that,

does not contain any duplicate or complementary literals and,
does not contain any subsumed literals (i.e. literals assigned on decision level 0) and,
is partially ordered w.r.t watchOrder(), i.e., watchOrder(l1) >= watchOrder(l2) and there is no lj, j > 2, s.th. watchOrder(lj) > watchOrder(l2)

Removes subsumed literals from lits and reorders lits s.th. the first literals are valid watches. Furthermore, if flags contains clause_force_simplify, duplicate literals are removed from lits and tautologies are replaced with the single literal True.

Definition at line 162 of file clause.cpp.

ClauseRep Clasp::ClauseCreator::prepare	(	Solver &	s,
		const Literal *	in,
		uint32	inSize,
		const ClauseInfo &	e,
		uint32	flags,
		Literal *	out,
		uint32	outMax = `UINT32_MAX`
	)		`[static, private]`

Definition at line 125 of file clause.cpp.

void Clasp::ClauseCreator::reserve ( LitVec::size_type s ) [inline]

Reserve space for a clause of size s.

Definition at line 94 of file clause.h.

ClauseCreator& Clasp::ClauseCreator::setActivity ( uint32 a ) [inline]

Sets the initial activity of the clause under construction.

Definition at line 133 of file clause.h.

ClauseCreator& Clasp::ClauseCreator::setLbd ( uint32 lbd ) [inline]

Sets the initial literal block distance of the clause under construction.

Definition at line 135 of file clause.h.

void Clasp::ClauseCreator::setSolver ( Solver & s ) [inline]

Sets the solver in which created clauses are stored.

Definition at line 90 of file clause.h.

uint32 Clasp::ClauseCreator::size ( ) const [inline]

Returns the current size of the clause under construction.

Definition at line 141 of file clause.h.

ClauseCreator & Clasp::ClauseCreator::start ( ConstraintType t = Constraint_t::static_constraint )

Starts the creation of a new clause.

Precondition:: s.decisionLevel() == 0 || t != Constraint_t::static_constraint

Definition at line 108 of file clause.cpp.

ClauseCreator::Status Clasp::ClauseCreator::status	(	const Solver &	s,
		const Literal *	clause_begin,
		const Literal *	clause_end
	)		`[static]`

Returns the status of the given clause w.r.t s.

Definition at line 176 of file clause.cpp.

ClauseCreator::Status Clasp::ClauseCreator::status	(	const Solver &	s,
		const ClauseRep &	c
	)		`[static]`

Definition at line 183 of file clause.cpp.

ConstraintType Clasp::ClauseCreator::type ( ) const [inline]

Returns the clause's type.

Definition at line 149 of file clause.h.

uint32 Clasp::ClauseCreator::watchOrder	(	const Solver &	s,
		Literal	p
	)		`[static]`

Returns an abstraction of p's decision level that can be used to order literals.

The function returns a value, s.th order(any true literal) > order(any free literal) > order(any false literal). Furthermore, for equally assigned literals p and q, order(p) > order(q), iff level(p) > level(q).

Definition at line 115 of file clause.cpp.