System Architecture

┌─────────────────────────────────────────────────────────────────────────────┐
│                         XLOG REASONING STACK                                │
├─────────────────────────────────────────────────────────────────────────────┤
│                                                                             │
│  ┌─────────────┐   ┌─────────────┐   ┌─────────────┐   ┌─────────────┐    │
│  │ xlog-logic  │   │ xlog-prob   │   │ EIR/GPU     │   │ xlog-solve  │    │
│  │             │   │             │   │ epistemic   │   │             │    │
│  │ Datalog     │   │ ProbLog     │   │ Epistemic   │   │ SAT/MaxSAT  │    │
│  │ recursion   │   │ inference   │   │ world views │   │ solving     │    │
│  │ stratified  │   │ WMC/MC      │   │ K/M ops     │   │ GPU search  │    │
│  │ negation    │   │ gradients   │   │ splitting   │   │ certificates│    │
│  └──────┬──────┘   └──────┬──────┘   └──────┬──────┘   └──────┬──────┘    │
│         │                 │                 │                 │            │
│         └────────────┬────┴────────┬────────┴────────┬────────┘            │
│                      ▼             ▼                 ▼                     │
│              ┌─────────────────────────────────────────────┐               │
│              │         GPU Kernel Provider                 │               │
│              │   joins · sorts · aggregations · circuits   │               │
│              └─────────────────────────────────────────────┘               │
│                                                                             │
└─────────────────────────────────────────────────────────────────────────────┘

Source Code
    │
    ▼
┌─────────┐
│   AST   │  Abstract Syntax Tree from parser
└────┬────┘
     │
     ▼
┌─────────┐
│   RIR   │  Relational IR: joins, projections, unions, dedup, fixpoint loops
└────┬────┘
     │
     ├──────────────────┬──────────────────┐
     ▼                  ▼                  ▼
┌─────────┐       ┌─────────┐       ┌─────────┐
│   PIR   │       │   EIR   │       │   SIR   │
│Provenance│       │Epistemic│       │ Solve  │
│   IR    │       │   IR    │       │   IR   │
└────┬────┘       └────┬────┘       └────┬────┘
     │                  │                 │
     ▼                  │                 │
┌─────────┐             │                 │
│  XGCF   │◄────────────┴─────────────────┘
│GPU Circt│
└─────────┘

┌─────────────────────────────────────────────────────────┐
│                    XGCF Structure                       │
├─────────────────────────────────────────────────────────┤
│                                                         │
│  node_type[i] ∈ {CONST0, CONST1, LIT, AND, OR, DECISION}│
│                                                         │
│  a[i], b[i]      Child indices (node-type dependent)    │
│  var[i]          Variable ID for DECISION nodes         │
│  lit[i]          Literal ID for LIT nodes               │
│                                                         │
│  level_offsets[] Topological levels for parallel eval   │
│                                                         │
│  value[i]        Forward pass values (log-space)        │
│  adj[i]          Backward pass adjoints                 │
│                                                         │
└─────────────────────────────────────────────────────────┘

PIR (Provenance IR)
    │
    ▼ Tseitin encoding
┌─────────┐
│   CNF   │  Conjunctive Normal Form (with weights)
└────┬────┘
     │ Optional GPU preprocessing (simplification)
     ▼
┌─────────┐
│GPU d-DNNF│ Decision-DNNF compiler (GPU-native)
└────┬────┘
     │
     ▼
┌─────────────┐
│Decision-DNNF│  Decomposable circuit form
└──────┬──────┘
       │ Lower to GPU format
       ▼
┌─────────┐
│  XGCF   │  GPU-evaluable levelized circuit
└─────────┘

                                              ┌──> RIR ──> Deterministic executor  (xlog-runtime)
                                              │             (semi-naive fixpoint on GPU)
   xlog source ──> Parser ──> Stratifier ──┤
                                              │──> PIR ──> CNF ──> Decision-DNNF compiler ──> XGCF
                                              │             (probabilistic inference; xlog-prob)
                                              │
                                              │──> Solver IR (planned) ──> GPU CDCL
                                              │             (SAT/MaxSAT verification; xlog-solve)
                                              │
                                              └──> RIR + dILP masks ──> differentiable trainer
                                                            (neural-symbolic; xlog-neural + pyxlog)

xlog/
├── crates/
│   ├── xlog-core/       # Foundation types, traits, error handling
│   ├── xlog-ir/         # Intermediate representations (RIR nodes)
│   ├── xlog-logic/      # Datalog frontend (parser, compiler, optimizer)
│   ├── xlog-runtime/    # Query executor, relation storage
│   ├── xlog-cuda/       # CUDA provider, memory management, interop (Arrow IPC/C Data, DLPack)
│   ├── xlog-stats/      # Runtime statistics (optimizer feedback + adaptive indexing)
│   ├── xlog-prob/       # Probabilistic tier (exact inference + Monte Carlo)
│   ├── xlog-neural/     # Neural-symbolic integration
│   ├── xlog-solve/      # Solver services (SAT/MaxSAT)
│   ├── xlog-gpu/        # High-level GPU API (Rust)
│   ├── xlog-induce/     # Bounded exact-induction engine for an external consumer
│   ├── xlog-cli/        # CLI binary (deterministic + probabilistic execution)
│   ├── pyxlog/     # Python module (PyO3 + DLPack + training API)
│   └── xlog-cuda-tests/ # CUDA/PTX certification suite (not published)
├── kernels/             # CUDA source files (.cu) + embedded PTX (.ptx)
├── examples/
│   └── neural/          # Neural-symbolic training examples

Tier 0 (leaf):  xlog-core

Tier 1:         xlog-ir ──────────> xlog-core
                xlog-cuda ─────────> xlog-core
                xlog-stats ────────> xlog-core
                xlog-neural ───────> xlog-core          (Wave 1: new edge)

Tier 2:         xlog-logic ────────> xlog-core + xlog-ir + xlog-stats
                xlog-runtime ──────> xlog-core + xlog-ir + xlog-cuda + xlog-stats
                xlog-solve ────────> xlog-core + xlog-cuda

Tier 3:         xlog-gpu ─────────> xlog-core + xlog-cuda + xlog-ir + xlog-logic + xlog-runtime
                xlog-prob ─────────> xlog-core + xlog-cuda + xlog-logic + xlog-runtime + xlog-solve + xlog-ir
                xlog-induce ──────> xlog-core + xlog-cuda + xlog-runtime

Tier 4:         pyxlog ────────────> 9 crates (integration hub; includes xlog-induce)
                xlog-cli ──────────> xlog-core + xlog-cuda + xlog-logic + xlog-gpu + xlog-prob
                xlog-cuda-tests ───> xlog-cuda + xlog-core + xlog-solve

pub enum ScalarType {
    U32, U64,           // Unsigned integers
    I32, I64,           // Signed integers
    F32, F64,           // Floating point
    Bool,               // Boolean
    Symbol,             // Dictionary-encoded strings (hashed to u32)
}

pub struct Schema {
    pub columns: Vec<(String, ScalarType)>,  // Column names and types
    pub key_columns: Vec<usize>,              // Key column indices
}

pub enum RirNode {
    Scan { rel: RelId },                                    // Read relation
    Filter { input: Box<RirNode>, predicate: Expr },        // Selection
    Project { input: Box<RirNode>, columns: Vec<ProjectExpr> }, // Projection (pass-through + computed)
    Join {                                                   // Hash join
        left: Box<RirNode>,
        right: Box<RirNode>,
        left_keys: Vec<usize>,
        right_keys: Vec<usize>,
        join_type: JoinType,  // Inner, Semi, Anti, LeftOuter
    },
    GroupBy {                                                // Aggregation
        input: Box<RirNode>,
        key_cols: Vec<usize>,
        aggs: Vec<(usize, AggOp)>,  // (column, operation)
    },
    Union { inputs: Vec<RirNode> },                          // Set union
    Distinct { input: Box<RirNode>, key_cols: Vec<usize> },  // Deduplication
    Diff { left: Box<RirNode>, right: Box<RirNode> },        // Set difference
    Fixpoint {                                               // Recursive iteration
        scc_id: u32,
        base: Box<RirNode>,
        recursive: Box<RirNode>,
        delta_rel: RelId,
        full_rel: RelId,
    },
}

