Updates to arithmetic verification.

10 files changed, 215 insertions, 128 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 68060119..dc6c679a 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1270,6 +1270,7 @@ extern void                Gia_ManOrigIdsInit( Gia_Man_t * p );
 extern void                Gia_ManOrigIdsStart( Gia_Man_t * p );
 extern void                Gia_ManOrigIdsRemap( Gia_Man_t * p, Gia_Man_t * pNew );
 extern Gia_Man_t *         Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs );
+extern Gia_Man_t *         Gia_ManComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose );
 extern void                Gia_ManEquivFixOutputPairs( Gia_Man_t * p );
 extern int                 Gia_ManCheckTopoOrder( Gia_Man_t * p );
 extern int *               Gia_ManDeriveNexts( Gia_Man_t * p );
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 584be4cd..1b0bce07 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -129,7 +129,7 @@ Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs )
     }
     Gia_ManHashStop( pNew );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Vec_IntFree( vMap );
     // compute equivalences
     assert( !p->pReprs && !p->pNexts );
@@ -171,6 +171,31 @@ Gia_Man_t * Gia_ManOrigIdsReduceTest( Gia_Man_t * p, Vec_Int_t * vPairs )
 
 /**Function*************************************************************
 
+  Synopsis    [Compute equivalence classes of nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose )
+{
+    Gia_Man_t * pTemp;
+    Cec_ParFra_t ParsFra, * pPars = &ParsFra;
+    Cec_ManFraSetDefaultParams( pPars );
+    pPars->fUseOrigIds = 1;
+    pPars->fSatSweeping = 1;
+    pPars->nBTLimit = nConfs;
+    pPars->fVerbose = fVerbose;
+    pTemp = Cec_ManSatSweeping( pGia, pPars, 0 );
+    Gia_ManStop( pTemp );
+    return Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if AIG is not in the required topo order.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 910014c6..1e94f28f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -40543,7 +40543,7 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c, nArgcNew;
     Acec_ManCecSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CTmdtvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CTmdtbvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -40578,6 +40578,9 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             pPars->fTwoOutput ^= 1;
             break;
+        case 'b':
+            pPars->fBooth ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -40720,13 +40723,14 @@ int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &acec [-CT num] [-mdtvh] <file1> <file2>\n" );
+    Abc_Print( -2, "usage: &acec [-CT num] [-mdtbvh] <file1> <file2>\n" );
     Abc_Print( -2, "\t         combinational equivalence checking for arithmetic circuits\n" );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
     Abc_Print( -2, "\t-m     : toggle miter vs. two circuits [default = %s]\n", pPars->fMiter? "miter":"two circuits");
     Abc_Print( -2, "\t-d     : toggle using dual output miter [default = %s]\n", pPars->fDualOutput? "yes":"no");
     Abc_Print( -2, "\t-t     : toggle using two-word miter [default = %s]\n", pPars->fTwoOutput? "yes":"no");
+    Abc_Print( -2, "\t-b     : toggle working with Booth multipliers [default = %s]\n", pPars->fBooth? "yes":"no");
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
     Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\tfile1  : (optional) the file with the first network\n");
@@ -40748,12 +40752,15 @@ usage:
 int Abc_CommandAbc9Anorm( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp;
-    int c, fVerbose = 0;
+    int c, fBooth = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "bvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'b':
+            fBooth ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -40768,13 +40775,14 @@ int Abc_CommandAbc9Anorm( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Anorm(): There is no AIG.\n" );
         return 0;
     }
-    pTemp = Acec_Normalize( pAbc->pGia, fVerbose );
+    pTemp = Acec_Normalize( pAbc->pGia, fBooth, fVerbose );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &anorm [-vh]\n" );
+    Abc_Print( -2, "usage: &anorm [-bvh]\n" );
     Abc_Print( -2, "\t         normalize adder trees in the current AIG\n" );
+    Abc_Print( -2, "\t-b     : toggles working with Booth multipliers [default = %s]\n",  fBooth? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDress3.c b/src/base/abci/abcDress3.c
index 33545f0a..ce0cb7f5 100644
--- a/src/base/abci/abcDress3.c
+++ b/src/base/abci/abcDress3.c
@@ -35,32 +35,6 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    [Compute equivalence classes of nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose )
-{
-    Gia_Man_t * pTemp;
-    Cec_ParFra_t ParsFra, * pPars = &ParsFra;
-    Cec_ManFraSetDefaultParams( pPars );
-    pPars->fUseOrigIds = 1;
-    pPars->fSatSweeping = 1;
-    pPars->nBTLimit = nConfs;
-    pPars->fVerbose = fVerbose;
-    pTemp = Cec_ManSatSweeping( pGia, pPars, 0 );
-    Gia_ManStop( pTemp );
-    pTemp = Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv );
-    Gia_ManStop( pTemp );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Converts AIG from HOP to GIA.]
 
   Description []
@@ -315,13 +289,15 @@ void Abc_NtkDumpEquivFile( char * pFileName, Vec_Int_t * vClasses, Abc_Ntk_t * p
 void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fByName, int fVerbose )
 {
     //abctime clk = Abc_Clock();
+    Gia_Man_t * pTemp;
     Vec_Int_t * vClasses;
     // derive shared AIG for the two networks
     Gia_Man_t * pGia = Abc_NtkAigToGiaTwo( pNtks[0], pNtks[1], fByName );
     if ( fVerbose )
         printf( "Computing equivalences for networks \"%s\" and \"%s\" with conflict limit %d.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]), nConfs );
     // compute equivalences in this AIG
-    Abc_NtkComputeGiaEquivs( pGia, nConfs, fVerbose );
+    pTemp = Gia_ManComputeGiaEquivs( pGia, nConfs, fVerbose );
+    Gia_ManStop( pTemp );
     //if ( fVerbose )
     //    Abc_PrintTime( 1, "Equivalence computation time", Abc_Clock() - clk );
     if ( fVerbose )
diff --git a/src/proof/acec/acec.h b/src/proof/acec/acec.h
index 7ad5baf9..5a24bec7 100644
--- a/src/proof/acec/acec.h
+++ b/src/proof/acec/acec.h
@@ -47,6 +47,7 @@ struct Acec_ParCec_t_
     int              fMiter;        // input circuit is a miter
     int              fDualOutput;   // dual-output miter
     int              fTwoOutput;    // two-output miter
+    int              fBooth;        // expecting Booth multiplier
     int              fSilent;       // print no messages
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
@@ -81,7 +82,7 @@ extern Vec_Int_t *   Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int
 extern int           Ree_ManCountFadds( Vec_Int_t * vAdds );
 extern void          Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
 /*=== acecTree.c ========================================================*/
