Updates to arithmetic verification.

4 files changed, 152 insertions, 143 deletions

diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c
index a2341704..1a575fbe 100644
--- a/src/proof/acec/acecCore.c
+++ b/src/proof/acec/acecCore.c
@@ -319,7 +319,7 @@ void Vec_IntInsertOrder( Vec_Int_t * vLits, Vec_Int_t * vClasses, int Lit, int C
 void Acec_MoveDuplicates( Vec_Wec_t * vLits, Vec_Wec_t * vClasses )
 {
     Vec_Int_t * vLevel1, * vLevel2; 
-    int i, k, Prev, This, Entry;
+    int i, k, Prev, This, Entry, Counter = 0;
     Vec_WecForEachLevel( vLits, vLevel1, i )
     {
         if ( i == Vec_WecSize(vLits) - 1 )
@@ -347,8 +347,10 @@ void Acec_MoveDuplicates( Vec_Wec_t * vLits, Vec_Wec_t * vClasses )
 
             assert( Vec_IntSize(vLevel1)                  == Vec_IntSize(vLevel2) );
             assert( Vec_IntSize(Vec_WecEntry(vLits, i+1)) == Vec_IntSize(Vec_WecEntry(vClasses, i+1)) );
+            Counter++;
         }
     }
+    printf( "Moved %d pairs of PPs to normalize the matrix.\n", Counter );
 }
 
 void Acec_MatchCheckShift( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * vMap0, Vec_Int_t * vMap1, Vec_Wec_t * vRoots0, Vec_Wec_t * vRoots1 )
@@ -490,12 +492,14 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
     Gia_Man_t * pMiter;
     Gia_Man_t * pGia0n = pGia0, * pGia1n = pGia1;
     Cec_ParCec_t ParsCec, * pCecPars = &ParsCec;
-    Vec_Bit_t * vIgnore0 = pPars->fBooth ? Acec_BoothFindPPG(pGia0) : NULL;
-    Vec_Bit_t * vIgnore1 = pPars->fBooth ? Acec_BoothFindPPG(pGia1) : NULL;
-    Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, vIgnore0, 0, 0, pPars->fVerbose );
-    Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, 0, 0, pPars->fVerbose );
-    Vec_BitFreeP( &vIgnore0 );
-    Vec_BitFreeP( &vIgnore1 );
+//    Vec_Bit_t * vIgnore0 = pPars->fBooth ? Acec_BoothFindPPG(pGia0) : NULL;
+//    Vec_Bit_t * vIgnore1 = pPars->fBooth ? Acec_BoothFindPPG(pGia1) : NULL;
+//    Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, vIgnore0, 0, 0, pPars->fVerbose );
+//    Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, 0, 0, pPars->fVerbose );
+//    Vec_BitFreeP( &vIgnore0 );
+//    Vec_BitFreeP( &vIgnore1 );
+    Acec_Box_t * pBox0 = Acec_ProduceBox( pGia0, pPars->fVerbose );
+    Acec_Box_t * pBox1 = Acec_ProduceBox( pGia1, pPars->fVerbose );
     if ( pBox0 == NULL || pBox1 == NULL ) // cannot match
         printf( "Cannot find arithmetic boxes in both LHS and RHS. Trying regular CEC.\n" );
     else if ( !Acec_MatchBoxes( pBox0, pBox1 ) ) // cannot find matching
diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h
index 47a32e78..381ab8d1 100644
--- a/src/proof/acec/acecInt.h
+++ b/src/proof/acec/acecInt.h
@@ -88,7 +88,7 @@ extern void          Acec_BoxFreeP( Acec_Box_t ** ppBox );
 extern void          Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose );
 extern Vec_Int_t *   Gia_PolynCollectLastXor( Gia_Man_t * pGia, int fVerbose );
 /*=== acecUtil.c ========================================================*/
-extern Acec_Box_t *  Acec_DetectXorTrees( Gia_Man_t * p, int fVerbose );
+extern Acec_Box_t *  Acec_ProduceBox( Gia_Man_t * p, int fVerbose );
 
 
 
diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c
index 330a5d58..ab17d7b9 100644
--- a/src/proof/acec/acecTree.c
+++ b/src/proof/acec/acecTree.c
@@ -333,6 +333,37 @@ void Acec_TreeVerifyPhases2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxe
     Vec_BitFree( vPhase );
     Vec_BitFree( vRoots );
 }
+void Acec_TreeVerifyConnections( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes )
+{
+    Vec_Int_t * vCounts = Vec_IntStartFull( Gia_ManObjNum(p) );
+    Vec_Int_t * vLevel;
+    int i, k, n, Box;
+    // mark outputs
+    Vec_WecForEachLevel( vBoxes, vLevel, i )
+        Vec_IntForEachEntry( vLevel, Box, k )
+        {
+            Vec_IntWriteEntry( vCounts, Vec_IntEntry( vAdds, 6*Box+3 ), 0 );
+            Vec_IntWriteEntry( vCounts, Vec_IntEntry( vAdds, 6*Box+4 ), 0 );
+        }
+    // count fanouts
+    Vec_WecForEachLevel( vBoxes, vLevel, i )
+        Vec_IntForEachEntry( vLevel, Box, k )
+            for ( n = 0; n < 3; n++ )
+                if ( Vec_IntEntry( vCounts, Vec_IntEntry(vAdds, 6*Box+n) ) != -1 )
+                    Vec_IntAddToEntry( vCounts, Vec_IntEntry(vAdds, 6*Box+n), 1 );
+    // print out
+    printf( "The adder tree has %d internal cut points. ", Vec_IntCountLarger(vCounts, -1) );
+    if ( Vec_IntCountLarger(vCounts, 1) == 0 )
+        printf( "There is no internal fanouts.\n" );
+    else
+    {
+        printf( "These %d points have more than one fanout:\n", Vec_IntCountLarger(vCounts, 1) );
+        Vec_IntForEachEntry( vCounts, Box, i )
+            if ( Box > 1 )
+                printf( "Node %d(lev %d) has fanout %d.\n", i, Gia_ObjLevelId(p, i), Box );
+    }
+    Vec_IntFree( vCounts );
+}
 
 /**Function*************************************************************
 
@@ -534,7 +565,7 @@ void Acec_TreeFindTreesTest( Gia_Man_t * p )
   SideEffects []
 
   SeeAlso     []
-
+`
 ***********************************************************************/
 void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds )
 {
@@ -560,6 +591,10 @@ void Acec_TreePrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds )
     Vec_WecPrintLits( pBox->vLeafLits );
     printf( "Outputs:\n" );
     Vec_WecPrintLits( pBox->vRootLits );
+//    printf( "Node %d has level %d.\n", 3715, Gia_ObjLevelId(pBox->pGia, 3715) );
+//    printf( "Node %d has level %d.\n", 167, Gia_ObjLevelId(pBox->pGia, 167) );
+//    printf( "Node %d has level %d.\n", 278, Gia_ObjLevelId(pBox->pGia, 278) );
+//    printf( "Node %d has level %d.\n", 597, Gia_ObjLevelId(pBox->pGia, 597) );
 }
 
 int Acec_CreateBoxMaxRank( Vec_Int_t * vTree )
