C++ Reference: class Literal

This documentation is automatically generated.

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.
Method
DebugString

Return type: std::string

Index

Return type: LiteralIndex

IsNegative

Return type: bool

IsPositive

Return type: bool

Literal

Arguments: int signed_value

Not explicit for tests so we can write: std::vector literal = {+1, -3, +4, -9};

Literal

Literal

Return type: explicit

Arguments: LiteralIndex index

Literal

Arguments: BooleanVariable variable, bool is_positive

Negated

Return type: Literal

NegatedIndex

Return type: LiteralIndex

SignedValue

Return type: int

Variable

Return type: BooleanVariable

Send feedback about...