Skip to main content

pred_to_proof

logicaffeine_compile::codegen_sva::bitblast

Function pred_to_proof 

Source 
pub fn pred_to_proof(p: &Pred) -> ProofExpr
Expand description

Materialise a predicate’s ProofExpr tree. The escape hatch for a consumer that genuinely needs the tree (an SMT printer, a ProofExpr-shaped prover call) — and the thing every path that only wants a CNF must NOT call, because the tree is exponentially larger than the circuit.