Minisat::Clause Class Reference

Represents a simple class for clause storage. More...

#include <ogdf/external/Minisat.h>

Public Member Functions
	Clause ()
	Clause (const Clause &src)
virtual	~Clause ()
void	add (Internal::Var signedVar)
	adds a literal to the clause
void	addMultiple (int Amount,...)
	add multiple literals to the clause
bool	getSign (Internal::Var x)
	returns the sign of a variable if its present within the clause, if the variable is not representet false will be returned with a message
void	removeLit (Internal::Var x)
void	setSign (Internal::Var x, bool sign)
	sets the sign of a variable if its present within the clause
void	writeToConsole ()

Static Public Member Functions
static char	convertLitSign (Internal::Lit lit)
	converts the sign of a lit into char

Public Attributes
Internal::vec< Internal::Lit >	m_ps

Detailed Description

Represents a simple class for clause storage.

This class is not similar to clause from Minisat. Only use it as a wrapper. Use clause as a pointer-type of Clause.

Definition at line 59 of file Minisat.h.

Constructor & Destructor Documentation

Clause() [1/2]

Minisat::Clause::Clause ( )

inline

Definition at line 63 of file Minisat.h.

Clause() [2/2]

Minisat::Clause::Clause ( const Clause &  src )

inline

Definition at line 65 of file Minisat.h.

~Clause()

virtual Minisat::Clause::~Clause ( )

inlinevirtual

Definition at line 67 of file Minisat.h.

Member Function Documentation

add()

void Minisat::Clause::add ( Internal::Var  signedVar )

inline

adds a literal to the clause

Parameters

signedVar

is a signed int representing a variable

Definition at line 76 of file Minisat.h.

addMultiple()

void Minisat::Clause::addMultiple	(	int	Amount,
			...
	)

add multiple literals to the clause

Parameters

Amount

is the number of literals to add to the clause

convertLitSign()

static char Minisat::Clause::convertLitSign ( Internal::Lit  lit )

inlinestatic

converts the sign of a lit into char

Definition at line 127 of file Minisat.h.

getSign()

bool Minisat::Clause::getSign ( Internal::Var  x )

inline

returns the sign of a variable if its present within the clause, if the variable is not representet false will be returned with a message

Definition at line 104 of file Minisat.h.

removeLit()

void Minisat::Clause::removeLit ( Internal::Var  x )

inline

Definition at line 114 of file Minisat.h.

setSign()

void Minisat::Clause::setSign ( Internal::Var  x, bool  sign  )

inline

sets the sign of a variable if its present within the clause

Definition at line 93 of file Minisat.h.

writeToConsole()

void Minisat::Clause::writeToConsole ( )

inline

Definition at line 135 of file Minisat.h.

Member Data Documentation

m_ps

Internal::vec<Internal::Lit> Minisat::Clause::m_ps

Definition at line 61 of file Minisat.h.

---

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

• include/ogdf/external/Minisat.h