Version abc71216

29 files changed, 3727 insertions, 234 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index b2e0293c..03574655 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -404,7 +404,7 @@ extern void            Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig
 extern void            Aig_ManFanoutStart( Aig_Man_t * p );
 extern void            Aig_ManFanoutStop( Aig_Man_t * p );
 /*=== aigFrames.c ==========================================================*/
-extern Aig_Man_t *     Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, Aig_Obj_t *** ppObjMap );
+extern Aig_Man_t *     Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t *** ppObjMap );
 /*=== aigHaig.c ==========================================================*/
 extern void            Aig_ManHaigRecord( Aig_Man_t * p );
 /*=== aigMan.c ==========================================================*/
diff --git a/src/aig/aig/aigFrames.c b/src/aig/aig/aigFrames.c
index dc3efe28..4a3b0c7c 100644
--- a/src/aig/aig/aigFrames.c
+++ b/src/aig/aig/aigFrames.c
@@ -45,7 +45,7 @@ static inline Aig_Obj_t * Aig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Ai
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, Aig_Obj_t *** ppObjMap )
+Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t *** ppObjMap )
 {
     Aig_Man_t * pFrames;
     Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
@@ -101,7 +101,7 @@ Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int
     }
     if ( fOuts )
     {
-        for ( f = 0; f < nFs; f++ )
+        for ( f = fEnlarge?nFs-1:0; f < nFs; f++ )
             Aig_ManForEachPoSeq( pAig, pObj, i )
             {
                 pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,f) );
@@ -113,7 +113,7 @@ Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int
         pFrames->nRegs = pAig->nRegs;
         Aig_ManForEachLiSeq( pAig, pObj, i )
         {
-            pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,nFs-1) );
+            pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFs,pObj,fEnlarge?0:nFs-1) );
             Aig_ObjSetFrames( pObjMap, nFs, pObj, nFs-1, pObjNew );
         }
     }
diff --git a/src/aig/fra/fraClau.c b/src/aig/fra/fraClau.c
index ea8406c7..fc239a40 100644
--- a/src/aig/fra/fraClau.c
+++ b/src/aig/fra/fraClau.c
@@ -227,7 +227,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
     p->vCexBmc   = Vec_IntAlloc( Aig_ManRegNum(pMan) );
 
     // derive two timeframes to be checked
-    pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, NULL ); // nFrames, fInit, fOuts, fRegs
+    pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, 0, NULL ); // nFrames, fInit, fOuts, fRegs
 //Aig_ManShow( pFramesMain, 0, NULL );
     assert( Aig_ManPoNum(pFramesMain) == 2 );
     Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output
@@ -245,14 +245,14 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
 */
 
     // derive one timeframe to be checked
-    pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, NULL );
+    pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, 0, NULL );
     assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) );
     pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) );
     p->pSatTest = Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 );
     p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest );
 
     // derive one timeframe to be checked for BMC
-    pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, NULL );
+    pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, 0, NULL );
 //Aig_ManShow( pFramesBmc, 0, NULL );
     assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
     pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) );
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index 8024431e..e3ac9aa3 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -30,12 +30,16 @@ typedef struct Clu_Man_t_    Clu_Man_t;
 struct Clu_Man_t_
 {
     // parameters
-    int              nFrames;
-    int              nClausesMax;
-    int              fVerbose;
+    int              nFrames;        // the K of the K-step induction
+    int              nPref;          // the number of timeframes to skip  
+    int              nClausesMax;    // the max number of 4-clauses to consider
+    int              fVerbose;       
     int              fVeryVerbose;
-    int              nSimWords;
-    int              nSimFrames;
+    // internal parameters
+    int              nSimWords;      // the number of simulation words
+    int              nSimWordsPref;  // the number of simulation words in the prefix
+    int              nSimFrames;     // the number of frames to simulate 
+    int              nBTLimit;       // the largest number of backtracks (0 = infinite)
     // the network
     Aig_Man_t *      pAig;
     // SAT solvers
@@ -43,8 +47,6 @@ struct Clu_Man_t_
     sat_solver *     pSatBmc;
     // CNF for the test solver
     Cnf_Dat_t *      pCnf;
-    // the counter example
-    Vec_Int_t *      vValues;
     // clauses
     Vec_Int_t *      vLits;
     Vec_Int_t *      vClauses;
@@ -74,35 +76,17 @@ struct Clu_Man_t_
 int Fra_ClausRunBmc( Clu_Man_t * p )
 {
     Aig_Obj_t * pObj;
-    int * pLits;
-    int nBTLimit = 0;
-    int i, RetValue;
-    pLits = ALLOC( int, p->nFrames + 1 );
+    int Lits[2], nLitsTot, RetValue, i;
     // set the output literals
+    nLitsTot = 2 * p->pCnf->nVars;
     pObj = Aig_ManPo(p->pAig, 0);
-    for ( i = 0; i < p->nFrames; i++ )
-        pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); 
-    // try to solve the problem
-//    sat_solver_act_var_clear( p->pSatBmc );
-//    RetValue = sat_solver_solve( p->pSatBmc, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-    for ( i = 0; i < p->nFrames; i++ )
+    for ( i = 0; i < p->nPref + p->nFrames; i++ )
     {
-        RetValue = sat_solver_solve( p->pSatBmc, pLits + i, pLits + i + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); 
+        RetValue = sat_solver_solve( p->pSatBmc, Lits, Lits + 1, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
         if ( RetValue != l_False )
-        {
-            free( pLits );
             return 0;
-        }
     }
-    free( pLits );
-
-/*
-    // get the counter-example
-    assert( RetValue == l_True );
-    nVarsTot = p->nFrames * p->pCnf->nVars;
-    Aig_ManForEachObj( p->pAig, pObj, i )
-        Vec_IntWriteEntry( p->vValues, i, sat_solver_var_value(p->pSatBmc, nVarsTot + p->pCnf->pVarNums[i]) );
-*/
     return 1;
 }
 
@@ -119,27 +103,21 @@ int Fra_ClausRunBmc( Clu_Man_t * p )
 ***********************************************************************/
 int Fra_ClausRunSat( Clu_Man_t * p )
 {
-    int nBTLimit = 0;
     Aig_Obj_t * pObj;
     int * pLits;
-    int i, nVarsTot, RetValue;
+    int i, RetValue;
     pLits = ALLOC( int, p->nFrames + 1 );
     // set the output literals
     pObj = Aig_ManPo(p->pAig, 0);
     for ( i = 0; i <= p->nFrames; i++ )
         pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], i != p->nFrames ); 
     // try to solve the problem
-//    sat_solver_act_var_clear( p->pSatMain );
-//    RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-    RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
     free( pLits );
     if ( RetValue == l_False )
         return 1;
     // get the counter-example
     assert( RetValue == l_True );
-    nVarsTot = p->nFrames * p->pCnf->nVars;
-    Aig_ManForEachObj( p->pAig, pObj, i )
-        Vec_IntWriteEntry( p->vValues, i, sat_solver_var_value(p->pSatMain, nVarsTot + p->pCnf->pVarNums[i]) );
     return 0;
 }
 
@@ -156,12 +134,11 @@ int Fra_ClausRunSat( Clu_Man_t * p )
 ***********************************************************************/
 int Fra_ClausRunSat0( Clu_Man_t * p )
 {
-    int nBTLimit = 0;
     Aig_Obj_t * pObj;
     int Lits[2], RetValue;
     pObj = Aig_ManPo(p->pAig, 0);
     Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); 
-    RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
     if ( RetValue == l_False )
         return 1;
     return 0;
@@ -169,86 +146,6 @@ int Fra_ClausRunSat0( Clu_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Processes the clauses.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-/*
-int Fra_ClausProcessClausesCut( Clu_Man_t * p, Dar_Cut_t * pCut )
-{
-    unsigned * pSimsC[4], * pSimsS[4];
-    int pLits[4];
-    int i, b, k, iMint, uMask, RetValue, nLeaves, nWordsTotal, nCounter;
-    // compute parameters
-    nLeaves = pCut->nLeaves;
-    nWordsTotal = p->pComb->nWordsTotal;
-    assert( nLeaves > 1 && nLeaves < 5 );
-    assert( nWordsTotal == p->pSeq->nWordsTotal );
-    // get parameters
-    for ( i = 0; i < (int)pCut->nLeaves; i++ )
-    {
-        pSimsC[i] = Fra_ObjSim( p->pComb, pCut->pLeaves[i] );
-        pSimsS[i] = Fra_ObjSim( p->pSeq,  pCut->pLeaves[i] );
-    }
-    // add combinational patterns
-    uMask = 0;
-    for ( i = 0; i < nWordsTotal; i++ )
-        for ( k = 0; k < 32; k++ )
-        {
-            iMint = 0;
-            for ( b = 0; b < nLeaves; b++ )
-                if ( pSimsC[b][i] & (1 << k) )
-                    iMint |= (1 << b);
-            uMask |= (1 << iMint);
-        }
-    // remove sequential patterns
-    for ( i = 0; i < nWordsTotal; i++ )
-        for ( k = 0; k < 32; k++ )
-        {
-            iMint = 0;
-            for ( b = 0; b < nLeaves; b++ )
-                if ( pSimsS[b][i] & (1 << k) )
-                    iMint |= (1 << b);
-            uMask &= ~(1 << iMint);
-        }
-    if ( uMask == 0 )
-        return 0;
-    // add clauses for the remaining patterns
-    nCounter = 0;
-    for ( i = 0; i < (1<<nLeaves); i++ )
-    {
-        if ( (uMask & (1 << i)) == 0 )
-            continue;
-        nCounter++;
-//        continue;
-
-        // add every third clause
-//        if ( (nCounter % 2) == 0 )
-//            continue;
-
-        for ( b = 0; b < nLeaves; b++ )
-            pLits[b] = toLitCond( p->pCnf->pVarNums[pCut->pLeaves[b]], (i&(1<<b)) );
-        // add the clause
-        RetValue = sat_solver_addclause( p->pSatMain, pLits, pLits + nLeaves );
-//        assert( RetValue == 1 );
-        if ( RetValue == 0 )
-        {
-            printf( "Already UNSAT after %d clauses.\n", nCounter );
-            return -1;
-        }
-    }
-    return nCounter;
-}
-*/
-
-
-/**Function*************************************************************
-
   Synopsis    [Return combinations appearing in the cut.]
 
   Description [This procedure is taken from "Hacker's Delight" by H.S.Warren.]
@@ -289,36 +186,23 @@ int Fra_ClausProcessClausesCut( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t *
     unsigned Matrix[32];
     unsigned * pSims[4], uWord;
     int nSeries, i, k, j;
+    int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
     // compute parameters
     assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
-    assert( pSimMan->nWordsTotal % 8 == 0 );
+    assert( nWordsForSim % 8 == 0 );
     // get parameters
     for ( i = 0; i < (int)pCut->nLeaves; i++ )
-        pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] );
+        pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ) + p->nSimWordsPref;
     // add combinational patterns
     memset( pScores, 0, sizeof(int) * 16 );
-    nSeries = pSimMan->nWordsTotal / 8;
+    nSeries = nWordsForSim / 8;
     for ( i = 0; i < nSeries; i++ )
     {
         memset( Matrix, 0, sizeof(unsigned) * 32 );
         for ( k = 0; k < 8; k++ )
             for ( j = 0; j < (int)pCut->nLeaves; j++ )
                 Matrix[31-(k*4+j)] = pSims[j][i*8+k];
-/*
-        for ( k = 0; k < 32; k++ )
-        {
-            Extra_PrintBinary( stdout, Matrix + k, 32 ); printf( "\n" );
-        }
-        printf( "\n" );
-*/
         transpose32a( Matrix );
-/*
-        for ( k = 0; k < 32; k++ )
-        {
-            Extra_PrintBinary( stdout, Matrix + k, 32 ); printf( "\n" );
-        }
-        printf( "\n" );
-*/
         for ( k = 0; k < 32; k++ )
             for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 )
                 pScores[uWord & 0xF]++;
@@ -347,15 +231,16 @@ int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t *
 {
     unsigned * pSims[4], uWord;
     int iMint, i, k, b;
+    int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
     // compute parameters
     assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
-    assert( pSimMan->nWordsTotal % 8 == 0 );
+    assert( nWordsForSim % 8 == 0 );
     // get parameters
     for ( i = 0; i < (int)pCut->nLeaves; i++ )
-        pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] );
+        pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ) + p->nSimWordsPref;
     // add combinational patterns
     memset( pScores, 0, sizeof(int) * 16 );
-    for ( i = 0; i < pSimMan->nWordsTotal; i++ )
+    for ( i = 0; i < nWordsForSim; i++ )
         for ( k = 0; k < 32; k++ )
         {
             iMint = 0;
@@ -373,6 +258,60 @@ int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t *
     return (int)uWord;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the cut-off cost.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausSelectClauses( Clu_Man_t * p )
+{
+    int * pCostCount, nClauCount, Cost, CostMax, i, c;
+    assert( Vec_IntSize(p->vClauses) > p->nClausesMax );   
+    // count how many implications have each cost
+    CostMax = p->nSimWords * 32 + 1;
+    pCostCount = ALLOC( int, CostMax );
+    memset( pCostCount, 0, sizeof(int) * CostMax );
+    Vec_IntForEachEntry( p->vCosts, Cost, i )
+    {
+        assert( Cost < CostMax );
+        pCostCount[ Cost ]++;
+    }
+    assert( pCostCount[0] == 0 );
+    // select the bound on the cost (above this bound, implication will be included)
+    nClauCount = 0;
+    for ( c = CostMax - 1; c > 0; c-- )
+    {
+        assert( pCostCount[c] >= 0 );
+        nClauCount += pCostCount[c];
+        if ( nClauCount >= p->nClausesMax )
+            break;
+    }
+    // collect implications with the given costs
+    nClauCount = 0;
+    Vec_IntForEachEntry( p->vCosts, Cost, i )
+    {
+        if ( Cost >= c && nClauCount < p->nClausesMax )
+        {
+            nClauCount++;
+            continue;
+        }
+        Vec_IntWriteEntry( p->vCosts, i, -1 );
+    }
+    free( pCostCount );
+    p->nClauses = nClauCount;
+if ( p->fVerbose )
+printf( "Selected %d clauses. Cost range: [%d < %d < %d]\n", nClauCount, 1, c, CostMax );
+    return c;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Processes the clauses.]
@@ -395,6 +334,145 @@ void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausSmlNodeIsConst( Fra_Sml_t * pSeq, Aig_Obj_t * pObj )
+{
+    unsigned * pSims;
+    int i;
+    pSims = Fra_ObjSim(pSeq, pObj->Id);
+    for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ )
+        if ( pSims[i] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if implications holds.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausSmlNodesAreImp( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
+{
+    unsigned * pSimL, * pSimR;
+    int k;
+    pSimL = Fra_ObjSim(pSeq, pObj1->Id);
+    pSimR = Fra_ObjSim(pSeq, pObj2->Id);
+    for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
+        if ( pSimL[k] & ~pSimR[k] ) // !(Obj1 -> Obj2)
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if implications holds.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausSmlNodesAreImpC( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
+{
+    unsigned * pSimL, * pSimR;
+    int k;
+    pSimL = Fra_ObjSim(pSeq, pObj1->Id);
+    pSimR = Fra_ObjSim(pSeq, pObj2->Id);
+    for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
+        if ( pSimL[k] & pSimR[k] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Processes the clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
+{
+    Aig_Obj_t * pObj1, * pObj2;
+    unsigned * pSims1, * pSims2;
+    int CostMax, i, k, nCountConst, nCountImps;
+
+    nCountConst = nCountImps = 0;
+    CostMax = p->nSimWords * 32;
+    pSeq->nWordsPref = p->nSimWordsPref;
+    Aig_ManForEachLoSeq( p->pAig, pObj1, i )
+    {
+        pSims1 = Fra_ObjSim( pSeq, pObj1->Id );
+        if ( Fra_ClausSmlNodeIsConst( pSeq, pObj1 ) )
+        {
+            Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
+            Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
+            Vec_IntPush( p->vCosts, CostMax );
+            nCountConst++;
+            continue;
+        }
+        Aig_ManForEachLoSeq( p->pAig, pObj2, k )
+        {
+            pSims2 = Fra_ObjSim( pSeq, pObj2->Id );
+            if ( Fra_ClausSmlNodesAreImp( pSeq, pObj1, pObj2 ) )
+            {
+                Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
+                Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 0 ) );
+                Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
+                Vec_IntPush( p->vCosts, CostMax );
+                nCountImps++;
+                continue;
+            }
+            if ( Fra_ClausSmlNodesAreImp( pSeq, pObj2, pObj1 ) )
+            {
+                Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 ) );
+                Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 0 ) );
+                Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
+                Vec_IntPush( p->vCosts, CostMax );
+                nCountImps++;
+                continue;
+            }
+            if ( Fra_ClausSmlNodesAreImpC( pSeq, pObj1, pObj2 ) )
+            {
+                Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
+                Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 ) );
+                Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
+                Vec_IntPush( p->vCosts, CostMax );
+                nCountImps++;
+                continue;
+            }
+        }
+        if ( nCountConst + nCountImps > p->nClausesMax / 2 )
+            break;
+    }
+    pSeq->nWordsPref = 0;
+    if ( p->fVerbose )
+    printf( "Collected %d constants and %d implications.\n", nCountConst, nCountImps );
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Processes the clauses.]
 
   Description []
