[][src]Struct varisat_formula::lit::Lit

#[repr(transparent)]pub struct Lit { /* fields omitted */ }

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[src]

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

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

pub fn positive(var: Var) -> Lit[src]

Create a positive literal from a Var.

pub fn negative(var: Var) -> Lit[src]

Create a negative literal from a Var.

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

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[src]

Create a literal with the given encoding.

pub fn from_dimacs(number: isize) -> Lit[src]

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[src]

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

pub fn index(self) -> usize[src]

0-based index of the literal's variable.

pub fn var(self) -> Var[src]

The literal's variable.

pub fn is_negative(self) -> bool[src]

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

pub fn is_positive(self) -> bool[src]

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

pub fn code(self) -> usize[src]

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[src]

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

Trait Implementations

impl BitXor<bool> for Lit[src]

type Output = Lit

The resulting type after applying the ^ operator.

impl Clone for Lit[src]

impl Copy for Lit[src]

impl Debug for Lit[src]

Uses the 1-based DIMACS CNF encoding.

impl Display for Lit[src]

Uses the 1-based DIMACS CNF encoding.

impl Eq for Lit[src]

impl From<Var> for Lit[src]

impl Hash for Lit[src]

impl Not for Lit[src]

type Output = Lit

The resulting type after applying the ! operator.

impl Ord for Lit[src]

impl PartialEq<Lit> for Lit[src]

impl PartialOrd<Lit> for Lit[src]

impl StructuralEq for Lit[src]

impl StructuralPartialEq for Lit[src]

Auto Trait Implementations

impl RefUnwindSafe for Lit

impl Send for Lit

impl Sync for Lit

impl Unpin for Lit

impl UnwindSafe for Lit

Blanket Implementations

impl<T> Any for T where
    T: 'static + ?Sized
[src]

impl<T> Borrow<T> for T where
    T: ?Sized
[src]

impl<T> BorrowMut<T> for T where
    T: ?Sized
[src]

impl<T> From<T> for T[src]

impl<T, U> Into<U> for T where
    U: From<T>, 
[src]

impl<T> ToOwned for T where
    T: Clone
[src]

type Owned = T

The resulting type after obtaining ownership.

impl<T> ToString for T where
    T: Display + ?Sized
[src]

impl<T, U> TryFrom<U> for T where
    U: Into<T>, 
[src]

type Error = Infallible

The type returned in the event of a conversion error.

impl<T, U> TryInto<U> for T where
    U: TryFrom<T>, 
[src]

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.