Merged alanmi/abc into default

17 files changed, 3567 insertions, 46 deletions

diff --git a/src/proof/acec/acec.h b/src/proof/acec/acec.h
index c61b4485..fcbd32df 100644
--- a/src/proof/acec/acec.h
+++ b/src/proof/acec/acec.h
@@ -38,6 +38,22 @@ ABC_NAMESPACE_HEADER_START
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
+// combinational equivalence checking parameters
+typedef struct Acec_ParCec_t_ Acec_ParCec_t;
+struct Acec_ParCec_t_
+{
+    int              nBTLimit;      // conflict limit at a node
+    int              TimeLimit;     // the runtime limit in seconds
+    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
+    int              iOutFail;      // the number of failed output
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -50,8 +66,11 @@ ABC_NAMESPACE_HEADER_START
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== acecCl.c ========================================================*/
+extern Gia_Man_t *   Acec_ManDecla( Gia_Man_t * pGia, int fBooth, int fVerbose );
 /*=== acecCore.c ========================================================*/
-extern int           Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars );
+extern void          Acec_ManCecSetDefaultParams( Acec_ParCec_t * p );
+extern int           Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars );
 /*=== acecFadds.c ========================================================*/
 extern Vec_Int_t *   Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose, Vec_Int_t ** vCutsXor2 );
 extern Vec_Int_t *   Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose );
@@ -60,6 +79,12 @@ extern Vec_Int_t *   Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVery
 extern Vec_Int_t *   Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int fVerbose, int fVeryVerbose );
 /*=== acecPolyn.c ========================================================*/
 extern void          Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fSigned, int fVerbose, int fVeryVerbose );
+/*=== acecRe.c ========================================================*/
+extern Vec_Int_t *   Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
+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 fBooth, int fVerbose );
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/proof/acec/acecBo.c b/src/proof/acec/acecBo.c
new file mode 100644
index 00000000..9cddcd13
--- /dev/null
+++ b/src/proof/acec/acecBo.c
@@ -0,0 +1,216 @@
+/**CFile****************************************************************
+
+  FileName    [acecBo.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [CEC for arithmetic circuits.]
+
+  Synopsis    [Core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: acecBo.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/vec/vecWec.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acec_DetectBoothXorMux( Gia_Man_t * p, Gia_Obj_t * pMux, Gia_Obj_t * pXor, int pIns[3] )
+{
+    Gia_Obj_t * pFan0, * pFan1;
+    Gia_Obj_t * pDat0, * pDat1, * pCtrl;
+    if ( !Gia_ObjIsMuxType(pMux) || !Gia_ObjIsMuxType(pXor) )
+        return 0;
+    if ( !Gia_ObjRecognizeExor( pXor, &pFan0, &pFan1 ) )
+        return 0;
+    pFan0 = Gia_Regular(pFan0);
+    pFan1 = Gia_Regular(pFan1);
+    if ( Gia_ObjId(p, pFan0) > Gia_ObjId(p, pFan1) )
+        ABC_SWAP( Gia_Obj_t *, pFan0, pFan1 );
+    if ( !(pCtrl = Gia_ObjRecognizeMux( pMux, &pDat0, &pDat1 )) )
+        return 0;
+    pDat0 = Gia_Regular(pDat0);
+    pDat1 = Gia_Regular(pDat1);
+    pCtrl = Gia_Regular(pCtrl);
+    if ( !Gia_ObjIsAnd(pDat0) || !Gia_ObjIsAnd(pDat1) )
+        return 0;
+    if ( Gia_ObjFaninId0p(p, pDat0) != Gia_ObjFaninId0p(p, pDat1) ||
+         Gia_ObjFaninId1p(p, pDat0) != Gia_ObjFaninId1p(p, pDat1) )
+         return 0;
+    if ( Gia_ObjFaninId0p(p, pDat0) != Gia_ObjId(p, pFan0) ||
+         Gia_ObjFaninId1p(p, pDat0) != Gia_ObjId(p, pFan1) )
+         return 0;
+    pIns[0] = Gia_ObjId(p, pFan0);
+    pIns[1] = Gia_ObjId(p, pFan1);
+    pIns[2] = Gia_ObjId(p, pCtrl);
+    return 1;
+}
+int Acec_DetectBoothXorFanin( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] )
+{
+    Gia_Obj_t * pFan0, * pFan1;
+    //int Id = Gia_ObjId(p, pObj);
+    if ( !Gia_ObjIsAnd(pObj) )
+        return 0;
+    if ( !Gia_ObjFaninC0(pObj) || !Gia_ObjFaninC1(pObj) )
+        return 0;
+    pFan0 = Gia_ObjFanin0(pObj);
+    pFan1 = Gia_ObjFanin1(pObj);
+    if ( !Gia_ObjIsAnd(pFan0) || !Gia_ObjIsAnd(pFan1) )
+        return 0;
+    if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin0(pFan0), Gia_ObjFanin0(pFan1), pIns) )
+    {
+        pIns[3] = Gia_ObjId(p, Gia_ObjFanin1(pFan0));
+        pIns[4] = Gia_ObjId(p, Gia_ObjFanin1(pFan1));
+        return 1;
+    }
+    if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin0(pFan0), Gia_ObjFanin1(pFan1), pIns) )
+    {
+        pIns[3] = Gia_ObjId(p, Gia_ObjFanin1(pFan0));
+        pIns[4] = Gia_ObjId(p, Gia_ObjFanin0(pFan1));
+        return 1;
+    }
+    if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin1(pFan0), Gia_ObjFanin0(pFan1), pIns) )
+    {
+        pIns[3] = Gia_ObjId(p, Gia_ObjFanin0(pFan0));
+        pIns[4] = Gia_ObjId(p, Gia_ObjFanin1(pFan1));
+        return 1;
+    }
+    if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin1(pFan0), Gia_ObjFanin1(pFan1), pIns) )
+    {
+        pIns[3] = Gia_ObjId(p, Gia_ObjFanin0(pFan0));
+        pIns[4] = Gia_ObjId(p, Gia_ObjFanin0(pFan1));
+        return 1;
+    }
+    return 0;
+}
+int Acec_DetectBoothOne( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] )
+{
+    Gia_Obj_t * pFan0, * pFan1;
+    if ( !Gia_ObjRecognizeExor( pObj, &pFan0, &pFan1 ) )
+        return 0;
+    pFan0 = Gia_Regular(pFan0);
+    pFan1 = Gia_Regular(pFan1);
+    if ( Acec_DetectBoothXorFanin( p, pFan0, pIns ) && pIns[2] == Gia_ObjId(p, pFan1) )
+        return 1;
+    if ( Acec_DetectBoothXorFanin( p, pFan1, pIns ) && pIns[2] == Gia_ObjId(p, pFan0) )
+        return 1;
+    return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acec_DetectBoothTwoXor( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] )
+{
+    Gia_Obj_t * pFan0, * pFan1;
+    if ( !Gia_ObjIsAnd(pObj) )
+        return 0;
+    if ( Gia_ObjRecognizeExor( Gia_ObjFanin0(pObj), &pFan0, &pFan1 ) )
+    {
+        pIns[0] = Gia_ObjId(p, Gia_Regular(pFan0));
+        pIns[1] = Gia_ObjId(p, Gia_Regular(pFan1));
+        pIns[2] = -1;
+        pIns[3] = 0;
+        pIns[4] = Gia_ObjId(p, Gia_ObjFanin1(pObj));
+        return 1;
+    }
+    if ( Gia_ObjRecognizeExor( Gia_ObjFanin1(pObj), &pFan0, &pFan1 ) )
+    {
+        pIns[0] = Gia_ObjId(p, Gia_Regular(pFan0));
+        pIns[1] = Gia_ObjId(p, Gia_Regular(pFan1));
+        pIns[2] = -1;
+        pIns[3] = 0;
+        pIns[4] = Gia_ObjId(p, Gia_ObjFanin0(pObj));
+        return 1;
+    }
+    return 0;
+}
+int Acec_DetectBoothTwo( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] )
+{
+    Gia_Obj_t * pFan0, * pFan1;
+    if ( !Gia_ObjRecognizeExor( pObj, &pFan0, &pFan1 ) )
+        return 0;
+    pFan0 = Gia_Regular(pFan0);
+    pFan1 = Gia_Regular(pFan1);
+    if ( Acec_DetectBoothTwoXor( p, pFan0, pIns ) )
+    {
+        pIns[2] = Gia_ObjId(p, pFan1);
+        return 1;
+    }
+    if ( Acec_DetectBoothTwoXor( p, pFan1, pIns ) )
+    {
+        pIns[2] = Gia_ObjId(p, pFan0);
+        return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_DetectBoothTest( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, pIns[5];
+    Gia_ManForEachAnd( p, pObj, i )
+    {        
+        if ( !Acec_DetectBoothOne(p, pObj, pIns) && !Acec_DetectBoothTwo(p, pObj, pIns) )
+                continue;
+        printf( "obj = %4d  :  b0 = %4d  b1 = %4d  b2 = %4d    a0 = %4d  a1 = %4d\n", 
+            i, pIns[0], pIns[1], pIns[2], pIns[3], pIns[4] );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c
index 32be3b30..6185677b 100644
--- a/src/proof/acec/acecCl.c
+++ b/src/proof/acec/acecCl.c
@@ -45,6 +45,396 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+void Acec_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * vMirrors )
+{
+    Gia_Obj_t * pObj;
+    int Obj = Node;
+    if ( Vec_IntEntry(vMirrors, Node) >= 0 )
+        Obj = Abc_Lit2Var( Vec_IntEntry(vMirrors, Node) );
+    pObj = Gia_ManObj( p, Obj );
+    if ( !~pObj->Value )
+    {
+        assert( Gia_ObjIsAnd(pObj) );
+        Acec_ManDerive_rec( pNew, p, Gia_ObjFaninId0(pObj, Obj), vMirrors );
+        Acec_ManDerive_rec( pNew, p, Gia_ObjFaninId1(pObj, Obj), vMirrors );
+        if ( Gia_ObjIsXor(pObj) )
+            pObj->Value = Gia_ManAppendXorReal( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else
+            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    }
+    // set the original node as well
+    if ( Obj != Node )
+        Gia_ManObj(p, Node)->Value = Abc_LitNotCond( pObj->Value, Abc_LitIsCompl(Vec_IntEntry(vMirrors, Node)) );
+} 
+Gia_Man_t * Acec_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( p->pMuxes == NULL );
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachCo( p, pObj, i )
+        Acec_ManDerive_rec( pNew, p, Gia_ObjFaninId0p(p, pObj), vMirrors );
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acec_CollectXorTops( Gia_Man_t * p )
+{
+    Vec_Int_t * vRootXorSet = Vec_IntAlloc( Gia_ManCoNum(p) );
+    Gia_Obj_t * pObj, * pFan0, * pFan1, * pFan00, * pFan01, * pFan10, * pFan11;
+    int i, fXor0, fXor1, fFirstXor = 0;
+    Gia_ManForEachCoDriver( p, pObj, i )
+    {
+        if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+        {
+            if ( fFirstXor )
+            {
+                printf( "XORs do not form a continuous sequence\n" );
+                Vec_IntFreeP( &vRootXorSet );
+                break;
+            }
+            continue;
+        }
+        fFirstXor = 1;
+        fXor0 = Gia_ObjRecognizeExor(Gia_Regular(pFan0), &pFan00, &pFan01);
+        fXor1 = Gia_ObjRecognizeExor(Gia_Regular(pFan1), &pFan10, &pFan11);
+        if ( fXor0 == fXor1 )
+        {
+            printf( "Both inputs of top level XOR have XOR/non-XOR\n" );
+            Vec_IntFreeP( &vRootXorSet );
+            break;
+        }
+        Vec_IntPush( vRootXorSet, Gia_ObjId(p, pObj) );
+        Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan0))  : Gia_ObjId(p, Gia_Regular(pFan1)) );
+        Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan10)) : Gia_ObjId(p, Gia_Regular(pFan00)) );
+        Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan11)) : Gia_ObjId(p, Gia_Regular(pFan01)) );
+    }
+    for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ )
+    {
+        printf( "%2d : ", i );
+        printf( "%4d <- ", Vec_IntEntry(vRootXorSet, 4*i) );
+        printf( "%4d ", Vec_IntEntry(vRootXorSet, 4*i+1) );
+        printf( "%4d ", Vec_IntEntry(vRootXorSet, 4*i+2) );
+        printf( "%4d ", Vec_IntEntry(vRootXorSet, 4*i+3) );
+        printf( "\n" );
+    }
+    return vRootXorSet;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acec_DetectLitPolarity( Gia_Man_t * p, int Node, int Leaf )
+{
+    Gia_Obj_t * pNode;
+    int Lit0, Lit1;
+    if ( Node < Leaf )
+        return -1;
+    if ( Node == Leaf )
+        return Abc_Var2Lit(Node, 0);
+    pNode = Gia_ManObj( p, Node );
+    Lit0 = Acec_DetectLitPolarity( p, Gia_ObjFaninId0(pNode, Node), Leaf );
+    Lit1 = Acec_DetectLitPolarity( p, Gia_ObjFaninId1(pNode, Node), Leaf );
+    Lit0 = Lit0 == -1 ? Lit0 : Abc_LitNotCond( Lit0, Gia_ObjFaninC0(pNode) );
+    Lit1 = Lit1 == -1 ? Lit1 : Abc_LitNotCond( Lit1, Gia_ObjFaninC1(pNode) );
+    if ( Lit0 == -1 && Lit1 == -1 )
+        return -1;
+    assert( Lit0 != -1 || Lit1 != -1 );
+    if ( Lit0 != -1 && Lit1 != -1 )
+    {
+        assert( Lit0 == Lit1 );
+        printf( "Problem for leaf %d\n", Leaf );
+        return Lit0;
+    }
+    return Lit0 != -1 ? Lit0 : Lit1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_DetectComputeSuppOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Int_t * vNods )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( pObj->fMark0 )
+    {
+        Vec_IntPush( vSupp, Gia_ObjId(p, pObj) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Acec_DetectComputeSuppOne_rec( p, Gia_ObjFanin0(pObj), vSupp, vNods );
+    Acec_DetectComputeSuppOne_rec( p, Gia_ObjFanin1(pObj), vSupp, vNods );
+    Vec_IntPush( vNods, Gia_ObjId(p, pObj) );
+}
+void Acec_DetectComputeSupports( Gia_Man_t * p, Vec_Int_t * vRootXorSet )
+{
+    Vec_Int_t * vNods = Vec_IntAlloc( 100 ); 
+    Vec_Int_t * vPols = Vec_IntAlloc( 100 ); 
+    Vec_Int_t * vSupp = Vec_IntAlloc( 100 );  int i, k, Node, Pol;
+    for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ )
+    {
+        Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 1;
+        Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+2) )->fMark0 = 1;
+        Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+3) )->fMark0 = 1;
+    }
+    for ( i = 1; 4*i < Vec_IntSize(vRootXorSet); i++ )
+    {
+        Vec_IntClear( vSupp );
+        Gia_ManIncrementTravId( p );
+
+        Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 0;
+        Acec_DetectComputeSuppOne_rec( p, Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) ), vSupp, vNods );
+        Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 1;
+
+        Vec_IntSort( vSupp, 0 );
+
+        printf( "Out %4d : %4d  \n", i, Vec_IntEntry(vRootXorSet, 4*i+1) );
+        Vec_IntPrint( vSupp );
+
+        printf( "Cone:\n" );
+        Vec_IntForEachEntry( vNods, Node, k )
+            Gia_ObjPrint( p, Gia_ManObj(p, Node) );
+
+
+        Vec_IntClear( vPols );
+        Vec_IntForEachEntry( vSupp, Node, k )
+            Vec_IntPush( vPols, Acec_DetectLitPolarity(p, Vec_IntEntry(vRootXorSet, 4*i+1), Node) );
+
+        Vec_IntForEachEntryTwo( vSupp, vPols, Node, Pol, k )
+            printf( "%d(%d)  ", Node, Abc_LitIsCompl(Pol) );
+
+        printf( "\n" );
+
+        Vec_IntPrint( vSupp );
+    }
+    for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ )
+    {
+        Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 0;
+        Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+2) )->fMark0 = 0;
+        Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+3) )->fMark0 = 0;
+    }
+    Vec_IntFree( vSupp );
+    Vec_IntFree( vPols );
+    Vec_IntFree( vNods );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Acec_DetectXorBuildNew( Gia_Man_t * p, Vec_Int_t * vRootXorSet )
+{
+    Gia_Man_t * pNew;
+    int i, k, iOr1, iAnd1, iAnd2, pLits[3]; // carry, in1, in2
+    Vec_Int_t * vMirrors = Vec_IntStart( Gia_ManObjNum(p) );
+    for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ )
+    {
+        pLits[0] = Acec_DetectLitPolarity( p, Vec_IntEntry(vRootXorSet, 4*i), Vec_IntEntry(vRootXorSet, 4*i+1) );
+        // get polarity of two new ones
+        for ( k = 1; k < 3; k++ )
+            pLits[k] = Acec_DetectLitPolarity( p, Vec_IntEntry(vRootXorSet, 4*i), Vec_IntEntry(vRootXorSet, 4*i+k+1) );
+        // create the gate
+        iOr1  = Gia_ManAppendOr( p, pLits[1], pLits[2] );
+        iAnd1 = Gia_ManAppendAnd( p, pLits[0], iOr1 );
+        iAnd2 = Gia_ManAppendAnd( p, pLits[1], pLits[2] );
+        pLits[0] = Gia_ManAppendOr( p, iAnd1, iAnd2 );
+        Vec_IntWriteEntry( vMirrors, Vec_IntEntry(vRootXorSet, 4*i+1), pLits[0] );
+    }
+    // remap the AIG using map
+    pNew = Acec_ManDerive( p, vMirrors );
+    Vec_IntFree( vMirrors );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Acec_DetectAdditional( Gia_Man_t * p, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Gia_Man_t * pNew;
+    Vec_Int_t * vRootXorSet;
+//    Vec_Int_t * vXors, * vAdds = Ree_ManComputeCuts( p, &vXors, 0 );
+
+    //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 );
+
+    clk = Abc_Clock();
+    vRootXorSet = Acec_CollectXorTops( p );
+    if ( vRootXorSet )
+    {
+        Acec_DetectComputeSupports( p, vRootXorSet );
+
+        pNew = Acec_DetectXorBuildNew( p, vRootXorSet );
+        Vec_IntFree( vRootXorSet );
+    }
+    else
+        pNew = Gia_ManDup( p );
+
+    printf( "Detected %d top XORs.  ", Vec_IntSize(vRootXorSet)/4 );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+//    Vec_IntFree( vXors );
+//    Vec_IntFree( vAdds );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acec_RewriteTop( Gia_Man_t * p, Acec_Box_t * pBox )
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( Gia_ManCoNum(p) + 1 );
+    Vec_Int_t * vLevel;
+    int i, k, iStart, iLit, Driver, Count = 0;
+    // determine how much to shift
+    Driver = Gia_ObjFaninId0p( p, Gia_ManCo(p, 0) );
+    Vec_WecForEachLevel( pBox->vRootLits, vLevel, iStart )
+        if ( Abc_Lit2Var(Vec_IntEntry(vLevel,0)) == Driver )
+            break;
+    assert( iStart < Gia_ManCoNum(p) );
+    //Vec_WecPrintLits( pBox->vRootLits );
+    Vec_WecForEachLevelStart( pBox->vRootLits, vLevel, i, iStart )
+    {
+        int In[3] = {0}, Out[2];
+        assert( Vec_IntSize(vLevel) > 0 );
+        assert( Vec_IntSize(vLevel) <= 3 );
+        if ( Vec_IntSize(vLevel) == 1 )
+        {
+            Vec_IntPush( vRes, Vec_IntEntry(vLevel, 0) );
+            continue;
+        }
+        Vec_IntForEachEntry( vLevel, iLit, k )
+            In[k] = iLit;
+        Acec_InsertFadd( p, In, Out );
+        Vec_IntPush( vRes, Out[0] );
+        if ( i+1 < Vec_WecSize(pBox->vRootLits) )
+            Vec_IntPush( Vec_WecEntry(pBox->vRootLits, i+1), Out[1] );
+        else
+            Vec_IntPush( Vec_WecPushLevel(pBox->vRootLits), Out[1] );
+        Count++;
+    }
+    assert( Vec_IntSize(vRes) >= Gia_ManCoNum(p) );
+    Vec_IntShrink( vRes, Gia_ManCoNum(p) );
+    printf( "Added %d adders for replace CLAs.  ", Count );
+    return vRes;
+}
+Gia_Man_t * Acec_RewriteReplace( Gia_Man_t * p, Vec_Int_t * vRes )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;  int i;
+    assert( Gia_ManCoNum(p) == Vec_IntSize(vRes) );
+    // create new manager
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        int iLit = Vec_IntEntry( vRes, i );
+        Gia_Obj_t * pRepr = Gia_ManObj( p, Abc_Lit2Var(iLit) );
+        pObj->Value = Gia_ManAppendCo( pNew, pRepr->Value );
+    }
+    // set correct phase
+    Gia_ManSetPhase( p );
+    Gia_ManSetPhase( pNew );
+    Gia_ManForEachCo( pNew, pObj, i )
+        if ( Gia_ObjPhase(pObj) != Gia_ObjPhase(Gia_ManCo(p, i)) )
+            Gia_ObjFlipFaninC0( pObj );
+    // remove dangling nodes
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+Gia_Man_t * Acec_ManDecla( Gia_Man_t * pGia, int fBooth, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    Gia_Man_t * pNew = NULL;
+    Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG(pGia) : NULL;
+    Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, 0, 0, fVerbose );
+    Vec_Int_t * vResult;
+    Vec_BitFreeP( &vIgnore );
+    if ( pBox == NULL ) // cannot match
+    {
+        printf( "Cannot find arithmetic boxes.\n" );
+        return Gia_ManDup( pGia );
+    }
+    vResult = Acec_RewriteTop( pGia, pBox );
+    Acec_BoxFreeP( &pBox );
+    pNew = Acec_RewriteReplace( pGia, vResult );
+    Vec_IntFree( vResult );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    return pNew;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/proof/acec/acecCo.c b/src/proof/acec/acecCo.c
index 1e8ed7bb..a997eb03 100644
--- a/src/proof/acec/acecCo.c
+++ b/src/proof/acec/acecCo.c
@@ -109,7 +109,7 @@ Vec_Int_t * Gia_PolynCoreOrder_int( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Wec
 {
     Vec_Int_t * vOrder  = Vec_IntAlloc( 1000 );
     Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(pGia) );
-    int i, k, Index, Driver, Entry1, Entry2 = -1;
+    int i, k, Index = -1, Driver, Entry1, Entry2 = -1;
     // mark roots
     Vec_IntForEachEntry( vRoots, Driver, i )
         Vec_BitWriteEntry( vIsRoot, Driver, 1 );
diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c
index ac7ee67b..1a575fbe 100644
--- a/src/proof/acec/acecCore.c
+++ b/src/proof/acec/acecCore.c
@@ -19,6 +19,9 @@
 ***********************************************************************/
 
 #include "acecInt.h"
