Struct Lit

pub struct Lit { /* private fields */ }

Type representing literals, possibly negated boolean variables.

Representation in Memory

Literal representation is idx << 1 with the last bit representing whether the literal is negated or not. This way the literal can directly be used to index data structures with the two literals of a variable being close together.

Implementations

impl Lit

pub const 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.

Errors

TypeError::IdxTooHigh(idx, Var::MAX_IDX) if idx > Var::MAX_IDX.

pub const unsafe 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.

Safety

idx must be guaranteed to be not higher than Var::MAX_IDX

pub const fn positive(idx: u32) -> Lit

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

pub const 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.

Errors

If idx > Var::MAX_IDX.

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

Creates a new negated literal with a given index.

Errors

If idx > Var::MAX_IDX.

pub const unsafe 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.

Safety

idx must be guaranteed to be not higher than Var::MAX_IDX

pub const unsafe 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.

Safety

idx must be guaranteed to be not higher than Var::MAX_IDX

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

Create a literal from an IPASIR/DIMACS integer value.

Errors

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 32-bit 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());

Examples found in repository

examples/profiling.rs (line 72)

fn build_full_ub<PBE: BoundUpper + FromIterator<(Lit, usize)>>(lits: &[(Lit, usize)]) {
    let mut enc = PBE::from_iter(lits.iter().copied());
    let max_var = lits
        .iter()
        .fold(Var::new(0), |mv, (lit, _)| std::cmp::max(lit.var(), mv));
    let mut var_manager = BasicVarManager::default();
    var_manager.increase_next_free(max_var + 1);
    let mut collector = Cnf::new();
    enc.encode_ub(.., &mut collector, &mut var_manager).unwrap();
}

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 IPASIR and the DIMACS file format. 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.

Panics

If the variable index does not fit in c_int. As c_int will almost always be i32, this is only the case on very esoteric platforms.

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

Converts the literal to an integer as accepted by IPASIR and the DIMACS file format. The IPASIR literal will have idx+1 and be negative if the literal is negated.

Errors

TypeError::IdxTooHigh(_, _) if the literal does not fit into a c_int. As c_int will almost always be i32, it is mostly safe to simply use Self::to_ipasir instead.

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 duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lit

Literals can be printed with the Debug trait

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Lit

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

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<const N: usize, Sub> Extend<Lit> for Bimander<N, Sub>

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 Bitwise

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 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<const N: usize, Sub> Extend<Lit> for Commander<N, Sub>

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 Ladder

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 From<Lit> for Axiom<Var>

Available on crate feature proof-logging only.

fn from(value: Lit) -> Self

Converts to this type from the input type.

impl FromIterator<Lit> for Assignment

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

Creates a value from an iterator.

impl<const N: usize, Sub> FromIterator<Lit> for Bimander<N, Sub>

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

Creates a value from an iterator.

impl FromIterator<Lit> for Bitwise

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<const N: usize, Sub> FromIterator<Lit> for Commander<N, Sub>

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 Ladder

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,

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

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

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