Updates to arithmetic verification.

abclib.dsp

@@ -5507,6 +5507,10 @@ SOURCE=.\src\proof\acec\acecInt.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\proof\acec\acecNorm.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\proof\acec\acecOrder.c
 # End Source File
 # Begin Source File

src/base/abci/abc.c

@@ -481,6 +481,7 @@ static int Abc_CommandAbc9Fadds              ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9ATree              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Polyn              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Acec               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Anorm              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Esop               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Exorcism           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Mfs                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1124,6 +1125,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&atree",        Abc_CommandAbc9ATree,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&polyn",        Abc_CommandAbc9Polyn,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&acec",         Abc_CommandAbc9Acec,         0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&anorm",        Abc_CommandAbc9Anorm,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&esop",         Abc_CommandAbc9Esop,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&exorcism",     Abc_CommandAbc9Exorcism,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mfs",          Abc_CommandAbc9Mfs,          0 );
@@ -40728,6 +40730,52 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Anorm( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Anorm(): There is no AIG.\n" );
+        return 0;
+    }
+    pTemp = Acec_Normalize( pAbc->pGia, fVerbose );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &anorm [-vh]\n" );
+    Abc_Print( -2, "\t         normalize adder trees in the current AIG\n" );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []

src/base/wlc/wlcBlast.c

@@ -1509,7 +1509,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
         assert( Vec_PtrSize(pNew->vNamesOut) == Gia_ManCoNum(pNew) );
     }
 
-    pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName );
+    //pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName );
     // dump the miter parts
     if ( 0 )
     {

src/proof/acec/acec.h

@@ -80,6 +80,8 @@ extern void          Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int f
 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 fVerbose );
 
 
 ABC_NAMESPACE_HEADER_END

src/proof/acec/acecCore.c

@@ -57,98 +57,6 @@ void Acec_ManCecSetDefaultParams( Acec_ParCec_t * p )
     p->iOutFail       =      -1;    // the number of failed output
 }  
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Acec_BoxFree( Acec_Box_t * pBox )
-{
-    Vec_WecFreeP( &pBox->vAdds );
-    Vec_WecFreeP( &pBox->vLeafs );
-    Vec_WecFreeP( &pBox->vRoots );
-    Vec_WecFreeP( &pBox->vLeafLits );
-    Vec_WecFreeP( &pBox->vRootLits );
-    Vec_WecFreeP( &pBox->vUnique );
-    Vec_WecFreeP( &pBox->vShared );
-    Vec_BitFreeP( &pBox->vInvHadds );
-    ABC_FREE( pBox );
-}
-void Acec_BoxFreeP( Acec_Box_t ** ppBox )
-{
-    if ( *ppBox )
-        Acec_BoxFree( *ppBox );
-    *ppBox = NULL;
-}
-
-/**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[0] = Vec_IntPop( vLevel );
-            In[1] = Vec_IntPop( vLevel );
-            In[2] = Vec_IntPop( vLevel );
-            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] );
-        }
-        assert( Vec_IntSize(vLevel) == 1 );
-        Vec_IntPush( vRootRanks, Vec_IntEntry(vLevel, 0) );
-    }
-    return vRootRanks;
-}
-
 /**Function*************************************************************
 
   Synopsis    []
@@ -251,12 +159,14 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
         int * pEnd1 = Vec_IntLimit(vLevel1);
         while ( pBeg0 < pEnd0 && pBeg1 < pEnd1 )
         {
-            if ( *pBeg0 == *pBeg1 )
+            int Entry0 = Abc_Lit2LitV( Vec_IntArray(vMap0), *pBeg0 );
+            int Entry1 = Abc_Lit2LitV( Vec_IntArray(vMap1), *pBeg1 );
+            if ( Entry0 == Entry1 )
             {
                 Vec_IntPush( vShared0, *pBeg0++ );
                 Vec_IntPush( vShared1, *pBeg1++ );
             }
-            else if ( *pBeg0 > *pBeg1 )
+            else if ( Entry0 > Entry1 )
                 Vec_IntPush( vUnique0, *pBeg0++ );
             else 
                 Vec_IntPush( vUnique1, *pBeg1++ );
@@ -269,105 +179,14 @@ int Acec_MatchBoxes( Acec_Box_t * pBox0, Acec_Box_t * pBox1 )
         assert( Vec_IntSize(vShared0) + Vec_IntSize(vUnique0) == Vec_IntSize(vLevel0) );
         assert( Vec_IntSize(vShared1) + Vec_IntSize(vUnique1) == Vec_IntSize(vLevel1) );
     }
+    Vec_IntFree( vMap0 );
+    Vec_IntFree( vMap1 );
     nTotal = Vec_WecSizeSize(pBox0->vShared);
     printf( "Box0: Matched %d entries out of %d.\n", nTotal, Vec_WecSizeSize(pBox0->vLeafLits) );
     printf( "Box1: Matched %d entries out of %d.\n", nTotal, Vec_WecSizeSize(pBox1->vLeafLits) );
     return nTotal;
 }
 
-/**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_ManAppendAnd( 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_Wec_t * vLeafMap = Vec_WecStart( Vec_WecSize(vLeafLits) );
-    Vec_Int_t * vLevel, * vRootRanks;  
-    int i, k, iLit, iLitNew;
-    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;
-    int i, k, iLit, iLitNew;
-    pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Abc_UtilStrsav( p->pName );
-    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
-    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 );
-    else
-    {
-        Vec_Wec_t * vLeafLits;
-        assert( pBox->vShared != NULL );
-        assert( pBox->vUnique != NULL );
-        vRootRanks = Acec_BuildTree( p, p, pBox->vShared );
-        // add these roots to the unique ones
-        vLeafLits = Vec_WecDup( pBox->vUnique );
-        Vec_IntForEachEntry( vRootRanks, iLit, i )
-        {
-            if ( i < Vec_WecSize(vLeafLits) )
-                vLevel = Vec_WecEntry(vLeafLits, i);
-            else
-                vLevel = Vec_WecPushLevel(vLeafLits);
-            Vec_IntPush( vLevel, iLit );
-        }
-        Vec_IntFree( vRootRanks );
-        vRootRanks = Acec_BuildTree( pNew, p, vLeafLits );
-        Vec_WecFree( vLeafLits );
-    }
-    // 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, k );
-            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    []
@@ -385,8 +204,8 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
     Gia_Man_t * pMiter;
     Gia_Man_t * pGia0n = pGia0, * pGia1n = pGia1;
     Cec_ParCec_t ParsCec, * pCecPars = &ParsCec;
-    Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0 );
+    Acec_Box_t * pBox0 = Acec_DeriveBox( pGia0, pPars->fVerbose );
-    Acec_Box_t * pBox1 = Acec_DeriveBox( pGia1 );
+    Acec_Box_t * pBox1 = Acec_DeriveBox( 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
@@ -403,7 +222,7 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
     pMiter = Gia_ManMiter( pGia0n, pGia1n, 0, 1, 0, 0, pPars->fVerbose );
     if ( pMiter )
     {
-        int fDumpMiter = 1;
+        int fDumpMiter = 0;
         if ( fDumpMiter )
         {
             Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "acec_miter.aig" );

src/proof/acec/acecInt.h

@@ -70,8 +70,11 @@ struct Acec_Box_t_
 /*=== 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 );
+/*=== acecNorm.c ========================================================*/
+extern Gia_Man_t *   Acec_InsertBox( Acec_Box_t * pBox, int fAll );
 /*=== acecTree.c ========================================================*/
-extern Acec_Box_t *  Acec_DeriveBox( Gia_Man_t * p );
+extern Acec_Box_t *  Acec_DeriveBox( Gia_Man_t * p, 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 );

src/proof/acec/acecNorm.c

@@ -0,0 +1,215 @@
+/**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 );
+            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_ManAppendAnd( 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_Wec_t * vLeafMap = Vec_WecStart( Vec_WecSize(vLeafLits) );
+    Vec_Int_t * vLevel, * vRootRanks;  
+    int i, k, iLit, iLitNew;
+    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;
+    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 );
+    else
+    {
+        Vec_Wec_t * vLeafLits;
+        assert( pBox->vShared != NULL );
+        assert( pBox->vUnique != NULL );
+        vRootRanks = Acec_BuildTree( p, p, pBox->vShared );
+        // add these roots to the unique ones
+        vLeafLits = Vec_WecDup( pBox->vUnique );
+        Vec_IntForEachEntry( vRootRanks, iLit, i )
+        {
+            if ( i < Vec_WecSize(vLeafLits) )
+                vLevel = Vec_WecEntry(vLeafLits, i);
+            else
+                vLevel = Vec_WecPushLevel(vLeafLits);
+            Vec_IntPush( vLevel, iLit );
+        }
+        Vec_IntFree( vRootRanks );
+        vRootRanks = Acec_BuildTree( pNew, p, vLeafLits );
+        Vec_WecFree( vLeafLits );
+    }
+    // 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 fVerbose )
+{
+    Acec_Box_t * pBox = Acec_DeriveBox( pGia, fVerbose );
+    Gia_Man_t * pNew  = Acec_InsertBox( pBox, 1 );
+    Acec_BoxFreeP( &pBox );
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/proof/acec/acecTree.c

@@ -31,6 +31,36 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_BoxFree( Acec_Box_t * pBox )
+{
+    Vec_WecFreeP( &pBox->vAdds );
+    Vec_WecFreeP( &pBox->vLeafs );
+    Vec_WecFreeP( &pBox->vRoots );
+    Vec_WecFreeP( &pBox->vLeafLits );
+    Vec_WecFreeP( &pBox->vRootLits );
+    Vec_WecFreeP( &pBox->vUnique );
+    Vec_WecFreeP( &pBox->vShared );
+    Vec_BitFreeP( &pBox->vInvHadds );
+    ABC_FREE( pBox );
+}
+void Acec_BoxFreeP( Acec_Box_t ** ppBox )
+{
+    if ( *ppBox )
+        Acec_BoxFree( *ppBox );
+    *ppBox = NULL;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Find internal cut points with exactly one adder fanin/fanout.]
@@ -412,6 +442,31 @@ void Acec_TreePhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes,
   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 : {", i );
+        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( " }\n" );
+    }
+}
+void Vec_WecPrintLits( Vec_Wec_t * p )
+{
+    Vec_Int_t * vVec;
+    int i, k, Entry;
+    Vec_WecForEachLevel( p, vVec, i )
+    {
+        printf( " %4d : {", i );
+        Vec_IntForEachEntry( vVec, Entry, k )
+            printf( " %c%d", Abc_LitIsCompl(Entry) ? '-' : '+', Abc_Lit2Var(Entry) );
+        printf( " }\n" );
+    }
+}
 void Acec_PrintRootLits( Vec_Wec_t * vRoots )
 {
     Vec_Int_t * vLevel;
@@ -429,30 +484,6 @@ void Acec_PrintRootLits( Vec_Wec_t * vRoots )
         printf( "\n" );
     }
 }
-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 : {", i );
-        Vec_IntForEachEntry( vLevel, iBox, k )
-            printf( " (%d,%d)", Vec_IntEntry(vAdds, 6*iBox+3), Vec_IntEntry(vAdds, 6*iBox+4) );
-        printf( " }\n" );
-    }
-}
-void Vec_WecPrintLits( Vec_Wec_t * p )
-{
-    Vec_Int_t * vVec;
-    int i, k, Entry;
-    Vec_WecForEachLevel( p, vVec, i )
-    {
-        printf( " %4d : {", i );
-        Vec_IntForEachEntry( vVec, Entry, k )
-            printf( " %c%d", Abc_LitIsCompl(Entry) ? '-' : '+', Abc_Lit2Var(Entry) );
-        printf( " }\n" );
-    }
-}
 void Acec_PrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds )
 {
     printf( "Adders:\n" );
@@ -488,7 +519,6 @@ Acec_Box_t * Acec_CreateBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree
 }
 void Acec_CreateBoxTest( Gia_Man_t * p )
 {
-    extern void Acec_BoxFree( Acec_Box_t * pBox );
     Acec_Box_t * pBox;
     Vec_Wec_t * vTrees;
     Vec_Int_t * vTree;
@@ -511,8 +541,8 @@ void Acec_CreateBoxTest( Gia_Man_t * p )
         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_PrintBox( pBox );
+        Acec_PrintBox( pBox, vAdds );
-        Acec_BoxFree( pBox );
+        Acec_BoxFreeP( &pBox );
     }
 
     Vec_WecFree( vTrees );
@@ -530,9 +560,22 @@ void Acec_CreateBoxTest( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p )
+Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, int fVerbose )
 {
-    return NULL;
+    Acec_Box_t * pBox = NULL;
+    Vec_Int_t * vAdds = Ree_ManComputeCuts( p, NULL, fVerbose );
+    Vec_Wec_t * vTrees = Acec_TreeFindTrees( p, vAdds );
+    if ( vTrees && Vec_WecSize(vTrees) > 0 )
+        pBox = Acec_CreateBox( p, vAdds, Vec_WecEntry(vTrees, 0) );
+    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_PrintBox( pBox, vAdds );
+    Vec_WecFreeP( &vTrees );
+    Vec_IntFree( vAdds );
+    return pBox;
 }
 
 ////////////////////////////////////////////////////////////////////////

src/proof/acec/module.make

@@ -8,6 +8,7 @@ SRC +=    src/proof/acec/acecCl.c \
     src/proof/acec/acecPool.c \
     src/proof/acec/acecCover.c \
     src/proof/acec/acecFadds.c \
+    src/proof/acec/acecNorm.c \
     src/proof/acec/acecOrder.c \
     src/proof/acec/acecPolyn.c \
     src/proof/acec/acecSt.c \