Version abc80130_2

1 files changed, 330 insertions, 116 deletions

diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index a11e6eef..be8a25f1 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -26,16 +26,19 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
-static Abc_Ntk_t *   Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
-static Abc_Obj_t *   Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig );
-
-static int           Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk );
-static void          Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-static Abc_Obj_t *   Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
+extern Abc_Ntk_t *    Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
+static Abc_Ntk_t *    Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
+static Abc_Obj_t *    Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig );
+static void           Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs );
+extern Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc );
+static void           Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
+
+static int            Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk );
+static void           Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+static Abc_Obj_t *    Abc_NodeFraigTrust( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode );
  
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -49,19 +52,30 @@ static Abc_Obj_t *   Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
+Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc )
 {
     Fraig_Params_t * pPars = pParams;
     Abc_Ntk_t * pNtkNew;
-    Fraig_Man_t * pMan;
+    Fraig_Man_t * pMan; 
+    // check if EXDC is present
+    if ( fExdc && pNtk->pExdc == NULL )
+        fExdc = 0, printf( "Warning: Networks has no EXDC.\n" );
     // perform fraiging
-    pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes ); 
+    pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes, fExdc ); 
+    // add algebraic choices
+//    if ( pPars->fChoicing )
+//        Fraig_ManAddChoices( pMan, 0, 6 );
     // prove the miter if asked to
     if ( pPars->fTryProve )
         Fraig_ManProveMiter( pMan );
     // reconstruct FRAIG in the new network
-    pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
+    if ( fExdc ) 
+        pNtkNew = Abc_NtkFromFraig2( pMan, pNtk );
+    else
+        pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
     Fraig_ManFree( pMan );
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
@@ -83,13 +97,13 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
   SeeAlso     []
 
 ***********************************************************************/
-Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes )
+void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc )
 {
+    int fInternal = ((Fraig_Params_t *)pParams)->fInternal;
     Fraig_Man_t * pMan;
     ProgressBar * pProgress;
-    Fraig_Node_t * pNodeFraig;
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pNode, * pConst1, * pReset;
+    Abc_Obj_t * pNode;
     int i;
 
     assert( Abc_NtkIsStrash(pNtk) );
@@ -97,36 +111,35 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
     // create the FRAIG manager
     pMan = Fraig_ManCreate( pParams );
 
-    // create PIs and remember them in the old nodes
+    // map the constant node
     Abc_NtkCleanCopy( pNtk );
+    Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
+    // create PIs and remember them in the old nodes
     Abc_NtkForEachCi( pNtk, pNode, i )
         pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
-    pConst1 = Abc_AigConst1( pNtk->pManFunc );
-    pReset  = Abc_AigReset( pNtk->pManFunc );
-
+ 
     // perform strashing
     vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
-    if ( !pParams->fInternal )
+    if ( !fInternal )
         pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
-        if ( !pParams->fInternal )
-            Extra_ProgressBarUpdate( pProgress, i, NULL );
-        if ( pNode == pConst1 )
-            pNodeFraig = Fraig_ManReadConst1(pMan);
-        else if ( pNode == pReset )
+        if ( Abc_ObjFaninNum(pNode) == 0 )
             continue;
-        else
-            pNodeFraig = Fraig_NodeAnd( pMan, 
+        if ( !fInternal )
+            Extra_ProgressBarUpdate( pProgress, i, NULL );
+        pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
                 Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
                 Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
-        assert( pNode->pCopy == NULL );
-        pNode->pCopy = (Abc_Obj_t *)pNodeFraig;
     }
-    if ( !pParams->fInternal )
+    if ( !fInternal )
         Extra_ProgressBarStop( pProgress );
     Vec_PtrFree( vNodes );
 
+    // use EXDC to change the mapping of nodes into FRAIG nodes
+    if ( fExdc )
+        Abc_NtkFraigRemapUsingExdc( pMan, pNtk );
+
     // set the primary outputs
     Abc_NtkForEachCo( pNtk, pNode, i )
         Fraig_ManSetPo( pMan, (Fraig_Node_t *)Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
@@ -135,7 +148,123 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
 
 /**Function*************************************************************
 
-  Synopsis    [Transforms FRAIG into what looks like a strashed network.]
+  Synopsis    [Derives EXDC node for the given network.]
+
+  Description [Assumes that EXDCs of all POs are the same.
+  Returns the EXDC of the first PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc )
+{
+    Abc_Ntk_t * pNtkStrash;
+    Abc_Obj_t * pObj;
+    Fraig_Node_t * gResult;
+    char ** ppNames;
+    int i, k;
+    // strash the EXDC network
+    pNtkStrash = Abc_NtkStrash( pNtkExdc, 0, 0, 0 );
+    Abc_NtkCleanCopy( pNtkStrash );
+    Abc_AigConst1(pNtkStrash)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
+    // set the mapping of the PI nodes
+    ppNames = Abc_NtkCollectCioNames( pNtkMain, 0 );
+    Abc_NtkForEachCi( pNtkStrash, pObj, i )
+    {
+        for ( k = 0; k < Abc_NtkCiNum(pNtkMain); k++ )
+            if ( strcmp( Abc_ObjName(pObj), ppNames[k] ) == 0 )
+            {
+                pObj->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, k);
+                break;
+            }
+        assert( pObj->pCopy != NULL );
+    }
+    free( ppNames );
+    // build FRAIG for each node
+    Abc_AigForEachAnd( pNtkStrash, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
+                Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ),
+                Fraig_NotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) ) );
+    // get the EXDC to be returned
+    pObj = Abc_NtkPo( pNtkStrash, 0 );
+    gResult = Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+    Abc_NtkDelete( pNtkStrash );
+    return gResult;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Changes mapping of the old nodes into FRAIG nodes using EXDC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    Fraig_Node_t * gNodeNew, * gNodeExdc;
+    stmm_table * tTable;
+    stmm_generator * gen;
+    Abc_Obj_t * pNode, * pNodeBest;
+    Abc_Obj_t * pClass, ** ppSlot;
+    Vec_Ptr_t * vNexts;
+    int i;
+
+    // get the global don't-cares
+    assert( pNtk->pExdc );
+    gNodeExdc = Abc_NtkToFraigExdc( pMan, pNtk, pNtk->pExdc );
+
+    // save the next pointers
+    vNexts = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Vec_PtrWriteEntry( vNexts, pNode->Id, pNode->pNext );
+
+    // find the classes of AIG nodes which have FRAIG nodes assigned
+    Abc_NtkCleanNext( pNtk );
+    tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->pCopy )
+        {
+            gNodeNew = Fraig_NodeAnd( pMan, (Fraig_Node_t *)pNode->pCopy, Fraig_Not(gNodeExdc) );
+            if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(gNodeNew), (char ***)&ppSlot ) )
+                *ppSlot = NULL;
+            pNode->pNext = *ppSlot;
+            *ppSlot = pNode;
+        }
+
+    // for reach non-trival class, find the node with minimum level, and replace other nodes by it
+    Abc_AigSetNodePhases( pNtk );
+    stmm_foreach_item( tTable, gen, (char **)&gNodeNew, (char **)&pClass )
+    {
+        if ( pClass->pNext == NULL )
+            continue;
+        // find the node with minimum level
+        pNodeBest = pClass;
+        for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext )
+            if ( pNodeBest->Level > pNode->Level )
+                 pNodeBest = pNode;
+        // remap the class nodes
+        for ( pNode = pClass; pNode; pNode = pNode->pNext )
+            pNode->pCopy = Abc_ObjNotCond( pNodeBest->pCopy, pNode->fPhase ^ pNodeBest->fPhase );
+    }
+    stmm_free_table( tTable );
+
+    // restore the next pointers
+    Abc_NtkCleanNext( pNtk );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        pNode->pNext = Vec_PtrEntry( vNexts, pNode->Id );
+    Vec_PtrFree( vNexts );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms FRAIG into strashed network with choices.]
 
   Description []
                
@@ -146,26 +275,27 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
 {
-//    ProgressBar * pProgress;
+    ProgressBar * pProgress;
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode, * pNodeNew;
     int i;
     // create the new network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
     // make the mapper point to the new network
     Abc_NtkForEachCi( pNtk, pNode, i )
         Fraig_NodeSetData1( Fraig_ManReadIthVar(pMan, i), (Fraig_Node_t *)pNode->pCopy );
     // set the constant node
-    Fraig_NodeSetData1( Fraig_ManReadConst1(pMan), (Fraig_Node_t *)Abc_AigConst1(pNtkNew->pManFunc) );
+    Fraig_NodeSetData1( Fraig_ManReadConst1(pMan), (Fraig_Node_t *)Abc_AigConst1(pNtkNew) );
     // process the nodes in topological order
-//    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
-//        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
         pNodeNew = Abc_NodeFromFraig_rec( pNtkNew, Fraig_ManReadOutputs(pMan)[i] );
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     }
-//    Extra_ProgressBarStop( pProgress );
+    Extra_ProgressBarStop( pProgress );
+    Abc_NtkReassignIds( pNtkNew );
     return pNtkNew;
 }
 
@@ -232,6 +362,109 @@ Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFrai
     return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Transforms FRAIG into strashed network without choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    stmm_table * tTable;
+    Vec_Ptr_t * vNodeReprs;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode, * pRepr, ** ppSlot;
+    int i;
+
+    // map the nodes into their lowest level representives
+    tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
+    pNode = Abc_AigConst1(pNtk);
+    if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
+        *ppSlot = pNode;
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
+            *ppSlot = pNode;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->pCopy )
+        {
+            if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
+                *ppSlot = pNode;
+            else if ( (*ppSlot)->Level > pNode->Level )
+                *ppSlot = pNode;
+        }
+    // save representatives for each node
+    vNodeReprs = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->pCopy )
+        {           
+            if ( !stmm_lookup( tTable, (char *)Fraig_Regular(pNode->pCopy), (char **)&pRepr ) )
+                assert( 0 );
+            if ( pNode != pRepr )
+                Vec_PtrWriteEntry( vNodeReprs, pNode->Id, pRepr );
+        }
+    stmm_free_table( tTable );
+
+    // create the new network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+
+    // perform strashing
+    Abc_AigSetNodePhases( pNtk );
+    Abc_NtkIncrementTravId( pNtk );
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin0(pNode), vNodeReprs );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vNodeReprs );
+
+    // finalize the network
+    Abc_NtkFinalize( pNtk, pNtkNew );
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms into AIG one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs )
+{
+    Abc_Obj_t * pRepr;
+    // skip the PIs and constants
+    if ( Abc_ObjFaninNum(pNode) < 2 )
+        return;
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    assert( Abc_ObjIsNode( pNode ) );
+    // get the node's representative
+    if ( pRepr = Vec_PtrEntry(vNodeReprs, pNode->Id) )
+    {
+        Abc_NtkFromFraig2_rec( pNtkNew, pRepr, vNodeReprs );
+        pNode->pCopy = Abc_ObjNotCond( pRepr->pCopy, pRepr->fPhase ^ pNode->fPhase );
+        return;
+    }
+    Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin0(pNode), vNodeReprs );
+    Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin1(pNode), vNodeReprs );
+    pNode->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
+}
 
 
 
@@ -263,9 +496,10 @@ Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk )
     }
     
     // perform strashing
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_STRASH, ABC_FUNC_AIG );
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
     Abc_NtkFraigTrustOne( pNtk, pNtkNew );
     Abc_NtkFinalize( pNtk, pNtkNew );
+    Abc_NtkReassignIds( pNtkNew );
 
     // print a warning about choice nodes
     printf( "Warning: The resulting AIG contains %d choice nodes.\n", Abc_NtkGetChoiceNum( pNtkNew ) );
@@ -322,7 +556,6 @@ int Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk )
 void Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
 {
     ProgressBar * pProgress;
-    Abc_Aig_t * pMan = pNtkNew->pManFunc;
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode, * pNodeNew, * pObj;
     int i;
@@ -336,7 +569,7 @@ void Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
         // get the node
         assert( Abc_ObjIsNode(pNode) );
          // strash the node
-        pNodeNew = Abc_NodeFraigTrust( pMan, pNode );
+        pNodeNew = Abc_NodeFraigTrust( pNtkNew, pNode );
         // get the old object
         if ( Abc_NtkIsNetlist(pNtk) )
             pObj = Abc_ObjFanout0( pNode ); // the fanout net 
@@ -362,10 +595,9 @@ void Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
+Abc_Obj_t * Abc_NodeFraigTrust( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
 {
     Abc_Obj_t * pSum, * pFanin;
-    Abc_Obj_t * pConst1 = Abc_AigConst1(pMan);
     void ** ppTail;
     int i, nFanins, fCompl;
 
@@ -375,11 +607,11 @@ Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
     assert( nFanins == Abc_SopGetVarNum(pNode->pData) );
     // check if it is a constant
     if ( nFanins == 0 )
-        return Abc_ObjNotCond( pConst1, Abc_SopIsConst0(pNode->pData) );
+        return Abc_ObjNotCond( Abc_AigConst1(pNtkNew), Abc_SopIsConst0(pNode->pData) );
     if ( nFanins == 1 )
         return Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_SopIsInv(pNode->pData) );
     if ( nFanins == 2 && Abc_SopIsAndType(pNode->pData) )
-        return Abc_AigAnd( pMan, 
+        return Abc_AigAnd( pNtkNew->pManFunc, 
             Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, !Abc_SopGetIthCareLit(pNode->pData,0) ),
             Abc_ObjNotCond( Abc_ObjFanin1(pNode)->pCopy, !Abc_SopGetIthCareLit(pNode->pData,1) )  );
     assert( Abc_SopIsOrType(pNode->pData) );
@@ -416,49 +648,32 @@ Abc_Obj_t * Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
+int Abc_NtkFraigStore( Abc_Ntk_t * pNtkAdd )
 {
-    extern int Abc_NtkAppendNew( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
-
-    Abc_Ntk_t * pStore;
-    int nAndsOld;
-
-    if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
+    Vec_Ptr_t * vStore;
+    Abc_Ntk_t * pNtk;
+    // create the network to be stored
+    pNtk = Abc_NtkStrash( pNtkAdd, 0, 0, 0 );
+    if ( pNtk == NULL )
     {
-        printf( "The netlist need to be converted into a logic network before adding it to storage.\n" );
+        printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );
         return 0;
     }
-
     // get the network currently stored
-    pStore = Abc_FrameReadNtkStore();
-    if ( pStore == NULL )
+    vStore = Abc_FrameReadStore();
+    if ( Vec_PtrSize(vStore) > 0 )
     {
-        // start the stored network
-        pStore = Abc_NtkStrash( pNtk, 0, 0 );
-        if ( pStore == NULL )
+        // check that the networks have the same PIs
+        // reorder PIs of pNtk2 according to pNtk1
+        if ( !Abc_NtkCompareSignals( pNtk, Vec_PtrEntry(vStore, 0), 1, 1 ) )
         {
-            printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );
-            return 0;
+            printf( "Trying to store the network with different primary inputs.\n" );
+            printf( "The previously stored networks are deleted and this one is added.\n" );
+            Abc_NtkFraigStoreClean();
         }
-        // save the parameters
-        Abc_FrameSetNtkStore( pStore );
-        Abc_FrameSetNtkStoreSize( 1 );
-        nAndsOld = 0;
     }
-    else
-    {
-        // add the new network to storage
-        nAndsOld = Abc_NtkNodeNum( pStore );
-//        if ( !Abc_NtkAppend( pStore, pNtk ) )
-        if ( !Abc_NtkAppendNew( pStore, pNtk ) )
-        {
-            printf( "The current network cannot be appended to the stored network.\n" );
-            return 0;
-        }
-        // set the number of networks stored
-        Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 );
-    }
-    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld );
+    Vec_PtrPush( vStore, pNtk );
+//    printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pNtk) );
     return 1;
 }
 
@@ -475,56 +690,54 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFraigRestore()
 {
-    extern Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams );
-
+    extern Abc_Ntk_t * Abc_NtkFraigPartitioned( Vec_Ptr_t * vStore, void * pParams );
     Fraig_Params_t Params;
-    Abc_Ntk_t * pStore, * pFraig;
+    Vec_Ptr_t * vStore;
+    Abc_Ntk_t * pNtk, * pFraig;
     int nWords1, nWords2, nWordsMin;
     int clk = clock();
 
     // get the stored network
-    pStore = Abc_FrameReadNtkStore();
-    Abc_FrameSetNtkStore( NULL );
-    if ( pStore == NULL )
+    vStore = Abc_FrameReadStore();
+    if ( Vec_PtrSize(vStore) == 0 )
     {
         printf( "There are no network currently in storage.\n" );
         return NULL;
     }
-    printf( "Currently stored %d networks with %d nodes will be fraiged.\n", 
-        Abc_FrameReadNtkStoreSize(), Abc_NtkNodeNum(pStore) );
+//    printf( "Currently stored %d networks will be fraiged.\n", Vec_PtrSize(vStore) );
+    pNtk = Vec_PtrEntry( vStore, 0 );
+
+    // swap the first and last network
+    // this should lead to the primary choice being "better" because of synthesis
+    pNtk = Vec_PtrPop( vStore );
+    Vec_PtrPush( vStore, Vec_PtrEntry(vStore,0) );
+    Vec_PtrWriteEntry( vStore, 0, pNtk );
 
     // to determine the number of simulation patterns
     // use the following strategy
     // at least 64 words (32 words random and 32 words dynamic)
     // no more than 256M for one circuit (128M + 128M)
     nWords1 = 32;
-    nWords2 = (1<<27) / (Abc_NtkNodeNum(pStore) + Abc_NtkCiNum(pStore));
+    nWords2 = (1<<27) / (Abc_NtkNodeNum(pNtk) + Abc_NtkCiNum(pNtk));
     nWordsMin = ABC_MIN( nWords1, nWords2 );
 
     // set parameters for fraiging
     Fraig_ParamsSetDefault( &Params );
-    Params.nPatsRand  = nWordsMin * 32; // the number of words of random simulation info
-    Params.nPatsDyna  = nWordsMin * 32; // the number of words of dynamic simulation info
-//    Params.nBTLimit   = 99;             // the max number of backtracks to perform
-    Params.nBTLimit   = 1000000;             // the max number of backtracks to perform
-    Params.fFuncRed   =  1;             // performs only one level hashing
-    Params.fFeedBack  =  1;             // enables solver feedback
-    Params.fDist1Pats =  1;             // enables distance-1 patterns
-    Params.fDoSparse  =  1;             // performs equiv tests for sparse functions 
-    Params.fChoicing  =  1;             // enables recording structural choices
-    Params.fTryProve  =  0;             // tries to solve the final miter
-    Params.fVerbose   =  0;             // the verbosiness flag
-    Params.fInternal  =  1;             // the flag indicates the internal run 
-
-//    Fraig_ManReportChoices( p );
-    // transform it into FRAIG
-//    pFraig = Abc_NtkFraig( pStore, &Params, 1 );
-    pFraig = Abc_NtkFraigPartitioned( pStore, &Params );
-
-PRT( "Total fraiging time", clock() - clk );
-    if ( pFraig == NULL )
-        return NULL;
-    Abc_NtkDelete( pStore );
+    Params.nPatsRand  = nWordsMin * 32;    // the number of words of random simulation info
+    Params.nPatsDyna  = nWordsMin * 32;    // the number of words of dynamic simulation info
+    Params.nBTLimit   = 1000;              // the max number of backtracks to perform
+    Params.fFuncRed   =    1;              // performs only one level hashing
+    Params.fFeedBack  =    1;              // enables solver feedback
+    Params.fDist1Pats =    1;              // enables distance-1 patterns
+    Params.fDoSparse  =    1;              // performs equiv tests for sparse functions 
+    Params.fChoicing  =    1;              // enables recording structural choices
+    Params.fTryProve  =    0;              // tries to solve the final miter
+    Params.fVerbose   =    0;              // the verbosiness flag
+
+    // perform partitioned computation of structural choices
+    pFraig = Abc_NtkFraigPartitioned( vStore, &Params );
+    Abc_NtkFraigStoreClean();
+//PRT( "Total choicing time", clock() - clk );
     return pFraig;
 }
 
@@ -541,12 +754,13 @@ PRT( "Total fraiging time", clock() - clk );
 ***********************************************************************/
 void Abc_NtkFraigStoreClean()
 {
-    Abc_Ntk_t * pStore;
-    // get the stored network
-    pStore = Abc_FrameReadNtkStore();
-    if ( pStore )
-        Abc_NtkDelete( pStore );
-    Abc_FrameSetNtkStore( NULL );
+    Vec_Ptr_t * vStore;
+    Abc_Ntk_t * pNtk;
+    int i;
+    vStore = Abc_FrameReadStore();
+    Vec_PtrForEachEntry( vStore, pNtk, i )
+        Abc_NtkDelete( pNtk );
+    Vec_PtrClear( vStore );
 }
 
 /**Function*************************************************************
@@ -567,7 +781,7 @@ void Abc_NtkFraigStoreCheck( Abc_Ntk_t * pFraig )
     int i, k;
     // check that the PO functions are correct
     nPoFinal = Abc_NtkPoNum(pFraig);
-    nStored  = Abc_FrameReadNtkStoreSize(Abc_FrameGetGlobalFrame());
+    nStored  = Abc_FrameReadStoreSize();
     assert( nPoFinal % nStored == 0 );
     nPoOrig  = nPoFinal / nStored;
     for ( i = 0; i < nPoOrig; i++ )