Version abc80301

20 files changed, 546 insertions, 78 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 86cc7e62..1d5195c7 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -201,9 +201,10 @@ struct Abc_Ntk_t_
     Abc_Ntk_t *       pExdc;         // the EXDC network (if given)
     void *            pExcare;       // the EXDC network (if given)
     void *            pData;         // misc
-    Abc_Ntk_t *       pCopy;
+    Abc_Ntk_t *       pCopy;         // copy of this network
     Hop_Man_t *       pHaig;         // history AIG
     float *           pLutTimes;     // arrivals/requireds/slacks using LUT-delay model
+    Vec_Ptr_t *       vOnehots;      // names of one-hot-encoded registers
     // node attributes
     Vec_Ptr_t *       vAttrs;        // managers of various node attributes (node functionality, global BDDs, etc)
 };
@@ -328,10 +329,10 @@ static inline Abc_Obj_t * Abc_NtkAssert( Abc_Ntk_t * pNtk, int i )   { return (A
 static inline Abc_Obj_t * Abc_NtkBox( Abc_Ntk_t * pNtk, int i )      { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vBoxes, i );  }
 
 // working with complemented attributes of objects
-static inline bool        Abc_ObjIsComplement( Abc_Obj_t * p )       { return (bool)((unsigned long)p & (unsigned long)01);             }
-static inline Abc_Obj_t * Abc_ObjRegular( Abc_Obj_t * p )            { return (Abc_Obj_t *)((unsigned long)p & ~(unsigned long)01);     }
-static inline Abc_Obj_t * Abc_ObjNot( Abc_Obj_t * p )                { return (Abc_Obj_t *)((unsigned long)p ^  (unsigned long)01);     }
-static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c )     { return (Abc_Obj_t *)((unsigned long)p ^  (unsigned long)(c!=0)); }
+static inline bool        Abc_ObjIsComplement( Abc_Obj_t * p )       { return (bool)((PORT_PTRUINT_T)p & (PORT_PTRUINT_T)01);             }
+static inline Abc_Obj_t * Abc_ObjRegular( Abc_Obj_t * p )            { return (Abc_Obj_t *)((PORT_PTRUINT_T)p & ~(PORT_PTRUINT_T)01);     }
+static inline Abc_Obj_t * Abc_ObjNot( Abc_Obj_t * p )                { return (Abc_Obj_t *)((PORT_PTRUINT_T)p ^  (PORT_PTRUINT_T)01);     }
+static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c )     { return (Abc_Obj_t *)((PORT_PTRUINT_T)p ^  (PORT_PTRUINT_T)(c!=0)); }
 
 // reading data members of the object
 static inline unsigned    Abc_ObjType( Abc_Obj_t * pObj )            { return pObj->Type;               }
@@ -441,9 +442,6 @@ static inline void *      Abc_ObjMvVar( Abc_Obj_t * pObj )              { return
 static inline int         Abc_ObjMvVarNum( Abc_Obj_t * pObj )           { return (Abc_NtkMvVar(pObj->pNtk) && Abc_ObjMvVar(pObj))? *((int*)Abc_ObjMvVar(pObj)) : 2;   }
 static inline void        Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_AttWriteEntry( (Vec_Att_t *)Abc_NtkMvVar(pObj->pNtk), pObj->Id, pV );                }
 
-// outputs the runtime in seconds
-#define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
-
 ////////////////////////////////////////////////////////////////////////
 ///                        ITERATORS                                 ///
 ////////////////////////////////////////////////////////////////////////
@@ -523,7 +521,7 @@ extern Abc_Obj_t *        Abc_AigMuxLookup( Abc_Aig_t * pMan, Abc_Obj_t * pC, Ab
 extern Abc_Obj_t *        Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
 extern Abc_Obj_t *        Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
 extern Abc_Obj_t *        Abc_AigMux( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * p1, Abc_Obj_t * p0 );
-extern Abc_Obj_t *        Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs );
+extern Abc_Obj_t *        Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs, int fImplic );
 extern void               Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool fUpdateLevel );
 extern void               Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld );
 extern void               Abc_AigRehash( Abc_Aig_t * pMan );
@@ -635,6 +633,7 @@ extern Vec_Int_t *        Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues );
 extern Abc_Obj_t *        Abc_NtkAddLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pDriver, Abc_InitType_t Init );
 extern void               Abc_NtkConvertDcLatches( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *        Abc_NtkConverLatchNamesIntoNumbers( Abc_Ntk_t * pNtk );
  /*=== abcLib.c ==========================================================*/
 extern Abc_Lib_t *        Abc_LibCreate( char * pName );
 extern void               Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk );
@@ -649,7 +648,7 @@ extern int                Abc_NodeMinimumBase( Abc_Obj_t * pNode );
 extern int                Abc_NtkRemoveDupFanins( Abc_Ntk_t * pNtk );
 extern int                Abc_NodeRemoveDupFanins( Abc_Obj_t * pNode );
 /*=== abcMiter.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize );
+extern Abc_Ntk_t *        Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic );
 extern void               Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * pNode );
 extern Abc_Ntk_t *        Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOr, int fCompl2 );
 extern Abc_Ntk_t *        Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues );
@@ -739,6 +738,7 @@ extern void               Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int
 extern void               Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
+extern void               Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk );
 extern void               Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode );
 extern void               Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, int fUseRealNames );
 extern void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 89026863..3cc4d59c 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -786,15 +786,23 @@ Abc_Obj_t * Abc_AigMiter_rec( Abc_Aig_t * pMan, Abc_Obj_t ** ppObjs, int nObjs )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
+Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs, int fImplic )
 {
     int i;
     if ( vPairs->nSize == 0 )
         return Abc_ObjNot( Abc_AigConst1(pMan->pNtkAig) );
     assert( vPairs->nSize % 2 == 0 );
     // go through the cubes of the node's SOP
-    for ( i = 0; i < vPairs->nSize; i += 2 )
-        vPairs->pArray[i/2] = Abc_AigXor( pMan, vPairs->pArray[i], vPairs->pArray[i+1] );
+    if ( fImplic )
+    {
+        for ( i = 0; i < vPairs->nSize; i += 2 )
+            vPairs->pArray[i/2] = Abc_AigAnd( pMan, vPairs->pArray[i], Abc_ObjNot(vPairs->pArray[i+1]) );
+    }
+    else
+    {
+        for ( i = 0; i < vPairs->nSize; i += 2 )
+            vPairs->pArray[i/2] = Abc_AigXor( pMan, vPairs->pArray[i], vPairs->pArray[i+1] );
+    }
     vPairs->nSize = vPairs->nSize/2;
     return Abc_AigMiter_rec( pMan, (Abc_Obj_t **)vPairs->pArray, vPairs->nSize );
 }
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 778581c2..4c6a7fb0 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -121,6 +121,8 @@ Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes
     // go through the PO nodes and call for each of them
     for ( i = 0; i < nNodes; i++ )
     {
+        if ( Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(ppNodes[i]) )
+            continue;
         if ( Abc_ObjIsCo(ppNodes[i]) )
         {
             Abc_NodeSetTravIdCurrent(ppNodes[i]);
diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index d96bbfac..4529d9f3 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -318,6 +318,58 @@ void Abc_NtkConvertDcLatches( Abc_Ntk_t * pNtk )
     printf( "The number of converted latches with DC values = %d.\n", Counter );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Transfors the array of latch names into that of latch numbers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkConverLatchNamesIntoNumbers( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vResult, * vNames;
+    Vec_Int_t * vNumbers;
+    Abc_Obj_t * pObj;
+    char * pName;
+    int i, k, Num;
+    if ( pNtk->vOnehots == NULL )
+        return NULL;
+    // set register numbers
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        pObj->pNext = (Abc_Obj_t *)i;
+    // add the numbers
+    vResult = Vec_PtrAlloc( Vec_PtrSize(pNtk->vOnehots) );
+    Vec_PtrForEachEntry( pNtk->vOnehots, vNames, i )
+    {
+        vNumbers = Vec_IntAlloc( Vec_PtrSize(vNames) );
+        Vec_PtrForEachEntry( vNames, pName, k )
+        {
+            Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BO );
+            if ( Num < 0 )
+                continue;
+            pObj = Abc_NtkObj( pNtk, Num );
+            if ( Abc_ObjFaninNum(pObj) != 1 || !Abc_ObjIsLatch(Abc_ObjFanin0(pObj)) )
+                continue;
+            Vec_IntPush( vNumbers, (int)pObj->pNext );
+        }
+        if ( Vec_IntSize( vNumbers ) > 1 )
+        {
+            Vec_PtrPush( vResult, vNumbers );
+printf( "Converted %d one-hot registers.\n", Vec_IntSize(vNumbers) );
+        }
+        else
+            Vec_IntFree( vNumbers );
+    }
+    // clean the numbers
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        pObj->pNext = NULL;
+    return vResult;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 5c565ce6..1e88859c 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -125,6 +125,8 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
     // transfer the names
 //    Abc_NtkTrasferNames( pNtk, pNtkNew );
     Abc_ManTimeDup( pNtk, pNtkNew );
+    if ( pNtk->vOnehots )
+        pNtkNew->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
     // check that the CI/CO/latches are copied correctly
     assert( Abc_NtkCiNum(pNtk)    == Abc_NtkCiNum(pNtkNew) );
     assert( Abc_NtkCoNum(pNtk)    == Abc_NtkCoNum(pNtkNew) );
@@ -520,7 +522,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNode
     int i, k;
 
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) );
-    assert( Abc_ObjIsNode(pNode) ); 
+    assert( Abc_ObjIsNode(pNode) || (Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(pNode))  ); 
     
     // start the network
     pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
@@ -1032,6 +1034,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     FREE( pNtk->pName );
     FREE( pNtk->pSpec );
     FREE( pNtk->pLutTimes );
+    if ( pNtk->vOnehots )
+        Vec_VecFree( (Vec_Vec_t *)pNtk->vOnehots );
     free( pNtk );
 }
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 99da9201..11ef85f9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -685,7 +685,7 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fPrintSccs = 1;
+    fPrintSccs = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF )
     {
@@ -736,17 +736,22 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
+    int fVerbose;
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -761,12 +766,16 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // print the nodes
-    Abc_NtkPrintFanio( pOut, pNtk );
+    if ( fVerbose )
+        Abc_NtkPrintFanio( pOut, pNtk );
+    else
+        Abc_NtkPrintFanioNew( pOut, pNtk );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_fanio [-h]\n" );
+    fprintf( pErr, "usage: print_fanio [-vh]\n" );
     fprintf( pErr, "\t        prints the statistics about fanins/fanouts of all nodes\n" );
+    fprintf( pErr, "\t-v    : toggles verbose way of printing the stats [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -2066,10 +2075,12 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
+    Abc_Obj_t * pObj;
     int c;
     int fAllNodes;
     int fRecord;
     int fCleanup;
+    int fComplOuts;
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -2079,8 +2090,9 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     fAllNodes = 0;
     fCleanup  = 1;
     fRecord   = 0;
+    fComplOuts= 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "acrh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "acrih" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2093,6 +2105,9 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             fRecord ^= 1;
             break;
+        case 'i':
+            fComplOuts ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -2113,16 +2128,20 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Strashing has failed.\n" );
         return 1;
     }
+    if ( fComplOuts )
+    Abc_NtkForEachCo( pNtkRes, pObj, c )
+        Abc_ObjXorFaninC( pObj, 0 );
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: strash [-acrh]\n" );
+    fprintf( pErr, "usage: strash [-acrih]\n" );
     fprintf( pErr, "\t        transforms combinational logic into an AIG\n" );
     fprintf( pErr, "\t-a    : toggles between using all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "DFS" );
     fprintf( pErr, "\t-c    : toggles cleanup to remove the dagling AIG nodes [default = %s]\n", fCleanup? "all": "DFS" );
-    fprintf( pErr, "\t-r    : enables using the record of AIG subgraphs [default = %s]\n", fRecord? "yes": "no" );
+    fprintf( pErr, "\t-r    : toggles using the record of AIG subgraphs [default = %s]\n", fRecord? "yes": "no" );
+    fprintf( pErr, "\t-i    : toggles complementing the COs of the AIG [default = %s]\n", fComplOuts? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -3281,20 +3300,21 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    pPars->nWinTfoLevs  =   2;
-    pPars->nFanoutsMax  =  10;
-    pPars->nDepthMax    =  20;
-    pPars->nDivMax      = 250;
-    pPars->nWinSizeMax  = 300;
-    pPars->nGrowthLevel =   0;
-    pPars->fResub       =   1;
-    pPars->fArea        =   0;
-    pPars->fMoreEffort  =   0;
-    pPars->fSwapEdge    =   0;
-    pPars->fVerbose     =   0;
-    pPars->fVeryVerbose =   0;
+    pPars->nWinTfoLevs  =    2;
+    pPars->nFanoutsMax  =   10;
+    pPars->nDepthMax    =   20;
+    pPars->nDivMax      =  250;
+    pPars->nWinSizeMax  =  300;
+    pPars->nGrowthLevel =    0;
+    pPars->nBTLimit     =10000;
+    pPars->fResub       =    1;
+    pPars->fArea        =    0;
+    pPars->fMoreEffort  =    0;
+    pPars->fSwapEdge    =    0;
+    pPars->fVerbose     =    0;
+    pPars->fVeryVerbose =    0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLraesvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCraesvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3353,6 +3373,17 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY ) 
                 goto usage;
             break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBTLimit < 0 ) 
+                goto usage;
+            break;
         case 'r':
             pPars->fResub ^= 1;
             break;
@@ -3398,13 +3429,14 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: mfs [-WFDML <num>] [-raesvh]\n" );
+    fprintf( pErr, "usage: mfs [-WFDMLC <num>] [-raesvh]\n" );
     fprintf( pErr, "\t           performs don't-care-based optimization of logic networks\n" );
     fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
     fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
     fprintf( pErr, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
     fprintf( pErr, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
     fprintf( pErr, "\t-L <num> : the max increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
+    fprintf( pErr, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
     fprintf( pErr, "\t-r       : toggle resubstitution and dc-minimization [default = %s]\n", pPars->fResub? "resub": "dc-min" );
     fprintf( pErr, "\t-a       : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
     fprintf( pErr, "\t-e       : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
@@ -4423,6 +4455,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int fCheck;
     int fComb;
+    int fImplic;
     int nPartSize;
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -4432,9 +4465,10 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     fComb  = 1;
     fCheck = 1;
+    fImplic = 0;
     nPartSize = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Pch" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Pcih" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4452,6 +4486,9 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             fComb ^= 1;
             break;
+        case 'i':
+            fImplic ^= 1;
+            break;
         default:
             goto usage;
         }
@@ -4463,7 +4500,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
 
     // compute the miter
-    pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, nPartSize );
+    pNtkRes = Abc_NtkMiter( pNtk1, pNtk2, fComb, nPartSize, fImplic );
     if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
     if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
 
@@ -4482,10 +4519,11 @@ usage:
         strcpy( Buffer, "unused" );
     else
         sprintf( Buffer, "%d", nPartSize );
-    fprintf( pErr, "usage: miter [-P num] [-ch] <file1> <file2>\n" );
+    fprintf( pErr, "usage: miter [-P num] [-cih] <file1> <file2>\n" );
     fprintf( pErr, "\t         computes the miter of the two circuits\n" );
     fprintf( pErr, "\t-P num : output partition size [default = %s]\n", Buffer );
-    fprintf( pErr, "\t-c     : computes combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" );
+    fprintf( pErr, "\t-c     : toggles deriving combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" );
+    fprintf( pErr, "\t-i     : toggles deriving implication miter (file1 => file2) [default = %s]\n", fImplic? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     fprintf( pErr, "\tfile1  : (optional) the file with the first network\n");
     fprintf( pErr, "\tfile2  : (optional) the file with the second network\n");
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 6f5138c8..d69a7097 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -85,7 +85,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
             printf( "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
             printf( "The don't-care are assumed to be 0. The result may not verify.\n" );
             printf( "Use command \"print_latch\" to see the init values of registers.\n" );
-            printf( "Use command \"init\" to change the values.\n" );
+            printf( "Use command \"zero\" to convert or \"init\" to change the values.\n" );
         }
     }
     // create the manager
@@ -97,6 +97,9 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
         pMan->nRegs = Abc_NtkLatchNum(pNtk);
         pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
 //        pMan->vFlopNums = NULL;
+//        pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
+        if ( pNtk->vOnehots )
+            pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
     }
     // transfer the pointers to the basic nodes
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
@@ -974,7 +977,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVe
     if ( pNtk2 != NULL )
     {
         // get the miter of the two networks
-        pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
+        pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 );
         if ( pMiter == NULL )
         {
             printf( "Miter computation has failed.\n" );
@@ -1224,7 +1227,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim
     int RetValue;
  
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -1525,7 +1528,7 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
+Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
 {
     extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose );
     Abc_Ntk_t * pNtkAig;
@@ -1573,6 +1576,67 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
+{
+    Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter;
+    Abc_Obj_t * pObj;
+    int i;
+    if ( Abc_NtkCoNum(pNtkOn) != Abc_NtkCoNum(pNtkOff) )
+    {
+        printf( "Currently works only for networks with equal number of POs.\n" );
+        return NULL;
+    }
+    if ( Abc_NtkCoNum(pNtkOn) == 1 )
+        return Abc_NtkInterOne( pNtkOn, pNtkOff, fVerbose );
+    // start the new newtork
+    pNtkInter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+    pNtkInter->pName = Extra_UtilStrsav(pNtkOn->pName);
+    Abc_NtkForEachPi( pNtkOn, pObj, i )
+        Abc_NtkDupObj( pNtkInter, pObj, 1 );
+    // process each POs separately
+    Abc_NtkForEachCo( pNtkOn, pObj, i )
+    {
+        pNtkOn1 = Abc_NtkCreateCone( pNtkOn, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 1 );
+        if ( Abc_ObjFaninC0(pObj) )
+            Abc_ObjXorFaninC( Abc_NtkPo(pNtkOn1, 0), 0 );
+
+        pObj   = Abc_NtkCo(pNtkOff, i);
+        pNtkOff1 = Abc_NtkCreateCone( pNtkOff, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 1 );
+        if ( Abc_ObjFaninC0(pObj) )
+            Abc_ObjXorFaninC( Abc_NtkPo(pNtkOff1, 0), 0 );
+
+        if ( Abc_NtkNodeNum(pNtkOn1) == 0 )
+            pNtkInter1 = Abc_NtkDup( pNtkOn1 );
+        else if ( Abc_NtkNodeNum(pNtkOff1) == 0 )
+        {
+            pNtkInter1 = Abc_NtkDup( pNtkOff1 );
+            Abc_ObjXorFaninC( Abc_NtkPo(pNtkInter1, 0), 0 );
+        }
+        else
+            pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, fVerbose );
+        Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
+
+        Abc_NtkDelete( pNtkOn1 );
+        Abc_NtkDelete( pNtkOff1 );
+        Abc_NtkDelete( pNtkInter1 );
+    }
+    // return the network
+    if ( !Abc_NtkCheck( pNtkInter ) )
+        fprintf( stdout, "Abc_NtkAttachBottom(): Network check has failed.\n" );
+    return pNtkInter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Interplates two networks.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose )
 {
 //    extern Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize );
diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
index 0b66c476..7c18ca2c 100644
--- a/src/base/abci/abcGen.c
+++ b/src/base/abci/abcGen.c
@@ -1,12 +1,12 @@
 /**CFile****************************************************************
 
-  FileName    [abc_.c]
+  FileName    [abcGen.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
   PackageName [Network and node package.]
 
-  Synopsis    []
+  Synopsis    [Procedures to generate various type of circuits.]
 
   Author      [Alan Mishchenko]
   
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: abcGen.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -545,6 +545,60 @@ void Abc_GenOneHot( char * pFileName, int nVars )
     fclose( pFile );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Generates structure of L K-LUTs implementing an N-var function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_GenOneHotIntervals( char * pFileName, int nPis, int nRegs, Vec_Ptr_t * vOnehots )
+{
+    Vec_Int_t * vLine;
+    FILE * pFile;
+    int i, j, k, iReg1, iReg2, Counter, Counter2, nDigitsIn, nDigitsOut;
+    pFile = fopen( pFileName, "w" );
+    fprintf( pFile, "# One-hotness with %d vars and %d regs generated by ABC on %s\n", nPis, nRegs, Extra_TimeStamp() );
+    fprintf( pFile, "# Used %d intervals of 1-hot registers: { ", Vec_PtrSize(vOnehots) );
+    Counter = 0;
+    Vec_PtrForEachEntry( vOnehots, vLine, k )
+    {
+        fprintf( pFile, "%d ", Vec_IntSize(vLine) );
+        Counter += Vec_IntSize(vLine) * (Vec_IntSize(vLine) - 1) / 2;
+    }
+    fprintf( pFile, "}\n" );
+    fprintf( pFile, ".model 1hot_%dvars_%dregs\n", nPis, nRegs );
+    fprintf( pFile, ".inputs" );
+    nDigitsIn = Extra_Base10Log( nPis+nRegs );
+    for ( i = 0; i < nPis+nRegs; i++ )
+        fprintf( pFile, " i%0*d", nDigitsIn, i );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, ".outputs" );
+    nDigitsOut = Extra_Base10Log( Counter );
+    for ( i = 0; i < Counter; i++ )
+        fprintf( pFile, " o%0*d", nDigitsOut, i );
+    fprintf( pFile, "\n" );
+    Counter2 = 0;
+    Vec_PtrForEachEntry( vOnehots, vLine, k )
+    {
+        Vec_IntForEachEntry( vLine, iReg1, i )
+        Vec_IntForEachEntryStart( vLine, iReg2, j, i+1 )
+        {
+            fprintf( pFile, ".names i%0*d i%0*d o%0*d\n", nDigitsIn, nPis+iReg1, nDigitsIn, nPis+iReg2, nDigitsOut, Counter2 ); 
+            fprintf( pFile, "11 0\n" ); 
+            Counter2++;
+        }
+    }
+    assert( Counter == Counter2 );
+    fprintf( pFile, ".end\n" ); 
+    fprintf( pFile, "\n" ); 
+    fclose( pFile );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index a054a474..3e3c9580 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -24,10 +24,10 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize );
+static Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic );
 static void        Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize );
 static void        Abc_NtkMiterAddOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter );
-static void        Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize );
+static void        Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize, int fImplic );
 static void        Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame );
 
 // to be exported 
@@ -50,7 +50,7 @@ static void        Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, i
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize )
+Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic )
 {
     Abc_Ntk_t * pTemp = NULL;
     int fRemove1, fRemove2;
@@ -63,7 +63,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int n
     fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0, 0));
     fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0));
     if ( pNtk1 && pNtk2 )
-        pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb, nPartSize );
+        pTemp = Abc_NtkMiterInt( pNtk1, pNtk2, fComb, nPartSize, fImplic );
     if ( fRemove1 )  Abc_NtkDelete( pNtk1 );
     if ( fRemove2 )  Abc_NtkDelete( pNtk2 );
     return pTemp;
@@ -80,7 +80,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int n
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize )
+Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, int nPartSize, int fImplic )
 {
     char Buffer[1000];
     Abc_Ntk_t * pNtkMiter;
@@ -97,7 +97,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, in
     Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );
     Abc_NtkMiterAddOne( pNtk1, pNtkMiter );
     Abc_NtkMiterAddOne( pNtk2, pNtkMiter );
-    Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize );
+    Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize, fImplic );
     Abc_AigCleanup(pNtkMiter->pManFunc);
 
     // make sure that everything is okay
@@ -250,7 +250,7 @@ void Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, Abc_Obj_t * p
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize )
+void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb, int nPartSize, int fImplic )
 {
     Vec_Ptr_t * vPairs;
     Abc_Obj_t * pMiter, * pNode;
@@ -285,7 +285,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
     // add the miter
     if ( nPartSize <= 0 )
     {
-        pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs );
+        pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs, fImplic );
         Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter );
         Vec_PtrFree( vPairs );
     }
@@ -309,7 +309,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
                 Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur  ) );
                 Vec_PtrPush( vPairsPart, Vec_PtrEntry(vPairs, 2*iCur+1) );
             }
-            pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairsPart );
+            pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairsPart, fImplic );
             pNode = Abc_NtkCreatePo( pNtkMiter );
             Abc_ObjAddFanin( pNode, pMiter );
             // assign the name to the node
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 239b155c..e5f028fe 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -468,6 +468,118 @@ void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk )
     Vec_IntFree( vFanins );
     Vec_IntFree( vFanouts );
 }
+/**Function*************************************************************
+
+  Synopsis    [Prints the distribution of fanins/fanouts in the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintFanioNew( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    char Buffer[100];
+    Abc_Obj_t * pNode;
+    Vec_Int_t * vFanins, * vFanouts;
+    int nFanins, nFanouts, nFaninsMax, nFanoutsMax, nFaninsAll, nFanoutsAll;
+    int i, k, nSizeMax;
+
+    // determine the largest fanin and fanout
+    nFaninsMax = nFanoutsMax = 0;
+    nFaninsAll = nFanoutsAll = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        nFanins  = Abc_ObjFaninNum(pNode);
+        if ( Abc_NtkIsNetlist(pNtk) )
+            nFanouts = Abc_ObjFanoutNum( Abc_ObjFanout0(pNode) );
+        else
+            nFanouts = Abc_ObjFanoutNum(pNode);
+        nFaninsAll  += nFanins;
+        nFanoutsAll += nFanouts;
+        nFaninsMax   = ABC_MAX( nFaninsMax, nFanins );
+        nFanoutsMax  = ABC_MAX( nFanoutsMax, nFanouts );
+    }
+
+    // allocate storage for fanin/fanout numbers
+    nSizeMax = ABC_MAX( 10 * (Extra_Base10Log(nFaninsMax) + 1), 10 * (Extra_Base10Log(nFanoutsMax) + 1) );
+    vFanins  = Vec_IntStart( nSizeMax );
+    vFanouts = Vec_IntStart( nSizeMax );
+
+    // count the number of fanins and fanouts
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        nFanins  = Abc_ObjFaninNum(pNode);
+        if ( Abc_NtkIsNetlist(pNtk) )
+            nFanouts = Abc_ObjFanoutNum( Abc_ObjFanout0(pNode) );
+        else
+            nFanouts = Abc_ObjFanoutNum(pNode);
+//            nFanouts = Abc_NodeMffcSize(pNode);
+
+        if ( nFanins < 10 )
+            Vec_IntAddToEntry( vFanins, nFanins, 1 );
+        else if ( nFanins < 100 )
+            Vec_IntAddToEntry( vFanins, 10 + nFanins/10, 1 );
+        else if ( nFanins < 1000 )
+            Vec_IntAddToEntry( vFanins, 20 + nFanins/100, 1 );
+        else if ( nFanins < 10000 )
+            Vec_IntAddToEntry( vFanins, 30 + nFanins/1000, 1 );
+        else if ( nFanins < 100000 )
+            Vec_IntAddToEntry( vFanins, 40 + nFanins/10000, 1 );
+        else if ( nFanins < 1000000 )
+            Vec_IntAddToEntry( vFanins, 50 + nFanins/100000, 1 );
+        else if ( nFanins < 10000000 )
+            Vec_IntAddToEntry( vFanins, 60 + nFanins/1000000, 1 );
+
+        if ( nFanouts < 10 )
+            Vec_IntAddToEntry( vFanouts, nFanouts, 1 );
+        else if ( nFanouts < 100 )
+            Vec_IntAddToEntry( vFanouts, 10 + nFanouts/10, 1 );
+        else if ( nFanouts < 1000 )
+            Vec_IntAddToEntry( vFanouts, 20 + nFanouts/100, 1 );
+        else if ( nFanouts < 10000 )
+            Vec_IntAddToEntry( vFanouts, 30 + nFanouts/1000, 1 );
+        else if ( nFanouts < 100000 )
+            Vec_IntAddToEntry( vFanouts, 40 + nFanouts/10000, 1 );
+        else if ( nFanouts < 1000000 )
+            Vec_IntAddToEntry( vFanouts, 50 + nFanouts/100000, 1 );
+        else if ( nFanouts < 10000000 )
+            Vec_IntAddToEntry( vFanouts, 60 + nFanouts/1000000, 1 );
+    }
+
+    fprintf( pFile, "The distribution of fanins and fanouts in the network:\n" );
+    fprintf( pFile, "         Number   Nodes with fanin  Nodes with fanout\n" );
+    for ( k = 0; k < nSizeMax; k++ )
+    {
+        if ( vFanins->pArray[k] == 0 && vFanouts->pArray[k] == 0 )
+            continue;
+        if ( k < 10 )
+            fprintf( pFile, "%15d : ", k );
+        else
+        {
+            sprintf( Buffer, "%d - %d", (int)pow(10, k/10) * (k%10), (int)pow(10, k/10) * (k%10+1) - 1 ); 
+            fprintf( pFile, "%15s : ", Buffer );
+        }
+        if ( vFanins->pArray[k] == 0 )
+            fprintf( pFile, "              " );
+        else
+            fprintf( pFile, "%12d  ", vFanins->pArray[k] );
+        fprintf( pFile, "    " );
+        if ( vFanouts->pArray[k] == 0 )
+            fprintf( pFile, "              " );
+        else
+            fprintf( pFile, "%12d  ", vFanouts->pArray[k] );
+        fprintf( pFile, "\n" );
+    }
+    Vec_IntFree( vFanins );
+    Vec_IntFree( vFanouts );
+
+    fprintf( pFile, "Fanins: Max = %d. Ave = %.2f.  Fanouts: Max = %d. Ave =  %.2f.\n", 
+        nFaninsMax,  1.0*nFaninsAll/Abc_NtkNodeNum(pNtk), 
+        nFanoutsMax, 1.0*nFanoutsAll/Abc_NtkNodeNum(pNtk)  );
+}
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c
index 0f2bd72f..24981d1c 100644
--- a/src/base/abci/abcQuant.c
+++ b/src/base/abci/abcQuant.c
@@ -187,7 +187,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
         Vec_PtrPush( vPairs, Abc_ObjChild0Copy(pObj) );
         Vec_PtrPush( vPairs, Abc_NtkPi(pNtkNew, i+nLatches) );
     }
-    pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs );
+    pMiter = Abc_AigMiter( pNtkNew->pManFunc, vPairs, 0 );
     Vec_PtrFree( vPairs );
     // add the primary output
     Abc_ObjAddFanin( Abc_NtkPo(pNtkNew,0), Abc_ObjNot(pMiter) );
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index 92adc718..80d234f1 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -354,7 +354,7 @@ int Abc_NtkRRProve( Abc_RRMan_t * p )
     Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy->pCopy, p->pFanin->pCopy->pCopy, p->pFanout? p->pFanout->pCopy->pCopy : NULL );
     if ( !Abc_NtkIsDfsOrdered(pWndCopy) )
         Abc_NtkReassignIds(pWndCopy);
-    p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0 );
+    p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1, 0, 0 );
     Abc_NtkDelete( pWndCopy );
 clk = clock();
     RetValue  = Abc_NtkMiterProve( &p->pMiter, p->pParams );
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index c77f8dea..744d9c95 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -260,7 +260,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
         {
             Abc_NtkDupObj( pNtk1, pObj, 0 );
             Abc_ObjAddFanin( pObj->pCopy, Abc_ObjChild0Copy(pObj) );
-            Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj->pCopy), NULL );
+            Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), NULL );
         }
     }
     else
@@ -271,6 +271,8 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
         Abc_NtkForEachCo( pNtk2, pObj, i )
         {
             iNodeId = Nm_ManFindIdByNameTwoTypes( pNtk1->pManName, Abc_ObjName(pObj), ABC_OBJ_PO, ABC_OBJ_BI );
+//            if ( iNodeId < 0 )
+//                continue;
             assert( iNodeId >= 0 );
             pObjOld = Abc_NtkObj( pNtk1, iNodeId );
             // derive the new driver
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 9c9bbcfd..1d72a767 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -52,7 +52,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     int RetValue;
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -120,7 +120,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     int RetValue;
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -225,7 +225,7 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
     assert( nPartSize > 0 );
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, nPartSize );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, nPartSize, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -342,7 +342,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
     //    pParams->fVerbose = 1;
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 1 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 1, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -456,7 +456,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     int RetValue;
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
@@ -538,7 +538,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr
     int RetValue;
 
     // get the miter of the two networks
-    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
+    pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0, 0 );
     if ( pMiter == NULL )
     {
         printf( "Miter computation has failed.\n" );
diff --git a/src/base/io/io.c b/src/base/io/io.c
index fe88a285..628ef2b9 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -722,14 +722,19 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     char * pFileName;
     int fCheck;
+    int fZeros;
     int c;
 
+    fZeros = 0;
     fCheck = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "zch" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'z':
+                fZeros ^= 1;
+                break;
             case 'c':
                 fCheck ^= 1;
                 break;
@@ -744,7 +749,20 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
     // get the input file name
     pFileName = argv[globalUtilOptind];
     // read the file using the corresponding file reader
-    pNtk = Io_Read( pFileName, IO_FILE_PLA, fCheck );
+    if ( fZeros )
+    {
+        Abc_Ntk_t * pTemp;
+        pNtk = Io_ReadPla( pFileName, fZeros, fCheck );
+        if ( pNtk == NULL )
+        {
+            printf( "Reading PLA file has failed.\n" );
+            return 1;
+        }
+        pNtk = Abc_NtkToLogic( pTemp = pNtk );
+        Abc_NtkDelete( pTemp );
+    }
+    else
+        pNtk = Io_Read( pFileName, IO_FILE_PLA, fCheck );
     if ( pNtk == NULL )
         return 1;
     // replace the current network
@@ -752,8 +770,9 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: read_pla [-ch] <file>\n" );
+    fprintf( pAbc->Err, "usage: read_pla [-zch] <file>\n" );
     fprintf( pAbc->Err, "\t         read the network in PLA\n" );
+    fprintf( pAbc->Err, "\t-z     : toggle reading on-set and off-set [default = %s]\n", fZeros? "off-set":"on-set" );
     fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
     fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
     fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 126de332..eea76efe 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -83,7 +83,7 @@ extern Abc_Ntk_t *        Io_ReadEdif( char * pFileName, int fCheck );
 /*=== abcReadEqn.c ============================================================*/
 extern Abc_Ntk_t *        Io_ReadEqn( char * pFileName, int fCheck );
 /*=== abcReadPla.c ============================================================*/
-extern Abc_Ntk_t *        Io_ReadPla( char * pFileName, int fCheck );
+extern Abc_Ntk_t *        Io_ReadPla( char * pFileName, int fZeros, int fCheck );
 /*=== abcReadVerilog.c ========================================================*/
 extern Abc_Ntk_t *        Io_ReadVerilog( char * pFileName, int fCheck );
 /*=== abcWriteAiger.c =========================================================*/
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 8a1fe309..84378024 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -49,6 +49,7 @@ struct Io_MvMod_t_
     Vec_Ptr_t *          vResets;      // .reset lines
     Vec_Ptr_t *          vNames;       // .names lines
     Vec_Ptr_t *          vSubckts;     // .subckt lines
+    Vec_Ptr_t *          vOnehots;     // .onehot lines
     Vec_Ptr_t *          vMvs;         // .mv lines
     int                  fBlackBox;    // indicates blackbox model
     // the resulting network
@@ -97,6 +98,7 @@ static int               Io_MvParseLineInputs( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineOutputs( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine );
+static Vec_Int_t *       Io_MvParseLineOnehot( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineMv( Io_MvMod_t * p, char * pLine );
 static int               Io_MvParseLineNamesMv( Io_MvMod_t * p, char * pLine, int fReset );
 static int               Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine );
@@ -295,6 +297,7 @@ static Io_MvMod_t * Io_MvModAlloc()
     p->vResets  = Vec_PtrAlloc( 512 );
     p->vNames   = Vec_PtrAlloc( 512 );
     p->vSubckts = Vec_PtrAlloc( 512 );
+    p->vOnehots = Vec_PtrAlloc( 512 );
     p->vMvs     = Vec_PtrAlloc( 512 );
     return p;
 }
@@ -320,6 +323,7 @@ static void Io_MvModFree( Io_MvMod_t * p )
     Vec_PtrFree( p->vResets );
     Vec_PtrFree( p->vNames );
     Vec_PtrFree( p->vSubckts );
+    Vec_PtrFree( p->vOnehots );
     Vec_PtrFree( p->vMvs );
     free( p );
 }
@@ -597,6 +601,8 @@ static void Io_MvReadPreparse( Io_MvMan_t * p )
             Vec_PtrPush( p->pLatest->vOutputs, pCur );
         else if ( !strncmp(pCur, "subckt", 6) )
             Vec_PtrPush( p->pLatest->vSubckts, pCur );
+        else if ( !strncmp(pCur, "onehot", 6) )
+            Vec_PtrPush( p->pLatest->vOnehots, pCur );
         else if ( p->fBlifMv && !strncmp(pCur, "mv", 2) )
             Vec_PtrPush( p->pLatest->vMvs, pCur );
         else if ( !strncmp(pCur, "blackbox", 8) )
@@ -743,6 +749,42 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
                 return NULL;
         // finalize the network
         Abc_NtkFinalizeRead( pMod->pNtk );
+        // read the one-hotness lines
+        if ( Vec_PtrSize(pMod->vOnehots) > 0 )
+        {
+            Vec_Int_t * vLine; 
+            Abc_Obj_t * pObj;
+            // set register numbers
+            Abc_NtkForEachLatch( pMod->pNtk, pObj, k )
+                pObj->pNext = (Abc_Obj_t *)k;
+            // derive register
+            pMod->pNtk->vOnehots = Vec_PtrAlloc( Vec_PtrSize(pMod->vOnehots) );
+            Vec_PtrForEachEntry( pMod->vOnehots, pLine, k )
+            {
+                vLine = Io_MvParseLineOnehot( pMod, pLine );
+                if ( vLine == NULL )
+                    return NULL;
+                Vec_PtrPush( pMod->pNtk->vOnehots, vLine );
+//                printf( "Parsed %d one-hot registers.\n", Vec_IntSize(vLine) );
+            }
+            // reset register numbers
+            Abc_NtkForEachLatch( pMod->pNtk, pObj, k )
+                pObj->pNext = NULL;
+            // print the result
+            printf( "Parsed %d groups of 1-hot registers: { ", Vec_PtrSize(pMod->pNtk->vOnehots) );
+            Vec_PtrForEachEntry( pMod->pNtk->vOnehots, vLine, k )
+                printf( "%d ", Vec_IntSize(vLine) );
+            printf( "}\n" );
+            printf( "The total number of 1-hot registers = %d. (%.2f %%)\n", 
+                Vec_VecSizeSize( (Vec_Vec_t *)pMod->pNtk->vOnehots ), 
+                100.0 * Vec_VecSizeSize( (Vec_Vec_t *)pMod->pNtk->vOnehots ) / Abc_NtkLatchNum(pMod->pNtk) );
+            {
+                extern void Abc_GenOneHotIntervals( char * pFileName, int nPis, int nRegs, Vec_Ptr_t * vOnehots );
+                char * pFileName = Extra_FileNameGenericAppend( pMod->pMan->pFileName, "_1h.blif" );
+                Abc_GenOneHotIntervals( pFileName, Abc_NtkPiNum(pMod->pNtk), Abc_NtkLatchNum(pMod->pNtk), pMod->pNtk->vOnehots );
+                printf( "One-hotness condition is written into file \"%s\".\n", pFileName );
+            }
+        }
     }
     if ( p->nNDnodes )
 //        printf( "Warning: The parser added %d PIs to replace non-deterministic nodes.\n", p->nNDnodes );
@@ -995,6 +1037,63 @@ static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Parses the subckt line.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Vec_Int_t * Io_MvParseLineOnehot( Io_MvMod_t * p, char * pLine )
+{
+    Vec_Ptr_t * vTokens = p->pMan->vTokens;
+//    Vec_Ptr_t * vResult;
+    Vec_Int_t * vResult;
+    Abc_Obj_t * pNet, * pTerm;
+    char * pToken;
+    int nEquals, i;
+
+    // split the line into tokens
+    nEquals = Io_MvCountChars( pLine, '=' );
+    Io_MvSplitIntoTokensAndClear( vTokens, pLine, '\0', '=' );
+    pToken = Vec_PtrEntry(vTokens,0);
+    assert( !strcmp(pToken, "onehot") );
+
+    // iterate through the register names
+//    vResult = Vec_PtrAlloc( Vec_PtrSize(vTokens) );
+    vResult = Vec_IntAlloc( Vec_PtrSize(vTokens) );
+    Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 )
+    {
+        // check if this register exists
+        pNet = Abc_NtkFindNet( p->pNtk, pToken );
+        if ( pNet == NULL )
+        {
+            sprintf( p->pMan->sError, "Line %d: Signal with name \"%s\" does not exist in the model \"%s\".", 
+                Io_MvGetLine(p->pMan, pToken), pToken, Abc_NtkName(p->pNtk) );
+            return NULL;
+        }
+        // check if this is register output net
+        pTerm = Abc_ObjFanin0( pNet );
+        if ( pTerm == NULL || Abc_ObjFanin0(pTerm) == NULL || !Abc_ObjIsLatch(Abc_ObjFanin0(pTerm)) )
+        {
+            sprintf( p->pMan->sError, "Line %d: Signal with name \"%s\" is not a register in the model \"%s\".", 
+                Io_MvGetLine(p->pMan, pToken), pToken, Abc_NtkName(p->pNtk) );
+            return NULL;
+        }
+        // save register name
+//        Vec_PtrPush( vResult, Abc_ObjName(pNet) );
+        Vec_IntPush( vResult, (int)Abc_ObjFanin0(pTerm)->pNext );
+//        printf( "%d(%d) ", (int)Abc_ObjFanin0(pTerm)->pNext, ((int)Abc_ObjFanin0(pTerm)->pData) -1 );
+        printf( "%d", ((int)Abc_ObjFanin0(pTerm)->pData)-1 );
+    }
+    printf( "\n" );
+    return vResult;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c
index fdfdb4f6..288c3704 100644
--- a/src/base/io/ioReadPla.c
+++ b/src/base/io/ioReadPla.c
@@ -24,7 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p );
+static Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -41,7 +41,7 @@ static Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck )
+Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fCheck )
 {
     Extra_FileReader_t * p;
     Abc_Ntk_t * pNtk;
@@ -52,7 +52,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck )
         return NULL;
 
     // read the network
-    pNtk = Io_ReadPlaNetwork( p );
+    pNtk = Io_ReadPlaNetwork( p, fZeros );
     Extra_FileReaderFree( p );
     if ( pNtk == NULL )
         return NULL;
@@ -77,7 +77,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fCheck )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p )
+Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
 {
     ProgressBar * pProgress;
     Vec_Ptr_t * vTokens;
@@ -205,12 +205,26 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p )
                 Abc_NtkDelete( pNtk );
                 return NULL;
             }
-            for ( i = 0; i < nOutputs; i++ )
+            if ( fZeros )
             {
-                if ( pCubeOut[i] == '1' )
+                for ( i = 0; i < nOutputs; i++ )
+                {
+                    if ( pCubeOut[i] == '0' )
+                    {
+                        Vec_StrAppend( ppSops[i], pCubeIn );
+                        Vec_StrAppend( ppSops[i], " 1\n" );
+                    }
+                }
+            }
+            else
+            {
+                for ( i = 0; i < nOutputs; i++ )
                 {
-                    Vec_StrAppend( ppSops[i], pCubeIn );
-                    Vec_StrAppend( ppSops[i], " 1\n" );
+                    if ( pCubeOut[i] == '1' )
+                    {
+                        Vec_StrAppend( ppSops[i], pCubeIn );
+                        Vec_StrAppend( ppSops[i], " 1\n" );
+                    }
                 }
             }
             nCubes++;
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 4f9f2e9f..51a00274 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -134,7 +134,7 @@ Abc_Ntk_t * Io_ReadNetlist( char * pFileName, Io_FileType_t FileType, int fCheck
     else if ( FileType == IO_FILE_EQN )
         pNtk = Io_ReadEqn( pFileName, fCheck );
     else if ( FileType == IO_FILE_PLA )
-        pNtk = Io_ReadPla( pFileName, fCheck );
+        pNtk = Io_ReadPla( pFileName, 0, fCheck );
     else if ( FileType == IO_FILE_VERILOG )
         pNtk = Io_ReadVerilog( pFileName, fCheck );
     else 
diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c
index 58cc33ec..1f090cf4 100644
--- a/src/base/main/mainUtils.c
+++ b/src/base/main/mainUtils.c
@@ -21,7 +21,7 @@
 #include "mainInt.h"
 
 #ifndef _WIN32
-#include "readline/readline.h"
+#include <readline/readline.h>
 #endif
 
 ////////////////////////////////////////////////////////////////////////