pub enum Expr {
    Column(usize),                              // Column reference
    Const(ConstValue),                          // Literal value
    Compare { left, op, right },                // Comparison (Eq, Ne, Lt, Le, Gt, Ge)
    And(Vec<Expr>),                             // Logical AND
    Or(Vec<Expr>),                              // Logical OR
    Not(Box<Expr>),                             // Logical NOT

    // Arithmetic (used by `is` expressions)
    Add(Box<Expr>, Box<Expr>),
    Sub(Box<Expr>, Box<Expr>),
    Mul(Box<Expr>, Box<Expr>),
    Div(Box<Expr>, Box<Expr>),
    Mod(Box<Expr>, Box<Expr>),
    Abs(Box<Expr>),
    Min(Box<Expr>, Box<Expr>),
    Max(Box<Expr>, Box<Expr>),
    Pow(Box<Expr>, Box<Expr>),
    Cast(Box<Expr>, ScalarType),
}

pub enum AggOp {
    Count,      // Count rows per group
    Sum,        // Sum values per group
    Min,        // Minimum value per group
    Max,        // Maximum value per group
    LogSumExp,  // Numerically stable log-sum-exp (for probabilistic inference)
}

use xlog_logic::parse_program;

let program = parse_program(source)?;

edge(1, 2).
edge(2, 3).
reach(X, Y) :- edge(X, Y).
reach(X, Z) :- reach(X, Y), edge(Y, Z).

use xlog_logic::stratify;

let strata = stratify(&program)?;

lowerer.set_strata(strata_preds);
let plan = lowerer.lower_program(&program)?;

use xlog_logic::Compiler;

pub struct Compiler {
    lowerer: Lowerer,
}

impl Compiler {
    pub fn compile(&mut self, source: &str) -> Result<ExecutionPlan> {
        // Phase 1: parse to AST
        let program = parse_program(source)?;

        // Compiler-internal desugaring of queries/constraints into internal rules

        // Phase 2: stratify + pass predicate groups into the lowerer
        let strata = stratify(&program)?;
        self.lowerer.set_strata(strata.into_iter().map(|s| s.predicates).collect());

        // Phase 3: lower to RIR plan
        let plan = self.lowerer.lower_program(&program)?;

        // Phase 4: optimizer rewrites (predicate pushdown, cost-aware join planning)

        Ok(plan)
    }
}

pub struct Executor {
    provider: Arc<CudaKernelProvider>,   // GPU kernel interface
    store: RelationStore,                 // Versioned relation storage
    rel_names: HashMap<RelId, String>,    // RelId → name mapping
    name_to_rel: HashMap<String, RelId>,  // name → RelId mapping
    stats: StatsManager,                  // Runtime statistics (optimizer feedback)
    join_index_cache: JoinIndexCache,     // Cached build-side indexes (adaptive indexing)
}

