Stay organized with collections
Save and categorize content based on your preferences.
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.
[[["Easy to understand","easyToUnderstand","thumb-up"],["Solved my problem","solvedMyProblem","thumb-up"],["Other","otherUp","thumb-up"]],[["Missing the information I need","missingTheInformationINeed","thumb-down"],["Too complicated / too many steps","tooComplicatedTooManySteps","thumb-down"],["Out of date","outOfDate","thumb-down"],["Samples / code issue","samplesCodeIssue","thumb-down"],["Other","otherDown","thumb-down"]],["Last updated 2024-08-06 UTC."],[[["A literal in C++ represents a variable or its negation, indicated as positive or negative, respectively."],["Literals have two encoding schemes: \"signed\" for input/output and \"index\" for internal efficiency."],["The \"signed\" encoding uses (x + 1) for variable x and -(x + 1) for its negation, where x is the 0-based variable index."],["The \"index\" encoding utilizes (x \u003c\u003c 1) for variable x and the same value XOR 1 for its negation, ensuring a positive or zero value."],["The `Literal` class provides methods for creation, manipulation, and accessing information about literals, such as negation, index, and signed value."]]],["Literals represent a variable or its negation, categorized as positive or negative. They use two encodings: \"signed\" for I/O, and \"index\" internally. Signed encoding uses `(x + 1)` for variable `x` and `-(x + 1)` for negation, with 0 undefined. Index encoding uses `(x \u003c\u003c 1)` for `x` and `XOR 1` for negation. Key methods include `Index`, `IsNegative`, `IsPositive`, `SignedValue`, `Negated` and `NegatedIndex`, for managing literal properties and encodings. The `Literal` constructor is also described.\n"]]
