Updates to arithmetic verification.

5 files changed, 326 insertions, 278 deletions

diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c
index 28e874bf..cf89d942 100644
--- a/src/aig/gia/giaShow.c
+++ b/src/aig/gia/giaShow.c
@@ -52,7 +52,7 @@ void Gia_ShowPath( Gia_Man_t * p, char * pFileName )
     Gia_Obj_t * pNode;
     Vec_Bit_t * vPath = Vec_BitStart( Gia_ManObjNum(p) );
     int i, k, iFan, LevelMax, nLevels, * pLevels, Level, Prev;
-    int nLuts = 0, nNodes = 0, nEdges = 0, nEdgesAll = 0;
+    int nLuts = 0, nNodes = 0, nEdges = 0;
     assert( Gia_ManHasMapping(p) );
 
     // set critical CO drivers
@@ -670,7 +670,7 @@ int Gia_ShowAddOut( Vec_Int_t * vAdds, Vec_Int_t * vMapAdds, int Node )
         return Vec_IntEntry( vAdds, 6*iBox+4 );
     return Node;
 }
-void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_Int_t * vXors, Vec_Int_t * vMapAdds, Vec_Int_t * vMapXors, Vec_Int_t * vOrder )
+void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_Int_t * vAdds, Vec_Int_t * vXors, Vec_Int_t * vMapAdds, Vec_Int_t * vMapXors, Vec_Int_t * vOrder )
 {
     FILE * pFile;
     Gia_Obj_t * pNode;//, * pTemp, * pPrev;
@@ -689,6 +689,11 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In
         return;
     }
 
+    // mark the nodes
+    if ( vBold )
+        Gia_ManForEachObjVec( vBold, p, pNode, i )
+            pNode->fMark0 = 1;
+
     // compute levels
     LevelMax = 1 + p->nLevels;
     Gia_ManForEachCo( p, pNode, i )
@@ -819,7 +824,7 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In
             else
                 fprintf( pFile, ", shape = ellipse" );
 */
-            if ( Vec_IntEntry(vMapAdds, iNode) >= 0 )
+            if ( !pNode->fMark0 && Vec_IntEntry(vMapAdds, iNode) >= 0 )
             {
                 int iBox = Vec_IntEntry(vMapAdds, iNode);
                 fprintf( pFile, "  Node%d [label = \"%d_%d\"", Gia_ShowAddOut(vAdds, vMapAdds, iNode), Vec_IntEntry(vAdds, 6*iBox+3), Vec_IntEntry(vAdds, 6*iBox+4) ); 
@@ -848,8 +853,8 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In
                 fprintf( pFile, "  Node%d [label = \"%d\"", iNode, iNode ); 
                 fprintf( pFile, ", shape = ellipse" );
             }
-//            if ( pNode->fMark0 )
-//                fprintf( pFile, ", style = filled" );
+            if ( pNode->fMark0 )
+                fprintf( pFile, ", style = filled" );
             fprintf( pFile, "];\n" );
         }
         fprintf( pFile, "}" );
@@ -920,8 +925,6 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In
     Gia_ManForEachObjVec( vOrder, p, pNode, i )
     {
         int iNode = Gia_ObjId( p, pNode );
-//        if ( !Gia_ObjIsAnd(pNode) && !Gia_ObjIsCo(pNode) && !Gia_ObjIsBuf(pNode) )
-//            continue;
         if ( Vec_IntEntry(vMapAdds, Gia_ObjId(p, pNode)) >= 0 )
         {
             int k, iBox = Vec_IntEntry(vMapAdds, iNode);
@@ -990,6 +993,11 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In
     fprintf( pFile, "\n" );
     fclose( pFile );
 
+    // unmark nodes
+    if ( vBold )
+        Gia_ManForEachObjVec( vBold, p, pNode, i )
+            pNode->fMark0 = 0;
+
     Vec_IntFreeP( &p->vLevels );
 }
 
@@ -1093,12 +1101,12 @@ Vec_Int_t * Gia_ShowCollectObjs( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * v
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_Int_t * vXors, int fFadds )
+void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_Int_t * vAdds, Vec_Int_t * vXors, int fFadds )
 {
     Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds, fFadds );
     Vec_Int_t * vMapXors = Gia_ShowMapXors( p, vXors );
     Vec_Int_t * vOrder = Gia_ShowCollectObjs( p, vAdds, vXors, vMapAdds, vMapXors );
