Clasp::SatPreprocessor Class Reference

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

#include <shared_context.h>

Inheritance diagram for Clasp::SatPreprocessor:

Collaboration diagram for Clasp::SatPreprocessor:

Classes
class	Clause
	A clause class optimized for preprocessing. More...
struct	Stats

Public Types
typedef SatPreParams	Options

Public Member Functions
	SatPreprocessor ()
virtual	~SatPreprocessor ()
virtual SatPreprocessor *	clone ()=0
	Creates a clone of this preprocessor. More...
uint32	numClauses () const
bool	addClause (const LitVec &cl)
	Adds a clause to the preprocessor. More...
bool	addClause (const Literal *clause, uint32 size)
bool	preprocess (SharedContext &ctx, SatPreParams &opts)
	Runs the preprocessor on all clauses that were previously added. More...
bool	preprocess (SharedContext &ctx)
void	cleanUp (bool discardEliminated=false)
	Force removal of state & clauses. More...
void	extendModel (ValueVec &m, LitVec &open)
	Extends the model in m with values for any eliminated variables. More...

Public Attributes
struct Clasp::SatPreprocessor::Stats	stats

Protected Types
typedef PodVector< Clause * >::type	ClauseList

Protected Member Functions
virtual bool	initPreprocess (SatPreParams &opts)=0
virtual bool	doPreprocess ()=0
virtual void	doExtendModel (ValueVec &m, LitVec &open)=0
virtual void	doCleanUp ()=0
Clause *	clause (uint32 clId)
const Clause *	clause (uint32 clId) const
void	freezeSeen ()
void	discardClauses (bool discardEliminated)
void	setClause (uint32 clId, const LitVec &cl)
void	destroyClause (uint32 clId)
void	eliminateClause (uint32 id)

Protected Attributes
SharedContext *	ctx_
Clause *	elimTop_

Detailed Description

Base class for preprocessors working on clauses only.

Member Typedef Documentation

typedef PodVector<Clause*>::type Clasp::SatPreprocessor::ClauseList

protected

typedef SatPreParams Clasp::SatPreprocessor::Options

Constructor & Destructor Documentation

Clasp::SatPreprocessor::SatPreprocessor ( )

inline

Clasp::SatPreprocessor::~SatPreprocessor ( )

virtual

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

Here is the call graph for this function:

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

Clause* Clasp::SatPreprocessor::clause ( uint32  clId )

inlineprotected

const Clause* Clasp::SatPreprocessor::clause ( uint32  clId ) const

inlineprotected

void Clasp::SatPreprocessor::cleanUp

(

bool

discardEliminated = false

)

Force removal of state & clauses.

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 )

inlineprotected

void Clasp::SatPreprocessor::discardClauses ( bool  discardEliminated )

protected

Here is the call graph for this function:

virtual void Clasp::SatPreprocessor::doCleanUp ( )

protectedpure virtual

Implemented in Clasp::SatElite::SatElite.

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

protectedpure virtual

Implemented in Clasp::SatElite::SatElite.

virtual bool Clasp::SatPreprocessor::doPreprocess ( )

protectedpure virtual

Implemented in Clasp::SatElite::SatElite.

void Clasp::SatPreprocessor::eliminateClause ( uint32  id )

inlineprotected

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

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

void Clasp::SatPreprocessor::freezeSeen ( )

protected

virtual bool Clasp::SatPreprocessor::initPreprocess ( SatPreParams &  opts )

protectedpure virtual

Implemented in Clasp::SatElite::SatElite.

uint32 Clasp::SatPreprocessor::numClauses ( ) const

inline

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.

Here is the call graph for this function:

bool Clasp::SatPreprocessor::preprocess

(

SharedContext &

ctx

)

Here is the call graph for this function:

void Clasp::SatPreprocessor::setClause ( uint32  clId, const LitVec &  cl  )

inlineprotected

Here is the call graph for this function:

Member Data Documentation

SharedContext* Clasp::SatPreprocessor::ctx_

protected

Clause* Clasp::SatPreprocessor::elimTop_

protected

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

---

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

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