diff --git a/src/proof/acec/acecXor.c b/src/proof/acec/acecXor.c
index ae5aeff7..acbde1a0 100644
--- a/src/proof/acec/acecXor.c
+++ b/src/proof/acec/acecXor.c
@@ -44,43 +44,43 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Acec_OrderXorRoots( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vXorRoots, Vec_Wec_t * vXorTrees, Vec_Int_t * vMap )
+Vec_Int_t * Acec_OrderTreeRoots( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vXorRoots, Vec_Int_t * vRanks )
 {
-    Vec_Int_t * vOrder = Vec_IntAlloc( Vec_WecSize(vXorTrees) );
-    Vec_Int_t * vReMap = Vec_IntStartFull( Vec_WecSize(vXorTrees) );
+    Vec_Int_t * vOrder = Vec_IntAlloc( Vec_IntSize(vXorRoots) );
+    Vec_Int_t * vMove = Vec_IntStartFull( Vec_IntSize(vXorRoots) );
     int i, k, Entry, This;
     // iterate through adders and for each try mark the next one
     for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
     {
         int Node = Vec_IntEntry(vAdds, 6*i+4);
-        if ( Vec_IntEntry(vMap, Node) == -1 )
+        if ( Vec_IntEntry(vRanks, Node) == -1 )
             continue;
         for ( k = 0; k < 3; k++ )
         {
             int Fanin = Vec_IntEntry(vAdds, 6*i+k);
-            if ( Vec_IntEntry(vMap, Fanin) == -1 )
+            if ( Vec_IntEntry(vRanks, Fanin) == -1 )
                 continue;
-            //printf( "%4d:  %2d -> %2d\n", Node, Vec_IntEntry(vMap, Node), Vec_IntEntry(vMap, Fanin) );
-            Vec_IntWriteEntry( vReMap, Vec_IntEntry(vMap, Node), Vec_IntEntry(vMap, Fanin) );
+            //printf( "%4d:  %2d -> %2d\n", Node, Vec_IntEntry(vRanks, Node), Vec_IntEntry(vRanks, Fanin) );
+            Vec_IntWriteEntry( vMove, Vec_IntEntry(vRanks, Node), Vec_IntEntry(vRanks, Fanin) );
         }
     }
-//Vec_IntPrint( vReMap );
+//Vec_IntPrint( vMove );
     // find reodering
-    Vec_IntForEachEntry( vReMap, Entry, i )
-        if ( Entry == -1 && Vec_IntFind(vReMap, i) >= 0 )
+    Vec_IntForEachEntry( vMove, Entry, i )
+        if ( Entry == -1 && Vec_IntFind(vMove, i) >= 0 )
             break;
-    assert( i < Vec_IntSize(vReMap) );
+    assert( i < Vec_IntSize(vMove) );
     while ( 1 )
     {
         Vec_IntPush( vOrder, Vec_IntEntry(vXorRoots, i) );
         Entry = i;
-        Vec_IntForEachEntry( vReMap, This, i )
+        Vec_IntForEachEntry( vMove, This, i )
             if ( This == Entry )
                 break;
-        if ( i == Vec_IntSize(vReMap) )
+        if ( i == Vec_IntSize(vMove) )
             break;
     }
-    Vec_IntFree( vReMap );
+    Vec_IntFree( vMove );
 //Vec_IntPrint( vOrder );
     return vOrder;
 }
@@ -96,27 +96,24 @@ Vec_Int_t * Acec_OrderXorRoots( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vX
   SeeAlso     []
 
 ***********************************************************************/
-// marks nodes appearing as fanins to XORs
-Vec_Bit_t * Acec_MapXorIns( Gia_Man_t * p, Vec_Int_t * vXors )
+// marks XOR outputs
+Vec_Bit_t * Acec_MapXorOuts( Gia_Man_t * p, Vec_Int_t * vXors )
 {
     Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(p) ); int i;
     for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
-    {
-        Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i+1), 1 );
-        Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i+2), 1 );
-        Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i+3), 1 );
-    }
+        Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i), 1 );
     return vMap;
 }
-// marks nodes having XOR cuts
-Vec_Bit_t * Acec_MapXorOuts( Gia_Man_t * p, Vec_Int_t * vXors )
+// marks XOR outputs participating in trees
+Vec_Bit_t * Acec_MapXorOuts2( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vRanks )
 {
     Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(p) ); int i;
     for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
-        Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i), 1 );
+        if ( Vec_IntEntry(vRanks, Vec_IntEntry(vXors, 4*i)) != -1 )
+            Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i), 1 );
     return vMap;
 }
-// marks nodes appearing as outputs of MAJs
+// marks MAJ outputs
 Vec_Bit_t * Acec_MapMajOuts( Gia_Man_t * p, Vec_Int_t * vAdds )
 {
     Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(p) ); int i;