@@ -404,7 +482,7 @@ void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_ClausProcessClauses( Clu_Man_t * p )
+int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
 {
     Aig_MmFixed_t * pMemCuts;
     Fra_Sml_t * pComb, * pSeq;
@@ -415,19 +493,37 @@ int Fra_ClausProcessClauses( Clu_Man_t * p )
     // simulate the AIG
 clk = clock();
     srand( 0xAABBAABB );
-    pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nSimFrames, p->nSimWords/p->nSimFrames );
+    pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
     if ( pSeq->fNonConstOut )
     {
         printf( "Property failed after sequential simulation!\n" );
         Fra_SmlStop( pSeq );
         return 0;
     }
+if ( p->fVerbose )
+{
 PRT( "Sim-seq", clock() - clk );
+}
+
+
+clk = clock();
+    if ( fRefs )
+    {
+    Fra_ClausCollectLatchClauses( p, pSeq );
+if ( p->fVerbose )
+{
+PRT( "Lat-cla", clock() - clk );
+}
+    }
+
 
     // generate cuts for all nodes, assign cost, and find best cuts
 clk = clock();
     pMemCuts = Dar_ManComputeCuts( p->pAig, 10 );
+if ( p->fVerbose )
+{
 PRT( "Cuts   ", clock() - clk );
+}
 
     // collect sequential info for each cut
 clk = clock();
@@ -442,14 +538,20 @@ clk = clock();
 //                    int x = 0;
 //                }
             }
+if ( p->fVerbose )
+{
 PRT( "Infoseq", clock() - clk );
+}
     Fra_SmlStop( pSeq );
 
     // perform combinational simulation
 clk = clock();
     srand( 0xAABBAABB );
-    pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords );
+    pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref  );
+if ( p->fVerbose )
+{
 PRT( "Sim-cmb", clock() - clk );
+}
 
     // collect combinational info for each cut
 clk = clock();
@@ -470,10 +572,19 @@ clk = clock();
             }
     Fra_SmlStop( pComb );
     Aig_MmFixedStop( pMemCuts, 0 );
+if ( p->fVerbose )
+{
 PRT( "Infocmb", clock() - clk );
+}
 
+    if ( p->fVerbose )
     printf( "Node = %5d. Non-triv cuts = %7d. Clauses = %6d. Clause per cut = %6.2f.\n", 
         Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
+
+    if ( Vec_IntSize(p->vClauses) > p->nClausesMax )
+        Fra_ClausSelectClauses( p );
+    else
+        p->nClauses = Vec_IntSize( p->vClauses );
     return 1;
 }
 
@@ -490,7 +601,6 @@ PRT( "Infocmb", clock() - clk );
 ***********************************************************************/
 int Fra_ClausBmcClauses( Clu_Man_t * p )
 {
-    int nBTLimit = 0;
     int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f;
 /*
     for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
@@ -499,7 +609,16 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
 */
     // add the clauses
     Counter = 0;
+    // skip through the prefix variables
+    if ( p->nPref )
+    {
+        nLitsTot = p->nPref * 2 * p->pCnf->nVars;
+        for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
+            p->vLits->pArray[i] += nLitsTot;
+    }
+    // go through the timeframes
     nLitsTot = 2 * p->pCnf->nVars;
+    pStart = Vec_IntArray(p->vLits);
     for ( f = 0; f < p->nFrames; f++ )
     {
         Beg = 0;
@@ -512,12 +631,13 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
             }
             assert( Vec_IntEntry( p->vCosts, i ) > 0 );
             assert( End - Beg < 5 );
-            pStart = Vec_IntArray(p->vLits);
+
             for ( k = Beg; k < End; k++ )
                 pStart[k] = lit_neg( pStart[k] );
-            RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
             for ( k = Beg; k < End; k++ )
                 pStart[k] = lit_neg( pStart[k] );
+
             if ( RetValue != l_False )
             {
                 Beg = End;
@@ -551,7 +671,7 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
     }
 
     // return clauses back to normal
-    nLitsTot = p->nFrames * nLitsTot;
+    nLitsTot = (p->nPref + p->nFrames) * nLitsTot;
     for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
         p->vLits->pArray[i] -= nLitsTot;
 /*
@@ -564,6 +684,113 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Cleans simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClausSimInfoClean( Clu_Man_t * p )
+{
+    assert( p->pCnf->nVars <= Vec_PtrSize(p->vCexes) );
+    Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
+    p->nCexes = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reallocs simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClausSimInfoRealloc( Clu_Man_t * p )
+{
+    assert( p->nCexes == p->nCexesAlloc );
+    Vec_PtrReallocSimInfo( p->vCexes );
+    Vec_PtrCleanSimInfo( p->vCexes, p->nCexesAlloc/32, 2 * p->nCexesAlloc/32 );
+    p->nCexesAlloc *= 2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Records simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClausSimInfoRecord( Clu_Man_t * p, int * pModel )
+{
+    int i;
+    if ( p->nCexes == p->nCexesAlloc )
+        Fra_ClausSimInfoRealloc( p );
+    assert( p->nCexes < p->nCexesAlloc );
+    for ( i = 0; i < p->pCnf->nVars; i++ )
+    {
+        if ( pModel[i] == l_True )
+        {
+            assert( Aig_InfoHasBit( Vec_PtrEntry(p->vCexes, i), p->nCexes ) == 0 );
+            Aig_InfoSetBit( Vec_PtrEntry(p->vCexes, i), p->nCexes );
+        }
+    }
+    p->nCexes++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Uses the simulation info.]
+
+  Description [Returns 1 if the simulation info disproved the clause.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausSimInfoCheck( Clu_Man_t * p, int * pLits, int nLits )
+{
+    unsigned * pSims[4], uWord;
+    int nWords, iVar, i, w;
+    for ( i = 0; i < nLits; i++ )
+    {
+        iVar = lit_var(pLits[i]) - p->nFrames * p->pCnf->nVars;
+        assert( iVar > 0 && iVar < p->pCnf->nVars );
+        pSims[i] = Vec_PtrEntry( p->vCexes, iVar );
+    }
+    nWords = p->nCexes / 32;
+    for ( w = 0; w < nWords; w++ )
+    {
+        uWord = ~(unsigned)0;
+        for ( i = 0; i < nLits; i++ )
+            uWord &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
+        if ( uWord )
+            return 1;
+    }
+    if ( p->nCexes % 32 )
+    {
+        uWord = ~(unsigned)0;
+        for ( i = 0; i < nLits; i++ )
+            uWord &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
+        if ( uWord & Aig_InfoMask( p->nCexes % 32 ) )
+            return 1;
+    }
+    return 0;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Converts AIG into the SAT solver.]
 
   Description []
@@ -575,8 +802,8 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
 ***********************************************************************/
 int Fra_ClausInductiveClauses( Clu_Man_t * p )
 {
-    int nBTLimit = 0;
-    int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f;
+//    Aig_Obj_t * pObjLi, * pObjLo;
+    int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f, fFail = 0, fFlag;//, Lits[2];
 
     // reset the solver
     if ( p->pSatMain )  sat_solver_delete( p->pSatMain );
@@ -585,7 +812,9 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
     {
         printf( "Error: Main solver is unsat.\n" );
         return -1;
-    }
+    }  
+    Fra_ClausSimInfoClean( p );
+
 /*
     // check if the property holds
     if ( Fra_ClausRunSat0( p ) )
@@ -593,8 +822,26 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
     else
         printf( "Property does not hold without strengthening.\n" );
 */
+/*
+    // add constant registers
+    Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )  
+        if ( Aig_ObjFanin0(pObjLi) == Aig_ManConst1(p->pAig) )
+        {
+            for ( k = 0; k < p->nFrames; k++ )
+            {
+                Lits[0] = k * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObjLo->Id], Aig_ObjFaninC0(pObjLi) ); 
+                RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 );
+                if ( RetValue == 0 )
+                {
+                    printf( "Error: Solver is UNSAT after adding constant-register clauses.\n" );
+                    return -1;
+                }
+            }
+        }
+*/
     // add the clauses
     nLitsTot = 2 * p->pCnf->nVars;
+    pStart = Vec_IntArray(p->vLits);
     for ( f = 0; f < p->nFrames; f++ )
     {
         Beg = 0;
@@ -607,7 +854,6 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
             }
             assert( Vec_IntEntry( p->vCosts, i ) > 0 );
             assert( End - Beg < 5 );
-            pStart = Vec_IntArray(p->vLits);
             // add the clause to all timeframes
             RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
             if ( RetValue == 0 )
@@ -633,13 +879,15 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
     // check if the property holds
     if ( Fra_ClausRunSat0( p ) )
     {
-//        printf( "Property holds with strengthening.\n" );
+        if ( p->fVerbose )
         printf( " Property holds.  " );
     }
     else
     {
+        if ( p->fVerbose )
         printf( " Property fails.  " );
-        return -2;
+//        return -2;
+        fFail = 1;
     }
 
 /*
@@ -683,30 +931,55 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
         }
         assert( Vec_IntEntry( p->vCosts, i ) > 0 );
         assert( End - Beg < 5 );
-        pStart = Vec_IntArray(p->vLits);
+
+        if ( Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg) )
+        {
+            fFlag = 1;
+//            printf( "s-" );
+
+            Beg = End;
+            Vec_IntWriteEntry( p->vCosts, i, -1 );
+            Counter++;
+            continue;
+        }
+        else
+        {
+            fFlag = 0;
+//            printf( "s?" );
+        }
 
         for ( k = Beg; k < End; k++ )
             pStart[k] = lit_neg( pStart[k] );
-        RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
         for ( k = Beg; k < End; k++ )
             pStart[k] = lit_neg( pStart[k] );
 
         // the problem is not solved
         if ( RetValue != l_False )
         {
+//            printf( "S- " );
+            Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model.ptr + p->nFrames * p->pCnf->nVars );
+//            RetValue = Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg);
+//            assert( RetValue );
+
             Beg = End;
             Vec_IntWriteEntry( p->vCosts, i, -1 );
             Counter++;
             continue;
         }
+//        printf( "S+ " );
+//        assert( !fFlag );
+
+/*
         // add the clause
         RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
 //        assert( RetValue == 1 );
         if ( RetValue == 0 )
         {
-            printf( "Error: Solver is UNSAT after adding BMC clauses.\n" );
+            printf( "Error: Solver is UNSAT after adding proved clauses.\n" );
             return -1;
         }
+*/
         Beg = End;
 
         // simplify the solver
@@ -723,10 +996,13 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
     for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
         p->vLits->pArray[i] -= nLitsTot;
 
+    if ( fFail )
+        return -2;
     return Counter;
 }
 
 
+
 /**Function*************************************************************
 
   Synopsis    [Converts AIG into the SAT solver.]
@@ -738,26 +1014,27 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nClausesMax, int fVerbose, int fVeryVerbose )
+Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int fVerbose, int fVeryVerbose )
 {
     Clu_Man_t * p;
     p = ALLOC( Clu_Man_t, 1 );
     memset( p, 0, sizeof(Clu_Man_t) );
-    p->pAig         = pAig;
-    p->nFrames      = nFrames;
-    p->nClausesMax  = nClausesMax;
-    p->fVerbose     = fVerbose;
-    p->fVeryVerbose = fVeryVerbose;
-    p->nSimWords    = 256;//1024;//64;
-    p->nSimFrames   = 16;//8;//32;
-    p->vValues      = Vec_IntStart( Aig_ManObjNumMax(p->pAig) );
-
-    p->vLits        = Vec_IntAlloc( 1<<14 );
-    p->vClauses     = Vec_IntAlloc( 1<<12 );
-    p->vCosts       = Vec_IntAlloc( 1<<12 );
-
-    p->nCexesAlloc  = 1024;
-    p->vCexes       = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pAig), p->nCexesAlloc/32 );
+    p->pAig          = pAig;
+    p->nFrames       = nFrames;
+    p->nPref         = nPref;
+    p->nClausesMax   = nClausesMax;
+    p->fVerbose      = fVerbose;
+    p->fVeryVerbose  = fVeryVerbose;
+    p->nSimWords     = 512;//1024;//64;
+    p->nSimFrames    = 32;//8;//32;
+    p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
+
+    p->vLits         = Vec_IntAlloc( 1<<14 );
+    p->vClauses      = Vec_IntAlloc( 1<<12 );
+    p->vCosts        = Vec_IntAlloc( 1<<12 );
+
+    p->nCexesAlloc   = 1024;
+    p->vCexes        = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pAig)+1, p->nCexesAlloc/32 );
     Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
     return p;
 }
@@ -779,7 +1056,6 @@ void Fra_ClausFree( Clu_Man_t * p )
     if ( p->vLits )     Vec_IntFree( p->vLits );
     if ( p->vClauses )  Vec_IntFree( p->vClauses );
     if ( p->vCosts )    Vec_IntFree( p->vCosts );
-    if ( p->vValues )   Vec_IntFree( p->vValues );
     if ( p->pCnf )      Cnf_DataFree( p->pCnf );
     if ( p->pSatMain )  sat_solver_delete( p->pSatMain );
     if ( p->pSatBmc )   sat_solver_delete( p->pSatBmc );
@@ -797,40 +1073,46 @@ void Fra_ClausFree( Clu_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nClausesMax, int fBmc, int fVerbose, int fVeryVerbose )
+int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int fBmc, int fRefs, int fVerbose, int fVeryVerbose )
 {
     Clu_Man_t * p;
     int clk, clkTotal = clock();
-    int Iter, Counter;
+    int Iter, Counter, nPrefOld;
 
     assert( Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
 
     // create the manager
-    p = Fra_ClausAlloc( pAig, nFrames, nClausesMax, fVerbose, fVeryVerbose );
+    p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, fVerbose, fVeryVerbose );
 
 clk = clock();
     // derive CNF
     p->pAig->nRegs++;
     p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManPoNum(p->pAig) );
     p->pAig->nRegs--;
+if ( fVerbose )
+{
 PRT( "CNF    ", clock() - clk );
+}
 
     // check BMC
 clk = clock();
-    p->pSatBmc = Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames, 1 );
+    p->pSatBmc = Cnf_DataWriteIntoSolver( p->pCnf, p->nPref + p->nFrames, 1 );
     if ( p->pSatBmc == NULL )
     {
         printf( "Error: BMC solver is unsat.\n" );
         Fra_ClausFree( p );
         return 1;
-    }
+    } 
     if ( !Fra_ClausRunBmc( p ) )
     {
-        printf( "Problem trivially fails the base case.\n" );
+        printf( "Problem fails the base case after %d frame expansion.\n", p->nPref + p->nFrames );
         Fra_ClausFree( p );
         return 1;
     }
-PRT( "SAT try", clock() - clk );
+if ( fVerbose )
+{
+PRT( "SAT-bmc", clock() - clk );
+}
 
     // start the SAT solver
 clk = clock();
@@ -848,13 +1130,19 @@ clk = clock();
         Fra_ClausFree( p );
         return 1;
     }
-PRT( "SAT try", clock() - clk );
+if ( fVerbose )
+{
+PRT( "SAT-ind", clock() - clk );
+}
  
     // collect the candidate inductive clauses using 4-cuts
 clk = clock();
-    Fra_ClausProcessClauses( p );
-    p->nClauses = Vec_IntSize( p->vClauses );
-PRT( "Clauses", clock() - clk );
+    nPrefOld = p->nPref; p->nPref = 0; p->nSimWordsPref = 0;
+    Fra_ClausProcessClauses( p, fRefs );
+    p->nPref = nPrefOld;
+    p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
+
+//PRT( "Clauses", clock() - clk );
 
 
     // check clauses using BMC
@@ -863,8 +1151,11 @@ PRT( "Clauses", clock() - clk );
 clk = clock();
         Counter = Fra_ClausBmcClauses( p );
         p->nClauses -= Counter;
+if ( fVerbose )
+{
         printf( "BMC disproved %d clauses.\n", Counter );
 PRT( "Cla-bmc", clock() - clk );
+}
     }
 
 
@@ -873,33 +1164,27 @@ clk = clock();
     Counter = 1;
     for ( Iter = 0; Counter > 0; Iter++ )
     {
-        printf( "Iter %3d :  Begin = %5d. ", Iter, p->nClauses );
+        if ( fVerbose )
+        printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses );
         Counter = Fra_ClausInductiveClauses( p );
         if ( Counter > 0 )
            p->nClauses -= Counter;
-        printf( "End = %5d. ", p->nClauses );
+        if ( fVerbose )
+        {
+        printf( "End = %5d. Exs = %5d.  ", p->nClauses, p->nCexes );
 //        printf( "\n" );
         PRT( "Time", clock() - clk );
+        }
         clk = clock();
     }
     if ( Counter == -1 )
-        printf( "Fra_Claus(): Internal error.\n" );
+        printf( "Fra_Claus(): Internal error.  " );
     else if ( Counter == -2 )
-        printf( "Property FAILS after %d iterations of refinement.\n", Iter );
+        printf( "Property FAILS during refinement.  " );
     else
-        printf( "Property HOLDS inductively after strengthening.\n" );
-
-/*
-clk = clock();
-    if ( Fra_ClausRunSat( p ) )
-        printf( "Problem is solved.\n" );
-    else
-        printf( "Problem is unsolved.\n" );
-PRT( "SAT try", clock() - clk );
-*/
+        printf( "Property HOLDS inductively after strengthening.  " );
+    PRT( "Time  ", clock() - clkTotal );
 