-    Gia_WriteDotAig( p, pFileName, vAdds, vXors, vMapAdds, vMapXors, vOrder );
+    Gia_WriteDotAig( p, pFileName, vBold, vAdds, vXors, vMapAdds, vMapXors, vOrder );
     Vec_IntFree( vMapAdds );
     Vec_IntFree( vMapXors );
     Vec_IntFree( vOrder );
@@ -1121,7 +1129,7 @@ void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds,
     if ( fPath )
         Gia_ShowPath( pMan, FileNameDot );
     else if ( fAdders )
-        Gia_ShowProcess( pMan, FileNameDot, vAdds, vXors, fFadds );
+        Gia_ShowProcess( pMan, FileNameDot, vBold, vAdds, vXors, fFadds );
     else
         Gia_WriteDotAigSimple( pMan, FileNameDot, vBold );
     // visualize the file 
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index b22ac6cd..b49c2dd7 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -645,12 +645,22 @@ void Wlc_IntInsert( Vec_Int_t * vProd, Vec_Int_t * vLevel, int Node, int Level )
 }
 void Wlc_BlastPrintMatrix( Gia_Man_t * p, Vec_Wec_t * vProds )
 {
+    int fVerbose = 0;
     Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
     Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
     Vec_Int_t * vLevel;  word Truth;
     int i, k, iLit; 
     Vec_WecForEachLevel( vProds, vLevel, i )
         Vec_IntForEachEntry( vLevel, iLit, k )
+            if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) )
+                Vec_IntPushUnique( vSupp, Abc_Lit2Var(iLit) );
+    printf( "Booth partial products: %d pps, %d unique, %d nodes.\n", 
+        Vec_WecSizeSize(vProds), Vec_IntSize(vSupp), Gia_ManAndNum(p) );
+    Vec_IntPrint( vSupp );
+
+    if ( fVerbose )
+    Vec_WecForEachLevel( vProds, vLevel, i )
+        Vec_IntForEachEntry( vLevel, iLit, k )
         {
             printf( "Obj = %4d : ", Abc_Lit2Var(iLit) );
             printf( "Compl = %d  ", Abc_LitIsCompl(iLit) );
diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h
index 0dc3f706..125d923f 100644
--- a/src/proof/acec/acecInt.h
+++ b/src/proof/acec/acecInt.h
@@ -42,13 +42,10 @@ struct Acec_Box_t_
 {
     Gia_Man_t *    pGia;      // AIG manager
     Vec_Wec_t *    vAdds;     // adders by rank
-    Vec_Wec_t *    vLeafs;    // leaf literals by rank
-    Vec_Wec_t *    vRoots;    // root literals by rank
     Vec_Wec_t *    vLeafLits; // leaf literals by rank
     Vec_Wec_t *    vRootLits; // root literals by rank
     Vec_Wec_t *    vShared;   // shared leaves
     Vec_Wec_t *    vUnique;   // unique leaves
-    Vec_Bit_t *    vInvHadds; // complemented half adders
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c
index 33c32144..8ccf966e 100644
--- a/src/proof/acec/acecMult.c
+++ b/src/proof/acec/acecMult.c
@@ -20,6 +20,7 @@
 
 #include "acecInt.h"
 #include "misc/extra/extra.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -400,6 +401,15 @@ Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec
                 if ( Vec_IntSize(vSupp) <= 2 ) printf( "       " );
                 printf( "  " );
                 Vec_IntPrint( vSupp );
+                /*
+                if ( Truth == 0xF335ACC0F335ACC0 )
+                {
+                    int iObj = Abc_Lit2Var(iLit);
+                    Gia_Man_t * pGia0 = Gia_ManDupAndCones( p, &iObj, 1, 1 );
+                    Gia_ManShow( pGia0, NULL, 0, 0, 0 );
+                    Gia_ManStop( pGia0 );
+                }
+                */
             }
             // support rank counts
             Vec_IntForEachEntry( vSupp, Entry, j )
@@ -423,6 +433,103 @@ Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec
     return vInputs;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_MultFindPPs_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vBold )