+#include "proof/cec/cec.h"
+#include "misc/util/utilTruth.h"
+#include "misc/extra/extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -27,12 +30,452 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define TRUTH_UNUSED 0x1234567812345678
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p )
+{
+    memset( p, 0, sizeof(Acec_ParCec_t) );
+    p->nBTLimit       =    1000;    // conflict limit at a node
+    p->TimeLimit      =       0;    // the runtime limit in seconds
+    p->fMiter         =       0;    // input circuit is a miter
+    p->fDualOutput    =       0;    // dual-output miter
+    p->fTwoOutput     =       0;    // two-output miter
+    p->fSilent        =       0;    // print no messages
+    p->fVeryVerbose   =       0;    // verbose stats
+    p->fVerbose       =       0;    // verbose stats
+    p->iOutFail       =      -1;    // the number of failed output
+}  
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_VerifyClasses( Gia_Man_t * p, Vec_Wec_t * vLits, Vec_Wec_t * vReprs )
+{
+    Vec_Ptr_t * vFunc = Vec_PtrAlloc( Vec_WecSize(vLits) );
+    Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+    Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vLevel;
+    int i, j, k, Entry, Entry2, nOvers = 0, nErrors = 0;
+    Vec_WecForEachLevel( vLits, vLevel, i )
+    {
+        Vec_Wrd_t * vTruths = Vec_WrdAlloc( Vec_IntSize(vLevel) );
+        Vec_IntForEachEntry( vLevel, Entry, k )
+        {
+            word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp );
+            if ( Vec_IntSize(vSupp) > 6  )
+            {
+                nOvers++;
+                Vec_WrdPush( vTruths, TRUTH_UNUSED );
+                continue;
+            }
+            vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
+            if ( Vec_IntSize(vSupp) > 5  )
+            {
+                nOvers++;
+                Vec_WrdPush( vTruths, TRUTH_UNUSED );
+                continue;
+            }
+            Vec_WrdPush( vTruths, Truth );
+        }
+        Vec_PtrPush( vFunc, vTruths );
+    }
+    if ( nOvers )
+        printf( "Detected %d oversize support nodes.\n", nOvers );
+    Vec_IntFree( vSupp );
+    Vec_WrdFree( vTemp );
+    // verify the classes
+    Vec_WecForEachLevel( vReprs, vLevel, i )
+    {
+        Vec_Wrd_t * vTruths = (Vec_Wrd_t *)Vec_PtrEntry( vFunc, i );
+        Vec_IntForEachEntry( vLevel, Entry, k )
+        Vec_IntForEachEntryStart( vLevel, Entry2, j, k+1 )
+        {
+            word Truth = Vec_WrdEntry( vTruths, k );
+            word Truth2 = Vec_WrdEntry( vTruths, j );
+            if ( Entry == Entry2 )
+            {
+                nErrors++;
+                if ( Truth != Truth2 && Truth != TRUTH_UNUSED && Truth2 != TRUTH_UNUSED )
+                    printf( "Rank %d:  Lit %d and %d do not pass verification.\n", i, k, j );
+            }
+            if ( Entry == Abc_LitNot(Entry2) )
+            {
+                nErrors++;
+                if ( Truth != ~Truth2 && Truth != TRUTH_UNUSED && Truth2 != TRUTH_UNUSED )
+                    printf( "Rank %d:  Lit %d and %d do not pass verification.\n", i, k, j );
+            }
+        }
+    }
+    if ( nErrors )
+        printf( "Total errors in equivalence classes = %d.\n", nErrors );
+    Vec_VecFree( (Vec_Vec_t *)vFunc );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Acec_CommonStart( Gia_Man_t * pBase, Gia_Man_t * pAdd )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManFillValue( pAdd );
+    Gia_ManConst0(pAdd)->Value = 0;
+    if ( pBase == NULL )
+    {
+        pBase = Gia_ManStart( Gia_ManObjNum(pAdd) );
+        pBase->pName = Abc_UtilStrsav( pAdd->pName );
+        pBase->pSpec = Abc_UtilStrsav( pAdd->pSpec );
+        Gia_ManForEachCi( pAdd, pObj, i )
+            pObj->Value = Gia_ManAppendCi(pBase);
+        Gia_ManHashAlloc( pBase );
+    }
+    else
+    {
+        assert( Gia_ManCiNum(pBase) == Gia_ManCiNum(pAdd) );
+        Gia_ManForEachCi( pAdd, pObj, i )
+            pObj->Value = Gia_Obj2Lit( pBase, Gia_ManCi(pBase, i) );
+    }
+    Gia_ManForEachAnd( pAdd, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pBase, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    return pBase;
+}
+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 )
+    {
+        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 )
+{
+    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 )
+{
+    int i, j, best_i;
+    for ( i = 0; i < nSize-1; i++ )
+    {
+        best_i = i;
+        for ( j = i+1; j < nSize; j++ )
+            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( Gia_Man_t * p, Vec_Wec_t * vLits, int * pCostLits, int fVerbose )
+{
+    Vec_Int_t * vSupp;
+    Vec_Wrd_t * vTemp;
+    Vec_Int_t * vLevel;
+    int i, k, Entry;
+    printf( "Leaf literals and their classes:\n" );
+    Vec_WecForEachLevel( vLits, vLevel, i )
+    {
+        if ( Vec_IntSize(vLevel) == 0 )
+            continue;
+        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" );
+    }
+    if ( !fVerbose )
+        return;
+    vSupp = Vec_IntAlloc( 100 );
+    vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+    Vec_WecForEachLevel( vLits, vLevel, i )
+    {
+        //if ( i != 20 )
+        //    continue;
+        if ( Vec_IntSize(vLevel) == 0 )
+            continue;
+        Vec_IntForEachEntry( vLevel, Entry, k )
+        {
+            word Truth = Gia_ObjComputeTruth6Cis( p, Entry, vSupp, vTemp );
+/*
+            {
+                int iObj = Abc_Lit2Var(Entry);
+                Gia_Man_t * pGia0 = Gia_ManDupAndCones( p, &iObj, 1, 1 );
+                Gia_ManShow( pGia0, NULL, 0, 0, 0 );
+                Gia_ManStop( pGia0 );
+            }
+*/
+            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 Vec_IntInsertOrder( Vec_Int_t * vLits, Vec_Int_t * vClasses, int Lit, int Class )
+{
+    int i;
+    for ( i = Vec_IntSize(vClasses)-1; i >= 0; i-- )
+        if ( Vec_IntEntry(vClasses,i) >= Class )
+            break;
+    Vec_IntInsert( vLits, i+1, Lit );
+    Vec_IntInsert( vClasses, i+1, Class );
+}
+void Acec_MoveDuplicates( Vec_Wec_t * vLits, Vec_Wec_t * vClasses )
+{
+    Vec_Int_t * vLevel1, * vLevel2; 
+    int i, k, Prev, This, Entry, Counter = 0;
+    Vec_WecForEachLevel( vLits, vLevel1, i )
+    {
+        if ( i == Vec_WecSize(vLits) - 1 )
+            break;
+        vLevel2 = Vec_WecEntry(vClasses, i);
+        assert( Vec_IntSize(vLevel1) == Vec_IntSize(vLevel2) );
+        Prev = -1;
+        Vec_IntForEachEntry( vLevel2, This, k )
+        {
+            if ( Prev != This )
+            {
+                Prev = This;
+                continue;
+            }
+            Prev = -1;
+            Entry = Vec_IntEntry( vLevel1, k );
+
+            Vec_IntDrop( vLevel1, k );
+            Vec_IntDrop( vLevel2, k-- );
+
+            Vec_IntDrop( vLevel1, k );
+            Vec_IntDrop( vLevel2, k-- );
+
+            Vec_IntInsertOrder( Vec_WecEntry(vLits, i+1), Vec_WecEntry(vClasses, i+1), Entry, This );
+
+            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 )
+{
+    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 );
+        Vec_WecInsertLevel( vRes0, 0 );
+        printf( "Shifted one level up.\n" );
+    }
+    else if ( nCommonMinus > nCommonPlus && nCommonMinus > nCommon )
+    {
+        Vec_WecInsertLevel( vLits1, 0 );
+        Vec_WecInsertLevel( vRoots1, 0 );
+        Vec_WecInsertLevel( vRes1, 0 );
+        printf( "Shifted one level down.\n" );
+    }
+    Acec_MoveDuplicates( vLits0, vRes0 );
+    Acec_MoveDuplicates( vLits1, vRes1 );
+
+    //Vec_WecPrintLits( vLits1 );
+    //printf( "Input literals:\n" );
+    //Vec_WecPrintLits( vLits0 );
+    //printf( "Equiv classes:\n" );
+    //Vec_WecPrintLits( vRes0 );
+    //printf( "Input literals:\n" );
+    //Vec_WecPrintLits( vLits1 );
+    //printf( "Equiv classes:\n" );
+    //Vec_WecPrintLits( vRes1 );
+    //Acec_VerifyClasses( pGia0, vLits0, vRes0 );
+    //Acec_VerifyClasses( pGia1, vLits1, vRes1 );
+    Vec_WecFree( vRes0 );
+    Vec_WecFree( vRes1 );
+}
+int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
+{
+    Vec_Int_t * vMap0, * vMap1, * vLevel; 
+    int i, nSize, nTotal;
+    Acec_ComputeEquivClasses( pBox0->pGia, pBox1->pGia, &vMap0, &vMap1 );
+    // sort nodes in the classes by their equivalences
+    Vec_WecForEachLevel( pBox0->vLeafLits, vLevel, i )
+        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_MatchCheckShift( pBox0->pGia, pBox1->pGia, 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 );
+    //printf( "Outputs:\n" );
+    //Vec_WecPrintLits( pBox0->vRootLits );
+    //printf( "Outputs:\n" );
+    //Vec_WecPrintLits( pBox1->vRootLits );
+
+    // reorder nodes to have the same order
+    assert( pBox0->vShared == NULL );
+    assert( pBox1->vShared == NULL );
+    pBox0->vShared = Vec_WecStart( Vec_WecSize(pBox0->vLeafLits) );
+    pBox1->vShared = Vec_WecStart( Vec_WecSize(pBox1->vLeafLits) );
+    pBox0->vUnique = Vec_WecStart( Vec_WecSize(pBox0->vLeafLits) );
+    pBox1->vUnique = Vec_WecStart( Vec_WecSize(pBox1->vLeafLits) );
+    nSize = Abc_MinInt( Vec_WecSize(pBox0->vLeafLits), Vec_WecSize(pBox1->vLeafLits) );
+    Vec_WecForEachLevelStart( pBox0->vLeafLits, vLevel, i, nSize )
+        Vec_IntAppend( Vec_WecEntry(pBox0->vUnique, i), vLevel );
+    Vec_WecForEachLevelStart( pBox1->vLeafLits, vLevel, i, nSize )
+        Vec_IntAppend( Vec_WecEntry(pBox1->vUnique, i), vLevel );
+    for ( i = 0; i < nSize; i++ )
+    {
+        Vec_Int_t * vShared0 = Vec_WecEntry( pBox0->vShared, i );
+        Vec_Int_t * vShared1 = Vec_WecEntry( pBox1->vShared, i );
+        Vec_Int_t * vUnique0 = Vec_WecEntry( pBox0->vUnique, i );
+        Vec_Int_t * vUnique1 = Vec_WecEntry( pBox1->vUnique, i );
+
+        Vec_Int_t * vLevel0 = Vec_WecEntry( pBox0->vLeafLits, i );
+        Vec_Int_t * vLevel1 = Vec_WecEntry( pBox1->vLeafLits, i );
+        int * pBeg0 = Vec_IntArray(vLevel0);
+        int * pBeg1 = Vec_IntArray(vLevel1);
+        int * pEnd0 = Vec_IntLimit(vLevel0);
+        int * pEnd1 = Vec_IntLimit(vLevel1);
+        while ( pBeg0 < pEnd0 && pBeg1 < pEnd1 )
+        {
+            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++ );
+                Vec_IntPush( vShared1, *pBeg1++ );
+            }
+            else if ( Entry0 > Entry1 )
+                Vec_IntPush( vUnique0, *pBeg0++ );
+            else 
+                Vec_IntPush( vUnique1, *pBeg1++ );
+        }
+        while ( pBeg0 < pEnd0 )
+            Vec_IntPush( vUnique0, *pBeg0++ );
+        while ( pBeg1 < pEnd1 )
+            Vec_IntPush( vUnique1, *pBeg1++ );
+        assert( Vec_IntSize(vShared0) == Vec_IntSize(vShared1) );
+        assert( Vec_IntSize(vShared0) + Vec_IntSize(vUnique0) == Vec_IntSize(vLevel0) );
+        assert( Vec_IntSize(vShared1) + Vec_IntSize(vUnique1) == Vec_IntSize(vLevel1) );
+    }
+    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->vShared, Vec_IntArray(vMap0), 0 );
+    //Acec_MatchPrintEquivLits( pBox1->pGia, pBox1->vShared, Vec_IntArray(vMap1), 0 );
+    //printf( "\n" );
+
+    //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;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -42,15 +485,63 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-int Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars )
-{
-    Vec_Int_t * vOrder0 = Gia_PolynReorder( pGia0, pPars->fVerbose, pPars->fVeryVerbose );
-    Vec_Int_t * vOrder1 = Gia_PolynReorder( pGia1, pPars->fVerbose, pPars->fVeryVerbose );
-    Gia_PolynBuild( pGia0, vOrder0, 0, pPars->fVerbose, pPars->fVeryVerbose );
-    Gia_PolynBuild( pGia1, vOrder1, 0, pPars->fVerbose, pPars->fVeryVerbose );
-    Vec_IntFree( vOrder0 );
-    Vec_IntFree( vOrder1 );
-    return 1;
+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;
+//    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
+        printf( "Cannot match arithmetic boxes in LHS and RHS. Trying regular CEC.\n" );
+    else 
+    {
+        pGia0n = Acec_InsertBox( pBox0, 0 );
+        pGia1n = Acec_InsertBox( pBox1, 0 );
+        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 );
+
+        Gia_ManPatchCoDriver( pGia0n, Gia_ManCoNum(pGia0n)-2, 0 );
+        Gia_ManPatchCoDriver( pGia1n, Gia_ManCoNum(pGia1n)-2, 0 );
+    }
+    // solve regular CEC problem 
+    Cec_ManCecSetDefaultParams( pCecPars );
+    pCecPars->nBTLimit = pPars->nBTLimit;
+    pMiter = Gia_ManMiter( pGia0n, pGia1n, 0, 1, 0, 0, pPars->fVerbose );
+    if ( pMiter )
+    {
+        int fDumpMiter = 0;
+        if ( fDumpMiter )
+        {
+            Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "acec_miter.aig" );
+            Gia_AigerWrite( pMiter, "acec_miter.aig", 0, 0 );
+        }
+        status = Cec_ManVerify( pMiter, pCecPars );
+        ABC_SWAP( Abc_Cex_t *, pGia0->pCexComb, pMiter->pCexComb );
+        Gia_ManStop( pMiter );
+    }
+    else
+        printf( "Miter computation has failed.\n" );
+    if ( pGia0n != pGia0 )
+        Gia_ManStop( pGia0n );
+    if ( pGia1n != pGia1 )
+        Gia_ManStop( pGia1n );
+    Acec_BoxFreeP( &pBox0 );
+    Acec_BoxFreeP( &pBox1 );
+    return status;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h
index e761e56e..c4c8061e 100644
--- a/src/proof/acec/acecInt.h
+++ b/src/proof/acec/acecInt.h
@@ -27,7 +27,6 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include "aig/gia/gia.h"
-#include "proof/cec/cec.h"
 #include "acec.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -38,6 +37,17 @@
 ABC_NAMESPACE_HEADER_START
  
 
+typedef struct Acec_Box_t_ Acec_Box_t;
+struct Acec_Box_t_
+{
+    Gia_Man_t *    pGia;      // AIG manager
+    Vec_Wec_t *    vAdds;     // adders 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
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -46,6 +56,12 @@ ABC_NAMESPACE_HEADER_START
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
+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)); }
+
 ////////////////////////////////////////////////////////////////////////
 ///                             ITERATORS                            ///
 ////////////////////////////////////////////////////////////////////////
