Clasp::SatPreprocessor Class Reference

Base class for preprocessors working on clauses only. More...

#include <shared_context.h>

Inheritance diagram for Clasp::SatPreprocessor:

List of all members.

Classes
class	Clause
	A clause class optimized for preprocessing. More...
struct	Stats
Public Types
typedef SatPreParams	Options
Public Member Functions
bool	addClause (const LitVec &cl)
	Adds a clause to the preprocessor.
bool	addClause (const Literal *clause, uint32 size)
void	cleanUp (bool discardEliminated=false)
	Force removal of state & clauses.
virtual SatPreprocessor *	clone ()=0
	Creates a clone of this preprocessor.
void	extendModel (ValueVec &m, LitVec &open)
	Extends the model in m with values for any eliminated variables.
uint32	numClauses () const
bool	preprocess (SharedContext &ctx, SatPreParams &opts)
	Runs the preprocessor on all clauses that were previously added.
bool	preprocess (SharedContext &ctx)
	SatPreprocessor ()
virtual	~SatPreprocessor ()
Public Attributes
struct Clasp::SatPreprocessor::Stats	stats
Protected Types
typedef PodVector< Clause * >::type	ClauseList
Protected Member Functions
Clause *	clause (uint32 clId)
const Clause *	clause (uint32 clId) const
void	destroyClause (uint32 clId)
void	discardClauses (bool discardEliminated)
virtual void	doCleanUp ()=0
virtual void	doExtendModel (ValueVec &m, LitVec &open)=0
virtual bool	doPreprocess ()=0
void	eliminateClause (uint32 id)
void	freezeSeen ()
virtual bool	initPreprocess (SatPreParams &opts)=0
void	setClause (uint32 clId, const LitVec &cl)
Protected Attributes
SharedContext *	ctx_
Clause *	elimTop_
Private Member Functions
SatPreprocessor &	operator= (const SatPreprocessor &)
	SatPreprocessor (const SatPreprocessor &)
Private Attributes
ClauseList	clauses_
Range32	seen_
LitVec	units_

---

Detailed Description

Base class for preprocessors working on clauses only.

Definition at line 51 of file shared_context.h.

---

Member Typedef Documentation

typedef PodVector<Clause*>::type Clasp::SatPreprocessor::ClauseList [protected]

Definition at line 122 of file shared_context.h.

typedef SatPreParams Clasp::SatPreprocessor::Options

Definition at line 120 of file shared_context.h.

---

Constructor & Destructor Documentation

Clasp::SatPreprocessor::SatPreprocessor

(

)

[inline]

Definition at line 84 of file shared_context.h.

Clasp::SatPreprocessor::~SatPreprocessor

(

)

[virtual]

Definition at line 311 of file shared_context.cpp.

Clasp::SatPreprocessor::SatPreprocessor

(

const SatPreprocessor &

)

[private]

---

Member Function Documentation

bool Clasp::SatPreprocessor::addClause

(

const LitVec &

cl

)

[inline]

Adds a clause to the preprocessor.

Precondition:

clause is not a tautology (i.e. does not contain both l and ~l)

clause is a set (i.e. does not contain l more than once)

Returns:

true if clause was added. False if adding the clause makes the problem UNSAT

Definition at line 100 of file shared_context.h.

bool Clasp::SatPreprocessor::addClause	(	const Literal *	clause,
		uint32	size
	)

Definition at line 335 of file shared_context.cpp.

Clause* Clasp::SatPreprocessor::clause

(

uint32

clId

)

[inline, protected]

Definition at line 127 of file shared_context.h.

const Clause* Clasp::SatPreprocessor::clause

(

uint32

clId

)

const [inline, protected]

Definition at line 128 of file shared_context.h.

void Clasp::SatPreprocessor::cleanUp

(

bool

discardEliminated = false

)

Force removal of state & clauses.

Definition at line 329 of file shared_context.cpp.

virtual SatPreprocessor* Clasp::SatPreprocessor::clone

(

)

[pure virtual]

Creates a clone of this preprocessor.

Note:

The function does not clone any clauses already added to *this.

Implemented in Clasp::SatElite::SatElite.

void Clasp::SatPreprocessor::destroyClause

(

uint32

clId

)

[inline, protected]

Definition at line 134 of file shared_context.h.

void Clasp::SatPreprocessor::discardClauses

(

bool

discardEliminated

)

[protected]

Definition at line 314 of file shared_context.cpp.

virtual void Clasp::SatPreprocessor::doCleanUp

(

)

[protected, pure virtual]

Implemented in Clasp::SatElite::SatElite.

virtual void Clasp::SatPreprocessor::doExtendModel	(	ValueVec &	m,
		LitVec &	open
	)		[protected, pure virtual]

Implemented in Clasp::SatElite::SatElite.

virtual bool Clasp::SatPreprocessor::doPreprocess

(

)

[protected, pure virtual]

Implemented in Clasp::SatElite::SatElite.

void Clasp::SatPreprocessor::eliminateClause

(

uint32

id

)

[inline, protected]

Definition at line 139 of file shared_context.h.

void Clasp::SatPreprocessor::extendModel	(	ValueVec &	m,
		LitVec &	open
	)

Extends the model in m with values for any eliminated variables.

Definition at line 433 of file shared_context.cpp.

void Clasp::SatPreprocessor::freezeSeen

(

)

[protected]

Definition at line 348 of file shared_context.cpp.

virtual bool Clasp::SatPreprocessor::initPreprocess

(

SatPreParams &

opts

)

[protected, pure virtual]

Implemented in Clasp::SatElite::SatElite.

uint32 Clasp::SatPreprocessor::numClauses

(

)

const [inline]

Definition at line 93 of file shared_context.h.

SatPreprocessor& Clasp::SatPreprocessor::operator=

(

const SatPreprocessor &

)

[private]

bool Clasp::SatPreprocessor::preprocess	(	SharedContext &	ctx,
		SatPreParams &	opts
	)

Runs the preprocessor on all clauses that were previously added.

Precondition:

A ctx.startAddConstraint() was called and has variables for all added clauses.

Definition at line 357 of file shared_context.cpp.

bool Clasp::SatPreprocessor::preprocess

(

SharedContext &

ctx

)

Definition at line 429 of file shared_context.cpp.

void Clasp::SatPreprocessor::setClause	(	uint32	clId,
		const LitVec &	cl
	)		[inline, protected]

Definition at line 131 of file shared_context.h.

---

Member Data Documentation

ClauseList Clasp::SatPreprocessor::clauses_ [private]

Definition at line 149 of file shared_context.h.

SharedContext* Clasp::SatPreprocessor::ctx_ [protected]

Definition at line 144 of file shared_context.h.

Clause* Clasp::SatPreprocessor::elimTop_ [protected]

Definition at line 145 of file shared_context.h.

Range32 Clasp::SatPreprocessor::seen_ [private]

Definition at line 151 of file shared_context.h.

struct Clasp::SatPreprocessor::Stats Clasp::SatPreprocessor::stats

LitVec Clasp::SatPreprocessor::units_ [private]

Definition at line 150 of file shared_context.h.

---

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

• shared_context.h
• shared_context.cpp