Struct Reason

pub struct Reason(/* private fields */);

The reason for assigning a literal

A literal can be assumed, or forced by some clause. The clause is stored as offset to reduce the number of indirections in propagate.

This is essentially this enum, but we pack everything into size_of::<usize>() bits.

enum Reason {
    Assumed,
    Forced(usize),
}

Implementations

impl Reason

pub fn invalid() -> Reason

Create an invalid reason, i.e. for unassigned literals.

pub fn assumed() -> Reason

Create a reason for assumed literals.

pub fn forced(offset: usize) -> Reason

Create a reason for a clause that has been forced by the clause with the given offset.

pub fn is_assumed(self) -> bool

Return true when this is an assumption.

pub fn offset(self) -> usize

Return the offset of the clause. Only valid if this is not an assumption or invalid.

Trait Implementations

impl Clone for Reason

fn clone(&self) -> Reason

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Reason

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

Formats the value using the given formatter.

impl Default for Reason

fn default() -> Reason

Returns the “default value” for a type.

impl Display for Reason

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

Formats the value using the given formatter.

impl PartialEq for Reason

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

impl Eq for Reason

impl StructuralPartialEq for Reason