Enum SatOutput

pub enum SatOutput {
    Unknown,
    Unsatisfiable,
    Satisfiable(Option<Vec<bool>>),
}

Sat solver output.

Variants

Unknown

Unknown satisfiability.

Unsatisfiable

Instance is unsatisfiable.

Satisfiable(Option<Vec<bool>>)

Instance is satisfiable. Possible assignment given as vector boolean values. Index in this vector is literal value. Just v[2] gets value of second variable.

Trait Implementations

impl Clone for SatOutput

fn clone(&self) -> SatOutput

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for SatOutput

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

Formats the value using the given formatter.

impl PartialEq for SatOutput

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

impl StructuralPartialEq for SatOutput