fn execute_node(&mut self, node: &RirNode) -> Result<CudaBuffer> {
    match node {
        RirNode::Scan { rel } => {
            self.execute_scan(*rel)
        }
        RirNode::Filter { input, predicate } => {
            let buf = self.execute_node(input)?;
            self.execute_filter(&buf, predicate)
        }
        RirNode::Join { left, right, left_keys, right_keys, join_type } => {
            let l = self.execute_node(left)?;
            let r = self.execute_node(right)?;
            self.provider.hash_join_v2(&l, &r, left_keys, right_keys, *join_type)
        }
        RirNode::GroupBy { input, key_cols, aggs } => {
            let buf = self.execute_node(input)?;
            self.provider.groupby_multi_agg(&buf, key_cols, aggs)
        }
        RirNode::Union { inputs } => {
            let bufs: Vec<_> = inputs.iter()
                .map(|n| self.execute_node(n))
                .collect::<Result<_>>()?;
            self.provider.union_all(&bufs)
        }
        RirNode::Distinct { input, key_cols } => {
            let buf = self.execute_node(input)?;
            self.provider.dedup(&buf, key_cols)
        }
        RirNode::Diff { left, right } => {
            let l = self.execute_node(left)?;
            let r = self.execute_node(right)?;
            self.provider.diff(&l, &r)
        }
        RirNode::Project { input, columns } => {
            let buf = self.execute_node(input)?;
            self.execute_project(&buf, columns)
        }
        RirNode::Fixpoint { .. } => {
            self.execute_fixpoint(node)
        }
    }
}

__global__ void compute_composite_hash(
    const uint8_t* data,          // Packed row data
    const uint32_t* col_offsets,  // Byte offset of each key column
    const uint32_t* col_sizes,    // Byte size of each key column
    uint32_t num_key_cols,
    uint32_t num_rows,
    uint32_t row_stride,
    uint64_t* hashes              // Output: 64-bit hash per row
) {
    uint32_t gid = blockIdx.x * blockDim.x + threadIdx.x;
    if (gid >= num_rows) return;

    const uint8_t* row = data + gid * row_stride;

    // FNV-1a hash combining all key columns
    uint64_t hash = 14695981039346656037ULL;
    for (uint32_t k = 0; k < num_key_cols; k++) {
        const uint8_t* col_start = row + col_offsets[k];
        for (uint32_t b = 0; b < col_sizes[k]; b++) {
            hash ^= col_start[b];
            hash *= 1099511628211ULL;
        }
    }
    hashes[gid] = hash;
}

// Radix sort operates on u32 digit segments; passes depend on key width (8 passes per 32 bits).
__global__ void radix_histogram(
    const uint32_t* keys,
    uint32_t n,
    uint32_t* histograms,  // [grid_size * 16]
    uint32_t shift
) {
    __shared__ uint32_t local_hist[16];

    // Initialize shared memory
    if (threadIdx.x < 16) local_hist[threadIdx.x] = 0;
    __syncthreads();

    uint32_t gid = blockIdx.x * blockDim.x + threadIdx.x;
    if (gid < n) {
        uint32_t digit = (keys[gid] >> shift) & 0xF;
        atomicAdd(&local_hist[digit], 1);
    }
    __syncthreads();

    // Write to global histogram
    if (threadIdx.x < 16) {
        histograms[blockIdx.x * 16 + threadIdx.x] = local_hist[threadIdx.x];
    }
}

__global__ void groupby_sum(
    const uint32_t* values,
    const uint32_t* group_ids,  // Pre-computed from sorted keys
    uint32_t num_rows,
    uint64_t* sums              // Output: sum per group
) {
    uint32_t gid = blockIdx.x * blockDim.x + threadIdx.x;
    if (gid >= num_rows) return;

    uint32_t group = group_ids[gid];
    atomicAdd((unsigned long long*)&sums[group], values[gid]);
}

pub enum CudaColumn {
    Owned(TrackedCudaSlice<u8>),      // XLOG-allocated GPU memory
    Dlpack(DlpackColumn),              // External memory via DLPack (calls deleter on drop)
}

pub struct CudaBuffer {
    pub columns: Vec<CudaColumn>,      // Column-major storage, bytes; typed by schema
    pub num_rows: u64,
    pub schema: Schema,
}

impl CudaBuffer {
    pub fn column(&self, idx: usize) -> Option<&CudaColumn>;
    pub fn num_rows(&self) -> u64;
    pub fn arity(&self) -> usize;      // Number of columns
    pub fn schema(&self) -> &Schema;
    pub fn is_empty(&self) -> bool;
}

