C++ Reference: class Literal

Note: 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: 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