Version abc70710

6 files changed, 249 insertions, 101 deletions

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*************************************************************