pub struct GpuCnf {
pub var_cap: u32,
pub clause_cap: u32,
pub lit_cap: u32,
pub num_vars: TrackedCudaSlice<u32>,
pub num_clauses: TrackedCudaSlice<u32>,
pub num_lits: TrackedCudaSlice<u32>,
pub clause_offsets: TrackedCudaSlice<u32>,
pub literals: TrackedCudaSlice<i32>,
}Expand description
GPU-resident CNF in CSR form (DIMACS literals, 1-based variable ids).
This is the solver-facing CNF representation used by the GPU CDCL verifier.
Fields§
§var_cap: u32Variable capacity (>= num_vars).
clause_cap: u32Clause capacity (>= num_clauses).
lit_cap: u32Literal capacity (>= num_lits).
num_vars: TrackedCudaSlice<u32>Device-resident num_vars (len = 1).
num_clauses: TrackedCudaSlice<u32>Device-resident num_clauses (len = 1).
num_lits: TrackedCudaSlice<u32>Device-resident num_lits (len = 1).
clause_offsets: TrackedCudaSlice<u32>CSR offsets (len = clause_cap + 1).
literals: TrackedCudaSlice<i32>Flattened CSR literal array (len = lit_cap).
Implementations§
Source§impl GpuCnf
impl GpuCnf
pub fn num_literals_cap(&self) -> usize
Sourcepub fn from_host(
instance: &SolveInstance,
provider: &Arc<CudaKernelProvider>,
) -> Result<Self>
pub fn from_host( instance: &SolveInstance, provider: &Arc<CudaKernelProvider>, ) -> Result<Self>
Host -> device upload helper for tests and tooling.
Production GPU-native paths should build GpuCnf directly on device.
Auto Trait Implementations§
impl Freeze for GpuCnf
impl RefUnwindSafe for GpuCnf
impl Send for GpuCnf
impl Sync for GpuCnf
impl Unpin for GpuCnf
impl UnsafeUnpin for GpuCnf
impl UnwindSafe for GpuCnf
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more