-extern Gia_Man_t *   Acec_Normalize( Gia_Man_t * pGia, int fVerbose );
+extern Gia_Man_t *   Acec_Normalize( Gia_Man_t * pGia, int fBooth, int fVerbose );
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c
index 3e31fa36..4a91663f 100644
--- a/src/proof/acec/acecCore.c
+++ b/src/proof/acec/acecCore.c
@@ -68,7 +68,7 @@ void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Acec_FindEquivs( Gia_Man_t * pBase, Gia_Man_t * pAdd )
+Gia_Man_t * Acec_CommonStart( Gia_Man_t * pBase, Gia_Man_t * pAdd )
 {
     Gia_Obj_t * pObj;
     int i;
@@ -93,35 +93,69 @@ Gia_Man_t * Acec_FindEquivs( Gia_Man_t * pBase, Gia_Man_t * pAdd )
         pObj->Value = Gia_ManHashAnd( pBase, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     return pBase;
 }
-Vec_Int_t * Acec_CountRemap( Gia_Man_t * pAdd )
+void Acec_CommonFinish( Gia_Man_t * pBase )
+{
+    int Id;
+    Gia_ManCreateRefs( pBase );
+    Gia_ManForEachAndId( pBase, Id )
+        if ( Gia_ObjRefNumId(pBase, Id) == 0 )
+            Gia_ManAppendCo( pBase, Abc_Var2Lit(Id,0) );
+}
+Vec_Int_t * Acec_CountRemap( Gia_Man_t * pAdd, Gia_Man_t * pBase )
 {
     Gia_Obj_t * pObj; int i;
     Vec_Int_t * vMapNew = Vec_IntStartFull( Gia_ManObjNum(pAdd) );
+    Gia_ManSetPhase( pAdd );
+    Vec_IntWriteEntry( vMapNew, 0, 0 );
     Gia_ManForEachCand( pAdd, pObj, i )
-        Vec_IntWriteEntry( vMapNew, i, Abc_Lit2Var(pObj->Value) );
+    {
+        int iObjBase = Abc_Lit2Var(pObj->Value);
+        Gia_Obj_t * pObjBase = Gia_ManObj( pBase, iObjBase );
+        int iObjRepr = Abc_Lit2Var(pObjBase->Value);
+        Vec_IntWriteEntry( vMapNew, i, Abc_Var2Lit(iObjRepr, Gia_ObjPhase(pObj)) );
+    }
     return vMapNew;
 }
 void Acec_ComputeEquivClasses( Gia_Man_t * pOne, Gia_Man_t * pTwo, Vec_Int_t ** pvMap1, Vec_Int_t ** pvMap2 )
 {
-    Gia_Man_t * pBase;
-    pBase = Acec_FindEquivs( NULL, pOne );
-    pBase = Acec_FindEquivs( pBase, pTwo );
-    *pvMap1 = Acec_CountRemap( pOne );
-    *pvMap2 = Acec_CountRemap( pTwo );
+    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 );
 }
