Enum CertifyRefusal 

pub enum CertifyRefusal {
    Blast(BlastRefusal),
    NotRefuted,
}

Why a mapping earned no certificate. The three answers are genuinely different — “we cannot express this obligation”, “we will not pay to materialise it”, and “it is not true” — and a caller that prints Uncertified { reason } must not collapse them into one sentence.

Variants

Blast(BlastRefusal)

The obligation never reached a formula: no propositional form, or over the bit-blast budget.

NotRefuted

The formula was built but could not be refuted — the mapping is NOT equivalent to the spec, or the prover declined it. Fail-closed: a wrong mapping earns no certificate.

Implementations

impl CertifyRefusal

pub fn reason(&self) -> String

The prose a certificate carries when it declines. Names the cause — and, for a budget refusal, the budget itself, so the reader can tell a limit from a failure.

Trait Implementations

impl Clone for CertifyRefusal

fn clone(&self) -> CertifyRefusal

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CertifyRefusal

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

Formats the value using the given formatter.

impl PartialEq for CertifyRefusal

fn eq(&self, other: &CertifyRefusal) -> 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 Eq for CertifyRefusal

impl StructuralPartialEq for CertifyRefusal