Make Aig_And commutative when fAddStrash is enabled. - #553
Closed
TrevorHansen wants to merge 1 commit into
Closed
Conversation
Aig_ObjCreateGhost() orders an AND's operands by regular id, but that happens after the fAddStrash block has run. That block tests p0's grandchildren against p1 before testing p1's against p0, so where two of its rules could both fire, the argument order decides which one wins: Aig_And(p,a,b) and Aig_And(p,b,a) can return different nodes for the same function. Order the operands at the top of that block. Measured over 16000 ordered pairs of random gates with fAddStrash set, 126 returned different nodes before this change and none do after. With fAddStrash clear the block never runs and Aig_And is already commutative, which is why the swap belongs inside it rather than ahead of it: ABC's default configuration then pays nothing. It does not cost nodes. On the same measurement the resulting AIGs are slightly smaller in total -- 14517 AND nodes against 14627, about 0.75% -- because equivalent requests now take the same path through the rules and so land on the same node. On structured circuits it is neutral: gen -N 20 -m and gen -N 24 -a give identical AND counts through strash and dc2, and cec reports the results equivalent in both builds. Note that this changes the AIG built for a given sequence of Aig_And calls, and so anything derived from it, including CNF.
TrevorHansen
force-pushed
the
upstream-commutative-and
branch
from
August 29, 2026 12:34
265b8f1 to
fce0338
Compare
Author
|
I reopened this in #554 because I accidentally closed this by deleting the head repo. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
ANDs' operands are ordered by regular id, but if
fAddStrashis enabled, afterp0's children are compared againstp1's .A different node can be a produced when
p0andp1are swapped. That isAig_And(p0, p1)does not necessarily produce the same result asAig_And(p1, p0).This patch makes
Aig_Andcommutative whenfAddStreshis enabled.