3 files changed, 69 insertions, 1 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index bb3c6524..eec6dd22 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -853,7 +853,9 @@ extern int                 Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t **
 extern Gia_Obj_t *         Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE );
 extern int                 Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
 extern int                 Gia_ManHasChoices( Gia_Man_t * p );
+extern void                Gia_ManVerifyChoices( Gia_Man_t * p );
 extern int                 Gia_ManHasDangling( Gia_Man_t * p );
+extern int                 Gia_ManMarkDangling( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManGetDangling( Gia_Man_t * p );
 extern void                Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern int                 Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 3c5ad848..492f55ef 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -53,7 +53,7 @@ int Gia_ManCheckTopoOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
         return 0;
     if ( !Gia_ManCheckTopoOrder_rec( p, Gia_ObjFanin1(pObj) ) )
         return 0;
-    pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
+    pRepr = p->pReprs ? Gia_ObjReprObj( p, Gia_ObjId(p,pObj) ) : NULL;
     return pRepr == NULL || pRepr->Value == 0;
 }
 
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index e56f6ea9..333fe58e 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -963,6 +963,41 @@ int Gia_ManHasChoices( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManVerifyChoices( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, fProb = 0;
+    assert( p->pReprs );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) )
+                printf( "Fanin 0 of AND node %d has a repr.\n", i ), fProb = 1;
+            if ( Gia_ObjHasRepr(p, Gia_ObjFaninId1(pObj, i)) )
+                printf( "Fanin 1 of AND node %d has a repr.\n", i ), fProb = 1;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+        {
+            if ( Gia_ObjHasRepr(p, Gia_ObjFaninId0(pObj, i)) )
+                printf( "Fanin 0 of CO node %d has a repr.\n", i ), fProb = 1;
+        }
+    }
+    if ( !fProb )
+        printf( "GIA with choices is correct.\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if AIG has dangling nodes.]
 
   Description []
@@ -1004,6 +1039,37 @@ int Gia_ManHasDangling( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Gia_ManMarkDangling( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter = 0;
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        pObj->fMark0 = 0;
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+            Gia_ObjFanin1(pObj)->fMark0 = 1;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+    }
+    Gia_ManForEachAnd( p, pObj, i )
+        Counter += !pObj->fMark0;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if AIG has dangling nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Vec_Int_t * Gia_ManGetDangling( Gia_Man_t * p )
 {
     Vec_Int_t * vDangles;