Version abc80305

13 files changed, 126 insertions, 53 deletions

diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c
index b3bc28b2..c939a38c 100644
--- a/src/aig/aig/aigInter.c
+++ b/src/aig/aig/aigInter.c
@@ -26,6 +26,10 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern int timeCnf;
+extern int timeSat;
+extern int timeInt;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -51,17 +55,20 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose
     Vec_Int_t * vVarsAB;
     Aig_Obj_t * pObj, * pObj2;
     int Lits[3], status, i;
-    int clk = clock();
+    int clk;
 
     assert( Aig_ManPiNum(pManOn) == Aig_ManPiNum(pManOff) );
 
+clk = clock();
     // derive CNFs
-    pCnfOn  = Cnf_Derive( pManOn, 0 );
-    pCnfOff = Cnf_Derive( pManOff, 0 );
-//    pCnfOn  = Cnf_DeriveSimple( pManOn, 0 );
-//    pCnfOff = Cnf_DeriveSimple( pManOff, 0 );
+//    pCnfOn  = Cnf_Derive( pManOn, 0 );
+//    pCnfOff = Cnf_Derive( pManOff, 0 );
+    pCnfOn  = Cnf_DeriveSimple( pManOn, 0 );
+    pCnfOff = Cnf_DeriveSimple( pManOff, 0 );
     Cnf_DataLift( pCnfOff, pCnfOn->nVars );
+timeCnf += clock() - clk;
 
+clk = clock();
     // start the solver
     pSat = sat_solver_new();
     sat_solver_store_alloc( pSat );
@@ -112,10 +119,6 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose
     Cnf_DataFree( pCnfOn );
     Cnf_DataFree( pCnfOff );
     sat_solver_store_mark_roots( pSat );
-    if ( fVerbose )
-    {
-        PRT( "Prepare", clock() - clk );
-    }
 
 /*
     status = sat_solver_simplify(pSat);
@@ -130,12 +133,8 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose
 */
 
     // solve the problem
-    clk = clock();
     status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
-    if ( fVerbose )
-    {
-        PRT( "Solving", clock() - clk );
-    }
+timeSat += clock() - clk;
     if ( status == l_False )
     {
         pSatCnf = sat_solver_store_release( pSat );
@@ -158,9 +157,11 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose
     }
 
     // create the resulting manager
+clk = clock();
     pManInter = Inta_ManAlloc();
     pRes = Inta_ManInterpolate( pManInter, pSatCnf, vVarsAB, fVerbose );
     Inta_ManFree( pManInter );
+timeInt += clock() - clk;
 
     Vec_IntFree( vVarsAB );
     Sto_ManFree( pSatCnf );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 2d03e65d..baae7c3f 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -207,7 +207,7 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_PrintClass( Aig_Obj_t ** pClass )
+void Fra_PrintClass( Fra_Cla_t * p, Aig_Obj_t ** pClass )
 {
     Aig_Obj_t * pTemp;
     int i;
@@ -215,7 +215,7 @@ void Fra_PrintClass( Aig_Obj_t ** pClass )
         assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
     printf( "{ " );
     for ( i = 0; (pTemp = pClass[i]); i++ )
-        printf( "%d(%d) ", pTemp->Id, pTemp->Level );
+        printf( "%d(%d,%d) ", pTemp->Id, pTemp->Level, Aig_SupportSize(p->pAig,pTemp) );
     printf( "}\n" );
 }
 
@@ -248,12 +248,12 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
             assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
         printf( "Constants { " );
         Vec_PtrForEachEntry( p->vClasses1, pObj, i )
-            printf( "%d ", pObj->Id );
+            printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
         printf( "}\n" );
         Vec_PtrForEachEntry( p->vClasses, pClass, i )
         {
             printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
-            Fra_PrintClass( pClass );
+            Fra_PrintClass( p, pClass );
         }
         printf( "\n" );
     }
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index d95515d5..c9ea4907 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -1526,11 +1526,11 @@ Aig_Obj_t * Fra_ClausGetLiteral( Clu_Man_t * p, int * pVar2Id, int Lit )
 
 ***********************************************************************/
 void Fra_ClausWriteIndClauses( Clu_Man_t * p )
