Updates to arithmetic verification.

9 files changed, 201 insertions, 35 deletions

diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c
index cf89d942..4dd85aab 100644
--- a/src/aig/gia/giaShow.c
+++ b/src/aig/gia/giaShow.c
@@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define NODE_MAX 2000
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -79,11 +81,11 @@ void Gia_ShowPath( Gia_Man_t * p, char * pFileName )
         }
     }
 
-    if ( nNodes > 500 )
+    if ( nNodes > NODE_MAX )
     {
         ABC_FREE( pLevels );
         Vec_BitFree( vPath );
-        fprintf( stdout, "Cannot visualize AIG with more than 500 critical nodes.\n" );
+        fprintf( stdout, "Cannot visualize AIG with more than %d critical nodes.\n", NODE_MAX );
         return;
     }
     if ( (pFile = fopen( pFileName, "w" )) == NULL )
@@ -341,9 +343,9 @@ void Gia_WriteDotAigSimple( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold )
     int LevelMax, Prev, Level, i;
     int fConstIsUsed = 0;
 
-    if ( Gia_ManAndNum(p) > 500 )
+    if ( Gia_ManAndNum(p) > NODE_MAX )
     {
-        fprintf( stdout, "Cannot visualize AIG with more than 500 nodes.\n" );
+        fprintf( stdout, "Cannot visualize AIG with more than %d nodes.\n", NODE_MAX );
         return;
     }
     if ( (pFile = fopen( pFileName, "w" )) == NULL )
@@ -678,9 +680,9 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_In
     int fConstIsUsed = 0;
     int nFadds = Ree_ManCountFadds( vAdds );
 
-    if ( Gia_ManAndNum(p) > 1000 )
+    if ( Gia_ManAndNum(p) > NODE_MAX )
     {
-        fprintf( stdout, "Cannot visualize AIG with more than 1000 nodes.\n" );
+        fprintf( stdout, "Cannot visualize AIG with more than %d nodes.\n", NODE_MAX );
         return;
     }
     if ( (pFile = fopen( pFileName, "w" )) == NULL )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1e94f28f..9db3d7d6 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -42690,7 +42690,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Jf_ManTestCnf( pAbc->pGia );
 //    Gia_ManCheckFalseTest( pAbc->pGia, nFrames );
 //    Gia_ParTest( pAbc->pGia, nWords, nProcs );
-//    Gia_PolynExplore( pAbc->pGia );
+    Acec_MultFindPPsTest( pAbc->pGia );
 
 //    printf( "\nThis command is currently disabled.\n\n" );
     return 0;
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index f09b8783..d952518f 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -1692,6 +1692,24 @@ static inline int Vec_IntTwoFindCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Ve
     }
     return Vec_IntSize(vArr);
 }
+static inline int Vec_IntTwoFindCommonReverse( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vArr )
+{
+    int * pBeg1 = vArr1->pArray;
+    int * pBeg2 = vArr2->pArray;
+    int * pEnd1 = vArr1->pArray + vArr1->nSize;
+    int * pEnd2 = vArr2->pArray + vArr2->nSize;
+    Vec_IntClear( vArr );
+    while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+    {
+        if ( *pBeg1 == *pBeg2 )
+            Vec_IntPush( vArr, *pBeg1 ), pBeg1++, pBeg2++;
+        else if ( *pBeg1 > *pBeg2 )
+            pBeg1++;
+        else 
+            pBeg2++;
+    }
+    return Vec_IntSize(vArr);
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h
index e4e92503..8180e984 100644
--- a/src/misc/vec/vecWec.h
+++ b/src/misc/vec/vecWec.h
@@ -303,6 +303,23 @@ static inline Vec_Int_t * Vec_WecPushLevel( Vec_Wec_t * p )
     ++p->nSize;
     return Vec_WecEntryLast( p );
 }