-static inline void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCosts )
+void Acec_MatchBoxesSort( int * pArray, int nSize, int * pCostLits )
 {
     int i, j, best_i;
     for ( i = 0; i < nSize-1; i++ )
     {
         best_i = i;
         for ( j = i+1; j < nSize; j++ )
-            if ( pCosts[Abc_Lit2Var(pArray[j])] > pCosts[Abc_Lit2Var(pArray[best_i])] )
+            if ( Abc_Lit2LitL(pCostLits, pArray[j]) > Abc_Lit2LitL(pCostLits, pArray[best_i]) )
                 best_i = j;
         ABC_SWAP( int, pArray[i], pArray[best_i] );
     }
 }
+void Acec_MatchPrintEquivLits( Vec_Wec_t * vLits, int * pCostLits )
+{
+    Vec_Int_t * vLevel;
+    int i, k, Entry;
+    printf( "Leaf literals and their classes:\n" );
+    Vec_WecForEachLevel( vLits, vLevel, i )
+    {
+        printf( "Rank %2d : %2d  ", i, Vec_IntSize(vLevel) );
+        Vec_IntForEachEntry( vLevel, Entry, k )
+            printf( "%s%d(%d) ", Abc_LitIsCompl(Entry) ? "-":"+", Abc_Lit2Var(Entry), Abc_Lit2LitL(pCostLits, Entry) );
+        printf( "\n" );
+    }
+}
 int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
 {
     Vec_Int_t * vMap0, * vMap1, * vLevel; 
@@ -132,6 +166,8 @@ 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) );
     // reorder nodes to have the same order
     assert( pBox0->vShared == NULL );
     assert( pBox1->vShared == NULL );
@@ -159,8 +195,9 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
         int * pEnd1 = Vec_IntLimit(vLevel1);
         while ( pBeg0 < pEnd0 && pBeg1 < pEnd1 )
         {
-            int Entry0 = Abc_Lit2LitV( Vec_IntArray(vMap0), *pBeg0 );
-            int Entry1 = Abc_Lit2LitV( Vec_IntArray(vMap1), *pBeg1 );
+            int Entry0 = Abc_Lit2LitL( Vec_IntArray(vMap0), *pBeg0 );
+            int Entry1 = Abc_Lit2LitL( Vec_IntArray(vMap1), *pBeg1 );
+            assert( *pBeg0 && *pBeg1 );
             if ( Entry0 == Entry1 )
             {
                 Vec_IntPush( vShared0, *pBeg0++ );
@@ -201,11 +238,16 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
 int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
 {
     int status = -1;
+    abctime clk = Abc_Clock();
     Gia_Man_t * pMiter;
     Gia_Man_t * pGia0n = pGia0, * pGia1n = pGia1;
     Cec_ParCec_t ParsCec, * pCecPars = &ParsCec;
-    Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, pPars->fVerbose );
-    Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, pPars->fVerbose );
+    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, pPars->fVerbose );
+    Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1, vIgnore1, pPars->fVerbose );
+    Vec_BitFreeP( &vIgnore0 );
+    Vec_BitFreeP( &vIgnore1 );
     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
@@ -214,7 +256,8 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
     {
         pGia0n = Acec_InsertBox( pBox0, 1 );
         pGia1n = Acec_InsertBox( pBox1, 1 );
-        printf( "Found, matched, and normalized arithmetic boxes in LHS and RHS. Solving resulting CEC.\n" );
+        printf( "Matching of adder trees in LHS and RHS succeeded.  " );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     }
     // solve regular CEC problem 
     Cec_ManCecSetDefaultParams( pCecPars );
diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h
index 125d923f..cc5786bb 100644
--- a/src/proof/acec/acecInt.h
+++ b/src/proof/acec/acecInt.h
@@ -69,10 +69,11 @@ extern Vec_Int_t *   Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Ve
 extern Vec_Wec_t *   Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes );
 /*=== acecMult.c ========================================================*/
 extern Vec_Int_t *   Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits );
+extern Vec_Bit_t *   Acec_BoothFindPPG( Gia_Man_t * p );
 /*=== acecNorm.c ========================================================*/
 extern Gia_Man_t *   Acec_InsertBox( Acec_Box_t * pBox, int fAll );
 /*=== acecTree.c ========================================================*/
-extern Acec_Box_t *  Acec_DeriveBox( Gia_Man_t * p, int fVerbose );
+extern Acec_Box_t *  Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fVerbose );
 extern void          Acec_BoxFreeP( Acec_Box_t ** ppBox );
 /*=== acecUtil.c ========================================================*/
 extern void          Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose );
diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c
index 8ccf966e..0733c00b 100644
--- a/src/proof/acec/acecMult.c
+++ b/src/proof/acec/acecMult.c
@@ -490,18 +490,16 @@ Vec_Int_t * Acec_MultFindPPs( Gia_Man_t * p )
     Gia_ManForEachAndId( p, iObj )
     {
         word Truth = Gia_ObjComputeTruth6Cis( p, Abc_Var2Lit(iObj, 0), vSupp, vTemp );
+        if ( Vec_IntSize(vSupp) > 6  )
+            continue;
         vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
         if ( Vec_IntSize(vSupp) > 5  )
             continue;
-        for ( i = 0; i < 32; i++ )
+        for ( i = 0; i < 32 && Saved[i]; 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;
             }
@@ -515,7 +513,6 @@ Vec_Int_t * Acec_MultFindPPs( Gia_Man_t * p )
         Vec_IntPrint( vSupp );
 */
     }
-    printf( "\n" );
     Gia_ManCleanMark0(p);
     printf( "Collected %d pps and %d nodes.\n", nProds, Vec_IntSize(vBold) );
 
@@ -523,6 +520,16 @@ Vec_Int_t * Acec_MultFindPPs( Gia_Man_t * p )
     Vec_WrdFree( vTemp );
     return vBold;
 }
+Vec_Bit_t * Acec_BoothFindPPG( Gia_Man_t * p )
+{
+    Vec_Bit_t * vIgnore = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vMap = Acec_MultFindPPs( p );
+    int i, Entry;
+    Vec_IntForEachEntry( vMap, Entry, i )
+        Vec_BitWriteEntry( vIgnore, Entry, 1 );
+    Vec_IntFree( vMap );
+    return vIgnore;
+}
 void Acec_MultFindPPsTest( Gia_Man_t * p )
 {
     Vec_Int_t * vBold = Acec_MultFindPPs( p );
diff --git a/src/proof/acec/acecNorm.c b/src/proof/acec/acecNorm.c
index 9faf7acf..4ed32e7b 100644
--- a/src/proof/acec/acecNorm.c
+++ b/src/proof/acec/acecNorm.c
@@ -198,11 +198,13 @@ Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Acec_Normalize( Gia_Man_t * pGia, int fVerbose )
+Gia_Man_t * Acec_Normalize( Gia_Man_t * pGia, int fBooth, int fVerbose )
 {
-    Acec_Box_t * pBox = Acec_DeriveBox( pGia, fVerbose );
+    Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG( pGia ) : NULL;
+    Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, fVerbose );
     Gia_Man_t * pNew  = Acec_InsertBox( pBox, 1 );
     Acec_BoxFreeP( &pBox );
+    Vec_BitFreeP( &vIgnore );
     return pNew;
 }
 
diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c
index 370e8eb6..fef36923 100644
--- a/src/proof/acec/acecTree.c
+++ b/src/proof/acec/acecTree.c
@@ -27,6 +27,12 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static inline int Acec_SignBit( Vec_Int_t * vAdds, int iBox, int b )  { return (Vec_IntEntry(vAdds, 6*iBox+5) >> b)      & 1; }
+static inline int Acec_SignBit2( Vec_Int_t * vAdds, int iBox, int b ) { return (Vec_IntEntry(vAdds, 6*iBox+5) >> (16+b)) & 1; }
+
+static inline void Acec_SignSetBit( Vec_Int_t * vAdds, int iBox, int b, int v )  { if ( v ) *Vec_IntEntryP(vAdds, 6*iBox+5) |= (1 << b);      }
+static inline void Acec_SignSetBit2( Vec_Int_t * vAdds, int iBox, int b, int v ) { if ( v ) *Vec_IntEntryP(vAdds, 6*iBox+5) |= (1 << (16+b)); }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -147,10 +153,7 @@ 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;
+    int fFlip = !fFadd && Acec_SignBit2(vAdds, iBox, 2);
 
     Gia_ManIncrementTravId( p );
     for ( k = 0; k < 3; k++ )
@@ -159,17 +162,17 @@ void Acec_TreeVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox )
         if ( iObj == 0 )
             continue;
         pObj = Gia_ManObj( p, iObj );
