Version abc80318

4 files changed, 201 insertions, 3 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index bd77c0a4..33f7b2a0 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -526,6 +526,7 @@ extern Vec_Ptr_t *     Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSu
 extern Vec_Ptr_t *     Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
 extern Vec_Ptr_t *     Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );
 extern Aig_Man_t *     Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
+extern Aig_Man_t *     Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
 /*=== aigPartReg.c =========================================================*/
 extern Vec_Ptr_t *     Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize );
 extern Vec_Ptr_t *     Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index df5792b2..1fb93eb7 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -1022,6 +1022,75 @@ Vec_Ptr_t * Aig_ManDupPart( Aig_Man_t * pNew, Aig_Man_t * pOld, Vec_Int_t * vPar
 
 /**Function*************************************************************
 
+  Synopsis    [Adds internal nodes in the topological order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManDupPartAll_rec( Aig_Man_t * pNew, Aig_Man_t * pOld, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pObjNew;
+    assert( !Aig_IsComplement(pObj) );
+    if ( Aig_ObjIsTravIdCurrent(pOld, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(pOld, pObj);
+    if ( Aig_ObjIsPi(pObj) )
+        pObjNew = Aig_ObjCreatePi(pNew);
+    else if ( Aig_ObjIsPo(pObj) )
+    {
+        Aig_ManDupPartAll_rec( pNew, pOld, Aig_ObjFanin0(pObj) );
+        pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    }
+    else
+    {
+        assert( Aig_ObjIsNode(pObj) );
+        Aig_ManDupPartAll_rec( pNew, pOld, Aig_ObjFanin0(pObj) );
+        Aig_ManDupPartAll_rec( pNew, pOld, Aig_ObjFanin1(pObj) );
+        pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    }
+    pObj->pData = pObjNew;
+    pObjNew->pData = pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds internal nodes in the topological order.]
+
+  Description [Returns the array of new outputs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupPartAll( Aig_Man_t * pOld, Vec_Int_t * vPart )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i, Entry;
+    Aig_ManIncrementTravId( pOld );
+    pNew = Aig_ManStart( 5000 );
+    // map constant nodes
+    pObj = Aig_ManConst1(pOld);
+    pObjNew = Aig_ManConst1(pNew);
+    pObj->pData = pObjNew;
+    pObjNew->pData = pObj;
+    Aig_ObjSetTravIdCurrent(pOld, pObj);
+    // map all other nodes
+    Vec_IntForEachEntry( vPart, Entry, i )
+    {
+        pObj = Aig_ManPo( pOld, Entry );
+        Aig_ManDupPartAll_rec( pNew, pOld, pObj );
+    }
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Create partitioned miter of the two AIGs.]
 
   Description [Assumes that each output in the second AIG cannot have 
@@ -1205,6 +1274,77 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
     return pAig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs partitioned choice computation.]
+
+  Description [Assumes that each output in the second AIG cannot have 
+  more supp vars than the same output in the first AIG.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose )
+{
+    extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
+
+    Aig_Man_t * pAigPart, * pAigTemp;
+    Vec_Int_t * vPart;
+    Vec_Ptr_t * vParts;
+    Aig_Obj_t * pObj;
+    void ** ppData;
+    int i, k;
+
+    // partition the outputs of the AIG
+    vParts = Aig_ManPartitionNaive( pAig, nPartSize );
+
+    // start the equivalence classes
+    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
+
+    // set the PI numbers
+    Aig_ManForEachPi( pAig, pObj, k )
+        pObj->pNext = (Aig_Obj_t *)(long)k;
+
+    // create the total fraiged AIG
+    Vec_PtrForEachEntry( vParts, vPart, i )
+    {
+        // derive the partition AIG
+        pAigPart = Aig_ManDupPartAll( pAig, vPart );
+        // store contents of pData pointers
+        ppData = ALLOC( void *, Aig_ManObjNumMax(pAigPart) );
+        Aig_ManForEachObj( pAigPart, pObj, k )
+            ppData[k] = pObj->pData;
+        // report the process
+        if ( fVerbose )
+        printf( "Part %4d  (out of %4d)  PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", 
+            i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart), 
+            Aig_ManNodeNum(pAigPart), Aig_ManLevelNum(pAigPart) );
+        // compute equivalence classes (to be stored in pNew->pReprs)
+        pAigTemp = Fra_FraigChoice( pAigPart, nConfMax, nLevelMax );
+        Aig_ManStop( pAigTemp );
+        // reset the pData pointers
+        Aig_ManForEachObj( pAigPart, pObj, k )
+            pObj->pData = ppData[k];
+        free( ppData );
+        // transfer representatives to the total AIG
+        if ( pAigPart->pReprs )
+            Aig_ManTransferRepr( pAig, pAigPart );
+        Aig_ManStop( pAigPart );
+    }
+    if ( fVerbose )
+    printf( "                                                                                          \r" );
+    Vec_VecFree( (Vec_Vec_t *)vParts );
+
+    // clear the PI numbers
+    Aig_ManForEachPi( pAig, pObj, k )
+        pObj->pNext = NULL;
+
+    // derive the result of choicing
+    return Aig_ManDupRepr( pAig, 0 );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 91133b2a..7178cc0a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8458,23 +8458,39 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c, fProve, fVerbose, fDoSparse;
     int nConfLimit;
+    int nPartSize;
+    int nLevelMax;
 
     extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarFraigPart( Abc_Ntk_t * pNtk, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    nPartSize    = 0;
+    nLevelMax    = 0;
     nConfLimit   = 100;   
     fDoSparse    = 0;
     fProve       = 0;
     fVerbose     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Cspvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PCLspvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPartSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPartSize < 0 ) 
+                goto usage;
+            break;
         case 'C':
             if ( globalUtilOptind >= argc )
             {
@@ -8486,6 +8502,17 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConfLimit < 0 ) 
                 goto usage;
             break;
+         case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLevelMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLevelMax < 0 ) 
+                goto usage;
+            break;
         case 's':
             fDoSparse ^= 1;
             break;
@@ -8512,7 +8539,10 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose );
+    if ( nPartSize > 0 )
+        pNtkRes = Abc_NtkDarFraigPart( pNtk, nPartSize, nConfLimit, nLevelMax, fVerbose );
+    else
+        pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -8523,9 +8553,11 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ifraig [-C num] [-spvh]\n" );
+    fprintf( pErr, "usage: ifraig [-P num] [-C num] [-L num] [-spvh]\n" );
     fprintf( pErr, "\t         performs fraiging using a new method\n" );
+    fprintf( pErr, "\t-P num : partition size (0 = partitioning is not used) [default = %d]\n", nPartSize );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
+    fprintf( pErr, "\t-L num : limit on node level to fraig (0 = fraig all nodes) [default = %d]\n", nLevelMax );
     fprintf( pErr, "\t-s     : toggle considering sparse functions [default = %s]\n", fDoSparse? "yes": "no" );
     fprintf( pErr, "\t-p     : toggle proving the miter outputs [default = %s]\n", fProve? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 78f43aac..e1b3828e 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -604,6 +604,31 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarFraigPart( Abc_Ntk_t * pNtk, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 0 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Aig_ManFraigPartitioned( pTemp = pMan, nPartSize, nConfLimit, nLevelMax, fVerbose );
+    Aig_ManStop( pTemp );
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose )
 {
     extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );