pub fn formula(aig: &Aig) -> Vec<Vec<Lit>>
The miter’s formula: for each And node in order its three Tseitin clauses, and node 0 false.