tiny.smt.Status

1/// The answer of one solve. A caller switches on it to decide whether to read a satisfying2/// assignment, an unsat core and a proof, or neither.3pub const Status = enum {4    /// Some assignment makes every clause and every assumption of the solve true. `Solver.value`5    /// and `Solver.literalValue` read that assignment until the next solve.6    sat,7    /// No assignment makes every clause and every assumption of the solve true. The solver then8    /// holds a proof trace that ends in the empty clause, and after a solve under assumptions an9    /// unsat core.10    unsat,11    /// The solve ran out of its conflict limit (`Solver.conflict_budget`) before it reached an12    /// answer, or while core minimization certified a smaller core. After the second case the core13    /// is empty, but the proof trace still holds a refutation under every assumption of the solve.14    unknown,15};

1pub const Status = sat.Status;