-PRT( "TOTAL  ", clock() - clkTotal );
-printf( "\n" );
     // clean the manager
     Fra_ClausFree( p );
     return 1;
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index a5fc7d58..e2bee834 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -345,6 +345,8 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
     for ( k = pSeq->nWordsTotal * 32; k > 0; k-- )
         for ( i = k - 1; i > 0; i-- )
         {
+            // HERE WE ARE MISSING SOME POTENTIAL IMPLICATIONS (with complement!)
+
             for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
             for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
             {
diff --git a/src/aig/kit/kitFactor.c b/src/aig/kit/kitFactor.c
index e3288342..f596d9a8 100644
--- a/src/aig/kit/kitFactor.c
+++ b/src/aig/kit/kitFactor.c
@@ -56,7 +56,7 @@ Kit_Graph_t * Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_
     Kit_Edge_t eRoot;
 //    int nCubes;
 
-    // works for up to 15 variables because divisin procedure
+    // works for up to 15 variables because division procedure
     // used the last bit for marking the cubes going to the remainder
     assert( nVars < 16 );
 
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
new file mode 100644
index 00000000..e58047ae
--- /dev/null
+++ b/src/aig/ntl/ntl.h
@@ -0,0 +1,259 @@
+/**CFile****************************************************************
+
+  FileName    [ntl.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: .h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __NTL_H__
+#define __NTL_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ntl_Man_t_    Ntl_Man_t;
+typedef struct Ntl_Mod_t_    Ntl_Mod_t;
+typedef struct Ntl_Obj_t_    Ntl_Obj_t;
+typedef struct Ntl_Net_t_    Ntl_Net_t;
+typedef struct Ntl_Lut_t_    Ntl_Lut_t;
+
+// object types
+typedef enum { 
+    NTL_OBJ_NONE,                     // 0: non-existent object
+    NTL_OBJ_PI,                       // 1: primary input
+    NTL_OBJ_PO,                       // 2: primary output
+    NTL_OBJ_LATCH,                    // 3: latch node
+    NTL_OBJ_NODE,                     // 4: logic node
+    NTL_OBJ_BOX,                      // 5: white box or black box
+    NTL_OBJ_VOID                      // 6: unused object
+} Ntl_Type_t;
+
+struct Ntl_Man_t_
+{
+    // models of this design
+    char *             pName;          // the name of this design
+    char *             pSpec;          // the name of input file
+    Vec_Ptr_t *        vModels;        // the array of all models used to represent boxes
+    // memory managers
+    Aig_MmFlex_t *     pMemObjs;       // memory for objects
+    Aig_MmFlex_t *     pMemSops;       // memory for SOPs
+    // extracted representation
+    Vec_Ptr_t *        vCis;           // the primary inputs of the extracted part
+    Vec_Ptr_t *        vCos;           // the primary outputs of the extracted part 
+    Vec_Ptr_t *        vNodes;         // the nodes of the abstracted part
+    Aig_Man_t *        pAig;           // the extracted AIG
+    Aig_TMan_t *       pManTime;       // the timing manager
+};
+
+struct Ntl_Mod_t_
+{
+    // model description
+    Ntl_Man_t *        pMan;           // the model manager 
+    char *             pName;          // the model name
+    Vec_Ptr_t *        vObjs;          // the array of all objects
+    Vec_Ptr_t *        vPis;           // the array of PI objects
+    Vec_Ptr_t *        vPos;           // the array of PO objects
+    int                nObjs[NTL_OBJ_VOID]; // counter of objects of each type
+    // hashing names into nets
+    Ntl_Net_t **       pTable;         // the hash table of names into nets
+    int                nTableSize;     // the allocated table size
+    int                nEntries;       // the number of entries in the hash table
+}; 
+
+struct Ntl_Obj_t_
+{
+    Ntl_Mod_t *        pModel;         // the model  
+    unsigned           Type   :  3;    // object type
+    unsigned           Id     : 27;    // object ID
+    unsigned           MarkA  :  1;    // temporary mark  
+    unsigned           MarkB  :  1;    // temporary mark
+    short              nFanins;        // the number of fanins
+    short              nFanouts;       // the number of fanouts
+    union {                            // functionality
+        Ntl_Mod_t *    pImplem;        // model (for boxes)
+        char *         pSop;           // SOP (for logic nodes)
+        unsigned       LatchId;        // init state + register class (for latches) 
+    };
+    Ntl_Net_t *        pFanio[0];      // fanins/fanouts
+};
+
+struct Ntl_Net_t_
+{
+    Ntl_Obj_t *        pDriver;        // driver of the net
+    Ntl_Net_t *        pNext;          // next net in the hash table
+    Aig_Obj_t *        pFunc;          // the AIG representation
+    char               nVisits;        // the number of times the net is visited
+    char               fMark;          // temporary mark
+    char               pName[0];       // the name of this net
+};
+
+struct Ntl_Lut_t_
+{
+    int                Id;             // the ID of the root AIG node
+    int                nFanins;        // the number of fanins
+    int *              pFanins;        // the array of fanins
+    unsigned *         pTruth;         // the truth table
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                      INLINED FUNCTIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int         Ntl_ModelPiNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PI];                } 
+static inline int         Ntl_ModelPoNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PO];                } 
+static inline int         Ntl_ModelNodeNum( Ntl_Mod_t * p )       { return p->nObjs[NTL_OBJ_NODE];              } 
+static inline int         Ntl_ModelLatchNum( Ntl_Mod_t * p )      { return p->nObjs[NTL_OBJ_LATCH];             } 
+static inline int         Ntl_ModelBoxNum( Ntl_Mod_t * p )        { return p->nObjs[NTL_OBJ_BOX];               } 
+
+static inline Ntl_Obj_t * Ntl_ModelPi( Ntl_Mod_t * p, int i )     { return Vec_PtrEntry(p->vPis, i);            } 
+static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i )     { return Vec_PtrEntry(p->vPos, i);            } 
+
+static inline char *      Ntl_ModelPiName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPi(p, i)->pFanio[0]->pName; } 
+static inline char *      Ntl_ModelPoName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPo(p, i)->pFanio[0]->pName; } 
+
+static inline int         Ntl_ModelIsBlackBox( Ntl_Mod_t * p )    { return Ntl_ModelPiNum(p) + Ntl_ModelPoNum(p) == Vec_PtrSize(p->vObjs); } 
+
+static inline int         Ntl_ObjNumFanins( Ntl_Obj_t * p )       { return p->nFanins;                          } 
+static inline int         Ntl_ObjNumFanouts( Ntl_Obj_t * p )      { return p->nFanouts;                         } 
+
+static inline int         Ntl_ObjIsPi( Ntl_Obj_t * p )            { return p->Type == NTL_OBJ_PI;               } 
+static inline int         Ntl_ObjIsPo( Ntl_Obj_t * p )            { return p->Type == NTL_OBJ_PO;               } 
+static inline int         Ntl_ObjIsNode( Ntl_Obj_t * p )          { return p->Type == NTL_OBJ_NODE;             } 
+static inline int         Ntl_ObjIsLatch( Ntl_Obj_t * p )         { return p->Type == NTL_OBJ_LATCH;            } 
+static inline int         Ntl_ObjIsBox( Ntl_Obj_t * p )           { return p->Type == NTL_OBJ_BOX;              } 
+
+static inline Ntl_Net_t * Ntl_ObjFanin0( Ntl_Obj_t * p )          { return p->pFanio[0];                        } 
+static inline Ntl_Net_t * Ntl_ObjFanout0( Ntl_Obj_t * p )         { return p->pFanio[p->nFanins];               } 
+
+static inline Ntl_Net_t * Ntl_ObjFanin( Ntl_Obj_t * p, int i )    { return p->pFanio[i];                        } 
+static inline Ntl_Net_t * Ntl_ObjFanout( Ntl_Obj_t * p, int i )   { return p->pFanio[p->nFanins+1];             } 
+
+static inline void        Ntl_ObjSetFanin( Ntl_Obj_t * p, Ntl_Net_t * pNet, int i )    { p->pFanio[i] = pNet;   } 
+static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int i )   { p->pFanio[p->nFanins+i] = pNet; pNet->pDriver = p; } 
+
+////////////////////////////////////////////////////////////////////////
+///                         ITERATORS                                ///
+////////////////////////////////////////////////////////////////////////
+
+#define Ntl_ManForEachModel( p, pNtl, i )                                       \
+    Vec_PtrForEachEntry( p->vModels, pNtl, i )
+#define Ntl_ManForEachCiNet( p, pNtl, i )                                       \
+    Vec_PtrForEachEntry( p->vCis, pNtl, i )
+#define Ntl_ManForEachCoNet( p, pNtl, i )                                       \
+    Vec_PtrForEachEntry( p->vCos, pNtl, i )
+#define Ntl_ManForEachNode( p, pObj, i )                                   \
+    for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \
+        if ( !Ntl_ObjIsNode(pObj) ) {} else
+#define Ntl_ManForEachBox( p, pObj, i )                                    \
+    for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \
+        if ( !Ntl_ObjIsBox(pObj) ) {} else
+
+#define Ntl_ModelForEachPi( pNtl, pObj, i )                                     \
+    Vec_PtrForEachEntry( pNtl->vPis, pObj, i )
+#define Ntl_ModelForEachPo( pNtl, pObj, i )                                     \
+    Vec_PtrForEachEntry( pNtl->vPos, pObj, i )
+#define Ntl_ModelForEachObj( pNtl, pObj, i )                                    \
+    for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \
+        if ( pObj == NULL ) {} else
+#define Ntl_ModelForEachLatch( pNtl, pObj, i )                                  \
+    for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \
+        if ( !Ntl_ObjIsLatch(pObj) ) {} else
+#define Ntl_ModelForEachNode( pNtl, pObj, i )                                   \
+    for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \
+        if ( !Ntl_ObjIsNode(pObj) ) {} else
+#define Ntl_ModelForEachBox( pNtl, pObj, i )                                    \
+    for ( i = 0; (i < Vec_PtrSize(pNtl->vObjs)) && (((pObj) = Vec_PtrEntry(pNtl->vObjs, i)), 1); i++ ) \
+        if ( !Ntl_ObjIsBox(pObj) ) {} else
+#define Ntl_ModelForEachNet( pNtl, pNet, i )                                    \
+    for ( i = 0; i < pNtl->nTableSize; i++ )                                    \
+        for ( pNet = pNtl->pTable[i]; pNet; pNet = pNet->pNext ) 
+
+#define Ntl_ObjForEachFanin( pObj, pFanin, i )                                  \
+    for ( i = 0; (i < (pObj)->nFanins) && ((pFanin) = (pObj)->pFanio[i]); i++ )
+#define Ntl_ObjForEachFanout( pObj, pFanout, i )                                \
+    for ( i = 0; (i < (pObj)->nFanouts) && ((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== ntlAig.c ==========================================================*/
+extern int             Ntl_ManExtract( Ntl_Man_t * p );
+extern int             Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping );
+extern int             Ntl_ManInsertTest( Ntl_Man_t * p );
+/*=== ntlCheck.c ==========================================================*/
+extern int             Ntl_ManCheck( Ntl_Man_t * pMan );
+extern int             Ntl_ModelCheck( Ntl_Mod_t * pModel );
+extern void            Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
+/*=== ntlDfs.c ==========================================================*/
+extern int             Ntl_ManDfs( Ntl_Man_t * p );
+/*=== ntlMan.c ============================================================*/
+extern Ntl_Man_t *     Ntl_ManAlloc( char * pFileName );
+extern Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
+extern void            Ntl_ManFree( Ntl_Man_t * p );
+extern Ntl_Mod_t *     Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
+extern void            Ntl_ModelFree( Ntl_Mod_t * p );
+/*=== ntlMap.c ============================================================*/
+extern Vec_Ptr_t *     Ntl_MappingAlloc( int nLuts, int nVars );
+extern Vec_Ptr_t *     Ntl_MappingFromAig( Aig_Man_t * p );
+/*=== ntlObj.c ============================================================*/
+extern Ntl_Obj_t *     Ntl_ModelCreatePi( Ntl_Mod_t * pModel );
+extern Ntl_Obj_t *     Ntl_ModelCreatePo( Ntl_Mod_t * pModel, Ntl_Net_t * pNet );
+extern Ntl_Obj_t *     Ntl_ModelCreateLatch( Ntl_Mod_t * pModel );
+extern Ntl_Obj_t *     Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins );
+extern Ntl_Obj_t *     Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts );
+extern char *          Ntl_ManStoreName( Ntl_Man_t * p, char * pName );
+extern char *          Ntl_ManStoreSop( Ntl_Man_t * p, char * pSop );
+extern char *          Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
+/*=== ntlTable.c ==========================================================*/
+extern Ntl_Net_t *     Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
+extern Ntl_Net_t *     Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
+extern int             Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
+/*=== ntlReadBlif.c ==========================================================*/
+extern Ntl_Man_t *     Ioa_ReadBlif( char * pFileName, int fCheck );
+/*=== ntlWriteBlif.c ==========================================================*/
+extern void            Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/ntl/ntlAig.c b/src/aig/ntl/ntlAig.c
new file mode 100644
index 00000000..bc8a8c35
--- /dev/null
+++ b/src/aig/ntl/ntlAig.c
@@ -0,0 +1,504 @@
+/**CFile****************************************************************
+
+  FileName    [ntlAig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Netlist SOP to AIG conversion.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlAig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+#include "dec.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define Ntl_SopForEachCube( pSop, nFanins, pCube )                \
+    for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )
+#define Ntl_CubeForEachVar( pCube, Value, i )                     \
+    for ( i = 0; (pCube[i] != ' ') && (Value = pCube[i]); i++ )           
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Checks if the cover is constant 0.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_SopIsConst0( char * pSop )
+{
+    return pSop[0] == ' ' && pSop[1] == '0';
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the number of variables in the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_SopGetVarNum( char * pSop )
+{
+    char * pCur;
+    for ( pCur = pSop; *pCur != '\n'; pCur++ );
+    return pCur - pSop - 2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the number of cubes in the cover.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_SopGetCubeNum( char * pSop )
+{
+    char * pCur;
+    int nCubes = 0;
+    if ( pSop == NULL )
+        return 0;
+    for ( pCur = pSop; *pCur; pCur++ )
+        nCubes += (*pCur == '\n');
+    return nCubes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_SopIsComplement( char * pSop )
+{
+    char * pCur;
+    for ( pCur = pSop; *pCur; pCur++ )
+        if ( *pCur == '\n' )
+            return (int)(*(pCur - 1) == '0' || *(pCur - 1) == 'n');
+    assert( 0 );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_SopComplement( char * pSop )
+{
+    char * pCur;
+    for ( pCur = pSop; *pCur; pCur++ )
+        if ( *pCur == '\n' )
+        {
+            if ( *(pCur - 1) == '0' )
+                *(pCur - 1) = '1';
+            else if ( *(pCur - 1) == '1' )
+                *(pCur - 1) = '0';
+            else if ( *(pCur - 1) == 'x' )
+                *(pCur - 1) = 'n';
+            else if ( *(pCur - 1) == 'n' )
+                *(pCur - 1) = 'x';
+            else
+                assert( 0 );
+        }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the constant 1 cover with the given number of variables and cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ntl_SopStart( Aig_MmFlex_t * pMan, int nCubes, int nVars )
+{
+    char * pSopCover, * pCube;
+    int i, Length;
+
+    Length = nCubes * (nVars + 3);
+    pSopCover = Aig_MmFlexEntryFetch( pMan, Length + 1 );
+    memset( pSopCover, '-', Length );
+    pSopCover[Length] = 0;
+
+    for ( i = 0; i < nCubes; i++ )
+    {
+        pCube = pSopCover + i * (nVars + 3);
+        pCube[nVars + 0] = ' ';
+        pCube[nVars + 1] = '1';
+        pCube[nVars + 2] = '\n';
+    }
+    return pSopCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the cover from the ISOP computed from TT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ntl_SopCreateFromIsop( Aig_MmFlex_t * pMan, int nVars, Vec_Int_t * vCover )
+{
+    char * pSop, * pCube;
+    int i, k, Entry, Literal;
+    assert( Vec_IntSize(vCover) > 0 );
+    if ( Vec_IntSize(vCover) == 0 )
+        return NULL;
+    // start the cover
+    pSop = Ntl_SopStart( pMan, Vec_IntSize(vCover), nVars );
+    // create cubes
+    Vec_IntForEachEntry( vCover, Entry, i )
+    {
+        pCube = pSop + i * (nVars + 3);
+        for ( k = 0; k < nVars; k++ )
+        {
+            Literal = 3 & (Entry >> (k << 1));
+            if ( Literal == 1 )
+                pCube[k] = '0';
+            else if ( Literal == 2 )
+                pCube[k] = '1';
+            else if ( Literal != 0 )
+                assert( 0 );
+        }
+    }
+    return pSop;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms truth table into the SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover )
+{
+    char * pSop;
+    int RetValue;
+    if ( Kit_TruthIsConst0(pTruth, nVars) )
+        return Ntl_ManStoreSop( p, " 0\n" );
+    if ( Kit_TruthIsConst1(pTruth, nVars) )
+        return Ntl_ManStoreSop( p, " 1\n" );
+    RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 0 ); // 1 );
+    assert( RetValue == 0 || RetValue == 1 );
+    pSop = Ntl_SopCreateFromIsop( p->pMemSops, nVars, vCover );
+    if ( RetValue )
+        Ntl_SopComplement( pSop );
+    return pSop;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Ntl_ConvertSopToAigInternal( Aig_Man_t * pMan, Ntl_Obj_t * pNode, char * pSop )
+{
+    Ntl_Net_t * pNet;
+    Aig_Obj_t * pAnd, * pSum;
+    int i, Value, nFanins;
+    char * pCube;
+    // get the number of variables
+    nFanins = Ntl_SopGetVarNum(pSop);
+    // go through the cubes of the node's SOP
+    pSum = Aig_ManConst0(pMan);
+    Ntl_SopForEachCube( pSop, nFanins, pCube )
+    {
+        // create the AND of literals
+        pAnd = Aig_ManConst1(pMan);
+        Ntl_CubeForEachVar( pCube, Value, i )
+        {
+            pNet = Ntl_ObjFanin( pNode, i );
+            if ( Value == '1' )
+                pAnd = Aig_And( pMan, pAnd, pNet->pFunc );
+            else if ( Value == '0' )
+                pAnd = Aig_And( pMan, pAnd, Aig_Not(pNet->pFunc) );
+        }
+        // add to the sum of cubes
+        pSum = Aig_Or( pMan, pSum, pAnd );
+    }
+    // decide whether to complement the result
+    if ( Ntl_SopIsComplement(pSop) )
+        pSum = Aig_Not(pSum);
+    return pSum;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the decomposition graph into the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Ntl_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
+{
+    Dec_Node_t * pNode;
+    Aig_Obj_t * pAnd0, * pAnd1;
+    int i;
+    // check for constant function
+    if ( Dec_GraphIsConst(pGraph) )
+        return Aig_NotCond( Aig_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
+    // check for a literal
+    if ( Dec_GraphIsVar(pGraph) )
+        return Aig_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
+    // build the AIG nodes corresponding to the AND gates of the graph
+    Dec_GraphForEachNode( pGraph, pNode, i )
+    {
+        pAnd0 = Aig_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
+        pAnd1 = Aig_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
+        pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 );
+    }
+    // complement the result if necessary
+    return Aig_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from AIG to BDD representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Ntl_ManExtractAigNode( Ntl_Obj_t * pNode )
+{
+    Aig_Man_t * pMan = pNode->pModel->pMan->pAig;
+    int fUseFactor = 0;
+    // consider the constant node
+    if ( Ntl_SopGetVarNum(pNode->pSop) == 0 )
+        return Aig_NotCond( Aig_ManConst1(pMan), Ntl_SopIsConst0(pNode->pSop) );
+    // decide when to use factoring
+    if ( fUseFactor && Ntl_SopGetVarNum(pNode->pSop) > 2 && Ntl_SopGetCubeNum(pNode->pSop) > 1 )
+    {
+        Dec_Graph_t * pFForm;
+        Dec_Node_t * pFFNode;
+        Aig_Obj_t * pFunc;
+        int i;
+        // perform factoring
+        pFForm = Dec_Factor( pNode->pSop );
+        // collect the fanins
+        Dec_GraphForEachLeaf( pFForm, pFFNode, i )
+            pFFNode->pFunc = Ntl_ObjFanin(pNode, i)->pFunc;
+        // perform strashing
+        pFunc = Ntl_GraphToNetworkAig( pMan, pFForm );
+        Dec_GraphFree( pFForm );
+        return pFunc;
+    }
+    return Ntl_ConvertSopToAigInternal( pMan, pNode, pNode->pSop );
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts AIG from the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManExtract( Ntl_Man_t * p )
+{
+    Ntl_Obj_t * pNode;
+    Ntl_Net_t * pNet;
+    int i;
+    // check the DFS traversal
+    if ( !Ntl_ManDfs( p ) )
+        return 0;
+    // start the AIG manager
+    assert( p->pAig == NULL );
+    p->pAig = Aig_ManStart( 10000 );
+    // create the primary inputs
+    Ntl_ManForEachCiNet( p, pNet, i )
+        pNet->pFunc = Aig_ObjCreatePi( p->pAig );
+    // convert internal nodes to AIGs
+    Ntl_ManForEachNode( p, pNode, i )
+        Ntl_ObjFanout0(pNode)->pFunc = Ntl_ManExtractAigNode( pNode );
+    // create the primary outputs
+    Ntl_ManForEachCoNet( p, pNet, i )
+        Aig_ObjCreatePo( p->pAig, pNet->pFunc );
+    // cleanup the AIG
+    Aig_ManCleanup( p->pAig );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the given mapping into the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping )
+{
+    char Buffer[100];
+    Vec_Ptr_t * vCopies;
+    Vec_Int_t * vCover;
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pNode;
+    Ntl_Net_t * pNet, * pNetCo;
+    Ntl_Lut_t * pLut;
+    int i, k, nDigits;
+    nDigits = Aig_Base10Log( Vec_PtrSize(vMapping) );
+    // start mapping of AIG nodes into their copies
+    vCopies = Vec_PtrStart( Aig_ManObjNumMax(p->pAig) );
+    Ntl_ManForEachCiNet( p, pNet, i )
+        Vec_PtrWriteEntry( vCopies, pNet->pFunc->Id, pNet );
+    // create a new node for each LUT
+    vCover = Vec_IntAlloc( 1 << 16 );
+    pRoot = Vec_PtrEntry( p->vModels, 0 );
+    Vec_PtrForEachEntry( vMapping, pLut, i )
+    {
+        pNode = Ntl_ModelCreateNode( pRoot, pLut->nFanins );
+        pNode->pSop = Ntl_SopFromTruth( p, pLut->pTruth, pLut->nFanins, vCover );
+        for ( k = 0; k < pLut->nFanins; k++ )
+        {
+            pNet = Vec_PtrEntry( vCopies, pLut->pFanins[k] );
+            if ( pNet == NULL )
+            {
+                printf( "Ntl_ManInsert(): Internal error: Net not found.\n" );
+                return 0;
+            }
+            Ntl_ObjSetFanin( pNode, pNet, k );
+        }
+        sprintf( Buffer, "lut%0*d", nDigits, i );
+        if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: Intermediate net name is not unique.\n" );
+            return 0;
+        }
+        pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
+        if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: Net has more than one fanin.\n" );
+            return 0;
+        }
+        Vec_PtrWriteEntry( vCopies, pLut->Id, pNet );
+    }
+    Vec_IntFree( vCover );
+    // remove old nodes
+    Ntl_ManForEachNode( p, pNode, i )
+        Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
+    // update the CO pointers
+    Ntl_ManForEachCoNet( p, pNetCo, i )
+    {
+        pNode = Ntl_ModelCreateNode( pRoot, 1 );
+        pNode->pSop = Aig_IsComplement(pNetCo->pFunc)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
+        pNet = Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pFunc)->Id );
+        Ntl_ObjSetFanin( pNode, pNet, 0 );
+        // update the CO driver net
+        pNetCo->pDriver = NULL;
+        if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
+        {
+            printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
+            return 0;
+        }
+    }
+    Vec_PtrFree( vCopies );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Testing procedure for insertion of mapping into the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManInsertTest( Ntl_Man_t * p )
+{
+    Vec_Ptr_t * vMapping;
+    int RetValue;
+    if ( !Ntl_ManExtract( p ) )
+        return 0;
+    assert( p->pAig != NULL );
+    vMapping = Ntl_MappingFromAig( p->pAig );
+    RetValue = Ntl_ManInsert( p, vMapping );
+    Vec_PtrFree( vMapping );
+    return RetValue;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c
new file mode 100644
index 00000000..d01c7d5e
--- /dev/null
+++ b/src/aig/ntl/ntlCheck.c
@@ -0,0 +1,126 @@
+/**CFile****************************************************************
+
+  FileName    [ntlCheck.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Checks consistency of the netlist.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManCheck( Ntl_Man_t * pMan )
+{
+    // check that the models have unique names
+    // check that the models (except the first one) do not have boxes
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCheck( Ntl_Mod_t * pModel )
+{
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the verilog file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel )
+{ 
+    Vec_Ptr_t * vNets;
+    Ntl_Net_t * pNet;
+    Ntl_Obj_t * pNode;
+    int i;
+
+    if ( Ntl_ModelIsBlackBox(pModel) )
+        return;
+
+    // check for non-driven nets
+    vNets = Vec_PtrAlloc( 100 );
+    Ntl_ModelForEachNet( pModel, pNet, i )
+    {
+        if ( pNet->pDriver != NULL )
+            continue;
+        // add the constant 0 driver
+        pNode = Ntl_ModelCreateNode( pModel, 0 );
+        pNode->pSop = Ntl_ManStoreSop( pModel->pMan, " 0\n" );
+        Ntl_ModelSetNetDriver( pNode, pNet );
+        // add the net to those for which the warning will be printed
+        Vec_PtrPush( vNets, pNet );
+    }
+
+    // print the warning
+    if ( Vec_PtrSize(vNets) > 0 )
+    {
+        printf( "Warning: Constant-0 drivers added to %d non-driven nets in network \"%s\":\n", Vec_PtrSize(vNets), pModel->pName );
+        Vec_PtrForEachEntry( vNets, pNet, i )
+        {
+            printf( "%s%s", (i? ", ": ""), pNet->pName );
+            if ( i == 3 )
+            {
+                if ( Vec_PtrSize(vNets) > 3 )
+                    printf( " ..." );
+                break;
+            }
+        }
+        printf( "\n" );
+    }
+    Vec_PtrFree( vNets );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlDfs.c b/src/aig/ntl/ntlDfs.c
new file mode 100644
index 00000000..6b5dc407
--- /dev/null
+++ b/src/aig/ntl/ntlDfs.c
@@ -0,0 +1,165 @@
+/**CFile****************************************************************
+
+  FileName    [ntlDfs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [DFS traversal.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlDfs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the nodes in a topological order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManDfs_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
+{
+    Ntl_Obj_t * pObj;
+    Ntl_Net_t * pNetFanin;
+    int i;
+    // skip visited
+    if ( pNet->nVisits == 2 ) 
+        return 1;
+    // if the node is on the path, this is a combinational loop
+    if ( pNet->nVisits == 1 )
+        return 0; 
+    // mark the node as the one on the path
+    pNet->nVisits = 1;
+    // derive the box
+    pObj = pNet->pDriver;
+    assert( Ntl_ObjIsNode(pObj) || Ntl_ObjIsBox(pObj) );
+    // visit the input nets of the box
+    Ntl_ObjForEachFanin( pObj, pNetFanin, i )
+        if ( !Ntl_ManDfs_rec( p, pNetFanin ) )
+            return 0;
+    // add box inputs/outputs to COs/CIs
+    if ( Ntl_ObjIsBox(pObj) )
+    {
+        Ntl_ObjForEachFanin( pObj, pNetFanin, i )
+            Vec_PtrPush( p->vCos, pNetFanin );
+        Ntl_ObjForEachFanout( pObj, pNetFanin, i )
+            Vec_PtrPush( p->vCis, pNetFanin );
+    }
+    // store the node
+    Vec_PtrPush( p->vNodes, pObj );
+    pNet->nVisits = 2;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS.]
+
+  Description [Checks for combinational loops. Collects PI/PO nets.
+  Collects nodes in the topological order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManDfs( Ntl_Man_t * p )
+{
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pObj;
+    Ntl_Net_t * pNet;
+    int i, nUselessObjects;
+    assert( Vec_PtrSize(p->vCis) == 0 );
+    assert( Vec_PtrSize(p->vCos) == 0 );
+    assert( Vec_PtrSize(p->vNodes) == 0 );
+    // get the root model
+    pRoot = Vec_PtrEntry( p->vModels, 0 );
+    // collect primary inputs
+    Ntl_ModelForEachPi( pRoot, pObj, i )
+    {
+        assert( Ntl_ObjNumFanouts(pObj) == 1 );
+        pNet = Ntl_ObjFanout0(pObj);
+        Vec_PtrPush( p->vCis, pNet );
+        if ( pNet->nVisits )
+        {
+            printf( "Ntl_ManDfs(): Primary input appears twice in the list.\n" );
+            return 0;
+        }
+        pNet->nVisits = 2;
+    }
+    // collect latch outputs
+    Ntl_ModelForEachLatch( pRoot, pObj, i )
+    {
+        assert( Ntl_ObjNumFanouts(pObj) == 1 );
+        pNet = Ntl_ObjFanout0(pObj);
+        Vec_PtrPush( p->vCis, pNet );
+        if ( pNet->nVisits )
+        {
+            printf( "Ntl_ManDfs(): Latch output is duplicated or defined as a primary input.\n" );
+            return 0;
+        }
+        pNet->nVisits = 2;
+    }
+    // visit the nodes starting from primary outputs
+    Ntl_ModelForEachPo( pRoot, pObj, i )
+    {
+        pNet = Ntl_ObjFanin0(pObj);
+        if ( !Ntl_ManDfs_rec( p, pNet ) )
+        {
+            printf( "Ntl_ManDfs(): Error: Combinational loop is detected.\n" );
+            Vec_PtrClear( p->vCis );
+            Vec_PtrClear( p->vCos );
+            Vec_PtrClear( p->vNodes );
+            return 0;
+        }
+        Vec_PtrPush( p->vCos, pNet );
+    }
+    // visit the nodes starting from latch inputs outputs
+    Ntl_ModelForEachLatch( pRoot, pObj, i )
+    {
+        pNet = Ntl_ObjFanin0(pObj);
+        if ( !Ntl_ManDfs_rec( p, pNet ) )
+        {
+            printf( "Ntl_ManDfs(): Error: Combinational loop is detected.\n" );
+            Vec_PtrClear( p->vCis );
+            Vec_PtrClear( p->vCos );
+            Vec_PtrClear( p->vNodes );
+            return 0;
+        }
+        Vec_PtrPush( p->vCos, pNet );
+    }
+    // report the number of dangling objects
+    nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
+    if ( nUselessObjects )
+        printf( "The number of nodes that do not feed into POs = %d.\n", nUselessObjects );
+    return 1;    
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
new file mode 100644
index 00000000..cc9bd029
--- /dev/null
+++ b/src/aig/ntl/ntlMan.c
@@ -0,0 +1,166 @@
+/**CFile****************************************************************
+
+  FileName    [ntlMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Netlist manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the netlist manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Man_t * Ntl_ManAlloc( char * pFileName )
+{
+    Ntl_Man_t * p;
+    // start the manager
+    p = ALLOC( Ntl_Man_t, 1 );
+    memset( p, 0, sizeof(Ntl_Man_t) );
+    p->vModels = Vec_PtrAlloc( 1000 );
+    p->vCis = Vec_PtrAlloc( 1000 );
+    p->vCos = Vec_PtrAlloc( 1000 );
+    p->vNodes = Vec_PtrAlloc( 1000 );
+    // start the manager
+    p->pMemObjs = Aig_MmFlexStart();
+    p->pMemSops = Aig_MmFlexStart();
+    // same the names
+    p->pName = Ntl_ManStoreFileName( p, pFileName );
+    p->pSpec = Ntl_ManStoreName( p, pFileName );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the netlist manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManFree( Ntl_Man_t * p )
+{
+    if ( p->vModels )
+    {
+        Ntl_Mod_t * pModel;
+        int i;
+        Ntl_ManForEachModel( p, pModel, i )
+            Ntl_ModelFree( pModel );
+        Vec_PtrFree( p->vModels );
+    }
+    if ( p->vCis )     Vec_PtrFree( p->vCis );
+    if ( p->vCos )     Vec_PtrFree( p->vCos );
+    if ( p->vNodes )   Vec_PtrFree( p->vNodes );
+    if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 );
+    if ( p->pMemSops ) Aig_MmFlexStop( p->pMemSops, 0 );
+    if ( p->pAig )     Aig_ManStop( p->pAig );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the model with the given name.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName )
+{
+    Ntl_Mod_t * pModel;
+    int i;
+    Vec_PtrForEachEntry( p->vModels, pModel, i )
+        if ( !strcmp( pModel->pName, pName ) )
+            return pModel;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName )
+{
+    Ntl_Mod_t * p;
+    // start the manager
+    p = ALLOC( Ntl_Mod_t, 1 );
+    memset( p, 0, sizeof(Ntl_Mod_t) );
+    p->pMan  = pMan;
+    p->pName = Ntl_ManStoreName( p->pMan, pName );
+    Vec_PtrPush( pMan->vModels, p );
+    p->vObjs = Vec_PtrAlloc( 10000 );
+    p->vPis  = Vec_PtrAlloc( 1000 );
+    p->vPos  = Vec_PtrAlloc( 1000 );
+    // start the table
+    p->nTableSize = Aig_PrimeCudd( 10000 );
+    p->pTable = ALLOC( Ntl_Net_t *, p->nTableSize );
+    memset( p->pTable, 0, sizeof(Ntl_Net_t *) * p->nTableSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ModelFree( Ntl_Mod_t * p )
+{
+    Vec_PtrFree( p->vObjs );
+    Vec_PtrFree( p->vPis );
+    Vec_PtrFree( p->vPos );
+    free( p->pTable );
+    free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlMap.c b/src/aig/ntl/ntlMap.c
new file mode 100644
index 00000000..1d8443b4
--- /dev/null
+++ b/src/aig/ntl/ntlMap.c
@@ -0,0 +1,110 @@
+/**CFile****************************************************************
+
+  FileName    [ntlMap.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Derives mapped network from AIG.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlMap.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates mapping for the given AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ntl_MappingAlloc( int nLuts, int nVars )
+{
+    char * pMemory;
+    Ntl_Lut_t ** pArray;
+    int nEntrySize, i;
+    nEntrySize = sizeof(Ntl_Lut_t) + sizeof(int) * nVars + sizeof(unsigned) * Aig_TruthWordNum(nVars);
+    pArray = (Ntl_Lut_t **)malloc( (sizeof(Ntl_Lut_t *) + nEntrySize) * nLuts );
+    pMemory = (char *)(pArray + nLuts);
+    memset( pMemory, 0, nEntrySize * nLuts );
+    for ( i = 0; i < nLuts; i++ )
+    {
+        pArray[i] = (Ntl_Lut_t *)pMemory;
+        pArray[i]->pFanins = (int *)(pMemory + sizeof(Ntl_Lut_t));
+        pArray[i]->pTruth = (unsigned *)(pMemory + sizeof(Ntl_Lut_t) + sizeof(int) * nVars);
+        pMemory += nEntrySize;
+    }
+    return Vec_PtrAllocArray( (void **)pArray, nLuts );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives trivial mapping from the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vMapping;
+    Ntl_Lut_t * pLut;
+    Aig_Obj_t * pObj;
+    int i, k = 0, nBytes = 4;
+    vMapping = Ntl_MappingAlloc( Aig_ManAndNum(p) + (int)(Aig_ManConst1(p)->nRefs > 0), 2 );
+    if ( Aig_ManConst1(p)->nRefs > 0 )
+    {
+        pLut = Vec_PtrEntry( vMapping, k++ );
+        pLut->Id = 0;
+        pLut->nFanins = 0;
+        memset( pLut->pTruth, 0xFF, nBytes );
+    }
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        pLut = Vec_PtrEntry( vMapping, k++ );
+        pLut->Id = pObj->Id;
+        pLut->nFanins = 2;
+        pLut->pFanins[0] = Aig_ObjFaninId0(pObj);
+        pLut->pFanins[1] = Aig_ObjFaninId1(pObj);
+        if      (  Aig_ObjFaninC0(pObj) &&  Aig_ObjFaninC1(pObj) ) 
+            memset( pLut->pTruth, 0x11, nBytes );
+        else if ( !Aig_ObjFaninC0(pObj) &&  Aig_ObjFaninC1(pObj) )
+            memset( pLut->pTruth, 0x22, nBytes );
+        else if (  Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
+            memset( pLut->pTruth, 0x44, nBytes );
+        else if ( !Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
+            memset( pLut->pTruth, 0x88, nBytes );
+    }
+    assert( k == Vec_PtrSize(vMapping) );
+    return vMapping;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlObj.c b/src/aig/ntl/ntlObj.c
new file mode 100644
index 00000000..2e39fbbf
--- /dev/null
+++ b/src/aig/ntl/ntlObj.c
@@ -0,0 +1,238 @@
+/**CFile****************************************************************
+
+  FileName    [.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: .c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the primary input.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Obj_t * Ntl_ModelCreatePi( Ntl_Mod_t * pModel )
+{
+    Ntl_Obj_t * p;
+    p = (Ntl_Obj_t *)Aig_MmFlexEntryFetch( pModel->pMan->pMemObjs, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) );
+    memset( p, 0, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) );
+    p->Id = Vec_PtrSize( pModel->vObjs );
+    Vec_PtrPush( pModel->vObjs, p );
+    Vec_PtrPush( pModel->vPis, p );
+    p->pModel   = pModel;
+    p->Type     = NTL_OBJ_PI;
+    p->nFanins  = 0;
+    p->nFanouts = 1;
+    pModel->nObjs[NTL_OBJ_PI]++;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the primary output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Obj_t * Ntl_ModelCreatePo( Ntl_Mod_t * pModel, Ntl_Net_t * pNet )
+{
+    Ntl_Obj_t * p;
+    p = (Ntl_Obj_t *)Aig_MmFlexEntryFetch( pModel->pMan->pMemObjs, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) );
+    memset( p, 0, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) );
+    p->Id = Vec_PtrSize( pModel->vObjs );
+    Vec_PtrPush( pModel->vObjs, p );
+    Vec_PtrPush( pModel->vPos, p );
+    p->pModel    = pModel;
+    p->Type      = NTL_OBJ_PO;
+    p->nFanins   = 1;
+    p->nFanouts  = 0;
+    p->pFanio[0] = pNet;
+    pModel->nObjs[NTL_OBJ_PO]++;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the primary output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Obj_t * Ntl_ModelCreateLatch( Ntl_Mod_t * pModel )
+{
+    Ntl_Obj_t * p;
+    p = (Ntl_Obj_t *)Aig_MmFlexEntryFetch( pModel->pMan->pMemObjs, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) * 3 );
+    memset( p, 0, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) * 3 );
+    p->Id = Vec_PtrSize( pModel->vObjs );
+    Vec_PtrPush( pModel->vObjs, p );
+    p->pModel   = pModel;
+    p->Type     = NTL_OBJ_LATCH;
+    p->nFanins  = 2;
+    p->nFanouts = 1;
+    pModel->nObjs[NTL_OBJ_LATCH]++;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Obj_t * Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins )
+{
+    Ntl_Obj_t * p;
+    p = (Ntl_Obj_t *)Aig_MmFlexEntryFetch( pModel->pMan->pMemObjs, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) * (nFanins + 1) );
+    memset( p, 0, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) * (nFanins + 1) );
+    p->Id = Vec_PtrSize( pModel->vObjs );
+    Vec_PtrPush( pModel->vObjs, p );
+    p->pModel   = pModel;
+    p->Type     = NTL_OBJ_NODE;
+    p->nFanins  = nFanins;
+    p->nFanouts = 1;
+    pModel->nObjs[NTL_OBJ_NODE]++;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create the latch.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts )
+{
+    Ntl_Obj_t * p;
+    p = (Ntl_Obj_t *)Aig_MmFlexEntryFetch( pModel->pMan->pMemObjs, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) * (nFanins + nFanouts) );
+    memset( p, 0, sizeof(Ntl_Obj_t) + sizeof(Ntl_Net_t *) * (nFanins + nFanouts) );
+    p->Id = Vec_PtrSize( pModel->vObjs );
+    Vec_PtrPush( pModel->vObjs, p );
+    p->pModel   = pModel;
+    p->Type     = NTL_OBJ_BOX;
+    p->nFanins  = nFanins;
+    p->nFanouts = nFanouts;
+    pModel->nObjs[NTL_OBJ_BOX]++;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates memory and copies the name into it.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ntl_ManStoreName( Ntl_Man_t * p, char * pName )
+{
+    char * pStore;
+    pStore = Aig_MmFlexEntryFetch( p->pMemObjs, strlen(pName) + 1 );
+    strcpy( pStore, pName );
+    return pStore;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates memory and copies the SOP into it.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ntl_ManStoreSop( Ntl_Man_t * p, char * pSop )
+{
+    char * pStore;
+    pStore = Aig_MmFlexEntryFetch( p->pMemSops, strlen(pSop) + 1 );
+    strcpy( pStore, pSop );
+    return pStore;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates memory and copies the root of file name there.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName )
+{
+    char * pBeg, * pEnd, * pStore, * pCur;
+    // find the first dot
+    for ( pEnd = pFileName; *pEnd; pEnd++ )
+        if ( *pEnd == '.' )
+            break;
+    // find the first char
+    for ( pBeg = pEnd - 1; pBeg >= pFileName; pBeg-- )
+        if ( !((*pBeg >= 'a' && *pBeg <= 'z') || (*pBeg >= 'A' && *pBeg <= 'Z') || (*pBeg >= '0' && *pBeg <= '9') || *pBeg == '_') )
+            break;
+    pBeg++;
+    // fill up storage
+    pStore = Aig_MmFlexEntryFetch( p->pMemSops, pEnd - pBeg + 1 );
+    for ( pCur = pStore; pBeg < pEnd; pBeg++, pCur++ )
+        *pCur = *pBeg;
+    *pCur = 0;
+    return pStore;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
new file mode 100644
index 00000000..feb8e488
--- /dev/null
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -0,0 +1,975 @@
+/**CFile****************************************************************
+
+  FileName    [ntlReadBlif.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to read BLIF file.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 8, 2007.]
+
+  Revision    [$Id: ntlReadBlif.c,v 1.00 2007/01/08 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ioa_ReadMod_t_ Ioa_ReadMod_t;   // parsing model
+typedef struct Ioa_ReadMan_t_ Ioa_ReadMan_t;   // parsing manager
+
+struct Ioa_ReadMod_t_
+{
+    // file lines
+    char *               pFirst;       // .model line
+    Vec_Ptr_t *          vInputs;      // .inputs lines
+    Vec_Ptr_t *          vOutputs;     // .outputs lines
+    Vec_Ptr_t *          vLatches;     // .latch lines
+    Vec_Ptr_t *          vNames;       // .names lines
+    Vec_Ptr_t *          vSubckts;     // .subckt lines
+    int                  fBlackBox;    // indicates blackbox model
+    // the resulting network
+    Ntl_Mod_t *          pNtk;   
+    // the parent manager
+    Ioa_ReadMan_t *      pMan;         
+};
+
+struct Ioa_ReadMan_t_
+{
+    // general info about file
+    char *               pFileName;    // the name of the file
+    char *               pBuffer;      // the contents of the file
+    Vec_Ptr_t *          vLines;       // the line beginnings
+    // the results of reading
+    Ntl_Man_t *          pDesign;      // the design under construction
+    // intermediate storage for models
+    Vec_Ptr_t *          vModels;      // vector of models
+    Ioa_ReadMod_t *      pLatest;      // the current model
+    // current processing info
+    Vec_Ptr_t *          vTokens;      // the current tokens
+    Vec_Ptr_t *          vTokens2;     // the current tokens
+    Vec_Str_t *          vFunc;        // the local function
+    // error reporting
+    char                 sError[512];  // the error string generated during parsing
+    // statistics 
+    int                  nTablesRead;  // the number of processed tables
+    int                  nTablesLeft;  // the number of dangling tables
+};
+
+// static functions
+static Ioa_ReadMan_t *   Ioa_ReadAlloc();
+static void              Ioa_ReadFree( Ioa_ReadMan_t * p );
+static Ioa_ReadMod_t *   Ioa_ReadModAlloc();
+static void              Ioa_ReadModFree( Ioa_ReadMod_t * p );
+static char *            Ioa_ReadLoadFile( char * pFileName );
+static void              Ioa_ReadReadPreparse( Ioa_ReadMan_t * p );
+static void              Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p );
+static Ntl_Man_t *       Ioa_ReadParse( Ioa_ReadMan_t * p );
+static int               Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine );
+static int               Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLine );
+static int               Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine );
+static int               Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine );
+static int               Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine );
+static int               Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine );
+
+static int               Ioa_ReadCharIsSpace( char s )   { return s == ' ' || s == '\t' || s == '\r' || s == '\n';             }
+static int               Ioa_ReadCharIsSopSymb( char s ) { return s == '0' || s == '1' || s == '-' || s == '\r' || s == '\n';  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the network from the BLIF file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck )
+{
+    FILE * pFile;
+    Ioa_ReadMan_t * p;
+    Ntl_Mod_t * pNtk;
+    Ntl_Man_t * pDesign;
+    int i;
+
+    // check that the file is available
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Ioa_ReadBlif(): The file is unavailable (absent or open).\n" );
+        return 0;
+    }
+    fclose( pFile );
+
+    // start the file reader
+    p = Ioa_ReadAlloc();
+    p->pFileName = pFileName;
+    p->pBuffer   = Ioa_ReadLoadFile( pFileName );
+    if ( p->pBuffer == NULL )
+    {
+        Ioa_ReadFree( p );
+        return NULL;
+    }
+    // set the design name
+    p->pDesign = Ntl_ManAlloc( pFileName );
+    // prepare the file for parsing
+    Ioa_ReadReadPreparse( p );
+    // parse interfaces of each network
+    Ioa_ReadReadInterfaces( p );
+    // construct the network
+    pDesign = Ioa_ReadParse( p );
+    if ( p->sError[0] )
+        fprintf( stdout, "%s\n", p->sError );
+    if ( pDesign == NULL )
+        return NULL;
+    p->pDesign = NULL;
+    Ioa_ReadFree( p );
+// pDesign should be linked to all models of the design
+
+    // make sure that everything is okay with the network structure
+    if ( fCheck )
+    {
+        // check individual models
+        Vec_PtrForEachEntry( pDesign->vModels, pNtk, i )
+        {
+            if ( !Ntl_ModelCheck( pNtk ) )
+            {
+                printf( "Ioa_ReadBlif: The network check has failed for network %s.\n", pNtk->pName );
+                Ntl_ManFree( pDesign );
+                return NULL;
+            }
+        }
+        // check the hierarchy
+        if ( !Ntl_ManCheck( pDesign ) )
+        {
+            printf( "Ioa_ReadBlif: The hierarchy check has failed for design %s.\n", pDesign->pName );
+            Ntl_ManFree( pDesign );
+            return NULL;
+        }
+
+    }
+//Ioa_WriteBlif( pDesign, "_temp_.blif" );
+    return pDesign;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the BLIF parsing structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Ioa_ReadMan_t * Ioa_ReadAlloc()
+{
+    Ioa_ReadMan_t * p;
+    p = ALLOC( Ioa_ReadMan_t, 1 );
+    memset( p, 0, sizeof(Ioa_ReadMan_t) );
+    p->vLines   = Vec_PtrAlloc( 512 );
+    p->vModels  = Vec_PtrAlloc( 512 );
+    p->vTokens  = Vec_PtrAlloc( 512 );
+    p->vTokens2 = Vec_PtrAlloc( 512 );
+    p->vFunc    = Vec_StrAlloc( 512 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the BLIF parsing structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Ioa_ReadFree( Ioa_ReadMan_t * p )
+{
+    Ioa_ReadMod_t * pMod;
+    int i;
+    if ( p->pDesign )
+        Ntl_ManFree( p->pDesign );
+    if ( p->pBuffer )  
+        free( p->pBuffer );
+    if ( p->vLines )
+        Vec_PtrFree( p->vLines );
+    if ( p->vModels )
+    {
+        Vec_PtrForEachEntry( p->vModels, pMod, i )
+            Ioa_ReadModFree( pMod );
+        Vec_PtrFree( p->vModels );
+    }
+    Vec_PtrFree( p->vTokens );
+    Vec_PtrFree( p->vTokens2 );
+    Vec_StrFree( p->vFunc );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates the BLIF parsing structure for one model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Ioa_ReadMod_t * Ioa_ReadModAlloc()
+{
+    Ioa_ReadMod_t * p;
+    p = ALLOC( Ioa_ReadMod_t, 1 );
+    memset( p, 0, sizeof(Ioa_ReadMod_t) );
+    p->vInputs  = Vec_PtrAlloc( 512 );
+    p->vOutputs = Vec_PtrAlloc( 512 );
+    p->vLatches = Vec_PtrAlloc( 512 );
+    p->vNames   = Vec_PtrAlloc( 512 );
+    p->vSubckts = Vec_PtrAlloc( 512 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocates the BLIF parsing structure for one model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Ioa_ReadModFree( Ioa_ReadMod_t * p )
+{
+    Vec_PtrFree( p->vInputs );
+    Vec_PtrFree( p->vOutputs );
+    Vec_PtrFree( p->vLatches );
+    Vec_PtrFree( p->vNames );
+    Vec_PtrFree( p->vSubckts );
+    free( p );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of given chars.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Ioa_ReadCountChars( char * pLine, char Char )
+{
+    char * pCur;
+    int Counter = 0;
+    for ( pCur = pLine; *pCur; pCur++ )
+        if ( *pCur == Char )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the already split tokens.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Ioa_ReadCollectTokens( Vec_Ptr_t * vTokens, char * pInput, char * pOutput )
+{
+    char * pCur;
+    Vec_PtrClear( vTokens );
+    for ( pCur = pInput; pCur < pOutput; pCur++ )
+    {
+        if ( *pCur == 0 )
+            continue;
+        Vec_PtrPush( vTokens, pCur );
+        while ( *++pCur );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Splits the line into tokens.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Ioa_ReadSplitIntoTokens( Vec_Ptr_t * vTokens, char * pLine, char Stop )
+{
+    char * pCur;
+    // clear spaces
+    for ( pCur = pLine; *pCur != Stop; pCur++ )
+        if ( Ioa_ReadCharIsSpace(*pCur) )
+            *pCur = 0;
+    // collect tokens
+    Ioa_ReadCollectTokens( vTokens, pLine, pCur );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Splits the line into tokens.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Ioa_ReadSplitIntoTokensAndClear( Vec_Ptr_t * vTokens, char * pLine, char Stop, char Char )
+{
+    char * pCur;
+    // clear spaces
+    for ( pCur = pLine; *pCur != Stop; pCur++ )
+        if ( Ioa_ReadCharIsSpace(*pCur) || *pCur == Char )
+            *pCur = 0;
+    // collect tokens
+    Ioa_ReadCollectTokens( vTokens, pLine, pCur );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the 1-based number of the line in which the token occurs.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Ioa_ReadGetLine( Ioa_ReadMan_t * p, char * pToken )
+{
+    char * pLine;
+    int i;
+    Vec_PtrForEachEntry( p->vLines, pLine, i )
+        if ( pToken < pLine )
+            return i;
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the file into a character buffer.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static char * Ioa_ReadLoadFile( char * pFileName )
+{
+    FILE * pFile;
+    int nFileSize;
+    char * pContents;
+    pFile = fopen( pFileName, "rb" );
+    if ( pFile == NULL )
+    {
+        printf( "Ioa_ReadLoadFile(): The file is unavailable (absent or open).\n" );
+        return NULL;
+    }
+    fseek( pFile, 0, SEEK_END );  
+    nFileSize = ftell( pFile ); 
+    if ( nFileSize == 0 )
+    {
+        printf( "Ioa_ReadLoadFile(): The file is empty.\n" );
+        return NULL;
+    }
+    pContents = ALLOC( char, nFileSize + 10 );
+    rewind( pFile );
+    fread( pContents, nFileSize, 1, pFile );
+    fclose( pFile );
+    // finish off the file with the spare .end line
+    // some benchmarks suddenly break off without this line
+    strcpy( pContents + nFileSize, "\n.end\n" );
+    return pContents;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the parsing.]
+
+  Description [Performs several preliminary operations:
+  - Cuts the file buffer into separate lines.
+  - Removes comments and line extenders.
+  - Sorts lines by directives.
+  - Estimates the number of objects.
+  - Allocates room for the objects.
+  - Allocates room for the hash table.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
+{
+    char * pCur, * pPrev;
+    int i, fComment = 0;
+    // parse the buffer into lines and remove comments
+    Vec_PtrPush( p->vLines, p->pBuffer );
+    for ( pCur = p->pBuffer; *pCur; pCur++ )
+    {
+        if ( *pCur == '\n' )
+        {
+            *pCur = 0;
+//            if ( *(pCur-1) == '\r' )
+//                *(pCur-1) = 0;
+            fComment = 0;
+            Vec_PtrPush( p->vLines, pCur + 1 );
+        }
+        else if ( *pCur == '#' )
+            fComment = 1;
+        // remove comments
+        if ( fComment )
+            *pCur = 0;
+    }
+
+    // unfold the line extensions and sort lines by directive
+    Vec_PtrForEachEntry( p->vLines, pCur, i )
+    {
+        if ( *pCur == 0 )
+            continue;
+        // find previous non-space character
+        for ( pPrev = pCur - 2; pPrev >= p->pBuffer; pPrev-- )
+            if ( !Ioa_ReadCharIsSpace(*pPrev) )
+                break;
+        // if it is the line extender, overwrite it with spaces
+        if ( *pPrev == '\\' )
+        {
+            for ( ; *pPrev; pPrev++ )
+                *pPrev = ' ';
+            *pPrev = ' ';
+            continue;
+        }
+        // skip spaces at the beginning of the line
+        while ( Ioa_ReadCharIsSpace(*pCur++) );
+        // parse directives
+        if ( *(pCur-1) != '.' )
+            continue;
+        if ( !strncmp(pCur, "names", 5) )
+            Vec_PtrPush( p->pLatest->vNames, pCur );
+        else if ( !strncmp(pCur, "latch", 5) )
+            Vec_PtrPush( p->pLatest->vLatches, pCur );
+        else if ( !strncmp(pCur, "inputs", 6) )
+            Vec_PtrPush( p->pLatest->vInputs, pCur );
+        else if ( !strncmp(pCur, "outputs", 7) )
+            Vec_PtrPush( p->pLatest->vOutputs, pCur );
+        else if ( !strncmp(pCur, "subckt", 6) )
+            Vec_PtrPush( p->pLatest->vSubckts, pCur );
+        else if ( !strncmp(pCur, "blackbox", 8) )
+            p->pLatest->fBlackBox = 1;
+        else if ( !strncmp(pCur, "model", 5) ) 
+        {
+            p->pLatest = Ioa_ReadModAlloc();
+            p->pLatest->pFirst = pCur;
+            p->pLatest->pMan = p;
+        }
+        else if ( !strncmp(pCur, "end", 3) )
+        {
+            if ( p->pLatest )
+                Vec_PtrPush( p->vModels, p->pLatest );
+            p->pLatest = NULL;
+        }
+        else if ( !strncmp(pCur, "exdc", 4) )
+        {
+            fprintf( stdout, "Line %d: Skipping EXDC network.\n", Ioa_ReadGetLine(p, pCur) );
+            break;
+        }
+        else
+        {
+            pCur--;
+            if ( pCur[strlen(pCur)-1] == '\r' )
+                pCur[strlen(pCur)-1] = 0;
+            fprintf( stdout, "Line %d: Skipping line \"%s\".\n", Ioa_ReadGetLine(p, pCur), pCur );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses interfaces of the models.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static void Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
+{
+    Ioa_ReadMod_t * pMod;
+    char * pLine;
+    int i, k;
+    // iterate through the models
+    Vec_PtrForEachEntry( p->vModels, pMod, i )
+    {
+        // parse the model
+        if ( !Ioa_ReadParseLineModel( pMod, pMod->pFirst ) )
+            return;
+        // parse the inputs
+        Vec_PtrForEachEntry( pMod->vInputs, pLine, k )
+            if ( !Ioa_ReadParseLineInputs( pMod, pLine ) )
+                return;
+        // parse the outputs
+        Vec_PtrForEachEntry( pMod->vOutputs, pLine, k )
+            if ( !Ioa_ReadParseLineOutputs( pMod, pLine ) )
+                return;
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static Ntl_Man_t * Ioa_ReadParse( Ioa_ReadMan_t * p )
+{
+    Ntl_Man_t * pDesign;
+    Ioa_ReadMod_t * pMod;
+    char * pLine;
+    int i, k;
+    // iterate through the models
+    Vec_PtrForEachEntry( p->vModels, pMod, i )
+    {
+        // parse the latches
+        Vec_PtrForEachEntry( pMod->vLatches, pLine, k )
+            if ( !Ioa_ReadParseLineLatch( pMod, pLine ) )
+                return NULL;
+        // parse the nodes
+        Vec_PtrForEachEntry( pMod->vNames, pLine, k )
+            if ( !Ioa_ReadParseLineNamesBlif( pMod, pLine ) )
+                return NULL;
+        // parse the subcircuits
+        Vec_PtrForEachEntry( pMod->vSubckts, pLine, k )
+            if ( !Ioa_ReadParseLineSubckt( pMod, pLine ) )
+                return NULL;
+        // finalize the network
+        Ntl_ModelFixNonDrivenNets( pMod->pNtk );
+    }
+    // return the network
+    pDesign = p->pDesign;
+    p->pDesign = NULL;
+    return pDesign;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses the model line.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine )
+{
+    Vec_Ptr_t * vTokens = p->pMan->vTokens;
+    char * pToken;
+    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
+    pToken = Vec_PtrEntry( vTokens, 0 );
+    assert( !strcmp(pToken, "model") );
+    if ( Vec_PtrSize(vTokens) != 2 )
+    {
+        sprintf( p->pMan->sError, "Line %d: Model line has %d entries while it should have 2.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
+        return 0;
+    }
+    p->pNtk = Ntl_ModelAlloc( p->pMan->pDesign, Vec_PtrEntry(vTokens, 1) );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses the inputs line.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLine )
+{
+    Ntl_Net_t * pNet;
+    Ntl_Obj_t * pObj;
+    Vec_Ptr_t * vTokens = p->pMan->vTokens;
+    char * pToken;
+    int i;
+    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
+    pToken = Vec_PtrEntry(vTokens, 0);
+    assert( !strcmp(pToken, "inputs") );
+    Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 )
+    {
+        pObj = Ntl_ModelCreatePi( p->pNtk );
+        pNet = Ntl_ModelFindOrCreateNet( p->pNtk, pToken );
+        if ( !Ntl_ModelSetNetDriver( pObj, pNet ) )
+        {
+            sprintf( p->pMan->sError, "Line %d: Net %s already has a driver.", Ioa_ReadGetLine(p->pMan, pToken), pNet->pName );
+            return 0;
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses the outputs line.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine )
+{
+    Ntl_Net_t * pNet;
+    Ntl_Obj_t * pObj;
+    Vec_Ptr_t * vTokens = p->pMan->vTokens;
+    char * pToken;
+    int i;
+    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
+    pToken = Vec_PtrEntry(vTokens, 0);
+    assert( !strcmp(pToken, "outputs") );
+    Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 )
+    {
+        pNet = Ntl_ModelFindOrCreateNet( p->pNtk, pToken );
+        pObj = Ntl_ModelCreatePo( p->pNtk, pNet );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses the latches line.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine )
+{
+    Vec_Ptr_t * vTokens = p->pMan->vTokens;
+    Ntl_Net_t * pNetLi, * pNetLo;
+    Ntl_Obj_t * pObj;
+    char * pToken, * pNameLi, * pNameLo;
+    int Init, Class;
+    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
+    pToken = Vec_PtrEntry(vTokens,0);
+    assert( !strcmp(pToken, "latch") );
+    if ( Vec_PtrSize(vTokens) < 3 )
+    {
+        sprintf( p->pMan->sError, "Line %d: Latch does not have input name and output name.", Ioa_ReadGetLine(p->pMan, pToken) );
+        return 0;
+    }
+    // create latch
+    pNameLi = Vec_PtrEntry( vTokens, 1 );
+    pNameLo = Vec_PtrEntry( vTokens, 2 );
+    pNetLi  = Ntl_ModelFindOrCreateNet( p->pNtk, pNameLi );
+    pNetLo  = Ntl_ModelFindOrCreateNet( p->pNtk, pNameLo );
+    pObj    = Ntl_ModelCreateLatch( p->pNtk );
+    pObj->pFanio[0] = pNetLi;
+    if ( !Ntl_ModelSetNetDriver( pObj, pNetLo ) )
+    {
+        sprintf( p->pMan->sError, "Line %d: Net %s already has a driver.", Ioa_ReadGetLine(p->pMan, pToken), pNetLo->pName );
+        return 0;
+    }
+    // get initial value
+    if ( Vec_PtrSize(vTokens) > 3 )
+        Init = atoi( Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-1) );
+    else
+        Init = 2;
+    if ( Init < 0 || Init > 2 )
+    {
+        sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) );
+        return 0;
+    }
+    // get the register class
+    if ( Vec_PtrSize(vTokens) == 6 )
+        Class = atoi( Vec_PtrEntry(vTokens,3) );
+    else
+        Class = 0;
+    if ( Class < 0 || Class > (1<<24) )
+    {
+        sprintf( p->pMan->sError, "Line %d: Class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,4) );
+        return 0;
+    }
+    pObj->LatchId = (Class << 2) | Init;
+    // get the clock
+    if ( Vec_PtrSize(vTokens) == 5 || Vec_PtrSize(vTokens) == 6 )
+    {
+        pToken = Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-2);
+        pNetLi = Ntl_ModelFindOrCreateNet( p->pNtk, pToken );
+        pObj->pFanio[1] = pNetLi;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses the subckt line.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine )
+{
+    Vec_Ptr_t * vTokens = p->pMan->vTokens;
+    Ntl_Mod_t * pModel;
+    Ntl_Obj_t * pBox, * pTerm;
+    Ntl_Net_t * pNet;
+    char * pToken, * pName, ** ppNames;
+    int nEquals, i, k;
+
+    // split the line into tokens
+    nEquals = Ioa_ReadCountChars( pLine, '=' );
+    Ioa_ReadSplitIntoTokensAndClear( vTokens, pLine, '\0', '=' );
+    pToken = Vec_PtrEntry(vTokens,0);
+    assert( !strcmp(pToken, "subckt") );
+
+    // get the model for this box
+    pName = Vec_PtrEntry(vTokens,1);
+    pModel = Ntl_ManFindModel( p->pMan->pDesign, pName );
+    if ( pModel == NULL )
+    {
+        sprintf( p->pMan->sError, "Line %d: Cannot find the model for subcircuit %s.", Ioa_ReadGetLine(p->pMan, pToken), pName );
+        return 0;
+    }
+
+    // check if the number of tokens is correct
+    if ( nEquals != Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) )
+    {
+        sprintf( p->pMan->sError, "Line %d: The number of ports (%d) in .subckt differs from the sum of PIs and POs of the model (%d).", 
+            Ioa_ReadGetLine(p->pMan, pToken), nEquals, Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) );
+        return 0;
+    }
+
+    // get the names
+    ppNames = (char **)Vec_PtrArray(vTokens) + 2;
+
+    // create the box with these terminals
+    pBox = Ntl_ModelCreateBox( p->pNtk, Ntl_ModelPiNum(pModel), Ntl_ModelPoNum(pModel) );
+    pBox->pImplem = pModel;
+    Ntl_ModelForEachPi( pModel, pTerm, i )
+    {
+        // find this terminal among the formal inputs of the subcircuit
+        pName = Ntl_ObjFanout0(pTerm)->pName;
+        for ( k = 0; k < nEquals; k++ )
+            if ( !strcmp( ppNames[2*k], pName ) )
+                break;
+        if ( k == nEquals )
+        {
+            sprintf( p->pMan->sError, "Line %d: Cannot find PI \"%s\" of the model \"%s\" as a formal input of the subcircuit.", 
+                Ioa_ReadGetLine(p->pMan, pToken), pName, pModel->pName );
+            return 0;
+        }
+        // create the BI with the actual name
+        pNet = Ntl_ModelFindOrCreateNet( p->pNtk, ppNames[2*k+1] );
+        Ntl_ObjSetFanin( pBox, pNet, i );
+    }
+    Ntl_ModelForEachPo( pModel, pTerm, i )
+    {
+        // find this terminal among the formal outputs of the subcircuit
+        pName = Ntl_ObjFanin0(pTerm)->pName;
+        for ( k = 0; k < nEquals; k++ )
+            if ( !strcmp( ppNames[2*k], pName ) )
+                break;
+        if ( k == nEquals )
+        {
+            sprintf( p->pMan->sError, "Line %d: Cannot find PO \"%s\" of the model \"%s\" as a formal output of the subcircuit.", 
+                Ioa_ReadGetLine(p->pMan, pToken), pName, pModel->pName );
+            return 0;
+        }
+        // create the BI with the actual name
+        pNet = Ntl_ModelFindOrCreateNet( p->pNtk, ppNames[2*k+1] );
+        Ntl_ObjSetFanout( pBox, pNet, i );
+    }
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs the SOP cover from the file parsing info.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static char * Ioa_ReadParseTableBlif( Ioa_ReadMod_t * p, char * pTable, int nFanins )
+{
+    Vec_Ptr_t * vTokens = p->pMan->vTokens;
+    Vec_Str_t * vFunc = p->pMan->vFunc;
+    char * pProduct, * pOutput;
+    int i, Polarity = -1;
+
+    p->pMan->nTablesRead++;
+    // get the tokens
+    Ioa_ReadSplitIntoTokens( vTokens, pTable, '.' );
+    if ( Vec_PtrSize(vTokens) == 0 )
+        return Ntl_ManStoreSop( p->pMan->pDesign, " 0\n" );
+    if ( Vec_PtrSize(vTokens) == 1 )
+    {
+        pOutput = Vec_PtrEntry( vTokens, 0 );
+        if ( ((pOutput[0] - '0') & 0x8E) || pOutput[1] )
+        {
+            sprintf( p->pMan->sError, "Line %d: Constant table has wrong output value \"%s\".", Ioa_ReadGetLine(p->pMan, pOutput), pOutput );
+            return NULL;
+        }
+        return Ntl_ManStoreSop( p->pMan->pDesign, (pOutput[0] == '0') ? " 0\n" : " 1\n" );
+    }
+    pProduct = Vec_PtrEntry( vTokens, 0 );
+    if ( Vec_PtrSize(vTokens) % 2 == 1 )
+    {
+        sprintf( p->pMan->sError, "Line %d: Table has odd number of tokens (%d).", Ioa_ReadGetLine(p->pMan, pProduct), Vec_PtrSize(vTokens) );
+        return NULL;
+    }
+    // parse the table
+    Vec_StrClear( vFunc );
+    for ( i = 0; i < Vec_PtrSize(vTokens)/2; i++ )
+    {
+        pProduct = Vec_PtrEntry( vTokens, 2*i + 0 );
+        pOutput  = Vec_PtrEntry( vTokens, 2*i + 1 );
+        if ( strlen(pProduct) != (unsigned)nFanins )
+        {
+            sprintf( p->pMan->sError, "Line %d: Cube \"%s\" has size different from the fanin count (%d).", Ioa_ReadGetLine(p->pMan, pProduct), pProduct, nFanins );
+            return NULL;
+        }
+        if ( ((pOutput[0] - '0') & 0x8E) || pOutput[1] )
+        {
+            sprintf( p->pMan->sError, "Line %d: Output value \"%s\" is incorrect.", Ioa_ReadGetLine(p->pMan, pProduct), pOutput );
+            return NULL;
+        }
+        if ( Polarity == -1 )
+            Polarity = pOutput[0] - '0';
+        else if ( Polarity != pOutput[0] - '0' )
+        {
+            sprintf( p->pMan->sError, "Line %d: Output value \"%s\" differs from the value in the first line of the table (%d).", Ioa_ReadGetLine(p->pMan, pProduct), pOutput, Polarity );
+            return NULL;
+        }
+        // parse one product 
+        Vec_StrAppend( vFunc, pProduct );
+        Vec_StrPush( vFunc, ' ' );
+        Vec_StrPush( vFunc, pOutput[0] );
+        Vec_StrPush( vFunc, '\n' );
+    }
+    Vec_StrPush( vFunc, '\0' );
+    return Vec_StrArray( vFunc );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Parses the nodes line.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static int Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine )
+{
+    Vec_Ptr_t * vTokens = p->pMan->vTokens;
+    Ntl_Obj_t * pNode;
+    Ntl_Net_t * pNetOut, * pNetIn;
+    char * pNameOut, * pNameIn;
+    int i;
+    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
+    // parse the mapped node
+//    if ( !strcmp(Vec_PtrEntry(vTokens,0), "gate") )
+//        return Ioa_ReadParseLineGateBlif( p, vTokens );
+    // parse the regular name line
+    assert( !strcmp(Vec_PtrEntry(vTokens,0), "names") );
+    pNameOut = Vec_PtrEntryLast( vTokens );
+/*
+    if ( strcmp( pNameOut, "18434" ) == 0 )
+    {
+        int x = 0;
+    }
+*/
+    pNetOut = Ntl_ModelFindOrCreateNet( p->pNtk, pNameOut );
+    // create fanins
+    pNode = Ntl_ModelCreateNode( p->pNtk, Vec_PtrSize(vTokens) - 2 );
+    for ( i = 0; i < Vec_PtrSize(vTokens) - 2; i++ )
+    {
+        pNameIn = Vec_PtrEntry(vTokens, i+1);
+        pNetIn = Ntl_ModelFindOrCreateNet( p->pNtk, pNameIn );
+        Ntl_ObjSetFanin( pNode, pNetIn, i );
+    }
+    if ( !Ntl_ModelSetNetDriver( pNode, pNetOut ) )
+    {
+        sprintf( p->pMan->sError, "Line %d: Signal \"%s\" is defined more than once.", Ioa_ReadGetLine(p->pMan, pNameOut), pNameOut );
+        return 0;
+    }
+    // parse the table of this node
+    pNode->pSop = Ioa_ReadParseTableBlif( p, pNameOut + strlen(pNameOut), pNode->nFanins );
+    if ( pNode->pSop == NULL )
+        return 0;
+    pNode->pSop = Ntl_ManStoreSop( p->pNtk->pMan, pNode->pSop );
+    return 1;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c
new file mode 100644
index 00000000..87048f10
--- /dev/null
+++ b/src/aig/ntl/ntlTable.c
@@ -0,0 +1,178 @@
+/**CFile****************************************************************
+
+  FileName    [ntlTable.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    [Name table manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlTable.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// hashing for strings
+static unsigned Ntl_HashString( char * pName, int TableSize ) 
+{
+    static int s_Primes[10] = { 
+        1291, 1699, 2357, 4177, 5147, 
+        5647, 6343, 7103, 7873, 8147
+    };
+    unsigned i, Key = 0;
+    for ( i = 0; pName[i] != '\0'; i++ )
+        Key ^= s_Primes[i%10]*pName[i]*pName[i];
+    return Key % TableSize;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates memory for the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Net_t * Ntl_ModelCreateNet( Ntl_Mod_t * p, char * pName )
+{
+    Ntl_Net_t * pNet;
+    pNet = (Ntl_Net_t *)Aig_MmFlexEntryFetch( p->pMan->pMemObjs, sizeof(Ntl_Net_t) + strlen(pName) + 1 );
+    memset( pNet, 0, sizeof(Ntl_Net_t) );
+    strcpy( pNet->pName, pName );
+    return pNet;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ModelTableResize( Ntl_Mod_t * p )
+{
+    Ntl_Net_t ** pTableNew, ** ppSpot, * pEntry, * pEntry2;
+    int nTableSizeNew, Counter, e, clk;
+clk = clock();
+    // get the new table size
+    nTableSizeNew = Aig_PrimeCudd( 3 * p->nTableSize ); 
+    // allocate a new array
+    pTableNew = ALLOC( Ntl_Net_t *, nTableSizeNew );
+    memset( pTableNew, 0, sizeof(Ntl_Net_t *) * nTableSizeNew );
+    // rehash entries 
+    Counter = 0;
+    for ( e = 0; e < p->nTableSize; e++ )
+        for ( pEntry = p->pTable[e], pEntry2 = pEntry? pEntry->pNext : NULL; 
+              pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNext : NULL )
+            {
+                ppSpot = pTableNew + Ntl_HashString( pEntry->pName, nTableSizeNew );
+                pEntry->pNext = *ppSpot;
+                *ppSpot = pEntry;
+                Counter++;
+            }
+    assert( Counter == p->nEntries );
+//    printf( "Increasing the structural table size from %6d to %6d. ", p->nTableSize, nTableSizeNew );
+//    PRT( "Time", clock() - clk );
+    // replace the table and the parameters
+    free( p->pTable );
+    p->pTable = pTableNew;
+    p->nTableSize = nTableSizeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds or creates the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName )
+{
+    Ntl_Net_t * pEnt;
+    unsigned Key = Ntl_HashString( pName, p->nTableSize );
+    for ( pEnt = p->pTable[Key]; pEnt; pEnt = pEnt->pNext )
+        if ( !strcmp( pEnt->pName, pName ) )
+            return pEnt;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds or creates the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName )
+{
+    Ntl_Net_t * pEnt;
+    unsigned Key = Ntl_HashString( pName, p->nTableSize );
+    for ( pEnt = p->pTable[Key]; pEnt; pEnt = pEnt->pNext )
+        if ( !strcmp( pEnt->pName, pName ) )
+            return pEnt;
+    pEnt = Ntl_ModelCreateNet( p, pName );
+    pEnt->pNext = p->pTable[Key];
+    p->pTable[Key] = pEnt;
+    if ( ++p->nEntries > 2 * p->nTableSize )
+        Ntl_ModelTableResize( p );
+    return pEnt;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds or creates the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet )
+{
+    if ( pObj->pFanio[pObj->nFanins] != NULL )
+        return 0;
+    if ( pNet->pDriver != NULL )
+        return 0;
+    pObj->pFanio[pObj->nFanins] = pNet;
+    pNet->pDriver = pObj;
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
new file mode 100644
index 00000000..8bcd2044
--- /dev/null
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -0,0 +1,127 @@
+/**CFile****************************************************************
+
+  FileName    [ntlWriteBlif.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Command processing package.]
+
+  Synopsis    [Procedures to write BLIF files.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntlWriteBlif.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+#include "ioa.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Writes one model into the BLIF file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
+{
+    Ntl_Obj_t * pObj;
+    Ntl_Net_t * pNet;
+    int i, k;
+    fprintf( pFile, ".model %s\n", pModel->pName );
+    fprintf( pFile, ".inputs" );
+    Ntl_ModelForEachPi( pModel, pObj, i )
+        fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
+    fprintf( pFile, "\n" );
+    fprintf( pFile, ".outputs" );
+    Ntl_ModelForEachPo( pModel, pObj, i )
+        fprintf( pFile, " %s", Ntl_ObjFanin0(pObj)->pName );
+    fprintf( pFile, "\n" );
+    Ntl_ModelForEachObj( pModel, pObj, i )
+    {
+        if ( Ntl_ObjIsNode(pObj) )
+        {
+            fprintf( pFile, ".names" );
+            Ntl_ObjForEachFanin( pObj, pNet, k )
+                fprintf( pFile, " %s", pNet->pName );
+            fprintf( pFile, " %s\n", Ntl_ObjFanout0(pObj)->pName );
+            fprintf( pFile, "%s", pObj->pSop );
+        }
+        else if ( Ntl_ObjIsLatch(pObj) )
+        {
+            fprintf( pFile, ".latch" );
+            fprintf( pFile, " %s", Ntl_ObjFanin0(pObj)->pName );
+            fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
+            if ( pObj->LatchId >> 2 )
+                fprintf( pFile, " %d", pObj->LatchId >> 2 );
+            if ( pObj->pFanio[1] != NULL )
+                fprintf( pFile, " %s", Ntl_ObjFanin(pObj, 1)->pName );
+            fprintf( pFile, " %d", pObj->LatchId & 3 );
+            fprintf( pFile, "\n" );
+        }
+        else if ( Ntl_ObjIsBox(pObj) )
+        {
+            fprintf( pFile, ".subckt %s", pObj->pImplem->pName );
+            Ntl_ObjForEachFanin( pObj, pNet, k )
+                fprintf( pFile, " %s=%s", Ntl_ModelPiName(pObj->pImplem, k), pNet->pName );
+            Ntl_ObjForEachFanout( pObj, pNet, k )
+                fprintf( pFile, " %s=%s", Ntl_ModelPoName(pObj->pImplem, k), pNet->pName );
+            fprintf( pFile, "\n" );
+        }
+    }
+    fprintf( pFile, ".end\n\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the network into the BLIF file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName )
+{
+    FILE * pFile;
+    Ntl_Mod_t * pModel;
+    int i;
+    // start the output stream
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Ioa_WriteBlif(): Cannot open the output file \"%s\".\n", pFileName );
+        return;
+    }
+    fprintf( pFile, "# Benchmark \"%s\" written by ABC-8 on %s\n", p->pName, Ioa_TimeStamp() );
+    // write the models
+    Ntl_ManForEachModel( p, pModel, i )
+        Ioa_WriteBlifModel( pFile, pModel );
+    // close the file
+    fclose( pFile );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntl_.c b/src/aig/ntl/ntl_.c
new file mode 100644
index 00000000..4b3ad684
--- /dev/null
+++ b/src/aig/ntl/ntl_.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [ntl_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Netlist representation.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: ntl_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3b238779..98dcde81 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -184,6 +184,8 @@ static int Abc_CommandProve          ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandIProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDebug          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBmc            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandIndcut         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandEnlarge        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandTraceStart     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTraceCheck     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -355,6 +357,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "iprove",        Abc_CommandIProve,           1 );
     Cmd_CommandAdd( pAbc, "Verification", "debug",         Abc_CommandDebug,            0 );
     Cmd_CommandAdd( pAbc, "Verification", "bmc",           Abc_CommandBmc,              0 );
+    Cmd_CommandAdd( pAbc, "Verification", "indcut",        Abc_CommandIndcut,           0 );
+    Cmd_CommandAdd( pAbc, "Verification", "enlarge",       Abc_CommandEnlarge,          1 );
 
 //    Cmd_CommandAdd( pAbc, "Verification", "trace_start",   Abc_CommandTraceStart,       0 );
 //    Cmd_CommandAdd( pAbc, "Verification", "trace_check",   Abc_CommandTraceCheck,       0 );
@@ -6210,12 +6214,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
     extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
     extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
-    extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int fVerbose, int fVeryVerbose );
+    extern void Abc_NtkDarTestBlif( char * pFileName );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
+//    printf( "This command is temporarily disabled.\n" );
+//    return 0;
+
     // set defaults
     fVeryVerbose = 0;
     fVerbose = 1;
@@ -6351,13 +6358,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 */
-
+/*
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
         return 0;
     }
-
+*/
 /*
     if ( Abc_NtkIsStrash(pNtk) )
     {
@@ -6378,7 +6385,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
 */
 //    Abc_NtkDarHaigRecord( pNtk );