-        pObj->Value = Phase[k] ? 0xFF & ~Truths[k] : Truths[k];
+        pObj->Value = (Acec_SignBit2(vAdds, iBox, k) ^ fFlip) ? 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;
+    TruthXor = (Acec_SignBit2(vAdds, iBox, 3) ^ fFlip) ? 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;
+    TruthMaj = (Acec_SignBit2(vAdds, iBox, 4) ^ fFlip) ? 0xFF & ~TruthMaj : TruthMaj;
 
     if ( fFadd ) // FADD
     {
@@ -180,6 +183,8 @@ void Acec_TreeVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox )
     }
     else
     {
+        //printf( "Sign1 = %d%d%d %d\n", Acec_SignBit(vAdds, iBox, 0), Acec_SignBit(vAdds, iBox, 1), Acec_SignBit(vAdds, iBox, 2), Acec_SignBit(vAdds, iBox, 3) );
+        //printf( "Sign2 = %d%d%d %d%d\n", Acec_SignBit2(vAdds, iBox, 0), Acec_SignBit2(vAdds, iBox, 1), Acec_SignBit2(vAdds, iBox, 2), Acec_SignBit2(vAdds, iBox, 3), Acec_SignBit2(vAdds, iBox, 4) );
         if ( TruthXor != 0x66 )
             printf( "Hadd %d sum %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+3 ) );
         if ( TruthMaj != 0x88 )
@@ -194,6 +199,36 @@ void Acec_TreeVerifyPhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes
         Vec_IntForEachEntry( vLevel, Box, k )
             Acec_TreeVerifyPhaseOne( p, vAdds, Box );
 }
+void Acec_TreeVerifyPhases2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes )
+{
+    Vec_Bit_t * vPhase = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Bit_t * vRoots = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vLevel;
+    int i, k, n, Box;
+    // mark all output points and their values
+    Vec_WecForEachLevel( vBoxes, vLevel, i )
+        Vec_IntForEachEntry( vLevel, Box, k )
+        {
+            Vec_BitWriteEntry( vRoots, Vec_IntEntry( vAdds, 6*Box+3 ), 1 );
+            Vec_BitWriteEntry( vRoots, Vec_IntEntry( vAdds, 6*Box+4 ), 1 );
+            Vec_BitWriteEntry( vPhase, Vec_IntEntry( vAdds, 6*Box+3 ), Acec_SignBit2(vAdds, Box, 3) );
+            Vec_BitWriteEntry( vPhase, Vec_IntEntry( vAdds, 6*Box+4 ), Acec_SignBit2(vAdds, Box, 4) );
+        }
+    // compare with input points
+    Vec_WecForEachLevel( vBoxes, vLevel, i )
+        Vec_IntForEachEntry( vLevel, Box, k )
+            for ( n = 0; n < 3; n++ )
+            {
+                if ( !Vec_BitEntry(vRoots, Vec_IntEntry(vAdds, 6*Box+n)) )
+                    continue;
+                if ( Vec_BitEntry(vPhase, Vec_IntEntry(vAdds, 6*Box+n)) == Acec_SignBit2(vAdds, Box, n) )
+                    continue;
+                printf( "Phase of input %d=%d is mismatched in box %d=(%d,%d).\n",
+                    n, Vec_IntEntry(vAdds, 6*Box+n), Box, Vec_IntEntry(vAdds, 6*Box+3), Vec_IntEntry(vAdds, 6*Box+4) );
+            }
+    Vec_BitFree( vPhase );
+    Vec_BitFree( vRoots );
+}
 
 /**Function*************************************************************
 
@@ -216,40 +251,40 @@ Vec_Int_t * Acec_TreeCarryMap( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBo
             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 )
+void Acec_TreePhases_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, int Node, int fPhase, Vec_Bit_t * vVisit )
 {
-    int k, iBox, iXor, Sign, fXorPhase, fPhaseThis;
+    int k, iBox, iXor, fXorPhase, fPhaseThis;
     assert( Node != 0 );
     iBox = Vec_IntEntry( vMap, Node );
     if ( iBox == -1 )
         return;
     assert( Node == Vec_IntEntry( vAdds, 6*iBox+4 ) );
+    if ( Vec_BitEntry(vVisit, iBox) )
+        return;
+    Vec_BitWriteEntry( vVisit, iBox, 1 );
     iXor = Vec_IntEntry( vAdds, 6*iBox+3 );
-    Sign = Vec_IntEntry( vAdds, 6*iBox+5 ) & 0xFFFFFFF0;
-    fXorPhase = ((Sign >> 3) & 1);
+    fXorPhase = Acec_SignBit(vAdds, iBox, 3);
     if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 )
     {
-        fPhase ^= ((Sign >> 2) & 1);
-        if ( fPhase ) // complemented HADD
-            Sign |= (1 << 6);
+        //fPhaseThis = Acec_SignBit( vAdds, iBox, 2 ) ^ fPhase;
+        //fXorPhase ^= fPhaseThis;
+        //Acec_SignSetBit2( vAdds, iBox, 2, fPhaseThis ); // complemented HADD -- create const1 input
+        fPhase ^= Acec_SignBit( vAdds, iBox, 2 );
+        fXorPhase ^= fPhase;
+        Acec_SignSetBit2( vAdds, iBox, 2, fPhase ); // complemented HADD -- create const1 input
     }
     for ( k = 0; k < 3; k++ )
     {
         int iObj = Vec_IntEntry( vAdds, 6*iBox+k );
         if ( iObj == 0 )
             continue;
-        fPhaseThis = ((Sign >> k) & 1) ^ fPhase;
+        fPhaseThis = Acec_SignBit(vAdds, iBox, k) ^ fPhase;
         fXorPhase ^= fPhaseThis;
-        Acec_TreePhases_rec( p, vAdds, vMap, iObj, fPhaseThis );
-        if ( fPhaseThis )
-            Sign |= (1 << (4+k));
+        Acec_TreePhases_rec( p, vAdds, vMap, iObj, fPhaseThis, vVisit );
+        Acec_SignSetBit2( vAdds, iBox, k, fPhaseThis );
     }
-    if ( fXorPhase )
-        Sign |= (1 << 7);
-    if ( fPhase )
-        Sign |= (1 << 8);
-    // save updated signature
-    Vec_IntWriteEntry( vAdds, 6*iBox+5, Sign );
+    Acec_SignSetBit2( vAdds, iBox, 3, fXorPhase );
+    Acec_SignSetBit2( vAdds, iBox, 4, fPhase );
 }
 
 /**Function*************************************************************
@@ -271,12 +306,14 @@ void Acec_TreeAddInOutPoint( Vec_Int_t * vMap, int iObj, int iAdd, int fOut )
     else if ( *pPlace >= 0 )
         *pPlace = -2;
 }
-Vec_Int_t * Acec_TreeFindPoints( Gia_Man_t * p, Vec_Int_t * vAdds )
+Vec_Int_t * Acec_TreeFindPoints( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vIgnore )
 {
     Vec_Int_t * vMap = Vec_IntStartFull( 2*Gia_ManObjNum(p) );
     int i;
     for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
     {
+        if ( vIgnore && (Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+3)) || Vec_BitEntry(vIgnore, Vec_IntEntry(vAdds, 6*i+4))) )
+            continue;
         Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+0), i, 0 );
         Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+1), i, 0 );
         Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+2), i, 0 );
@@ -328,10 +365,10 @@ void Acec_TreeFindTrees_rec( Vec_Int_t * vAdds, Vec_Int_t * vMap, int iObj, int
     Acec_TreeFindTrees2_rec( vAdds, vMap, In,  Acec_TreeWhichPoint(vAdds, In, iObj) == 4 ? Rank-1 : Rank, vTree, vFound );
     Acec_TreeFindTrees2_rec( vAdds, vMap, Out, Rank, vTree, vFound );
 }
-Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds )
+Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Bit_t * vIgnore )
 {
     Vec_Wec_t * vTrees = Vec_WecAlloc( 10 );
-    Vec_Int_t * vMap   = Acec_TreeFindPoints( p, vAdds );
+    Vec_Int_t * vMap   = Acec_TreeFindPoints( p, vAdds, vIgnore );
     Vec_Bit_t * vFound = Vec_BitStart( Vec_IntSize(vAdds)/6 );
     Vec_Int_t * vTree;
     int i, k, In, Out, Box, Rank, MinRank;
@@ -371,7 +408,7 @@ void Acec_TreeFindTreesTest( Gia_Man_t * p )
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
     clk = Abc_Clock();
-    vTrees = Acec_TreeFindTrees( p, vAdds );
+    vTrees = Acec_TreeFindTrees( p, vAdds, NULL );
     printf( "Collected %d trees with %d adders in them.  ", Vec_WecSize(vTrees), Vec_WecSizeSize(vTrees)/2 );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     Vec_WecPrint( vTrees, 0 );
@@ -417,23 +454,6 @@ void Vec_WecPrintLits( Vec_Wec_t * p )
         printf( " }\n" );
     }
 }
-void Acec_PrintRootLits( Vec_Wec_t * vRoots )
-{
-    Vec_Int_t * vLevel;
-    int i, k, iObj;
-    Vec_WecForEachLevel( vRoots, vLevel, i )
-    {
-        printf( "Rank %d : %2d  ", i, Vec_IntSize(vLevel) );
-        Vec_IntForEachEntry( vLevel, iObj, k )
-        {
-            int fFadd = Abc_LitIsCompl(iObj);
-            int fCout = Abc_LitIsCompl(Abc_Lit2Var(iObj));
-            int Node  = Abc_Lit2Var(Abc_Lit2Var(iObj));
-            printf( "%d%s%s ", Node, fCout ? "*" : "", (fCout && fFadd) ? "*" : "" );
-        }
-        printf( "\n" );
-    }
-}
 void Acec_PrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds )
 {
     printf( "Adders:\n" );
@@ -442,8 +462,6 @@ void Acec_PrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds )
     Vec_WecPrintLits( pBox->vLeafLits );
     printf( "Outputs:\n" );
     Vec_WecPrintLits( pBox->vRootLits );
-    //printf( "Raw outputs:\n" );
-    //Acec_PrintRootLits( pBox->vRoots );
 }
 
 int Acec_CreateBoxMaxRank( Vec_Int_t * vTree )
@@ -456,10 +474,11 @@ int Acec_CreateBoxMaxRank( Vec_Int_t * vTree )
 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 * vVisit  = Vec_BitStart( Vec_IntSize(vAdds)/6 );
     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;
+    int i, j, k, Box, Rank;
 
     Acec_Box_t * pBox = ABC_CALLOC( Acec_Box_t, 1 );
     pBox->pGia        = p;
@@ -470,38 +489,42 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
     // 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 );
+        Vec_WecPush( pBox->vAdds, Rank, Box );
     }
     // sort each level
     Vec_WecForEachLevel( pBox->vAdds, vLevel, i )
         Vec_IntSort( vLevel, 0 );
 
-    // set phases
+    // set phases starting from roots
     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 );
+    Vec_WecForEachLevelReverse( pBox->vAdds, vLevel, i )
+        Vec_IntForEachEntry( vLevel, Box, k )
+            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, vVisit );
     Acec_TreeVerifyPhases( p, vAdds, pBox->vAdds );
+    Acec_TreeVerifyPhases2( p, vAdds, pBox->vAdds );
+    Vec_BitFree( vVisit );
     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_BitWriteEntry( vIsRoot, 0, 1 );
+    Vec_WecForEachLevel( pBox->vAdds, vLevel, i )
+        Vec_IntForEachEntry( vLevel, Box, j )
+        {
+            for ( k = 0; k < 3; k++ )
+                if ( !Vec_BitEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+k) ) )
+                    Vec_WecPush( pBox->vLeafLits, i, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), Acec_SignBit2(vAdds, Box, k)) );
+            for ( k = 3; k < 5; k++ )
+                if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+k) ) )
+                    Vec_WecPush( pBox->vRootLits, k == 4 ? i + 1 : i, Abc_Var2Lit(Vec_IntEntry(vAdds, 6*Box+k), Acec_SignBit2(vAdds, Box, k)) );
+            if ( Vec_IntEntry(vAdds, 6*Box+2) == 0 && Acec_SignBit2(vAdds, Box, 2) )
+                Vec_WecPush( pBox->vLeafLits, i, 1 );
+        }
     Vec_BitFree( vIsLeaf );
     Vec_BitFree( vIsRoot );
     // sort each level
@@ -524,7 +547,7 @@ void Acec_CreateBoxTest( Gia_Man_t * p )
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
     clk = Abc_Clock();
-    vTrees = Acec_TreeFindTrees( p, vAdds );
+    vTrees = Acec_TreeFindTrees( p, vAdds, NULL );
     printf( "Collected %d trees with %d adders in them.  ", Vec_WecSize(vTrees), Vec_WecSizeSize(vTrees)/2 );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     //Vec_WecPrint( vTrees, 0 );
@@ -554,11 +577,11 @@ void Acec_CreateBoxTest( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, int fVerbose )
+Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fVerbose )
 {
     Acec_Box_t * pBox = NULL;
     Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, fVerbose );
-    Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds );
+    Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds, vIgnore );
     if ( vTrees && Vec_WecSize(vTrees) > 0 )
         pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, 0) );
     if ( pBox )//&& fVerbose )
@@ -567,7 +590,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;