[−][src]Struct varisat_formula::lit::Lit
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.
fn bitxor(self, rhs: bool) -> Lit
[src]
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]
fn hash<__H: Hasher>(&self, state: &mut __H)
[src]
fn hash_slice<H>(data: &[Self], state: &mut H) where
H: Hasher,
1.3.0[src]
H: Hasher,
impl Not for Lit
[src]
impl Ord for Lit
[src]
fn cmp(&self, other: &Lit) -> Ordering
[src]
#[must_use]fn max(self, other: Self) -> Self
1.21.0[src]
#[must_use]fn min(self, other: Self) -> Self
1.21.0[src]
#[must_use]fn clamp(self, min: Self, max: Self) -> Self
[src]
impl PartialEq<Lit> for Lit
[src]
impl PartialOrd<Lit> for Lit
[src]
fn partial_cmp(&self, other: &Lit) -> Option<Ordering>
[src]
fn lt(&self, other: &Lit) -> bool
[src]
fn le(&self, other: &Lit) -> bool
[src]
fn gt(&self, other: &Lit) -> bool
[src]
fn ge(&self, other: &Lit) -> bool
[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]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T> ToString for T where
T: Display + ?Sized,
[src]
T: Display + ?Sized,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,