pub struct GpuMemoryManager {
    device: Arc<CudaDevice>,
    budget: MemoryBudget,
    allocated: AtomicU64,
}

impl GpuMemoryManager {
    pub fn alloc<T: DeviceRepr>(self: &Arc<Self>, len: usize) -> Result<TrackedCudaSlice<T>> {
        let bytes = (len as u64) * (std::mem::size_of::<T>() as u64);

        // Atomic budget check with compare-exchange loop
        loop {
            let current = self.allocated.load(Ordering::SeqCst);
            let new = current.checked_add(bytes)
                .ok_or_else(|| XlogError::ResourceExhausted {
                    context: "allocation overflow".into(),
                    estimated_bytes: bytes,
                    budget_bytes: self.budget.device_bytes,
                })?;

            if new > self.budget.device_bytes {
                return Err(XlogError::ResourceExhausted {
                    context: "GPU memory budget exceeded".into(),
                    estimated_bytes: bytes,
                    budget_bytes: self.budget.device_bytes,
                });
            }

            if self.allocated.compare_exchange(
                current, new, Ordering::SeqCst, Ordering::SeqCst
            ).is_ok() {
                break;
            }
        }

        // Allocate via cudarc; tracked slice decrements budget on drop
        let slice = self.device.inner().alloc::<T>(len)?;
        Ok(TrackedCudaSlice::new(slice, bytes, self.clone()))
    }
}

pub struct MemoryBudget {
    pub device_bytes: u64,      // Hard limit
    pub allow_ooc: bool,        // Out-of-core spill (future feature)
    pub abort_on_exceed: bool,  // Fail vs warn
}

impl MemoryBudget {
    /// Use 80% of total device memory
    pub fn from_device_memory(total: u64) -> Self {
        Self {
            device_bytes: total * 80 / 100,
            allow_ooc: false,
            abort_on_exceed: true,
        }
    }

    /// Fixed byte limit
    pub fn with_limit(bytes: u64) -> Self {
        Self {
            device_bytes: bytes,
            allow_ooc: false,
            abort_on_exceed: true,
        }
    }
}

use xlog_logic::Compiler;

