pub fn decide(
aig: &Aig,
pairs: &[(AigLit, AigLit)],
opts: &Options,
) -> (Vec<Verdict>, Lrat, Stats)Expand description
Decide a ≡ b for every pair of literals of aig, latches read as free values: a verdict per pair, the derivation
of every equality from formula, and the cost.