From fce0338b33b5528e21c4f70adce95e6c371be396 Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Sat, 29 Aug 2026 21:51:30 +1000 Subject: [PATCH] aig: canonicalize operands before the two-level rules 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. --- src/aig/aig/aigOper.c | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/aig/aig/aigOper.c b/src/aig/aig/aigOper.c index d6f02a6e0b..63f8717cec 100644 --- a/src/aig/aig/aigOper.c +++ b/src/aig/aig/aigOper.c @@ -118,6 +118,8 @@ Aig_Obj_t * Aig_And( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 ) if ( p->fAddStrash && (Aig_ObjIsNode(Aig_Regular(p0)) || Aig_ObjIsNode(Aig_Regular(p1))) ) { // http://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf Aig_Obj_t * pFanA, * pFanB, * pFanC, * pFanD; + if ( Aig_Regular(p0)->Id > Aig_Regular(p1)->Id ) + ABC_SWAP( Aig_Obj_t *, p0, p1 ); pFanA = Aig_ObjChild0(Aig_Regular(p0)); pFanB = Aig_ObjChild1(Aig_Regular(p0)); pFanC = Aig_ObjChild0(Aig_Regular(p1));