Skip to main content

pred_size

logicaffeine_compile::codegen_sva::bitblast

Function pred_size 

Source 
pub fn pred_size(p: &Pred) -> BlastSize
Expand description

What this predicate’s circuit costs — gates allocated vs. the ProofExpr tree a materialisation would hold. The instrument a budget reads.