+static inline Vec_Int_t * Vec_WecInsertLevel( Vec_Wec_t * p, int i )
+{
+    Vec_Int_t * pTemp;
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Vec_WecGrow( p, 16 );
+        else
+            Vec_WecGrow( p, 2 * p->nCap );
+    }
+    ++p->nSize;
+    assert( i >= 0 && i < p->nSize );
+    for ( pTemp = p->pArray + p->nSize - 2; pTemp >= p->pArray + i; pTemp-- )
+        pTemp[1] = pTemp[0];
+    Vec_IntZero( p->pArray + i );
+    return p->pArray + i;
+}
 
 /**Function*************************************************************
 
diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c
index 4a91663f..6b631a1b 100644
--- a/src/proof/acec/acecCore.c
+++ b/src/proof/acec/acecCore.c
@@ -20,6 +20,8 @@
 
 #include "acecInt.h"
 #include "proof/cec/cec.h"
+#include "misc/util/utilTruth.h"
+#include "misc/extra/extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -118,18 +120,19 @@ Vec_Int_t * Acec_CountRemap( Gia_Man_t * pAdd, Gia_Man_t * pBase )
 }
 void Acec_ComputeEquivClasses( Gia_Man_t * pOne, Gia_Man_t * pTwo, Vec_Int_t ** pvMap1, Vec_Int_t ** pvMap2 )
 {
+    abctime clk = Abc_Clock();
     Gia_Man_t * pBase, * pRepr;
     pBase = Acec_CommonStart( NULL, pOne );
     pBase = Acec_CommonStart( pBase, pTwo );
     Acec_CommonFinish( pBase );
-
     //Gia_ManShow( pBase, NULL, 0, 0, 0 );
-
     pRepr = Gia_ManComputeGiaEquivs( pBase, 100, 0 );
     *pvMap1 = Acec_CountRemap( pOne, pBase );
     *pvMap2 = Acec_CountRemap( pTwo, pBase );
     Gia_ManStop( pBase );
     Gia_ManStop( pRepr );
+    printf( "Finished computing equivalent nodes.  " );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 }
 void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCostLits )
 {
@@ -143,8 +146,10 @@ void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCostLits )
         ABC_SWAP( int, pArray[i], pArray[best_i] );
     }
 }
-void Acec_MatchPrintEquivLits( Vec_Wec_t * vLits, int * pCostLits )
+void Acec_MatchPrintEquivLits( Gia_Man_t * p, Vec_Wec_t * vLits, int * pCostLits, int fVerbose )
 {
+    Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+    Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
     Vec_Int_t * vLevel;
     int i, k, Entry;
     printf( "Leaf literals and their classes:\n" );
@@ -155,6 +160,85 @@ void Acec_MatchPrintEquivLits( Vec_Wec_t * vLits, int * pCostLits )
             printf( "%s%d(%d) ", Abc_LitIsCompl(Entry) ? "-":"+", Abc_Lit2Var(Entry), Abc_Lit2LitL(pCostLits, Entry) );
         printf( "\n" );
     }
+    if ( !fVerbose )
+        return;
+    Vec_WecForEachLevel( vLits, vLevel, i )
+    {
+        if ( i != 20 )
+            continue;
+        Vec_IntForEachEntry( vLevel, Entry, k )
+        {
+            word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp );
+            printf( "Rank = %4d : ", i );
+            printf( "Obj = %4d  ", Abc_Lit2Var(Entry) );
+            if ( Vec_IntSize(vSupp) > 6  )
+            {
+                printf( "Supp = %d.\n", Vec_IntSize(vSupp) );
+                continue;
+            }
+            vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
+            if ( Vec_IntSize(vSupp) > 5  )
+            {
+                printf( "Supp = %d.\n", Vec_IntSize(vSupp) );
+                continue;
+            }
+            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" );
+    }
+    Vec_IntFree( vSupp );
+    Vec_WrdFree( vTemp );
+}
+Vec_Wec_t * Acec_MatchCopy( Vec_Wec_t * vLits, Vec_Int_t * vMap )
+{
+    Vec_Wec_t * vRes = Vec_WecStart( Vec_WecSize(vLits) );
+    Vec_Int_t * vLevel; int i, k, iLit;
+    Vec_WecForEachLevel( vLits, vLevel, i )
+        Vec_IntForEachEntry( vLevel, iLit, k )
+            Vec_WecPush( vRes, i, Abc_Lit2LitL(Vec_IntArray(vMap), iLit) );
+    return vRes;
+}
+int Acec_MatchCountCommon( Vec_Wec_t * vLits1, Vec_Wec_t * vLits2, int Shift )
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+    Vec_Int_t * vLevel1, * vLevel2; 
+    int i, nCommon = 0;
+    Vec_WecForEachLevel( vLits1, vLevel1, i )
+    {
+        if ( i+Shift < 0 || i+Shift >= Vec_WecSize(vLits2) )
+            continue;
+        vLevel2 = Vec_WecEntry( vLits2, i+Shift );
+        nCommon += Vec_IntTwoFindCommonReverse( vLevel1, vLevel2, vRes );
+    }
+    Vec_IntFree( vRes );
+    return nCommon;
+}
+void Acec_MatchCheckShift( Vec_Wec_t * vLits0, Vec_Wec_t * vLits1, Vec_Int_t * vMap0, Vec_Int_t * vMap1, Vec_Wec_t * vRoots0, Vec_Wec_t * vRoots1 )
+{
+    Vec_Wec_t * vRes0 = Acec_MatchCopy( vLits0, vMap0 );
+    Vec_Wec_t * vRes1 = Acec_MatchCopy( vLits1, vMap1 );
+    int nCommon      = Acec_MatchCountCommon( vRes0, vRes1,  0 );
+    int nCommonPlus  = Acec_MatchCountCommon( vRes0, vRes1,  1 );
+    int nCommonMinus = Acec_MatchCountCommon( vRes0, vRes1, -1 );
+    if ( nCommonPlus >= nCommonMinus && nCommonPlus > nCommon )
+    {
+        Vec_WecInsertLevel( vLits0, 0 );
+        Vec_WecInsertLevel( vRoots0, 0 );
+    }
+    else if ( nCommonMinus > nCommonPlus && nCommonMinus > nCommon )
+    {
+        Vec_WecInsertLevel( vLits1, 0 );
+        Vec_WecInsertLevel( vRoots1, 0 );
+    }
+    Vec_WecPrint( vRes0, 0 );
+    Vec_WecPrint( vRes1, 0 );
+    Vec_WecFree( vRes0 );
+    Vec_WecFree( vRes1 );
 }
 int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
 {
@@ -166,8 +250,11 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
         Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap0) );
     Vec_WecForEachLevel( pBox1->vLeafLits, vLevel, i )
         Acec_MatchBoxesSort( Vec_IntArray(vLevel), Vec_IntSize(vLevel), Vec_IntArray(vMap1) );
-    //Acec_MatchPrintEquivLits( pBox0->vLeafLits, Vec_IntArray(vMap0) );
-    //Acec_MatchPrintEquivLits( pBox1->vLeafLits, Vec_IntArray(vMap1) );
+    Acec_MatchCheckShift( pBox0->vLeafLits, pBox1->vLeafLits, vMap0, vMap1, pBox0->vRootLits, pBox1->vRootLits );
+    
+    //Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vLeafLits, Vec_IntArray(vMap0), 0 );
+    //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vLeafLits, Vec_IntArray(vMap1), 0 );
+
     // reorder nodes to have the same order
     assert( pBox0->vShared == NULL );
     assert( pBox1->vShared == NULL );
@@ -216,11 +303,15 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
         assert( Vec_IntSize(vShared0) + Vec_IntSize(vUnique0) == Vec_IntSize(vLevel0) );
         assert( Vec_IntSize(vShared1) + Vec_IntSize(vUnique1) == Vec_IntSize(vLevel1) );
     }
-    Vec_IntFree( vMap0 );
-    Vec_IntFree( vMap1 );
     nTotal = Vec_WecSizeSize(pBox0->vShared);
     printf( "Box0: Matched %d entries out of %d.\n", nTotal, Vec_WecSizeSize(pBox0->vLeafLits) );
     printf( "Box1: Matched %d entries out of %d.\n", nTotal, Vec_WecSizeSize(pBox1->vLeafLits) );
+
+    //Acec_MatchPrintEquivLits( pBox0->pGia, pBox0->vUnique, Vec_IntArray(vMap0), 0 );
+    //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vUnique, Vec_IntArray(vMap1), 0 );
+
+    Vec_IntFree( vMap0 );
+    Vec_IntFree( vMap1 );
     return nTotal;
 }
 
@@ -258,6 +349,9 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
         pGia1n = Acec_InsertBox( pBox1, 1 );
         printf( "Matching of adder trees in LHS and RHS succeeded.  " );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+        // remove the last output
+        //Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-1, 0 );
+        //Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-1, 0 );
     }
     // solve regular CEC problem 
     Cec_ManCecSetDefaultParams( pCecPars );
diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c
index 0733c00b..d868c399 100644
--- a/src/proof/acec/acecMult.c
+++ b/src/proof/acec/acecMult.c
@@ -504,14 +504,18 @@ Vec_Int_t * Acec_MultFindPPs( Gia_Man_t * p )
                 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 );
-*/
+        /*
+        if ( Saved[i] )
+        {
+            printf( "Obj = %4d  ", iObj );
+            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 );
+        }
+        */
     }
     Gia_ManCleanMark0(p);
     printf( "Collected %d pps and %d nodes.\n", nProds, Vec_IntSize(vBold) );
diff --git a/src/proof/acec/acecNorm.c b/src/proof/acec/acecNorm.c
index 4ed32e7b..0d209524 100644
--- a/src/proof/acec/acecNorm.c
+++ b/src/proof/acec/acecNorm.c
@@ -112,7 +112,7 @@ int Acec_InsertBox_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
     assert( Gia_ObjIsAnd(pObj) );
     Acec_InsertBox_rec( pNew, p, Gia_ObjFanin0(pObj) );
     Acec_InsertBox_rec( pNew, p, Gia_ObjFanin1(pObj) );
-    return (pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ));
+    return (pObj->Value = Gia_ManAppendAnd2( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ));
 }
 Vec_Int_t * Acec_BuildTree( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Wec_t * vLeafLits )
 {
diff --git a/src/proof/acec/acecRe.c b/src/proof/acec/acecRe.c
index 161b6fbb..7f87df85 100644
--- a/src/proof/acec/acecRe.c
+++ b/src/proof/acec/acecRe.c
@@ -147,6 +147,7 @@ static inline int Ree_ManCutFind( int iObj, int * pCut )
 }
 static inline int Ree_ManCutNotFind( int iObj1, int iObj2, int * pCut )
 {
+    assert( pCut[0] == 3 );
     if ( pCut[3] != iObj1 && pCut[3] != iObj2 ) return 0;
     if ( pCut[2] != iObj1 && pCut[2] != iObj2 ) return 1;
     if ( pCut[1] != iObj1 && pCut[1] != iObj2 ) return 2;
@@ -162,13 +163,19 @@ static inline int Ree_ManCutTruthOne( int * pCut0, int * pCut )
     Truth0 = fComp0 ? ~Truth0 : Truth0;
     if ( pCut0[0] == 2 )
     {
-        int Truths[3][8] = {
-            { 0x00, 0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77 }, // {0,1,-}
-            { 0x00, 0x05, 0x0A, 0x0F, 0x50, 0x55, 0x5A, 0x5F }, // {0,-,1}
-            { 0x00, 0x03, 0x0C, 0x0F, 0x30, 0x33, 0x3C, 0x3F }  // {-,0,1}
-        };
-        int Truth = Truths[Ree_ManCutNotFind(pCut0[1], pCut0[2], pCut)][Truth0 & 0x7];
-        return 0xFF & (fComp0 ? ~Truth : Truth);
+        if ( pCut[0] == 3 )
+        {
+            int Truths[3][8] = {
+                { 0x00, 0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77 }, // {0,1,-}
+                { 0x00, 0x05, 0x0A, 0x0F, 0x50, 0x55, 0x5A, 0x5F }, // {0,-,1}
+                { 0x00, 0x03, 0x0C, 0x0F, 0x30, 0x33, 0x3C, 0x3F }  // {-,0,1}
+            };
+            int Truth = Truths[Ree_ManCutNotFind(pCut0[1], pCut0[2], pCut)][Truth0 & 0x7];
+            return 0xFF & (fComp0 ? ~Truth : Truth);
+        }
+        assert( pCut[0] == 2 );
+        assert( pCut[1] == pCut0[1] && pCut[2] == pCut0[2] );
+        return pCut0[pCut0[0]+1];
     }
     if ( pCut0[0] == 1 )
     {
@@ -236,10 +243,10 @@ int Ree_ObjComputeTruth( Gia_Man_t * p, int iObj, int * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-void Ree_ManCutPrint( int * pCut, int Count, word Truth )
+void Ree_ManCutPrint( int * pCut, int Count, word Truth, int iObj )
 {
     int c;
-    printf( "%d : ", Count );
+    printf( "%d : %d : ", Count, iObj );
     for ( c = 1; c <= pCut[0]; c++ )
         printf( "%3d ", pCut[c] );
     for (      ; c <= 4; c++ )
@@ -290,7 +297,7 @@ void Ree_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
             Vec_IntPushThree( vData, iObj, Value, TruthC );
         }
         if ( fVerbose )
-            Ree_ManCutPrint( pCut, ++Count, TruthC );
+            Ree_ManCutPrint( pCut, ++Count, TruthC, iObj );
     }
     if ( !vXors )
         return;
diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c
index fef36923..295fd738 100644
--- a/src/proof/acec/acecTree.c
+++ b/src/proof/acec/acecTree.c
@@ -392,7 +392,7 @@ Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vI
     Vec_BitFree( vFound );
     Vec_IntFree( vMap );
     // filter trees
-    Acec_TreeFilterTrees( p, vAdds, vTrees );
+    //Acec_TreeFilterTrees( p, vAdds, vTrees );
     // sort by size
     Vec_WecSort( vTrees, 1 );
     return vTrees;
@@ -478,7 +478,7 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * 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, j, k, Box, Rank;
+    int i, j, k, Box, Rank, Count = 0;
 
     Acec_Box_t * pBox = ABC_CALLOC( Acec_Box_t, 1 );
     pBox->pGia        = p;
@@ -532,6 +532,30 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
         Vec_IntSort( vLevel, 0 );
     Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
         Vec_IntSort( vLevel, 0 );
+    //return pBox;
+    // push literals forward
+    //Vec_WecPrint( pBox->vLeafLits, 0 );
+    Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
+    {
+        int This, Prev = Vec_IntEntry(vLevel, 0);
+        Vec_IntForEachEntryStart( vLevel, This, j, 1 )
+        {
+            if ( Prev != This )
+            {
+                Prev = This;
+                continue;
+            }
+            if ( i+1 >= Vec_WecSize(pBox->vLeafLits) )
+                continue;
+            Vec_IntPushOrder( Vec_WecEntry(pBox->vLeafLits, i+1), This );
+            Vec_IntDrop( vLevel, j-- );
+            Vec_IntDrop( vLevel, j-- );
+            Prev = -1;
+            Count++;
+        }
+    }
+    printf( "Pushed forward %d input literals.\n", Count );
+    //Vec_WecPrint( pBox->vLeafLits, 0 );
     return pBox;
 }
 void Acec_CreateBoxTest( Gia_Man_t * p )