@@ -54,9 +70,28 @@ ABC_NAMESPACE_HEADER_START
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== acecCo.c ========================================================*/
+extern Vec_Int_t *   Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts );
+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 );
+extern Vec_Bit_t *   Acec_MultMarkPPs( Gia_Man_t * p );
+/*=== acecNorm.c ========================================================*/
+extern void          Acec_InsertFadd( Gia_Man_t * pNew, int In[3], int Out[2] );
+extern Gia_Man_t *   Acec_InsertBox( Acec_Box_t * pBox, int fAll );
+/*=== acecTree.c ========================================================*/
+extern void          Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds );
+extern void          Acec_TreePrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds );
+extern Acec_Box_t *  Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut, int fVerbose );
+extern void          Acec_BoxFreeP( Acec_Box_t ** ppBox );
 /*=== acecUtil.c ========================================================*/
 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_ProduceBox( Gia_Man_t * p, int fVerbose );
+
+
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c
new file mode 100644
index 00000000..c63fdde2
--- /dev/null
+++ b/src/proof/acec/acecMult.c
@@ -0,0 +1,617 @@
+/**CFile****************************************************************
+
+  FileName    [acecMult.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [CEC for arithmetic circuits.]
+
+  Synopsis    [Multiplier.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: acecMult.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/extra/extra.h"
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+unsigned s_Classes4a[96] = {
+    0xD728, 0xB748, 0x9F60, 0xD278, 0xB478, 0x96F0, 0xC66C, 0x96CC, 0x9C6C, 0x96AA, 0xA66A, 0x9A6A,
+    0x28D7, 0x48B7, 0x609F, 0x2D87, 0x4B87, 0x690F, 0x3993, 0x6933, 0x6393, 0x6955, 0x5995, 0x6595,
+    0xEB14, 0xED12, 0xF906, 0xE1B4, 0xE1D2, 0xF096, 0xC99C, 0xCC96, 0xC9C6, 0xAA96, 0xA99A, 0xA9A6,
+    0x14EB, 0x12ED, 0x06F9, 0x1E4B, 0x1E2D, 0x0F69, 0x3663, 0x3369, 0x3639, 0x5569, 0x5665, 0x5659,
+    0x7D82, 0x7B84, 0x6F90, 0x78D2, 0x78B4, 0x69F0, 0x6CC6, 0x69CC, 0x6C9C, 0x69AA, 0x6AA6, 0x6A9A,
+    0x827D, 0x847B, 0x906F, 0x872D, 0x874B, 0x960F, 0x9339, 0x9633, 0x9363, 0x9655, 0x9559, 0x9565,
+    0xBE41, 0xDE21, 0xF609, 0xB4E1, 0xD2E1, 0xF069, 0x9CC9, 0xCC69, 0xC6C9, 0xAA69, 0x9AA9, 0xA6A9,
+    0x41BE, 0x21DE, 0x09F6, 0x4B1E, 0x2D1E, 0x0F96, 0x6336, 0x3396, 0x3936, 0x5596, 0x6556, 0x5956
+};
+
+unsigned s_Classes4b[384] = {
+    0x35C0, 0x53A0, 0x1DC0, 0x4788, 0x2788, 0x1BA0, 0x3C50, 0x5A30, 0x1CD0, 0x4878, 0x2878, 0x1AB0,
+    0x34C4, 0x606C, 0x3C44, 0x660C, 0x268C, 0x286C, 0x606A, 0x52A2, 0x486A, 0x468A, 0x660A, 0x5A22,
+    0x3AC0, 0x5CA0, 0x2EC0, 0x7488, 0x7288, 0x4EA0, 0x3CA0, 0x5AC0, 0x2CE0, 0x7848, 0x7828, 0x4AE0,
+    0x38C8, 0x6C60, 0x3C88, 0x66C0, 0x62C8, 0x6C28, 0x6A60, 0x58A8, 0x6A48, 0x64A8, 0x66A0, 0x5A88,
+    0xC530, 0xA350, 0xD10C, 0x8B44, 0x8D22, 0xB10A, 0xC350, 0xA530, 0xD01C, 0x84B4, 0x82D2, 0xB01A,
+    0xC434, 0x909C, 0xC344, 0x990C, 0x8C26, 0x82C6, 0x909A, 0xA252, 0x84A6, 0x8A46, 0x990A, 0xA522,
+    0xCA30, 0xAC50, 0xE20C, 0xB844, 0xD822, 0xE40A, 0xC3A0, 0xA5C0, 0xE02C, 0xB484, 0xD282, 0xE04A,
+    0xC838, 0x9C90, 0xC388, 0x99C0, 0xC862, 0xC682, 0x9A90, 0xA858, 0xA684, 0xA864, 0x99A0, 0xA588,
+    0x530C, 0x350A, 0x4730, 0x1D22, 0x1B44, 0x2750, 0x503C, 0x305A, 0x4370, 0x12D2, 0x14B4, 0x2570,
+    0x434C, 0x06C6, 0x443C, 0x0C66, 0x194C, 0x149C, 0x06A6, 0x252A, 0x129A, 0x192A, 0x0A66, 0x225A,
+    0xA30C, 0xC50A, 0x8B30, 0xD122, 0xB144, 0x8D50, 0xA03C, 0xC05A, 0x83B0, 0xD212, 0xB414, 0x85D0,
+    0x838C, 0xC606, 0x883C, 0xC066, 0x91C4, 0x9C14, 0xA606, 0x858A, 0x9A12, 0x91A2, 0xA066, 0x885A,
+    0x5C03, 0x3A05, 0x7403, 0x2E11, 0x4E11, 0x7205, 0x50C3, 0x30A5, 0x7043, 0x21E1, 0x41E1, 0x7025,
+    0x4C43, 0x09C9, 0x44C3, 0x0C99, 0x4C19, 0x41C9, 0x09A9, 0x2A25, 0x21A9, 0x2A19, 0x0A99, 0x22A5,
+    0xAC03, 0xCA05, 0xB803, 0xE211, 0xE411, 0xD805, 0xA0C3, 0xC0A5, 0xB083, 0xE121, 0xE141, 0xD085,
+    0x8C83, 0xC909, 0x88C3, 0xC099, 0xC491, 0xC941, 0xA909, 0x8A85, 0xA921, 0xA291, 0xA099, 0x88A5,
+    0xC035, 0xA053, 0xC01D, 0x8847, 0x8827, 0xA01B, 0xC305, 0xA503, 0xC10D, 0x8487, 0x8287, 0xA10B,
+    0xC131, 0x9093, 0xC311, 0x9903, 0x8923, 0x8293, 0x9095, 0xA151, 0x8495, 0x8945, 0x9905, 0xA511,
+    0xC03A, 0xA05C, 0xC02E, 0x8874, 0x8872, 0xA04E, 0xC30A, 0xA50C, 0xC20E, 0x8784, 0x8782, 0xA40E,
+    0xC232, 0x9390, 0xC322, 0x9930, 0x9832, 0x9382, 0x9590, 0xA454, 0x9584, 0x9854, 0x9950, 0xA544,
+    0x30C5, 0x50A3, 0x0CD1, 0x448B, 0x228D, 0x0AB1, 0x3C05, 0x5A03, 0x0DC1, 0x484B, 0x282D, 0x0BA1,
+    0x31C1, 0x6063, 0x3C11, 0x6603, 0x2389, 0x2839, 0x6065, 0x51A1, 0x4859, 0x4589, 0x6605, 0x5A11,
+    0x30CA, 0x50AC, 0x0CE2, 0x44B8, 0x22D8, 0x0AE4, 0x3C0A, 0x5A0C, 0x0EC2, 0x4B48, 0x2D28, 0x0EA4,
+    0x32C2, 0x6360, 0x3C22, 0x6630, 0x3298, 0x3928, 0x6560, 0x54A4, 0x5948, 0x5498, 0x6650, 0x5A44,
+    0x0C53, 0x0A35, 0x3047, 0x221D, 0x441B, 0x5027, 0x05C3, 0x03A5, 0x3407, 0x212D, 0x414B, 0x5207,
+    0x1C13, 0x0939, 0x11C3, 0x0399, 0x4613, 0x4163, 0x0959, 0x1A15, 0x2165, 0x2615, 0x0599, 0x11A5,
+    0x0CA3, 0x0AC5, 0x308B, 0x22D1, 0x44B1, 0x508D, 0x0AC3, 0x0CA5, 0x380B, 0x2D21, 0x4B41, 0x580D,
+    0x2C23, 0x3909, 0x22C3, 0x3099, 0x6431, 0x6341, 0x5909, 0x4A45, 0x6521, 0x6251, 0x5099, 0x44A5,
+    0x035C, 0x053A, 0x0374, 0x112E, 0x114E, 0x0572, 0x053C, 0x035A, 0x0734, 0x121E, 0x141E, 0x0752,
+    0x131C, 0x0636, 0x113C, 0x0366, 0x1346, 0x1436, 0x0656, 0x151A, 0x1256, 0x1526, 0x0566, 0x115A,
+    0x03AC, 0x05CA, 0x03B8, 0x11E2, 0x11E4, 0x05D8, 0x0A3C, 0x0C5A, 0x0B38, 0x1E12, 0x1E14, 0x0D58,
+    0x232C, 0x3606, 0x223C, 0x3066, 0x3164, 0x3614, 0x5606, 0x454A, 0x5612, 0x5162, 0x5066, 0x445A
+};
+
+unsigned s_Classes4c[768] = {
+    0x35C0, 0x53A0, 0x1DC0, 0x4788, 0x2788, 0x1BA0, 0x3C50, 0x5A30, 0x1CD0, 0x4878, 0x2878, 0x1AB0,
+    0x34C4, 0x606C, 0x3C44, 0x660C, 0x268C, 0x286C, 0x606A, 0x52A2, 0x486A, 0x468A, 0x660A, 0x5A22,
+    0xCA3F, 0xAC5F, 0xE23F, 0xB877, 0xD877, 0xE45F, 0xC3AF, 0xA5CF, 0xE32F, 0xB787, 0xD787, 0xE54F,
+    0xCB3B, 0x9F93, 0xC3BB, 0x99F3, 0xD973, 0xD793, 0x9F95, 0xAD5D, 0xB795, 0xB975, 0x99F5, 0xA5DD,
+    0x3AC0, 0x5CA0, 0x2EC0, 0x7488, 0x7288, 0x4EA0, 0x3CA0, 0x5AC0, 0x2CE0, 0x7848, 0x7828, 0x4AE0,
+    0x38C8, 0x6C60, 0x3C88, 0x66C0, 0x62C8, 0x6C28, 0x6A60, 0x58A8, 0x6A48, 0x64A8, 0x66A0, 0x5A88,
+    0xC53F, 0xA35F, 0xD13F, 0x8B77, 0x8D77, 0xB15F, 0xC35F, 0xA53F, 0xD31F, 0x87B7, 0x87D7, 0xB51F,
+    0xC737, 0x939F, 0xC377, 0x993F, 0x9D37, 0x93D7, 0x959F, 0xA757, 0x95B7, 0x9B57, 0x995F, 0xA577,
+    0xC530, 0xA350, 0xD10C, 0x8B44, 0x8D22, 0xB10A, 0xC350, 0xA530, 0xD01C, 0x84B4, 0x82D2, 0xB01A,
+    0xC434, 0x909C, 0xC344, 0x990C, 0x8C26, 0x82C6, 0x909A, 0xA252, 0x84A6, 0x8A46, 0x990A, 0xA522,
+    0x3ACF, 0x5CAF, 0x2EF3, 0x74BB, 0x72DD, 0x4EF5, 0x3CAF, 0x5ACF, 0x2FE3, 0x7B4B, 0x7D2D, 0x4FE5,
+    0x3BCB, 0x6F63, 0x3CBB, 0x66F3, 0x73D9, 0x7D39, 0x6F65, 0x5DAD, 0x7B59, 0x75B9, 0x66F5, 0x5ADD,
+    0xCA30, 0xAC50, 0xE20C, 0xB844, 0xD822, 0xE40A, 0xC3A0, 0xA5C0, 0xE02C, 0xB484, 0xD282, 0xE04A,
+    0xC838, 0x9C90, 0xC388, 0x99C0, 0xC862, 0xC682, 0x9A90, 0xA858, 0xA684, 0xA864, 0x99A0, 0xA588,
+    0x35CF, 0x53AF, 0x1DF3, 0x47BB, 0x27DD, 0x1BF5, 0x3C5F, 0x5A3F, 0x1FD3, 0x4B7B, 0x2D7D, 0x1FB5,
+    0x37C7, 0x636F, 0x3C77, 0x663F, 0x379D, 0x397D, 0x656F, 0x57A7, 0x597B, 0x579B, 0x665F, 0x5A77,
+    0x530C, 0x350A, 0x4730, 0x1D22, 0x1B44, 0x2750, 0x503C, 0x305A, 0x4370, 0x12D2, 0x14B4, 0x2570,
+    0x434C, 0x06C6, 0x443C, 0x0C66, 0x194C, 0x149C, 0x06A6, 0x252A, 0x129A, 0x192A, 0x0A66, 0x225A,
+    0xACF3, 0xCAF5, 0xB8CF, 0xE2DD, 0xE4BB, 0xD8AF, 0xAFC3, 0xCFA5, 0xBC8F, 0xED2D, 0xEB4B, 0xDA8F,
+    0xBCB3, 0xF939, 0xBBC3, 0xF399, 0xE6B3, 0xEB63, 0xF959, 0xDAD5, 0xED65, 0xE6D5, 0xF599, 0xDDA5,
+    0xA30C, 0xC50A, 0x8B30, 0xD122, 0xB144, 0x8D50, 0xA03C, 0xC05A, 0x83B0, 0xD212, 0xB414, 0x85D0,
+    0x838C, 0xC606, 0x883C, 0xC066, 0x91C4, 0x9C14, 0xA606, 0x858A, 0x9A12, 0x91A2, 0xA066, 0x885A,
+    0x5CF3, 0x3AF5, 0x74CF, 0x2EDD, 0x4EBB, 0x72AF, 0x5FC3, 0x3FA5, 0x7C4F, 0x2DED, 0x4BEB, 0x7A2F,
+    0x7C73, 0x39F9, 0x77C3, 0x3F99, 0x6E3B, 0x63EB, 0x59F9, 0x7A75, 0x65ED, 0x6E5D, 0x5F99, 0x77A5,
+    0x5C03, 0x3A05, 0x7403, 0x2E11, 0x4E11, 0x7205, 0x50C3, 0x30A5, 0x7043, 0x21E1, 0x41E1, 0x7025,
+    0x4C43, 0x09C9, 0x44C3, 0x0C99, 0x4C19, 0x41C9, 0x09A9, 0x2A25, 0x21A9, 0x2A19, 0x0A99, 0x22A5,
+    0xA3FC, 0xC5FA, 0x8BFC, 0xD1EE, 0xB1EE, 0x8DFA, 0xAF3C, 0xCF5A, 0x8FBC, 0xDE1E, 0xBE1E, 0x8FDA,
+    0xB3BC, 0xF636, 0xBB3C, 0xF366, 0xB3E6, 0xBE36, 0xF656, 0xD5DA, 0xDE56, 0xD5E6, 0xF566, 0xDD5A,
+    0xAC03, 0xCA05, 0xB803, 0xE211, 0xE411, 0xD805, 0xA0C3, 0xC0A5, 0xB083, 0xE121, 0xE141, 0xD085,
+    0x8C83, 0xC909, 0x88C3, 0xC099, 0xC491, 0xC941, 0xA909, 0x8A85, 0xA921, 0xA291, 0xA099, 0x88A5,
+    0x53FC, 0x35FA, 0x47FC, 0x1DEE, 0x1BEE, 0x27FA, 0x5F3C, 0x3F5A, 0x4F7C, 0x1EDE, 0x1EBE, 0x2F7A,
+    0x737C, 0x36F6, 0x773C, 0x3F66, 0x3B6E, 0x36BE, 0x56F6, 0x757A, 0x56DE, 0x5D6E, 0x5F66, 0x775A,
+    0xC035, 0xA053, 0xC01D, 0x8847, 0x8827, 0xA01B, 0xC305, 0xA503, 0xC10D, 0x8487, 0x8287, 0xA10B,
+    0xC131, 0x9093, 0xC311, 0x9903, 0x8923, 0x8293, 0x9095, 0xA151, 0x8495, 0x8945, 0x9905, 0xA511,
+    0x3FCA, 0x5FAC, 0x3FE2, 0x77B8, 0x77D8, 0x5FE4, 0x3CFA, 0x5AFC, 0x3EF2, 0x7B78, 0x7D78, 0x5EF4,
+    0x3ECE, 0x6F6C, 0x3CEE, 0x66FC, 0x76DC, 0x7D6C, 0x6F6A, 0x5EAE, 0x7B6A, 0x76BA, 0x66FA, 0x5AEE,
+    0xC03A, 0xA05C, 0xC02E, 0x8874, 0x8872, 0xA04E, 0xC30A, 0xA50C, 0xC20E, 0x8784, 0x8782, 0xA40E,
+    0xC232, 0x9390, 0xC322, 0x9930, 0x9832, 0x9382, 0x9590, 0xA454, 0x9584, 0x9854, 0x9950, 0xA544,
+    0x3FC5, 0x5FA3, 0x3FD1, 0x778B, 0x778D, 0x5FB1, 0x3CF5, 0x5AF3, 0x3DF1, 0x787B, 0x787D, 0x5BF1,
+    0x3DCD, 0x6C6F, 0x3CDD, 0x66CF, 0x67CD, 0x6C7D, 0x6A6F, 0x5BAB, 0x6A7B, 0x67AB, 0x66AF, 0x5ABB,
+    0x30C5, 0x50A3, 0x0CD1, 0x448B, 0x228D, 0x0AB1, 0x3C05, 0x5A03, 0x0DC1, 0x484B, 0x282D, 0x0BA1,
+    0x31C1, 0x6063, 0x3C11, 0x6603, 0x2389, 0x2839, 0x6065, 0x51A1, 0x4859, 0x4589, 0x6605, 0x5A11,
+    0xCF3A, 0xAF5C, 0xF32E, 0xBB74, 0xDD72, 0xF54E, 0xC3FA, 0xA5FC, 0xF23E, 0xB7B4, 0xD7D2, 0xF45E,
+    0xCE3E, 0x9F9C, 0xC3EE, 0x99FC, 0xDC76, 0xD7C6, 0x9F9A, 0xAE5E, 0xB7A6, 0xBA76, 0x99FA, 0xA5EE,
+    0x30CA, 0x50AC, 0x0CE2, 0x44B8, 0x22D8, 0x0AE4, 0x3C0A, 0x5A0C, 0x0EC2, 0x4B48, 0x2D28, 0x0EA4,
+    0x32C2, 0x6360, 0x3C22, 0x6630, 0x3298, 0x3928, 0x6560, 0x54A4, 0x5948, 0x5498, 0x6650, 0x5A44,
+    0xCF35, 0xAF53, 0xF31D, 0xBB47, 0xDD27, 0xF51B, 0xC3F5, 0xA5F3, 0xF13D, 0xB4B7, 0xD2D7, 0xF15B,
+    0xCD3D, 0x9C9F, 0xC3DD, 0x99CF, 0xCD67, 0xC6D7, 0x9A9F, 0xAB5B, 0xA6B7, 0xAB67, 0x99AF, 0xA5BB,
+    0x0C53, 0x0A35, 0x3047, 0x221D, 0x441B, 0x5027, 0x05C3, 0x03A5, 0x3407, 0x212D, 0x414B, 0x5207,
+    0x1C13, 0x0939, 0x11C3, 0x0399, 0x4613, 0x4163, 0x0959, 0x1A15, 0x2165, 0x2615, 0x0599, 0x11A5,
+    0xF3AC, 0xF5CA, 0xCFB8, 0xDDE2, 0xBBE4, 0xAFD8, 0xFA3C, 0xFC5A, 0xCBF8, 0xDED2, 0xBEB4, 0xADF8,
+    0xE3EC, 0xF6C6, 0xEE3C, 0xFC66, 0xB9EC, 0xBE9C, 0xF6A6, 0xE5EA, 0xDE9A, 0xD9EA, 0xFA66, 0xEE5A,
+    0x0CA3, 0x0AC5, 0x308B, 0x22D1, 0x44B1, 0x508D, 0x0AC3, 0x0CA5, 0x380B, 0x2D21, 0x4B41, 0x580D,
+    0x2C23, 0x3909, 0x22C3, 0x3099, 0x6431, 0x6341, 0x5909, 0x4A45, 0x6521, 0x6251, 0x5099, 0x44A5,
+    0xF35C, 0xF53A, 0xCF74, 0xDD2E, 0xBB4E, 0xAF72, 0xF53C, 0xF35A, 0xC7F4, 0xD2DE, 0xB4BE, 0xA7F2,
+    0xD3DC, 0xC6F6, 0xDD3C, 0xCF66, 0x9BCE, 0x9CBE, 0xA6F6, 0xB5BA, 0x9ADE, 0x9DAE, 0xAF66, 0xBB5A,
+    0x035C, 0x053A, 0x0374, 0x112E, 0x114E, 0x0572, 0x053C, 0x035A, 0x0734, 0x121E, 0x141E, 0x0752,
+    0x131C, 0x0636, 0x113C, 0x0366, 0x1346, 0x1436, 0x0656, 0x151A, 0x1256, 0x1526, 0x0566, 0x115A,
+    0xFCA3, 0xFAC5, 0xFC8B, 0xEED1, 0xEEB1, 0xFA8D, 0xFAC3, 0xFCA5, 0xF8CB, 0xEDE1, 0xEBE1, 0xF8AD,
+    0xECE3, 0xF9C9, 0xEEC3, 0xFC99, 0xECB9, 0xEBC9, 0xF9A9, 0xEAE5, 0xEDA9, 0xEAD9, 0xFA99, 0xEEA5,
+    0x03AC, 0x05CA, 0x03B8, 0x11E2, 0x11E4, 0x05D8, 0x0A3C, 0x0C5A, 0x0B38, 0x1E12, 0x1E14, 0x0D58,
+    0x232C, 0x3606, 0x223C, 0x3066, 0x3164, 0x3614, 0x5606, 0x454A, 0x5612, 0x5162, 0x5066, 0x445A,
+    0xFC53, 0xFA35, 0xFC47, 0xEE1D, 0xEE1B, 0xFA27, 0xF5C3, 0xF3A5, 0xF4C7, 0xE1ED, 0xE1EB, 0xF2A7,
+    0xDCD3, 0xC9F9, 0xDDC3, 0xCF99, 0xCE9B, 0xC9EB, 0xA9F9, 0xBAB5, 0xA9ED, 0xAE9D, 0xAF99, 0xBBA5
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes NPN-canonical form using brute-force methods.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Extra_TruthCanonNPN2( unsigned uTruth, int nVars, Vec_Int_t * vRes )
+{
+    static int nVarsOld, nPerms;
+    static char ** pPerms = NULL;
+
+    unsigned uTruthMin, uTruthC, uPhase, uPerm;
+    int nMints, k, i;
+
+    if ( pPerms == NULL )
+    {
+        nPerms = Extra_Factorial( nVars );   
+        pPerms = Extra_Permutations( nVars );
+        nVarsOld = nVars;
+    }
+    else if ( nVarsOld != nVars )
+    {
+        ABC_FREE( pPerms );
+        nPerms = Extra_Factorial( nVars );   
+        pPerms = Extra_Permutations( nVars );
+        nVarsOld = nVars;
+    }
+
+    nMints    = (1 << nVars);
+    uTruthC   = (unsigned)( (~uTruth) & ((~((unsigned)0)) >> (32-nMints)) );
+    uTruthMin = 0xFFFFFFFF;
+    for ( i = 0; i < nMints; i++ )
+    {
+        uPhase = Extra_TruthPolarize( uTruth, i, nVars ); 
+        for ( k = 0; k < nPerms; k++ )
+        {
+            uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
+            Vec_IntPushUnique( vRes, uPerm );
+            if ( uTruthMin > uPerm )
+                uTruthMin = uPerm;
+        }
+        uPhase = Extra_TruthPolarize( uTruthC, i, nVars ); 
+        for ( k = 0; k < nPerms; k++ )
+        {
+            uPerm = Extra_TruthPermute( uPhase, pPerms[k], nVars, 0 );
+            Vec_IntPushUnique( vRes, uPerm );
+            if ( uTruthMin > uPerm )
+                uTruthMin = uPerm;
+        }
+    }
+    return uTruthMin;
+}
+
+void Acec_MultFuncTest5()
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( 1000 );
+    int i, Entry;
+
+    unsigned Truth = 0xF335ACC0;
+    unsigned Canon = Extra_TruthCanonNPN2( Truth, 5, vRes );
+
+    Extra_PrintHex( stdout, (unsigned*)&Truth, 5 );  printf( "\n" );
+    Extra_PrintHex( stdout, (unsigned*)&Canon, 5 );  printf( "\n" );
+
+    printf( "Members = %d.\n", Vec_IntSize(vRes) );
+    Vec_IntForEachEntry( vRes, Entry, i )
+    {
+        Extra_PrintHex( stdout, (unsigned*)&Entry, 5 );  
+        printf( ", " );
+        if ( i % 8 == 7 )
+            printf( "\n" );
+    }
+
+    Vec_IntFree( vRes );
+}
+
+void Acec_MultFuncTest4()
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( 1000 );
+    int i, Entry;
+
+    unsigned Truth = 0x35C0;
+    //unsigned Truth = 0xD728;
+    unsigned Canon = Extra_TruthCanonNPN2( Truth, 4, vRes );
+
+    Extra_PrintHex( stdout, (unsigned*)&Truth, 4 );  printf( "\n" );
+    Extra_PrintHex( stdout, (unsigned*)&Canon, 4 );  printf( "\n" );
+
+    printf( "Members = %d.\n", Vec_IntSize(vRes) );
+    Vec_IntForEachEntry( vRes, Entry, i )
+    {
+        Extra_PrintHex( stdout, (unsigned*)&Entry, 4 );  
+        printf( ", " );
+        if ( i % 12 == 11 )
+            printf( "\n" );
+    }
+
+    Vec_IntFree( vRes );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acec_MultCollectInputs( Vec_Int_t * vPairs, Vec_Int_t * vRanks, int iObj )
+{
+    Vec_Int_t * vItems = Vec_IntAlloc( 100 );
+    int k, iObj1, iObj2;
+    // collect all those appearing with this one
+    Vec_IntForEachEntryDouble( vPairs, iObj1, iObj2, k )
+        if ( iObj == iObj1 )
+            Vec_IntPushUnique( vItems, iObj2 );
+        else if ( iObj == iObj2 )
+            Vec_IntPushUnique( vItems, iObj1 );
+    // sort items by rank cost
+    Vec_IntSelectSortCost( Vec_IntArray(vItems), Vec_IntSize(vItems), vRanks );
+    return vItems;
+}
+Vec_Int_t * Acec_MultDetectInputs1( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits )
+{
+    Vec_Int_t * vInputs = Vec_IntAlloc( 100 );
+    Vec_Int_t * vCounts = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vRanks  = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vPairs  = Vec_IntAlloc( 100 );
+    Vec_Int_t * vItems  = Vec_IntAlloc( 100 );
+    Vec_Int_t * vItems0;
+    Vec_Int_t * vItems1;
+    Vec_Int_t * vLevel;
+    int i, k, iLit, iObj, Count;
+    // count how many times each input appears
+    Vec_WecForEachLevel( vLeafLits, vLevel, i )
+        Vec_IntForEachEntry( vLevel, iLit, k )
+        {
+            iObj = Abc_Lit2Var(iLit);
+            Vec_IntAddToEntry( vCounts, Gia_ObjFaninId0(Gia_ManObj(p, iObj), iObj), 1 );
+            Vec_IntAddToEntry( vCounts, Gia_ObjFaninId1(Gia_ManObj(p, iObj), iObj), 1 );
+/*
+            printf( "Rank %2d : Leaf = %4d : (%2d, %2d)\n", i, iObj, 
+                Gia_ObjFaninId0(Gia_ManObj(p, iObj), iObj), Gia_ObjFaninId1(Gia_ManObj(p, iObj), iObj) );
+            if ( k == Vec_IntSize(vLevel) - 1 )
+                printf( "\n" );
+*/
+        }
+    // count ranks for each one
+    Vec_WecForEachLevel( vLeafLits, vLevel, i )
+        Vec_IntForEachEntry( vLevel, iLit, k )
+        {
+            iObj = Abc_Lit2Var(iLit);
+            if ( Vec_IntEntry(vCounts, Gia_ObjFaninId0(Gia_ManObj(p, iObj), iObj)) < 2 )
+            {
+                printf( "Skipping %d.\n", iObj );
+                continue;
+            }
+            if ( Vec_IntEntry(vCounts, Gia_ObjFaninId1(Gia_ManObj(p, iObj), iObj)) < 2 )
+            {
+                printf( "Skipping %d.\n", iObj );
+                continue;
+            }
+            Vec_IntAddToEntry( vRanks, Gia_ObjFaninId0(Gia_ManObj(p, iObj), iObj), i );
+            Vec_IntAddToEntry( vRanks, Gia_ObjFaninId1(Gia_ManObj(p, iObj), iObj), i );
+
+            Vec_IntPushTwo( vPairs, Gia_ObjFaninId0(Gia_ManObj(p, iObj), iObj), Gia_ObjFaninId1(Gia_ManObj(p, iObj), iObj) );
+        }
+
+    // print statistics
+    Vec_IntForEachEntry( vCounts, Count, i )
+    {
+        if ( !Count )
+            continue;
+        if ( !Vec_IntEntry(vRanks, i) )
+            continue;
+        Vec_IntPush( vItems, i );
+        printf( "Obj = %3d  Occurs = %3d  Ranks = %3d\n", i, Count, Vec_IntEntry(vRanks, i) );
+    }
+    // sort items by rank cost
+    Vec_IntSelectSortCost( Vec_IntArray(vItems), Vec_IntSize(vItems), vRanks );
+    // collect all those appearing with the last one
+    vItems0 = Acec_MultCollectInputs( vPairs, vRanks, Vec_IntEntryLast(vItems) );
+    Vec_IntAppend( vInputs, vItems0 );
+    // collect all those appearing with the last one
+    vItems1 = Acec_MultCollectInputs( vPairs, vRanks, Vec_IntEntryLast(vItems0) );
+    Vec_IntAppend( vInputs, vItems1 );
+
+    Vec_IntPrint( vItems0 );
+    Vec_IntPrint( vItems1 );
+
+    Vec_IntFree( vCounts );
+    Vec_IntFree( vRanks );
+    Vec_IntFree( vPairs );
+    Vec_IntFree( vItems );
+    Vec_IntFree( vItems0 );
+    Vec_IntFree( vItems1 );
+    return vInputs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits )
+{
+    Vec_Int_t * vInputs = Vec_IntAlloc( 100 );
+    Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+    Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vRanks  = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vCounts = Vec_IntStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vLevel;
+    int i, k, iLit, iObj, j, Entry;
+
+    ABC_FREE( p->pRefs );
+    Gia_ManCreateRefs( p );
+    Gia_ManForEachCiId( p, iObj, i )
+        printf( "%d=%d ", iObj, Gia_ObjRefNumId(p, iObj) );
+    printf( "\n" );
+    Gia_ManForEachAndId( p, iObj )
+        if ( Gia_ObjRefNumId(p, iObj) >= 4 )
+            printf( "%d=%d ", iObj, Gia_ObjRefNumId(p, iObj) );
+    printf( "\n" );
+
+    Vec_WecForEachLevel( vLeafLits, vLevel, i )
+        Vec_IntForEachEntry( vLevel, iLit, k )
+        {
+            word Truth = Gia_ObjComputeTruth6Cis( p, iLit, vSupp, vTemp );
+            if ( Vec_IntSize(vSupp) >= 0 )
+            {
+                printf( "Leaf = %4d : ", Abc_Lit2Var(iLit) );
+                printf( "Rank = %2d  ", i );
+                printf( "Supp = %2d  ", Vec_IntSize(vSupp) );
+                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 ( 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 )
+            {
+                Vec_IntAddToEntry( vRanks, Entry, i );
+                Vec_IntAddToEntry( vCounts, Entry, 1 );
+            }
+            if ( k == Vec_IntSize(vLevel)-1 )
+                printf( "\n" );
+        }
+
+    Vec_IntForEachEntry( vCounts, Entry, j )
+        if ( Entry )
+            printf( "%d=%d(%.2f) ", j, Entry, 1.0*Vec_IntEntry(vRanks, j)/Entry );
+    printf( "\n" );
+
+    Vec_IntFree( vSupp );
+    Vec_WrdFree( vTemp );
+    Vec_IntFree( vRanks );
+    Vec_IntFree( vCounts );
+    return vInputs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Mark nodes whose function is exactly that of a Booth PP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Bit_t * Acec_MultMarkPPs( 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_Bit_t * vRes = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+    int i, iObj, nProds = 0;
+    Gia_ManCleanMark0(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 && Saved[i]; i++ )
+        {
+            if ( Truth == Saved[i] || Truth == ~Saved[i] )
+            {
+                Vec_BitWriteEntry( vRes, iObj, 1 );
+                nProds++;
+                break;
+            }
+        }
+    }
+    Gia_ManCleanMark0(p);
+    printf( "Collected %d pps.\n", nProds );
+    Vec_IntFree( vSupp );
+    Vec_WrdFree( vTemp );
+    return vRes;
+}
+
+/**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 );
+        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 && Saved[i]; i++ )
+        {
+            if ( Truth == Saved[i] || Truth == ~Saved[i] )
+            {
+                //printf( "*** Node %d is PP with support %d.\n", iObj, Vec_IntSize(vSupp) );
+                Acec_MultFindPPs_rec( p, iObj, vBold );
+                nProds++;
+                break;
+            }
+        }
+        /*
+        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) );
+
+    Vec_IntFree( vSupp );
+    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 );
+    Gia_ManShow( p, vBold, 1, 0, 0 );
+    Vec_IntFree( vBold );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecNorm.c b/src/proof/acec/acecNorm.c
new file mode 100644
index 00000000..f2acb37b
--- /dev/null
+++ b/src/proof/acec/acecNorm.c
@@ -0,0 +1,226 @@
+/**CFile****************************************************************
+
+  FileName    [acecNorm.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [CEC for arithmetic circuits.]
+
+  Synopsis    [Adder tree normalization.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: acecNorm.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_InsertHadd( Gia_Man_t * pNew, int In[2], int Out[2] )
+{
+    int And, Or;
+    Out[1] = Gia_ManAppendAnd2( pNew, In[0], In[1] );
+    And    = Gia_ManAppendAnd2( pNew, Abc_LitNot(In[0]), Abc_LitNot(In[1]) );
+    Or     = Gia_ManAppendOr2( pNew, Out[1], And );
+    Out[0] = Abc_LitNot( Or );
+}
+void Acec_InsertFadd( Gia_Man_t * pNew, int In[3], int Out[2] )
+{
+    int In2[2], Out1[2], Out2[2];
+    Acec_InsertHadd( pNew, In, Out1 );
+    In2[0] = Out1[0];
+    In2[1] = In[2];
+    Acec_InsertHadd( pNew, In2, Out2 );
+    Out[0] = Out2[0];
+    Out[1] = Gia_ManAppendOr2( pNew, Out1[1], Out2[1] );
+}
+Vec_Int_t * Acec_InsertTree( Gia_Man_t * pNew, Vec_Wec_t * vLeafMap )
+{
+    Vec_Int_t * vRootRanks = Vec_IntAlloc( Vec_WecSize(vLeafMap) + 5 );
+    Vec_Int_t * vLevel;
+    int i, In[3], Out[2];
+    Vec_WecForEachLevel( vLeafMap, vLevel, i )
+    {
+        if ( Vec_IntSize(vLevel) == 0 )
+        {
+            Vec_IntPush( vRootRanks, 0 );
+            continue;
+        }
+        while ( Vec_IntSize(vLevel) > 1 )
+        {
+            if ( Vec_IntSize(vLevel) == 2 )
+                Vec_IntPush( vLevel, 0 );
+            //In[2] = Vec_IntPop( vLevel );
+            //In[1] = Vec_IntPop( vLevel );
+            //In[0] = Vec_IntPop( vLevel );
+
+            In[0] = Vec_IntEntry( vLevel, 0 );
+            Vec_IntDrop( vLevel, 0 );
+
+            In[1] = Vec_IntEntry( vLevel, 0 );
+            Vec_IntDrop( vLevel, 0 );
+
+            In[2] = Vec_IntEntry( vLevel, 0 );
+            Vec_IntDrop( vLevel, 0 );
+
+            Acec_InsertFadd( pNew, In, Out );
+            Vec_IntPush( vLevel, Out[0] );
+            if ( i+1 < Vec_WecSize(vLeafMap) )
+                vLevel = Vec_WecEntry(vLeafMap, i+1);
+            else
+                vLevel = Vec_WecPushLevel(vLeafMap);
+            Vec_IntPush( vLevel, Out[1] );
+            vLevel = Vec_WecEntry(vLeafMap, i);
+        }
+        assert( Vec_IntSize(vLevel) == 1 );
+        Vec_IntPush( vRootRanks, Vec_IntEntry(vLevel, 0) );
+    }
+    return vRootRanks;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acec_InsertBox_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return pObj->Value;
+    assert( Gia_ObjIsAnd(pObj) );
+    Acec_InsertBox_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Acec_InsertBox_rec( pNew, p, Gia_ObjFanin1(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, Vec_Int_t * vRootLits )
+{
+    Vec_Wec_t * vLeafMap = Vec_WecStart( Vec_WecSize(vLeafLits) );
+    Vec_Int_t * vLevel, * vRootRanks;  
+    int i, k, iLit, iLitNew;
+    // add roo literals
+    if ( vRootLits )
+        Vec_IntForEachEntry( vRootLits, iLit, i )
+        {
+            if ( i < Vec_WecSize(vLeafMap) )
+                vLevel = Vec_WecEntry(vLeafMap, i);
+            else
+                vLevel = Vec_WecPushLevel(vLeafMap);
+            Vec_IntPush( vLevel, iLit );
+        }
+    // add other literals
+    Vec_WecForEachLevel( vLeafLits, vLevel, i )
+        Vec_IntForEachEntry( vLevel, iLit, k )
+        {
+            Gia_Obj_t * pObj = Gia_ManObj( p, Abc_Lit2Var(iLit) );
+            iLitNew = Acec_InsertBox_rec( pNew, p, pObj );
+            iLitNew = Abc_LitNotCond( iLitNew, Abc_LitIsCompl(iLit) );
+            Vec_WecPush( vLeafMap, i, iLitNew );
+        }
+    // construct map of root literals
+    vRootRanks = Acec_InsertTree( pNew, vLeafMap );
+    Vec_WecFree( vLeafMap );
+    return vRootRanks;
+}
+Gia_Man_t * Acec_InsertBox( Acec_Box_t * pBox, int fAll )
+{
+    Gia_Man_t * p = pBox->pGia;
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vRootRanks, * vLevel, * vTemp;
+    int i, k, iLit, iLitNew;
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManFillValue(p);
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    // implement tree
+    if ( fAll )
+        vRootRanks = Acec_BuildTree( pNew, p, pBox->vLeafLits, NULL );
+    else
+    {
+        assert( pBox->vShared != NULL );
+        assert( pBox->vUnique != NULL );
+        vRootRanks = Acec_BuildTree( pNew, p, pBox->vShared, NULL );
+        vRootRanks = Acec_BuildTree( pNew, p, pBox->vUnique, vTemp = vRootRanks );
+        Vec_IntFree( vTemp );
+    }
+    // update polarity of literals
+    Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
+        Vec_IntForEachEntry( vLevel, iLit, k )
+        {
+            pObj = Gia_ManObj( p, Abc_Lit2Var(iLit) );
+            iLitNew = k ? 0 : Vec_IntEntry( vRootRanks, i );
+            pObj->Value = Abc_LitNotCond( iLitNew, Abc_LitIsCompl(iLit) );
+        }
+    Vec_IntFree( vRootRanks );
+    // construct the outputs
+    Gia_ManForEachCo( p, pObj, i )
+        Acec_InsertBox_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Acec_Normalize( Gia_Man_t * pGia, int fBooth, int fVerbose )
+{
+    Vec_Bit_t * vIgnore = fBooth ? Acec_BoothFindPPG( pGia ) : NULL;
+    Acec_Box_t * pBox = Acec_DeriveBox( pGia, vIgnore, 0, 0, fVerbose );
+    Gia_Man_t * pNew  = Acec_InsertBox( pBox, 1 );
+    Acec_BoxFreeP( &pBox );
+    Vec_BitFreeP( &vIgnore );
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecPa.c b/src/proof/acec/acecPa.c
index ecaf2047..6b382d91 100644
--- a/src/proof/acec/acecPa.c
+++ b/src/proof/acec/acecPa.c
@@ -248,11 +248,6 @@ int Pas_ManComputeCuts( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vOrder, Ve
 ***********************************************************************/
 void Pas_ManComputeCutsTest( Gia_Man_t * p )
 {
-    extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
-    extern Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts );
-
-    extern int Ree_ManCountFadds( Vec_Int_t * vAdds );
-    extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
     abctime clk = Abc_Clock();
     Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, 1 );
     Vec_Int_t * vIns, * vOuts;
