Enum ModelOutcome 

pub enum ModelOutcome {
    Sat(Vec<(String, bool)>),
    Unsat,
    Unsupported,
}

The result of a satisfiability query over a propositional obligation.

Variants

Sat(Vec<(String, bool)>)

Satisfiable, with a model over the source atoms (sorted by name). For a hardware obligation these are the signal@t bindings of a witnessing trace.

Unsat

Unsatisfiable — no assignment satisfies the obligation.

Unsupported

Not a quantifier-free propositional formula over recognisable atoms, so the SAT engine cannot speak to it (the caller must escalate, e.g. bit-blast first).

Trait Implementations

impl Clone for ModelOutcome

fn clone(&self) -> ModelOutcome

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ModelOutcome

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

Formats the value using the given formatter.

impl PartialEq for ModelOutcome

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

impl StructuralPartialEq for ModelOutcome