This module contains an implementation of a verified Tseitin transformation on AIGs. The key results are the toCNF function and the toCNF_equisat correctness statement. The implementation is done in the style of section 3.4 of the AIGNET paper.

def Std.Sat.AIG.toCNF (entry : Entrypoint Nat) : CNF Nat

Convert an AIG into CNF, starting at some entry node.

theorem Std.Sat.AIG.toCNF_equisat (entry : Entrypoint Nat) : (toCNF entry).Unsat ↔ entry.Unsat

An AIG is unsat iff its CNF is unsat.