diff --git a/src/proof/acec/acecPool.c b/src/proof/acec/acecPool.c
index 08ee37f2..0868545e 100644
--- a/src/proof/acec/acecPool.c
+++ b/src/proof/acec/acecPool.c
@@ -303,17 +303,9 @@ void Acec_ManPrintRanks( Vec_Int_t * vPairs )
 ***********************************************************************/
 void Acec_ManProfile( Gia_Man_t * p, int fVerbose )
 {
-    extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
-    extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds );
-    extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds );
-    extern int Ree_ManCountFadds( Vec_Int_t * vAdds );
-    extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
-
     abctime clk = Abc_Clock();
     Vec_Wec_t * vBoxes; int i;
     Vec_Int_t * vXors, * vAdds = Ree_ManComputeCuts( p, &vXors, fVerbose );
-    Ree_ManRemoveTrivial( p, vAdds );
-    Ree_ManRemoveContained( p, vAdds );
 
     //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 );
@@ -396,13 +388,6 @@ Vec_Int_t * Acec_ManPoolTopMost( Gia_Man_t * p, Vec_Int_t * vAdds )
 }
 void Acec_ManPool( Gia_Man_t * p )
 {
-    extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
-    extern Vec_Wec_t * Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes );
-
-    extern int Ree_ManCountFadds( Vec_Int_t * vAdds );
-    extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose );
-    extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds );
-    extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds );
     Vec_Int_t * vTops, * vTree;
     Vec_Wec_t * vTrees;
 