@@ -124,25 +121,24 @@ Vec_Bit_t * Acec_MapMajOuts( Gia_Man_t * p, Vec_Int_t * vAdds )
         Vec_BitWriteEntry( vMap, Vec_IntEntry(vAdds, 6*i+4), 1 );
     return vMap;
 }
-// maps MAJ outputs into their FAs and HAs
-Vec_Int_t * Acec_MapMajOutsToAdds( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vXorOuts, Vec_Int_t * vMapRank )
+// marks MAJ outputs participating in trees
+Vec_Int_t * Acec_MapMajOuts2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vRanks )
 {
     Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); int i;
     for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+        if ( Vec_IntEntry(vRanks, Vec_IntEntry(vAdds, 6*i+4)) != -1 )
+            Vec_IntWriteEntry( vMap, Vec_IntEntry(vAdds, 6*i+4), i );
+    return vMap;
+}
+// marks nodes appearing as fanins to XORs
+Vec_Bit_t * Acec_MapXorIns( Gia_Man_t * p, Vec_Int_t * vXors )
+{
+    Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(p) ); int i;
+    for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
     {
-        int Xor = Vec_IntEntry(vAdds, 6*i+3);
-        int Maj = Vec_IntEntry(vAdds, 6*i+4);
-        if ( Vec_IntEntry(vMap, Maj) >= 0 )
-        {
-            int i2 = Vec_IntEntry(vMap, Maj);
-            int Xor2 = Vec_IntEntry(vAdds, 6*i2+3);
-            int Maj2 = Vec_IntEntry(vAdds, 6*i2+4);
-            printf( "*** Node %d has two MAJ adder drivers: %d%s (%d  rank %d) and %d%s (%d  rank %d).\n", 
-                Maj, 
-                i, Vec_IntEntry(vAdds, 6*i+2) ? "":"*", Vec_BitEntry(vXorOuts, Xor), Vec_IntEntry(vMapRank, Xor),
-                i2, Vec_IntEntry(vAdds, 6*i2+2) ? "":"*", Vec_BitEntry(vXorOuts, Xor2), Vec_IntEntry(vMapRank, Xor2) );
-        }
-        Vec_IntWriteEntry( vMap, Vec_IntEntry(vAdds, 6*i+4), i );
+        Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i+1), 1 );
+        Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i+2), 1 );
+        Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i+3), 1 );
     }
     return vMap;
 }
@@ -159,103 +155,83 @@ Vec_Int_t * Acec_FindXorRoots( Gia_Man_t * p, Vec_Int_t * vXors )
     return vXorRoots;
 }
 // collects XOR trees belonging to each of XOR roots
-Vec_Wec_t * Acec_FindXorTrees( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vXorRoots, Vec_Int_t ** pvMap )
+Vec_Int_t * Acec_RankTrees( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vXorRoots )
 {
     Vec_Int_t * vDoubles = Vec_IntAlloc( 100 );
-    Vec_Wec_t * vXorTrees = Vec_WecStart( Vec_IntSize(vXorRoots) );
-    Vec_Int_t * vLevel;
     int i, k, Entry;
-    // map roots into their classes
-    Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); 
+    // map roots into their ranks
+    Vec_Int_t * vRanks = Vec_IntStartFull( Gia_ManObjNum(p) ); 
     Vec_IntForEachEntry( vXorRoots, Entry, i )
