Struct Assignment

pub struct Assignment { /* private fields */ }

An assignment comprising a mapping plus a trail (vector of literals).

Note that Literal::TOP is always assigned.

It is valid to assign both a literal and its negation - this is how we detect a conflict.

Implementations

impl Assignment

pub fn new(maxvar: Variable) -> Assignment

Create an empty assignment.

pub fn len(&self) -> usize

Return the number of assigned literals.

pub fn position_in_trail(&self, literal: Literal) -> usize

Return the position in the trail where this literal was assigned.

pub fn trail_at(&self, offset: usize) -> (Literal, Reason)

Access the trail by offset.

pub fn push(&mut self, lit: Literal, reason: Reason)

Add a new literal to the trail, assigning it to true.

pub fn peek(&mut self) -> (Literal, Reason)

View the literal that was assigned last.

pub fn pop(&mut self) -> Option<(Literal, Reason)>

Unassign the literal that was assigned last.

pub fn move_to(&mut self, src: usize, dst: usize)

Move the literal at trail position src to dst.

pub fn resize(&mut self, level: usize)

Change the size of the trail. Note: this does not change the assigned values, only the trail.

pub fn unassign(&mut self, literal: Literal)

Remove the assignment for a literal, without modifying the trail.

pub fn set_trail_at(&mut self, offset: usize, literal: Literal, reason: Reason)

Insert a literal into the trail and assign it.

pub fn iter(&self) -> Iter<'_, (Literal, Reason)>

Trait Implementations

impl Clone for Assignment

fn clone(&self) -> Assignment

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Assignment

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

Formats the value using the given formatter.

impl Display for Assignment

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

Formats the value using the given formatter.

impl HeapSpace for Assignment

fn heap_space(&self) -> usize

The number of bytes allocated on the heap that this owns.

impl Index<Literal> for Assignment

type Output = bool

The returned type after indexing.

fn index(&self, literal: Literal) -> &bool

Performs the indexing (container[index]) operation.

impl<'a> IntoIterator for &'a Assignment

Iterate over the literals in the trail, from oldest to newest.

type Item = &'a (Literal, Reason)

The type of the elements being iterated over.

type IntoIter = Iter<'a, (Literal, Reason)>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl PartialEq for Assignment

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