Version abc70710

18 files changed, 417 insertions, 125 deletions

diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index 147cd38f..23563766 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -64,10 +64,6 @@ int Dar_ManRewrite( Dar_Man_t * p )
             continue;
         if ( i > nNodesOld )
             break;
-        if ( pObj->Id == 654 )
-        {
-            int x = 0;
-        }
         // compute cuts for the node
 clk = clock();
         pCutSet = Dar_ObjComputeCuts_rec( p, pObj );
diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c
index 25b15e9c..52df8890 100644
--- a/src/aig/dar/darMan.c
+++ b/src/aig/dar/darMan.c
@@ -94,7 +94,7 @@ Dar_Man_t * Dar_ManStartFrom( Dar_Man_t * p )
     Dar_Obj_t * pObj;
     int i;
     // create the new manager
-    pNew = Dar_ManStart();
+    pNew = Dar_ManStart( Dar_ManObjIdMax(p) + 1 );
     // create the PIs
     Dar_ManConst1(p)->pData = Dar_ManConst1(pNew);
     Dar_ManForEachPi( p, pObj, i )
@@ -119,7 +119,7 @@ Dar_Man_t * Dar_ManDup( Dar_Man_t * p )
     Dar_Obj_t * pObj;
     int i;
     // create the new manager
-    pNew = Dar_ManStart();
+    pNew = Dar_ManStart( Dar_ManObjIdMax(p) + 1 );
     // create the PIs
     Dar_ManConst1(p)->pData = Dar_ManConst1(pNew);
     Dar_ManForEachPi( p, pObj, i )
diff --git a/src/aig/dar/module.make b/src/aig/dar/module.make
index e258757f..4bf473d4 100644
--- a/src/aig/dar/module.make
+++ b/src/aig/dar/module.make
@@ -9,5 +9,7 @@ SRC +=    src/aig/dar/darBalance.c \
     src/aig/dar/darMem.c \
     src/aig/dar/darObj.c \
     src/aig/dar/darOper.c \
+    src/aig/dar/darSeq.c \
     src/aig/dar/darTable.c \
+    src/aig/dar/darTruth.c \
     src/aig/dar/darUtil.c 
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 41d8692d..ee52520a 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -142,14 +142,14 @@ static inline Dar_Obj_t *  Fra_ObjRepr( Dar_Obj_t * pObj )
 static inline Vec_Ptr_t *  Fra_ObjFaninVec( Dar_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];      }
 static inline int          Fra_ObjSatNum( Dar_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];     }
 
-static inline Dar_Obj_t *  Fra_ObjChild0Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin0(pObj)), Dar_ObjFaninC0(pObj)) : NULL;  }
-static inline Dar_Obj_t *  Fra_ObjChild1Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin1(pObj)), Dar_ObjFaninC1(pObj)) : NULL;  }
-
 static inline void         Fra_ObjSetFraig( Dar_Obj_t * pObj, Dar_Obj_t * pNode )        { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]   = pNode;    }
 static inline void         Fra_ObjSetRepr( Dar_Obj_t * pObj, Dar_Obj_t * pNode )         { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]    = pNode;    }
 static inline void         Fra_ObjSetFaninVec( Dar_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]  = vFanins;  }
 static inline void         Fra_ObjSetSatNum( Dar_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;      }
 
+static inline Dar_Obj_t *  Fra_ObjChild0Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin0(pObj)), Dar_ObjFaninC0(pObj)) : NULL;  }
+static inline Dar_Obj_t *  Fra_ObjChild1Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin1(pObj)), Dar_ObjFaninC1(pObj)) : NULL;  }
+
 ////////////////////////////////////////////////////////////////////////
 ///                         ITERATORS                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -161,6 +161,7 @@ static inline void         Fra_ObjSetSatNum( Dar_Obj_t * pObj, int Num )
 /*=== fraAnd.c ========================================================*/
 extern void                Fra_Sweep( Fra_Man_t * p );
 /*=== fraClass.c ========================================================*/
+extern void                Fra_PrintClasses( Fra_Man_t * p );
 extern void                Fra_CreateClasses( Fra_Man_t * p );
 extern int                 Fra_RefineClasses( Fra_Man_t * p );
 extern int                 Fra_RefineClasses1( Fra_Man_t * p );
@@ -171,6 +172,7 @@ extern Dar_Man_t *         Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pParams
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern Fra_Man_t *         Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pParams );
+extern void                Fra_ManPrepare( Fra_Man_t * p );
 extern void                Fra_ManStop( Fra_Man_t * p );
 extern void                Fra_ManPrint( Fra_Man_t * p );
 /*=== fraSat.c ========================================================*/
diff --git a/src/aig/fra/fraAnd.c b/src/aig/fra/fraAnd.c
index 333ef1b1..86cbbc9e 100644
--- a/src/aig/fra/fraAnd.c
+++ b/src/aig/fra/fraAnd.c
@@ -51,14 +51,15 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
     pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
     // get the fraiged node
     pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
