logicaffeine_compile/codegen_dram/
set_algebra.rs

1//! Set algebra on the DRAM plane — the COMPLETE finite set algebra over BITSET-encoded sets, lowered
2//! to DRAM dataflow kernels. A set over a bounded universe is a bit vector (a row): membership of
3//! element `i` is bit `i`. Over that encoding the set algebra IS the bitwise algebra —
4//!
5//!   intersection ∩ = AND        union ∪ = OR              difference \ = AND-NOT
6//!   symmetric difference △ = XOR complement (¬) = NOT (within the universe)
7//!
8//! — so each set op lowers to a [`DramDataflow`] kernel built from the DRAM basis `{And, Or, Not}`,
9//! and is proven ≡ its set-theoretic reference. The VM's first-class set ops — `IntersectOp`/`UnionOp`
10//! — are [`recognize`]d directly; difference / symmetric_difference / complement are provided as
11//! proven kernels (the VM currently represents those via the AOT set-method path, not a VM ISA op).
12
13use super::dataflow::DramDataflow;
14use crate::codegen_sva::unified_placement::Row;
15use crate::vm::Op;
16
17/// A finite set operation over bitset-encoded sets.
18#[derive(Clone, Copy, PartialEq, Eq, Debug)]
19pub enum SetOp {
20    Intersection,
21    Union,
22    Difference,
23    SymmetricDifference,
24    Complement,
25}
26
27impl SetOp {
28    /// The number of set operands (Complement is unary; the rest are binary).
29    pub fn arity(self) -> usize {
30        if self == SetOp::Complement {
31            1
32        } else {
33            2
34        }
35    }
36
37    /// Every set operation this backend realizes in-DRAM — the coverage of the set-algebra lowering.
38    pub const ALL: &'static [SetOp] = &[
39        SetOp::Intersection,
40        SetOp::Union,
41        SetOp::Difference,
42        SetOp::SymmetricDifference,
43        SetOp::Complement,
44    ];
45}
46
47/// Recognize a VM ISA op as a set operation, if it is one. `IntersectOp`/`UnionOp` are the VM's
48/// first-class set ops; difference / symmetric_difference / complement have no VM ISA op yet (the AOT
49/// tier emits them as IndexSet methods), so they are not recognized from a VM program — but their
50/// kernels below are proven and ready to dispatch once those ops become first-class.
51pub fn recognize(op: &Op) -> Option<SetOp> {
52    match op {
53        Op::IntersectOp { .. } => Some(SetOp::Intersection),
54        Op::UnionOp { .. } => Some(SetOp::Union),
55        _ => None,
56    }
57}
58
59/// Lower a set op to a DRAM dataflow kernel over operand rows `a` (and `b` for binary ops; `b` is
60/// ignored for Complement). Returns the result row index. Built entirely from the DRAM basis.
61pub fn lower(op: SetOp, df: &mut DramDataflow, a: usize, b: usize) -> usize {
62    match op {
63        SetOp::Intersection => df.and(a, b),
64        SetOp::Union => df.or(a, b),
65        SetOp::Difference => df.difference(a, b), // a AND NOT b
66        SetOp::SymmetricDifference => df.xor(a, b),
67        SetOp::Complement => df.not(a), // within the universe = the full row width
68    }
69}
70
71/// The set-theoretic reference over bitset rows — the universe is the full row width (`!0` per word).
72pub fn reference(op: SetOp, a: &Row, b: &Row) -> Row {
73    match op {
74        SetOp::Intersection => a.iter().zip(b).map(|(x, y)| x & y).collect(),
75        SetOp::Union => a.iter().zip(b).map(|(x, y)| x | y).collect(),
76        SetOp::Difference => a.iter().zip(b).map(|(x, y)| x & !y).collect(),
77        SetOp::SymmetricDifference => a.iter().zip(b).map(|(x, y)| x ^ y).collect(),
78        SetOp::Complement => a.iter().map(|x| !x).collect(),
79    }
80}
81
82#[cfg(test)]
83#[path = "../../../logicaffeine_tests/unit/logicaffeine_compile/codegen_dram/set_algebra/tests.rs"]
84mod tests;
logicaffeine_compile/codegen_dram/set_algebra.rs

logicaffeine_compile/codegen_dram/
set_algebra.rs
