Struct Lit

pub struct Lit { /* private fields */ }

A boolean literal.

A literal is a variable or the negation of a variable.

Conceptually a literal consists of a Var and a bool indicating whether the literal represents the variable (positive literal) or its negation (negative literal).

Internally a literal is represented as an integer that is two times the index of its variable when it is positive or one more when it is negative. This integer is called the code of the literal.

The restriction on the range of allowed indices for Var also applies to Lit.

Implementations

impl Lit

pub fn from_var(var: Var, polarity: bool) -> Lit

Creates a literal from a Var and a bool that is true when the literal is positive.

pub fn positive(var: Var) -> Lit

Create a positive literal from a Var.

pub fn negative(var: Var) -> Lit

Create a negative literal from a Var.

pub fn from_index(index: usize, polarity: bool) -> Lit

Create a literal from a variable index and a bool that is true when the literal is positive.

pub fn from_code(code: usize) -> Lit

Create a literal with the given encoding.

pub fn from_dimacs(number: isize) -> Lit

Creates a literal from an integer.

The absolute value is used as 1-based index, the sign of the integer is used as sign of the literal.

pub fn to_dimacs(self) -> isize

1-based Integer representation of the literal, opposite of from_dimacs.

pub fn index(self) -> usize

0-based index of the literal’s variable.

pub fn var(self) -> Var

The literal’s variable.

pub fn is_negative(self) -> bool

Whether the literal is negative, i.e. a negated variable.

pub fn is_positive(self) -> bool

Whether the literal is positive, i.e. a non-negated variable.

pub fn code(self) -> usize

Two times the variable’s index for positive literals and one more for negative literals.

This is also the internal encoding.

pub fn map_var(self, f: impl FnOnce(Var) -> Var) -> Lit

Apply a function to the variable of the literal, without changing the polarity.

Trait Implementations

impl BitXor<bool> for Lit

type Output = Lit

The resulting type after applying the ^ operator.

fn bitxor(self, rhs: bool) -> Lit

Performs the ^ operation.

impl Clone for Lit

fn clone(&self) -> Lit

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Lit

Uses the 1-based DIMACS CNF encoding.

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Display for Lit

Uses the 1-based DIMACS CNF encoding.

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl From<Var> for Lit

fn from(var: Var) -> Lit

Converts to this type from the input type.

impl Hash for Lit

fn hash<__H>(&self, state: &mut __H)

where __H: Hasher,

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Not for Lit

type Output = Lit

The resulting type after applying the ! operator.

fn not(self) -> Lit

Performs the unary ! operation.

impl Ord for Lit

fn cmp(&self, other: &Lit) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl PartialEq for Lit

fn eq(&self, other: &Lit) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PartialOrd for Lit

fn partial_cmp(&self, other: &Lit) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl Copy for Lit

impl Eq for Lit

impl StructuralPartialEq for Lit