1use crate::algebra::Algebra;
14use crate::limits::{LimitError, Limits, checked_pow3};
15use crate::value::Ternary;
16
17#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
19pub struct BitPlane(pub u64);
20
21impl BitPlane {
22 pub const ZERO: Self = Self(0);
24 pub const ONES: Self = Self(u64::MAX);
26
27 pub const fn with_bit(bit: u32) -> Self {
32 Self(1u64 << (bit % 64))
33 }
34
35 pub const fn checked_with_bit(bit: u32) -> Option<Self> {
37 if bit < 64 {
38 Some(Self(1u64 << bit))
39 } else {
40 None
41 }
42 }
43
44 pub const fn bit(self, bit: u32) -> bool {
48 (self.0 >> (bit % 64)) & 1 == 1
49 }
50
51 pub const fn checked_bit(self, bit: u32) -> Option<bool> {
53 if bit < 64 {
54 Some((self.0 >> bit) & 1 == 1)
55 } else {
56 None
57 }
58 }
59
60 pub const fn count_ones(self) -> u32 {
62 self.0.count_ones()
63 }
64}
65
66#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
68pub struct TriBit {
69 pub ones: BitPlane,
71 pub unknowns: BitPlane,
73}
74
75impl TriBit {
76 pub const fn from_binary(ones: u64) -> Self {
80 Self {
81 ones: BitPlane(ones),
82 unknowns: BitPlane::ZERO,
83 }
84 }
85
86 pub const fn is_binary(self) -> bool {
88 self.unknowns.0 == 0
89 }
90
91 pub const fn as_binary(self) -> Option<u64> {
93 if self.is_binary() {
94 Some(self.ones.0)
95 } else {
96 None
97 }
98 }
99
100 pub const FALSE: Self = Self {
102 ones: BitPlane::ZERO,
103 unknowns: BitPlane::ZERO,
104 };
105 pub const TRUE: Self = Self {
107 ones: BitPlane::ONES,
108 unknowns: BitPlane::ZERO,
109 };
110 pub const UNKNOWN: Self = Self {
112 ones: BitPlane::ZERO,
113 unknowns: BitPlane::ONES,
114 };
115
116 pub const fn constant(v: Ternary) -> Self {
118 match v {
119 Ternary::False => Self::FALSE,
120 Ternary::Unknown => Self::UNKNOWN,
121 Ternary::True => Self::TRUE,
122 }
123 }
124
125 pub const fn get(self, bit: u32) -> Ternary {
127 if self.unknowns.bit(bit) {
128 Ternary::Unknown
129 } else if self.ones.bit(bit) {
130 Ternary::True
131 } else {
132 Ternary::False
133 }
134 }
135
136 pub const fn checked_get(self, bit: u32) -> Option<Ternary> {
138 if bit >= 64 {
139 return None;
140 }
141 let ones = (self.ones.0 >> bit) & 1 == 1;
142 let unknowns = (self.unknowns.0 >> bit) & 1 == 1;
143 Some(if unknowns {
144 Ternary::Unknown
145 } else if ones {
146 Ternary::True
147 } else {
148 Ternary::False
149 })
150 }
151
152 const fn crisp_ones(self) -> u64 {
154 self.ones.0 & !self.unknowns.0
155 }
156
157 const fn crisp_zeros(self) -> u64 {
159 !self.ones.0 & !self.unknowns.0
160 }
161
162 const fn unknowns(self) -> u64 {
164 self.unknowns.0
165 }
166
167 pub const fn not(self) -> Self {
169 Self {
170 ones: BitPlane(!self.crisp_ones() & !self.unknowns()),
171 unknowns: self.unknowns,
172 }
173 }
174
175 pub const fn and(self, other: Self, alg: Algebra) -> Self {
179 if alg.is_poisonous() {
180 return Self::poison_and(self, other);
181 }
182 self.and_lattice(other)
183 }
184
185 pub const fn or(self, other: Self, alg: Algebra) -> Self {
189 if alg.is_poisonous() {
190 return Self::poison_or(self, other);
191 }
192 self.or_lattice(other)
193 }
194
195 const fn poison_and(self, other: Self) -> Self {
197 let resx = self.unknowns() | other.unknowns();
198 let a1 = self.crisp_ones();
199 let b1 = other.crisp_ones();
200 let res1 = a1 & b1;
201 Self {
202 ones: BitPlane(res1),
203 unknowns: BitPlane(resx),
204 }
205 }
206
207 const fn poison_or(self, other: Self) -> Self {
209 let resx = self.unknowns() | other.unknowns();
210 let a1 = self.crisp_ones();
211 let b1 = other.crisp_ones();
212 let res1 = (a1 | b1) & !resx;
214 Self {
215 ones: BitPlane(res1),
216 unknowns: BitPlane(resx),
217 }
218 }
219
220 pub const fn and_lattice(self, other: Self) -> Self {
222 let a0 = self.crisp_zeros();
223 let b0 = other.crisp_zeros();
224 let a1 = self.crisp_ones();
225 let b1 = other.crisp_ones();
226 let res0 = a0 | b0;
227 let res1 = a1 & b1;
228 let resx = !res0 & !res1;
229 Self {
230 ones: BitPlane(res1),
231 unknowns: BitPlane(resx),
232 }
233 }
234
235 pub const fn or_lattice(self, other: Self) -> Self {
237 let a0 = self.crisp_zeros();
238 let b0 = other.crisp_zeros();
239 let a1 = self.crisp_ones();
240 let b1 = other.crisp_ones();
241 let res1 = a1 | b1;
242 let res0 = a0 & b0;
243 let resx = !res1 & !res0;
244 Self {
245 ones: BitPlane(res1),
246 unknowns: BitPlane(resx),
247 }
248 }
249
250 pub const fn strong_add(self, other: Self, alg: Algebra) -> Self {
252 match alg {
253 Algebra::Lukasiewicz => {
255 let a0 = self.crisp_zeros();
256 let a1 = self.crisp_ones();
257 let ax = self.unknowns();
258 let b0 = other.crisp_zeros();
259 let b1 = other.crisp_ones();
260 let bx = other.unknowns();
261 let res1 = (a0 & b1) | (a1 & b0) | (a1 & b1) | (ax & bx) | (ax & b1) | (a1 & bx);
262 let res0 = a0 & b0;
263 let resx = !res1 & !res0;
264 Self {
265 ones: BitPlane(res1),
266 unknowns: BitPlane(resx),
267 }
268 }
269 Algebra::Kleene | Algebra::Bochvar => {
271 let a1 = self.crisp_ones();
272 let b1 = other.crisp_ones();
273 let res1 = a1 & b1;
274 let resx = self.unknowns() | other.unknowns();
275 let _res0 = !res1 & !resx;
276 Self {
277 ones: BitPlane(res1),
278 unknowns: BitPlane(resx),
279 }
280 }
281 }
282 }
283
284 pub const fn strong_and(self, other: Self, alg: Algebra) -> Self {
286 match alg {
287 Algebra::Lukasiewicz => {
289 let a1 = self.crisp_ones();
290 let b1 = other.crisp_ones();
291 let res1 = a1 & b1;
292 let res0 =
293 self.crisp_zeros() | other.crisp_zeros() | (self.unknowns() & other.unknowns());
294 let resx = !res1 & !res0;
295 Self {
296 ones: BitPlane(res1),
297 unknowns: BitPlane(resx),
298 }
299 }
300 Algebra::Kleene | Algebra::Bochvar => {
302 let a1 = self.crisp_ones();
303 let b1 = other.crisp_ones();
304 let res1 = a1 & b1;
305 let resx = self.unknowns() | other.unknowns();
306 let _res0 = !res1 & !resx;
307 Self {
308 ones: BitPlane(res1),
309 unknowns: BitPlane(resx),
310 }
311 }
312 }
313 }
314
315 pub const fn implies(self, other: Self, alg: Algebra) -> Self {
317 match alg {
318 Algebra::Kleene => self.not().or_lattice(other),
320 Algebra::Bochvar => {
322 let a0 = self.crisp_zeros();
323 let a1 = self.crisp_ones();
324 let b0 = other.crisp_zeros();
325 let b1 = other.crisp_ones();
326 let res1 = (a0 & (b0 | b1)) | (a1 & b1);
327 let resx = self.unknowns() | other.unknowns();
328 Self {
329 ones: BitPlane(res1),
330 unknowns: BitPlane(resx),
331 }
332 }
333 Algebra::Lukasiewicz => {
335 let a0 = self.crisp_zeros();
336 let a1 = self.crisp_ones();
337 let ax = self.unknowns();
338 let b0 = other.crisp_zeros();
339 let b1 = other.crisp_ones();
340 let bx = other.unknowns();
341 let res1 = (a0 & (b0 | bx | b1)) | (ax & (bx | b1)) | (a1 & b1);
342 let res0 = a1 & b0;
343 let resx = !res1 & !res0;
344 Self {
345 ones: BitPlane(res1),
346 unknowns: BitPlane(resx),
347 }
348 }
349 }
350 }
351
352 pub const fn equiv(self, other: Self, alg: Algebra) -> Self {
354 self.implies(other, alg).and(other.implies(self, alg), alg)
355 }
356}
357
358#[derive(Debug, Clone)]
360pub struct TruthTable {
361 pub variables: Vec<String>,
363 pub values: Vec<Ternary>,
365}
366
367impl TruthTable {
368 pub fn value_at(&self, index: usize) -> Option<Ternary> {
370 self.values.get(index).copied()
371 }
372
373 pub fn distinct_values(&self) -> Vec<Ternary> {
375 let mut seen = [false; 3];
376 for v in &self.values {
377 seen[match v {
378 Ternary::False => 0,
379 Ternary::Unknown => 1,
380 Ternary::True => 2,
381 }] = true;
382 }
383 let mut out = Vec::new();
384 if seen[0] {
385 out.push(Ternary::False);
386 }
387 if seen[1] {
388 out.push(Ternary::Unknown);
389 }
390 if seen[2] {
391 out.push(Ternary::True);
392 }
393 out
394 }
395
396 pub fn is_always_false(&self) -> bool {
398 self.values.iter().all(|v| v.is_false())
399 }
400
401 pub fn is_always_true(&self) -> bool {
403 self.values.iter().all(|v| v.is_true())
404 }
405
406 pub fn has_unknown(&self) -> bool {
408 self.values.iter().any(|v| v.is_unknown())
409 }
410}
411
412#[derive(Debug, Clone)]
414pub struct Evaluator {
415 algebra: Algebra,
416 variables: Vec<String>,
417}
418
419impl Evaluator {
420 pub fn new(algebra: Algebra) -> Self {
422 Self {
423 algebra,
424 variables: Vec::new(),
425 }
426 }
427
428 pub fn algebra(&self) -> Algebra {
430 self.algebra
431 }
432
433 pub fn variables(&self) -> &[String] {
435 &self.variables
436 }
437
438 pub fn declare(&mut self, name: impl Into<String>) -> usize {
440 let name = name.into();
441 if let Some(idx) = self.variables.iter().position(|v| *v == name) {
442 return idx;
443 }
444 self.variables.push(name);
445 self.variables.len() - 1
446 }
447
448 pub fn assignment_count(&self) -> Result<u64, LimitError> {
450 checked_pow3(self.variables.len())
451 }
452
453 pub fn chunk_planes(&self, base: u64) -> Result<Vec<TriBit>, LimitError> {
459 if !base.is_multiple_of(64) {
460 return Err(LimitError::ChunkBase { base });
461 }
462 base.checked_add(63).ok_or(LimitError::ChunkBase { base })?;
463 let mut planes = Vec::with_capacity(self.variables.len());
464 for i in 0..self.variables.len() {
465 let pow = checked_pow3(i)?;
466 let mut ones = 0u64;
467 let mut unknowns = 0u64;
468 for bit in 0..64u32 {
469 let group = base + bit as u64;
470 let digit = (group / pow) % 3;
471 match digit {
472 1 => ones |= 1u64 << bit,
473 2 => unknowns |= 1u64 << bit,
474 _ => {}
475 }
476 }
477 planes.push(TriBit {
478 ones: BitPlane(ones),
479 unknowns: BitPlane(unknowns),
480 });
481 }
482 Ok(planes)
483 }
484
485 pub fn evaluate<F>(&self, f: F) -> Result<TruthTable, LimitError>
489 where
490 F: Fn(&[TriBit]) -> TriBit,
491 {
492 self.evaluate_within(f, Limits::default())
493 }
494
495 pub fn evaluate_within<F>(&self, f: F, limits: Limits) -> Result<TruthTable, LimitError>
500 where
501 F: Fn(&[TriBit]) -> TriBit,
502 {
503 if self.variables.len() > limits.max_vars {
504 return Err(LimitError::Vars {
505 limit: limits.max_vars,
506 });
507 }
508 let total = self.assignment_count()?;
509 if total > limits.max_rows as u64 {
510 return Err(LimitError::Rows {
511 limit: limits.max_rows,
512 });
513 }
514 let capacity = usize::try_from(total).map_err(|_| LimitError::Rows {
515 limit: limits.max_rows,
516 })?;
517 let mut values = Vec::with_capacity(capacity);
518 let mut base = 0u64;
519 while base < total {
520 let planes = self.chunk_planes(base)?;
521 let res = f(&planes);
522 let take = (total - base).min(64) as u32;
523 for bit in 0..take {
524 values.push(res.get(bit));
525 }
526 base += 64;
527 }
528 Ok(TruthTable {
529 variables: self.variables.clone(),
530 values,
531 })
532 }
533}
534
535#[cfg(test)]
536mod tests {
537 use super::*;
538
539 fn tri(v: Ternary) -> TriBit {
540 TriBit::constant(v)
541 }
542
543 #[test]
544 fn not_matches_scalar() {
545 for a in Ternary::ALL {
546 assert_eq!(tri(a).not().get(0), Algebra::Kleene.not(a), "NOT {a}");
547 }
548 }
549
550 #[test]
551 fn and_or_match_scalar_for_all_algebras() {
552 for alg in Algebra::ALL {
553 for a in Ternary::ALL {
554 for b in Ternary::ALL {
555 assert_eq!(
556 tri(a).and(tri(b), alg).get(0),
557 alg.and(a, b),
558 "{alg} {a}&{b}"
559 );
560 assert_eq!(tri(a).or(tri(b), alg).get(0), alg.or(a, b), "{alg} {a}|{b}");
561 }
562 }
563 }
564 }
565
566 #[test]
567 fn strong_add_matches_scalar_for_all_algebras() {
568 for alg in Algebra::ALL {
569 for a in Ternary::ALL {
570 for b in Ternary::ALL {
571 assert_eq!(
572 tri(a).strong_add(tri(b), alg).get(0),
573 alg.strong_add(a, b),
574 "{alg} {a}+{b}"
575 );
576 }
577 }
578 }
579 }
580
581 #[test]
582 fn strong_and_matches_scalar_for_all_algebras() {
583 for alg in Algebra::ALL {
584 for a in Ternary::ALL {
585 for b in Ternary::ALL {
586 assert_eq!(
587 tri(a).strong_and(tri(b), alg).get(0),
588 alg.strong_and(a, b),
589 "{alg} {a}*{b}"
590 );
591 }
592 }
593 }
594 }
595
596 #[test]
597 fn ops_never_produce_illegal_rails() {
598 for alg in Algebra::ALL {
599 for a in Ternary::ALL {
600 for b in Ternary::ALL {
601 for r in [
602 tri(a).and(tri(b), alg),
603 tri(a).or(tri(b), alg),
604 tri(a).strong_add(tri(b), alg),
605 ] {
606 assert_eq!(r.ones.0 & r.unknowns.0, 0, "{alg} {a} {b} 产生了 (1,1)");
607 }
608 }
609 }
610 }
611 }
612
613 #[test]
614 fn implies_matches_scalar_for_all_algebras() {
615 for alg in Algebra::ALL {
616 for a in Ternary::ALL {
617 for b in Ternary::ALL {
618 assert_eq!(
619 tri(a).implies(tri(b), alg).get(0),
620 alg.implies(a, b),
621 "{alg} {a}=>{b}"
622 );
623 }
624 }
625 }
626 }
627
628 #[test]
629 fn equiv_matches_scalar_for_all_algebras() {
630 for alg in Algebra::ALL {
631 for a in Ternary::ALL {
632 for b in Ternary::ALL {
633 assert_eq!(
634 tri(a).equiv(tri(b), alg).get(0),
635 alg.equiv(a, b),
636 "{alg} {a}<=>{b}"
637 );
638 }
639 }
640 }
641 }
642
643 #[test]
644 fn bitwise_ops_agree_across_64_lanes() {
645 let mut ones = 0u64;
647 let mut unknowns = 0u64;
648 for i in 0..64u32 {
649 match i % 3 {
650 1 => ones |= 1u64 << i,
651 2 => unknowns |= 1u64 << i,
652 _ => {}
653 }
654 }
655 let t = TriBit {
656 ones: BitPlane(ones),
657 unknowns: BitPlane(unknowns),
658 };
659 let other = TriBit {
660 ones: BitPlane(0x5555_5555_5555_5555),
661 unknowns: BitPlane(0x0f0f_0f0f_0f0f_0f0f),
662 };
663 for alg in Algebra::ALL {
664 let got = t.and(other, alg);
665 for i in 0..64u32 {
666 assert_eq!(
667 got.get(i),
668 alg.and(t.get(i), other.get(i)),
669 "{alg} lane {i}"
670 );
671 }
672 }
673 }
674
675 #[test]
676 fn evaluator_covers_all_assignments() {
677 let mut ev = Evaluator::new(Algebra::Kleene);
678 ev.declare("a");
679 ev.declare("b");
680 assert_eq!(ev.assignment_count().unwrap(), 9);
681 let tt = ev.evaluate(|p| p[0]).unwrap();
682 assert_eq!(tt.values.len(), 9);
683 assert_eq!(tt.value_at(0), Some(Ternary::False));
685 assert_eq!(tt.value_at(1), Some(Ternary::True));
686 assert_eq!(tt.value_at(2), Some(Ternary::Unknown));
687 assert_eq!(tt.value_at(3), Some(Ternary::False));
688 }
689
690 #[test]
691 fn assignment_count_is_checked_not_saturated() {
692 let mut ev = Evaluator::new(Algebra::Kleene);
693 for i in 0..41 {
694 ev.declare(format!("v{i}"));
695 }
696 assert_eq!(
697 ev.assignment_count().unwrap_err(),
698 LimitError::CountOverflow { vars: 41 }
699 );
700 }
701
702 #[test]
703 fn chunk_base_must_be_aligned_and_not_overflow() {
704 let mut ev = Evaluator::new(Algebra::Kleene);
705 ev.declare("a");
706 assert_eq!(
707 ev.chunk_planes(1).unwrap_err(),
708 LimitError::ChunkBase { base: 1 }
709 );
710 assert!(matches!(
711 ev.chunk_planes(u64::MAX - 1).unwrap_err(),
712 LimitError::ChunkBase { .. }
713 ));
714 assert!(ev.chunk_planes(0).is_ok());
715 }
716
717 #[test]
718 fn evaluate_enforces_row_budget_before_allocating() {
719 let mut ev = Evaluator::new(Algebra::Kleene);
720 ev.declare("a");
721 let limits = Limits {
722 max_rows: 2,
723 ..Limits::default()
724 };
725 assert_eq!(
726 ev.evaluate_within(|p| p[0], limits).unwrap_err(),
727 LimitError::Rows { limit: 2 }
728 );
729 }
730
731 #[test]
732 fn evaluate_within_enforces_var_budget_directly() {
733 let mut ev = Evaluator::new(Algebra::Kleene);
734 for i in 0..13 {
735 ev.declare(format!("v{i}"));
736 }
737 let limits = Limits {
738 max_vars: 12,
739 ..Limits::default()
740 };
741 assert_eq!(
742 ev.evaluate_within(|_| TriBit::FALSE, limits).unwrap_err(),
743 LimitError::Vars { limit: 12 }
744 );
745 }
746
747 #[test]
748 fn bit_plane_checked_access_rejects_lane_overflow() {
749 let plane = BitPlane::with_bit(3);
750 assert_eq!(BitPlane::checked_with_bit(64), None);
751 assert_eq!(plane.checked_bit(3), Some(true));
752 assert_eq!(plane.checked_bit(64), None);
753 assert_eq!(BitPlane::with_bit(64), BitPlane::with_bit(0));
755 let tri = TriBit::from_binary(0b1);
756 assert_eq!(tri.checked_get(0), Some(Ternary::True));
757 assert_eq!(tri.checked_get(64), None);
758 }
759
760 #[test]
761 fn checked_bit_access_covers_all_boundaries() {
762 for bit in [0u32, 63] {
763 assert_eq!(BitPlane::checked_with_bit(bit), Some(BitPlane(1u64 << bit)));
764 }
765 for bit in [64u32, 65, u32::MAX] {
766 assert_eq!(BitPlane::checked_with_bit(bit), None);
767 assert_eq!(BitPlane::ONES.checked_bit(bit), None);
768 }
769 assert_eq!(BitPlane::ONES.checked_bit(63), Some(true));
770 }
771
772 #[test]
773 fn evaluator_with_zero_variables_has_one_row() {
774 let ev = Evaluator::new(Algebra::Kleene);
775 assert_eq!(ev.assignment_count().unwrap(), 1);
776 let tt = ev.evaluate(|_| TriBit::TRUE).unwrap();
777 assert!(tt.variables.is_empty());
778 assert_eq!(tt.values, vec![Ternary::True]);
779 }
780
781 #[test]
782 fn evaluator_spans_multiple_chunks() {
783 let mut ev = Evaluator::new(Algebra::Kleene);
785 for name in ["a", "b", "c", "d"] {
786 ev.declare(name);
787 }
788 assert_eq!(ev.assignment_count().unwrap(), 81);
789 let tt = ev.evaluate(|p| p[3]).unwrap();
790 assert_eq!(tt.values.len(), 81);
791 for (i, v) in tt.values.iter().enumerate() {
792 let digit = (i as u64 / 27) % 3;
793 let expect = match digit {
794 0 => Ternary::False,
795 1 => Ternary::True,
796 _ => Ternary::Unknown,
797 };
798 assert_eq!(*v, expect, "group {i}");
799 }
800 }
801}