+{
+    Gia_Obj_t * pObj;
+    pObj = Gia_ManObj( p, iObj );
+    if ( pObj->fMark0 )
+        return;
+    pObj->fMark0 = 1;
+    if ( !Gia_ObjIsAnd(pObj) )
+        return;
+    Acec_MultFindPPs_rec( p, Gia_ObjFaninId0(pObj, iObj), vBold );
+    Acec_MultFindPPs_rec( p, Gia_ObjFaninId1(pObj, iObj), vBold );
+    Vec_IntPush( vBold, iObj );
+}
+Vec_Int_t * Acec_MultFindPPs( Gia_Man_t * p )
+{
+    word Saved[32] = {
+        ABC_CONST(0xF335ACC0F335ACC0),
+        ABC_CONST(0x35C035C035C035C0),
+        ABC_CONST(0xD728D728D728D728),
+        ABC_CONST(0xFD80FD80FD80FD80),
+        ABC_CONST(0xACC0ACC0ACC0ACC0),
+        ABC_CONST(0x7878787878787878),
+        ABC_CONST(0x2828282828282828),
+        ABC_CONST(0xD0D0D0D0D0D0D0D0),
+        ABC_CONST(0x8080808080808080),
+        ABC_CONST(0x8888888888888888),
+        ABC_CONST(0xAAAAAAAAAAAAAAAA),
+        ABC_CONST(0x5555555555555555),
+
+        ABC_CONST(0xD5A8D5A8D5A8D5A8),
+        ABC_CONST(0x2A572A572A572A57),
+        ABC_CONST(0xF3C0F3C0F3C0F3C0),
+        ABC_CONST(0x5858585858585858),
+        ABC_CONST(0xA7A7A7A7A7A7A7A7),
+        ABC_CONST(0x2727272727272727),
+        ABC_CONST(0xD8D8D8D8D8D8D8D8)
+    };
+
+    Vec_Int_t * vBold = Vec_IntAlloc( 100 );
+    Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+    Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+    int i, iObj, nProds = 0;
+    Gia_ManCleanMark0(p);
+    Gia_ManForEachAndId( p, iObj )
+    {
+        word Truth = Gia_ObjComputeTruth6Cis( p, Abc_Var2Lit(iObj, 0), vSupp, vTemp );
+        vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
+        if ( Vec_IntSize(vSupp) > 5  )
+            continue;
+        for ( i = 0; i < 32; i++ )
+        {
+            if ( Saved[i] == 0 )
+                break;
+            if ( Truth == Saved[i] || Truth == ~Saved[i] )
+            {
+                //Vec_IntPush( vBold, iObj );
+                Acec_MultFindPPs_rec( p, iObj, vBold );
+                printf( "%d ", iObj );
+                nProds++;
+                break;
+            }
+        }
+/*
+        Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) );
+        if ( Vec_IntSize(vSupp) == 4 ) printf( "    " );
+        if ( Vec_IntSize(vSupp) == 3 ) printf( "      " );
+        if ( Vec_IntSize(vSupp) <= 2 ) printf( "       " );
+        printf( "  " );
+        Vec_IntPrint( vSupp );
+*/
+    }
+    printf( "\n" );
+    Gia_ManCleanMark0(p);
+    printf( "Collected %d pps and %d nodes.\n", nProds, Vec_IntSize(vBold) );
+
+    Vec_IntFree( vSupp );
+    Vec_WrdFree( vTemp );
+    return vBold;
+}
+void Acec_MultFindPPsTest( Gia_Man_t * p )
+{
+    Vec_Int_t * vBold = Acec_MultFindPPs( p );
+    Gia_ManShow( p, vBold, 1, 0, 0 );
+    Vec_IntFree( vBold );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c
index 8be8a340..370e8eb6 100644
--- a/src/proof/acec/acecTree.c
+++ b/src/proof/acec/acecTree.c
@@ -45,13 +45,10 @@ ABC_NAMESPACE_IMPL_START
 void Acec_BoxFree( Acec_Box_t * pBox )
 {
     Vec_WecFreeP( &pBox->vAdds );
-    Vec_WecFreeP( &pBox->vLeafs );
-    Vec_WecFreeP( &pBox->vRoots );
     Vec_WecFreeP( &pBox->vLeafLits );
     Vec_WecFreeP( &pBox->vRootLits );
     Vec_WecFreeP( &pBox->vUnique );
     Vec_WecFreeP( &pBox->vShared );
-    Vec_BitFreeP( &pBox->vInvHadds );
     ABC_FREE( pBox );
 }
 void Acec_BoxFreeP( Acec_Box_t ** ppBox )
@@ -122,6 +119,141 @@ void Acec_TreeFilterTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vTrees
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acec_TreeVerifyPhaseOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    int Truth0, Truth1;
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return pObj->Value;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    assert( Gia_ObjIsAnd(pObj) );
+    assert( !Gia_ObjIsXor(pObj) );
+    Truth0 = Acec_TreeVerifyPhaseOne_rec( p, Gia_ObjFanin0(pObj) );
+    Truth1 = Acec_TreeVerifyPhaseOne_rec( p, Gia_ObjFanin1(pObj) );
+    Truth0 = Gia_ObjFaninC0(pObj) ? 0xFF & ~Truth0 : Truth0;
+    Truth1 = Gia_ObjFaninC1(pObj) ? 0xFF & ~Truth1 : Truth1;
+    return (pObj->Value = Truth0 & Truth1);
+}
+void Acec_TreeVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox )
+{
+    Gia_Obj_t * pObj;
+    unsigned TruthXor, TruthMaj, Truths[3] = { 0xAA, 0xCC, 0xF0 };
+    int k, iObj, fFadd = Vec_IntEntry(vAdds, 6*iBox+2) > 0;
+
+    int Sign = Vec_IntEntry( vAdds, 6*iBox+5 ), Phase[5];
+    for ( k = 0; k < 5; k++ )
+        Phase[k] = (Sign >> (4+k)) & 1;
+
+    Gia_ManIncrementTravId( p );
+    for ( k = 0; k < 3; k++ )
+    {
+        iObj = Vec_IntEntry( vAdds, 6*iBox+k );
+        if ( iObj == 0 )
+            continue;
+        pObj = Gia_ManObj( p, iObj );
+        pObj->Value = Phase[k] ? 0xFF & ~Truths[k] : Truths[k];
+        Gia_ObjSetTravIdCurrent( p, pObj );
+    }
+
+    iObj = Vec_IntEntry( vAdds, 6*iBox+3 );
+    TruthXor = Acec_TreeVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
+    TruthXor = Phase[3] ? 0xFF & ~TruthXor : TruthXor;
+
+    iObj = Vec_IntEntry( vAdds, 6*iBox+4 );
+    TruthMaj = Acec_TreeVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
+    TruthMaj = Phase[4] ? 0xFF & ~TruthMaj : TruthMaj;
+
+    if ( fFadd ) // FADD
+    {
+        if ( TruthXor != 0x96 )
+            printf( "Fadd %d sum %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+3 ) );
+        if ( TruthMaj != 0xE8 )
+            printf( "Fadd %d carry %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+4 ) );
+    }
+    else
+    {
+        if ( TruthXor != 0x66 )
+            printf( "Hadd %d sum %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+3 ) );
+        if ( TruthMaj != 0x88 )
+            printf( "Hadd %d carry %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+4 ) );
+    }
+}
+void Acec_TreeVerifyPhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes )
+{
+    Vec_Int_t * vLevel;
+    int i, k, Box;
+    Vec_WecForEachLevel( vBoxes, vLevel, i )
+        Vec_IntForEachEntry( vLevel, Box, k )
+            Acec_TreeVerifyPhaseOne( p, vAdds, Box );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates polarity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acec_TreeCarryMap( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes )
+{
+    Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
+    Vec_Int_t * vLevel;
+    int i, k, Box;
+    Vec_WecForEachLevel( vBoxes, vLevel, i )
+        Vec_IntForEachEntry( vLevel, Box, k )
+            Vec_IntWriteEntry( vMap, Vec_IntEntry(vAdds, 6*Box+4), Box );
+    return vMap;
+}
+void Acec_TreePhases_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, int Node, int fPhase )
+{
+    int k, iBox, iXor, Sign, fXorPhase, fPhaseThis;
+    assert( Node != 0 );
+    iBox = Vec_IntEntry( vMap, Node );
+    if ( iBox == -1 )
+        return;
+    assert( Node == Vec_IntEntry( vAdds, 6*iBox+4 ) );
+    iXor = Vec_IntEntry( vAdds, 6*iBox+3 );
+    Sign = Vec_IntEntry( vAdds, 6*iBox+5 ) & 0xFFFFFFF0;
+    fXorPhase = ((Sign >> 3) & 1);
+    if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 )
+    {
+        fPhase ^= ((Sign >> 2) & 1);
+        if ( fPhase ) // complemented HADD
+            Sign |= (1 << 6);
+    }
+    for ( k = 0; k < 3; k++ )
+    {
+        int iObj = Vec_IntEntry( vAdds, 6*iBox+k );
+        if ( iObj == 0 )
+            continue;
+        fPhaseThis = ((Sign >> k) & 1) ^ fPhase;
+        fXorPhase ^= fPhaseThis;
+        Acec_TreePhases_rec( p, vAdds, vMap, iObj, fPhaseThis );
+        if ( fPhaseThis )
+            Sign |= (1 << (4+k));
+    }
+    if ( fXorPhase )
+        Sign |= (1 << 7);
+    if ( fPhase )
+        Sign |= (1 << 8);
+    // save updated signature
+    Vec_IntWriteEntry( vAdds, 6*iBox+5, Sign );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Find internal cut points with exactly one adder fanin/fanout.]
 
   Description [Returns a map of point into its input/output adder.]
@@ -251,256 +383,6 @@ void Acec_TreeFindTreesTest( Gia_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Creates leaves and roots.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Acec_CreateBoxMaxRank( Vec_Int_t * vTree )
-{
-    int k, Box, Rank, MaxRank = 0;
-    Vec_IntForEachEntryDouble( vTree, Box, Rank, k )
-        MaxRank = Abc_MaxInt( MaxRank, Rank );
-    return MaxRank;
-}
-void Acec_TreeInsOuts( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree, Vec_Wec_t * vBoxes, Vec_Wec_t * vLeaves, Vec_Wec_t * vRoots )
-{
-    Vec_Bit_t * vIsLeaf = Vec_BitStart( Gia_ManObjNum(p) );
-    Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(p) );
-    Vec_Int_t * vLevel;
-    int i, k, Box, Rank;
-    Vec_BitWriteEntry( vIsLeaf, 0, 1 );
-    Vec_BitWriteEntry( vIsRoot, 0, 1 );
-    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
-    {
-        Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+0), 1 );
-        Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+1), 1 );
-        Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+2), 1 );
-        Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+3), 1 );
-        Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+4), 1 );
-    }
-    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
-    {
-        Vec_WecPush( vBoxes, Rank, Box );
-        for ( k = 0; k < 3; k++ )
-        {
-            if ( Vec_BitEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+k) ) )
-                continue;
-            Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+k), 1 );
-            Vec_WecPush( vLeaves, Rank, Vec_IntEntry(vAdds, 6*Box+k) );
-        }
-        for ( k = 3; k < 5; k++ )
-        {
-            if ( Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+k) ) )
-                continue;
-            Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+k), 1 );
-            Vec_WecPush( vRoots, k == 4 ? Rank + 1 : Rank, Abc_Var2Lit(Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), k==4), Vec_IntEntry(vAdds, 6*Box+2)!=0)  );
-        }
-    }
-    Vec_BitFree( vIsLeaf );
-    Vec_BitFree( vIsRoot );
-    // sort each level
-    Vec_WecForEachLevel( vBoxes, vLevel, i )
-        Vec_IntSort( vLevel, 0 );
-    Vec_WecForEachLevel( vLeaves, vLevel, i )
-        Vec_IntSort( vLevel, 0 );
-    Vec_WecForEachLevel( vRoots, vLevel, i )
-        Vec_IntSort( vLevel, 0 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Acec_TreeVerifyPhaseOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
-{
-    int Truth0, Truth1;
-    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
-        return pObj->Value;
-    Gia_ObjSetTravIdCurrent(p, pObj);
-    assert( Gia_ObjIsAnd(pObj) );
-    assert( !Gia_ObjIsXor(pObj) );
-    Truth0 = Acec_TreeVerifyPhaseOne_rec( p, Gia_ObjFanin0(pObj) );
-    Truth1 = Acec_TreeVerifyPhaseOne_rec( p, Gia_ObjFanin1(pObj) );
-    Truth0 = Gia_ObjFaninC0(pObj) ? 0xFF & ~Truth0 : Truth0;
-    Truth1 = Gia_ObjFaninC1(pObj) ? 0xFF & ~Truth1 : Truth1;
-    return (pObj->Value = Truth0 & Truth1);
-}
-void Acec_TreeVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox, Vec_Bit_t * vPhase )
-{
-    Gia_Obj_t * pObj;
-    unsigned TruthXor, TruthMaj, Truths[3] = { 0xAA, 0xCC, 0xF0 };
-    int k, iObj, fFadd = Vec_IntEntry(vAdds, 6*iBox+2) > 0;
-
-    //if ( !fFadd )
-    //    return;
-
-    Gia_ManIncrementTravId( p );
-    for ( k = 0; k < 3; k++ )
-    {
-        iObj = Vec_IntEntry( vAdds, 6*iBox+k );
-        if ( iObj == 0 )
-            continue;
-        pObj = Gia_ManObj( p, iObj );
-        pObj->Value = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~Truths[k] : Truths[k];
-        Gia_ObjSetTravIdCurrent( p, pObj );
-    }
-
-    iObj = Vec_IntEntry( vAdds, 6*iBox+3 );
-    TruthXor = Acec_TreeVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
-    TruthXor = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthXor : TruthXor;
-
-    iObj = Vec_IntEntry( vAdds, 6*iBox+4 );
-    TruthMaj = Acec_TreeVerifyPhaseOne_rec( p, Gia_ManObj(p, iObj) );
-    TruthMaj = Vec_BitEntry(vPhase, iObj) ? 0xFF & ~TruthMaj : TruthMaj;
-
-    if ( fFadd ) // FADD
-    {
-        if ( TruthXor != 0x96 )
-            printf( "Fadd %d sum %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+3 ) );
-        if ( TruthMaj != 0xE8 )
-            printf( "Fadd %d carry %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+4 ) );
-    }
-    else
-    {
-        if ( TruthXor != 0x66 )
-            printf( "Hadd %d sum %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+3 ) );
-        if ( TruthMaj != 0x88 )
-            printf( "Hadd %d carry %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+4 ) );
-    }
-}
-void Acec_TreeVerifyPhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes, Vec_Bit_t * vPhase )
-{
-    Vec_Int_t * vLevel;
-    int i, k, Box;
-    Vec_WecForEachLevel( vBoxes, vLevel, i )
-        Vec_IntForEachEntry( vLevel, Box, k )
-            Acec_TreeVerifyPhaseOne( p, vAdds, Box, vPhase );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates polarity.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Acec_TreeCarryMap( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes )
-{
-    Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
-    Vec_Int_t * vLevel;
-    int i, k, Box;
-    Vec_WecForEachLevel( vBoxes, vLevel, i )
-        Vec_IntForEachEntry( vLevel, Box, k )
-            Vec_IntWriteEntry( vMap, Vec_IntEntry(vAdds, 6*Box+4), Box );
-    return vMap;
-}
-void Acec_TreePhases_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, int Node, int fPhase,
-                         Vec_Bit_t * vPhase, Vec_Bit_t * vInvHadds, Vec_Bit_t * vVisit )
-{
-    int k, iBox, iXor, Sign, fXorPhase, fPhaseThis;
-    assert( Node != 0 );
-    if ( Vec_BitEntry(vVisit, Node) )
-    {
-        //assert( Vec_BitEntry(vPhase, Node) == fPhase );
-        if ( Vec_BitEntry(vPhase, Node) != fPhase )
-            printf( "Phase check failed for node %d.\n", Node );
-        return;
-    }
-    Vec_BitWriteEntry( vVisit, Node, 1 );
-    if ( fPhase )
-        Vec_BitWriteEntry( vPhase, Node, fPhase );
-    iBox = Vec_IntEntry( vMap, Node );
-    if ( iBox == -1 )
-        return;
-    assert( Node == Vec_IntEntry( vAdds, 6*iBox+4 ) );
-    iXor = Vec_IntEntry( vAdds, 6*iBox+3 );
-    Sign = Vec_IntEntry( vAdds, 6*iBox+5 );
-    fXorPhase = ((Sign >> 3) & 1);
-    if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 )
-    {
-        fPhase ^= ((Sign >> 2) & 1);
-        // remember complemented HADD
-        if ( fPhase )
-            Vec_BitWriteEntry( vInvHadds, iBox, 1 );
-    }
-    for ( k = 0; k < 3; k++ )
-    {
-        int iObj = Vec_IntEntry( vAdds, 6*iBox+k );
-        if ( iObj == 0 )
-            continue;
-        fPhaseThis = ((Sign >> k) & 1) ^ fPhase;
-        fXorPhase ^= fPhaseThis;
-        Acec_TreePhases_rec( p, vAdds, vMap, iObj, fPhaseThis, vPhase, vInvHadds, vVisit );
-    }
-    if ( Vec_BitEntry(vVisit, iXor) )
-    {
-        //assert( Vec_BitEntry(vPhase, iXor) == fXorPhase );
-        if ( Vec_BitEntry(vPhase, iXor) != fXorPhase )
-            printf( "Phase check failed for XOR %d.\n", iXor );
-        return;
-    }
-    if ( fXorPhase )
-        Vec_BitWriteEntry( vPhase, iXor, fXorPhase );
-}
-void Acec_TreePhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes, 
-                     Vec_Wec_t * vLeaves, Vec_Wec_t * vRoots, 
-                     Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits, Vec_Bit_t * vInvHadds )
-{
-    Vec_Int_t * vMap = Acec_TreeCarryMap( p, vAdds, vBoxes );
-    Vec_Bit_t * vPhase = Vec_BitStart( Gia_ManObjNum(p) );
-    Vec_Bit_t * vVisit = Vec_BitStart( Gia_ManObjNum(p) );
-    Vec_Int_t * vLevel;
-    int i, k, iObj;
-    Vec_WecForEachLevelReverse( vRoots, vLevel, i )
-    {
-        Vec_IntForEachEntry( vLevel, iObj, k )
-        {
-            int fFadd = Abc_LitIsCompl(iObj);
-            int fCout = Abc_LitIsCompl(Abc_Lit2Var(iObj));
-            int Node  = Abc_Lit2Var(Abc_Lit2Var(iObj));
-            if ( !fCout )
-                continue;
-            Acec_TreePhases_rec( p, vAdds, vMap, Node, fFadd, vPhase, vInvHadds, vVisit );
-        }
-    }
-    Vec_IntFree( vMap );
-    Vec_BitFree( vVisit );
-    Acec_TreeVerifyPhases( p, vAdds, vBoxes, vPhase );
-    // create leaves
-    Vec_WecForEachLevel( vLeaves, vLevel, i )
-        Vec_IntForEachEntry( vLevel, iObj, k )
-            Vec_WecPush( vLeafLits, i, Abc_Var2Lit(iObj, Vec_BitEntry(vPhase, iObj)) );
-    // add constants
-    Vec_WecForEachLevel( vBoxes, vLevel, i )
-        Vec_IntForEachEntry( vLevel, iObj, k )
-            if ( Vec_BitEntry(vInvHadds, iObj) )
-                Vec_WecPush( vLeafLits, i, 1 );
-    // create roots
-    Vec_WecForEachLevel( vRoots, vLevel, i )
-        Vec_IntForEachEntry( vLevel, iObj, k )
-            iObj >>= 2, Vec_WecPush( vRootLits, i, Abc_Var2Lit(iObj, Vec_BitEntry(vPhase, iObj)) );
-    // cleanup
-    Vec_BitFree( vPhase );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Derives one adder tree.]
 
   Description []
@@ -564,25 +446,69 @@ void Acec_PrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds )
     //Acec_PrintRootLits( pBox->vRoots );
 }
 
