Clasp::SatPreprocessor::Clause Class Reference

A clause class optimized for preprocessing. More...

#include <shared_context.h>

List of all members.

Public Member Functions
uint64	abstraction () const
uint64 &	abstraction ()
void	destroy ()
bool	inQ () const
Clause *	linkRemoved (Clause *next)
bool	marked () const
Clause *	next () const
const Literal &	operator[] (uint32 x) const
Literal &	operator[] (uint32 x)
void	setInQ (bool b)
void	setMarked (bool b)
void	simplify (Solver &s)
uint32	size () const
void	strengthen (Literal p)
Static Public Member Functions
static uint64	abstractLit (Literal p)
static Clause *	newClause (const Literal *lits, uint32 size)
Private Member Functions
	Clause (const Literal *lits, uint32 size)
Private Attributes
union {
uint64   abstr
Clause *   next
}	data_
uint32	inQ_: 1
Literal	lits_ [1]
uint32	marked_: 1
uint32	size_: 30

---

Detailed Description

A clause class optimized for preprocessing.

Definition at line 54 of file shared_context.h.

---

Constructor & Destructor Documentation

Clasp::SatPreprocessor::Clause::Clause	(	const Literal *	lits,
		uint32	size
	)		[private]

Definition at line 449 of file shared_context.cpp.

---

Member Function Documentation

uint64 Clasp::SatPreprocessor::Clause::abstraction

(

)

const [inline]

Definition at line 61 of file shared_context.h.

uint64& Clasp::SatPreprocessor::Clause::abstraction

(

)

[inline]

Definition at line 67 of file shared_context.h.

static uint64 Clasp::SatPreprocessor::Clause::abstractLit

(

Literal

p

)

[inline, static]

Definition at line 57 of file shared_context.h.

void Clasp::SatPreprocessor::Clause::destroy

(

)

Definition at line 472 of file shared_context.cpp.

bool Clasp::SatPreprocessor::Clause::inQ

(

)

const [inline]

Definition at line 60 of file shared_context.h.

Clause* Clasp::SatPreprocessor::Clause::linkRemoved

(

Clause *

next

)

[inline]

Definition at line 68 of file shared_context.h.

bool Clasp::SatPreprocessor::Clause::marked

(

)

const [inline]

Definition at line 63 of file shared_context.h.

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

Definition at line 444 of file shared_context.cpp.

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

(

)

const [inline]

Definition at line 62 of file shared_context.h.

const Literal& Clasp::SatPreprocessor::Clause::operator[]

(

uint32

x

)

const [inline]

Definition at line 59 of file shared_context.h.

Literal& Clasp::SatPreprocessor::Clause::operator[]

(

uint32

x

)

[inline]

Definition at line 64 of file shared_context.h.

void Clasp::SatPreprocessor::Clause::setInQ

(

bool

b

)

[inline]

Definition at line 65 of file shared_context.h.

void Clasp::SatPreprocessor::Clause::setMarked

(

bool

b

)

[inline]

Definition at line 66 of file shared_context.h.

void Clasp::SatPreprocessor::Clause::simplify

(

Solver &

s

)

Definition at line 460 of file shared_context.cpp.

uint32 Clasp::SatPreprocessor::Clause::size

(

)

const [inline]

Definition at line 58 of file shared_context.h.

void Clasp::SatPreprocessor::Clause::strengthen

(

Literal

p

)

Definition at line 452 of file shared_context.cpp.

---

Member Data Documentation

uint64 Clasp::SatPreprocessor::Clause::abstr

Definition at line 75 of file shared_context.h.

union { ... } Clasp::SatPreprocessor::Clause::data_ [private]

uint32 Clasp::SatPreprocessor::Clause::inQ_ [private]

Definition at line 79 of file shared_context.h.

Literal Clasp::SatPreprocessor::Clause::lits_[1] [private]

Definition at line 81 of file shared_context.h.

uint32 Clasp::SatPreprocessor::Clause::marked_ [private]

Definition at line 80 of file shared_context.h.

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

Definition at line 76 of file shared_context.h.

uint32 Clasp::SatPreprocessor::Clause::size_ [private]

Definition at line 78 of file shared_context.h.

---

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

• shared_context.h
• shared_context.cpp