Open
Graph Drawing
Framework

 v. 2022.02 (Dogwood)
 

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 More...
 
void addMultiple (int Amount,...)
 add multiple literals to the clause More...
 
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 More...
 
void removeLit (Internal::Var x)
 
void setSign (Internal::Var x, bool sign)
 sets the sign of a variable if its present within the clause More...
 
void writeToConsole ()
 

Static Public Member Functions

static char convertLitSign (Internal::Lit lit)
 converts the sign of a lit into char More...
 

Public Attributes

Internal::vec< Internal::Litm_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 62 of file Minisat.h.

Constructor & Destructor Documentation

◆ Clause() [1/2]

Minisat::Clause::Clause ( )
inline

Definition at line 66 of file Minisat.h.

◆ Clause() [2/2]

Minisat::Clause::Clause ( const Clause src)
inline

Definition at line 67 of file Minisat.h.

◆ ~Clause()

virtual Minisat::Clause::~Clause ( )
inlinevirtual

Definition at line 68 of file Minisat.h.

Member Function Documentation

◆ add()

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

adds a literal to the clause

Parameters
signedVaris a signed int representing a variable

Definition at line 77 of file Minisat.h.

◆ addMultiple()

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

add multiple literals to the clause

Parameters
Amountis 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 138 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 111 of file Minisat.h.

◆ removeLit()

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

Definition at line 122 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 98 of file Minisat.h.

◆ writeToConsole()

void Minisat::Clause::writeToConsole ( )
inline

Definition at line 146 of file Minisat.h.

Member Data Documentation

◆ m_ps

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

Definition at line 65 of file Minisat.h.


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