@@ -413,8 +398,6 @@ void Acec_ManPool( Gia_Man_t * p )
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
     clk = Abc_Clock();
-    Ree_ManRemoveTrivial( p, vAdds );
-    Ree_ManRemoveContained( p, vAdds );
     nFadds = Ree_ManCountFadds( vAdds );
     printf( "Detected %d FAs and %d HAs.  ", nFadds, Vec_IntSize(vAdds)/6-nFadds );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
diff --git a/src/proof/acec/acecRe.c b/src/proof/acec/acecRe.c
index 26faad00..5e5ca688 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;
@@ -370,7 +377,7 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData, int fVerbos
         Vec_IntForEachEntryDouble( vXorOne, iObj, Truth, j )
         Vec_IntForEachEntryDouble( vMajOne, iObj2, Truth2, k )
         {
-            int SignAnd[8] = {0x88, 0x44, 0x22, 0x11, 0xEE, 0xDD, 0xBB, 0x77};
+            int SignAnd[8] = {0x88, 0x44, 0x22, 0x11, 0x77, 0xBB, 0xDD, 0xEE};
             int SignMaj[8] = {0xE8, 0xD4, 0xB2, 0x71, 0x8E, 0x4D, 0x2B, 0x17};
             int n, SignXor = (Truth == 0x99 || Truth == 0x69) << 3;
             for ( n = 0; n < 8; n++ )
@@ -390,8 +397,18 @@ Vec_Int_t * Ree_ManDeriveAdds( Hash_IntMan_t * p, Vec_Int_t * vData, int fVerbos
     Vec_WecFree( vMajMap );
     return vAdds;
 }
+int Ree_ManCompare( int * pCut0, int * pCut1 )
+{
+    if ( pCut0[3] < pCut1[3] ) return -1;
+    if ( pCut0[3] > pCut1[3] ) return  1;
+    if ( pCut0[4] < pCut1[4] ) return -1;
+    if ( pCut0[4] > pCut1[4] ) return  1;
+    return 0;
+}
 Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose )
 {
+    extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds );
+    extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds );
     Gia_Obj_t * pObj; 
     int * pList0, * pList1, i, nCuts = 0;
     Hash_IntMan_t * pHash = Hash_IntManStart( 1000 );
