Struct ExactDdnnfProgram

Source

pub struct ExactDdnnfProgram { /* private fields */ }

Implementations§

Source §

pub fn compile_from_program( program: &Program, config: GpuConfig, ) -> Result<Self>

Compile an already parsed program with the requested GPU configuration.

Imports must already be resolved and merged. This method does not load unresolved use declarations from the filesystem.

Source

pub fn uses_gpu_production_backend(&self) -> bool

Source

pub fn last_compile_profile(&self) -> Option<&CircuitCompileProfile>

Get the latest circuit compilation profile (populated when XLOG_WARMUP_PROFILE=1).

Source

pub fn prob_var_map(&self) -> Vec<ProbVarInfo>

Materializes a dense vector describing what each CNF variable stands for.

The returned vector’s length is the CNF encoder’s variable capacity (3 * number of PIR nodes at compile time, see compilation/gpu_cnf.rs) — not the number of CNF variables actually in use, and not the number of random variables in the program. Slot v describes CNF variable v directly when v was assigned; slot 0 is always unused padding (CNF variables are 1-indexed), and so is any other slot with no variable assigned to it — those padding slots are indistinguishable from ProbVarInfo::Other. Do not treat len() of the result as a variable count or a random-variable count; use Self::random_var_indices for that (Self::num_vars returns this same capacity, not a count, so it is not a substitute here).

What is guaranteed is alignment with evaluate_gpu_with_grads’s grad_true/grad_false vectors, which are allocated with the same capacity: prob_var_map()[v] and grad_true[v] name and value the same variable v.

Rebuilds the dense vector on every call from the sparse prob_var_entries storage that actually lives for the lifetime of the program.

On the GPU count-lift fast path (count aggregates without evidence or disjunctions — see Self::uses_gpu_native_count_lift), no CNF encoding is ever built, so this returns an empty vector even for programs that do have probabilistic facts. Callers that need to enumerate a program’s probabilistic facts must check uses_gpu_native_count_lift() first and treat an empty map from that path as “mapping unavailable”, not as “no random variables”.

Source

pub fn evaluate(&self) -> Result<ExactResult>

Source

pub fn num_vars(&self) -> usize

Returns the CNF encoder’s variable capacity (max_var + 1), i.e. the same quantity as prob_var_map().len() — not the number of CNF variables actually assigned, and not the number of random variables in the program (most CNF variables are auxiliary Tseitin variables with no probabilistic meaning). Use Self::random_var_indices to count or enumerate random variables instead.

Source

pub fn random_var_indices(&self) -> Vec<u32>

Returns the indices of random (probabilistic) variables in order.

Random variables are those with non-trivial weights (not (0.0, 0.0)). These correspond to annotated disjunctions in the source program. The order matches the order variables were assigned during CNF encoding.

Source

pub fn neural_backward_nll_buffers( &self, slots: &GpuWeightSlots, query_idx: usize, probs: &[CudaBuffer], out_grads: &mut [CudaBuffer], cfg: NeuralFastPathConfig, ) -> Result<()>

GPU neural fast-path: compute NLL gradients w.r.t. probability tensors (no host reads).

This implements the design in docs/design/2026-01-22-gpu-native-compilation-design.md §5.3:

Fill AD conditional-chain log-weights from device-resident p[label].
Run XGCF forward+backward on GPU.
Scatter gradients back into probability-space via the correct chain rule (uses both grad_true + grad_false).

The output gradient buffers are updated in-place: