Unifying representation of mapping in GIA.

18 files changed, 365 insertions, 463 deletions

diff --git a/abclib.dsp b/abclib.dsp
index c4c9e0aa..a3228d4c 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3503,10 +3503,6 @@ SOURCE=.\src\aig\gia\giaCex.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\gia\giaChoice.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\aig\gia\giaCof.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 559d40a1..5d3a8762 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -127,9 +127,8 @@ struct Gia_Man_t_
     int            nFansAlloc;    // the size of fanout representation
     Vec_Int_t *    vFanoutNums;   // static fanout
     Vec_Int_t *    vFanout;       // static fanout
-    int *          pMapping;      // mapping for each node
-    int            nOffset;       // mapping offset
-    Vec_Int_t *    vMapping;
+    Vec_Int_t *    vMapping;      // mapping for each node
+    Vec_Int_t *    vPacking;      // packing information
     Vec_Int_t *    vLutConfigs;   // LUT configurations
     Abc_Cex_t *    pCexComb;      // combinational counter-example
     Abc_Cex_t *    pCexSeq;       // sequential counter-example
@@ -144,7 +143,6 @@ struct Gia_Man_t_
     Gia_Man_t *    pAigExtra;     // combinational logic of holes
     Vec_Flt_t *    vInArrs;       // PI arrival times
     Vec_Flt_t *    vOutReqs;      // PO required times
-    Vec_Int_t *    vPacking;      // packing information
     int *          pTravIds;      // separate traversal ID representation
     int            nTravIdsAlloc; // the number of trav IDs allocated
     Vec_Ptr_t *    vNamesIn;      // the input names 
@@ -310,7 +308,7 @@ static inline int          Gia_ManMuxNum( Gia_Man_t * p )      { return p->nMuxe
 static inline int          Gia_ManCandNum( Gia_Man_t * p )     { return Gia_ManCiNum(p) + Gia_ManAndNum(p);                                }
 static inline int          Gia_ManConstrNum( Gia_Man_t * p )   { return p->nConstrs;                                                       }
 static inline void         Gia_ManFlipVerbose( Gia_Man_t * p ) { p->fVerbose ^= 1;                                                         } 
-static inline int          Gia_ManWithChoices( Gia_Man_t * p ) { return p->pSibls != NULL;                                                 } 
+static inline int          Gia_ManHasChoices( Gia_Man_t * p )  { return p->pSibls != NULL;                                                 } 
 
 static inline Gia_Obj_t *  Gia_ManConst0( Gia_Man_t * p )      { return p->pObjs;                                                          }
 static inline Gia_Obj_t *  Gia_ManConst1( Gia_Man_t * p )      { return Gia_Not(Gia_ManConst0(p));                                         }
@@ -791,9 +789,10 @@ static inline void        Gia_ObjSetFanout( Gia_Man_t * p, Gia_Obj_t * pObj, int
 #define Gia_ObjForEachFanoutStatic( p, pObj, pFanout, i )      \
     for ( i = 0; (i < Gia_ObjFanoutNum(p, pObj))   && (((pFanout) = Gia_ObjFanout(p, pObj, i)), 1); i++ )
 
-static inline int         Gia_ObjIsLut( Gia_Man_t * p, int Id )             { return p->pMapping[Id] != 0;               }
-static inline int         Gia_ObjLutSize( Gia_Man_t * p, int Id )           { return p->pMapping[p->pMapping[Id]];       }
-static inline int *       Gia_ObjLutFanins( Gia_Man_t * p, int Id )         { return p->pMapping + p->pMapping[Id] + 1;  }
+static inline int         Gia_ManHasMapping( Gia_Man_t * p )                { return p->vMapping != NULL;                }
+static inline int         Gia_ObjIsLut( Gia_Man_t * p, int Id )             { return Vec_IntEntry(p->vMapping, Id) != 0; }
+static inline int         Gia_ObjLutSize( Gia_Man_t * p, int Id )           { return Vec_IntEntry(p->vMapping, Vec_IntEntry(p->vMapping, Id));       }
+static inline int *       Gia_ObjLutFanins( Gia_Man_t * p, int Id )         { return Vec_IntEntryP(p->vMapping, Vec_IntEntry(p->vMapping, Id)) + 1;  }
 static inline int         Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i )   { return Gia_ObjLutFanins(p, Id)[i];         }
 
 #define Gia_ManForEachLut( p, i )                              \
@@ -870,11 +869,6 @@ extern void                Gia_ManCounterExampleValueStop( Gia_Man_t * pGia );
 extern int                 Gia_ManCounterExampleValueLookup( Gia_Man_t * pGia, int Id, int iFrame );
 extern Abc_Cex_t *         Gia_ManCexExtendToIncludeCurrentStates( Gia_Man_t * p, Abc_Cex_t * pCex );
 extern Abc_Cex_t *         Gia_ManCexExtendToIncludeAllObjects( Gia_Man_t * p, Abc_Cex_t * pCex );
-/*=== giaChoice.c ============================================================*/
-extern void                Gia_ManVerifyChoices( Gia_Man_t * p );
-extern void                Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing );
-extern int                 Gia_ManHasChoices( Gia_Man_t * p );
-extern int                 Gia_ManChoiceLevel( Gia_Man_t * p );
 /*=== giaCsatOld.c ============================================================*/
 extern Vec_Int_t *         Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
 /*=== giaCsat.c ============================================================*/
@@ -1170,7 +1164,6 @@ extern Vec_Int_t *         Gia_ManSaveValue( Gia_Man_t * p );
 extern void                Gia_ManLoadValue( Gia_Man_t * p, Vec_Int_t * vValues );
 extern Vec_Int_t *         Gia_ManFirstFanouts( Gia_Man_t * p );
 