@@ -425,11 +442,15 @@ Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose
     Vec_IntFree( vTemp );
     Vec_IntFree( vCuts );
     vAdds = Ree_ManDeriveAdds( pHash, vData, fVerbose );
+    qsort( Vec_IntArray(vAdds), Vec_IntSize(vAdds)/6, 24, (int (*)(const void *, const void *))Ree_ManCompare );
     if ( fVerbose )
         printf( "Adders = %d.  Total cuts = %d.  Hashed cuts = %d.  Hashed/Adders = %.2f.\n", 
             Vec_IntSize(vAdds)/6, Vec_IntSize(vData)/3, Hash_IntManEntryNum(pHash), 6.0*Hash_IntManEntryNum(pHash)/Vec_IntSize(vAdds) );
     Vec_IntFree( vData );
     Hash_IntManStop( pHash );
+    Ree_ManRemoveTrivial( p, vAdds );
+    Ree_ManRemoveContained( p, vAdds );
+    //Ree_ManPrintAdders( vAdds, 1 );
     return vAdds;
 }
 
@@ -503,6 +524,10 @@ void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds )
         {
             pObjX = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+3) );
             pObjM = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*i+4) );
+            // rule out if MAJ is a fanout of XOR
+            //if ( pObjX == Gia_ObjFanin0(pObjM) || pObjX == Gia_ObjFanin1(pObjM) )
+            //    continue;
+            // rule out if MAJ is a fanin of XOR and has no other fanouts
             if ( (pObjM == Gia_ObjFanin0(pObjX) || pObjM == Gia_ObjFanin1(pObjX)) && Gia_ObjRefNum(p, pObjM) == 1 )
                 continue;
         }
diff --git a/src/proof/acec/acecSt.c b/src/proof/acec/acecSt.c
index 63aa8131..d97dadc9 100644
--- a/src/proof/acec/acecSt.c
+++ b/src/proof/acec/acecSt.c
@@ -21,6 +21,8 @@
 #include "acecInt.h"
 #include "misc/vec/vecWec.h"
 #include "misc/extra/extra.h"
