tiny.smt.BoolValue

1/// A truth value that may also be unset. A caller switches on the value `Solver.literalValue`2/// returns to read a literal in a satisfying assignment.3pub const BoolValue = enum {4    /// The variable is unassigned, or the literal names a variable at or above the solver's5    /// variable count.6    unset,7    /// The literal or variable is false.8    false,9    /// The literal or variable is true.10    true,1112    /// Returns `.true` for true and `.false` for false. The solver and the proof checker record an13    /// assigned value through it.14    pub fn fromBool(value: bool) BoolValue {15        return if (value) .true else .false;16    }1718    /// Returns the opposite value, and `.unset` for `.unset`. The solver and the proof checker read19    /// a negated literal's value from its variable's value through it.20    pub fn invert(self: BoolValue) BoolValue {21        return switch (self) {22            .unset => .unset,23            .false => .true,24            .true => .false,25        };26    }27};

1pub const BoolValue = sat.BoolValue;