+int Acec_CreateBoxMaxRank( Vec_Int_t * vTree )
+{
+    int k, Box, Rank, MaxRank = 0;
+    Vec_IntForEachEntryDouble( vTree, Box, Rank, k )
+        MaxRank = Abc_MaxInt( MaxRank, Rank );
+    return MaxRank;
+}
 Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
 {
     int MaxRank = Acec_CreateBoxMaxRank(vTree);
+    Vec_Bit_t * vIsLeaf = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vLevel, * vMap;
+    int i, k, Box, Rank;
 
     Acec_Box_t * pBox = ABC_CALLOC( Acec_Box_t, 1 );
-    pBox->pGia      = p;
-
-    pBox->vAdds     = Vec_WecStart( MaxRank + 1 );
-    pBox->vLeafs    = Vec_WecStart( MaxRank + 1 );
-    pBox->vRoots    = Vec_WecStart( MaxRank + 2 );
+    pBox->pGia        = p;
+    pBox->vAdds       = Vec_WecStart( MaxRank + 1 );
+    pBox->vLeafLits   = Vec_WecStart( MaxRank + 1 );
+    pBox->vRootLits   = Vec_WecStart( MaxRank + 2 );
 
-    Acec_TreeInsOuts( p, vAdds, vTree, pBox->vAdds, pBox->vLeafs, pBox->vRoots );
-
-    pBox->vLeafLits = Vec_WecStart( Vec_WecSize(pBox->vLeafs) );
-    pBox->vRootLits = Vec_WecStart( Vec_WecSize(pBox->vRoots) );
-    pBox->vInvHadds = Vec_BitStart( Vec_IntSize(vAdds)/6 );
+    // collect boxes; mark inputs/outputs
+    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+    {
+        Vec_WecPush( pBox->vAdds, Rank, Box );
+        Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+0), 1 );
+        Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+1), 1 );
+        Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+2), 1 );
+        Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+3), 1 );
+        Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+4), 1 );
+    }
+    // sort each level
+    Vec_WecForEachLevel( pBox->vAdds, vLevel, i )
+        Vec_IntSort( vLevel, 0 );
 