-
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
 extern Tas_Man_t *         Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index fd5996c9..8f199f43 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -612,17 +612,12 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
             {
                 extern int * Gia_AigerReadMapping( unsigned char ** ppPos, int nSize );
                 extern int * Gia_AigerReadMappingSimple( unsigned char ** ppPos, int nSize );
-                extern int * Gia_AigerReadMappingDoc( unsigned char ** ppPos, int nObjs, int * pOffset );
-                int nSize, nOffset;
+                extern Vec_Int_t * Gia_AigerReadMappingDoc( unsigned char ** ppPos, int nObjs );
+                int nSize;
                 pCur++;
                 nSize = Gia_AigerReadInt(pCur);
                 pCurTemp = pCur + nSize + 4;           pCur += 4;
-//                pNew->pMapping = Gia_AigerReadMapping( &pCur, Gia_ManObjNum(pNew) );
-//                pNew->pMapping = Gia_AigerReadMappingSimple( &pCur, nSize );
-//                pNew->nOffset = nSize / 4;
-//                pCur += nSize;
-                pNew->pMapping = Gia_AigerReadMappingDoc( &pCur, Gia_ManObjNum(pNew), &nOffset );
-                pNew->nOffset = nOffset;
+                pNew->vMapping = Gia_AigerReadMappingDoc( &pCur, Gia_ManObjNum(pNew) );
                 assert( pCur == pCurTemp );
                 if ( fVerbose ) printf( "Finished reading extension \"m\".\n" );
             }
@@ -786,6 +781,8 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
         ABC_FREE( pInit );
     }
     Vec_IntFreeP( &vInits );
+    if ( !fSkipStrash && pNew->vMapping )
+        Abc_Print( 0, "Structural hashing enabled while reading AIGER may have invalidated the mapping.  Consider using \"&r -s\".\n" );
     return pNew;
 }
 
@@ -1218,7 +1215,7 @@ void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         if ( fVerbose ) printf( "Finished writing extension \"k\".\n" );
     }
     // write mapping
-    if ( p->pMapping )
+    if ( Gia_ManHasMapping(p) )
     {
         extern Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p );
         extern Vec_Str_t * Gia_AigerWriteMappingSimple( Gia_Man_t * p );
diff --git a/src/aig/gia/giaAigerExt.c b/src/aig/gia/giaAigerExt.c
index f7781f5d..7b7758ff 100644
--- a/src/aig/gia/giaAigerExt.c
+++ b/src/aig/gia/giaAigerExt.c
@@ -171,7 +171,7 @@ unsigned char * Gia_AigerWriteMappingInt( Gia_Man_t * p, int * pMapSize )
 {
     unsigned char * pBuffer;
     int i, k, iPrev, iFan, nItems, iPos = 4;
-    assert( p->pMapping );
+    assert( Gia_ManHasMapping(p) );
     // count the number of entries to be written
     nItems = 0;
     Gia_ManForEachLut( p, i )
@@ -225,10 +225,10 @@ int * Gia_AigerReadMappingSimple( unsigned char ** ppPos, int nSize )
 }
 Vec_Str_t * Gia_AigerWriteMappingSimple( Gia_Man_t * p )
 {
-    unsigned char * pBuffer = ABC_ALLOC( unsigned char, 4*p->nOffset );
-    memcpy( pBuffer, p->pMapping, 4*p->nOffset );
-    assert( p->pMapping != NULL && p->nOffset >= Gia_ManObjNum(p) );
-    return Vec_StrAllocArray( (char *)pBuffer, 4*p->nOffset );
+    unsigned char * pBuffer = ABC_ALLOC( unsigned char, 4*Vec_IntSize(p->vMapping) );
+    memcpy( pBuffer, Vec_IntArray(p->vMapping), 4*Vec_IntSize(p->vMapping) );
+    assert( Vec_IntSize(p->vMapping) >= Gia_ManObjNum(p) );
+    return Vec_StrAllocArray( (char *)pBuffer, 4*Vec_IntSize(p->vMapping) );
 }
 
 /**Function*************************************************************
@@ -242,27 +242,27 @@ Vec_Str_t * Gia_AigerWriteMappingSimple( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int * Gia_AigerReadMappingDoc( unsigned char ** ppPos, int nObjs, int * pOffset )
+Vec_Int_t * Gia_AigerReadMappingDoc( unsigned char ** ppPos, int nObjs )
 {
-    int * pMapping, nLuts, LutSize, iRoot, nFanins, i, k;
+    int * pMapping, nLuts, LutSize, iRoot, nFanins, i, k, nOffset;
     nLuts    = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
     LutSize  = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
     pMapping = ABC_CALLOC( int, nObjs + (LutSize + 2) * nLuts );
-    *pOffset = nObjs;
+    nOffset = nObjs;
     for ( i = 0; i < nLuts; i++ )
     {
         iRoot   = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
         nFanins = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
-        pMapping[iRoot] = *pOffset;
+        pMapping[iRoot] = nOffset;
         // write one
-        pMapping[ (*pOffset)++ ] = nFanins; 
+        pMapping[ nOffset++ ] = nFanins; 
         for ( k = 0; k < nFanins; k++ )
         {
-            pMapping[ (*pOffset)++ ] = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
+            pMapping[ nOffset++ ] = Gia_AigerReadInt( *ppPos ); *ppPos += 4;
         }
-        pMapping[ (*pOffset)++ ] = iRoot; 
+        pMapping[ nOffset++ ] = iRoot; 
     }
-    return pMapping;
+    return Vec_IntAllocArray( pMapping, nOffset );
 }
 Vec_Str_t * Gia_AigerWriteMappingDoc( Gia_Man_t * p )
 {
diff --git a/src/aig/gia/giaChoice.c b/src/aig/gia/giaChoice.c
deleted file mode 100644
index ca2acb28..00000000
--- a/src/aig/gia/giaChoice.c
+++ /dev/null
@@ -1,373 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [giaChoice.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Scalable AIG package.]
-
-  Synopsis    [Normalization of structural choices.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: giaChoice.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "gia.h"
-#include "giaAig.h"
-#include "misc/tim/tim.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Reverse the order of nodes in equiv classes.]
-
-  Description [If the flag is 1, assumed current increasing order ]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing )
-{
-    Vec_Int_t * vCollected;
-    Vec_Int_t * vClass;
-    int i, k, iRepr, iNode, iPrev;
-    // collect classes
-    vCollected = Vec_IntAlloc( 100 );
-    Gia_ManForEachClass( p, iRepr )
-        Vec_IntPush( vCollected, iRepr );
-    // correct each class
-    vClass = Vec_IntAlloc( 100 );
-    Vec_IntForEachEntry( vCollected, iRepr, i )
-    {
-        Vec_IntClear( vClass );
-        Vec_IntPush( vClass, iRepr );
-        Gia_ClassForEachObj1( p, iRepr, iNode )
-        {
-            if ( fNowIncreasing )
-                assert( iRepr < iNode );
-            else
-                assert( iRepr > iNode );
-            Vec_IntPush( vClass, iNode );
-        }
-//        if ( !fNowIncreasing )
-//            Vec_IntSort( vClass, 1 );
-        // reverse the class
-        iPrev = 0;
-        iRepr = Vec_IntEntryLast( vClass );
-        Vec_IntForEachEntry( vClass, iNode, k )
-        {
-            if ( fNowIncreasing )
-                Gia_ObjSetReprRev( p, iNode, iNode == iRepr ? GIA_VOID : iRepr );
-            else
-                Gia_ObjSetRepr( p, iNode, iNode == iRepr ? GIA_VOID : iRepr );
-            Gia_ObjSetNext( p, iNode, iPrev );
-            iPrev = iNode;
-        }
-    }
-    Vec_IntFree( vCollected );
-    Vec_IntFree( vClass );
-    // verify
-    Gia_ManForEachClass( p, iRepr )
-        Gia_ClassForEachObj1( p, iRepr, iNode )
-            if ( fNowIncreasing )
-                assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr > iNode );
-            else
-                assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr < iNode );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManVerifyChoices( Gia_Man_t * p )
-{
-    Gia_Obj_t * pObj;
-    int i, iRepr, iNode, fProb = 0;
-    assert( p->pReprs );
-
-    // mark nodes 
-    Gia_ManCleanMark0(p);
-    Gia_ManForEachClass( p, iRepr )
-        Gia_ClassForEachObj1( p, iRepr, iNode )
-        {
-            if ( Gia_ObjIsHead(p, iNode) )
-                printf( "Member %d of choice class %d is a representative.\n", iNode, iRepr ), fProb = 1;
-            if ( Gia_ManObj( p, iNode )->fMark0 == 1 )
-                printf( "Node %d participates in more than one choice node.\n", iNode ), fProb = 1;
-            Gia_ManObj( p, iNode )->fMark0 = 1;
-        }
-    Gia_ManCleanMark0(p);
-
-    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    [Make sure reprsentative nodes do not have representatives.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManCheckReprs( Gia_Man_t * p )
-{
-    Gia_Obj_t * pObj;
-    int i, fProb = 0;
-    Gia_ManForEachObj( p, pObj, i )
-    {
-        if ( !Gia_ObjHasRepr(p, i) )
-            continue;
-        if ( !Gia_ObjIsAnd(pObj) )
-            printf( "Obj %d is not an AND but it has a repr %d.\n", i, Gia_ObjRepr(p, i) ), fProb = 1;
-        else if ( Gia_ObjHasRepr( p, Gia_ObjRepr(p, i) ) )
-            printf( "Obj %d has repr %d with a repr %d.\n", i, Gia_ObjRepr(p, i), Gia_ObjRepr(p, Gia_ObjRepr(p, i)) ), fProb = 1;
-    }
-    if ( !fProb )
-        printf( "GIA \"%s\": Representive verification successful.\n", Gia_ManName(p) );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if AIG has choices.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManHasChoices( Gia_Man_t * p )
-{
-    Gia_Obj_t * pObj;
-    int i, Counter1 = 0, Counter2 = 0;
-    int nFailNoRepr = 0;
-    int nFailHaveRepr = 0;
-    int nChoiceNodes = 0;
-    int nChoices = 0;
-    if ( p->pReprs == NULL || p->pNexts == NULL )
-        return 0;
-    // check if there are any representatives
-    Gia_ManForEachObj( p, pObj, i )
-    {
-        if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
-        {
-//            printf( "%d ", i );
-            Counter1++;
-        }
-//        if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
-//            Counter2++;
-    }
-//    printf( "\n" );
-    Gia_ManForEachObj( p, pObj, i )
-    {
-//        if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
-//            Counter1++;
-        if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
-        {
-//            printf( "%d ", i );
-            Counter2++;
-        }
-    }
-//    printf( "\n" );
-    if ( Counter1 == 0 )
-    {
-        printf( "Warning: AIG has repr data-strucure but not reprs.\n" );
-        return 0;
-    }
-    printf( "%d nodes have reprs.\n", Counter1 );
-    printf( "%d nodes have nexts.\n", Counter2 );
-    // check if there are any internal nodes without fanout
-    // make sure all nodes without fanout have representatives
-    // make sure all nodes with fanout have no representatives
-    ABC_FREE( p->pRefs );
-    Gia_ManCreateRefs( p );
-    Gia_ManForEachAnd( p, pObj, i )
-    {
-        if ( Gia_ObjRefNum(p, pObj) == 0 )
-        {
-            if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL )
-                nFailNoRepr++;
-            else
-                nChoices++;
-        }
-        else
-        {
-            if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL )
-                nFailHaveRepr++;
-            if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL )
-                nChoiceNodes++;
-        }
-        if ( Gia_ObjReprObj( p, i ) )
-            assert( Gia_ObjRepr(p, i) < i );
-    }
-    if ( nChoices == 0 )
-        return 0;
-    if ( nFailNoRepr )
-    {
-        printf( "Gia_ManHasChoices(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr );
-//        return 0;
-    }
-    if ( nFailHaveRepr )
-    {
-        printf( "Gia_ManHasChoices(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr );
-//        return 0;
-    }
-//    printf( "Gia_ManHasChoices(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices );
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Computes levels for AIG with choices and white boxes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManChoiceLevel_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
-{
-    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
-    Gia_Obj_t * pNext;
-    int i, iBox, iTerm1, nTerms, LevelMax = 0;
-    if ( Gia_ObjIsTravIdCurrent( p, pObj ) )
-        return;
-    Gia_ObjSetTravIdCurrent( p, pObj );
-    if ( Gia_ObjIsCi(pObj) )
-    {
-        if ( pManTime )
-        {
-            iBox = Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) );
-            if ( iBox >= 0 ) // this is not a true PI
-            {
-                iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
-                nTerms = Tim_ManBoxInputNum( pManTime, iBox );
-                for ( i = 0; i < nTerms; i++ )
-                {
-                    pNext = Gia_ManCo( p, iTerm1 + i );
-                    Gia_ManChoiceLevel_rec( p, pNext );
-                    if ( LevelMax < Gia_ObjLevel(p, pNext) )
-                        LevelMax = Gia_ObjLevel(p, pNext);
-                }
-                LevelMax++;
-            }
-        }
-//        Abc_Print( 1, "%d ", pObj->Level );
-    }
-    else if ( Gia_ObjIsCo(pObj) )
-    {
-        pNext = Gia_ObjFanin0(pObj);
-        Gia_ManChoiceLevel_rec( p, pNext );
-        if ( LevelMax < Gia_ObjLevel(p, pNext) )
-            LevelMax = Gia_ObjLevel(p, pNext);
-    }
-    else if ( Gia_ObjIsAnd(pObj) )
-    { 
-        // get the maximum level of the two fanins
-        pNext = Gia_ObjFanin0(pObj);
-        Gia_ManChoiceLevel_rec( p, pNext );
-        if ( LevelMax < Gia_ObjLevel(p, pNext) )
-            LevelMax = Gia_ObjLevel(p, pNext);
-        pNext = Gia_ObjFanin1(pObj);
-        Gia_ManChoiceLevel_rec( p, pNext );
-        if ( LevelMax < Gia_ObjLevel(p, pNext) )
-            LevelMax = Gia_ObjLevel(p, pNext);
-        LevelMax++;
-
-        // get the level of the nodes in the choice node
-        if ( p->pSibls && (pNext = Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))) )
-        {
-            Gia_ManChoiceLevel_rec( p, pNext );
-            if ( LevelMax < Gia_ObjLevel(p, pNext) )
-                LevelMax = Gia_ObjLevel(p, pNext);
-        }
-    }
-    else if ( !Gia_ObjIsConst0(pObj) )
-        assert( 0 );
-    Gia_ObjSetLevel( p, pObj, LevelMax );
-}
-int Gia_ManChoiceLevel( Gia_Man_t * p )
-{
-    Gia_Obj_t * pObj;
-    int i, LevelMax = 0;
-//    assert( Gia_ManRegNum(p) == 0 );
-    Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
-    Gia_ManIncrementTravId( p );
-    Gia_ManForEachCo( p, pObj, i )
-    {
-        Gia_ManChoiceLevel_rec( p, pObj );
-        if ( LevelMax < Gia_ObjLevel(p, pObj) )
-            LevelMax = Gia_ObjLevel(p, pObj);
-    }
-    // account for dangling boxes
-    Gia_ManForEachCi( p, pObj, i )
-    {
-        Gia_ManChoiceLevel_rec( p, pObj );
-        if ( LevelMax < Gia_ObjLevel(p, pObj) )
-            LevelMax = Gia_ObjLevel(p, pObj);
-//        Abc_Print( 1, "%d ", Gia_ObjLevel(p, pObj) );
-    }
-//    Abc_Print( 1, "\n" );
-    Gia_ManForEachAnd( p, pObj, i )
-        assert( Gia_ObjLevel(p, pObj) > 0 );
-//    printf( "Max level %d\n", LevelMax );
-    return LevelMax;
-} 
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/gia/giaHcd.c b/src/aig/gia/giaHcd.c
index 11f81e0a..5d3e28f5 100644
--- a/src/aig/gia/giaHcd.c
+++ b/src/aig/gia/giaHcd.c
@@ -642,7 +642,7 @@ Aig_Man_t * Hcd_ComputeChoices( Aig_Man_t * pAig, int nBTLimit, int fSynthesis,
     Vec_PtrFree( vGias );
     if ( fVerbose )
         ABC_PRT( "Choicing time", clock() - clk );
-    Gia_ManHasChoices( pGia );
+//    Gia_ManHasChoices_very_old( pGia );
     // transform back
     pAigNew = Gia_ManToAig( pGia, 1 );
     Gia_ManStop( pGia );
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 2e8805ae..e42cf638 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -215,7 +215,7 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p )
 {
     int * pLevels;
     int i, k, iFan, nLutSize = 0, nLuts = 0, nFanins = 0, LevelMax = 0;
-    if ( !p->pMapping )
+    if ( !Gia_ManHasMapping(p) )
         return;
     pLevels = ABC_CALLOC( int, Gia_ManObjNum(p) );
     Gia_ManForEachLut( p, i )
@@ -285,6 +285,107 @@ void Gia_ManPrintPackingStats( Gia_Man_t * p )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Computes levels for AIG with choices and white boxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManChoiceLevel_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
+    Gia_Obj_t * pNext;
+    int i, iBox, iTerm1, nTerms, LevelMax = 0;
+    if ( Gia_ObjIsTravIdCurrent( p, pObj ) )
+        return;
+    Gia_ObjSetTravIdCurrent( p, pObj );
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        if ( pManTime )
+        {
+            iBox = Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) );
+            if ( iBox >= 0 ) // this is not a true PI
+            {
+                iTerm1 = Tim_ManBoxInputFirst( pManTime, iBox );
+                nTerms = Tim_ManBoxInputNum( pManTime, iBox );
+                for ( i = 0; i < nTerms; i++ )
+                {
+                    pNext = Gia_ManCo( p, iTerm1 + i );
+                    Gia_ManChoiceLevel_rec( p, pNext );
+                    if ( LevelMax < Gia_ObjLevel(p, pNext) )
+                        LevelMax = Gia_ObjLevel(p, pNext);
+                }
+                LevelMax++;
+            }
+        }
+//        Abc_Print( 1, "%d ", pObj->Level );
+    }
+    else if ( Gia_ObjIsCo(pObj) )
+    {
+        pNext = Gia_ObjFanin0(pObj);
+        Gia_ManChoiceLevel_rec( p, pNext );
+        if ( LevelMax < Gia_ObjLevel(p, pNext) )
+            LevelMax = Gia_ObjLevel(p, pNext);
+    }
+    else if ( Gia_ObjIsAnd(pObj) )
+    { 
+        // get the maximum level of the two fanins
+        pNext = Gia_ObjFanin0(pObj);
+        Gia_ManChoiceLevel_rec( p, pNext );
+        if ( LevelMax < Gia_ObjLevel(p, pNext) )
+            LevelMax = Gia_ObjLevel(p, pNext);
+        pNext = Gia_ObjFanin1(pObj);
+        Gia_ManChoiceLevel_rec( p, pNext );
+        if ( LevelMax < Gia_ObjLevel(p, pNext) )
+            LevelMax = Gia_ObjLevel(p, pNext);
+        LevelMax++;
+
+        // get the level of the nodes in the choice node
+        if ( (pNext = Gia_ObjSiblObj(p, Gia_ObjId(p, pObj))) )
+        {
+            Gia_ManChoiceLevel_rec( p, pNext );
+            if ( LevelMax < Gia_ObjLevel(p, pNext) )
+                LevelMax = Gia_ObjLevel(p, pNext);
+        }
+    }
+    else if ( !Gia_ObjIsConst0(pObj) )
+        assert( 0 );
+    Gia_ObjSetLevel( p, pObj, LevelMax );
+}
+int Gia_ManChoiceLevel( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, LevelMax = 0;
+//    assert( Gia_ManRegNum(p) == 0 );
+    Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        Gia_ManChoiceLevel_rec( p, pObj );
+        if ( LevelMax < Gia_ObjLevel(p, pObj) )
+            LevelMax = Gia_ObjLevel(p, pObj);
+    }
+    // account for dangling boxes
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        Gia_ManChoiceLevel_rec( p, pObj );
+        if ( LevelMax < Gia_ObjLevel(p, pObj) )
+            LevelMax = Gia_ObjLevel(p, pObj);
+//        Abc_Print( 1, "%d ", Gia_ObjLevel(p, pObj) );
+    }
+//    Abc_Print( 1, "\n" );
+    Gia_ManForEachAnd( p, pObj, i )
+        assert( Gia_ObjLevel(p, pObj) > 0 );
+//    printf( "Max level %d\n", LevelMax );
+    return LevelMax;
+} 
+
+
 
 /**Function*************************************************************
 
@@ -606,9 +707,16 @@ int Gia_ManFromIfLogicNode( Gia_Man_t * pNew, int iObj, Vec_Int_t * vLeaves, Vec
         // derive truth table
         if ( Kit_TruthIsConst0((unsigned *)pRes, nLeaves) || Kit_TruthIsConst1((unsigned *)pRes, nLeaves) )
         {
-            assert( 0 );
 //            fprintf( pFile, ".names %s\n %d\n", Abc_ObjName(Abc_ObjFanout0(pObj)), Kit_TruthIsConst1((unsigned *)pRes, nLeaves) );
-            return -1;
+            iObjLit1 = Abc_LitNotCond( 0, Kit_TruthIsConst1((unsigned *)pRes, nLeaves) );
+            // write mapping
+            if ( Vec_IntEntry(vMapping, 0) == 0 )
+            {
+                Vec_IntSetEntry( vMapping, 0, Vec_IntSize(vMapping2) );
+                Vec_IntPush( vMapping2, 0 );
+                Vec_IntPush( vMapping2, 0 );
+            }
+            return iObjLit1;
         }
 
         // perform decomposition
@@ -928,18 +1036,15 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
     Vec_IntAppend( vMapping, vMapping2 );
     Vec_IntFree( vMapping2 );
     // attach mapping and packing
-    pNew->nOffset  = Vec_IntSize(vMapping);
-    pNew->pMapping = Vec_IntReleaseArray(vMapping);
+    assert( pNew->vMapping == NULL );
+    assert( pNew->vPacking == NULL );
+    pNew->vMapping = vMapping;
     pNew->vPacking = vPacking;
-    Vec_IntFree( vMapping );
     // verify that COs have mapping
     {
         Gia_Obj_t * pObj;
         Gia_ManForEachCo( pNew, pObj, i )
-        {
-            if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) )
-                assert( pNew->pMapping[Gia_ObjFaninId0p(pNew, pObj)] != 0 );
-        }
+           assert( !Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) || Gia_ObjIsLut(pNew, Gia_ObjFaninId0p(pNew, pObj)) );
     }
     return pNew;
 }
@@ -979,17 +1084,7 @@ void Gia_ManMappingVerify( Gia_Man_t * p )
 {
     Gia_Obj_t * pObj, * pFanin;
     int i, Result = 1;
-/*
-    if ( p->pMapping )
-    {
-        assert( p->nOffset != 0 );
-        Vec_IntFreeP( p->vMapping );
-        Vec_IntAlloc( p->vMapping, p->nOffset );
-        memmove( Vec_IntArray(p->vMapping), p->pMapping, p->nOffset );
-    }
-    assert( p->vMapping );
-*/
-    assert( p->pMapping );
+    assert( Gia_ManHasMapping(p) );
     Gia_ManIncrementTravId( p );
     Gia_ManForEachCo( p, pObj, i )
     {
@@ -1024,7 +1119,7 @@ void Gia_ManTransferMapping( Gia_Man_t * pGia, Gia_Man_t * p )
 {
     Gia_Obj_t * pObj;
     int i, k, iFan;
-    if ( pGia->pMapping == NULL )
+    if ( !Gia_ManHasMapping(pGia) )
         return;
     Gia_ManMappingVerify( pGia );
     Vec_IntFreeP( &p->vMapping );
@@ -1040,12 +1135,6 @@ void Gia_ManTransferMapping( Gia_Man_t * pGia, Gia_Man_t * p )
             Vec_IntPush( p->vMapping, Abc_Lit2Var(Gia_ObjValue(Gia_ManObj(pGia, iFan))) );
         Vec_IntPush( p->vMapping, Gia_ObjId(p, pObj) );
     }
-    // create standard mapping
-    assert( p->pMapping == NULL );
-    p->pMapping = Vec_IntArray( p->vMapping );
-    p->vMapping->pArray = NULL;
-    p->nOffset = Vec_IntSize(p->vMapping);
-    p->vMapping->nSize = 0;
     Gia_ManMappingVerify( p );
 }
 
