Struct Var

pub struct Var { /* private fields */ }

Type representing boolean variables in a SAT problem. Variables indexing in RustSAT starts from 0 and the maximum index is (u32::MAX - 1) / 2. This is because literals are represented as a single u32 as well. The memory representation of variables is u32.

Implementations

impl Var

pub const MAX_IDX: u32 = 2_147_483_647u32

The maximum index that can be represented.

pub const fn new(idx: u32) -> Var

Creates a new variables with a given index. Indices start from 0.

Panics

If idx > Var::MAX_IDX.

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 new_with_error(idx: u32) -> Result<Var, TypeError>

Creates a new variables with a given index. Indices start from 0.

Errors

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

pub const unsafe fn new_unchecked(idx: u32) -> Var

Creates a new variables with a given index. Indices start from 0. 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 lit(self, negated: bool) -> Lit

Creates a literal with a given negation from the variable

Examples

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

pub const fn pos_lit(self) -> Lit

Creates a literal that is not negated.

Examples

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

pub const fn neg_lit(self) -> Lit

Creates a negated literal.

Examples

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

pub fn idx(self) -> usize

Returns the index of the variable. This is a usize to enable easier indexing of data structures like vectors, even though the internal representation of a variable is u32. For the 32 bit index use Var::idx32.

Examples

let var = Var::new(5);
assert_eq!(5, var.idx());

pub fn idx32(self) -> u32

Returns the 32 bit index of the variable.

Examples

let var = Var::new(5);
assert_eq!(5, var.idx32());

pub fn to_ipasir(self) -> c_int

Converts the variable to an integer as accepted by IPASIR and the DIMACS file format. The IPASIR variable will have idx+1.

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 variable 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 Var

Incrementing variables

type Output = Var

The resulting type after applying the + operator.

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

Performs the + operation.

impl AddAssign<u32> for Var

fn add_assign(&mut self, rhs: u32)

Performs the += operation.

impl Clone for Var

fn clone(&self) -> Var

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Var

Variables can be printed with the Debug trait

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

Formats the value using the given formatter.

impl Display for Var

Variables can be printed with the Display trait

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

Formats the value using the given formatter.

impl Hash for Var

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 Index<Var> for Assignment

type Output = TernaryVal

The returned type after indexing.

fn index(&self, index: Var) -> &Self::Output

Performs the indexing (container[index]) operation.

impl IndexMut<Var> for Assignment

fn index_mut(&mut self, index: Var) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl Ord for Var

fn cmp(&self, other: &Var) -> 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 Var

fn eq(&self, other: &Var) -> 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 Var

fn partial_cmp(&self, other: &Var) -> 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 Sub<u32> for Var

Decrementing variables

type Output = Var

The resulting type after applying the - operator.

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

Performs the - operation.

impl SubAssign<u32> for Var

fn sub_assign(&mut self, rhs: u32)

Performs the -= operation.

impl Copy for Var

impl Eq for Var

impl StructuralPartialEq for Var