Enum Solved 

pub enum Solved {
    Sat(Vec<bool>),
    Unsat(Vec<SatLit>),
}

The outcome of solve_assuming.

Variants

Sat(Vec<bool>)

Satisfiable: a full model (var -> bool).

Unsat(Vec<SatLit>)

Unsatisfiable under the assumptions: a sufficient subset of them (a core) such that cnf ∧ core is unsatisfiable. Empty means the formula is unsatisfiable regardless of the assumptions. Not guaranteed minimal.

Trait Implementations

impl Clone for Solved

fn clone(&self) -> Solved

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Solved

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

Formats the value using the given formatter.

impl Eq for Solved

impl PartialEq for Solved

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