Version abc70407

3 files changed, 54 insertions, 6 deletions

diff --git a/src/map/if/if.h b/src/map/if/if.h
index a440d7ea..cdf9e1c7 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -331,17 +331,19 @@ extern void            If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t *
 extern void            If_ManSortCuts( If_Man_t * p, int Mode );
 /*=== ifMan.c =============================================================*/
 extern If_Man_t *      If_ManStart( If_Par_t * pPars );
+extern void            If_ManRestart( If_Man_t * p );
 extern void            If_ManStop( If_Man_t * p );
 extern If_Obj_t *      If_ManCreateCi( If_Man_t * p );
 extern If_Obj_t *      If_ManCreateCo( If_Man_t * p, If_Obj_t * pDriver, int fCompl0 );
 extern If_Obj_t *      If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_t * pFan1, int fCompl1 );
+extern If_Obj_t *      If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 );
 extern void            If_ManCreateChoice( If_Man_t * p, If_Obj_t * pRepr );
 extern void            If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId );
 extern void            If_ManSetupCiCutSets( If_Man_t * p );
 extern If_Set_t *      If_ManSetupNodeCutSet( If_Man_t * p, If_Obj_t * pObj );
 extern void            If_ManDerefNodeCutSet( If_Man_t * p, If_Obj_t * pObj );
 extern void            If_ManDerefChoiceCutSet( If_Man_t * p, If_Obj_t * pObj );
-extern void            If_ManSetupSetAll( If_Man_t * p );
+extern void            If_ManSetupSetAll( If_Man_t * p, int nCrossCut );
 /*=== ifMap.c =============================================================*/
 extern void            If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess );
 extern void            If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess );
diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c
index c36642bc..59ad5a1c 100644
--- a/src/map/if/ifCore.c
+++ b/src/map/if/ifCore.c
@@ -48,7 +48,7 @@ int If_ManPerformMapping( If_Man_t * p )
     // create the CI cutsets
     If_ManSetupCiCutSets( p );
     // allocate memory for other cutsets
-    If_ManSetupSetAll( p );
+    If_ManSetupSetAll( p, If_ManCrossCut(p) );
 
     // try sequential mapping
     if ( p->pPars->fSeqMap )
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 77f4930a..00a5b228 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -79,6 +79,7 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     p->pConst1 = If_ManSetupObj( p );
     p->pConst1->Type = IF_CONST1;
     p->pConst1->fPhase = 1;
+    p->nObjs[IF_CONST1]++;
     return p;
 }
 
@@ -93,6 +94,34 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
+void If_ManRestart( If_Man_t * p )
+{
+    FREE( p->pMemCi );
+    Vec_PtrClear( p->vCis );
+    Vec_PtrClear( p->vCos );
+    Vec_PtrClear( p->vObjs );
+    Vec_PtrClear( p->vMapped );
+    Vec_PtrClear( p->vTemp );
+    Mem_FixedRestart( p->pMemObj );
+    // create the constant node
+    p->pConst1 = If_ManSetupObj( p );
+    p->pConst1->Type = IF_CONST1;
+    p->pConst1->fPhase = 1;
+    // reset the counter of other nodes
+    p->nObjs[IF_CI] = p->nObjs[IF_CO] = p->nObjs[IF_AND] = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void If_ManStop( If_Man_t * p )
 {
     Vec_PtrFree( p->vCis );
@@ -103,7 +132,6 @@ void If_ManStop( If_Man_t * p )
     if ( p->vLatchOrder ) Vec_PtrFree( p->vLatchOrder );
     if ( p->vLags ) Vec_IntFree( p->vLags );
     Mem_FixedStop( p->pMemObj, 0 );
-//    Mem_FixedStop( p->pMemSet, 0 );
     FREE( p->pMemCi );
     FREE( p->pMemAnd );
     FREE( p->puTemp[0] );
@@ -190,6 +218,25 @@ If_Obj_t * If_ManCreateAnd( If_Man_t * p, If_Obj_t * pFan0, int fCompl0, If_Obj_
 
 /**Function*************************************************************
 
+  Synopsis    [Create the new node assuming it does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+If_Obj_t * If_ManCreateXnor( If_Man_t * p, If_Obj_t * pFan0, If_Obj_t * pFan1 )
+{
+    If_Obj_t * pRes1, * pRes2;
+    pRes1 = If_ManCreateAnd( p, pFan0, 0, pFan1, 1 );
+    pRes2 = If_ManCreateAnd( p, pFan0, 1, pFan1, 0 );
+    return If_ManCreateAnd( p, pRes1, 1, pRes2, 1 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates the choice node.]
 
   Description [Should be called after the equivalence class nodes are linked.]
@@ -460,11 +507,10 @@ void If_ManDerefChoiceCutSet( If_Man_t * p, If_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void If_ManSetupSetAll( If_Man_t * p )
+void If_ManSetupSetAll( If_Man_t * p, int nCrossCut )
 {
     If_Set_t * pCutSet;
-    int i, nCrossCut, nCutSets;
-    nCrossCut = If_ManCrossCut( p );
+    int i, nCutSets;
     nCutSets = 128 + nCrossCut;
     p->pFreeList = p->pMemAnd = pCutSet = (If_Set_t *)malloc( nCutSets * p->nSetBytes );
     for ( i = 0; i < nCutSets; i++ )