operations_research::sat::Literal Class Reference

#include <sat_base.h>

Public Member Functions
	Literal (int signed_value)
	Literal ()=default
	Literal (LiteralIndex index)
	Literal (BooleanVariable variable, bool is_positive)
	operator LiteralIndex () const
BooleanVariable	Variable () const
bool	IsPositive () const
bool	IsNegative () const
LiteralIndex	Index () const
LiteralIndex	NegatedIndex () const
int	SignedValue () const
Literal	Negated () const
std::string	DebugString () const
bool	operator== (Literal other) const
bool	operator!= (Literal other) const
bool	operator< (const Literal &other) const

Friends
template<typename H >
H	AbslHashValue (H h, Literal literal)

Detailed Description

A literal is used to represent a variable or its negation. If it represents the variable it is said to be positive. If it represent its negation, it is said to be negative. We support two representations as an integer.

The "signed" encoding of a literal is convenient for input/output and is used in the cnf file format. For a 0-based variable index x, (x + 1) represent the variable x and -(x + 1) represent its negation. The signed value 0 is an undefined literal and this class can never contain it.

The "index" encoding of a literal is convenient as an index to an array and is the one used internally for efficiency. It is always positive or zero, and for a 0-based variable index x, (x << 1) encode the variable x and the same number XOR 1 encode its negation.

Definition at line 66 of file sat_base.h.

Constructor & Destructor Documentation

Literal() [1/4]

operations_research::sat::Literal::Literal ( int signed_value )

inlineexplicit

Definition at line 68 of file sat_base.h.

Literal() [2/4]

operations_research::sat::Literal::Literal ( )

default

Literal() [3/4]

operations_research::sat::Literal::Literal ( LiteralIndex index )

inlineexplicit

Definition at line 75 of file sat_base.h.

Literal() [4/4]

operations_research::sat::Literal::Literal ( BooleanVariable variable, bool is_positive )

inline

Definition at line 76 of file sat_base.h.

Member Function Documentation

DebugString()

std::string operations_research::sat::Literal::DebugString ( ) const

inline

Definition at line 100 of file sat_base.h.

Index()

LiteralIndex operations_research::sat::Literal::Index ( ) const

inline

Definition at line 91 of file sat_base.h.

IsNegative()

bool operations_research::sat::Literal::IsNegative ( ) const

inline

Definition at line 89 of file sat_base.h.

IsPositive()

bool operations_research::sat::Literal::IsPositive ( ) const

inline

Definition at line 88 of file sat_base.h.

Negated()

Literal operations_research::sat::Literal::Negated ( ) const

inline

Definition at line 98 of file sat_base.h.

NegatedIndex()

LiteralIndex operations_research::sat::Literal::NegatedIndex ( ) const

inline

Definition at line 92 of file sat_base.h.

operator LiteralIndex()

operations_research::sat::Literal::operator LiteralIndex ( ) const

inline

We want a literal to be implicitly converted to a LiteralIndex(). Before this, we used to have many literal.Index() that didn't add anything.

Todo

(user): LiteralIndex might not even be needed, but because of the signed value business, it is still safer with it.

Definition at line 85 of file sat_base.h.

operator!=()

bool operations_research::sat::Literal::operator!= ( Literal other ) const

inline

Definition at line 105 of file sat_base.h.

operator<()

bool operations_research::sat::Literal::operator< ( const Literal & other ) const

inline

Definition at line 106 of file sat_base.h.

operator==()

bool operations_research::sat::Literal::operator== ( Literal other ) const

inline

Definition at line 104 of file sat_base.h.

SignedValue()

int operations_research::sat::Literal::SignedValue ( ) const

inline

Definition at line 94 of file sat_base.h.

Variable()

BooleanVariable operations_research::sat::Literal::Variable ( ) const

inline

Definition at line 87 of file sat_base.h.

Friends And Related Symbol Documentation

AbslHashValue

template<typename H >

H AbslHashValue ( H h, Literal literal )

friend

Definition at line 109 of file sat_base.h.

---

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

• ortools/sat/sat_base.h