elenchus_solver/v3.rs
1//! The three-valued Kleene truth value used throughout the forward pass.
2use elenchus_compiler::Value;
3
4/// Three-valued truth (Kleene). UNKNOWN is a first-class value, not hidden FALSE.
5#[derive(Debug, Clone, Copy, PartialEq, Eq)]
6pub enum V3 {
7 /// Known true.
8 True,
9 /// Known false.
10 False,
11 /// Not asserted and not derivable — the absence of information, not falsity.
12 Unknown,
13}
14
15impl V3 {
16 /// Kleene negation: TRUE↔FALSE, and UNKNOWN stays UNKNOWN.
17 pub(crate) fn not(self) -> V3 {
18 match self {
19 V3::True => V3::False,
20 V3::False => V3::True,
21 V3::Unknown => V3::Unknown,
22 }
23 }
24}
25
26/// Convert a three-valued model entry to a confident [`Value`] (UNKNOWN → `None`).
27pub(crate) fn v3_to_value(v: V3) -> Option<Value> {
28 match v {
29 V3::True => Some(Value::True),
30 V3::False => Some(Value::False),
31 V3::Unknown => None,
32 }
33}