Module sweep 

Combinational equivalence: two circuits’ outputs proven equal, or told apart by an input assignment that replays, every equality carried by a lemma whose LRAT proof a small checker re-validates.

Two circuits are joined in one and-inverter graph by miter: inputs of the same name shared, outputs paired by name. Structural hashing already merges every gate both compute the same way. decide then sweeps the rest (Kuehlmann, Dynamic transition relation simplification for bounded property checking, ICCAD 2004; Mishchenko et al., FRAIGs, 2005): random simulation groups nodes by their value signatures, each candidate pair is put to the CDCL solver in topological order, a refuted difference becomes a lemma that later queries may use, and a counterexample is added to the simulation patterns to split the classes it disproves. Each output pair is then equal by the lemmas, or decided by one more query.

A lemma’s formula is query_with_cut: the Tseitin clauses of the two literals’ cone, cut at the nodes the lemma names (left free, their own fan-in not encoded), the two clauses of each earlier lemma lying wholly inside that cone, and the difference itself. Leaving a cut free only removes constraints, so a refutation of the cut formula refutes the whole cone’s; a candidate is first put to the solver a few levels deep, where an equality implied by its fan-ins’ lemmas refutes at once, and only widened to the whole cone when the narrow formula has a model. The formula is a pure function of the graph, the cut and the lemmas before it, so check rebuilds it, replays the lemma’s LRAT proof with crate::lrat::check, and accepts a claimed equality only when the lemmas join its two literals, with matching phase, in a union-find. A solver whose UNSAT does not replay yields Verdict::Unknown, never an equality; a model that does not separate the two literals under Aig::eval likewise.

distinguish tells a family of circuits apart: the members that compute one function, each equality certified, and a few input assignments on which every two members that differ give different outputs, with each class’s outputs there: what names the member a black box computes from its measured outputs.

Structs

Certificate

Lemmas in proof order; a lemma’s query includes the lemmas before it.

CutCost

The queries put at one kind of cut, their verdicts and what they cost, summed.

Decided

decide’s verdict for each pair, the certificate behind its equalities, and its cost.

Distinction

A family of circuits told apart by distinguish.

Earlier

Lemmas in proof order, each node of one indexed by the lemmas that relate it: the lemmas touching a cone found in time proportional to the cone, not to every lemma, in lemma order.

Hard

One query’s cost: the pair, the cut it was put with (empty for the whole cone), its formula’s size and the conflicts its solve took.

Lemma

A proven equivalence a ≡ b: its proof refutes query_with_cut(a, b, cut, earlier lemmas).

Miter

Two circuits in one graph: inputs of the same name shared (unnamed and one-sided inputs kept apart), each named output of the left paired with the right’s output of that name, and an output a pair’s difference.

Options

How decide searches.

Progress

A report of a long search: report is handed the cost so far once every every candidates put to the solver.

Query

A lemma’s formula: variable k is the k-th node of cone (the two literals’ cone, in increasing order), then of extra (nodes outside the cone an earlier lemma relates to a node inside it, free, in increasing order).

Report

A decided miter: a verdict per output name, the certificate behind the equalities, and the search’s cost.

Stats

What a decision cost.

Enums

MiterError

Why two circuits cannot be paired.

Verdict

What decide found for one pair of literals.

Constants

CUT_DEPTHS

The depths a candidate is first tried at before its whole cone.

CUT_KINDS

The kinds of cut a query is put at: each of CUT_DEPTHS, where the cones meet, and none.

HARDEST

How many of the hardest queries Stats keeps.

Functions

check

Whether certificate proves every claim: each lemma’s proof refutes its query in order, and each claimed pair is one literal, or two literals the lemmas join with matching phase.

decide

Decide a ≡ b for every pair of literals of aig, latches read as free values.

distinguish

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.

equivalent

Pair left and right by output name and decide every pair.

miter

query

query_with_cut over the whole cone.

query_with_cut

The Tseitin clauses of the cone of a and b in node order, a node of cut (sorted) left free, then the two clauses of each earlier lemma with a literal in that cone, in lemma order (its other node, when outside the cone, a free variable of its own: lemmas joined through a representative the cone does not reach still join), then a ≠ b as (a ∨ b) ∧ (¬a ∨ ¬b).

separating_input

An input assignment on which some pair of left’s and right’s outputs differ, found by one search over every difference at once and replayed before it is returned, with the miter it is an assignment of; Ok(None) when the search shows they never differ. A search, not a certificate: an equality is claimed only by equivalent.