-{
+{ 
     extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
     Aig_Man_t * pNew;
     Aig_Obj_t * pClause, * pLiteral;
-    char Buffer[500], * pName;
+    char * pName;
     int * pStart, * pVar2Id; 
     int Beg, End, i, k;
     // create mapping from SAT vars to node IDs
@@ -1560,12 +1560,9 @@ void Fra_ClausWriteIndClauses( Clu_Man_t * p )
     }
     free( pVar2Id );
     Aig_ManCleanup( pNew );
-    // write the manager into a file
-    pName = Ioa_FileNameGeneric(p->pAig->pName);
-    sprintf( Buffer, "%s_care.aig", pName );
-    free( pName );
-    printf( "Care clauses are written into file \"%s\".\n", Buffer );
-    Ioa_WriteAiger( pNew, Buffer, 0, 1 );
+    pName = Ioa_FileNameGenericAppend( p->pAig->pName, "_care.aig" );
+    printf( "Care one-hotness clauses will be written into file \"%s\".\n", pName );
+    Ioa_WriteAiger( pNew, pName, 0, 1 );
     Aig_ManStop( pNew );
 }
 
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 0a81105b..67940c4f 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -328,6 +328,8 @@ void Fra_FraigSweep( Fra_Man_t * p )
         // quit if simulation detected a counter-example for a PO
         if ( p->pManFraig->pData )
             continue;
+//        if ( Aig_SupportSize(p->pManAig,pObj) > 16 )
+//            continue;
         // perform fraiging
         if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
             p->pPars->nBTLimitNode = 5;
@@ -381,6 +383,8 @@ clk = clock();
     p->nNodesBeg = Aig_ManNodeNum(pManAig);
     p->nRegsBeg  = Aig_ManRegNum(pManAig);
     // perform fraig sweep
+if ( p->pPars->fVerbose )
+Fra_ClassesPrint( p->pCla, 1 );
     Fra_FraigSweep( p );
     // call back the procedure to check implications
     if ( pManAig->pImpFunc )
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 7e0d080c..18c9ffcc 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -560,16 +560,12 @@ clk2 = clock();
     if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
     {
         extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
-        char Buffer[500], * pStart;
         Aig_Man_t * pNew;
+        char * pFileName = Ioa_FileNameGenericAppend( p->pManAig->pName, "_care.aig" );
+        printf( "Care one-hotness clauses will be written into file \"%s\".\n", pFileName );
         pManAigNew = Aig_ManDup( pManAig, 1 );
-//        pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots );
         pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
-        pStart = Ioa_FileNameGeneric(p->pManAig->pName);
-        sprintf( Buffer, "%s_care.aig", pStart );
-        free( pStart );
-        printf( "Care one-hotness clauses are written into file \"%s\".\n", Buffer );
-        Ioa_WriteAiger( pNew, Buffer, 0, 1 );
+        Ioa_WriteAiger( pNew, pFileName, 0, 1 );
         Aig_ManStop( pNew );
     }
     else 
diff --git a/src/aig/ioa/ioa.h b/src/aig/ioa/ioa.h
index e697a729..be8594e7 100644
--- a/src/aig/ioa/ioa.h
+++ b/src/aig/ioa/ioa.h
@@ -66,6 +66,7 @@ extern void           Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fW
 /*=== ioaUtil.c =======================================================*/
 extern int            Ioa_FileSize( char * pFileName );
 extern char *         Ioa_FileNameGeneric( char * FileName );
+extern char *         Ioa_FileNameGenericAppend( char * pBase, char * pSuffix );
 extern char *         Ioa_TimeStamp();
 
 #ifdef __cplusplus
