Rare bug fix in mapping with choices.

src/aig/gia/giaAig.c

@@ -100,6 +100,41 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Checks integrity of choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCheckChoices_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( !pObj || !Gia_ObjIsAnd(pObj) || pObj->fPhase )
+        return;
+    pObj->fPhase = 1;
+    Gia_ManCheckChoices_rec( p, Gia_ObjFanin0(pObj) );
+    Gia_ManCheckChoices_rec( p, Gia_ObjFanin1(pObj) );
+    Gia_ManCheckChoices_rec( p, Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)) );
+}
+void Gia_ManCheckChoices( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, fFound = 0;
+    Gia_ManCleanPhase( p );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManCheckChoices_rec( p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachAnd( p, pObj, i )
+        if ( !pObj->fPhase )
+            printf( "Object %d is dangling.\n", i ), fFound = 1;
+    if ( !fFound )
+        printf( "There are no dangling objects.\n" );
+    Gia_ManCleanPhase( p );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Duplicates AIG in the DFS order.]
@@ -155,6 +190,7 @@ Gia_Man_t * Gia_ManFromAigChoices( Aig_Man_t * p )
         Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     //assert( Gia_ManObjNum(pNew) == Aig_ManObjNum(p) );
+    //Gia_ManCheckChoices( pNew );
     return pNew;
 }
 

src/aig/gia/giaIf.c

@@ -756,6 +756,43 @@ int Gia_ManChoiceLevel( Gia_Man_t * p )
 } 
 
 
+/**Function*************************************************************
+
+  Synopsis    [Checks integrity of choice nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_ManCheckChoices_rec( If_Man_t * pIfMan, If_Obj_t * pIfObj )
+{
+    if ( !pIfObj || pIfObj->Type != IF_AND || pIfObj->fDriver )
+        return;
+    pIfObj->fDriver = 1;
+    If_ManCheckChoices_rec( pIfMan, If_ObjFanin0(pIfObj) );
+    If_ManCheckChoices_rec( pIfMan, If_ObjFanin1(pIfObj) );
+    If_ManCheckChoices_rec( pIfMan, pIfObj->pEquiv );
+}
+void If_ManCheckChoices( If_Man_t * pIfMan )
+{
+    If_Obj_t * pIfObj;
+    int i, fFound = 0;
+    If_ManForEachObj( pIfMan, pIfObj, i )
+        pIfObj->fDriver = 0;
+    If_ManForEachCo( pIfMan, pIfObj, i )
+        If_ManCheckChoices_rec( pIfMan, If_ObjFanin0(pIfObj) );
+    If_ManForEachNode( pIfMan, pIfObj, i )
+        if ( !pIfObj->fDriver )
+            printf( "Object %d is dangling.\n", i ), fFound = 1;
+    if ( !fFound )
+        printf( "There are no dangling objects.\n" );
+    If_ManForEachObj( pIfMan, pIfObj, i )
+        pIfObj->fDriver = 0;
+}
+
 
 /**Function*************************************************************
 
@@ -824,6 +861,7 @@ If_Man_t * Gia_ManToIf( Gia_Man_t * p, If_Par_t * pPars )
     }
     if ( Gia_ManHasChoices(p) )
         Gia_ManCleanMark0( p );
+    //If_ManCheckChoices( pIfMan );
     return pIfMan;
 }
 

src/map/if/ifMap.c

@@ -516,7 +516,8 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
 
     // remove elementary cuts
     for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
-        pTemp->pCutSet->nCuts--;
+        if ( pTemp != pObj || pTemp->pCutSet->nCuts > 1 )
+            pTemp->pCutSet->nCuts--;
 
     // update the cutset of the node
     pCutSet = pObj->pCutSet;