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) & !resx;
174 Self {
175 ones: BitPlane(res1),
176 unknowns: BitPlane(resx),
177 }
178 }
179
180 pub const fn and_lattice(self, other: Self) -> Self {
182 let a0 = self.crisp_zeros();
183 let b0 = other.crisp_zeros();
184 let a1 = self.crisp_ones();
185 let b1 = other.crisp_ones();
186 let res0 = a0 | b0;
187 let res1 = a1 & b1;
188 let resx = !res0 & !res1;
189 Self {
190 ones: BitPlane(res1),
191 unknowns: BitPlane(resx),
192 }
193 }
194
195 pub const fn or_lattice(self, other: Self) -> Self {
197 let a0 = self.crisp_zeros();
198 let b0 = other.crisp_zeros();
199 let a1 = self.crisp_ones();
200 let b1 = other.crisp_ones();
201 let res1 = a1 | b1;
202 let res0 = a0 & b0;
203 let resx = !res1 & !res0;
204 Self {
205 ones: BitPlane(res1),
206 unknowns: BitPlane(resx),
207 }
208 }
209
210 pub const fn strong_add(self, other: Self, alg: Algebra) -> Self {
212 match alg {
213 Algebra::Lukasiewicz => {
215 let a0 = self.crisp_zeros();
216 let a1 = self.crisp_ones();
217 let ax = self.unknowns();
218 let b0 = other.crisp_zeros();
219 let b1 = other.crisp_ones();
220 let bx = other.unknowns();
221 let res1 = (a0 & b1) | (a1 & b0) | (a1 & b1) | (ax & bx) | (ax & b1) | (a1 & bx);
222 let res0 = a0 & b0;
223 let resx = !res1 & !res0;
224 Self {
225 ones: BitPlane(res1),
226 unknowns: BitPlane(resx),
227 }
228 }
229 Algebra::Kleene | Algebra::Bochvar => {
231 let a1 = self.crisp_ones();
232 let b1 = other.crisp_ones();
233 let res1 = a1 & b1;
234 let resx = self.unknowns() | other.unknowns();
235 let _res0 = !res1 & !resx;
236 Self {
237 ones: BitPlane(res1),
238 unknowns: BitPlane(resx),
239 }
240 }
241 }
242 }
243
244 pub const fn strong_and(self, other: Self, alg: Algebra) -> Self {
246 match alg {
247 Algebra::Lukasiewicz => {
249 let a1 = self.crisp_ones();
250 let b1 = other.crisp_ones();
251 let res1 = a1 & b1;
252 let res0 =
253 self.crisp_zeros() | other.crisp_zeros() | (self.unknowns() & other.unknowns());
254 let resx = !res1 & !res0;
255 Self {
256 ones: BitPlane(res1),
257 unknowns: BitPlane(resx),
258 }
259 }
260 Algebra::Kleene | Algebra::Bochvar => {
262 let a1 = self.crisp_ones();
263 let b1 = other.crisp_ones();
264 let res1 = a1 & b1;
265 let resx = self.unknowns() | other.unknowns();
266 let _res0 = !res1 & !resx;
267 Self {
268 ones: BitPlane(res1),
269 unknowns: BitPlane(resx),
270 }
271 }
272 }
273 }
274
275 pub const fn implies(self, other: Self, alg: Algebra) -> Self {
277 match alg {
278 Algebra::Kleene => self.not().or_lattice(other),
280 Algebra::Bochvar => {
282 let a0 = self.crisp_zeros();
283 let a1 = self.crisp_ones();
284 let b0 = other.crisp_zeros();
285 let b1 = other.crisp_ones();
286 let res1 = (a0 & (b0 | b1)) | (a1 & b1);
287 let resx = self.unknowns() | other.unknowns();
288 Self {
289 ones: BitPlane(res1),
290 unknowns: BitPlane(resx),
291 }
292 }
293 Algebra::Lukasiewicz => {
295 let a0 = self.crisp_zeros();
296 let a1 = self.crisp_ones();
297 let ax = self.unknowns();
298 let b0 = other.crisp_zeros();
299 let b1 = other.crisp_ones();
300 let bx = other.unknowns();
301 let res1 = (a0 & (b0 | bx | b1)) | (ax & (bx | b1)) | (a1 & b1);
302 let res0 = a1 & b0;
303 let resx = !res1 & !res0;
304 Self {
305 ones: BitPlane(res1),
306 unknowns: BitPlane(resx),
307 }
308 }
309 }
310 }
311
312 pub const fn equiv(self, other: Self, alg: Algebra) -> Self {
314 self.implies(other, alg).and(other.implies(self, alg), alg)
315 }
316}
317
318#[derive(Debug, Clone)]
320pub struct TruthTable {
321 pub variables: Vec<String>,
323 pub values: Vec<Ternary>,
325}
326
327impl TruthTable {
328 pub fn value_at(&self, index: usize) -> Option<Ternary> {
330 self.values.get(index).copied()
331 }
332
333 pub fn distinct_values(&self) -> Vec<Ternary> {
335 let mut seen = [false; 3];
336 for v in &self.values {
337 seen[match v {
338 Ternary::False => 0,
339 Ternary::Unknown => 1,
340 Ternary::True => 2,
341 }] = true;
342 }
343 let mut out = Vec::new();
344 if seen[0] {
345 out.push(Ternary::False);
346 }
347 if seen[1] {
348 out.push(Ternary::Unknown);
349 }
350 if seen[2] {
351 out.push(Ternary::True);
352 }
353 out
354 }
355
356 pub fn is_always_false(&self) -> bool {
358 self.values.iter().all(|v| v.is_false())
359 }
360
361 pub fn is_always_true(&self) -> bool {
363 self.values.iter().all(|v| v.is_true())
364 }
365
366 pub fn has_unknown(&self) -> bool {
368 self.values.iter().any(|v| v.is_unknown())
369 }
370}
371
372#[derive(Debug, Clone)]
374pub struct Evaluator {
375 algebra: Algebra,
376 variables: Vec<String>,
377}
378
379impl Evaluator {
380 pub fn new(algebra: Algebra) -> Self {
382 Self {
383 algebra,
384 variables: Vec::new(),
385 }
386 }
387
388 pub fn algebra(&self) -> Algebra {
390 self.algebra
391 }
392
393 pub fn variables(&self) -> &[String] {
395 &self.variables
396 }
397
398 pub fn declare(&mut self, name: impl Into<String>) -> usize {
400 let name = name.into();
401 if let Some(idx) = self.variables.iter().position(|v| *v == name) {
402 return idx;
403 }
404 self.variables.push(name);
405 self.variables.len() - 1
406 }
407
408 pub fn assignment_count(&self) -> u64 {
410 3u64.saturating_pow(self.variables.len() as u32)
411 }
412
413 pub fn chunk_planes(&self, base: u64) -> Vec<TriBit> {
419 let mut planes = Vec::with_capacity(self.variables.len());
420 for i in 0..self.variables.len() {
421 let mut ones = 0u64;
422 let mut unknowns = 0u64;
423 let pow = 3u64.saturating_pow(i as u32);
424 for bit in 0..64u32 {
425 let group = base + bit as u64;
426 let digit = (group / pow) % 3;
427 match digit {
428 1 => ones |= 1u64 << bit,
429 2 => unknowns |= 1u64 << bit,
430 _ => {}
431 }
432 }
433 planes.push(TriBit {
434 ones: BitPlane(ones),
435 unknowns: BitPlane(unknowns),
436 });
437 }
438 planes
439 }
440
441 pub fn evaluate<F>(&self, f: F) -> TruthTable
445 where
446 F: Fn(&[TriBit]) -> TriBit,
447 {
448 let total = self.assignment_count();
449 let mut values = Vec::with_capacity(total as usize);
450 let mut base = 0u64;
451 while base < total {
452 let planes = self.chunk_planes(base);
453 let res = f(&planes);
454 let take = (total - base).min(64) as u32;
455 for bit in 0..take {
456 values.push(res.get(bit));
457 }
458 base += 64;
459 }
460 TruthTable {
461 variables: self.variables.clone(),
462 values,
463 }
464 }
465}
466
467#[cfg(test)]
468mod tests {
469 use super::*;
470
471 fn tri(v: Ternary) -> TriBit {
472 TriBit::constant(v)
473 }
474
475 #[test]
476 fn not_matches_scalar() {
477 for a in Ternary::ALL {
478 assert_eq!(tri(a).not().get(0), Algebra::Kleene.not(a), "NOT {a}");
479 }
480 }
481
482 #[test]
483 fn and_or_match_scalar_for_all_algebras() {
484 for alg in Algebra::ALL {
485 for a in Ternary::ALL {
486 for b in Ternary::ALL {
487 assert_eq!(
488 tri(a).and(tri(b), alg).get(0),
489 alg.and(a, b),
490 "{alg} {a}&{b}"
491 );
492 assert_eq!(tri(a).or(tri(b), alg).get(0), alg.or(a, b), "{alg} {a}|{b}");
493 }
494 }
495 }
496 }
497
498 #[test]
499 fn strong_add_matches_scalar_for_all_algebras() {
500 for alg in Algebra::ALL {
501 for a in Ternary::ALL {
502 for b in Ternary::ALL {
503 assert_eq!(
504 tri(a).strong_add(tri(b), alg).get(0),
505 alg.strong_add(a, b),
506 "{alg} {a}+{b}"
507 );
508 }
509 }
510 }
511 }
512
513 #[test]
514 fn strong_and_matches_scalar_for_all_algebras() {
515 for alg in Algebra::ALL {
516 for a in Ternary::ALL {
517 for b in Ternary::ALL {
518 assert_eq!(
519 tri(a).strong_and(tri(b), alg).get(0),
520 alg.strong_and(a, b),
521 "{alg} {a}*{b}"
522 );
523 }
524 }
525 }
526 }
527
528 #[test]
529 fn ops_never_produce_illegal_rails() {
530 for alg in Algebra::ALL {
531 for a in Ternary::ALL {
532 for b in Ternary::ALL {
533 for r in [
534 tri(a).and(tri(b), alg),
535 tri(a).or(tri(b), alg),
536 tri(a).strong_add(tri(b), alg),
537 ] {
538 assert_eq!(r.ones.0 & r.unknowns.0, 0, "{alg} {a} {b} 产生了 (1,1)");
539 }
540 }
541 }
542 }
543 }
544
545 #[test]
546 fn implies_matches_scalar_for_all_algebras() {
547 for alg in Algebra::ALL {
548 for a in Ternary::ALL {
549 for b in Ternary::ALL {
550 assert_eq!(
551 tri(a).implies(tri(b), alg).get(0),
552 alg.implies(a, b),
553 "{alg} {a}=>{b}"
554 );
555 }
556 }
557 }
558 }
559
560 #[test]
561 fn equiv_matches_scalar_for_all_algebras() {
562 for alg in Algebra::ALL {
563 for a in Ternary::ALL {
564 for b in Ternary::ALL {
565 assert_eq!(
566 tri(a).equiv(tri(b), alg).get(0),
567 alg.equiv(a, b),
568 "{alg} {a}<=>{b}"
569 );
570 }
571 }
572 }
573 }
574
575 #[test]
576 fn bitwise_ops_agree_across_64_lanes() {
577 let mut ones = 0u64;
579 let mut unknowns = 0u64;
580 for i in 0..64u32 {
581 match i % 3 {
582 1 => ones |= 1u64 << i,
583 2 => unknowns |= 1u64 << i,
584 _ => {}
585 }
586 }
587 let t = TriBit {
588 ones: BitPlane(ones),
589 unknowns: BitPlane(unknowns),
590 };
591 let other = TriBit {
592 ones: BitPlane(0x5555_5555_5555_5555),
593 unknowns: BitPlane(0x0f0f_0f0f_0f0f_0f0f),
594 };
595 for alg in Algebra::ALL {
596 let got = t.and(other, alg);
597 for i in 0..64u32 {
598 assert_eq!(
599 got.get(i),
600 alg.and(t.get(i), other.get(i)),
601 "{alg} lane {i}"
602 );
603 }
604 }
605 }
606
607 #[test]
608 fn evaluator_covers_all_assignments() {
609 let mut ev = Evaluator::new(Algebra::Kleene);
610 ev.declare("a");
611 ev.declare("b");
612 assert_eq!(ev.assignment_count(), 9);
613 let tt = ev.evaluate(|p| p[0]);
614 assert_eq!(tt.values.len(), 9);
615 assert_eq!(tt.value_at(0), Some(Ternary::False));
617 assert_eq!(tt.value_at(1), Some(Ternary::True));
618 assert_eq!(tt.value_at(2), Some(Ternary::Unknown));
619 assert_eq!(tt.value_at(3), Some(Ternary::False));
620 }
621
622 #[test]
623 fn evaluator_spans_multiple_chunks() {
624 let mut ev = Evaluator::new(Algebra::Kleene);
626 for name in ["a", "b", "c", "d"] {
627 ev.declare(name);
628 }
629 assert_eq!(ev.assignment_count(), 81);
630 let tt = ev.evaluate(|p| p[3]);
631 assert_eq!(tt.values.len(), 81);
632 for (i, v) in tt.values.iter().enumerate() {
633 let digit = (i as u64 / 27) % 3;
634 let expect = match digit {
635 0 => Ternary::False,
636 1 => Ternary::True,
637 _ => Ternary::Unknown,
638 };
639 assert_eq!(*v, expect, "group {i}");
640 }
641 }
642}