+#include "aig/aig/aig.h"
+#include "opt/dar/dar.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/proof/acec/acecStruct.c b/src/proof/acec/acecStruct.c
new file mode 100644
index 00000000..6702e13b
--- /dev/null
+++ b/src/proof/acec/acecStruct.c
@@ -0,0 +1,271 @@
+/**CFile****************************************************************
+
+  FileName    [acecStruct.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [CEC for arithmetic circuits.]
+
+  Synopsis    [Core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: acecStruct.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/vec/vecWec.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acec_StructDetectXorRoots( Gia_Man_t * p )
+{
+    Vec_Int_t * vXors = Vec_IntAlloc( 100 );
+    Vec_Bit_t * vXorIns = Vec_BitStart( Gia_ManObjNum(p) );
+    Gia_Obj_t * pFan0, * pFan1, * pObj; 
+    int i, k = 0, Entry;
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+            continue;
+        Vec_IntPush( vXors, i );
+        Vec_BitWriteEntry( vXorIns, Gia_ObjId(p, Gia_Regular(pFan0)), 1 );
+        Vec_BitWriteEntry( vXorIns, Gia_ObjId(p, Gia_Regular(pFan1)), 1 );
+    }
+    // collect XORs that not inputs of other XORs
+    Vec_IntForEachEntry( vXors, Entry, i )
+        if ( !Vec_BitEntry(vXorIns, Entry) )
+            Vec_IntWriteEntry( vXors, k++, Entry );
+    Vec_IntShrink( vXors, k );
+    Vec_BitFree( vXorIns );
+    return vXors;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acec_StructAssignRanks( Gia_Man_t * p, Vec_Int_t * vXorRoots )
+{
+    Vec_Int_t * vDoubles = Vec_IntAlloc( 100 );
+    Gia_Obj_t * pFan0, * pFan1, * pObj; 
+    int i, k, Fanins[2], Entry, Rank;
+    // map roots into their ranks
+    Vec_Int_t * vRanks = Vec_IntStartFull( Gia_ManObjNum(p) ); 
+    Vec_IntForEachEntry( vXorRoots, Entry, i )
+        Vec_IntWriteEntry( vRanks, Entry, i );
+    // map nodes into their ranks
+    Gia_ManForEachAndReverse( p, pObj, i )
+    {
+        if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+            continue;
+        Rank = Vec_IntEntry( vRanks, i );
+        // skip XORs that are not part of any tree
+        if ( Rank == -1 )
+            continue;
+        // iterate through XOR inputs
+        Fanins[0] = Gia_ObjId(p, Gia_Regular(pFan0));
+        Fanins[1] = Gia_ObjId(p, Gia_Regular(pFan1));
+        for ( k = 0; k < 2; k++ )
+        {
+            Entry = Vec_IntEntry( vRanks, Fanins[k] );
+            if ( Entry == Rank ) // the same tree -- allow fanout in this tree
+                continue;
+            if ( Entry == -1 )
+                Vec_IntWriteEntry( vRanks, Fanins[k], Rank );
+            else
+                Vec_IntPush( vDoubles, Fanins[k] );
+            if ( Entry != -1 && Gia_ObjIsAnd(Gia_ManObj(p, Fanins[k])))
+            printf( "Xor node %d belongs to Tree %d and Tree %d.\n", Fanins[k], Entry, Rank );
+        }
+    }
+    // remove duplicated entries
+    Vec_IntForEachEntry( vDoubles, Entry, i )
+        Vec_IntWriteEntry( vRanks, Entry, -1 );
+    Vec_IntFree( vDoubles );
+    return vRanks;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Acec_FindTreeLeaves( Gia_Man_t * p, Vec_Int_t * vXorRoots, Vec_Int_t * vRanks )
+{
+    Vec_Bit_t * vMapXors = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Wec_t * vTreeLeaves = Vec_WecStart( Vec_IntSize(vXorRoots) );
+    Gia_Obj_t * pFan0, * pFan1, * pObj; 
+    int i, k, Fanins[2], Rank;
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+            continue;
+        Vec_BitWriteEntry( vMapXors, i, 1 );
+        Rank = Vec_IntEntry( vRanks, i );
+        // skip XORs that are not part of any tree
+        if ( Rank == -1 )
+            continue;
+        // iterate through XOR inputs
+        Fanins[0] = Gia_ObjId(p, Gia_Regular(pFan0));
+        Fanins[1] = Gia_ObjId(p, Gia_Regular(pFan1));
+        for ( k = 0; k < 2; k++ )
+        {
+            if ( Vec_BitEntry(vMapXors, Fanins[k]) )
+            {
+                assert( Rank == Vec_IntEntry(vRanks, Fanins[k]) );
+                continue;
+            }
+            Vec_WecPush( vTreeLeaves, Rank, Fanins[k] );
+        }
+    }
+    Vec_BitFree( vMapXors );
+    return vTreeLeaves;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acec_FindShadows( Gia_Man_t * p, Vec_Int_t * vRanks )
+{
+    Vec_Int_t * vShadows = Vec_IntDup( vRanks );
+    Gia_Obj_t * pObj; int i, Shad0, Shad1;
+    Gia_ManForEachCi( p, pObj, i )
+        Vec_IntWriteEntry( vShadows, Gia_ObjId(p, pObj), -1 );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( Vec_IntEntry(vShadows, i) >= 0 )
+            continue;
+        Shad0 = Vec_IntEntry(vShadows, Gia_ObjFaninId0(pObj, i));
+        Shad1 = Vec_IntEntry(vShadows, Gia_ObjFaninId1(pObj, i));
+        if ( Shad0 == Shad1 && Shad0 != -1 )
+            Vec_IntWriteEntry(vShadows, i, Shad0);
+    }
+    return vShadows;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acec_CollectSupp_rec( Gia_Man_t * p, int iNode, int Rank, Vec_Int_t * vRanks )
+{
+    Gia_Obj_t * pObj;
+    int nSize;
+    if ( Gia_ObjIsTravIdCurrentId(p, iNode) )
+        return 0;
+    Gia_ObjSetTravIdCurrentId(p, iNode);
+    pObj = Gia_ManObj(p, iNode);
+    assert( Gia_ObjIsAnd(pObj) );
+    if ( Vec_IntEntry(vRanks, iNode) == Rank )
+        return 1;
+    nSize = Acec_CollectSupp_rec( p, Gia_ObjFaninId0(pObj, iNode), Rank, vRanks );
+    nSize += Acec_CollectSupp_rec( p, Gia_ObjFaninId1(pObj, iNode), Rank, vRanks );
+    return nSize;
+}
+Vec_Wec_t * Acec_FindNexts( Gia_Man_t * p, Vec_Int_t * vRanks, Vec_Int_t * vShadows, Vec_Wec_t * vTreeLeaves )
+{
+    Vec_Wec_t * vNexts = Vec_WecStart( Vec_WecSize(vTreeLeaves) );
+    Vec_Int_t * vTree;
+    int i, k, Node, Fanins[2], Shad0, Shad1, Rank, nSupp;
+    Vec_WecForEachLevel( vTreeLeaves, vTree, i )
+        Vec_IntForEachEntry( vTree, Node, k )
+        {
+            Gia_Obj_t * pObj = Gia_ManObj(p, Node);
+            if ( !Gia_ObjIsAnd(pObj) )
+                continue;
+            Fanins[0] = Gia_ObjFaninId0(pObj, Node);
+            Fanins[1] = Gia_ObjFaninId1(pObj, Node);
+            Shad0 = Vec_IntEntry(vShadows, Fanins[0]);
+            Shad1 = Vec_IntEntry(vShadows, Fanins[1]);
+            if ( Shad0 != Shad1 || Shad0 == -1 )
+                continue;
+            // check support size of Node in terms of the shadow of its fanins
+            Rank = Vec_IntEntry( vRanks, Node );
+            assert( Rank != Shad0 );
+            Gia_ManIncrementTravId( p );
+            nSupp = Acec_CollectSupp_rec( p, Node, Shad0, vRanks );
+            assert( nSupp > 1 );
+            if ( nSupp > 3 )
+                continue;
+            Vec_IntPushUniqueOrder( Vec_WecEntry(vNexts, Shad0), Rank );
+        }
+    return vNexts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_StructTest( Gia_Man_t * p )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c
new file mode 100644
index 00000000..ab17d7b9
--- /dev/null
+++ b/src/proof/acec/acecTree.c
@@ -0,0 +1,783 @@
+/**CFile****************************************************************
+
+  FileName    [acecTree.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [CEC for arithmetic circuits.]
+
+  Synopsis    [Adder tree construction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: acecTree.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_BoxFree( Acec_Box_t * pBox )
+{
+    Vec_WecFreeP( &pBox->vAdds );
+    Vec_WecFreeP( &pBox->vLeafLits );
+    Vec_WecFreeP( &pBox->vRootLits );
+    Vec_WecFreeP( &pBox->vUnique );
+    Vec_WecFreeP( &pBox->vShared );
+    ABC_FREE( pBox );
+}
+void Acec_BoxFreeP( Acec_Box_t ** ppBox )
+{
+    if ( *ppBox )
+        Acec_BoxFree( *ppBox );
+    *ppBox = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_VerifyBoxLeaves( Acec_Box_t * pBox, Vec_Bit_t * vIgnore )
+{
+    Vec_Int_t * vLevel;
+    int i, k, iLit, Count = 0;
+    if ( vIgnore == NULL )
+        return;
+    Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
+        Vec_IntForEachEntry( vLevel, iLit, k )
+            if ( Gia_ObjIsAnd(Gia_ManObj(pBox->pGia, Abc_Lit2Var(iLit))) && !Vec_BitEntry(vIgnore, Abc_Lit2Var(iLit)) )
+                printf( "Internal node %d of rank %d is not part of PPG.\n", Abc_Lit2Var(iLit), i ), Count++;
+    printf( "Detected %d suspicious leaves.\n", Count );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Filters trees by removing TFO of roots.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_TreeFilterOne( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
+{
+    Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Bit_t * vMarked = Vec_BitStart( Gia_ManObjNum(p) ) ;
+    Gia_Obj_t * pObj;
+    int i, k = 0, Box, Rank;
+    // mark roots
+    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+    {
+        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_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+0), 0 );
+        Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+1), 0 );
+        Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+2), 0 );
+    }
+    // iterate through nodes to detect TFO of roots
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( Vec_BitEntry(vIsRoot, Gia_ObjFaninId0(pObj,i)) || Vec_BitEntry(vIsRoot, Gia_ObjFaninId1(pObj,i)) ||
+             Vec_BitEntry(vMarked, Gia_ObjFaninId0(pObj,i)) || Vec_BitEntry(vMarked, Gia_ObjFaninId1(pObj,i)) )
+            Vec_BitWriteEntry( vMarked, i, 1 );
+    }
+    // remove those that overlap with roots
+    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+    {
+        // special case of the first bit
+//        if ( i == 0 )
+//            continue;
+
+/*
+        if ( Vec_IntEntry(vAdds, 6*Box+3) == 24 && Vec_IntEntry(vAdds, 6*Box+4) == 22 )
+        {
+            printf( "**** removing special one \n" );
+            continue;
+        }
+        if ( Vec_IntEntry(vAdds, 6*Box+3) == 48 && Vec_IntEntry(vAdds, 6*Box+4) == 49 )
+        {
+            printf( "**** removing special one \n" );
+            continue;
+        }
+*/
+        if ( Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+3)) || Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+4)) )
+        {
+            printf( "Removing box %d=(%d,%d) of rank %d.\n", Box, Vec_IntEntry(vAdds, 6*Box+3), Vec_IntEntry(vAdds, 6*Box+4), Rank ); 
+            continue;
+        }
+        Vec_IntWriteEntry( vTree, k++, Box );
+        Vec_IntWriteEntry( vTree, k++, Rank );
+    }
+    Vec_IntShrink( vTree, k );
+    Vec_BitFree( vIsRoot );
+    Vec_BitFree( vMarked );
+}
+void Acec_TreeFilterTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vTrees )
+{
+    Vec_Int_t * vLevel;
+    int i;
+    Vec_WecForEachLevel( vTrees, vLevel, i )
+        Acec_TreeFilterOne( p, vAdds, vLevel );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Filters trees by removing TFO of roots.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_TreeMarkTFI_rec( Gia_Man_t * p, int Id, Vec_Bit_t * vMarked )
+{
+    Gia_Obj_t * pObj = Gia_ManObj(p, Id);
+    if ( Vec_BitEntry(vMarked, Id) )
+        return;
+    Vec_BitWriteEntry( vMarked, Id, 1 );
+    if ( !Gia_ObjIsAnd(pObj) )
+        return;
+    Acec_TreeMarkTFI_rec( p, Gia_ObjFaninId0(pObj, Id), vMarked );
+    Acec_TreeMarkTFI_rec( p, Gia_ObjFaninId1(pObj, Id), vMarked );
+}
+void Acec_TreeFilterOne2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
+{
+    Vec_Bit_t * vIsLeaf = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Bit_t * vMarked = Vec_BitStart( Gia_ManObjNum(p) ) ;
+    Gia_Obj_t * pObj;
+    int i, k = 0, Box, Rank;
+    // mark leaves
+    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_IntForEachEntryDouble( vTree, Box, Rank, i )
+    {
+        Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+3), 0 );
+        Vec_BitWriteEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4), 0 );
+    }
+    // mark TFI of leaves
+    Gia_ManForEachAnd( p, pObj, i )
+        if ( Vec_BitEntry(vIsLeaf, i) )
+            Acec_TreeMarkTFI_rec( p, i, vMarked );
+    // additional one
+//if ( 10942 < Gia_ManObjNum(p) )
+//    Acec_TreeMarkTFI_rec( p, 10942, vMarked );
+    // remove those that overlap with the marked TFI
+    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+    {
+        if ( Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+3)) || Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+4)) )
+        {
+            printf( "Removing box %d=(%d,%d) of rank %d.\n", Box, Vec_IntEntry(vAdds, 6*Box+3), Vec_IntEntry(vAdds, 6*Box+4), Rank ); 
+            continue;
+        }
+        Vec_IntWriteEntry( vTree, k++, Box );
+        Vec_IntWriteEntry( vTree, k++, Rank );
+    }
+    Vec_IntShrink( vTree, k );
+    Vec_BitFree( vIsLeaf );
+    Vec_BitFree( vMarked );
+}
+void Acec_TreeFilterTrees2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vTrees )
+{
+    Vec_Int_t * vLevel;
+    int i;
+    Vec_WecForEachLevel( vTrees, vLevel, i )
+        Acec_TreeFilterOne2( p, vAdds, vLevel );
+}
+
+/**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 fFlip = !fFadd && Acec_SignBit2(vAdds, iBox, 2);
+
+    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 = (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 = (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 = (Acec_SignBit2(vAdds, iBox, 4) ^ fFlip) ? 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
+    {
+        //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 )
+            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 );
+}
+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 );
+}
+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*************************************************************
+
+  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 * vVisit )
+{
+    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 );
+    fXorPhase = Acec_SignBit(vAdds, iBox, 3);
+    if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 )
+    {
+        //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 = Acec_SignBit(vAdds, iBox, k) ^ fPhase;
+        fXorPhase ^= fPhaseThis;
+        Acec_TreePhases_rec( p, vAdds, vMap, iObj, fPhaseThis, vVisit );
+        Acec_SignSetBit2( vAdds, iBox, k, fPhaseThis );
+    }
+    Acec_SignSetBit2( vAdds, iBox, 3, fXorPhase );
+    Acec_SignSetBit2( vAdds, iBox, 4, fPhase );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find internal cut points with exactly one adder fanin/fanout.]
+
+  Description [Returns a map of point into its input/output adder.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_TreeAddInOutPoint( Vec_Int_t * vMap, int iObj, int iAdd, int fOut )
+{
+    int * pPlace = Vec_IntEntryP( vMap, Abc_Var2Lit(iObj, fOut) );
+    if ( *pPlace == -1 )
+        *pPlace = iAdd;
+    else if ( *pPlace >= 0 )
+        *pPlace = -2;
+}
+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 );
+        Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+3), i, 1 );
+        Acec_TreeAddInOutPoint( vMap, Vec_IntEntry(vAdds, 6*i+4), i, 1 );
+    }
+    return vMap;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find adder trees as groups of adders connected vis cut-points.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acec_TreeWhichPoint( Vec_Int_t * vAdds, int iAdd, int iObj )
+{
+    int k;
+    for ( k = 0; k < 5; k++ )
+        if ( Vec_IntEntry(vAdds, 6*iAdd+k) == iObj )
+            return k;
+    assert( 0 );
+    return -1;
+}
+void Acec_TreeFindTrees2_rec( Vec_Int_t * vAdds, Vec_Int_t * vMap, int iAdd, int Rank, Vec_Int_t * vTree, Vec_Bit_t * vFound )
+{
+    extern void Acec_TreeFindTrees_rec( Vec_Int_t * vAdds, Vec_Int_t * vMap, int iObj, int Rank, Vec_Int_t * vTree, Vec_Bit_t * vFound );
+    int k;
+    if ( Vec_BitEntry(vFound, iAdd) )
+        return;
+    Vec_BitWriteEntry( vFound, iAdd, 1 );
+    Vec_IntPush( vTree, iAdd );
+    Vec_IntPush( vTree, Rank );
+    //printf( "Assigning rank %d to (%d:%d).\n", Rank, Vec_IntEntry(vAdds, 6*iAdd+3), Vec_IntEntry(vAdds, 6*iAdd+4) );
+    for ( k = 0; k < 5; k++ )
+        Acec_TreeFindTrees_rec( vAdds, vMap, Vec_IntEntry(vAdds, 6*iAdd+k), k == 4 ? Rank + 1 : Rank, vTree, vFound );
+}
+void Acec_TreeFindTrees_rec( Vec_Int_t * vAdds, Vec_Int_t * vMap, int iObj, int Rank, Vec_Int_t * vTree, Vec_Bit_t * vFound )
+{
+    int In  = Vec_IntEntry( vMap, Abc_Var2Lit(iObj, 1) );
+    int Out = Vec_IntEntry( vMap, Abc_Var2Lit(iObj, 0) );
+    if ( In < 0 || Out < 0 )
+        return;
+    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_Bit_t * vIgnore, int fFilterIn, int fFilterOut )
+{
+    Vec_Wec_t * vTrees = Vec_WecAlloc( 10 );
+    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;
+    // go through the cut-points
+    Vec_IntForEachEntryDouble( vMap, In, Out, i )
+    {
+        if ( In < 0 || Out < 0 )
+            continue;
+        assert( Vec_BitEntry(vFound, In) == Vec_BitEntry(vFound, Out) );
+        if ( Vec_BitEntry(vFound, In) )
+            continue;
+        vTree = Vec_WecPushLevel( vTrees );
+        Acec_TreeFindTrees_rec( vAdds, vMap, i/2, 0, vTree, vFound );
+        // normalize rank
+        MinRank = ABC_INFINITY;
+        Vec_IntForEachEntryDouble( vTree, Box, Rank, k )
+            MinRank = Abc_MinInt( MinRank, Rank );
+        Vec_IntForEachEntryDouble( vTree, Box, Rank, k )
+            Vec_IntWriteEntry( vTree, k+1, Rank - MinRank );
+    }
+    Vec_BitFree( vFound );
+    Vec_IntFree( vMap );
+    // filter trees
+    if ( fFilterIn )
+        Acec_TreeFilterTrees2( p, vAdds, vTrees );
+    else if ( fFilterOut )
+        Acec_TreeFilterTrees( p, vAdds, vTrees );
+    // sort by size
+    Vec_WecSort( vTrees, 1 );
+    return vTrees;
+}
+void Acec_TreeFindTreesTest( Gia_Man_t * p )
+{
+    Vec_Wec_t * vTrees;
+
+    abctime clk = Abc_Clock();
+    Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, 1 );
+    int nFadds = Ree_ManCountFadds( vAdds );
+    printf( "Detected %d adders (%d FAs and %d HAs).  ", Vec_IntSize(vAdds)/6, nFadds, Vec_IntSize(vAdds)/6-nFadds );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+    clk = Abc_Clock();
+    vTrees = Acec_TreeFindTrees( p, vAdds, NULL, 0, 0 );
+    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 );
+
+    Vec_WecFree( vTrees );
+    Vec_IntFree( vAdds );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives one adder tree.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+`
+***********************************************************************/
+void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds )
+{
+    Vec_Int_t * vLevel;
+    int i, k, iBox;
+    Vec_WecForEachLevel( vBoxes, vLevel, i )
+    {
+        printf( " %4d : %2d  {", i, Vec_IntSize(vLevel) );
+        Vec_IntForEachEntry( vLevel, iBox, k )
+        {
+            printf( " %s%d=(%d,%d)", Vec_IntEntry(vAdds, 6*iBox+2) == 0 ? "*":"", iBox, 
+                                     Vec_IntEntry(vAdds, 6*iBox+3), Vec_IntEntry(vAdds, 6*iBox+4) );
+            //printf( "(%d,%d,%d)", Vec_IntEntry(vAdds, 6*iBox+0), Vec_IntEntry(vAdds, 6*iBox+1), Vec_IntEntry(vAdds, 6*iBox+2) );
+        }
+        printf( " }\n" );
+    }
+}
+void Acec_TreePrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds )
+{
+    printf( "Adders:\n" );
+    Acec_PrintAdders( pBox->vAdds, vAdds );
+    printf( "Inputs:\n" );
+    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 )
+{
+    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 * 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, j, k, Box, Rank;//, Count = 0;
+
+    Acec_Box_t * pBox = ABC_CALLOC( Acec_Box_t, 1 );
+    pBox->pGia        = p;
+    pBox->vAdds       = Vec_WecStart( MaxRank + 1 );
+    pBox->vLeafLits   = Vec_WecStart( MaxRank + 1 );
+    pBox->vRootLits   = Vec_WecStart( MaxRank + 2 );
+
+    // collect boxes; mark inputs/outputs
+    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+    {
+//        if ( 37 == Box && 6 == Rank )
+//        {
+//            printf( "Skipping one adder...\n" );
+//            continue;
+//        }
+        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 starting from roots
+    vMap = Acec_TreeCarryMap( p, vAdds, pBox->vAdds );
+    Vec_WecForEachLevelReverse( pBox->vAdds, vLevel, i )
+        Vec_IntForEachEntry( vLevel, Box, k )
+            if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4) ) )
+            {
+                //printf( "Pushing phase of output %d of box %d\n", Vec_IntEntry(vAdds, 6*Box+4), Box );
+                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( 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) ) )
+                {
+                    //if ( Vec_IntEntry(vAdds, 6*Box+k) == 10942 )
+                    //{
+                    //    printf( "++++++++++++ Skipping special\n" );
+                    //    continue;
+                    //}
+                    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
+    Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
+        Vec_IntSort( vLevel, 0 );
+    Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
+        Vec_IntSort( vLevel, 1 );
+    //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 )
+{
+    Acec_Box_t * pBox;
+    Vec_Wec_t * vTrees;
+    Vec_Int_t * vTree;
+
+    abctime clk = Abc_Clock();
+    Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, 1 );
+    int i, nFadds = Ree_ManCountFadds( vAdds );
+    printf( "Detected %d adders (%d FAs and %d HAs).  ", Vec_IntSize(vAdds)/6, nFadds, Vec_IntSize(vAdds)/6-nFadds );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+    clk = Abc_Clock();
+    vTrees = Acec_TreeFindTrees( p, vAdds, NULL, 0, 0 );
+    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 );
+
+    Vec_WecForEachLevel( vTrees, vTree, i )
+    {
+        pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, i) );
+        printf( "Processing tree %d:  Ranks = %d.  Adders = %d.  Leaves = %d.  Roots = %d.\n", 
+            i, Vec_WecSize(pBox->vAdds), Vec_WecSizeSize(pBox->vAdds), 
+            Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits)  );
+        Acec_TreePrintBox( pBox, vAdds );
+        Acec_BoxFreeP( &pBox );
+    }
+
+    Vec_WecFree( vTrees );
+    Vec_IntFree( vAdds );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut, int fVerbose )
+{
+    Acec_Box_t * pBox = NULL;
+    Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, fVerbose );
+    Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds, vIgnore, fFilterIn, fFilterOut );
+    if ( vTrees && Vec_WecSize(vTrees) > 0 )
+    {
+        pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, 0) );
+        Acec_VerifyBoxLeaves( pBox, vIgnore );
+    }
+    if ( pBox )//&& fVerbose )
+        printf( "Processing tree %d:  Ranks = %d.  Adders = %d.  Leaves = %d.  Roots = %d.\n", 
+            0, Vec_WecSize(pBox->vAdds), Vec_WecSizeSize(pBox->vAdds), 
+            Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits)  );
+    if ( pBox && fVerbose )
+        Acec_TreePrintBox( pBox, vAdds );
+    //Acec_PrintAdders( pBox0->vAdds, vAdds );
+    //Acec_MultDetectInputs( p, pBox->vLeafLits, pBox->vRootLits );
+    Vec_WecFreeP( &vTrees );
+    Vec_IntFree( vAdds );
+    return pBox;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecUtil.c b/src/proof/acec/acecUtil.c
index 191856cf..be12afef 100644
--- a/src/proof/acec/acecUtil.c
+++ b/src/proof/acec/acecUtil.c
@@ -90,6 +90,29 @@ void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose )
     Vec_IntFree( vXors );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupTopMostRange( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Vec_Int_t * vTops = Vec_IntAlloc( 10 );
+    int i;
+    for ( i = 45; i < 52; i++ )
+        Vec_IntPush( vTops, Gia_ObjId( p, Gia_ObjFanin0(Gia_ManCo(p, i)) ) );
+    pNew = Gia_ManDupAndConesLimit( p, Vec_IntArray(vTops), Vec_IntSize(vTops), 100 );
+    Vec_IntFree( vTops );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/acec/acecXor.c b/src/proof/acec/acecXor.c
new file mode 100644
index 00000000..71e0b7b3
--- /dev/null
+++ b/src/proof/acec/acecXor.c
@@ -0,0 +1,434 @@
+/**CFile****************************************************************
+
+  FileName    [acecXor.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [CEC for arithmetic circuits.]
+
+  Synopsis    [Detection of XOR trees.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: acecXor.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/vec/vecWec.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_CheckXors( Gia_Man_t * p, Vec_Int_t * vXors )
+{
+    Gia_Obj_t * pFan0, * pFan1;
+    Vec_Int_t * vCount2 = Vec_IntAlloc( Gia_ManObjNum(p) );
+    int i, Entry, Count = 0;
+    for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
+        if ( Vec_IntEntry(vXors, 4*i+3) == 0 )
+            Vec_IntAddToEntry( vCount2, Vec_IntEntry(vXors, 4*i), 1 );
+    Vec_IntForEachEntry( vCount2, Entry, i )
+        if ( Entry > 1 )
+            printf( "*** Obj %d has %d two-input XOR cuts.\n", i, Entry ), Count++;
+        else if ( Entry == 1 && Gia_ObjRecognizeExor(Gia_ManObj(p, i), &pFan0, &pFan1) )
+            printf( "*** Obj %d cannot be recognized as XOR.\n", i );
+    if ( Count == 0 )
+        printf( "*** There no multiple two-input XOR cuts.\n" );
+    Vec_IntFree( vCount2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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_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(vRanks, Node) == -1 )
+            continue;
+        for ( k = 0; k < 3; k++ )
+        {
+            int Fanin = Vec_IntEntry(vAdds, 6*i+k);
+            if ( Vec_IntEntry(vRanks, Fanin) == -1 )
+                continue;
+            //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( vMove );
+    // find reodering
+    Vec_IntForEachEntry( vMove, Entry, i )
+        if ( Entry == -1 && Vec_IntFind(vMove, i) >= 0 )
+            break;
+    assert( i < Vec_IntSize(vMove) );
+    while ( 1 )
+    {
+        Vec_IntPush( vOrder, Vec_IntEntry(vXorRoots, i) );
+        Entry = i;
+        Vec_IntForEachEntry( vMove, This, i )
+            if ( This == Entry )
+                break;
+        if ( i == Vec_IntSize(vMove) )
+            break;
+    }
+    Vec_IntFree( vMove );
+//Vec_IntPrint( vOrder );
+    return vOrder;
+}
+                       
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+// 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 );
+    return vMap;
+}
+// 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++ )
+        if ( Vec_IntEntry(vRanks, Vec_IntEntry(vXors, 4*i)) != -1 )
+            Vec_BitWriteEntry( vMap, Vec_IntEntry(vXors, 4*i), 1 );
+    return vMap;
+}
+// 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;
+    for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
+        Vec_BitWriteEntry( vMap, Vec_IntEntry(vAdds, 6*i+4), 1 );
+    return vMap;
+}
+// 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++ )
+    {
+        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;
+}
+// collects XOR roots (XOR nodes not appearing as fanins of other XORs)
+Vec_Int_t * Acec_FindXorRoots( Gia_Man_t * p, Vec_Int_t * vXors )
+{
+    Vec_Bit_t * vMapXorIns = Acec_MapXorIns( p, vXors );
+    Vec_Int_t * vXorRoots = Vec_IntAlloc( 100 );  int i;
+    for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
+        if ( !Vec_BitEntry(vMapXorIns, Vec_IntEntry(vXors, 4*i)) )
+            Vec_IntPushUniqueOrder( vXorRoots, Vec_IntEntry(vXors, 4*i) );
+    Vec_BitFree( vMapXorIns );
+    return vXorRoots;
+}
+// collects XOR trees belonging to each of XOR roots
+Vec_Int_t * Acec_RankTrees( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vXorRoots )
+{
+    Vec_Int_t * vDoubles = Vec_IntAlloc( 100 );
+    int i, k, Entry;
+    // map roots into their ranks
+    Vec_Int_t * vRanks = Vec_IntStartFull( Gia_ManObjNum(p) ); 
+    Vec_IntForEachEntry( vXorRoots, Entry, i )
+        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 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 ) // HA
+                continue;
+            Entry = Vec_IntEntry( vRanks, Node );
+            if ( Entry == Rank ) // the same tree
+                continue;
+            if ( Entry == -1 )
+                Vec_IntWriteEntry( vRanks, Node, Rank );
+            else
+                Vec_IntPush( vDoubles, Node );
+
+            if ( Entry != -1 && Gia_ObjIsAnd(Gia_ManObj(p, Node)))
+            printf( "Xor node %d belongs to Tree %d and Tree %d.\n", Node, Entry, Rank );
+        }
+    }
+    // remove duplicated entries
+    Vec_IntForEachEntry( vDoubles, Entry, i )
+        Vec_IntWriteEntry( vRanks, Entry, -1 );
+    Vec_IntFree( vDoubles );
+    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_Int_t * vXorRoots, Vec_Int_t * vRanks, Vec_Wec_t ** pvAddBoxes )
+{
+    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;
+    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 Fanin = Vec_IntEntry(vXors, 4*i+k);
+            //int RankFanin = Vec_IntEntry(vRanks, Fanin);
+            if ( Fanin == 0 )
+                continue;
+            if ( Vec_BitEntry(vMapXors, Fanin) )
+            {
+                assert( Rank == Vec_IntEntry(vRanks, Fanin) );
+                continue;
+            }
+//            if ( Vec_BitEntry(vMapXors, Fanin) && Rank == RankFanin )
+//                continue;
+            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 )
+        *pvAddBoxes = vAddBoxes;
+    return vXorLeaves;
+}
+void Acec_CheckBoothPPs( Gia_Man_t * p, Vec_Wec_t * vLitLeaves )
+{
+    Vec_Bit_t * vMarked = Acec_MultMarkPPs( p );
+    Vec_Int_t * vLevel;
+    int i, k, iLit;
+    Vec_WecForEachLevel( vLitLeaves, vLevel, i )
+    {
+        int CountPI = 0, CountB = 0, CountNB = 0;
+        Vec_IntForEachEntry( vLevel, iLit, k )
+            if ( !Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) )
+                CountPI++;
+            else if ( Vec_BitEntry( vMarked, Abc_Lit2Var(iLit) ) )
+                CountB++;
+            else
+                CountNB++;
+
+        printf( "Rank %2d : Lits = %5d    PI = %d  Booth = %5d  Non-Booth = %5d\n", i, Vec_IntSize(vLevel), CountPI, CountB, CountNB );
+    }
+    Vec_BitFree( vMarked );
+}
+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 );
+    extern void Acec_TreeVerifyPhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes );
+    extern void Acec_TreeVerifyPhases2( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes );
+
+    int MaxRank = Vec_WecSize( vAddBoxes );
+    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, * vLevel2, * vMap;
+    int i, j, k, Box, Node;
+
+    Acec_Box_t * pBox = ABC_CALLOC( Acec_Box_t, 1 );
+    pBox->pGia        = p;
+    pBox->vAdds       = vAddBoxes; // Vec_WecDup( vAddBoxes );
+    pBox->vLeafLits   = Vec_WecStart( MaxRank + 0 );
+    pBox->vRootLits   = Vec_WecStart( MaxRank + 0 );
+
+    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 )
+    Vec_IntForEachEntry( vLevel, Box, k )
+    {
+        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 );
+
+    // set phases starting from roots
+    vMap = Acec_TreeCarryMap( p, vAdds, pBox->vAdds );
+    Vec_WecForEachLevelReverse( pBox->vAdds, vLevel, i )
+        Vec_IntForEachEntry( vLevel, Box, k )
+            if ( !Vec_BitEntry( vIsLeaf, Vec_IntEntry(vAdds, 6*Box+4) ) )
+            {
+                //printf( "Pushing phase of output %d of box %d\n", Vec_IntEntry(vAdds, 6*Box+4), Box );
+                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( 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 );
+
+    // collect last bit
+    vLevel  = Vec_WecEntry( pBox->vLeafLits, Vec_WecSize(pBox->vLeafLits)-1 );
+    vLevel2 = Vec_WecEntry( vXorLeaves, Vec_WecSize(vXorLeaves)-1 );
+    if ( Vec_IntSize(vLevel) == 0 && Vec_IntSize(vLevel2) > 0 )
+    {
+        Vec_IntForEachEntry( vLevel2, Node, k )
+            Vec_IntPush( vLevel, Abc_Var2Lit(Node, 0) );
+    }
+    vLevel  = Vec_WecEntry( pBox->vRootLits, Vec_WecSize(pBox->vRootLits)-1 );
+    Vec_IntFill( vLevel, 1, Abc_Var2Lit(Vec_IntEntryLast(vXorRoots), 0) );
+
+    // sort each level
+    Vec_WecForEachLevel( pBox->vLeafLits, vLevel, i )
+        Vec_IntSort( vLevel, 0 );
+    Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
+        Vec_IntSort( vLevel, 1 );
+
+    //Acec_CheckBoothPPs( p, pBox->vLeafLits );
+    return pBox;
+}
+
+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 * vTemp, * vXorRoots = Acec_FindXorRoots( p, vXors ); 
+    Vec_Int_t * vRanks = Acec_RankTrees( p, vXors, vXorRoots ); 
+    Vec_Wec_t * vXorLeaves, * vAddBoxes = NULL; 
+
+    Gia_ManLevelNum(p);
+
+    //Acec_CheckXors( p, vXors );
+
+    //Ree_ManPrintAdders( vAdds, 1 );
+    if ( fVerbose )
+        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 );
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+    vXorRoots = Acec_OrderTreeRoots( p, vAdds, vTemp = vXorRoots, vRanks );
+    Vec_IntFree( vTemp );
+    Vec_IntFree( vRanks );
+
+    vRanks = Acec_RankTrees( p, vXors, vXorRoots ); 
+    vXorLeaves = Acec_FindXorLeaves( p, vXors, vAdds, vXorRoots, vRanks, &vAddBoxes ); 
+    Vec_IntFree( vRanks );
+
+    //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 );
+
+    Acec_TreeVerifyConnections( p, vAdds, vAddBoxes );
+
+    pBox = Acec_FindBox( p, vAdds, vAddBoxes, vXorLeaves, vXorRoots );
+    //Vec_WecFree( vAddBoxes );
+
+    if ( fVerbose )
+        Acec_TreePrintBox( pBox, vAdds );
+
+    Vec_IntFree( vXorRoots );
+    Vec_WecFree( vXorLeaves );
+
+    Vec_IntFree( vXors );
+    Vec_IntFree( vAdds );
+
+    return pBox;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make
index df6db695..f4c69892 100644
--- a/src/proof/acec/module.make
+++ b/src/proof/acec/module.make
@@ -1,13 +1,18 @@
 SRC +=    src/proof/acec/acecCl.c \
     src/proof/acec/acecCore.c \
     src/proof/acec/acecCo.c \
+    src/proof/acec/acecBo.c \
     src/proof/acec/acecRe.c \
     src/proof/acec/acecPa.c \
     src/proof/acec/acecPo.c \
     src/proof/acec/acecPool.c \
     src/proof/acec/acecCover.c \
     src/proof/acec/acecFadds.c \
+    src/proof/acec/acecMult.c \
+    src/proof/acec/acecNorm.c \
     src/proof/acec/acecOrder.c \
     src/proof/acec/acecPolyn.c \
     src/proof/acec/acecSt.c \
-    src/proof/acec/acecUtil.c      
+    src/proof/acec/acecTree.c \
+    src/proof/acec/acecUtil.c \
+    src/proof/acec/acecXor.c