Skip to main content

xlog_induce/
lib.rs

1//! xlog-induce — native bounded exact-induction engine.
2//!
3//! Scores all `(left, right)` candidate pairs for the four supported topologies (chain,
4//! star, fanout, fanin) in a single batched GPU pass and returns the top-K per topology
5//! with full candidate metadata.
6//!
7//! Behaviorally equivalent to the `backend="python"` reference implementation
8//! in `crates/pyxlog/python/pyxlog/ilp/exact_induce.py` on bounded requests;
9//! the parity contract is locked by `python/tests/test_ilp_exact_induce.py`.
10//!
11//! The native production path includes request validation, deterministic reduction,
12//! trivial-dead-end early returns, the batched scoring kernel, device-side top-K
13//! selection, and compact selected-row transfers.
14
15pub mod index;
16pub mod nary;
17pub mod nary_engine;
18pub mod nary_layout;
19pub mod nary_reference;
20pub mod provenance;
21pub mod reduce;
22pub mod score;
23pub mod types;
24mod validate;
25
26pub use nary::{
27    canonical_binary_pattern, enumerate_patterns, BodyAtomPattern, NaryEnumerationConfig,
28    NaryRulePattern, PatternVar,
29};
30pub use nary_engine::{
31    induce_exact_nary, InduceExactNaryRequest, NaryInductionConfig, NaryInductionResult,
32    ScoredNaryCandidate,
33};
34pub use provenance::InductionProvenanceRegistry;
35pub use reduce::{reduce_nary, reduce_per_topology, KeptNaryPattern, ScoredPair};
36pub use types::{
37    ExactInductionConfig, ExactInductionResult, InducedRuleProvenance, InducedRuleRegistry,
38    InductionAlternative, InductionSupportRow, RuleSourceKind, ScoredCandidate, Topology,
39};
40
41use xlog_core::{RelId, Result, ScalarType, XlogError};
42use xlog_cuda::{CudaBuffer, CudaKernelProvider};
43
44use validate::{classify_request, PreKernelOutcome, RequestMetadata};
45
46#[derive(Clone, Copy, Debug, Eq, PartialEq)]
47enum ExactPairType {
48    U64,
49    U32,
50    Symbol,
51}
52
53/// Inputs to one [`induce_exact`] call.
54///
55/// Each candidate is a `(RelId, &CudaBuffer)` pair: the `RelId` is a label that
56/// flows through to every [`ScoredCandidate`] produced from that buffer, and
57/// the `CudaBuffer` carries the relation's current binary-pair facts.
58///
59/// `positives` and `negatives` are themselves binary-pair buffers (arity 2,
60/// column type `U64`). Name-to-`RelId` resolution and relation-store lookup
61/// happen at the pyxlog boundary — the engine only sees indices + handles.
62pub struct InduceExactRequest<'a> {
63    pub head_rel_idx: RelId,
64    pub candidates: &'a [(RelId, &'a CudaBuffer)],
65    pub positives: &'a CudaBuffer,
66    pub negatives: Option<&'a CudaBuffer>,
67    pub config: ExactInductionConfig,
68}
69
70/// Run exact induction against one request.
71///
72/// Returns an [`ExactInductionResult`] matching the Python reference on
73/// bounded inputs.
74///
75/// The `provider` argument owns the kernel launcher — it's passed separately
76/// from the request so the engine can also materialize short-lived GPU
77/// buffers (an empty negatives buffer when `request.negatives` is `None`).
78pub fn induce_exact(
79    provider: &CudaKernelProvider,
80    request: &InduceExactRequest<'_>,
81) -> Result<ExactInductionResult> {
82    // Empty candidates is a trivial dead-end and needs no CUDA inspection —
83    // matches the Python reference's `if not body_indices: return ...` path.
84    if request.candidates.is_empty() {
85        return Ok(ExactInductionResult::default());
86    }
87
88    // Buffer-level validation (arity 2, accepted typed pair columns). Runs before
89    // metadata extraction so we fail loud on pyxlog-side assembly bugs.
90    let pair_type = validate_pair_buffer(request.positives, "positives")?;
91    if let Some(neg) = request.negatives {
92        require_pair_type(neg, "negatives", pair_type)?;
93    }
94    for (i, (_, buf)) in request.candidates.iter().enumerate() {
95        require_pair_type(buf, &format!("candidate[{}]", i), pair_type)?;
96    }
97
98    // Extract row counts from the cached host-side metadata. The DLPack ingest
99    // path (`CudaKernelProvider::from_dlpack_tensors_with_schema`) populates
100    // `cached_row_count`, so this is a pure struct read — no device-to-host
101    // transfer. That's how we keep the hot-loop device-to-host transfer budget
102    // flat across candidate counts.
103    let pos_count = cached_rows(request.positives, "positives")?;
104    let neg_count = request
105        .negatives
106        .map(|b| cached_rows(b, "negatives"))
107        .transpose()?
108        .unwrap_or(0);
109
110    let meta = RequestMetadata {
111        candidate_count: request.candidates.len() as u32,
112        positive_count: pos_count,
113        negative_count: neg_count,
114        k_per_topology: request.config.k_per_topology,
115    };
116
117    match classify_request(meta) {
118        PreKernelOutcome::TrivialEmpty(result) => Ok(result),
119        PreKernelOutcome::Proceed(m) => score_and_reduce(provider, request, m),
120    }
121}
122
123fn score_and_reduce(
124    provider: &CudaKernelProvider,
125    request: &InduceExactRequest<'_>,
126    meta: RequestMetadata,
127) -> Result<ExactInductionResult> {
128    // ── Normalize negatives: engine + launcher expect an always-present
129    //    buffer. When the caller passes `None`, construct an empty U64 pair
130    //    buffer (zero rows) using the positives' schema. This keeps the
131    //    launcher signature and kernel signature uniform.
132    let empty_neg_holder: Option<CudaBuffer> = if request.negatives.is_none() {
133        Some(provider.create_empty_buffer(request.positives.schema().clone())?)
134    } else {
135        None
136    };
137    let negatives: &CudaBuffer = match request.negatives {
138        Some(b) => b,
139        None => empty_neg_holder
140            .as_ref()
141            .expect("holder populated in the None branch above"),
142    };
143
144    // ── Drive the batched scoring kernel and device-side top-K selector.
145    let candidate_buffers: Vec<&CudaBuffer> = request.candidates.iter().map(|(_, b)| *b).collect();
146    let selected = provider.ilp_exact_score_topk(
147        &candidate_buffers,
148        request.positives,
149        negatives,
150        request.config.k_per_topology,
151    )?;
152    let mut candidates = Vec::with_capacity(selected.len());
153    for row in selected {
154        let topology = topology_from_kernel_idx(row.topology_idx)?;
155        let left_idx = row.left_idx as usize;
156        let right_idx = row.right_idx as usize;
157        let (left_rel_idx, _) = request.candidates.get(left_idx).ok_or_else(|| {
158            XlogError::Execution(format!(
159                "induce_exact: device selector returned left index {} for {} candidates",
160                left_idx,
161                request.candidates.len()
162            ))
163        })?;
164        let (right_rel_idx, _) = request.candidates.get(right_idx).ok_or_else(|| {
165            XlogError::Execution(format!(
166                "induce_exact: device selector returned right index {} for {} candidates",
167                right_idx,
168                request.candidates.len()
169            ))
170        })?;
171        candidates.push(ScoredCandidate {
172            topology,
173            head_rel_idx: request.head_rel_idx,
174            left_rel_idx: *left_rel_idx,
175            right_rel_idx: *right_rel_idx,
176            positives_covered: row.positives_covered,
177            negatives_covered: row.negatives_covered,
178            local_rank: row.local_rank,
179            next_positives_covered: row.next_positives_covered,
180            next_negatives_covered: row.next_negatives_covered,
181            tie_class_size: row.tie_class_size,
182        });
183    }
184    let total_scored = 4u32
185        .checked_mul(meta.candidate_count)
186        .and_then(|v| v.checked_mul(meta.candidate_count))
187        .ok_or_else(|| XlogError::Execution("induce_exact: total_scored overflow".into()))?;
188
189    Ok(ExactInductionResult {
190        candidates,
191        total_scored,
192        candidate_count: meta.candidate_count,
193        positive_count: meta.positive_count,
194        negative_count: meta.negative_count,
195    })
196}
197
198fn topology_from_kernel_idx(idx: u32) -> Result<Topology> {
199    match idx {
200        0 => Ok(Topology::Chain),
201        1 => Ok(Topology::Star),
202        2 => Ok(Topology::Fanout),
203        3 => Ok(Topology::Fanin),
204        _ => Err(XlogError::Execution(format!(
205            "induce_exact: device selector returned topology index {}",
206            idx
207        ))),
208    }
209}
210
211fn validate_pair_buffer(buf: &CudaBuffer, label: &str) -> Result<ExactPairType> {
212    if buf.arity() != 2 {
213        return Err(XlogError::Execution(format!(
214            "induce_exact: {} buffer has arity {}, expected 2",
215            label,
216            buf.arity(),
217        )));
218    }
219    let mut pair_type = None;
220    for col_idx in 0..2 {
221        let t = buf.schema().column_type(col_idx).ok_or_else(|| {
222            XlogError::Type(format!(
223                "induce_exact: {} buffer column {} has no schema type",
224                label, col_idx,
225            ))
226        })?;
227        let col_type = match t {
228            ScalarType::U64 => ExactPairType::U64,
229            ScalarType::U32 => ExactPairType::U32,
230            ScalarType::Symbol => ExactPairType::Symbol,
231            _ => {
232                return Err(XlogError::Type(format!(
233                    "induce_exact: {} buffer column {} has type {:?}, expected U64, U32, or Symbol",
234                    label, col_idx, t,
235                )));
236            }
237        };
238        if let Some(expected) = pair_type {
239            if expected != col_type {
240                return Err(XlogError::Type(format!(
241                    "induce_exact: {} buffer column {} type mismatch: {:?} vs {:?}",
242                    label, col_idx, expected, col_type,
243                )));
244            }
245        } else {
246            pair_type = Some(col_type);
247        }
248    }
249    Ok(pair_type.expect("arity 2 loop sets pair type"))
250}
251
252fn require_pair_type(buf: &CudaBuffer, label: &str, expected: ExactPairType) -> Result<()> {
253    let actual = validate_pair_buffer(buf, label)?;
254    if actual != expected {
255        return Err(XlogError::Type(format!(
256            "induce_exact: {} buffer type mismatch: expected {:?}, got {:?}",
257            label, expected, actual,
258        )));
259    }
260    Ok(())
261}
262
263fn cached_rows(buf: &CudaBuffer, label: &str) -> Result<u32> {
264    buf.cached_row_count().ok_or_else(|| {
265        XlogError::Execution(format!(
266            "induce_exact: {} buffer has no cached row count \
267             (DLPack ingest path should populate it; required to avoid hot-loop device-to-host transfer)",
268            label,
269        ))
270    })
271}
272
273#[cfg(test)]
274mod tests {
275    use super::*;
276
277    #[test]
278    fn topology_as_str_matches_python_contract() {
279        assert_eq!(Topology::Chain.as_str(), "chain");
280        assert_eq!(Topology::Star.as_str(), "star");
281        assert_eq!(Topology::Fanout.as_str(), "fanout");
282        assert_eq!(Topology::Fanin.as_str(), "fanin");
283    }
284
285    #[test]
286    fn topology_all_is_engine_order() {
287        assert_eq!(
288            Topology::ALL,
289            [
290                Topology::Chain,
291                Topology::Star,
292                Topology::Fanout,
293                Topology::Fanin
294            ],
295        );
296    }
297}