From 73f8b598ac0809f646007c84504ac6afb2a922e8 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 29 Oct 2020 17:21:37 -0700
Subject: Rare bug fix in mapping with choices.

---
 src/aig/gia/giaAig.c | 36 ++++++++++++++++++++++++++++++++++++
 src/aig/gia/giaIf.c  | 38 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 74 insertions(+)

(limited to 'src/aig/gia')

diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index dfd4a467..91a9c600 100644
--- a/src/aig/gia/giaAig.c
+++ b/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;
 }
 
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 2c206292..614f7b47 100644
--- a/src/aig/gia/giaIf.c
+++ b/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;
 }
 
-- 
cgit v1.2.3