Struct rate_common::clause::Reason

pub struct Reason(_);

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),
}

Methods

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 Copy for Reason

impl Default for Reason

fn default() -> Reason

Returns the "default value" for a type.

impl Eq for Reason

impl PartialEq<Reason> for Reason

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

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

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

This method tests for !=.

impl Display for Reason

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

Formats the value using the given formatter.

impl Debug for Reason

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

Formats the value using the given formatter.