@@ -1112,9 +1201,9 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp, int fNormalized )
     Gia_Man_t * pNew;
     If_Man_t * pIfMan;
     If_Par_t * pPars = (If_Par_t *)pp;
-    // disable cut minimization
-    if ( !(pPars->fDelayOpt || pPars->fUserRecLib) && !pPars->fDeriveLuts )//&& Gia_ManWithChoices(p) )
-        pPars->fCutMin = 0; // not compatible with deriving result
+    // disable cut minimization when GIA strucure is needed
+    if ( !pPars->fDelayOpt && !pPars->fUserRecLib && !pPars->fDeriveLuts )
+        pPars->fCutMin = 0;
     // reconstruct GIA according to the hierarchy manager
     assert( pPars->pTimesArr == NULL );
     assert( pPars->pTimesReq == NULL );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 5738595b..a573e9e7 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -111,7 +111,7 @@ void Gia_ManStop( Gia_Man_t * p )
     ABC_FREE( p->pCexSeq );
     ABC_FREE( p->pCexComb );
     ABC_FREE( p->pIso );
-    ABC_FREE( p->pMapping );
+//    ABC_FREE( p->pMapping );
     ABC_FREE( p->pFanData );
     ABC_FREE( p->pReprsOld );
     ABC_FREE( p->pReprs );
