Struct rustsat::types::Lit

pub struct Lit { /* private fields */ }

Type representing literals, possibly negated boolean variables.

Implementations

impl Lit

pub fn new(idx: u32, negated: bool) -> Lit

Creates a new (negated or not) literal with a given index. Panics if idx > Var::MAX_IDX.

pub fn new_with_error(idx: u32, negated: bool) -> Result<Lit, TypeError>

Creates a new (negated or not) literal with a given index. Returns Err(TypeError::IdxTooHigh(idx, Var::MAX_IDX) if idx > Var::MAX_IDX.

pub fn new_unchecked(idx: u32, negated: bool) -> Lit

Creates a new (negated or not) literal with a given index. Does not perform any check on the index, therefore might produce an inconsistent variable. Only use this for performance reasons if you are sure that idx <= Var::MAX_IDX.

pub fn positive(idx: u32) -> Lit

Creates a new positive literal with a given index. Panics if idx > Var::MAX_IDX.

pub fn negative(idx: u32) -> Lit

Creates a new negated literal with a given index. Panics if idx > Var::MAX_IDX.

pub fn positive_with_error(idx: u32) -> Result<Lit, TypeError>

Creates a new positive literal with a given index. Panics if idx > Var::MAX_IDX.

pub fn negative_with_error(idx: u32) -> Result<Lit, TypeError>

Creates a new negated literal with a given index. Panics if idx > Var::MAX_IDX.

pub fn positive_unchecked(idx: u32) -> Lit

Creates a new positive literal with a given index. Does not perform any check on the index, therefore might produce an inconsistent variable. Only use this for performance reasons if you are sure that idx <= Var::MAX_IDX.

pub fn negative_unchecked(idx: u32) -> Lit

Creates a new negated literal with a given index. Does not perform any check on the index, therefore might produce an inconsistent variable. Only use this for performance reasons if you are sure that idx <= Var::MAX_IDX.

pub fn from_ipasir(val: c_int) -> Result<Lit, TypeError>

Create a literal from an IPASIR integer value. Returns an error if the value is zero or the index too high.

pub fn vidx(&self) -> usize

Gets the variable index of the literal

pub fn vidx32(&self) -> u32

Gets the 32bit variable index of the literal

pub fn lidx(&self) -> usize

Gets a literal representation for indexing data structures

pub fn var(&self) -> Var

Gets the variables that the literal corresponds to.

Examples

let var = Var::new(5);
let lit = Lit::negative(5);
assert_eq!(var, lit.var());

pub fn is_pos(&self) -> bool

True if the literal is positive.

pub fn is_neg(&self) -> bool

True if the literal is negated.

pub fn to_ipasir(self) -> c_int

Converts the literal to an integer as accepted by the IPASIR API and similar. The IPASIR literal will have idx+1 and be negative if the literal is negated. Panics if the literal does not fit into a c_int.

pub fn to_ipasir_with_error(self) -> Result<c_int, TypeError>

Converts the literal to an integer as accepted by the IPASIR API and similar. The IPASIR literal will have idx+1 and be negative if the literal is negated. Returns Err(TypeError::IdxTooHigh(_, _)) if the literal does not fit into a c_int.

Trait Implementations

impl Add<u32> for Lit

Incrementing literals. This preserves the sign of the literal.

type Output = Lit

The resulting type after applying the + operator.

fn add(self, rhs: u32) -> Self::Output

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

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

Formats the value using the given formatter.

impl Display for Lit

Literals can be printed with the Display trait

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

Formats the value using the given formatter.

impl Extend<Lit> for Clause

fn extend<T: IntoIterator<Item = Lit>>(&mut self, iter: T)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

🔬This is a nightly-only experimental API. (extend_one)

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

🔬This is a nightly-only experimental API. (extend_one)

Reserves capacity in a collection for the given number of additional elements.

impl Extend<Lit> for DbTotalizer

fn extend<T: IntoIterator<Item = Lit>>(&mut self, iter: T)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

🔬This is a nightly-only experimental API. (extend_one)

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

🔬This is a nightly-only experimental API. (extend_one)

Reserves capacity in a collection for the given number of additional elements.

impl<UBE, LBE> Extend<Lit> for Double<UBE, LBE>

where UBE: BoundUpper + Extend<Lit> + 'static, LBE: BoundLower + Extend<Lit> + 'static,

fn extend<T: IntoIterator<Item = Lit>>(&mut self, iter: T)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

🔬This is a nightly-only experimental API. (extend_one)

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

🔬This is a nightly-only experimental API. (extend_one)

Reserves capacity in a collection for the given number of additional elements.

impl<CE> Extend<Lit> for Inverted<CE>

where CE: Encode + Extend<Lit> + 'static,

fn extend<T: IntoIterator<Item = Lit>>(&mut self, iter: T)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

🔬This is a nightly-only experimental API. (extend_one)

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

🔬This is a nightly-only experimental API. (extend_one)

Reserves capacity in a collection for the given number of additional elements.

impl Extend<Lit> for Pairwise

fn extend<T: IntoIterator<Item = Lit>>(&mut self, iter: T)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

🔬This is a nightly-only experimental API. (extend_one)

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

🔬This is a nightly-only experimental API. (extend_one)

Reserves capacity in a collection for the given number of additional elements.

impl Extend<Lit> for Totalizer

fn extend<T: IntoIterator<Item = Lit>>(&mut self, iter: T)

Extends a collection with the contents of an iterator.

fn extend_one(&mut self, item: A)

🔬This is a nightly-only experimental API. (extend_one)

Extends a collection with exactly one element.

fn extend_reserve(&mut self, additional: usize)

🔬This is a nightly-only experimental API. (extend_one)

Reserves capacity in a collection for the given number of additional elements.

impl FromIterator<Lit> for Assignment

fn from_iter<T: IntoIterator<Item = Lit>>(iter: T) -> Self

Creates a value from an iterator.

impl FromIterator<Lit> for Clause

fn from_iter<T: IntoIterator<Item = Lit>>(iter: T) -> Self

Creates a value from an iterator.

impl FromIterator<Lit> for DbTotalizer

fn from_iter<T: IntoIterator<Item = Lit>>(iter: T) -> Self

Creates a value from an iterator.

impl<UBE, LBE> FromIterator<Lit> for Double<UBE, LBE>

where UBE: BoundUpper + From<Vec<Lit>> + 'static, LBE: BoundLower + From<Vec<Lit>> + 'static,

fn from_iter<T: IntoIterator<Item = Lit>>(iter: T) -> Self

Creates a value from an iterator.

impl<CE> FromIterator<Lit> for Inverted<CE>

where CE: Encode + From<Vec<Lit>> + 'static,

fn from_iter<T: IntoIterator<Item = Lit>>(iter: T) -> Self

Creates a value from an iterator.

impl FromIterator<Lit> for Pairwise

fn from_iter<T: IntoIterator<Item = Lit>>(iter: T) -> Self

Creates a value from an iterator.

impl FromIterator<Lit> for Totalizer

fn from_iter<T: IntoIterator<Item = Lit>>(iter: T) -> Self

Creates a value from an iterator.

impl Hash for Lit

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

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 Neg for Lit

Trait implementation allowing for negating literals with the unary - operator.

type Output = Lit

The resulting type after applying the - operator.

fn neg(self) -> Lit

Performs the unary - operation.

impl Not for Lit

Trait implementation allowing for negating literals with the ! operator.

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 + PartialOrd,

Restrict a value to a certain interval.

impl PartialEq for Lit

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

This method tests for self and other values to be equal, and is used by ==.

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

This method 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

This method tests less than (for self and other) and is used by the < operator.

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

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

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

This method tests greater than (for self and other) and is used by the > operator.

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

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

impl Sub<u32> for Lit

Decrementing literals. This preserves the sign of the literal.

type Output = Lit

The resulting type after applying the - operator.

fn sub(self, rhs: u32) -> Self::Output

Performs the - operation.

impl Copy for Lit

impl Eq for Lit

impl StructuralPartialEq for Lit