-    {
-        Vec_IntWriteEntry( vMap, Entry, i );
-        Vec_WecPush( vXorTrees, i, Entry );
-    }
-    // map nodes into their classes
+        Vec_IntWriteEntry( vRanks, Entry, i );
+    // map nodes into their ranks
     for ( i = Vec_IntSize(vXors)/4 - 1; i >= 0; i-- )
     {
         int Root = Vec_IntEntry( vXors, 4*i );
-        int Repr = Vec_IntEntry( vMap, Root );
-        //assert( Repr != -1 );
-        if ( Repr == -1 )
+        int Rank = Vec_IntEntry( vRanks, Root );
+        // skip XORs that are not part of any tree
+        if ( Rank == -1 )
             continue;
+        // iterate through XOR inputs
         for ( k = 1; k < 4; k++ )
         {
             int Node = Vec_IntEntry( vXors, 4*i+k );
-            if ( Node == 0 )
+            if ( Node == 0 ) // HA
                 continue;
-            Entry = Vec_IntEntry( vMap, Node );
-            if ( Entry == Repr )
+            Entry = Vec_IntEntry( vRanks, Node );
+            if ( Entry == Rank ) // the same tree
                 continue;
             if ( Entry == -1 )
-            {
-                Vec_IntWriteEntry( vMap, Node, Repr );
-                Vec_WecPush( vXorTrees, Repr, Node );
-                continue;
-            }
-            //printf( "Node %d belongs to Tree %d and Tree %d.\n", Node, Entry, Repr );
-            Vec_IntPushUnique( Vec_WecEntry(vXorTrees, Entry), Node );
-            Vec_IntPush( vDoubles, Node );
+                Vec_IntWriteEntry( vRanks, Node, Rank );
+            else
+                Vec_IntPush( vDoubles, Node );
+            //if ( Entry != -1 )
+            //printf( "Xor node %d belongs to Tree %d and Tree %d.\n", Node, Entry, Rank );
         }
     }
-    // clean map 
+    // remove duplicated entries
     Vec_IntForEachEntry( vDoubles, Entry, i )
-        Vec_IntWriteEntry( vMap, Entry, -1 );
+        Vec_IntWriteEntry( vRanks, Entry, -1 );
     Vec_IntFree( vDoubles );
-    // sort nodes
-    Vec_WecForEachLevel( vXorTrees, vLevel, i )
-        Vec_IntSort( vLevel, 0 );
-    if ( pvMap )
-        *pvMap = vMap;
-    else
-        Vec_IntFree( vMap );
-    return vXorTrees;
+    return vRanks;
 }
 // collects leaves of each XOR tree
-Vec_Wec_t * Acec_FindXorLeaves( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vAdds, Vec_Wec_t * vXorTrees, Vec_Int_t * vMap, Vec_Wec_t ** pvAddBoxes )
+Vec_Wec_t * Acec_FindXorLeaves( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vAdds, Vec_Int_t * vXorRoots, Vec_Int_t * vRanks, Vec_Wec_t ** pvAddBoxes )
 {
-    Vec_Bit_t * vMapXorOuts = Acec_MapXorOuts( p, vXors );
-    Vec_Int_t * vMapMajOuts = Acec_MapMajOutsToAdds( p, vAdds, vMapXorOuts, vMap );
-    Vec_Wec_t * vXorLeaves = Vec_WecStart( Vec_WecSize(vXorTrees) );
+    Vec_Bit_t * vMapXors = Acec_MapXorOuts2( p, vXors, vRanks );
+    Vec_Int_t * vMapMajs = Acec_MapMajOuts2( p, vAdds, vRanks );
+    Vec_Wec_t * vXorLeaves = Vec_WecStart( Vec_IntSize(vXorRoots) );
+    Vec_Wec_t * vAddBoxes  = Vec_WecStart( Vec_IntSize(vXorRoots) );
     int i, k;
-    if ( pvAddBoxes )
-        *pvAddBoxes = Vec_WecStart( Vec_WecSize(vXorTrees) );
-    // collect leaves
     for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
     {
         int Xor = Vec_IntEntry(vXors, 4*i);
+        int Rank = Vec_IntEntry(vRanks, Xor);
+        if ( Rank == -1 )
+            continue;
         for ( k = 1; k < 4; k++ )
         {
-            int Node = Vec_IntEntry(vXors, 4*i+k);
-            if ( Node == 0 )
+            int Fanin = Vec_IntEntry(vXors, 4*i+k);
+            if ( Fanin == 0 )
                 continue;
-            if ( Vec_BitEntry(vMapXorOuts, Node) || Vec_IntEntry(vMap, Xor) == -1 )
+            if ( Vec_BitEntry(vMapXors, Fanin) )
+            {
+                assert( Rank == Vec_IntEntry(vRanks, Fanin) );
                 continue;
-            if ( Vec_IntEntry(vMapMajOuts, Node) == -1 ) // no maj driver
-                Vec_WecPush( vXorLeaves, Vec_IntEntry(vMap, Xor), Node );
-            else if ( pvAddBoxes && Vec_IntEntry(vMap, Xor) > 0 ) // save adder box
-                Vec_WecPush( *pvAddBoxes, Vec_IntEntry(vMap, Xor)-1, Vec_IntEntry(vMapMajOuts, Node) );
+            }
+            if ( Vec_IntEntry(vMapMajs, Fanin) == -1 ) // no adder driving this input
+                Vec_WecPush( vXorLeaves, Rank, Fanin );
+            else if ( Vec_IntEntry(vRanks, Xor) > 0 ) // save adder box
+                Vec_WecPush( vAddBoxes, Rank-1, Vec_IntEntry(vMapMajs, Fanin) );
         }
     }
-/*
+    Vec_BitFree( vMapXors );
+    Vec_IntFree( vMapMajs );
     if ( pvAddBoxes )
-    {
-        Vec_Int_t * vLevel;
-        //Vec_WecPrint( *pvAddBoxes, 0 );
-        Vec_WecForEachLevelReverse( *pvAddBoxes, vLevel, i )
-            if ( Vec_IntSize(vLevel) > 0 )
-                break;
-        Vec_WecShrink( *pvAddBoxes, i+1 );
-        //Vec_WecPrint( *pvAddBoxes, 0 );
-    }
-*/
-    Vec_BitFree( vMapXorOuts );
-    Vec_IntFree( vMapMajOuts );
+        *pvAddBoxes = vAddBoxes;
     return vXorLeaves;
 }
 
-Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBoxes, Vec_Wec_t * vXorTrees, Vec_Wec_t * vXorLeaves )
+Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBoxes, Vec_Wec_t * vXorLeaves, Vec_Int_t * vXorRoots )
 {
     extern Vec_Int_t * Acec_TreeCarryMap( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes );
     extern void Acec_TreePhases_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, int Node, int fPhase, Vec_Bit_t * vVisit );
@@ -275,8 +251,8 @@ Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBox
     pBox->vLeafLits   = Vec_WecStart( MaxRank + 0 );
     pBox->vRootLits   = Vec_WecStart( MaxRank + 0 );
 
-    assert( Vec_WecSize(vAddBoxes) == Vec_WecSize(vXorTrees) );
     assert( Vec_WecSize(vAddBoxes) == Vec_WecSize(vXorLeaves) );
+    assert( Vec_WecSize(vAddBoxes) == Vec_IntSize(vXorRoots) );
 
     // collect boxes; mark inputs/outputs
     Vec_WecForEachLevel( pBox->vAdds, vLevel, i )
@@ -332,12 +308,7 @@ Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBox
             Vec_IntPush( vLevel, Abc_Var2Lit(Node, 0) );
     }
     vLevel  = Vec_WecEntry( pBox->vRootLits, Vec_WecSize(pBox->vRootLits)-1 );
-    vLevel2 = Vec_WecEntry( vXorTrees, Vec_WecSize(vXorTrees)-1 );
-    Vec_IntClear( vLevel );
-    if ( Vec_IntSize(vLevel) == 0 && Vec_IntSize(vLevel2) > 0 )
-    {
-        Vec_IntPush( vLevel, Abc_Var2Lit(Vec_IntEntryLast(vLevel2), 0) );
-    }
+    Vec_IntFill( vLevel, 1, Abc_Var2Lit(Vec_IntEntryLast(vXorRoots), 0) );
 
     // sort each level
     Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
@@ -347,50 +318,49 @@ Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBox
     return pBox;
 }
 