-    Acec_TreePhases( p, vAdds, pBox->vAdds, pBox->vLeafs, pBox->vRoots, pBox->vLeafLits, pBox->vRootLits, pBox->vInvHadds );
+    // set phases
+    vMap = Acec_TreeCarryMap( p, vAdds, pBox->vAdds );
+    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+        if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4) ) )
+            Acec_TreePhases_rec( p, vAdds, vMap, Vec_IntEntry(vAdds, 6*Box+4), Vec_IntEntry(vAdds, 6*Box+2) != 0 );
+    Acec_TreeVerifyPhases( p, vAdds, pBox->vAdds );
+    Vec_IntFree( vMap );
 
+    // collect inputs/outputs
+    Vec_BitWriteEntry( vIsLeaf, 0, 0 );
+    Vec_BitWriteEntry( vIsRoot, 0, 0 );
+    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+    {
+        int Sign = Vec_IntEntry( vAdds, 6*Box+5 );
+        for ( k = 0; k < 3; k++ )
+            if ( !Vec_BitEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+k) ) )
+                Vec_WecPush( pBox->vLeafLits, Rank, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), (Sign >> (4+k)) & 1) );
+        for ( k = 3; k < 5; k++ )
+            if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+k) ) )
+                Vec_WecPush( pBox->vRootLits, k == 4 ? Rank + 1 : Rank, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), (Sign >> (7+k)) & 1) );
+    }
+    Vec_BitFree( vIsLeaf );
+    Vec_BitFree( vIsRoot );
+    // sort each level
+    Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
+        Vec_IntSort( vLevel, 0 );
+    Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
+        Vec_IntSort( vLevel, 0 );
     return pBox;
 }
 void Acec_CreateBoxTest( Gia_Man_t * p )
@@ -641,7 +567,7 @@ Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, int fVerbose )
             Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits)  );
     if ( pBox && fVerbose )
         Acec_PrintBox( pBox, vAdds );
-    //Acec_MultDetectInputs( p, pBox->vLeafLits, pBox->vRootLits );
+    Acec_MultDetectInputs( p, pBox->vLeafLits, pBox->vRootLits );
     Vec_WecFreeP( &vTrees );
     Vec_IntFree( vAdds );
     return pBox;