Enum GpuSolverProductionExpectation 

pub enum GpuSolverProductionExpectation {
    Sat,
    Unsat,
    Unknown {
        reason: &'static str,
    },
    Timeout {
        budget_micros: u64,
    },
}

Expected GPU CDCL result for one production lifecycle step.

Variants

Sat

The step must be SAT under the currently pushed assumptions.

Unsat

The step must be UNSAT under the currently pushed assumptions.

Unknown

The accepted lifecycle step ended without a determined SAT/UNSAT status.

Fields

reason: &'static str

Diagnostic reason reported by the GPU-backed lifecycle scheduler.

Timeout

The accepted lifecycle step exhausted its GPU-backed budget.

Fields

budget_micros: u64

Nonzero timeout budget observed by the lifecycle scheduler.

Trait Implementations

impl Clone for GpuSolverProductionExpectation

fn clone(&self) -> GpuSolverProductionExpectation

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for GpuSolverProductionExpectation

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for GpuSolverProductionExpectation

fn eq(&self, other: &GpuSolverProductionExpectation) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for GpuSolverProductionExpectation

impl Eq for GpuSolverProductionExpectation

impl StructuralPartialEq for GpuSolverProductionExpectation