Enum SatisfiabilityResult 

pub enum SatisfiabilityResult {
    Satisfiable,
    Unsatisfiable {
        mus: Vec<usize>,
    },
    Unknown,
}

Whether the conjunction of all formulas is satisfiable.

Variants

Satisfiable

All formulas can hold simultaneously.

Unsatisfiable

The formulas are contradictory. mus contains the indices of the Minimal Unsatisfiable Subset.

Fields

mus: Vec<usize>

Unknown

Z3 returned unknown (timeout or undecidable).

Trait Implementations

impl Debug for SatisfiabilityResult

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

Formats the value using the given formatter.

impl PartialEq for SatisfiabilityResult

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