`tiny.smt.Literal`

Reference tiny.smt Literal

Defined in sat.types.

A variable or its negation, packed into one 32-bit number.

API (10)

Public operations.

fromDimacs: Returns the literal a DIMACS number stands for: variable |value| - 1, negated when value is negative.
index: Returns the packed number as a usize.
init: Returns the literal of variable variable_index, unnegated when polarity is true and negated when it is false.
isPositive: Returns true for an unnegated literal.
negated: Returns the literal of the same variable with the opposite sign.
negative: Returns the negated literal of variable variable_index.
positive: Returns the unnegated literal of variable variable_index.
toDimacs: Returns the DIMACS number of the literal: the variable index plus one, negative for a negated literal.
variable: Returns the variable index of the literal.

Public fields and members.

Static calls · unresolved targets: unknown · external targets: unknown.

Source

Source: lib/smt/src/sat/types.zig:117

1/// A variable or its negation, packed into one 32-bit number. A caller builds every clause and2/// every assumption from literals. Variables are numbered from 0 in the order `Solver.addVariable`3/// returns them.4pub const Literal = struct {5    /// The packed number: twice the variable index, plus one for a negated literal. Two literals6    /// are equal when their `raw` values are equal, and callers compare literals that way.7    raw: u32,89    /// Returns the literal of variable `variable_index`, unnegated when `polarity` is true and10    /// negated when it is false. Code that picks the sign at run time calls it. An index of11    /// 2147483648 or more overflows the packed number, which panics in safe builds.12    pub fn init(variable_index: u32, polarity: bool) Literal {13        return .{ .raw = variable_index * 2 + if (polarity) @as(u32, 0) else @as(u32, 1) };14    }1516    /// Returns the unnegated literal of variable `variable_index`. A caller writes a clause whose17    /// signs it knows in its source.18    pub fn positive(variable_index: u32) Literal {19        return init(variable_index, true);20    }2122    /// Returns the negated literal of variable `variable_index`. A caller writes a clause whose23    /// signs it knows in its source.24    pub fn negative(variable_index: u32) Literal {25        return init(variable_index, false);26    }2728    /// Returns the variable index of the literal. A caller finds which variable a literal names,29    /// for example to check it against a variable count.30    pub fn variable(self: Literal) u32 {31        return self.raw >> 1;32    }3334    /// Returns true for an unnegated literal. A caller reads a literal's sign to evaluate it under35    /// an assignment.36    pub fn isPositive(self: Literal) bool {37        return self.raw & 1 == 0;38    }3940    /// Returns the literal of the same variable with the opposite sign. An encoder calls it to41    /// state the negation of a condition.42    pub fn negated(self: Literal) Literal {43        return .{ .raw = self.raw ^ 1 };44    }4546    /// Returns the packed number as a `usize`. The solver indexes its per-literal lists of watching47    /// clauses by it, two entries per variable.48    pub fn index(self: Literal) usize {49        return @intCast(self.raw);50    }5152    /// Returns the literal a DIMACS number stands for: variable `|value| - 1`, negated when `value`53    /// is negative. The DIMACS and proof readers call it on each number of a clause. The call54    /// returns `error.InvalidDimacsLiteral` for 0, the number that ends a clause in that format.55    /// The value -2147483648 makes it panic, because its negation does not fit in 32 bits.56    pub fn fromDimacs(value: i32) !Literal {57        if (value == 0) return error.InvalidDimacsLiteral;58        const magnitude: u32 = @intCast(if (value < 0) -value else value);59        return init(magnitude - 1, value > 0);60    }6162    /// Returns the DIMACS number of the literal: the variable index plus one, negative for a63    /// negated literal. The DIMACS and proof writers call it on each literal they print. Variable64    /// index 2147483647 makes it panic, because its number does not fit in `i32`.65    pub fn toDimacs(self: Literal) i32 {66        const one_based: i32 = @intCast(self.variable() + 1);67        return if (self.isPositive()) one_based else -one_based;68    }69};

Source: lib/smt/src/root.zig:105

1pub const Literal = sat.Literal;

Static calls · unresolved targets: 0 · external targets: 0.

Also reachable as

sat.Literal, sat.solver.Literal.

Complete caller list for `Literal.init`

9 direct callers.

Complete caller list for `Literal.negative`

40 direct callers.

Complete caller list for `Literal.positive`

42 direct callers.

Audit

Definitions	10
Public names	40
Members	1
Version	`26.7.0`
Revision	`daab053ee433`

tiny.smt.Literal

API (10)

Actions

Fields and members