let mut compiler = Compiler::new();
let plan = compiler.compile(r#"
    pred edge(u32, u32).
    pred reach(u32, u32).

    edge(1, 2).
    edge(2, 3).

    reach(X, Y) :- edge(X, Y).
    reach(X, Z) :- reach(X, Y), edge(Y, Z).

    ?- reach(1, N).
"#)?;

use std::sync::Arc;
use xlog_core::MemoryBudget;
use xlog_cuda::{CudaDevice, CudaKernelProvider, GpuMemoryManager};
use xlog_runtime::Executor;

// Initialize GPU
let device = Arc::new(CudaDevice::new(0)?);
let budget = MemoryBudget::with_limit(1 << 30);  // 1 GB
let memory = Arc::new(GpuMemoryManager::new(device.clone(), budget));
let provider = Arc::new(CudaKernelProvider::new(device, memory)?);

// Create executor
let mut executor = Executor::new(provider);

// Register input relations
executor.register_relation(RelId(0), "edge");
executor.store_mut().put("edge", edge_buffer);

// Execute plan
let result = executor.execute_plan(&plan)?;

// Read results
let reach = executor.store().get("reach").unwrap();
println!("Reachable pairs: {} rows", reach.num_rows());

use pyxlog::LogicProgram;

let program = LogicProgram::compile(source)?;
let results = program.run()?;

for (name, buffer) in results {
    println!("{}: {} rows", name, buffer.num_rows());
}

# Deterministic execution
xlog run examples/xlog/00-basics/01_tc_reachability.xlog
xlog run --input edge=data.arrow --output csv program.xlog

# Probabilistic execution
xlog prob examples/prob/01-wet-conditioning.xlog --prob-engine exact_ddnnf
xlog prob program.xlog --prob-engine mc --samples 10000 --seed 42

# Output formats
xlog run program.xlog --output pretty   # Default: formatted tables
xlog run program.xlog --output csv      # CSV format
xlog run program.xlog --output arrow --output-dir ./results  # Arrow IPC files

import pyxlog

# Deterministic execution
program = pyxlog.LogicProgram.compile(source)
results = program.evaluate()

# Results are DLPack capsules (zero-copy GPU tensors)
for name, capsule in results.items():
    import torch
    tensor = torch.from_dlpack(capsule)
    print(f"{name}: {tensor.shape}")

# Probabilistic execution
prob_program = pyxlog.Program.compile(source, prob_engine="exact_ddnnf")
prob_results = prob_program.evaluate()
import torch
prob = torch.from_dlpack(prob_results.prob)  # f64 CUDA tensor, shape [num_queries]
print(prob_results.atoms)
print(prob)
# Optional host read for a single scalar:
print(float(prob[0].item()))

# Neural-symbolic training
program = pyxlog.Program.compile("""
    nn(mnist_net, [X], Y, [0,1,2,3,4,5,6,7,8,9]) :: digit(X, Y).
    addition(X, Y, Z) :- digit(X, DigitX), digit(Y, DigitY), Z is DigitX + DigitY.
""")

# Register PyTorch network
program.register_network("mnist_net", model, optimizer)

# Add tensor data source
program.add_tensor_source("train", images_tensor)

# Train on addition queries
history = pyxlog.train_model(program, queries, epochs=50, batch_size=32)
print(f"Final loss: {history.epoch_losses[-1]}")

use xlog_runtime::{Profiler, OpStats};

let mut profiler = Profiler::new(true);  // enabled
profiler.record(OpStats::new("hash_join", 1000, 500, 1234, 8000));
profiler.record(OpStats::new("filter", 500, 100, 567, 4000));
println!("{}", profiler.summary());

┌─────────────────────────────────────────────────────────────────────────┐
│                         XLOG SYSTEM DATAFLOW                            │
├─────────────────────────────────────────────────────────────────────────┤
│                                                                         │
│  ┌─────────────────┐                                                    │
│  │ Datalog Source  │                                                    │
│  │                 │                                                    │
│  │ edge(1,2).      │                                                    │
│  │ reach(X,Y) :-   │                                                    │
│  │   edge(X,Y).    │                                                    │
│  └────────┬────────┘                                                    │
│           │                                                             │
│           ▼                                                             │
│  ┌─────────────────┐                                                    │
│  │ PARSER (Pest)   │  Tokenize → Parse → AST                           │
│  └────────┬────────┘                                                    │
│           │ Program { rules, facts, predicates }                        │
│           ▼                                                             │
│  ┌─────────────────┐                                                    │
│  │ STRATIFIER      │  Dependency graph → SCCs → Strata ordering        │
│  └────────┬────────┘                                                    │
│           │ Vec<Stratum>                                                │
│           ▼                                                             │
│  ┌─────────────────┐                                                    │
│  │ LOWERER         │  AST → Join trees → RIR nodes                     │
│  │                 │  Schema inference, variable tracking               │
│  └────────┬────────┘                                                    │
│           │ ExecutionPlan { sccs, strata, rules_by_scc }               │
│           ▼                                                             │
│  ┌─────────────────┐                                                    │
│  │ EXECUTOR        │  Execute strata → Execute rules → RIR nodes       │
│  │                 │                                                    │
│  │  for stratum:   │                                                    │
│  │    for scc:     │                                                    │
│  │      for rule:  │                                                    │
│  │        eval()   │───────────────────────┐                           │
│  └─────────────────┘                       │                           │
│                                            ▼                           │
│  ┌──────────────────────────────────────────────────────────┐          │
│  │ RIR NODE EVALUATION                                      │          │
│  │                                                          │          │
│  │  Scan ──────► Read from RelationStore                    │          │
│  │  Filter ────► GPU: mask DAG + compact                    │          │
│  │  Project ───► GPU: column selection + arithmetic         │          │
│  │  Join ──────► GPU: hash_join_v2 (build/probe)           │          │
│  │  GroupBy ───► GPU: sort → boundaries → ids/keys → agg    │          │
│  │  Union ─────► GPU: concat → sort → dedup                 │          │
│  │  Diff ──────► GPU: sort both → binary search mark        │          │
│  │  Distinct ──► GPU: sort → mark dups → compact            │          │
│  │  Fixpoint ──► Loop until convergence (semi-naive)        │          │
│  └──────────────────────────────────────────────────────────┘          │
│                          │                                              │
│                          ▼                                              │
│  ┌─────────────────────────────────────────────────────────────────┐   │
│  │ GPU KERNEL PROVIDER                                              │   │
│  │                                                                  │   │
│  │  ┌─────────┐ ┌─────────┐ ┌─────────┐ ┌─────────┐ ┌─────────┐   │   │
│  │  │ JOIN    │ │ FILTER  │ │ SORT    │ │ GROUPBY │ │ SET_OPS │   │   │
│  │  │ .cu     │ │ .cu     │ │ .cu     │ │ .cu     │ │ .cu     │   │   │
│  │  └────┬────┘ └────┬────┘ └────┬────┘ └────┬────┘ └────┬────┘   │   │
│  │       │           │           │           │           │         │   │
│  │       └───────────┴───────────┼───────────┴───────────┘         │   │
│  │                               ▼                                  │   │
│  │                    ┌─────────────────────┐                       │   │
│  │                    │ GPU MEMORY          │                       │   │
│  │                    │ (Column-Oriented)   │                       │   │
│  │                    │                     │                       │   │
│  │                    │ CudaBuffer {        │                       │   │
│  │                    │   columns: Vec<>    │                       │   │
│  │                    │   num_rows          │                       │   │
│  │                    │   schema            │                       │   │
│  │                    │ }                   │                       │   │
│  │                    └─────────────────────┘                       │   │
│  └─────────────────────────────────────────────────────────────────┘   │
│                          │                                              │
│                          ▼                                              │
│  ┌─────────────────┐                                                    │
│  │ RELATION STORE  │  HashMap<String, CudaBuffer>                      │
│  │                 │  Intermediate and final relations                  │
│  └────────┬────────┘                                                    │
│           │                                                             │
│           ▼                                                             │
│  ┌─────────────────┐                                                    │
│  │ RESULT          │  CudaBuffer (GPU-resident query result)           │
│  └─────────────────┘                                                    │
│                                                                         │
└─────────────────────────────────────────────────────────────────────────┘

pub enum XlogError {
    /// Syntax errors during parsing
    Parse(String),

    /// Unstratifiable negation (cycle through negation)
    StratificationCycle(Vec<String>),

    /// Domain safety violation (variable not bound in positive atoms)
    UnsafeVariable(String),

    /// Memory budget exceeded
    ResourceExhausted {
        context: String,
        estimated_bytes: u64,
        budget_bytes: u64,
    },

    /// CUDA kernel errors
    Kernel(String),

    /// Type mismatches
    Type(String),

    /// Semantic errors during compilation
    Compilation(String),

    /// Runtime failures
    Execution(String),
}

// Use 80% of total device memory
let total_device_bytes = device.total_memory()?;
let budget = MemoryBudget::from_device_memory(total_device_bytes);

// Fixed limit (e.g., 4 GB)
let budget = MemoryBudget::with_limit(4 * 1024 * 1024 * 1024);

// Maximum fixpoint iterations (prevent infinite loops)
const MAX_FIXPOINT_ITERATIONS: usize = 1000;
const MAX_SCC_ITERATIONS: usize = 1000;

# Debug mode
cargo test --workspace --all-targets --exclude pyxlog

# Release mode (recommended for GPU tests)
cargo test --workspace --all-targets --exclude pyxlog --release

cargo test -p xlog-cuda-tests --test certification_suite --release -- --nocapture