@@ -337,7 +337,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fTents, int fSwitch, int fCut )
         Gia_ManEquivPrintClasses( p, 0, 0.0 );
     if ( p->pSibls )
         Gia_ManPrintChoiceStats( p );
-    if ( p->pMapping )
+    if ( Gia_ManHasMapping(p) )
         Gia_ManPrintMappingStats( p );
     if ( p->vPacking )
         Gia_ManPrintPackingStats( p );
@@ -498,7 +498,7 @@ void Gia_ManPrintNpnClasses( Gia_Man_t * p )
     int * pLutClass, ClassCounts[222] = {0};
     int i, k, iFan, Class, OtherClasses, OtherClasses2, nTotal, Counter, Counter2;
     unsigned * pTruth;
-    assert( p->pMapping != NULL );
+    assert( Gia_ManHasMapping(p) );
     assert(  Gia_ManLutSizeMax( p ) <= 4 );
     vLeaves   = Vec_IntAlloc( 100 );
     vVisited  = Vec_IntAlloc( 100 );
diff --git a/src/aig/gia/giaShrink.c b/src/aig/gia/giaShrink.c
index af727726..1060dbe2 100644
--- a/src/aig/gia/giaShrink.c
+++ b/src/aig/gia/giaShrink.c
@@ -56,7 +56,7 @@ Gia_Man_t * Gia_ManMapShrink4( Gia_Man_t * p, int fKeepLevel, int fVerbose )
     abctime clk = Abc_Clock();
 //    int ClassCounts[222] = {0};
     int * pLutClass, Counter = 0;
