Enum SatResultWithModel

pub enum SatResultWithModel<'st> {
    Unsat,
    Sat(Model<'st>),
    Unknown,
}

The satisfiability result produced by a solver, where the Sat variant carries the satisfying model as well.

Variants

Unsat

The solver produced unsat

Sat(Model<'st>)

The solver produced sat and the associated model

Unknown

The solver produced unknown

Implementations

impl<'st> SatResultWithModel<'st>

pub fn expect_sat(self) -> Result<Model<'st>, Error>

Expect the result to be sat returning the satisfying model. If not sat, returns an error.

Trait Implementations

impl<'st> Debug for SatResultWithModel<'st>

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

Formats the value using the given formatter.