1use crate::algebra::Algebra;
14use crate::value::Ternary;
15
16#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
18pub struct BitPlane(pub u64);
19
20impl BitPlane {
21 pub const ZERO: Self = Self(0);
23 pub const ONES: Self = Self(u64::MAX);
25
26 pub const fn with_bit(bit: u32) -> Self {
28 Self(1u64 << (bit % 64))
29 }
30
31 pub const fn bit(self, bit: u32) -> bool {
33 (self.0 >> (bit % 64)) & 1 == 1
34 }
35
36 pub const fn count_ones(self) -> u32 {
38 self.0.count_ones()
39 }
40}
41
42#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
44pub struct TriBit {
45 pub ones: BitPlane,
47 pub unknowns: BitPlane,
49}
50
51impl TriBit {
52 pub const fn from_binary(ones: u64) -> Self {
56 Self {
57 ones: BitPlane(ones),
58 unknowns: BitPlane::ZERO,
59 }
60 }
61
62 pub const fn is_binary(self) -> bool {
64 self.unknowns.0 == 0
65 }
66
67 pub const fn as_binary(self) -> Option<u64> {
69 if self.is_binary() {
70 Some(self.ones.0)
71 } else {
72 None
73 }
74 }
75
76 pub const FALSE: Self = Self {
78 ones: BitPlane::ZERO,
79 unknowns: BitPlane::ZERO,
80 };
81 pub const TRUE: Self = Self {
83 ones: BitPlane::ONES,
84 unknowns: BitPlane::ZERO,
85 };
86 pub const UNKNOWN: Self = Self {
88 ones: BitPlane::ZERO,
89 unknowns: BitPlane::ONES,
90 };
91
92 pub const fn constant(v: Ternary) -> Self {
94 match v {
95 Ternary::False => Self::FALSE,
96 Ternary::Unknown => Self::UNKNOWN,
97 Ternary::True => Self::TRUE,
98 }
99 }
100
101 pub const fn get(self, bit: u32) -> Ternary {
103 if self.unknowns.bit(bit) {
104 Ternary::Unknown
105 } else if self.ones.bit(bit) {
106 Ternary::True
107 } else {
108 Ternary::False
109 }
110 }
111
112 const fn crisp_ones(self) -> u64 {
114 self.ones.0 & !self.unknowns.0
115 }
116
117 const fn crisp_zeros(self) -> u64 {
119 !self.ones.0 & !self.unknowns.0
120 }
121
122 const fn unknowns(self) -> u64 {
124 self.unknowns.0
125 }
126
127 pub const fn not(self) -> Self {
129 Self {
130 ones: BitPlane(!self.crisp_ones() & !self.unknowns()),
131 unknowns: self.unknowns,
132 }
133 }
134
135 pub const fn and(self, other: Self, alg: Algebra) -> Self {
139 if alg.is_poisonous() {
140 return Self::poison_and(self, other);
141 }
142 self.and_lattice(other)
143 }
144
145 pub const fn or(self, other: Self, alg: Algebra) -> Self {
149 if alg.is_poisonous() {
150 return Self::poison_or(self, other);
151 }
152 self.or_lattice(other)
153 }
154
155 const fn poison_and(self, other: Self) -> Self {
157 let resx = self.unknowns() | other.unknowns();
158 let a1 = self.crisp_ones();
159 let b1 = other.crisp_ones();
160 let res1 = a1 & b1;
161 Self {
162 ones: BitPlane(res1),
163 unknowns: BitPlane(resx),
164 }
165 }
166
167 const fn poison_or(self, other: Self) -> Self {
169 let resx = self.unknowns() | other.unknowns();
170 let a1 = self.crisp_ones();
171 let b1 = other.crisp_ones();
172 let res1 = a1 | b1;
173 Self {
174 ones: BitPlane(res1),
175 unknowns: BitPlane(resx),
176 }
177 }
178
179 pub const fn and_lattice(self, other: Self) -> Self {
181 let a0 = self.crisp_zeros();
182 let b0 = other.crisp_zeros();
183 let a1 = self.crisp_ones();
184 let b1 = other.crisp_ones();
185 let res0 = a0 | b0;
186 let res1 = a1 & b1;
187 let resx = !res0 & !res1;
188 Self {
189 ones: BitPlane(res1),
190 unknowns: BitPlane(resx),
191 }
192 }
193
194 pub const fn or_lattice(self, other: Self) -> Self {
196 let a0 = self.crisp_zeros();
197 let b0 = other.crisp_zeros();
198 let a1 = self.crisp_ones();
199 let b1 = other.crisp_ones();
200 let res1 = a1 | b1;
201 let res0 = a0 & b0;
202 let resx = !res1 & !res0;
203 Self {
204 ones: BitPlane(res1),
205 unknowns: BitPlane(resx),
206 }
207 }
208
209 pub const fn strong_add(self, other: Self, alg: Algebra) -> Self {
211 match alg {
212 Algebra::Lukasiewicz => {
214 let a0 = self.crisp_zeros();
215 let a1 = self.crisp_ones();
216 let ax = self.unknowns();
217 let b0 = other.crisp_zeros();
218 let b1 = other.crisp_ones();
219 let bx = other.unknowns();
220 let res1 = (a0 & b1) | (a1 & b0) | (a1 & b1) | (ax & bx) | (ax & b1) | (a1 & bx);
221 let res0 = a0 & b0;
222 let resx = !res1 & !res0;
223 Self {
224 ones: BitPlane(res1),
225 unknowns: BitPlane(resx),
226 }
227 }
228 Algebra::Kleene | Algebra::Bochvar => {
230 let a1 = self.crisp_ones();
231 let b1 = other.crisp_ones();
232 let res1 = a1 & b1;
233 let resx = self.unknowns() | other.unknowns();
234 let _res0 = !res1 & !resx;
235 Self {
236 ones: BitPlane(res1),
237 unknowns: BitPlane(resx),
238 }
239 }
240 }
241 }
242
243 pub const fn strong_and(self, other: Self, alg: Algebra) -> Self {
245 match alg {
246 Algebra::Lukasiewicz => {
248 let a1 = self.crisp_ones();
249 let b1 = other.crisp_ones();
250 let res1 = a1 & b1;
251 let res0 =
252 self.crisp_zeros() | other.crisp_zeros() | (self.unknowns() & other.unknowns());
253 let resx = !res1 & !res0;
254 Self {
255 ones: BitPlane(res1),
256 unknowns: BitPlane(resx),
257 }
258 }
259 Algebra::Kleene | Algebra::Bochvar => {
261 let a1 = self.crisp_ones();
262 let b1 = other.crisp_ones();
263 let res1 = a1 & b1;
264 let resx = self.unknowns() | other.unknowns();
265 let _res0 = !res1 & !resx;
266 Self {
267 ones: BitPlane(res1),
268 unknowns: BitPlane(resx),
269 }
270 }
271 }
272 }
273
274 pub const fn implies(self, other: Self, alg: Algebra) -> Self {
276 match alg {
277 Algebra::Kleene => self.not().or_lattice(other),
279 Algebra::Bochvar => {
281 let a0 = self.crisp_zeros();
282 let a1 = self.crisp_ones();
283 let b0 = other.crisp_zeros();
284 let b1 = other.crisp_ones();
285 let res1 = (a0 & (b0 | b1)) | (a1 & b1);
286 let resx = self.unknowns() | other.unknowns();
287 Self {
288 ones: BitPlane(res1),
289 unknowns: BitPlane(resx),
290 }
291 }
292 Algebra::Lukasiewicz => {
294 let a0 = self.crisp_zeros();
295 let a1 = self.crisp_ones();
296 let ax = self.unknowns();
297 let b0 = other.crisp_zeros();
298 let b1 = other.crisp_ones();
299 let bx = other.unknowns();
300 let res1 = (a0 & (b0 | bx | b1)) | (ax & (bx | b1)) | (a1 & b1);
301 let res0 = a1 & b0;
302 let resx = !res1 & !res0;
303 Self {
304 ones: BitPlane(res1),
305 unknowns: BitPlane(resx),
306 }
307 }
308 }
309 }
310
311 pub const fn equiv(self, other: Self, alg: Algebra) -> Self {
313 self.implies(other, alg).and(other.implies(self, alg), alg)
314 }
315}
316
317#[derive(Debug, Clone)]
319pub struct TruthTable {
320 pub variables: Vec<String>,
322 pub values: Vec<Ternary>,
324}
325
326impl TruthTable {
327 pub fn value_at(&self, index: usize) -> Option<Ternary> {
329 self.values.get(index).copied()
330 }
331
332 pub fn distinct_values(&self) -> Vec<Ternary> {
334 let mut seen = [false; 3];
335 for v in &self.values {
336 seen[match v {
337 Ternary::False => 0,
338 Ternary::Unknown => 1,
339 Ternary::True => 2,
340 }] = true;
341 }
342 let mut out = Vec::new();
343 if seen[0] {
344 out.push(Ternary::False);
345 }
346 if seen[1] {
347 out.push(Ternary::Unknown);
348 }
349 if seen[2] {
350 out.push(Ternary::True);
351 }
352 out
353 }
354
355 pub fn is_always_false(&self) -> bool {
357 self.values.iter().all(|v| v.is_false())
358 }
359
360 pub fn is_always_true(&self) -> bool {
362 self.values.iter().all(|v| v.is_true())
363 }
364
365 pub fn has_unknown(&self) -> bool {
367 self.values.iter().any(|v| v.is_unknown())
368 }
369}
370
371#[derive(Debug, Clone)]
373pub struct Evaluator {
374 algebra: Algebra,
375 variables: Vec<String>,
376}
377
378impl Evaluator {
379 pub fn new(algebra: Algebra) -> Self {
381 Self {
382 algebra,
383 variables: Vec::new(),
384 }
385 }
386
387 pub fn algebra(&self) -> Algebra {
389 self.algebra
390 }
391
392 pub fn variables(&self) -> &[String] {
394 &self.variables
395 }
396
397 pub fn declare(&mut self, name: impl Into<String>) -> usize {
399 let name = name.into();
400 if let Some(idx) = self.variables.iter().position(|v| *v == name) {
401 return idx;
402 }
403 self.variables.push(name);
404 self.variables.len() - 1
405 }
406
407 pub fn assignment_count(&self) -> u64 {
409 3u64.saturating_pow(self.variables.len() as u32)
410 }
411
412 pub fn chunk_planes(&self, base: u64) -> Vec<TriBit> {
418 let mut planes = Vec::with_capacity(self.variables.len());
419 for i in 0..self.variables.len() {
420 let mut ones = 0u64;
421 let mut unknowns = 0u64;
422 let pow = 3u64.saturating_pow(i as u32);
423 for bit in 0..64u32 {
424 let group = base + bit as u64;
425 let digit = (group / pow) % 3;
426 match digit {
427 1 => ones |= 1u64 << bit,
428 2 => unknowns |= 1u64 << bit,
429 _ => {}
430 }
431 }
432 planes.push(TriBit {
433 ones: BitPlane(ones),
434 unknowns: BitPlane(unknowns),
435 });
436 }
437 planes
438 }
439
440 pub fn evaluate<F>(&self, f: F) -> TruthTable
444 where
445 F: Fn(&[TriBit]) -> TriBit,
446 {
447 let total = self.assignment_count();
448 let mut values = Vec::with_capacity(total as usize);
449 let mut base = 0u64;
450 while base < total {
451 let planes = self.chunk_planes(base);
452 let res = f(&planes);
453 let take = (total - base).min(64) as u32;
454 for bit in 0..take {
455 values.push(res.get(bit));
456 }
457 base += 64;
458 }
459 TruthTable {
460 variables: self.variables.clone(),
461 values,
462 }
463 }
464}
465
466#[cfg(test)]
467mod tests {
468 use super::*;
469
470 fn tri(v: Ternary) -> TriBit {
471 TriBit::constant(v)
472 }
473
474 #[test]
475 fn not_matches_scalar() {
476 for a in Ternary::ALL {
477 assert_eq!(tri(a).not().get(0), Algebra::Kleene.not(a), "NOT {a}");
478 }
479 }
480
481 #[test]
482 fn and_or_match_scalar_for_all_algebras() {
483 for alg in Algebra::ALL {
484 for a in Ternary::ALL {
485 for b in Ternary::ALL {
486 assert_eq!(
487 tri(a).and(tri(b), alg).get(0),
488 alg.and(a, b),
489 "{alg} {a}&{b}"
490 );
491 assert_eq!(tri(a).or(tri(b), alg).get(0), alg.or(a, b), "{alg} {a}|{b}");
492 }
493 }
494 }
495 }
496
497 #[test]
498 fn strong_add_matches_scalar_for_all_algebras() {
499 for alg in Algebra::ALL {
500 for a in Ternary::ALL {
501 for b in Ternary::ALL {
502 assert_eq!(
503 tri(a).strong_add(tri(b), alg).get(0),
504 alg.strong_add(a, b),
505 "{alg} {a}+{b}"
506 );
507 }
508 }
509 }
510 }
511
512 #[test]
513 fn strong_and_matches_scalar_for_all_algebras() {
514 for alg in Algebra::ALL {
515 for a in Ternary::ALL {
516 for b in Ternary::ALL {
517 assert_eq!(
518 tri(a).strong_and(tri(b), alg).get(0),
519 alg.strong_and(a, b),
520 "{alg} {a}*{b}"
521 );
522 }
523 }
524 }
525 }
526
527 #[test]
528 fn implies_matches_scalar_for_all_algebras() {
529 for alg in Algebra::ALL {
530 for a in Ternary::ALL {
531 for b in Ternary::ALL {
532 assert_eq!(
533 tri(a).implies(tri(b), alg).get(0),
534 alg.implies(a, b),
535 "{alg} {a}=>{b}"
536 );
537 }
538 }
539 }
540 }
541
542 #[test]
543 fn equiv_matches_scalar_for_all_algebras() {
544 for alg in Algebra::ALL {
545 for a in Ternary::ALL {
546 for b in Ternary::ALL {
547 assert_eq!(
548 tri(a).equiv(tri(b), alg).get(0),
549 alg.equiv(a, b),
550 "{alg} {a}<=>{b}"
551 );
552 }
553 }
554 }
555 }
556
557 #[test]
558 fn bitwise_ops_agree_across_64_lanes() {
559 let mut ones = 0u64;
561 let mut unknowns = 0u64;
562 for i in 0..64u32 {
563 match i % 3 {
564 1 => ones |= 1u64 << i,
565 2 => unknowns |= 1u64 << i,
566 _ => {}
567 }
568 }
569 let t = TriBit {
570 ones: BitPlane(ones),
571 unknowns: BitPlane(unknowns),
572 };
573 let other = TriBit {
574 ones: BitPlane(0x5555_5555_5555_5555),
575 unknowns: BitPlane(0x0f0f_0f0f_0f0f_0f0f),
576 };
577 for alg in Algebra::ALL {
578 let got = t.and(other, alg);
579 for i in 0..64u32 {
580 assert_eq!(
581 got.get(i),
582 alg.and(t.get(i), other.get(i)),
583 "{alg} lane {i}"
584 );
585 }
586 }
587 }
588
589 #[test]
590 fn evaluator_covers_all_assignments() {
591 let mut ev = Evaluator::new(Algebra::Kleene);
592 ev.declare("a");
593 ev.declare("b");
594 assert_eq!(ev.assignment_count(), 9);
595 let tt = ev.evaluate(|p| p[0]);
596 assert_eq!(tt.values.len(), 9);
597 assert_eq!(tt.value_at(0), Some(Ternary::False));
599 assert_eq!(tt.value_at(1), Some(Ternary::True));
600 assert_eq!(tt.value_at(2), Some(Ternary::Unknown));
601 assert_eq!(tt.value_at(3), Some(Ternary::False));
602 }
603
604 #[test]
605 fn evaluator_spans_multiple_chunks() {
606 let mut ev = Evaluator::new(Algebra::Kleene);
608 for name in ["a", "b", "c", "d"] {
609 ev.declare(name);
610 }
611 assert_eq!(ev.assignment_count(), 81);
612 let tt = ev.evaluate(|p| p[3]);
613 assert_eq!(tt.values.len(), 81);
614 for (i, v) in tt.values.iter().enumerate() {
615 let digit = (i as u64 / 27) % 3;
616 let expect = match digit {
617 0 => Ternary::False,
618 1 => Ternary::True,
619 _ => Ternary::Unknown,
620 };
621 assert_eq!(*v, expect, "group {i}");
622 }
623 }
624}