-    assert( p->pMapping != NULL );
+    assert( Gia_ManHasMapping(p) );
     if ( Gia_ManLutSizeMax( p ) > 4 )
     {
         printf( "Resynthesis is not performed when nodes have more than 4 inputs.\n" );
diff --git a/src/aig/gia/giaShrink6.c b/src/aig/gia/giaShrink6.c
index 5ca95fd3..5deb033c 100644
--- a/src/aig/gia/giaShrink6.c
+++ b/src/aig/gia/giaShrink6.c
@@ -404,7 +404,7 @@ Gia_Man_t * Gia_ManMapShrink6( Gia_Man_t * p, int nFanoutMax, int fKeepLevel, in
     int RetValue, Counter1 = 0, Counter2 = 0;
     abctime clk2, clk = Abc_Clock();
     abctime timeFanout = 0;
-    assert( p->pMapping != NULL );
+    assert( Gia_ManHasMapping(p) );
     pMan = Shr_ManAlloc( p );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
diff --git a/src/aig/gia/giaSpeedup.c b/src/aig/gia/giaSpeedup.c
index 5be4dae9..b23decae 100644
--- a/src/aig/gia/giaSpeedup.c
+++ b/src/aig/gia/giaSpeedup.c
@@ -635,7 +635,7 @@ Gia_Man_t * Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int Degree, int fVerb
     int fUseLutLib = (p->pLutLib != NULL);
     void * pTempTim = NULL;
     unsigned * puTCEdges;
-    assert( p->pMapping != NULL );
+    assert( Gia_ManHasMapping(p) );
     if ( !fUseLutLib && p->pManTime )
     {
         pTempTim = p->pManTime;
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 99557c7a..2faf424e 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1443,6 +1443,98 @@ Vec_Int_t * Gia_ManFirstFanouts( Gia_Man_t * p )
     return vFans;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if AIG has choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManHasChoices_very_old( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter1 = 0, Counter2 = 0;
+    int nFailNoRepr = 0;
+    int nFailHaveRepr = 0;
+    int nChoiceNodes = 0;
+    int nChoices = 0;
+    if ( p->pReprs == NULL || p->pNexts == NULL )
+        return 0;
+    // check if there are any representatives
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
+        {
+//            printf( "%d ", i );
+            Counter1++;
+        }
+//        if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
+//            Counter2++;
+    }
+//    printf( "\n" );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+//        if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
+//            Counter1++;
+        if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
+        {
+//            printf( "%d ", i );
+            Counter2++;
+        }
+    }
+//    printf( "\n" );
+    if ( Counter1 == 0 )
+    {
+        printf( "Warning: AIG has repr data-strucure but not reprs.\n" );
+        return 0;
+    }
+    printf( "%d nodes have reprs.\n", Counter1 );
+    printf( "%d nodes have nexts.\n", Counter2 );
+    // check if there are any internal nodes without fanout
+    // make sure all nodes without fanout have representatives
+    // make sure all nodes with fanout have no representatives
+    ABC_FREE( p->pRefs );
+    Gia_ManCreateRefs( p );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( Gia_ObjRefNum(p, pObj) == 0 )
+        {
+            if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL )
+                nFailNoRepr++;
+            else
+                nChoices++;
+        }
+        else
+        {
+            if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL )
+                nFailHaveRepr++;
+            if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL )
+                nChoiceNodes++;
+        }
+        if ( Gia_ObjReprObj( p, i ) )
+            assert( Gia_ObjRepr(p, i) < i );
+    }
+    if ( nChoices == 0 )
+        return 0;
+    if ( nFailNoRepr )
+    {
+        printf( "Gia_ManHasChoices_very_old(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr );
+//        return 0;
+    }
+    if ( nFailHaveRepr )
+    {
+        printf( "Gia_ManHasChoices_very_old(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr );
+//        return 0;
+    }
+//    printf( "Gia_ManHasChoices_very_old(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices );
+    return 1;
+}
+
+
 #include "base/main/mainInt.h"
 
 /**Function*************************************************************
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 8cdbe137..aeda2428 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -4,7 +4,6 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaBidec.c \
     src/aig/gia/giaCCof.c \
     src/aig/gia/giaCex.c \
-    src/aig/gia/giaChoice.c \
     src/aig/gia/giaCof.c \
     src/aig/gia/giaCone.c \
     src/aig/gia/giaCSatOld.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 95e7320a..1ba51f0b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -24728,7 +24728,7 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Empty network.\n" );
         return 1;
     }
-    if ( pAbc->pGia->pMapping )
+    if ( Gia_ManHasMapping(pAbc->pGia) )
     {
         extern Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p );
         pNtk = Abc_NtkFromMappedGia( pAbc->pGia );
@@ -26861,7 +26861,7 @@ int Abc_CommandAbc9Bidec( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Bidec(): There is no AIG.\n" );
         return 1;
     }
-    if ( pAbc->pGia->pMapping == NULL )
+    if ( !Gia_ManHasMapping(pAbc->pGia) )
     {
         Abc_Print( -1, "Abc_CommandAbc9Bidec(): Mapping of the AIG is not defined.\n" );
         return 1;
@@ -26930,7 +26930,7 @@ int Abc_CommandAbc9Shrink( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Shrink(): There is no AIG.\n" );
         return 1;
     }
-    if ( pAbc->pGia->pMapping == NULL )
+    if ( !Gia_ManHasMapping(pAbc->pGia) )
     {
         Abc_Print( -1, "Abc_CommandAbc9Shrink(): Mapping of the AIG is not defined.\n" );
         return 1;
@@ -29256,7 +29256,7 @@ int Abc_CommandAbc9Trace( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Speedup(): There is no AIG to map.\n" );
         return 1;
     }
-    if ( pAbc->pGia->pMapping == NULL )
+    if ( !Gia_ManHasMapping(pAbc->pGia) )
     {
         Abc_Print( -1, "Abc_CommandAbc9Speedup(): Mapping of the AIG is not defined.\n" );
         return 1;
@@ -29347,7 +29347,7 @@ int Abc_CommandAbc9Speedup( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Speedup(): There is no AIG to map.\n" );
         return 1;
     }
-    if ( pAbc->pGia->pMapping == NULL )
+    if ( !Gia_ManHasMapping(pAbc->pGia) )
     {
         Abc_Print( -1, "Abc_CommandAbc9Speedup(): Mapping of the AIG is not defined.\n" );
         return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index de750146..552b124c 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -711,7 +711,7 @@ Abc_Ntk_t * Abc_NtkFromMappedGia( Gia_Man_t * p )
     Gia_Obj_t * pObj, * pObjLi, * pObjLo;
     Vec_Ptr_t * vReflect;
     int i, k, iFan, nDupGates; 
-    assert( p->pMapping != NULL );
+    assert( Gia_ManHasMapping(p) );
     pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_AIG, 1 );
     // duplicate the name and the spec
     pNtkNew->pName = Extra_UtilStrsav(p->pName);
diff --git a/src/base/abci/abcTim.c b/src/base/abci/abcTim.c
index 1f1b28f4..98d3220a 100644
--- a/src/base/abci/abcTim.c
+++ b/src/base/abci/abcTim.c
@@ -431,6 +431,115 @@ Gia_Man_t * Abc_NtkTestTimPerformSynthesis( Gia_Man_t * p, int fChoices )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManVerifyChoices( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, iRepr, iNode, fProb = 0;
+    assert( p->pReprs );
+
+    // mark nodes 
+    Gia_ManCleanMark0(p);
+    Gia_ManForEachClass( p, iRepr )
+        Gia_ClassForEachObj1( p, iRepr, iNode )
+        {
+            if ( Gia_ObjIsHead(p, iNode) )
+                printf( "Member %d of choice class %d is a representative.\n", iNode, iRepr ), fProb = 1;
+            if ( Gia_ManObj( p, iNode )->fMark0 == 1 )
+                printf( "Node %d participates in more than one choice node.\n", iNode ), fProb = 1;
+            Gia_ManObj( p, iNode )->fMark0 = 1;
+        }
+    Gia_ManCleanMark0(p);
+
+    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    [Reverse the order of nodes in equiv classes.]
+
+  Description [If the flag is 1, assumed current increasing order ]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManReverseClasses( Gia_Man_t * p, int fNowIncreasing )
+{
+    Vec_Int_t * vCollected;
+    Vec_Int_t * vClass;
+    int i, k, iRepr, iNode, iPrev;
+    // collect classes
+    vCollected = Vec_IntAlloc( 100 );
+    Gia_ManForEachClass( p, iRepr )
+        Vec_IntPush( vCollected, iRepr );
+    // correct each class
+    vClass = Vec_IntAlloc( 100 );
+    Vec_IntForEachEntry( vCollected, iRepr, i )
+    {
+        Vec_IntClear( vClass );
+        Vec_IntPush( vClass, iRepr );
+        Gia_ClassForEachObj1( p, iRepr, iNode )
+        {
+            if ( fNowIncreasing )
+                assert( iRepr < iNode );
+            else
+                assert( iRepr > iNode );
+            Vec_IntPush( vClass, iNode );
+        }
+//        if ( !fNowIncreasing )
+//            Vec_IntSort( vClass, 1 );
+        // reverse the class
+        iPrev = 0;
+        iRepr = Vec_IntEntryLast( vClass );
+        Vec_IntForEachEntry( vClass, iNode, k )
+        {
+            if ( fNowIncreasing )
+                Gia_ObjSetReprRev( p, iNode, iNode == iRepr ? GIA_VOID : iRepr );
+            else
+                Gia_ObjSetRepr( p, iNode, iNode == iRepr ? GIA_VOID : iRepr );
+            Gia_ObjSetNext( p, iNode, iPrev );
+            iPrev = iNode;
+        }
+    }
+    Vec_IntFree( vCollected );
+    Vec_IntFree( vClass );
+    // verify
+    Gia_ManForEachClass( p, iRepr )
+        Gia_ClassForEachObj1( p, iRepr, iNode )
+            if ( fNowIncreasing )
+                assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr > iNode );
+            else
+                assert( Gia_ObjRepr(p, iNode) == iRepr && iRepr < iNode );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Tests the hierarchy-timing manager.]
 
   Description []
@@ -445,7 +554,7 @@ void Abc_NtkTestTimByWritingFile( Gia_Man_t * pGia, char * pFileName )
     Gia_Man_t * pGia2;
 
     // normalize choices
-    if ( Gia_ManWithChoices(pGia) )
+    if ( Gia_ManHasChoices(pGia) )
     {
         Gia_ManVerifyChoices( pGia );
         Gia_ManReverseClasses( pGia, 0 );
@@ -453,14 +562,14 @@ void Abc_NtkTestTimByWritingFile( Gia_Man_t * pGia, char * pFileName )
     // write file
     Gia_AigerWrite( pGia, pFileName, 0, 0 );
     // unnormalize choices
-    if ( Gia_ManWithChoices(pGia) )
+    if ( Gia_ManHasChoices(pGia) )
         Gia_ManReverseClasses( pGia, 1 );
 
     // read file
     pGia2 = Gia_AigerRead( pFileName, 1, 1 );
 
     // normalize choices
-    if ( Gia_ManWithChoices(pGia2) )
+    if ( Gia_ManHasChoices(pGia2) )
     {
         Gia_ManVerifyChoices( pGia2 );
         Gia_ManReverseClasses( pGia2, 1 );
diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c
index 01b5adec..49025630 100644
--- a/src/proof/cec/cecChoice.c
+++ b/src/proof/cec/cecChoice.c
@@ -320,7 +320,7 @@ Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc
     RetValue = Cec_ManChoiceComputation_int( pGia, pPars );
     // derive AIG with choices
     pNew = Gia_ManEquivToChoices( pGia, nGias );
-    Gia_ManHasChoices( pNew );
+//    Gia_ManHasChoices_very_old( pNew );
 //    Gia_ManStop( pMiter );
     // report the results
     if ( pPars->fVerbose )
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index fac30004..83345ae5 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -1188,7 +1188,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     if ( pPars->fMakeChoices )
     {
         pNew = Gia_ManEquivToChoices( pAig, 1 );
-        Gia_ManHasChoices( pNew );
+//        Gia_ManHasChoices_very_old( pNew );
     }
     else
     {