Enum BlastRefusal 

pub enum BlastRefusal {
    NotBounded,
    Budget {
        size: BlastSize,
        budget: u128,
    },
    GateBudget {
        dag_nodes: u64,
        budget: u64,
    },
}

Why a bit-blast produced no formula.

Variants

NotBounded

The expression is not a supported bounded/bitvector obligation (wrong widths, an Int, a construct with no circuit).

Budget

The circuit blasts, but its ProofExpr materialisation is bigger than budget.

Fields

size: BlastSize

budget: u128

GateBudget

The circuit itself — the SHARED gate DAG, not its unfolding — is bigger than budget. The ceiling that bounds a path which never materialises a tree.

Fields

dag_nodes: u64

budget: u64

Implementations

impl BlastRefusal

pub fn reason(&self) -> String

The prose a certificate carries when it declines this obligation — it names the cause AND the budget, so a reader can tell “we cannot express this” from “we will not pay for this”.

Trait Implementations

impl Clone for BlastRefusal

fn clone(&self) -> BlastRefusal

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for BlastRefusal

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

Formats the value using the given formatter.

impl PartialEq for BlastRefusal

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

impl StructuralPartialEq for BlastRefusal