-Acec_Box_t * Acec_DetectXorTrees( Gia_Man_t * p, int fVerbose )
+Acec_Box_t * Acec_ProduceBox( Gia_Man_t * p, int fVerbose )
 {
+    extern void Acec_TreeVerifyConnections( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes );
+
     abctime clk = Abc_Clock();
     Acec_Box_t * pBox = NULL;
     Vec_Int_t * vXors, * vAdds = Ree_ManComputeCuts( p, &vXors, 0 );
-    Vec_Int_t * vMap, * vXorRootsNew;
-    Vec_Int_t * vXorRoots = Acec_FindXorRoots( p, vXors ); 
-    Vec_Wec_t * vXorTrees = Acec_FindXorTrees( p, vXors, vXorRoots, &vMap ); 
+    Vec_Int_t * vTemp, * vXorRoots = Acec_FindXorRoots( p, vXors ); 
+    Vec_Int_t * vRanks = Acec_RankTrees( p, vXors, vXorRoots ); 
     Vec_Wec_t * vXorLeaves, * vAddBoxes = NULL; 
 
+    Gia_ManLevelNum(p);
+
     //Ree_ManPrintAdders( vAdds, 1 );
     printf( "Detected %d full-adders and %d half-adders.  Found %d XOR-cuts.  ", Ree_ManCountFadds(vAdds), Vec_IntSize(vAdds)/6-Ree_ManCountFadds(vAdds), Vec_IntSize(vXors)/4 );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
-//    printf( "XOR roots: \n" );
-//    Vec_IntPrint( vXorRoots );
-//    Vec_WecPrint( vXorTrees, 0 );
+    vXorRoots = Acec_OrderTreeRoots( p, vAdds, vTemp = vXorRoots, vRanks );
+    Vec_IntFree( vTemp );
+    Vec_IntFree( vRanks );
 
-    vXorRootsNew = Acec_OrderXorRoots( p, vAdds, vXorRoots, vXorTrees, vMap );
-    Vec_IntFree( vXorRoots );
-    Vec_WecFree( vXorTrees );
-    Vec_IntFree( vMap );
+    vRanks = Acec_RankTrees( p, vXors, vXorRoots ); 
+    vXorLeaves = Acec_FindXorLeaves( p, vXors, vAdds, vXorRoots, vRanks, &vAddBoxes ); 
+    Vec_IntFree( vRanks );
 
-    vXorRoots = vXorRootsNew; vXorRootsNew = NULL;
-    vXorTrees = Acec_FindXorTrees( p, vXors, vXorRoots, &vMap ); 
-    vXorLeaves = Acec_FindXorLeaves( p, vXors, vAdds, vXorTrees, vMap, &vAddBoxes ); 
+    //printf( "XOR roots after reordering: \n" );
+    //Vec_IntPrint( vXorRoots );
+    //printf( "XOR leaves: \n" );
+    //Vec_WecPrint( vXorLeaves, 0 );
+    //printf( "Adder boxes: \n" );
+    //Vec_WecPrint( vAddBoxes, 0 );
 
-    printf( "XOR roots: \n" );
-    Vec_IntPrint( vXorRoots );
-    printf( "XOR leaves: \n" );
-    Vec_WecPrint( vXorLeaves, 0 );
-    printf( "Adder boxes: \n" );
-    Vec_WecPrint( vAddBoxes, 0 );
+    Acec_TreeVerifyConnections( p, vAdds, vAddBoxes );
 
-    pBox = Acec_FindBox( p, vAdds, vAddBoxes, vXorTrees, vXorLeaves );
+    pBox = Acec_FindBox( p, vAdds, vAddBoxes, vXorLeaves, vXorRoots );
+    //Vec_WecFree( vAddBoxes );
 
-    Acec_TreePrintBox( pBox, vAdds );
+    if ( fVerbose )
+        Acec_TreePrintBox( pBox, vAdds );
 
     Vec_IntFree( vXorRoots );
-    Vec_WecFree( vXorTrees );
     Vec_WecFree( vXorLeaves );
-    //Vec_WecFree( vAddBoxes );
 
-    Vec_IntFree( vMap );
     Vec_IntFree( vXors );
     Vec_IntFree( vAdds );