-    Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
+//    Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
+
+    if ( globalUtilOptind != 1 )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 1;
+    }
+    Abc_NtkDarTestBlif( argv[globalUtilOptind] );
     return 0;
 usage:
     fprintf( pErr, "usage: test [-vwh]\n" );
@@ -11302,7 +11316,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( Abc_NtkIsComb(pNtk) )
     {
         fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
-        return 1;
+        return 0;
     }
 
     if ( !Abc_NtkIsStrash(pNtk) )
@@ -11523,7 +11537,6 @@ usage:
     fprintf( pErr, "\t         - removes nodes/latches that do not feed into POs\n" );
     fprintf( pErr, "\t         - removes stuck-at and identical latches (latch sweep)\n" );
 //    fprintf( pErr, "\t         - replaces autonomous logic by free PI variables\n" );
-    fprintf( pErr, "\t           (the latter may change sequential behaviour)\n" );
     fprintf( pErr, "\t-l     : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" );
 //    fprintf( pErr, "\t-a     : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -12390,11 +12403,11 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     fVerbose     =  0;
     fVeryVerbose =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Krwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'K':
+        case 'F':
             if ( globalUtilOptind >= argc )
             {
                 fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
@@ -12435,9 +12448,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dprove [-K num] [-rwvh]\n" );
+    fprintf( pErr, "usage: dprove [-F num] [-rwvh]\n" );
     fprintf( pErr, "\t         performs SEC on the sequential miter\n" );
-    fprintf( pErr, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrames );
     fprintf( pErr, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
     fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
@@ -13031,6 +13044,217 @@ usage:
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandIndcut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int nFrames;
+    int nPref;
+    int nClauses;
+    int fBmc;
+    int fRegs;
+    int fVerbose;
+    int fVeryVerbose;
+    int c;
+    extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int fBmc, int fRegs, int fVerbose, int fVeryVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames      = 1;
+    nPref        = 0;
+    nClauses     = 5000;
+    fBmc         = 1;
+    fRegs        = 1;
+    fVerbose     = 0;
+    fVeryVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FPCbrvwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPref = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPref < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nClauses = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nClauses < 0 ) 
+                goto usage;
+            break;
+        case 'b':
+            fBmc ^= 1;
+            break;
+        case 'r':
+            fRegs ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "Only works for sequential networks.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+        return 0;
+    }
+    Abc_NtkDarClau( pNtk, nFrames, nPref, nClauses, fBmc, fRegs, fVerbose, fVeryVerbose );
+    return 0;
+usage:
+    fprintf( pErr, "usage: indcut [-F num] [-P num] [-C num] [-bvh]\n" );
+    fprintf( pErr, "\t         K-step induction strengthened with cut properties\n" );
+    fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-P num : number of time frames in the prefix (0=no prefix) [default = %d]\n", nPref );
+    fprintf( pErr, "\t-C num : the max number of clauses to use for strengthening [default = %d]\n", nClauses );
+    fprintf( pErr, "\t-b     : toggle enabling BMC check [default = %s]\n", fBmc? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggle enabling register clauses [default = %s]\n", fRegs? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+//    fprintf( pErr, "\t-w     : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandEnlarge( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int nFrames;
+    int fVerbose;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames      = 5;
+    fVerbose     = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "Only works for sequential networks.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+        return 0;
+    }
+
+    // modify the current network
+    pNtkRes = Abc_NtkDarEnlarge( pNtk, nFrames, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Target enlargement has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+usage:
+    fprintf( pErr, "usage: enlarge [-F num] [-vh]\n" );
+    fprintf( pErr, "\t         performs structural K-step target enlargement\n" );
+    fprintf( pErr, "\t-F num : the number of timeframes for enlargement [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
 
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index e23b04dd..62fc869c 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -211,6 +211,18 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 //    assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
     // perform strashing
     pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // consider the case of target enlargement
+    if ( Abc_NtkCiNum(pNtkNew) < Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) )
+    {
+        for ( i = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) - Abc_NtkCiNum(pNtkNew); i > 0; i-- )
+        {
+            pObjNew = Abc_NtkCreatePi( pNtkNew );
+            Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
+        }
+        Abc_NtkOrderCisCos( pNtkNew );
+    }
+    assert( Abc_NtkCiNum(pNtkNew) == Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan) );
+    assert( Abc_NtkCoNum(pNtkNew) == Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) );
     // transfer the pointers to the basic nodes
     Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
     Aig_ManForEachPiSeq( pMan, pObj, i )
