Clasp::SatPreprocessor::Clause Class Reference

A clause class optimized for preprocessing. More...

#include <shared_context.h>

Collaboration diagram for Clasp::SatPreprocessor::Clause:

Public Member Functions
uint32	size () const
const Literal &	operator[] (uint32 x) const
bool	inQ () const
uint64	abstraction () const
Clause *	next () const
bool	marked () const
Literal &	operator[] (uint32 x)
void	setInQ (bool b)
void	setMarked (bool b)
uint64 &	abstraction ()
Clause *	linkRemoved (Clause *next)
void	strengthen (Literal p)
void	simplify (Solver &s)
void	destroy ()

Static Public Member Functions
static Clause *	newClause (const Literal *lits, uint32 size)
static uint64	abstractLit (Literal p)

Detailed Description

A clause class optimized for preprocessing.

Member Function Documentation

uint64 Clasp::SatPreprocessor::Clause::abstraction ( ) const

inline

uint64& Clasp::SatPreprocessor::Clause::abstraction ( )

inline

static uint64 Clasp::SatPreprocessor::Clause::abstractLit ( Literal  p )

inlinestatic

Here is the call graph for this function:

void Clasp::SatPreprocessor::Clause::destroy

(

)

bool Clasp::SatPreprocessor::Clause::inQ ( ) const

inline

Clause* Clasp::SatPreprocessor::Clause::linkRemoved ( Clause *  next )

inline

Here is the call graph for this function:

bool Clasp::SatPreprocessor::Clause::marked ( ) const

inline

SatPreprocessor::Clause * Clasp::SatPreprocessor::Clause::newClause ( const Literal *  lits, uint32  size  )

static

Clause* Clasp::SatPreprocessor::Clause::next ( ) const

inline

const Literal& Clasp::SatPreprocessor::Clause::operator[] ( uint32  x ) const

inline

Literal& Clasp::SatPreprocessor::Clause::operator[] ( uint32  x )

inline

void Clasp::SatPreprocessor::Clause::setInQ ( bool  b )

inline

void Clasp::SatPreprocessor::Clause::setMarked ( bool  b )

inline

void Clasp::SatPreprocessor::Clause::simplify

(

Solver &

s

)

Here is the call graph for this function:

uint32 Clasp::SatPreprocessor::Clause::size ( ) const

inline

void Clasp::SatPreprocessor::Clause::strengthen

(

Literal

p

)

Here is the call graph for this function:

Member Data Documentation

uint64 Clasp::SatPreprocessor::Clause::abstr

Clause* Clasp::SatPreprocessor::Clause::next

---

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