+    Dar_Regular(pObjFraig)->pData = p;
     // get representative of this class
     pObjOldRepr = Fra_ObjRepr(pObjOld);
     if ( pObjOldRepr == NULL || // this is a unique node
        (!p->pPars->fDoSparse && pObjOldRepr == Dar_ManConst1(p->pManAig)) ) // this is a sparse node
     {
         assert( Dar_Regular(pFanin0Fraig) != Dar_Regular(pFanin1Fraig) );
-        assert( pObjFraig != Dar_Regular(pFanin0Fraig) );
-        assert( pObjFraig != Dar_Regular(pFanin1Fraig) );
+        assert( Dar_Regular(pObjFraig) != Dar_Regular(pFanin0Fraig) );
+        assert( Dar_Regular(pObjFraig) != Dar_Regular(pFanin1Fraig) );
         return pObjFraig;
     }
     // get the fraiged representative
@@ -67,11 +68,13 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
     if ( Dar_Regular(pObjFraig) == Dar_Regular(pObjOldReprFraig) )
         return pObjFraig;
     assert( Dar_Regular(pObjFraig) != Dar_ManConst1(p->pManFraig) );
+//    printf( "Node = %d. Repr = %d.\n", pObjOld->Id, pObjOldRepr->Id );
+
     // if they are proved different, the c-ex will be in p->pPatWords
     RetValue = Fra_NodesAreEquiv( p, Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) );
     if ( RetValue == 1 )  // proved equivalent
     {
-        pObjOld->fMarkA = 1;
+//        pObjOld->fMarkA = 1;
         return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
     }
     if ( RetValue == -1 ) // failed
@@ -79,11 +82,12 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
         if ( !p->pPars->fSpeculate )
             return pObjFraig;
         // substitute the node
-        pObjOld->fMarkB = 1;
+//        pObjOld->fMarkB = 1;
         return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
     }
     // simulate the counter-example and return the Fraig node
     Fra_Resimulate( p );
+    assert( Fra_ObjRepr(pObjOld) != pObjOldRepr );
     return pObjFraig;
 }
 
@@ -103,7 +107,7 @@ void Fra_Sweep( Fra_Man_t * p )
     Dar_Obj_t * pObj, * pObjNew;
     int i, k = 0;
 p->nClassesZero = Vec_PtrSize(p->vClasses1);
-p->nClassesBeg  = Vec_PtrSize(p->vClasses);
+p->nClassesBeg  = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
     // duplicate internal nodes
 //    p->pProgress = Extra_ProgressBarStart( stdout, Dar_ManNodeNum(p->pManAig) );
     Dar_ManForEachNode( p->pManAig, pObj, i )
@@ -114,11 +118,11 @@ p->nClassesBeg  = Vec_PtrSize(p->vClasses);
             pObjNew = Dar_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
         else
             pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented
-        assert( Fra_ObjFraig(pObj) != NULL );
         Fra_ObjSetFraig( pObj, pObjNew );
+        assert( Fra_ObjFraig(pObj) != NULL );
     }
 //    Extra_ProgressBarStop( p->pProgress );
-p->nClassesEnd = Vec_PtrSize(p->vClasses);
+p->nClassesEnd = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
     // try to prove the outputs of the miter
     p->nNodesMiter = Dar_ManNodeNum(p->pManFraig);
 //    Fra_MiterStatus( p->pManFraig );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 1f2fc165..ac6a4f4a 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -25,6 +25,7 @@
     to the array of pointers to the nodes in each class.
     The first node of the class is its representative node.
     The representative has the smallest topological order among the class nodes.
+    The nodes inside each class are ordered according to their topological order.
     The classes are ordered according to the topological order of their representatives.
     The array of pointers to the class nodes is terminated with a NULL pointer.
     To enable dynamic addition of new classes (during class refinement),
@@ -35,12 +36,55 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static inline Dar_Obj_t *  Fra_ObjNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pObj )                       { return ppNexts[pObj->Id];  }
+static inline void         Fra_ObjSetNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pObj, Dar_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Prints simulation classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_PrintClass( Dar_Obj_t ** pClass )
+{
+    Dar_Obj_t * pTemp;
+    int i;
+    printf( "{ " );
+    for ( i = 0; pTemp = pClass[i]; i++ )
+        printf( "%d ", pTemp->Id );
+    printf( "}\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints simulation classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_CountClass( Dar_Obj_t ** pClass )
+{
+    Dar_Obj_t * pTemp;
+    int i;
+    for ( i = 0; pTemp = pClass[i]; i++ );
+    return i;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Count the number of pairs.]
 
   Description []
@@ -56,22 +100,40 @@ int Fra_CountPairsClasses( Fra_Man_t * p )
     int i, nNodes, nPairs = 0;
     Vec_PtrForEachEntry( p->vClasses, pClass, i )
     {
-        for ( nNodes = 0; pClass[nNodes]; nNodes++ )
-        {
-            if ( nNodes > DAR_INFINITY )
-            {
-                printf( "Error in equivalence classes.\n" );
-                break;
-            }
-        }
-        nPairs += (nNodes - 1) * (nNodes - 2) / 2;
+        nNodes = Fra_CountClass( pClass );
+        assert( nNodes > 1 );
+        nPairs += nNodes * (nNodes - 1) / 2;
     }
     return nPairs;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes hash value using simulation info.]
+  Synopsis    [Prints simulation classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_PrintClasses( Fra_Man_t * p )
+{
+    Dar_Obj_t ** pClass;
+    int i;
+    printf( "Total classes = %d. Total pairs = %d.\n", Vec_PtrSize(p->vClasses), Fra_CountPairsClasses(p) );
+    Vec_PtrForEachEntry( p->vClasses, pClass, i )
+    {
+//        printf( "%3d (%3d) : ", Fra_CountClass(pClass) );
+//        Fra_PrintClass( pClass );
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes hash value of the node using its simulation info.]
 
   Description []
                
@@ -102,7 +164,7 @@ unsigned Fra_NodeHash( Fra_Man_t * p, Dar_Obj_t * pObj )
     int i;
     assert( p->nSimWords <= 128 );
     uHash = 0;
-    pSims  = Fra_ObjSim(pObj);
+    pSims = Fra_ObjSim(pObj);
     for ( i = 0; i < p->nSimWords; i++ )
         uHash ^= pSims[i] * s_FPrimes[i];
     return uHash;
@@ -110,7 +172,7 @@ unsigned Fra_NodeHash( Fra_Man_t * p, Dar_Obj_t * pObj )
 
 /**Function********************************************************************
 
-  Synopsis    [Returns the next prime &gt;= p.]
+  Synopsis    [Returns the next prime >= p.]
 
   Description [Copied from CUDD, for stand-aloneness.]
 
@@ -158,18 +220,21 @@ unsigned int Cudd_PrimeFra( unsigned int p )
 ***********************************************************************/
 void Fra_CreateClasses( Fra_Man_t * p )
 {
-    Dar_Obj_t ** pTable;
-    Dar_Obj_t * pObj;
-    int i, k, k2, nTableSize, nEntries, iEntry;
-    // allocate the table
-    nTableSize = Cudd_PrimeFra( Dar_ManNodeNum(p->pManAig) );
-    pTable = ALLOC( Dar_Obj_t *, nTableSize ); 
-    memset( pTable, 0, sizeof(Dar_Obj_t *) * nTableSize );
-    // collect nodes into the table
+    Dar_Obj_t ** ppTable, ** ppNexts;
+    Dar_Obj_t * pObj, * pTemp;
+    int i, k, nTableSize, nEntries, nNodes, iEntry;
+
+    // allocate the hash table hashing simulation info into nodes
+    nTableSize = Cudd_PrimeFra( Dar_ManObjIdMax(p->pManAig) + 1 );
+    ppTable = ALLOC( Dar_Obj_t *, nTableSize ); 
+    ppNexts = ALLOC( Dar_Obj_t *, nTableSize ); 
+    memset( ppTable, 0, sizeof(Dar_Obj_t *) * nTableSize );
+
+    // add all the nodes to the hash table
     Vec_PtrClear( p->vClasses1 );
     Dar_ManForEachObj( p->pManAig, pObj, i )
     {
-        if ( !Dar_ObjIsPi(pObj) && !Dar_ObjIsNode(pObj) )
+        if ( !Dar_ObjIsNode(pObj) && !Dar_ObjIsPi(pObj) )
             continue;
         // hash the node by its simulation info
         iEntry = Fra_NodeHash( p, pObj ) % nTableSize;
@@ -177,52 +242,80 @@ void Fra_CreateClasses( Fra_Man_t * p )
         if ( iEntry == 0 && Fra_NodeHasZeroSim( p, pObj ) )
         {
             Vec_PtrPush( p->vClasses1, pObj );
+            Fra_ObjSetRepr( pObj, Dar_ManConst1(p->pManAig) );
             continue;
         }
-        // add the node to the table
-        pObj->pData = pTable[iEntry];
-        pTable[iEntry] = pObj;
+        // add the node to the class
+        if ( ppTable[iEntry] == NULL )
+        {
+            ppTable[iEntry] = pObj;
+            Fra_ObjSetNext( ppNexts, pObj, pObj );
+        }
+        else
+        {
+            Fra_ObjSetNext( ppNexts, pObj, Fra_ObjNext(ppNexts,ppTable[iEntry]) );
+            Fra_ObjSetNext( ppNexts, ppTable[iEntry], pObj );
+        }
     }
+
     // count the total number of nodes in the non-trivial classes
+    // mark the representative nodes of each equivalence class
     nEntries = 0;
     for ( i = 0; i < nTableSize; i++ )
-        if ( pTable[i] && pTable[i]->pData )
+        if ( ppTable[i] && ppTable[i] != Fra_ObjNext(ppNexts, ppTable[i]) )
         {
-            k = 0;
-            for ( pObj = pTable[i]; pObj; pObj = pObj->pData )
-                k++;
-            nEntries += 2*k;
+            for ( pTemp = Fra_ObjNext(ppNexts, ppTable[i]), k = 1; 
+                  pTemp != ppTable[i]; 
+                  pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
+            assert( k > 1 );
+            nEntries += k;
+            // mark the node
+            assert( ppTable[i]->fMarkA == 0 );
+            ppTable[i]->fMarkA = 1;
         }
+
     // allocate room for classes
-    p->pMemClasses = ALLOC( Dar_Obj_t *, nEntries + 2*Vec_PtrSize(p->vClasses1) );
-    p->pMemClassesFree = p->pMemClasses + nEntries;
-    // copy the entries into storage
+    p->pMemClasses = ALLOC( Dar_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
+    p->pMemClassesFree = p->pMemClasses + 2*nEntries;
+
+    // copy the entries into storage in the topological order
     Vec_PtrClear( p->vClasses );
     nEntries = 0;
-    for ( i = 0; i < nTableSize; i++ )
-        if ( pTable[i] && pTable[i]->pData )
+    Dar_ManForEachObj( p->pManAig, pObj, i )
+    {
+        if ( !Dar_ObjIsNode(pObj) && !Dar_ObjIsPi(pObj) )
+            continue;
+        // skip the nodes that are not representatives of non-trivial classes
+        if ( pObj->fMarkA == 0 )
+            continue;
+        pObj->fMarkA = 0;
+        // add the class of nodes
+        Vec_PtrPush( p->vClasses, p->pMemClasses + 2*nEntries );
+        // count the number of entries in this class
+        for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 
+              pTemp != pObj; 
+              pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
+        nNodes = k;
+        assert( nNodes > 1 );
+        // add the nodes to the class in the topological order
+        p->pMemClasses[2*nEntries] = pObj;
+        for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 
+              pTemp != pObj; 
+              pTemp = Fra_ObjNext(ppNexts, pTemp), k++ )
         {
-            k = 0;
-            for ( pObj = pTable[i]; pObj; pObj = pObj->pData )
-                k++;
-            // write entries in the topological order
-            k2 = k;
-            for ( pObj = pTable[i]; pObj; pObj = pObj->pData )
-            {
-                k2--;
-                p->pMemClasses[nEntries+k2] = pObj;
-                p->pMemClasses[nEntries+k+k2] = NULL;
-            }
-            assert( k2 == 0 );
-            Vec_PtrPush( p->vClasses, p->pMemClasses + nEntries );
-            nEntries += 2*k;
+            p->pMemClasses[2*nEntries+nNodes-k] = pTemp;
+            Fra_ObjSetRepr( pTemp, pObj );
         }
-    free( pTable );
+        // add as many empty entries
+//        memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Dar_Obj_t *) * nNodes );
+        p->pMemClasses[2*nEntries + nNodes] = NULL;
+        // increment the number of entries
+        nEntries += k;
+    }
+    free( ppTable );
+    free( ppNexts );
     // now it is time to refine the classes
     Fra_RefineClasses( p );
-    // set the pointer to the manager
-    Dar_ManForEachObj( p->pManAig, pObj, i )
-        pObj->pData = p->pManAig;
 }
 
 /**Function*************************************************************
@@ -236,40 +329,42 @@ void Fra_CreateClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** pClass )
+Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass )
 {
-    Dar_Obj_t * pObj;
+    Dar_Obj_t * pObj, ** ppThis;
     int i;
-    assert( pClass[1] != NULL );
+    assert( ppClass[0] != NULL && ppClass[1] != NULL );
     // check if the class is going to be refined
-    for ( pObj = pClass[1]; pObj; pObj++ )        
-        if ( !Fra_NodeCompareSims(p, pClass[0], pObj) )
+    for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )        
+        if ( !Fra_NodeCompareSims(p, ppClass[0], pObj) )
             break;
     if ( pObj == NULL )
         return NULL;
     // split the class
     Vec_PtrClear( p->vClassOld );
     Vec_PtrClear( p->vClassNew );
-    Vec_PtrPush( p->vClassOld, pClass[0] );
-    for ( pObj = pClass[1]; pObj; pObj++ )        
-        if ( Fra_NodeCompareSims(p, pClass[0], pObj) )
+    Vec_PtrPush( p->vClassOld, ppClass[0] );
+    for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )        
+        if ( Fra_NodeCompareSims(p, ppClass[0], pObj) )
             Vec_PtrPush( p->vClassOld, pObj );
         else
             Vec_PtrPush( p->vClassNew, pObj );
     // put the nodes back into the class memory
     Vec_PtrForEachEntry( p->vClassOld, pObj, i )
     {
-        pClass[i] = pObj;
-        pClass[Vec_PtrSize(p->vClassOld)+i] = NULL;
+        ppClass[i] = pObj;
+        ppClass[Vec_PtrSize(p->vClassOld)+i] = NULL;
+        Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL );
     }
-    pClass += 2*Vec_PtrSize(p->vClassOld);
+    ppClass += 2*Vec_PtrSize(p->vClassOld);
     // put the new nodes into the class memory
     Vec_PtrForEachEntry( p->vClassNew, pObj, i )
     {
-        pClass[i] = pObj;
-        pClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
+        ppClass[i] = pObj;
+        ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
+        Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL );
     }
-    return pClass;
+    return ppClass;
 }
 
 /**Function*************************************************************
@@ -295,7 +390,10 @@ int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses )
             Vec_PtrPop( vClasses );
         // if the new class is trivial, stop
         if ( pClass2[1] == NULL )
+        {
+            nRefis++;
             break;
+        }
         // othewise, add the class and continue
         Vec_PtrPush( vClasses, pClass2 );
         pClass = pClass2;
@@ -319,7 +417,7 @@ int Fra_RefineClasses( Fra_Man_t * p )
 {
     Vec_Ptr_t * vTemp;
     Dar_Obj_t ** pClass;
-    int clk, i, nRefis = 0;
+    int clk, i, nRefis;
     // check if some outputs already became non-constant
     // this is a special case when computation can be stopped!!!
     if ( p->pPars->fProve )
@@ -328,12 +426,13 @@ int Fra_RefineClasses( Fra_Man_t * p )
         return 0;
     // refine the classes
 clk = clock();
+    nRefis = 0;
     Vec_PtrClear( p->vClassesTemp );
     Vec_PtrForEachEntry( p->vClasses, pClass, i )
     {
         // add the class to the new array
         Vec_PtrPush( p->vClassesTemp, pClass );
-        // refine the class interatively
+        // refine the class iteratively
         nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp );
     }
     // exchange the class representation
@@ -357,11 +456,17 @@ p->timeRef += clock() - clk;
 ***********************************************************************/
 int Fra_RefineClasses1( Fra_Man_t * p )
 {
-    Dar_Obj_t * pObj, ** pClass;
-    int i, k;
+    Dar_Obj_t * pObj, ** ppClass;
+    int i, k, nRefis, clk;
+    // check if there is anything to refine
+    if ( Vec_PtrSize(p->vClasses1) == 0 )
+        return 0;
+clk = clock();
+    // make sure constant 1 class contains only non-constant nodes
+    assert( Vec_PtrEntry(p->vClasses1,0) != Dar_ManConst1(p->pManAig) );
     // collect all the nodes to be refined
-    Vec_PtrClear( p->vClassNew );
     k = 0;
+    Vec_PtrClear( p->vClassNew );
     Vec_PtrForEachEntry( p->vClasses1, pObj, i )
     {
         if ( Fra_NodeHasZeroSim( p, pObj ) )
@@ -373,18 +478,24 @@ int Fra_RefineClasses1( Fra_Man_t * p )
     if ( Vec_PtrSize(p->vClassNew) == 0 )
         return 0;
     if ( Vec_PtrSize(p->vClassNew) == 1 )
+    {
+        Fra_ObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL );
         return 1;
+    }
     // create a new class composed of these nodes
-    pClass = p->pMemClassesFree;
+    ppClass = p->pMemClassesFree;
     p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew);
     Vec_PtrForEachEntry( p->vClassNew, pObj, i )
     {
-        pClass[i] = pObj;
-        pClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
+        ppClass[i] = pObj;
+        ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
+        Fra_ObjSetRepr( pObj, i? ppClass[0] : NULL );
     }
-    Vec_PtrPush( p->vClasses, pClass );
+    Vec_PtrPush( p->vClasses, ppClass );
     // iteratively refine this class
-    return 1 + Fra_RefineClassLastIter( p, p->vClasses );
+    nRefis = 1 + Fra_RefineClassLastIter( p, p->vClasses );
+p->timeRef += clock() - clk;
+    return nRefis;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraCnf.c b/src/aig/fra/fraCnf.c
index 18a5ceb6..a662ade2 100644
--- a/src/aig/fra/fraCnf.c
+++ b/src/aig/fra/fraCnf.c
@@ -209,6 +209,7 @@ Vec_Ptr_t * Fra_CollectSuper( Dar_Obj_t * pObj, int fUseMuxes )
 ***********************************************************************/
 void Fra_ObjAddToFrontier( Fra_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vFrontier )
 {
+    Fra_Man_t * pTemp = pObj->pData;
     assert( !Dar_IsComplement(pObj) );
     if ( Fra_ObjSatNum(pObj) )
         return;
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index cccd1d75..67921318 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -69,8 +69,6 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
 Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
 {
     Fra_Man_t * p;
-    Dar_Obj_t * pObj;
-    int i;
     // allocate the fraiging manager
     p = ALLOC( Fra_Man_t, 1 );
     memset( p, 0, sizeof(Fra_Man_t) );
@@ -82,13 +80,17 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
     p->nSimWords  = pPars->nSimWords;
     p->pSimWords  = ALLOC( unsigned, (Dar_ManObjIdMax(pManAig) + 1) * p->nSimWords );
     // clean simulation info of the constant node
-    memset( p->pSimWords, 0, p->nSimWords * sizeof(unsigned) );
+    memset( p->pSimWords, 0, sizeof(unsigned) * ((Dar_ManPiNum(pManAig) + 1) * p->nSimWords) );
     // allocate storage for sim pattern
     p->nPatWords  = Dar_BitWordNum( Dar_ManPiNum(pManAig) );
     p->pPatWords  = ALLOC( unsigned, p->nPatWords ); 
     p->pPatScores = ALLOC( int, 32 * p->nSimWords ); 
     p->vPiVars    = Vec_PtrAlloc( 100 );
     p->vClasses   = Vec_PtrAlloc( 100 );
+    p->vClasses1  = Vec_PtrAlloc( 100 );
+    p->vClassOld  = Vec_PtrAlloc( 100 );
+    p->vClassNew  = Vec_PtrAlloc( 100 );
+    p->vClassesTemp = Vec_PtrAlloc( 100 );
     // allocate other members
     p->nSizeAlloc = Dar_ManObjIdMax(pManAig) + 1;
     p->pMemFraig  = ALLOC( Dar_Obj_t *, p->nSizeAlloc );
@@ -98,17 +100,41 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
     p->pMemFanins  = ALLOC( Vec_Ptr_t *, p->nSizeAlloc );
     memset( p->pMemFanins, 0, p->nSizeAlloc * sizeof(Vec_Ptr_t *) );
     p->pMemSatNums  = ALLOC( int, p->nSizeAlloc );
-    memset( p->pMemSatNums, 0xff, p->nSizeAlloc * sizeof(int) );
+    memset( p->pMemSatNums, 0, p->nSizeAlloc * sizeof(int) );
+    // set random number generator
+    srand( 0xABCABC );
+    // make sure the satisfying assignment is node assigned
+    assert( p->pManFraig->pData == NULL );
+    // connect AIG managers to the FRAIG manager
+    Fra_ManPrepare( p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares managers by transfering pointers to the objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ManPrepare( Fra_Man_t * p )
+{
+    Dar_Obj_t * pObj;
+    int i;
+    // set the pointers to the manager
+    Dar_ManForEachObj( p->pManFraig, pObj, i )
+        pObj->pData = p;
+    // set the pointer to the manager
+    Dar_ManForEachObj( p->pManAig, pObj, i )
+        pObj->pData = p;
     // set the pointers to the available fraig nodes
     Fra_ObjSetFraig( Dar_ManConst1(p->pManAig), Dar_ManConst1(p->pManFraig) );
     Dar_ManForEachPi( p->pManAig, pObj, i )
         Fra_ObjSetFraig( pObj, Dar_ManPi(p->pManFraig, i) );
-    // set the pointers to the manager
-    Dar_ManForEachObj( p->pManFraig, pObj, i )
-        pObj->pData = p->pManFraig;
-    // set random number generator
-    srand( 0xABCABC );
-    return p;
 }
 
 /**Function*************************************************************
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index e8b88159..7207cfa2 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -105,7 +105,11 @@ void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
     Dar_Obj_t * pObj;
     int i, Limit;
     Dar_ManForEachPi( p->pManAig, pObj, i )
+    {
         Fra_NodeAssignConst( p, pObj, Dar_InfoHasBit(pPat, i) );
+//        printf( "%d", Dar_InfoHasBit(pPat, i) );
+    }
+//    printf( "\n" );
     Limit = DAR_MIN( Dar_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
     for ( i = 0; i < Limit; i++ )
         Dar_InfoXorBit( Fra_ObjSim( Dar_ManPi(p->pManAig,i) ), i+1 );
@@ -441,7 +445,7 @@ void Fra_Resimulate( Fra_Man_t * p )
     if ( nChanges < 1 )
         printf( "Error: A counter-example did not refine classes!\n" );
     assert( nChanges >= 1 );
-//printf( "Refined classes! = %5d.   Changes = %4d.\n", p->lClasses.nItems, nChanges );
+//printf( "Refined classes = %5d.   Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );
 
     if ( !p->pPars->fPatScores )
         return;
@@ -487,7 +491,7 @@ void Fra_Simulate( Fra_Man_t * p )
     Fra_SimulateOne( p );
     nChanges = Fra_RefineClasses( p );
     nChanges += Fra_RefineClasses1( p );
-    if ( p->pManFraig )
+    if ( p->pManFraig->pData )
         return;
 //printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
     Fra_SavePattern1( p );
@@ -495,7 +499,7 @@ void Fra_Simulate( Fra_Man_t * p )
     Fra_SimulateOne( p );
     nChanges = Fra_RefineClasses( p );
     nChanges += Fra_RefineClasses1( p );
-    if ( p->pManFraig )
+    if ( p->pManFraig->pData )
         return;
 //printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
     // refine classes by random simulation
@@ -505,11 +509,11 @@ void Fra_Simulate( Fra_Man_t * p )
         nClasses = Vec_PtrSize(p->vClasses);
         nChanges = Fra_RefineClasses( p );
         nChanges += Fra_RefineClasses1( p );
-        if ( p->pManFraig )
+        if ( p->pManFraig->pData )
             return;
 //printf( "Refined classes  = %5d.   Changes = %4d.   Pairs = %6d.\n", p->lClasses.nItems, nChanges, Fra_CountPairsClasses(p) );
     } while ( (double)nChanges / nClasses > p->pPars->dSimSatur );
-//    Fra_PrintSimClasses( p );
+//    Fra_PrintClasses( p );
 }
  
 /**Function*************************************************************
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index e9a65881..a922674d 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -733,7 +733,12 @@ void Ivy_FraigAssignDist1( Ivy_FraigMan_t * p, unsigned * pPat )
     Ivy_Obj_t * pObj;
     int i, Limit;
     Ivy_ManForEachPi( p->pManAig, pObj, i )
+    {
         Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) );
+//        printf( "%d", Ivy_InfoHasBit(pPat, i) );
+    }
+//    printf( "\n" );
+
     Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
     for ( i = 0; i < Limit; i++ )
         Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) )->pData, i+1 );
@@ -1742,7 +1747,6 @@ void Ivy_FraigResimulate( Ivy_FraigMan_t * p )
         printf( "Error: A counter-example did not refine classes!\n" );
     assert( nChanges >= 1 );
 //printf( "Refined classes! = %5d.   Changes = %4d.\n", p->lClasses.nItems, nChanges );
-
     if ( !p->pParams->fPatScores )
         return;
 
@@ -2018,6 +2022,8 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
     if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) )
         return pObjNew;
     assert( Ivy_Regular(pObjNew) != Ivy_ManConst1(p->pManFraig) );
+//    printf( "Node = %d. Repr = %d.\n", pObjOld->Id, Ivy_ObjClassNodeRepr(pObjOld)->Id );
+
     // they are different (the counter-example is in p->pPatWords)
     RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew) );
     if ( RetValue == 1 )  // proved equivalent
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 3de48f00..bb1ae2ed 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -1490,7 +1490,8 @@ void Abc_NtkTransferCopy( Abc_Ntk_t * pNtk )
 static inline int Abc_ObjCrossCutInc( Abc_Obj_t * pObj )
 {
 //    pObj->pCopy = (void *)(((int)pObj->pCopy)++);
-    ((char*)pObj->pCopy)++;
+    int Value = (int)pObj->pCopy;
+    pObj->pCopy = (void *)(Value + 1);
     return (int)pObj->pCopy == Abc_ObjFanoutNum(pObj);
 }
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index cd67205c..06f4299d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -112,6 +112,7 @@ static int Abc_CommandIRewriteSeq    ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandIResyn         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandISat           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIFraig         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDFraig         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandHaig           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMini           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -267,6 +268,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "iresyn",        Abc_CommandIResyn,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "isat",          Abc_CommandISat,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "ifraig",        Abc_CommandIFraig,           1 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "dfraig",        Abc_CommandDFraig,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "iprove",        Abc_CommandIProve,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "haig",          Abc_CommandHaig,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "mini",          Abc_CommandMini,             1 );
@@ -333,7 +335,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
     {
         extern void Dar_LibStart();
-        Dar_LibStart();
+//        Dar_LibStart();
     }
 } 
 
@@ -352,7 +354,7 @@ void Abc_End()
 {
     {
         extern void Dar_LibStop();
-        Dar_LibStop();
+//        Dar_LibStop();
     }
 
     Abc_NtkFraigStoreClean();
@@ -6077,14 +6079,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Abc_Ntk4VarTable( pNtk );
 //    Dar_NtkGenerateArrays( pNtk );
 //    Dar_ManDeriveCnfTest2();
-
+/*
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Network should be strashed. Command has failed.\n" );
         return 1;
     }
+*/
 //    pNtkRes = Abc_NtkDar( pNtk );
-    pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" );
+//    pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" );
+    pNtkRes = NULL;
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -6911,6 +6915,93 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c, fProve, fVerbose, fDoSparse;
+    int nConfLimit;
+
+    extern Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nConfLimit   = 100;   
+    fDoSparse    = 0;
+    fProve       = 0;
+    fVerbose     = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Cspvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfLimit < 0 ) 
+                goto usage;
+            break;
+        case 's':
+            fDoSparse ^= 1;
+            break;
+        case 'p':
+            fProve ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: dfraig [-C num] [-spvh]\n" );
+    fprintf( pErr, "\t         performs fraiging using a new method\n" );
+    fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
+    fprintf( pErr, "\t-s     : toggle considering sparse functions [default = %s]\n", fDoSparse? "yes": "no" );
+    fprintf( pErr, "\t-p     : toggle proving the miter outputs [default = %s]\n", fProve? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Prove_Params_t Params, * pParams = &Params;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index c2988cbb..ba3ac89d 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -21,6 +21,7 @@
 #include "abc.h"
 #include "dar.h"
 #include "cnf.h"
+#include "fra.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -443,6 +444,37 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose )
+{
+    Fra_Par_t Params, * pParams = &Params; 
+    Abc_Ntk_t * pNtkAig;
+    Dar_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk );
+    if ( pMan == NULL )
+        return NULL;
+    Fra_ParamsDefault( pParams );
+    pParams->nBTLimitNode = nConfLimit;
+    pParams->fVerbose     = fVerbose;
+    pParams->fProve       = fProve;
+    pParams->fDoSparse    = fDoSparse;
+    pMan = Fra_Perform( pTemp = pMan, pParams );
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Dar_ManStop( pTemp );
+    Dar_ManStop( pMan );
+    return pNtkAig;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/kit/kitGraph.c b/src/opt/kit/kitGraph.c
index e2deb4ef..8bc7ca91 100644
--- a/src/opt/kit/kitGraph.c
+++ b/src/opt/kit/kitGraph.c
@@ -357,6 +357,8 @@ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemor
     RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 1 ); // tried 1 and found not useful in "renode"
     if ( RetValue == -1 )
         return NULL;
+    if ( Vec_IntSize(vMemory) > 128 )
+        return NULL;
 //    printf( "Isop size = %d.\n", Vec_IntSize(vMemory) );
     assert( RetValue == 0 || RetValue == 1 );
     // derive factored form
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index aa0368a9..a1da45b5 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -229,7 +229,6 @@ p->timeMap += clock() - clk;
 int Lpk_ResynthesizeNode( Lpk_Man_t * p )
 {
     static int Count = 0;
-    char * pFileName;
     Kit_DsdNtk_t * pDsdNtk;
     Lpk_Cut_t * pCut;
     unsigned * pTruth;
@@ -245,6 +244,8 @@ p->timeCuts += clock() - clk;
     }
 p->timeCuts += clock() - clk;
 
+//return 0;
+
     if ( p->pPars->fVeryVerbose )
     printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
     // try the good cuts
@@ -289,12 +290,13 @@ p->timeTruth += clock() - clk;
 
         if ( p->pPars->fVeryVerbose )
         {
+//            char * pFileName;
             printf( "  C%02d: L= %2d/%2d  V= %2d/%d  N= %d  W= %4.2f  ", 
                 i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
             Kit_DsdPrint( stdout, pDsdNtk );
 //            Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
-            pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
-            printf( "Saved truth table in file \"%s\".\n", pFileName );
+//            pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
+//            printf( "Saved truth table in file \"%s\".\n", pFileName );
         }
 
         // update the network
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
index 12dae15b..27a0317c 100644
--- a/src/opt/lpk/lpkCut.c
+++ b/src/opt/lpk/lpkCut.c
@@ -474,12 +474,16 @@ if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 )
     assert( p->nCuts < LPK_CUTS_MAX );
     p->nCuts++;
 
-    assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup );
+//    assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup );
+
 /*
     printf( "      Creating cut: " );
     Lpk_NodePrintCut( p, pCutNew, 1 );
     printf( "\n" );
 */
+
+//    if ( !(pCut->nNodes <= p->nMffc + pCutNew->nNodesDup) )
+//        printf( "Assertion in line 477 failed.\n" );
 }
 
 /**Function*************************************************************
@@ -519,9 +523,17 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
         pCut = p->pCuts + i;
         if ( pCut->nLeaves == 0 )
             continue;
+
         // try to expand the fanins of this cut
         for ( k = 0; k < (int)pCut->nLeaves; k++ )
         {
+
+            if ( p->pObj->Id == 28 && i == 273 && k == 13 )
+            {
+                Abc_Obj_t * pFanin = Abc_NtkObj(p->pNtk, pCut->pLeaves[k]);
+                int s = 0;
+            }
+
             // create a new cut
             Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] );
             // quit if the number of cuts has exceeded the limit
diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c
index 5dd54450..c11a0a33 100644
--- a/src/opt/lpk/lpkMan.c
+++ b/src/opt/lpk/lpkMan.c
@@ -50,7 +50,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
     p->pPars = pPars;
     p->nCutsMax = LPK_CUTS_MAX;
     p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax );
-    p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nVarsMax) );
+    p->vTtNodes = Vec_PtrAllocSimInfo( 1024, Abc_TruthWordNum(pPars->nVarsMax) );
     p->vCover = Vec_IntAlloc( 1 << 12 );
     for ( i = 0; i < 8; i++ )
         p->vSets[i] = Vec_IntAlloc(100);
diff --git a/src/opt/lpk/module.make b/src/opt/lpk/module.make
index 9e7bbc7c..9a46e0ce 100644
--- a/src/opt/lpk/module.make
+++ b/src/opt/lpk/module.make
@@ -1,7 +1,7 @@
-SRC +=    src/aig/lpk/lpkCore.c \
-    src/aig/lpk/lpkCut.c \
-    src/aig/lpk/lpkMan.c \
-    src/aig/lpk/lpkMap.c \
-    src/aig/lpk/lpkMulti.c \
-    src/aig/lpk/lpkMux.c \
-    src/aig/lpk/lpkSets.c 
+SRC +=    src/opt/lpk/lpkCore.c \
+    src/opt/lpk/lpkCut.c \
+    src/opt/lpk/lpkMan.c \
+    src/opt/lpk/lpkMap.c \
+    src/opt/lpk/lpkMulti.c \
+    src/opt/lpk/lpkMux.c \
+    src/opt/lpk/lpkSets.c