sat::Literal Class Reference

Structure representing a literal in a CNF-SAT problem. More...

#include <basic_structures.hpp>

Public Member Functions
	Literal (unsigned val)
unsigned	get () const
Literal	negate () const
short	sign () const
bool	operator== (Literal) const

Detailed Description

Structure representing a literal in a CNF-SAT problem.

A literal of variable x is either x or ¬x

Constructor & Destructor Documentation

Literal()

sat::Literal::Literal

(

unsigned

val

)

CTor

Parameters

val	Literal identifier. A literal is related to a variable by dividing its identifier by two. An even identifier stands for a negative literal, an odd one for a positive see also sat::pos and sat::neg

Member Function Documentation

get()

unsigned sat::Literal::get

(

)

const

Gets the underlying literal identifier

Returns

the literal identifier

Referenced by sat::operator<<().

Here is the caller graph for this function:

negate()

Literal sat::Literal::negate

(

)

const

Gets the negated literal

Returns

the negated literal

operator==()

bool sat::Literal::operator==

(

Literal

other

)

const

Compares underlying literal identifiers

Returns

True if both literals are exactly the same (sign and variable)

sign()

short sat::Literal::sign

(

)

const

Gets the sign of the literal

Returns

-1 if negative literal, +1 else

Referenced by sat::operator<<().

Here is the caller graph for this function:

---

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

• Solver/basic_structures.hpp
• Solver/basic_structures.cpp