use crate::algebra::Algebra;
use crate::limits::{LimitError, Limits, checked_pow3};
use crate::value::Ternary;
#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
pub struct BitPlane(pub u64);
impl BitPlane {
pub const ZERO: Self = Self(0);
pub const ONES: Self = Self(u64::MAX);
pub const fn with_bit(bit: u32) -> Self {
Self(1u64 << (bit % 64))
}
pub const fn checked_with_bit(bit: u32) -> Option<Self> {
if bit < 64 {
Some(Self(1u64 << bit))
} else {
None
}
}
pub const fn bit(self, bit: u32) -> bool {
(self.0 >> (bit % 64)) & 1 == 1
}
pub const fn checked_bit(self, bit: u32) -> Option<bool> {
if bit < 64 {
Some((self.0 >> bit) & 1 == 1)
} else {
None
}
}
pub const fn count_ones(self) -> u32 {
self.0.count_ones()
}
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
pub struct TriBit {
pub ones: BitPlane,
pub unknowns: BitPlane,
}
impl TriBit {
pub const fn from_binary(ones: u64) -> Self {
Self {
ones: BitPlane(ones),
unknowns: BitPlane::ZERO,
}
}
pub const fn is_binary(self) -> bool {
self.unknowns.0 == 0
}
pub const fn as_binary(self) -> Option<u64> {
if self.is_binary() {
Some(self.ones.0)
} else {
None
}
}
pub const FALSE: Self = Self {
ones: BitPlane::ZERO,
unknowns: BitPlane::ZERO,
};
pub const TRUE: Self = Self {
ones: BitPlane::ONES,
unknowns: BitPlane::ZERO,
};
pub const UNKNOWN: Self = Self {
ones: BitPlane::ZERO,
unknowns: BitPlane::ONES,
};
pub const fn constant(v: Ternary) -> Self {
match v {
Ternary::False => Self::FALSE,
Ternary::Unknown => Self::UNKNOWN,
Ternary::True => Self::TRUE,
}
}
pub const fn get(self, bit: u32) -> Ternary {
if self.unknowns.bit(bit) {
Ternary::Unknown
} else if self.ones.bit(bit) {
Ternary::True
} else {
Ternary::False
}
}
pub const fn checked_get(self, bit: u32) -> Option<Ternary> {
if bit >= 64 {
return None;
}
let ones = (self.ones.0 >> bit) & 1 == 1;
let unknowns = (self.unknowns.0 >> bit) & 1 == 1;
Some(if unknowns {
Ternary::Unknown
} else if ones {
Ternary::True
} else {
Ternary::False
})
}
const fn crisp_ones(self) -> u64 {
self.ones.0 & !self.unknowns.0
}
const fn crisp_zeros(self) -> u64 {
!self.ones.0 & !self.unknowns.0
}
const fn unknowns(self) -> u64 {
self.unknowns.0
}
pub const fn not(self) -> Self {
Self {
ones: BitPlane(!self.crisp_ones() & !self.unknowns()),
unknowns: self.unknowns,
}
}
pub const fn and(self, other: Self, alg: Algebra) -> Self {
if alg.is_poisonous() {
return Self::poison_and(self, other);
}
self.and_lattice(other)
}
pub const fn or(self, other: Self, alg: Algebra) -> Self {
if alg.is_poisonous() {
return Self::poison_or(self, other);
}
self.or_lattice(other)
}
const fn poison_and(self, other: Self) -> Self {
let resx = self.unknowns() | other.unknowns();
let a1 = self.crisp_ones();
let b1 = other.crisp_ones();
let res1 = a1 & b1;
Self {
ones: BitPlane(res1),
unknowns: BitPlane(resx),
}
}
const fn poison_or(self, other: Self) -> Self {
let resx = self.unknowns() | other.unknowns();
let a1 = self.crisp_ones();
let b1 = other.crisp_ones();
let res1 = (a1 | b1) & !resx;
Self {
ones: BitPlane(res1),
unknowns: BitPlane(resx),
}
}
pub const fn and_lattice(self, other: Self) -> Self {
let a0 = self.crisp_zeros();
let b0 = other.crisp_zeros();
let a1 = self.crisp_ones();
let b1 = other.crisp_ones();
let res0 = a0 | b0;
let res1 = a1 & b1;
let resx = !res0 & !res1;
Self {
ones: BitPlane(res1),
unknowns: BitPlane(resx),
}
}
pub const fn or_lattice(self, other: Self) -> Self {
let a0 = self.crisp_zeros();
let b0 = other.crisp_zeros();
let a1 = self.crisp_ones();
let b1 = other.crisp_ones();
let res1 = a1 | b1;
let res0 = a0 & b0;
let resx = !res1 & !res0;
Self {
ones: BitPlane(res1),
unknowns: BitPlane(resx),
}
}
pub const fn strong_add(self, other: Self, alg: Algebra) -> Self {
match alg {
Algebra::Lukasiewicz => {
let a0 = self.crisp_zeros();
let a1 = self.crisp_ones();
let ax = self.unknowns();
let b0 = other.crisp_zeros();
let b1 = other.crisp_ones();
let bx = other.unknowns();
let res1 = (a0 & b1) | (a1 & b0) | (a1 & b1) | (ax & bx) | (ax & b1) | (a1 & bx);
let res0 = a0 & b0;
let resx = !res1 & !res0;
Self {
ones: BitPlane(res1),
unknowns: BitPlane(resx),
}
}
Algebra::Kleene | Algebra::Bochvar => {
let a1 = self.crisp_ones();
let b1 = other.crisp_ones();
let res1 = a1 & b1;
let resx = self.unknowns() | other.unknowns();
let _res0 = !res1 & !resx;
Self {
ones: BitPlane(res1),
unknowns: BitPlane(resx),
}
}
}
}
pub const fn strong_and(self, other: Self, alg: Algebra) -> Self {
match alg {
Algebra::Lukasiewicz => {
let a1 = self.crisp_ones();
let b1 = other.crisp_ones();
let res1 = a1 & b1;
let res0 =
self.crisp_zeros() | other.crisp_zeros() | (self.unknowns() & other.unknowns());
let resx = !res1 & !res0;
Self {
ones: BitPlane(res1),
unknowns: BitPlane(resx),
}
}
Algebra::Kleene | Algebra::Bochvar => {
let a1 = self.crisp_ones();
let b1 = other.crisp_ones();
let res1 = a1 & b1;
let resx = self.unknowns() | other.unknowns();
let _res0 = !res1 & !resx;
Self {
ones: BitPlane(res1),
unknowns: BitPlane(resx),
}
}
}
}
pub const fn implies(self, other: Self, alg: Algebra) -> Self {
match alg {
Algebra::Kleene => self.not().or_lattice(other),
Algebra::Bochvar => {
let a0 = self.crisp_zeros();
let a1 = self.crisp_ones();
let b0 = other.crisp_zeros();
let b1 = other.crisp_ones();
let res1 = (a0 & (b0 | b1)) | (a1 & b1);
let resx = self.unknowns() | other.unknowns();
Self {
ones: BitPlane(res1),
unknowns: BitPlane(resx),
}
}
Algebra::Lukasiewicz => {
let a0 = self.crisp_zeros();
let a1 = self.crisp_ones();
let ax = self.unknowns();
let b0 = other.crisp_zeros();
let b1 = other.crisp_ones();
let bx = other.unknowns();
let res1 = (a0 & (b0 | bx | b1)) | (ax & (bx | b1)) | (a1 & b1);
let res0 = a1 & b0;
let resx = !res1 & !res0;
Self {
ones: BitPlane(res1),
unknowns: BitPlane(resx),
}
}
}
}
pub const fn equiv(self, other: Self, alg: Algebra) -> Self {
self.implies(other, alg).and(other.implies(self, alg), alg)
}
}
#[derive(Debug, Clone)]
pub struct TruthTable {
pub variables: Vec<String>,
pub values: Vec<Ternary>,
}
impl TruthTable {
pub fn value_at(&self, index: usize) -> Option<Ternary> {
self.values.get(index).copied()
}
pub fn distinct_values(&self) -> Vec<Ternary> {
let mut seen = [false; 3];
for v in &self.values {
seen[match v {
Ternary::False => 0,
Ternary::Unknown => 1,
Ternary::True => 2,
}] = true;
}
let mut out = Vec::new();
if seen[0] {
out.push(Ternary::False);
}
if seen[1] {
out.push(Ternary::Unknown);
}
if seen[2] {
out.push(Ternary::True);
}
out
}
pub fn is_always_false(&self) -> bool {
self.values.iter().all(|v| v.is_false())
}
pub fn is_always_true(&self) -> bool {
self.values.iter().all(|v| v.is_true())
}
pub fn has_unknown(&self) -> bool {
self.values.iter().any(|v| v.is_unknown())
}
}
#[derive(Debug, Clone)]
pub struct Evaluator {
algebra: Algebra,
variables: Vec<String>,
}
impl Evaluator {
pub fn new(algebra: Algebra) -> Self {
Self {
algebra,
variables: Vec::new(),
}
}
pub fn algebra(&self) -> Algebra {
self.algebra
}
pub fn variables(&self) -> &[String] {
&self.variables
}
pub fn declare(&mut self, name: impl Into<String>) -> usize {
let name = name.into();
if let Some(idx) = self.variables.iter().position(|v| *v == name) {
return idx;
}
self.variables.push(name);
self.variables.len() - 1
}
pub fn assignment_count(&self) -> Result<u64, LimitError> {
checked_pow3(self.variables.len())
}
pub fn chunk_planes(&self, base: u64) -> Result<Vec<TriBit>, LimitError> {
if !base.is_multiple_of(64) {
return Err(LimitError::ChunkBase { base });
}
base.checked_add(63).ok_or(LimitError::ChunkBase { base })?;
let mut planes = Vec::with_capacity(self.variables.len());
for i in 0..self.variables.len() {
let pow = checked_pow3(i)?;
let mut ones = 0u64;
let mut unknowns = 0u64;
for bit in 0..64u32 {
let group = base + bit as u64;
let digit = (group / pow) % 3;
match digit {
1 => ones |= 1u64 << bit,
2 => unknowns |= 1u64 << bit,
_ => {}
}
}
planes.push(TriBit {
ones: BitPlane(ones),
unknowns: BitPlane(unknowns),
});
}
Ok(planes)
}
pub fn evaluate<F>(&self, f: F) -> Result<TruthTable, LimitError>
where
F: Fn(&[TriBit]) -> TriBit,
{
self.evaluate_within(f, Limits::default())
}
pub fn evaluate_within<F>(&self, f: F, limits: Limits) -> Result<TruthTable, LimitError>
where
F: Fn(&[TriBit]) -> TriBit,
{
if self.variables.len() > limits.max_vars {
return Err(LimitError::Vars {
limit: limits.max_vars,
});
}
let total = self.assignment_count()?;
if total > limits.max_rows as u64 {
return Err(LimitError::Rows {
limit: limits.max_rows,
});
}
let capacity = usize::try_from(total).map_err(|_| LimitError::Rows {
limit: limits.max_rows,
})?;
let mut values = Vec::with_capacity(capacity);
let mut base = 0u64;
while base < total {
let planes = self.chunk_planes(base)?;
let res = f(&planes);
let take = (total - base).min(64) as u32;
for bit in 0..take {
values.push(res.get(bit));
}
base += 64;
}
Ok(TruthTable {
variables: self.variables.clone(),
values,
})
}
}
#[cfg(test)]
mod tests {
use super::*;
fn tri(v: Ternary) -> TriBit {
TriBit::constant(v)
}
#[test]
fn not_matches_scalar() {
for a in Ternary::ALL {
assert_eq!(tri(a).not().get(0), Algebra::Kleene.not(a), "NOT {a}");
}
}
#[test]
fn and_or_match_scalar_for_all_algebras() {
for alg in Algebra::ALL {
for a in Ternary::ALL {
for b in Ternary::ALL {
assert_eq!(
tri(a).and(tri(b), alg).get(0),
alg.and(a, b),
"{alg} {a}&{b}"
);
assert_eq!(tri(a).or(tri(b), alg).get(0), alg.or(a, b), "{alg} {a}|{b}");
}
}
}
}
#[test]
fn strong_add_matches_scalar_for_all_algebras() {
for alg in Algebra::ALL {
for a in Ternary::ALL {
for b in Ternary::ALL {
assert_eq!(
tri(a).strong_add(tri(b), alg).get(0),
alg.strong_add(a, b),
"{alg} {a}+{b}"
);
}
}
}
}
#[test]
fn strong_and_matches_scalar_for_all_algebras() {
for alg in Algebra::ALL {
for a in Ternary::ALL {
for b in Ternary::ALL {
assert_eq!(
tri(a).strong_and(tri(b), alg).get(0),
alg.strong_and(a, b),
"{alg} {a}*{b}"
);
}
}
}
}
#[test]
fn ops_never_produce_illegal_rails() {
for alg in Algebra::ALL {
for a in Ternary::ALL {
for b in Ternary::ALL {
for r in [
tri(a).and(tri(b), alg),
tri(a).or(tri(b), alg),
tri(a).strong_add(tri(b), alg),
] {
assert_eq!(r.ones.0 & r.unknowns.0, 0, "{alg} {a} {b} 产生了 (1,1)");
}
}
}
}
}
#[test]
fn implies_matches_scalar_for_all_algebras() {
for alg in Algebra::ALL {
for a in Ternary::ALL {
for b in Ternary::ALL {
assert_eq!(
tri(a).implies(tri(b), alg).get(0),
alg.implies(a, b),
"{alg} {a}=>{b}"
);
}
}
}
}
#[test]
fn equiv_matches_scalar_for_all_algebras() {
for alg in Algebra::ALL {
for a in Ternary::ALL {
for b in Ternary::ALL {
assert_eq!(
tri(a).equiv(tri(b), alg).get(0),
alg.equiv(a, b),
"{alg} {a}<=>{b}"
);
}
}
}
}
#[test]
fn bitwise_ops_agree_across_64_lanes() {
let mut ones = 0u64;
let mut unknowns = 0u64;
for i in 0..64u32 {
match i % 3 {
1 => ones |= 1u64 << i,
2 => unknowns |= 1u64 << i,
_ => {}
}
}
let t = TriBit {
ones: BitPlane(ones),
unknowns: BitPlane(unknowns),
};
let other = TriBit {
ones: BitPlane(0x5555_5555_5555_5555),
unknowns: BitPlane(0x0f0f_0f0f_0f0f_0f0f),
};
for alg in Algebra::ALL {
let got = t.and(other, alg);
for i in 0..64u32 {
assert_eq!(
got.get(i),
alg.and(t.get(i), other.get(i)),
"{alg} lane {i}"
);
}
}
}
#[test]
fn evaluator_covers_all_assignments() {
let mut ev = Evaluator::new(Algebra::Kleene);
ev.declare("a");
ev.declare("b");
assert_eq!(ev.assignment_count().unwrap(), 9);
let tt = ev.evaluate(|p| p[0]).unwrap();
assert_eq!(tt.values.len(), 9);
assert_eq!(tt.value_at(0), Some(Ternary::False));
assert_eq!(tt.value_at(1), Some(Ternary::True));
assert_eq!(tt.value_at(2), Some(Ternary::Unknown));
assert_eq!(tt.value_at(3), Some(Ternary::False));
}
#[test]
fn assignment_count_is_checked_not_saturated() {
let mut ev = Evaluator::new(Algebra::Kleene);
for i in 0..41 {
ev.declare(format!("v{i}"));
}
assert_eq!(
ev.assignment_count().unwrap_err(),
LimitError::CountOverflow { vars: 41 }
);
}
#[test]
fn chunk_base_must_be_aligned_and_not_overflow() {
let mut ev = Evaluator::new(Algebra::Kleene);
ev.declare("a");
assert_eq!(
ev.chunk_planes(1).unwrap_err(),
LimitError::ChunkBase { base: 1 }
);
assert!(matches!(
ev.chunk_planes(u64::MAX - 1).unwrap_err(),
LimitError::ChunkBase { .. }
));
assert!(ev.chunk_planes(0).is_ok());
}
#[test]
fn evaluate_enforces_row_budget_before_allocating() {
let mut ev = Evaluator::new(Algebra::Kleene);
ev.declare("a");
let limits = Limits {
max_rows: 2,
..Limits::default()
};
assert_eq!(
ev.evaluate_within(|p| p[0], limits).unwrap_err(),
LimitError::Rows { limit: 2 }
);
}
#[test]
fn evaluate_within_enforces_var_budget_directly() {
let mut ev = Evaluator::new(Algebra::Kleene);
for i in 0..13 {
ev.declare(format!("v{i}"));
}
let limits = Limits {
max_vars: 12,
..Limits::default()
};
assert_eq!(
ev.evaluate_within(|_| TriBit::FALSE, limits).unwrap_err(),
LimitError::Vars { limit: 12 }
);
}
#[test]
fn bit_plane_checked_access_rejects_lane_overflow() {
let plane = BitPlane::with_bit(3);
assert_eq!(BitPlane::checked_with_bit(64), None);
assert_eq!(plane.checked_bit(3), Some(true));
assert_eq!(plane.checked_bit(64), None);
assert_eq!(BitPlane::with_bit(64), BitPlane::with_bit(0));
let tri = TriBit::from_binary(0b1);
assert_eq!(tri.checked_get(0), Some(Ternary::True));
assert_eq!(tri.checked_get(64), None);
}
#[test]
fn checked_bit_access_covers_all_boundaries() {
for bit in [0u32, 63] {
assert_eq!(BitPlane::checked_with_bit(bit), Some(BitPlane(1u64 << bit)));
}
for bit in [64u32, 65, u32::MAX] {
assert_eq!(BitPlane::checked_with_bit(bit), None);
assert_eq!(BitPlane::ONES.checked_bit(bit), None);
}
assert_eq!(BitPlane::ONES.checked_bit(63), Some(true));
}
#[test]
fn evaluator_with_zero_variables_has_one_row() {
let ev = Evaluator::new(Algebra::Kleene);
assert_eq!(ev.assignment_count().unwrap(), 1);
let tt = ev.evaluate(|_| TriBit::TRUE).unwrap();
assert!(tt.variables.is_empty());
assert_eq!(tt.values, vec![Ternary::True]);
}
#[test]
fn evaluator_spans_multiple_chunks() {
let mut ev = Evaluator::new(Algebra::Kleene);
for name in ["a", "b", "c", "d"] {
ev.declare(name);
}
assert_eq!(ev.assignment_count().unwrap(), 81);
let tt = ev.evaluate(|p| p[3]).unwrap();
assert_eq!(tt.values.len(), 81);
for (i, v) in tt.values.iter().enumerate() {
let digit = (i as u64 / 27) % 3;
let expect = match digit {
0 => Ternary::False,
1 => Ternary::True,
_ => Ternary::Unknown,
};
assert_eq!(*v, expect, "group {i}");
}
}
}