Function distinguish 

pub fn distinguish(
    members: &[Aig],
    seeds: &[Vec<(String, bool)>],
    budget: u64,
    opts: &Options,
) -> Result<Distinction, String>

Tell a family of circuits apart: which members compute the same function, each such equality proven and certified (equivalent), and input assignments on which every two members that differ give different outputs. The members share input and output names; an input without a name is refused unless no output reads it. Simulation on the vectors so far groups the members by their outputs; within a group each member is put against the group’s first, and an input that separates them (separating_input, budget conflicts) becomes a vector that splits the group, while none found makes it proven equal. The cover is chosen greedily from the seeds and the found vectors, each pick the vector that tells the most pairs of classes apart that no earlier pick does; the table is each class’s outputs there, what names the class of a black box whose outputs on the cover are measured.