diff --git a/src/aig/ioa/ioaUtil.c b/src/aig/ioa/ioaUtil.c
index 79dcca1e..6063d8be 100644
--- a/src/aig/ioa/ioaUtil.c
+++ b/src/aig/ioa/ioaUtil.c
@@ -88,6 +88,41 @@ char * Ioa_FileNameGeneric( char * FileName )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the composite name of the file.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ioa_FileNameGenericAppend( char * pBase, char * pSuffix )
+{
+    static char Buffer[1000];
+    char * pDot;
+    if ( pBase == NULL )
+    {
+        strcpy( Buffer, pSuffix );
+        return Buffer;
+    }
+    strcpy( Buffer, pBase );
+    pDot = strstr( Buffer, "." );
+    if ( pDot )
+        *pDot = 0;
+    strcat( Buffer, pSuffix );
+    // find the last occurrance of slash
+    for ( pDot = Buffer + strlen(Buffer) - 1; pDot >= Buffer; pDot-- )    
+        if (!((*pDot >= '0' && *pDot <= '9') ||
+              (*pDot >= 'a' && *pDot <= 'z') ||
+              (*pDot >= 'A' && *pDot <= 'Z') || 
+               *pDot == '_' || *pDot == '.') )
+               break;
+    return pDot + 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the time stamp.]
 
   Description [The file should be closed.]
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 11ef85f9..aea02c0e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10749,6 +10749,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nFlowIters  =  1;
     pPars->nAreaIters  =  2;
     pPars->DelayTarget = -1;
+    pPars->Epsilon     =  (float)0.001;
     pPars->fPreprocess =  1;
     pPars->fArea       =  0;
     pPars->fFancy      =  0;
@@ -10768,7 +10769,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->pFuncCost   =  NULL;   
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADpaflemrstvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEpaflemrstvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10828,6 +10829,16 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
             globalUtilOptind++;
             if ( pPars->DelayTarget <= 0.0 ) 
                 goto usage;
+        case 'E':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-E\" should be followed by a floating point number.\n" );
+                goto usage;
+            }
+            pPars->Epsilon = (float)atof(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->Epsilon < 0.0 || pPars->Epsilon > 1.0 ) 
+                goto usage;
             break;
         case 'p':
             pPars->fPreprocess ^= 1;
@@ -10980,13 +10991,14 @@ usage:
         sprintf( LutSize, "library" );
     else
         sprintf( LutSize, "%d", pPars->nLutSize );
-    fprintf( pErr, "usage: if [-K num] [-C num] [-F num] [-A num] [-D float] [-parlemsvh]\n" );
+    fprintf( pErr, "usage: if [-KCFA num] [-DE float] [-parlemsvh]\n" );
     fprintf( pErr, "\t           performs FPGA technology mapping of the network\n" );
     fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     fprintf( pErr, "\t-C num   : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
     fprintf( pErr, "\t-F num   : the number of area flow recovery iterations (num >= 0) [default = %d]\n", pPars->nFlowIters );
     fprintf( pErr, "\t-A num   : the number of exact area recovery iterations (num >= 0) [default = %d]\n", pPars->nAreaIters );
     fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );  
+    fprintf( pErr, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->Epsilon );  
     fprintf( pErr, "\t-p       : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
     fprintf( pErr, "\t-a       : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" );
 //    fprintf( pErr, "\t-f       : toggles one fancy feature [default = %s]\n", pPars->fFancy? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index d69a7097..c14d0317 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1565,6 +1565,11 @@ Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbo
     return pNtkAig;
 }
 
+
+int timeCnf;
+int timeSat;
+int timeInt;
+
 /**Function*************************************************************
 
   Synopsis    [Interplates two networks.]
@@ -1594,6 +1599,9 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose
     Abc_NtkForEachPi( pNtkOn, pObj, i )
         Abc_NtkDupObj( pNtkInter, pObj, 1 );
     // process each POs separately
+timeCnf = 0;
+timeSat = 0;
+timeInt = 0;
     Abc_NtkForEachCo( pNtkOn, pObj, i )
     {
         pNtkOn1 = Abc_NtkCreateCone( pNtkOn, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 1 );
@@ -1620,6 +1628,10 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose
         Abc_NtkDelete( pNtkOff1 );
         Abc_NtkDelete( pNtkInter1 );
     }
+//    PRT( "CNF", timeCnf );
+//    PRT( "SAT", timeSat );
+//    PRT( "Int", timeInt );
+
     // return the network
     if ( !Abc_NtkCheck( pNtkInter ) )
         fprintf( stdout, "Abc_NtkAttachBottom(): Network check has failed.\n" );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index acda5d51..32d458dc 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -81,6 +81,7 @@ struct If_Par_t_
     int                nFlowIters;    // the number of iterations of area recovery
     int                nAreaIters;    // the number of iterations of area recovery
     float              DelayTarget;   // delay target
+    float              Epsilon;       // value used in comparison floating point numbers
     int                fPreprocess;   // preprossing
     int                fArea;         // area-oriented mapping
     int                fFancy;        // a fancy feature
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 6b21919b..1528b08c 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -51,7 +51,7 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     p = ALLOC( If_Man_t, 1 );
     memset( p, 0, sizeof(If_Man_t) );
     p->pPars = pPars;
-    p->fEpsilon = (float)0.001;
+    p->fEpsilon = pPars->Epsilon;
     // allocate arrays for nodes
     p->vCis    = Vec_PtrAlloc( 100 );
     p->vCos    = Vec_PtrAlloc( 100 );
@@ -77,7 +77,7 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     p->puTemp[3] = p->puTemp[2] + p->nTruthWords;
     // create the constant node
     p->pConst1 = If_ManSetupObj( p );
-    p->pConst1->Type = IF_CONST1;
+    p->pConst1->Type   = IF_CONST1;
     p->pConst1->fPhase = 1;
     p->nObjs[IF_CONST1]++;
     return p;
diff --git a/src/misc/extra/extraUtilUtil.c b/src/misc/extra/extraUtilUtil.c
index c685f7bc..e2c407cd 100644
--- a/src/misc/extra/extraUtilUtil.c
+++ b/src/misc/extra/extraUtilUtil.c
@@ -49,22 +49,6 @@ static char *pScanStr;
 
 /**Function*************************************************************
 
-  Synopsis    [util_cpu_time()]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-long Extra_CpuTime()
-{
-    return clock();
-}
-
-/**Function*************************************************************
-
   Synopsis    [getSoftDataLimit()]
 
   Description []
@@ -349,6 +333,34 @@ void Extra_UtilMMout_Of_Memory( long size )
 void (*Extra_UtilMMoutOfMemory)() = Extra_UtilMMout_Of_Memory;
 
 
+/**Function*************************************************************
+
+  Synopsis    [util_cpu_time()]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+#if defined(NT) || defined(NT64) || defined(WIN32)
+long Extra_CpuTime()
+{
+    return clock();
+}
+#else
+#include <sys/time.h>
+#include <sys/resource.h>
+#include <unistd.h>
+long Extra_CpuTime()
+{
+    struct rusage ru;
+    getrusage(RUSAGE_SELF, &ru);
+    return (long)(CLOCKS_PER_SEC * ((double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000)); 
+}
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/fret/fretMain.c b/src/opt/fret/fretMain.c
index a9ba8c4b..9a981a8e 100644
--- a/src/opt/fret/fretMain.c
+++ b/src/opt/fret/fretMain.c
@@ -1115,6 +1115,8 @@ static Abc_Ntk_t* Abc_FlowRetime_NtkDup( Abc_Ntk_t * pNtk ) {
   int i, j;
 
   pNtkCopy = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
+  pNtkCopy->pName = Extra_UtilStrsav(pNtk->pName);
+  pNtkCopy->pSpec = Extra_UtilStrsav(pNtk->pSpec);
 
   // copy each object
   Abc_NtkForEachObj( pNtk, pObj, i) {