@@ -1040,7 +1052,13 @@ PRT( "Initial fraiging time", clock() - clk );
     if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
         pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
     else
+    {
+        Abc_Obj_t * pObj;
+        int i;
         pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+        Abc_NtkForEachLatch( pNtkAig, pObj, i )
+            Abc_LatchSetInit0( pObj );
+    }
     Aig_ManStop( pMan );
     return pNtkAig;
 }
@@ -1068,7 +1086,13 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
     if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
         pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
     else
+    {
+        Abc_Obj_t * pObj;
+        int i;
         pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+        Abc_NtkForEachLatch( pNtkAig, pObj, i )
+            Abc_LatchSetInit0( pObj );
+    }
     Aig_ManStop( pMan );
     return pNtkAig;
 }
@@ -1409,10 +1433,10 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int fVerbose, int fVeryVerbose )
+int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int fBmc, int fRefs, int fVerbose, int fVeryVerbose )
 {
     extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose );
-    extern int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nClauses, int fBmc, int fVerbose, int fVeryVerbose );
+    extern int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClauses, int fBmc, int fRefs, int fVerbose, int fVeryVerbose );
     Aig_Man_t * pMan;
     if ( Abc_NtkPoNum(pNtk) != 1 )
     {
@@ -1428,11 +1452,70 @@ int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int
     pMan->vFlopNums = NULL;
 
 //    Fra_Clau( pMan, nStepsMax, fVerbose, fVeryVerbose );
-    Fra_Claus( pMan, nFrames, nStepsMax, fBmc, fVerbose, fVeryVerbose );
+    Fra_Claus( pMan, nFrames, nPref, nClauses, fBmc, fRefs, fVerbose, fVeryVerbose );
     Aig_ManStop( pMan );
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs targe enlargement.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Aig_ManFrames( pTemp = pMan, nFrames, 0, 1, 1, 1, NULL );
+    Aig_ManStop( pTemp );
+    pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+
+#include "ntl.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Performs targe enlargement.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDarTestBlif( char * pFileName )
+{
+    char Buffer[1000];
+    Ntl_Man_t * p;
+    p = Ioa_ReadBlif( pFileName, 1 );
+    if ( p == NULL )
+    {
+        printf( "Abc_NtkDarTestBlif(): Reading BLIF has failed.\n" );
+        return;
+    }
+    if ( !Ntl_ManInsertTest( p ) )
+    {
+        printf( "Abc_NtkDarTestBlif(): Tranformation of the netlist has failed.\n" );
+        return;
+    }
+    sprintf( Buffer, "%s_.blif", p->pName );
+    Ioa_WriteBlif( p, Buffer );
+    Ntl_ManFree( p );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index d2b77ed2..b925f1b9 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -84,6 +84,7 @@ static Dec_Graph_t *  Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec
 ***********************************************************************/
 int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose )
 {
+    extern void           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
     ProgressBar * pProgress;
     Abc_ManRef_t * pManRef;
     Abc_ManCut_t * pManCut;
@@ -183,6 +184,7 @@ pManRef->timeTotal = clock() - clkStart;
 ***********************************************************************/
 Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose )
 {
+    extern int            Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
     int fVeryVerbose = 0;
     Abc_Obj_t * pFanin;
     Dec_Graph_t * pFForm;
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index 326d1543..aa9a2998 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -96,6 +96,7 @@ static void Abc_NtkManRstPrintStats( Abc_ManRst_t * p );
 ***********************************************************************/
 int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose )
 {
+    extern void           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
     ProgressBar * pProgress;
     Abc_ManRst_t * pManRst;
     Cut_Man_t * pManCut;
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index 309c328d..a2b23c0c 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -139,6 +139,7 @@ extern int s_ResubTime;
 ***********************************************************************/
 int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLevelsOdc, bool fUpdateLevel, bool fVerbose, bool fVeryVerbose )
 {
+    extern void           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
     ProgressBar * pProgress;
     Abc_ManRes_t * pManRes;
     Abc_ManCut_t * pManCut;
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index b615f47e..3b50107b 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -57,6 +57,7 @@ extern void  Abc_PlaceUpdate( Vec_Ptr_t * vAddedCells, Vec_Ptr_t * vUpdatedNets
 ***********************************************************************/
 int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable )
 {
+    extern void           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
     ProgressBar * pProgress;
     Cut_Man_t * pManCut;
     Rwr_Man_t * pManRwr;
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index 27638644..ddc92cc8 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -264,6 +264,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
 ***********************************************************************/
 Abc_Obj_t * Seq_NodeRetimeDerive( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pRoot, char * pSop, Vec_Ptr_t * vFanins )
 {
+    extern Abc_Obj_t *    Dec_GraphToNetworkNoStrash( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
     Dec_Graph_t * pFForm;
     Dec_Node_t * pNode;
     Abc_Obj_t * pResult, * pFanin, * pMirror;
diff --git a/src/map/fpga/fpgaInt.h b/src/map/fpga/fpgaInt.h
index b93eacab..c01d1e3d 100644
--- a/src/map/fpga/fpgaInt.h
+++ b/src/map/fpga/fpgaInt.h
@@ -184,8 +184,8 @@ struct Fpga_NodeStruct_t_
     Fpga_Node_t *       pLevel;        // the next node in the linked list by level
     int                 Num;           // the unique number of this node
     int                 NumA;          // the unique number of this node
-    short               Num2;          // the temporary number of this node
-    short               nRefs;         // the number of references (fanouts) of the given node
+    int                 Num2;          // the temporary number of this node
+    int                 nRefs;         // the number of references (fanouts) of the given node
     unsigned            fMark0 : 1;    // the mark used for traversals
     unsigned            fMark1 : 1;    // the mark used for traversals
     unsigned            fInv   : 1;    // the complemented attribute for the equivalent nodes
diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h
index 41d22649..d0d9981d 100644
--- a/src/opt/dec/dec.h
+++ b/src/opt/dec/dec.h
@@ -103,10 +103,6 @@ struct Dec_Man_t_
 ////////////////////////////////////////////////////////////////////////
 
 /*=== decAbc.c ========================================================*/
-extern Abc_Obj_t *    Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
-extern Abc_Obj_t *    Dec_GraphToNetworkNoStrash( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
-extern int            Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
-extern void           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain );
 /*=== decFactor.c ========================================================*/
 extern Dec_Graph_t *  Dec_Factor( char * pSop );
 /*=== decMan.c ========================================================*/
@@ -115,7 +111,6 @@ extern void           Dec_ManStop( Dec_Man_t * p );
 /*=== decPrint.c ========================================================*/
 extern void           Dec_GraphPrint( FILE * pFile, Dec_Graph_t * pGraph, char * pNamesIn[], char * pNameOut );
 /*=== decUtil.c ========================================================*/
-extern DdNode *       Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph );
 extern unsigned       Dec_GraphDeriveTruth( Dec_Graph_t * pGraph );
 
 ////////////////////////////////////////////////////////////////////////
@@ -317,7 +312,7 @@ static inline void Dec_GraphFree( Dec_Graph_t * pGraph )
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_GraphIsConst( Dec_Graph_t * pGraph )   
+static inline int Dec_GraphIsConst( Dec_Graph_t * pGraph )   
 {
     return pGraph->fConst;
 }
@@ -333,7 +328,7 @@ static inline bool Dec_GraphIsConst( Dec_Graph_t * pGraph )
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_GraphIsConst0( Dec_Graph_t * pGraph )   
+static inline int Dec_GraphIsConst0( Dec_Graph_t * pGraph )   
 {
     return pGraph->fConst && pGraph->eRoot.fCompl;
 }
@@ -349,7 +344,7 @@ static inline bool Dec_GraphIsConst0( Dec_Graph_t * pGraph )
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_GraphIsConst1( Dec_Graph_t * pGraph )   
+static inline int Dec_GraphIsConst1( Dec_Graph_t * pGraph )   
 {
     return pGraph->fConst && !pGraph->eRoot.fCompl;
 }
@@ -365,7 +360,7 @@ static inline bool Dec_GraphIsConst1( Dec_Graph_t * pGraph )
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_GraphIsComplement( Dec_Graph_t * pGraph )   
+static inline int Dec_GraphIsComplement( Dec_Graph_t * pGraph )   
 {
     return pGraph->eRoot.fCompl;
 }
@@ -478,7 +473,7 @@ static inline int Dec_GraphNodeInt( Dec_Graph_t * pGraph, Dec_Node_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_GraphIsVar( Dec_Graph_t * pGraph )   
+static inline int Dec_GraphIsVar( Dec_Graph_t * pGraph )   
 {
     return pGraph->eRoot.Node < (unsigned)pGraph->nLeaves;
 }
@@ -494,7 +489,7 @@ static inline bool Dec_GraphIsVar( Dec_Graph_t * pGraph )
   SeeAlso     []
 
 ***********************************************************************/
-static inline bool Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode )   
+static inline int Dec_GraphNodeIsVar( Dec_Graph_t * pGraph, Dec_Node_t * pNode )   
 {
     return Dec_GraphNodeInt(pGraph,pNode) < pGraph->nLeaves;
 }
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
index bd960c14..6adb0f98 100644
--- a/src/opt/dec/decAbc.c
+++ b/src/opt/dec/decAbc.c
@@ -189,6 +189,7 @@ int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa
 ***********************************************************************/
 void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain )
 {
+    extern Abc_Obj_t *    Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
     Abc_Obj_t * pRootNew;
     Abc_Ntk_t * pNtk = pRoot->pNtk;
     int nNodesNew, nNodesOld;
diff --git a/src/opt/dec/decFactor.c b/src/opt/dec/decFactor.c
index dca422ea..768dcd9b 100644
--- a/src/opt/dec/decFactor.c
+++ b/src/opt/dec/decFactor.c
@@ -364,6 +364,7 @@ Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
 ***********************************************************************/
 int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm )
 {
+    extern DdNode *       Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph );
     DdManager * dd = Abc_FrameReadManDd();
     DdNode * bFunc1, * bFunc2;
     int RetValue;
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index 0eb547f2..396a659c 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -245,6 +245,7 @@ p->timeRes += clock() - clk;
 ***********************************************************************/
 Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, int fPlaceEnable )
 {
+    extern int            Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
     Vec_Ptr_t * vSubgraphs;
     Dec_Graph_t * pGraphBest, * pGraphCur;
     Rwr_Node_t * pNode, * pFanin;