initial commit of public abc

34 files changed, 1717 insertions, 332 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 45b509dc..385d93b2 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -21,6 +21,7 @@
 #ifndef __AIG_H__
 #define __AIG_H__
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -37,9 +38,10 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef __cplusplus
-extern "C" {
-#endif 
+
+
+ABC_NAMESPACE_HEADER_START
+ 
 
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
@@ -105,6 +107,7 @@ struct Aig_Man_t_
     int              nTruePis;       // the number of true primary inputs
     int              nTruePos;       // the number of true primary outputs
     int              nAsserts;       // the number of asserts among POs (asserts are first POs)
+    int              nConstrs;       // the number of constraints (model checking only)
     // AIG node counters
     int              nObjs[AIG_OBJ_VOID];// the number of objects by type
     int              nCreated;       // the number of created objects
@@ -148,7 +151,8 @@ struct Aig_Man_t_
     Vec_Ptr_t *      vMapped;
     Vec_Int_t *      vFlopNums;      
     Vec_Int_t *      vFlopReprs;      
-    void *           pSeqModel;
+    Abc_Cex_t *      pSeqModel;
+    Vec_Ptr_t *      pSeqModelVec;   // vector of counter-examples (for sequential miters)
     Aig_Man_t *      pManExdc;
     Vec_Ptr_t *      vOnehots;
     Aig_Man_t *      pManHaig;
@@ -217,10 +221,12 @@ static inline Aig_Cut_t *  Aig_CutNext( Aig_Cut_t * pCut )              { return
 ////////////////////////////////////////////////////////////////////////
 
 static inline int          Aig_IntAbs( int n )                    { return (n < 0)? -n : n;                                }
-static inline int          Aig_Float2Int( float Val )             { return *((int *)&Val);                                 }
-static inline float        Aig_Int2Float( int Num )               { return *((float *)&Num);                               }
-static inline int          Aig_Base2Log( unsigned n )             { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
-static inline int          Aig_Base10Log( unsigned n )            { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
+//static inline int          Aig_Float2Int( float Val )             { return *((int *)&Val);                                 }
+//static inline float        Aig_Int2Float( int Num )               { return *((float *)&Num);                               }
+static inline int          Aig_Float2Int( float Val )             { union { int x; float y; } v; v.y = Val; return v.x;    }
+static inline float        Aig_Int2Float( int Num )               { union { int x; float y; } v; v.x = Num; return v.y;    }
+static inline int          Aig_Base2Log( unsigned n )             { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
+static inline int          Aig_Base10Log( unsigned n )            { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
 static inline char *       Aig_UtilStrsav( char * s )             { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL; }
 static inline int          Aig_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);                  }
 static inline int          Aig_TruthWordNum( int nVars )          { return nVars <= 5 ? 1 : (1 << (nVars - 5));            }
@@ -261,6 +267,7 @@ static inline int          Aig_ManGetCost( Aig_Man_t * p )        { return p->nO
 static inline int          Aig_ManObjNum( Aig_Man_t * p )         { return p->nCreated - p->nDeleted;                }
 static inline int          Aig_ManObjNumMax( Aig_Man_t * p )      { return Vec_PtrSize(p->vObjs);                    }
 static inline int          Aig_ManRegNum( Aig_Man_t * p )         { return p->nRegs;                                 }
+static inline int          Aig_ManConstrNum( Aig_Man_t * p )      { return p->nConstrs;                              }
 
 static inline Aig_Obj_t *  Aig_ManConst0( Aig_Man_t * p )         { return Aig_Not(p->pConst1);                      }
 static inline Aig_Obj_t *  Aig_ManConst1( Aig_Man_t * p )         { return p->pConst1;                               }
@@ -284,6 +291,7 @@ static inline int          Aig_ObjIsNode( Aig_Obj_t * pObj )      { return pObj-
 static inline int          Aig_ObjIsTerm( Aig_Obj_t * pObj )      { return pObj->Type == AIG_OBJ_PI  || pObj->Type == AIG_OBJ_PO || pObj->Type == AIG_OBJ_CONST1;   }
 static inline int          Aig_ObjIsHash( Aig_Obj_t * pObj )      { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR;                                 }
 static inline int          Aig_ObjIsChoice( Aig_Man_t * p, Aig_Obj_t * pObj )    { return p->pEquivs && p->pEquivs[pObj->Id] && pObj->nRefs > 0;                    }
+static inline int          Aig_ObjIsCand( Aig_Obj_t * pObj )      { return pObj->Type == AIG_OBJ_PI || pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR;     }
 
 static inline int          Aig_ObjIsMarkA( Aig_Obj_t * pObj )     { return pObj->fMarkA;  }
 static inline void         Aig_ObjSetMarkA( Aig_Obj_t * pObj )    { pObj->fMarkA = 1;     }
@@ -315,6 +323,9 @@ static inline Aig_Obj_t *  Aig_ObjChild0Next( Aig_Obj_t * pObj )  { assert( !Aig
 static inline Aig_Obj_t *  Aig_ObjChild1Next( Aig_Obj_t * pObj )  { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pNext, Aig_ObjFaninC1(pObj)) : NULL;  }
 static inline void         Aig_ObjChild0Flip( Aig_Obj_t * pObj )  { assert( !Aig_IsComplement(pObj) ); pObj->pFanin0 = Aig_Not(pObj->pFanin0);        }
 static inline void         Aig_ObjChild1Flip( Aig_Obj_t * pObj )  { assert( !Aig_IsComplement(pObj) ); pObj->pFanin1 = Aig_Not(pObj->pFanin1);        }
+static inline Aig_Obj_t *  Aig_ObjCopy( Aig_Obj_t * pObj )        { assert( !Aig_IsComplement(pObj) ); return (Aig_Obj_t *)pObj->pData;               } 
+static inline void         Aig_ObjSetCopy( Aig_Obj_t * pObj, Aig_Obj_t * pCopy )     {  assert( !Aig_IsComplement(pObj) ); pObj->pData = pCopy;       } 
+static inline Aig_Obj_t *  Aig_ObjRealCopy( Aig_Obj_t * pObj )    { return Aig_NotCond((Aig_Obj_t *)Aig_Regular(pObj)->pData, Aig_IsComplement(pObj));}
 static inline int          Aig_ObjLevel( Aig_Obj_t * pObj )       { assert( !Aig_IsComplement(pObj) ); return pObj->Level;                            }
 static inline int          Aig_ObjLevelNew( Aig_Obj_t * pObj )    { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + ABC_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
 static inline int          Aig_ObjSetLevel( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level = i;                    }
@@ -388,22 +399,22 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
 
 // iterator over the primary inputs
 #define Aig_ManForEachPi( p, pObj, i )                                          \
-    Vec_PtrForEachEntry( p->vPis, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vPis, pObj, i )
 // iterator over the primary outputs
 #define Aig_ManForEachPo( p, pObj, i )                                          \
-    Vec_PtrForEachEntry( p->vPos, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vPos, pObj, i )
 // iterator over the assertions
 #define Aig_ManForEachAssert( p, pObj, i )                                      \
-    Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-p->nAsserts )
+    Vec_PtrForEachEntryStart( Aig_Obj_t *, p->vPos, pObj, i, Aig_ManPoNum(p)-p->nAsserts )
 // iterator over all objects, including those currently not used
 #define Aig_ManForEachObj( p, pObj, i )                                         \
-    Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
 // iterator over all nodes
 #define Aig_ManForEachNode( p, pObj, i )                                        \
-    Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
 // iterator over all nodes
 #define Aig_ManForEachExor( p, pObj, i )                                        \
-    Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsExor(pObj) ) {} else
 // iterator over the nodes whose IDs are stored in the array
 #define Aig_ManForEachNodeVec( p, vIds, pObj, i )                               \
     for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
@@ -429,16 +440,16 @@ static inline int     Aig_ObjFanoutNext( Aig_Man_t * p, int iFan )   { assert(iF
 
 // iterator over the primary inputs
 #define Aig_ManForEachPiSeq( p, pObj, i )                                       \
-    Vec_PtrForEachEntryStop( p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManRegNum(p) )
+    Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManRegNum(p) )
 // iterator over the latch outputs
 #define Aig_ManForEachLoSeq( p, pObj, i )                                       \
-    Vec_PtrForEachEntryStart( p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManRegNum(p) )
+    Vec_PtrForEachEntryStart( Aig_Obj_t *, p->vPis, pObj, i, Aig_ManPiNum(p)-Aig_ManRegNum(p) )
 // iterator over the primary outputs
 #define Aig_ManForEachPoSeq( p, pObj, i )                                       \
-    Vec_PtrForEachEntryStop( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManRegNum(p) )
+    Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManRegNum(p) )
 // iterator over the latch inputs
 #define Aig_ManForEachLiSeq( p, pObj, i )                                       \
-    Vec_PtrForEachEntryStart( p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManRegNum(p) )
+    Vec_PtrForEachEntryStart( Aig_Obj_t *, p->vPos, pObj, i, Aig_ManPoNum(p)-Aig_ManRegNum(p) )
 // iterator over the latch input and outputs
 #define Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, k )                           \
     for ( k = 0; (k < Aig_ManRegNum(p)) && (((pObjLi) = Aig_ManLi(p, k)), 1)    \
@@ -475,10 +486,13 @@ extern Aig_Obj_t *     Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t
 extern void            Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes );
 extern int             Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper );
 /*=== aigDup.c ==========================================================*/
+extern Aig_Obj_t *     Aig_ManDupSimpleDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj );
 extern Aig_Man_t *     Aig_ManDupSimple( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManDupSimpleWithHints( Aig_Man_t * p, Vec_Int_t * vHints );
 extern Aig_Man_t *     Aig_ManDupSimpleDfs( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupSimpleDfsPart( Aig_Man_t * p, Vec_Ptr_t * vPis, Vec_Ptr_t * vPos );
 extern Aig_Man_t *     Aig_ManDupOrdered( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value );
 extern Aig_Man_t *     Aig_ManDupTrim( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupExor( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupDfs( Aig_Man_t * p );
@@ -503,7 +517,8 @@ extern Aig_Man_t *     Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int
 extern Aig_Man_t *     Aig_ManStart( int nNodesMax );
 extern Aig_Man_t *     Aig_ManStartFrom( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
-extern ABC_DLL void    Aig_ManStop( Aig_Man_t * p );
+extern void            Aig_ManStop( Aig_Man_t * p );
+extern void            Aig_ManStopP( Aig_Man_t ** p );
 extern int             Aig_ManCleanup( Aig_Man_t * p );
 extern int             Aig_ManAntiCleanup( Aig_Man_t * p );
 extern int             Aig_ManPiCleanup( Aig_Man_t * p );
@@ -512,6 +527,7 @@ extern void            Aig_ManPrintStats( Aig_Man_t * p );
 extern void            Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew );
 extern void            Aig_ManSetRegNum( Aig_Man_t * p, int nRegs );
 extern void            Aig_ManFlipFirstPo( Aig_Man_t * p );
+extern void *          Aig_ManReleaseData( Aig_Man_t * p );
 /*=== aigMem.c ==========================================================*/
 extern void            Aig_ManStartMemory( Aig_Man_t * p );
 extern void            Aig_ManStopMemory( Aig_Man_t * p );
@@ -620,6 +636,7 @@ extern Aig_Man_t *     Aig_ManConstReduce( Aig_Man_t * p, int fVerbose );
 /*=== aigUtil.c =========================================================*/
 extern unsigned        Aig_PrimeCudd( unsigned p );
 extern void            Aig_ManIncrementTravId( Aig_Man_t * p );
+extern char *          Aig_TimeStamp();
 extern int             Aig_ManHasNoGaps( Aig_Man_t * p );
 extern int             Aig_ManLevels( Aig_Man_t * p );
 extern void            Aig_ManResetRefs( Aig_Man_t * p );
@@ -650,6 +667,10 @@ extern unsigned        Aig_ManRandom( int fReset );
 extern void            Aig_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop );
 extern void            Aig_NodeUnionLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr );
 extern void            Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * vArr );
+extern void            Aig_ManSetPhase( Aig_Man_t * pAig );
+extern Vec_Ptr_t *     Aig_ManMuxesCollect( Aig_Man_t * pAig );
+extern void            Aig_ManMuxesDeref( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes );
+extern void            Aig_ManMuxesRef( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes );
 
 /*=== aigWin.c =========================================================*/
 extern void            Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
@@ -676,9 +697,11 @@ extern char *          Aig_MmStepEntryFetch( Aig_MmStep_t * p, int nBytes );
 extern void            Aig_MmStepEntryRecycle( Aig_MmStep_t * p, char * pEntry, int nBytes );
 extern int             Aig_MmStepReadMemUsage( Aig_MmStep_t * p );
 
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
 
 #endif
 
diff --git a/src/aig/aig/aigCanon.c b/src/aig/aig/aigCanon.c
index 4f241842..706a9c61 100644
--- a/src/aig/aig/aigCanon.c
+++ b/src/aig/aig/aigCanon.c
@@ -21,6 +21,10 @@
 #include "aig.h"
 #include "kit.h"
 #include "bdc.h"
+#include "ioa.h"
+
+ABC_NAMESPACE_IMPL_START
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -277,7 +281,7 @@ void Aig_RManStop( Aig_RMan_t * p )
 ***********************************************************************/
 void Aig_RManQuit()
 {
-    extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
+//    extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
     char Buffer[20];
     if ( s_pRMan == NULL )
         return;
@@ -537,7 +541,7 @@ unsigned Aig_RManSemiCanonicize( unsigned * pOut, unsigned * pIn, int nVars, cha
 
 ***********************************************************************/
 static inline Aig_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj )  
-{ return Aig_NotCond( Bdc_FuncCopy(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) );  }
+{ return Aig_NotCond( (Aig_Obj_t *)Bdc_FuncCopy(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) );  }
 
 /**Function*************************************************************
 
@@ -692,3 +696,5 @@ Extra_PrintBinary( stdout, s_pRMan->pTruth, 1<<nVars ); printf( "\n\n" );
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigCheck.c b/src/aig/aig/aigCheck.c
index 4cfdaaf1..298c5595 100644
--- a/src/aig/aig/aigCheck.c
+++ b/src/aig/aig/aigCheck.c
@@ -20,6 +20,9 @@
  
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -161,3 +164,5 @@ void Aig_ManCheckPhase( Aig_Man_t * p )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigCuts.c b/src/aig/aig/aigCuts.c
index dc677269..6de19484 100644
--- a/src/aig/aig/aigCuts.c
+++ b/src/aig/aig/aigCuts.c
@@ -21,6 +21,9 @@
 #include "aig.h"
 #include "kit.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -207,7 +210,7 @@ static inline float Aig_CutFindCost2( Aig_ManCut_t * p, Aig_Cut_t * pCut )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the next ABC_FREE cut to use.]
+  Synopsis    [Returns the next free cut to use.]
 
   Description []
                
@@ -667,3 +670,5 @@ Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, in
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index dfc35c83..6b30611a 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -21,6 +21,9 @@
 #include "aig.h"
 #include "tim.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -76,15 +79,15 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p )
         {
             if ( p->pManTime )
             {
-                iBox = Tim_ManBoxForCi( p->pManTime, Aig_ObjPioNum(pObj) );
+                iBox = Tim_ManBoxForCi( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pObj) );
                 if ( iBox >= 0 ) // this is not a true PI
                 {
-                    iTerm1 = Tim_ManBoxInputFirst( p->pManTime, iBox );
-                    nTerms = Tim_ManBoxInputNum( p->pManTime, iBox );
+                    iTerm1 = Tim_ManBoxInputFirst( (Tim_Man_t *)p->pManTime, iBox );
+                    nTerms = Tim_ManBoxInputNum( (Tim_Man_t *)p->pManTime, iBox );
                     for ( k = 0; k < nTerms; k++ )
                     {
                         pNext = Aig_ManPo( p, iTerm1 + k );
-                        assert( Tim_ManBoxForCo( p->pManTime, Aig_ObjPioNum(pNext) ) == iBox ); 
+                        assert( Tim_ManBoxForCo( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pNext) ) == iBox ); 
                         if ( !Aig_ObjIsTravIdCurrent(p,pNext) )
                         {
                             printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id );
@@ -276,7 +279,10 @@ Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
     // go through the nodes
     vNodes = Vec_PtrAlloc( Aig_ManNodeNum(p) );
     for ( i = 0; i < nNodes; i++ )
-        Aig_ManDfs_rec( p, ppNodes[i], vNodes );
+        if ( Aig_ObjIsPo(ppNodes[i]) )
+            Aig_ManDfs_rec( p, Aig_ObjFanin0(ppNodes[i]), vNodes );
+        else
+            Aig_ManDfs_rec( p, ppNodes[i], vNodes );
     return vNodes;
 }
 
@@ -435,11 +441,11 @@ void Aig_ManChoiceLevel_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
     {
         if ( p->pManTime )
         {
-            iBox = Tim_ManBoxForCi( p->pManTime, Aig_ObjPioNum(pObj) );
+            iBox = Tim_ManBoxForCi( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pObj) );
             if ( iBox >= 0 ) // this is not a true PI
             {
-                iTerm1 = Tim_ManBoxInputFirst( p->pManTime, iBox );
-                nTerms = Tim_ManBoxInputNum( p->pManTime, iBox );
+                iTerm1 = Tim_ManBoxInputFirst( (Tim_Man_t *)p->pManTime, iBox );
+                nTerms = Tim_ManBoxInputNum( (Tim_Man_t *)p->pManTime, iBox );
                 for ( i = 0; i < nTerms; i++ )
                 {
                     pNext = Aig_ManPo(p, iTerm1 + i);
@@ -815,7 +821,7 @@ Aig_Obj_t * Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pRoo
     Aig_Transfer_rec( pDest, Aig_Regular(pRoot) );
     // clear the markings
     Aig_ConeUnmark_rec( Aig_Regular(pRoot) );
-    return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
+    return Aig_NotCond( (Aig_Obj_t *)Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
 }
 
 /**Function*************************************************************
@@ -869,7 +875,7 @@ Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, in
     Aig_Compose_rec( p, Aig_Regular(pRoot), pFunc, Aig_ManPi(p, iVar) );
     // clear the markings
     Aig_ConeUnmark_rec( Aig_Regular(pRoot) );
-    return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
+    return Aig_NotCond( (Aig_Obj_t *)Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
 }
 
 /**Function*************************************************************
@@ -914,7 +920,7 @@ void Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNod
     int i;
     // collect and mark the leaves
     Vec_PtrClear( vNodes );
-    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
     {
         assert( pObj->fMarkA == 0 );
         pObj->fMarkA = 1;
@@ -924,9 +930,9 @@ void Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNod
     // collect and mark the nodes
     Aig_ObjCollectCut_rec( pRoot, vNodes );
     // clean the nodes
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         pObj->fMarkA = 0;
-    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
         pObj->fMarkA = 0;
 }
 
@@ -998,7 +1004,7 @@ int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
     RetValue = Aig_ObjCollectSuper_rec( pObj, pObj, vSuper );
     assert( Vec_PtrSize(vSuper) > 1 );
     // unmark the visited nodes
-    Vec_PtrForEachEntry( vSuper, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
         Aig_Regular(pObj)->fMarkA = 0;
     // if we found the node and its complement in the same implication supergate, 
     // return empty set of nodes (meaning that we should use constant-0 node)
@@ -1012,3 +1018,5 @@ int Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index 90579f59..91531093 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -21,6 +21,9 @@
 #include "saig.h"
 #include "tim.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -52,6 +55,7 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
+    pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
@@ -102,6 +106,57 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Derives AIG with hints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupSimpleWithHints( Aig_Man_t * p, Vec_Int_t * vHints )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i, Entry;
+    assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
+    assert( p->nAsserts == 0 || p->nConstrs == 0 );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        pObj->pData = Aig_ObjCreatePi( pNew );
+        Entry = Vec_IntEntry( vHints, Aig_ObjId(pObj) );
+        if ( Entry == 0 || Entry == 1 )
+            pObj->pData = Aig_NotCond( Aig_ManConst1(pNew), Entry ); // restrict to the complement of constraint!!!
+    }
+    // duplicate internal nodes
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        Entry = Vec_IntEntry( vHints, Aig_ObjId(pObj) );
+        if ( Entry == 0 || Entry == 1 )
+            pObj->pData = Aig_NotCond( Aig_ManConst1(pNew), Entry ); // restrict to the complement of constraint!!!
+    }
+    // add the POs
+    Aig_ManForEachPo( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    Aig_ManCleanup( pNew );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Llb_ManDeriveAigWithHints(): The check has failed.\n" );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates the AIG manager recursively.]
 
   Description []
@@ -114,14 +169,14 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
 Aig_Obj_t * Aig_ManDupSimpleDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
 {
     if ( pObj->pData )
-        return pObj->pData;
+        return (Aig_Obj_t *)pObj->pData;
     Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );
     if ( Aig_ObjIsBuf(pObj) )
-        return pObj->pData = Aig_ObjChild0Copy(pObj);
+        return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
     Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin1(pObj) );
     pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    Aig_Regular(pObj->pData)->pHaig = pObj->pHaig;
-    return pObj->pData;
+    Aig_Regular((Aig_Obj_t *)pObj->pData)->pHaig = pObj->pHaig;
+    return (Aig_Obj_t *)pObj->pData;
 }
 
 /**Function*************************************************************
@@ -151,6 +206,7 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
+    pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
@@ -213,10 +269,10 @@ Aig_Man_t * Aig_ManDupSimpleDfsPart( Aig_Man_t * p, Vec_Ptr_t * vPis, Vec_Ptr_t
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1( pNew );
-    Vec_PtrForEachEntry( vPis, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vPis, pObj, i )
         pObj->pData = Aig_ObjCreatePi( pNew );
     // duplicate internal nodes
-    Vec_PtrForEachEntry( vPos, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vPos, pObj, i )
     {
         pObjNew = Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );        
         pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
@@ -250,6 +306,7 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
+    pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
@@ -289,7 +346,7 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
     Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // duplicate the timing manager
     if ( p->pManTime )
-        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+        pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
     // pass the HAIG manager
     if ( p->pManHaig != NULL )
     {
@@ -301,6 +358,86 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
         printf( "Aig_ManDupOrdered(): The check has failed.\n" );
     return pNew;
 }
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description [Orders nodes as follows: PIs, ANDs, POs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i;
+    assert( p->pManTime == NULL );
+    assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nAsserts = p->nAsserts;
+    pNew->nConstrs = p->nConstrs;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        if ( i == iInput )
+            pObjNew = Value ? Aig_ManConst1(pNew) : Aig_ManConst0(pNew);
+        else
+        {
+            pObjNew = Aig_ObjCreatePi( pNew );
+            pObjNew->pHaig = pObj->pHaig;
+            pObjNew->Level = pObj->Level;
+        }
+        pObj->pData = pObjNew;
+    }
+    // duplicate internal nodes
+    Aig_ManForEachObj( p, pObj, i )
+        if ( Aig_ObjIsBuf(pObj) )
+        {
+            pObjNew = Aig_ObjChild0Copy(pObj);
+            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
+        }
+        else if ( Aig_ObjIsNode(pObj) )
+        {
+            pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+            pObj->pData = pObjNew;
+        }
+    // add the POs
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        pObjNew->pHaig = pObj->pHaig;
+        pObj->pData = pObjNew;
+    }
+//    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+    Aig_ManCleanup( pNew );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+    // pass the HAIG manager
+    if ( p->pManHaig != NULL )
+    {
+        pNew->pManHaig = p->pManHaig;  
+        p->pManHaig = NULL;
+    }
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDupSimple(): The check has failed.\n" );
+    return pNew;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Duplicates the AIG manager.]
@@ -321,6 +458,7 @@ Aig_Man_t * Aig_ManDupTrim( Aig_Man_t * p )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nConstrs = p->nConstrs;
     // create the PIs
     Aig_ManCleanData( p );
     // duplicate internal nodes
@@ -370,6 +508,7 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
+    pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // create the PIs
@@ -407,7 +546,7 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
     Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // duplicate the timing manager
     if ( p->pManTime )
-        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+        pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDupExor(): The check has failed.\n" );
@@ -429,12 +568,12 @@ Aig_Obj_t * Aig_ManDupDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
 {
     Aig_Obj_t * pObjNew, * pEquivNew = NULL;
     if ( pObj->pData )
-        return pObj->pData;
+        return (Aig_Obj_t *)pObj->pData;
     if ( p->pEquivs && Aig_ObjEquiv(p, pObj) )
         pEquivNew = Aig_ManDupDfs_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
     Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );
     if ( Aig_ObjIsBuf(pObj) )
-        return pObj->pData = Aig_ObjChild0Copy(pObj);
+        return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
     Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin1(pObj) );
     pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
     if ( p->pManHaig != NULL )
@@ -448,7 +587,7 @@ Aig_Obj_t * Aig_ManDupDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
         if ( pNew->pReprs )
             pNew->pReprs[Aig_Regular(pEquivNew)->Id] = Aig_Regular(pObjNew);
     }
-    return pObj->pData = pObjNew;
+    return (Aig_Obj_t *)(pObj->pData = pObjNew);
 }
 
 /**Function*************************************************************
@@ -472,6 +611,7 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
+    pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // duplicate representation of choice nodes
@@ -508,7 +648,7 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
     Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // duplicate the timing manager
     if ( p->pManTime )
-        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+        pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
     // pass the HAIG manager
     if ( p->pManHaig != NULL )
     {
@@ -567,7 +707,7 @@ Aig_Obj_t * Aig_ManDupDfsGuided_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t
 {
     Aig_Obj_t * pObjNew, * pEquivNew = NULL;
     if ( pObj->pData )
-        return pObj->pData;
+        return (Aig_Obj_t *)pObj->pData;
     if ( Aig_ObjIsPi(pObj) )
         return NULL;
     if ( p->pEquivs && Aig_ObjEquiv(p, pObj) )
@@ -575,7 +715,7 @@ Aig_Obj_t * Aig_ManDupDfsGuided_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t
     if ( !Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin0(pObj) ) )
         return NULL;
     if ( Aig_ObjIsBuf(pObj) )
-        return pObj->pData = Aig_ObjChild0Copy(pObj);
+        return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
     if ( !Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin1(pObj) ) )
         return NULL;
     pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
@@ -588,7 +728,7 @@ Aig_Obj_t * Aig_ManDupDfsGuided_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t
         if ( pNew->pReprs )
             pNew->pReprs[Aig_Regular(pEquivNew)->Id] = Aig_Regular(pObjNew);
     }
-    return pObj->pData = pObjNew;
+    return (Aig_Obj_t *)(pObj->pData = pObjNew);
 }
 
 /**Function*************************************************************
@@ -612,6 +752,7 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
+    pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // duplicate representation of choice nodes
@@ -630,7 +771,7 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
     // duplicate internal nodes
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
     Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
-    Vec_PtrForEachEntry( vPios, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vPios, pObj, i )
     {
         if ( Aig_ObjIsPi(pObj) )
         {
@@ -654,7 +795,7 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
     Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // duplicate the timing manager
     if ( p->pManTime )
-        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+        pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDupDfs(): The check has failed.\n" );
@@ -683,6 +824,7 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
+    pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // duplicate representation of choice nodes
@@ -708,7 +850,7 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
     }
     // duplicate internal nodes
     vLevels = Aig_ManLevelize( p );
-    Vec_VecForEachEntry( vLevels, pObj, i, k )
+    Vec_VecForEachEntry( Aig_Obj_t *, vLevels, pObj, i, k )
     {
         pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
         Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
@@ -728,7 +870,7 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
     Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
     // duplicate the timing manager
     if ( p->pManTime )
-        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+        pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDupLevelized(): The check has failed.\n" );
@@ -787,8 +929,8 @@ static inline Aig_Obj_t * Aig_ObjGetRepres( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t * pRepr;
     if ( (pRepr = Aig_ObjRepr(p, pObj)) )
-        return Aig_NotCond( pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
-    return pObj->pData;
+        return Aig_NotCond( (Aig_Obj_t *)pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
+    return (Aig_Obj_t *)pObj->pData;
 }
 static inline Aig_Obj_t * Aig_ObjChild0Repres( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjGetRepres(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) ); }
 static inline Aig_Obj_t * Aig_ObjChild1Repres( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjGetRepres(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) ); }
@@ -813,6 +955,7 @@ Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // map the const and primary inputs
@@ -855,15 +998,15 @@ Aig_Obj_t * Aig_ManDupRepres_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * p
 {
     Aig_Obj_t * pRepr;
     if ( pObj->pData )
-        return pObj->pData;
+        return (Aig_Obj_t *)pObj->pData;
     if ( (pRepr = Aig_ObjRepr(p, pObj)) )
     {
         Aig_ManDupRepres_rec( pNew, p, pRepr );
-        return pObj->pData = Aig_NotCond( pRepr->pData, pRepr->fPhase ^ pObj->fPhase );
+        return (Aig_Obj_t *)(pObj->pData = Aig_NotCond( (Aig_Obj_t *)pRepr->pData, pRepr->fPhase ^ pObj->fPhase ));
     }
     Aig_ManDupRepres_rec( pNew, p, Aig_ObjFanin0(pObj) );
     Aig_ManDupRepres_rec( pNew, p, Aig_ObjFanin1(pObj) );
-    return pObj->pData = Aig_And( pNew, Aig_ObjChild0Repres(p, pObj), Aig_ObjChild1Repres(p, pObj) );
+    return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Repres(p, pObj), Aig_ObjChild1Repres(p, pObj) ));
 }
 
 /**Function*************************************************************
@@ -886,6 +1029,7 @@ Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // map the const and primary inputs
@@ -985,6 +1129,11 @@ Aig_Man_t * Aig_ManDupOrpos( Aig_Man_t * p, int fAddRegs )
     Aig_Obj_t * pObj, * pMiter;
     int i;
     assert( Aig_ManRegNum(p) > 0 );
+    if ( p->nConstrs > 0 )
+    {
+        printf( "The AIG manager should have no constraints.\n" );
+        return NULL;
+    }
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
@@ -1080,6 +1229,11 @@ Aig_Man_t * Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs )
     Aig_Obj_t * pObj;
     int i, nOuts = 0;
     assert( Aig_ManRegNum(p) > 0 );
+    if ( p->nConstrs > 0 )
+    {
+        printf( "The AIG manager should have no constraints.\n" );
+        return NULL;
+    }
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
@@ -1120,3 +1274,5 @@ Aig_Man_t * Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigFact.c b/src/aig/aig/aigFact.c
index 7004618a..9c4e5689 100644
--- a/src/aig/aig/aigFact.c
+++ b/src/aig/aig/aigFact.c
@@ -19,6 +19,10 @@
 ***********************************************************************/
 
 #include "aig.h"
+#include "kit.h"
+
+ABC_NAMESPACE_IMPL_START
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -116,7 +120,7 @@ int Aig_ManFindConeOverlap( Aig_Man_t * p, Vec_Ptr_t * vImplics, Aig_Obj_t * pNo
     assert( !Aig_IsComplement(pNode) );
     assert( !Aig_ObjIsConst1(pNode) );
     Aig_ManIncrementTravId( p );
-    Vec_PtrForEachEntry( vImplics, pTemp, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vImplics, pTemp, i )
         Aig_ObjSetTravIdCurrent( p, Aig_Regular(pTemp) );
     Aig_ManIncrementTravId( p );
     return Aig_ManFindConeOverlap_rec( p, pNode );
@@ -136,13 +140,13 @@ int Aig_ManFindConeOverlap( Aig_Man_t * p, Vec_Ptr_t * vImplics, Aig_Obj_t * pNo
 Aig_Obj_t * Aig_ManDeriveNewCone_rec( Aig_Man_t * p, Aig_Obj_t * pNode )
 {
     if ( Aig_ObjIsTravIdCurrent( p, pNode ) )
-        return pNode->pData;
+        return (Aig_Obj_t *)pNode->pData;
     Aig_ObjSetTravIdCurrent( p, pNode );
     if ( Aig_ObjIsPi(pNode) )
-        return pNode->pData = pNode;
+        return (Aig_Obj_t *)(pNode->pData = pNode);
     Aig_ManDeriveNewCone_rec( p, Aig_ObjFanin0(pNode) );
     Aig_ManDeriveNewCone_rec( p, Aig_ObjFanin1(pNode) );
-    return pNode->pData = Aig_And( p, Aig_ObjChild0Copy(pNode), Aig_ObjChild1Copy(pNode) );
+    return (Aig_Obj_t *)(pNode->pData = Aig_And( p, Aig_ObjChild0Copy(pNode), Aig_ObjChild1Copy(pNode) ));
 }
 
 /**Function*************************************************************
@@ -163,7 +167,7 @@ Aig_Obj_t * Aig_ManDeriveNewCone( Aig_Man_t * p, Vec_Ptr_t * vImplics, Aig_Obj_t
     assert( !Aig_IsComplement(pNode) );
     assert( !Aig_ObjIsConst1(pNode) );
     Aig_ManIncrementTravId( p );
-    Vec_PtrForEachEntry( vImplics, pTemp, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vImplics, pTemp, i )
     {
         Aig_ObjSetTravIdCurrent( p, Aig_Regular(pTemp) );
         Aig_Regular(pTemp)->pData = Aig_NotCond( Aig_ManConst1(p), Aig_IsComplement(pTemp) );
@@ -267,6 +271,446 @@ void Aig_ManFactorAlgebraicTest( Aig_Man_t * p )
 */
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Determines what support variables can be cofactored.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_SuppMinPerform( Aig_Man_t * p, Vec_Ptr_t * vOrGate, Vec_Ptr_t * vNodes, Vec_Ptr_t * vSupp )
+{
+    Aig_Obj_t * pObj;
+    Vec_Ptr_t * vTrSupp, * vTrNode, * vCofs;
+    unsigned * uFunc, * uCare, * uFunc0, * uFunc1, * uCof;
+    int i, nWords = Aig_TruthWordNum( Vec_PtrSize(vSupp) );
+    // assign support nodes
+    vTrSupp = Vec_PtrAllocTruthTables( Vec_PtrSize(vSupp) );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSupp, pObj, i )
+    {
+        printf( "%d %d\n", Aig_ObjId(pObj), i );
+        pObj->pData = Vec_PtrEntry( vTrSupp, i );
+    }
+    // compute internal nodes
+    vTrNode = Vec_PtrAllocSimInfo( Vec_PtrSize(vNodes) + 5, nWords );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+    {
+        pObj->pData = uFunc = (unsigned *)Vec_PtrEntry( vTrNode, i );
+        uFunc0 = (unsigned *)Aig_ObjFanin0(pObj)->pData;
+        uFunc1 = (unsigned *)Aig_ObjFanin1(pObj)->pData;
+        Kit_TruthAndPhase( uFunc, uFunc0, uFunc1, Vec_PtrSize(vSupp), Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
+    }
+    // uFunc contains the result of computation
+    // compute care set
+    uCare = (unsigned *)Vec_PtrEntry( vTrNode, Vec_PtrSize(vNodes) );
+    Kit_TruthClear( uCare, Vec_PtrSize(vSupp) );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vOrGate, pObj, i )
+    {
+        printf( "%d %d %d - or gate\n", Aig_ObjId(Aig_Regular(pObj)), Aig_IsComplement(pObj), i );
+        Kit_TruthOrPhase( uCare, uCare, (unsigned *)Aig_Regular(pObj)->pData, Vec_PtrSize(vSupp), 0, Aig_IsComplement(pObj) );
+    }
+    // try cofactoring each variable in both polarities
+    vCofs = Vec_PtrAlloc( 10 );
+    uCof  = (unsigned *)Vec_PtrEntry( vTrNode, Vec_PtrSize(vNodes)+1 );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSupp, pObj, i )
+    {
+        // consider negative cofactor
+        Kit_TruthCofactor0New( uCof, uFunc, Vec_PtrSize(vSupp), i );
+        if ( Kit_TruthIsEqualWithCare( uFunc, uCof, uCare, Vec_PtrSize(vSupp) ) )
+        {
+            Vec_PtrPush( vCofs, Aig_Not(pObj) );
+            Kit_TruthCopy( uFunc, uCof, Vec_PtrSize(vSupp) );
+            Kit_TruthCofactor0( uCare, Vec_PtrSize(vSupp), i );
+            continue;
+        }
+        // consider positive cofactor
+        Kit_TruthCofactor1New( uCof, uFunc, Vec_PtrSize(vSupp), i );
+        if ( Kit_TruthIsEqualWithCare( uFunc, uCof, uCare, Vec_PtrSize(vSupp) ) )
+        {
+            Vec_PtrPush( vCofs, pObj );
+            Kit_TruthCopy( uFunc, uCof, Vec_PtrSize(vSupp) );
+            Kit_TruthCofactor1( uCare, Vec_PtrSize(vSupp), i );
+        }
+    }
+    Vec_PtrFree( vTrNode );
+    Vec_PtrFree( vTrSupp );
+    return vCofs;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the new node after cofactoring.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_SuppMinReconstruct( Aig_Man_t * p, Vec_Ptr_t * vCofs, Vec_Ptr_t * vNodes, Vec_Ptr_t * vSupp )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    // set the value of the support variables
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSupp, pObj, i )
+        assert( !Aig_IsComplement(pObj) );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSupp, pObj, i )
+        pObj->pData = pObj;
+    // set the value of the cofactoring variables
+    Vec_PtrForEachEntry( Aig_Obj_t *, vCofs, pObj, i )
+        Aig_Regular(pObj)->pData = Aig_NotCond( Aig_ManConst1(p), Aig_IsComplement(pObj) );
+    // reconstruct the node
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+        pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    return (Aig_Obj_t *)pObj->pData;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if all nodes of vOrGate are in vSupp.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_SuppMinGateIsInSupport( Aig_Man_t * p, Vec_Ptr_t * vOrGate, Vec_Ptr_t * vSupp )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManIncrementTravId( p );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSupp, pObj, i )
+        Aig_ObjSetTravIdCurrent( p, pObj );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vOrGate, pObj, i )
+        if ( !Aig_ObjIsTravIdCurrent( p, Aig_Regular(pObj) ) )
+            return 0;
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects fanins of the marked nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_SuppMinCollectSupport( Aig_Man_t * p, Vec_Ptr_t * vNodes )
+{
+    Vec_Ptr_t * vSupp;
+    Aig_Obj_t * pObj, * pFanin;
+    int i;
+    vSupp = Vec_PtrAlloc( 4 );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+    {
+        assert( Aig_ObjIsTravIdCurrent(p, pObj) );
+        assert( Aig_ObjIsNode(pObj) );
+        pFanin = Aig_ObjFanin0( pObj );
+        if ( !Aig_ObjIsTravIdCurrent(p, pFanin) )
+        {
+            Aig_ObjSetTravIdCurrent( p, pFanin );
+            Vec_PtrPush( vSupp, pFanin );
+        }
+        pFanin = Aig_ObjFanin1( pObj );
+        if ( !Aig_ObjIsTravIdCurrent(p, pFanin) )
+        {
+            Aig_ObjSetTravIdCurrent( p, pFanin );
+            Vec_PtrPush( vSupp, pFanin );
+        }
+    }
+    return vSupp;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the nodes in the cone with current trav ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_SuppMinCollectCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    if ( Aig_ObjIsTravIdCurrent( p, pObj ) ) // visited
+        return;
+    if ( !Aig_ObjIsTravIdPrevious( p, pObj ) ) // not visited, but outside
+        return;
+    assert( Aig_ObjIsTravIdPrevious(p, pObj) ); // not visited, inside
+    assert( Aig_ObjIsNode(pObj) );
+    Aig_ObjSetTravIdCurrent( p, pObj );
+    Aig_SuppMinCollectCone_rec( p, Aig_ObjFanin0(pObj), vNodes );
+    Aig_SuppMinCollectCone_rec( p, Aig_ObjFanin1(pObj), vNodes );
+    Vec_PtrPush( vNodes, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects nodes with the current trav ID rooted in the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_SuppMinCollectCone( Aig_Man_t * p, Aig_Obj_t * pRoot )
+{
+    Vec_Ptr_t * vNodes;
+    assert( !Aig_IsComplement(pRoot) ); 
+//    assert( Aig_ObjIsTravIdCurrent( p, pRoot ) );
+    vNodes = Vec_PtrAlloc( 4 );
+    Aig_ManIncrementTravId( p );
+    Aig_SuppMinCollectCone_rec( p, Aig_Regular(pRoot), vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the nodes in the cone with current trav ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_SuppMinHighlightCone_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    int RetValue;
+    if ( Aig_ObjIsTravIdCurrent( p, pObj ) ) // visited, marks there
+        return 1;
+    if ( Aig_ObjIsTravIdPrevious( p, pObj ) ) // visited, no marks there
+        return 0;
+    Aig_ObjSetTravIdPrevious( p, pObj );
+    if ( Aig_ObjIsPi(pObj) )
+        return 0;
+    RetValue = Aig_SuppMinHighlightCone_rec( p, Aig_ObjFanin0(pObj) ) |
+               Aig_SuppMinHighlightCone_rec( p, Aig_ObjFanin1(pObj) );
+//    printf( "%d %d\n", Aig_ObjId(pObj), RetValue );
+    if ( RetValue )
+        Aig_ObjSetTravIdCurrent( p, pObj );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the nodes in the cone with current trav ID.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_SuppMinHighlightCone( Aig_Man_t * p, Aig_Obj_t * pRoot, Vec_Ptr_t * vOrGate )
+{
+    Aig_Obj_t * pLeaf;
+    int i, RetValue;
+    assert( !Aig_IsComplement(pRoot) );
+    Aig_ManIncrementTravId( p );
+    Aig_ManIncrementTravId( p );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vOrGate, pLeaf, i )
+        Aig_ObjSetTravIdCurrent( p, Aig_Regular(pLeaf) );
+    RetValue = Aig_SuppMinHighlightCone_rec( p, pRoot );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vOrGate, pLeaf, i )
+        Aig_ObjSetTravIdPrevious( p, Aig_Regular(pLeaf) );
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_SuppMinCollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
+{
+    // if the new node is complemented or a PI, another gate begins
+    if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) ) // || (Aig_ObjRefs(pObj) > 1) )
+    {
+        Vec_PtrPushUnique( vSuper, Aig_Not(pObj) );
+        return;
+    }
+    // go through the branches
+    Aig_SuppMinCollectSuper_rec( Aig_ObjChild0(pObj), vSuper );
+    Aig_SuppMinCollectSuper_rec( Aig_ObjChild1(pObj), vSuper );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_SuppMinCollectSuper( Aig_Obj_t * pObj )
+{
+    Vec_Ptr_t * vSuper;
+    assert( !Aig_IsComplement(pObj) );
+    assert( !Aig_ObjIsPi(pObj) );
+    vSuper = Vec_PtrAlloc( 4 );
+    Aig_SuppMinCollectSuper_rec( Aig_ObjChild0(pObj), vSuper );
+    Aig_SuppMinCollectSuper_rec( Aig_ObjChild1(pObj), vSuper );
+    return vSuper;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the result of support minimization.]
+
+  Description [Returns internal AIG node that is equal to pFunc under 
+  assignment pCond == 1, or NULL if there is no such node. status is 
+  -1 if condition is not OR; 
+  -2 if cone is too large or no cone; 
+  -3 if no support reduction is possible.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManSupportMinimization( Aig_Man_t * p, Aig_Obj_t * pCond, Aig_Obj_t * pFunc, int * pStatus )
+{
+    int nSuppMax = 16;
+    Vec_Ptr_t * vOrGate, * vNodes, * vSupp, * vCofs;
+    Aig_Obj_t * pResult;
+    int RetValue;
+    *pStatus = 0;
+    // if pCond is not OR
+    if ( !Aig_IsComplement(pCond) || Aig_ObjIsPi(Aig_Regular(pCond)) || Aig_ObjIsConst1(Aig_Regular(pCond)) )
+    {
+        *pStatus = -1;
+        return NULL;
+    }
+    // if pFunc is not a node
+    if ( !Aig_ObjIsNode(Aig_Regular(pFunc)) )
+    {
+        *pStatus = -2;
+        return NULL;
+    }
+    // collect the multi-input OR gate rooted in the condition
+    vOrGate = Aig_SuppMinCollectSuper( Aig_Regular(pCond) );
+    if ( Vec_PtrSize(vOrGate) > nSuppMax )
+    {
+        Vec_PtrFree( vOrGate );
+        *pStatus = -2;
+        return NULL;
+    }
+    // highlight the cone limited by these gates
+    RetValue = Aig_SuppMinHighlightCone( p, Aig_Regular(pFunc), vOrGate );
+    if ( RetValue == 0 ) // no overlap
+    {
+        Vec_PtrFree( vOrGate );
+        *pStatus = -2;
+        return NULL;
+    }
+    // collect the cone rooted in pFunc limited by vOrGate
+    vNodes = Aig_SuppMinCollectCone( p, Aig_Regular(pFunc) );
+    // collect the support nodes reachable from the cone
+    vSupp = Aig_SuppMinCollectSupport( p, vNodes );
+    if ( Vec_PtrSize(vSupp) > nSuppMax )
+    {
+        Vec_PtrFree( vOrGate );
+        Vec_PtrFree( vNodes );
+        Vec_PtrFree( vSupp );
+        *pStatus = -2;
+        return NULL;
+    }
+    // check if all nodes belonging to OR gate are included in the support
+    // (if this is not the case, don't-care minimization is not possible)
+    if ( !Aig_SuppMinGateIsInSupport( p, vOrGate, vSupp ) )
+    {
+        Vec_PtrFree( vOrGate );
+        Vec_PtrFree( vNodes );
+        Vec_PtrFree( vSupp );
+        *pStatus = -3;
+        return NULL;
+    }
+    // create truth tables of all nodes and find the maximal number
+    // of support varialbles that can be replaced by constants
+    vCofs = Aig_SuppMinPerform( p, vOrGate, vNodes, vSupp );
+    if ( Vec_PtrSize(vCofs) == 0 )
+    {
+        Vec_PtrFree( vCofs );
+        Vec_PtrFree( vOrGate );
+        Vec_PtrFree( vNodes );
+        Vec_PtrFree( vSupp );
+        *pStatus = -3;
+        return NULL;
+    }
+    // reconstruct the cone
+    pResult = Aig_SuppMinReconstruct( p, vCofs, vNodes, vSupp );
+    pResult = Aig_NotCond( pResult, Aig_IsComplement(pFunc) );
+    Vec_PtrFree( vCofs );
+    Vec_PtrFree( vOrGate );
+    Vec_PtrFree( vNodes );
+    Vec_PtrFree( vSupp );
+    return pResult;
+}
+/**Function*************************************************************
+
+  Synopsis    [Testing procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManSupportMinimizationTest()
+{
+    Aig_Man_t * p;
+    Aig_Obj_t * pFunc, * pCond, * pRes;
+    int i, Status;
+    p = Aig_ManStart( 100 );
+    for ( i = 0; i < 5; i++ )
+        Aig_IthVar(p,i);
+    pFunc = Aig_Mux( p, Aig_IthVar(p,3), Aig_IthVar(p,1), Aig_IthVar(p,0) );
+    pFunc = Aig_Mux( p, Aig_IthVar(p,4), Aig_IthVar(p,2), pFunc );
+    pCond = Aig_Or( p, Aig_IthVar(p,3), Aig_IthVar(p,4) );
+    pRes  = Aig_ManSupportMinimization( p, pCond, pFunc, &Status );
+    assert( Status == 0 );
+
+    Aig_ObjPrint( p, Aig_Regular(pRes) );                printf( "\n" );
+    Aig_ObjPrint( p, Aig_ObjFanin0(Aig_Regular(pRes)) ); printf( "\n" );
+    Aig_ObjPrint( p, Aig_ObjFanin1(Aig_Regular(pRes)) ); printf( "\n" );
+
+    Aig_ManStop( p );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigFanout.c b/src/aig/aig/aigFanout.c
index a3b1e684..d6317f43 100644
--- a/src/aig/aig/aigFanout.c
+++ b/src/aig/aig/aigFanout.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 // 0: first iFan
 // 1: prev iFan0
 // 2: prev iFan1
@@ -187,3 +190,5 @@ void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigFrames.c b/src/aig/aig/aigFrames.c
index f25f7a8f..fdcd14aa 100644
--- a/src/aig/aig/aigFrames.c
+++ b/src/aig/aig/aigFrames.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -133,3 +136,5 @@ Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c
index 23c1dbf5..aa019191 100644
--- a/src/aig/aig/aigInter.c
+++ b/src/aig/aig/aigInter.c
@@ -22,6 +22,9 @@
 #include "cnf.h"
 #include "satStore.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -268,7 +271,7 @@ timeSat += clock() - clk;
     // create the resulting manager
 clk = clock();
     pManInter = Inta_ManAlloc();
-    pRes = Inta_ManInterpolate( pManInter, pSatCnf, vVarsAB, fVerbose );
+    pRes = (Aig_Man_t *)Inta_ManInterpolate( pManInter, (Sto_Man_t *)pSatCnf, vVarsAB, fVerbose );
     Inta_ManFree( pManInter );
 timeInt += clock() - clk;
 /*
@@ -283,7 +286,7 @@ timeInt += clock() - clk;
     }
 */
     Vec_IntFree( vVarsAB );
-    Sto_ManFree( pSatCnf );
+    Sto_ManFree( (Sto_Man_t *)pSatCnf );
 
 //    Ioa_WriteAiger( pRes, "inter2.aig", 0, 0 );
     return pRes;
@@ -294,3 +297,5 @@ timeInt += clock() - clk;
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 01b29f5f..40fe871b 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -21,6 +21,9 @@
 #include "aig.h"
 #include "tim.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -118,14 +121,14 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t * pObjNew;
     if ( pObj->pData )
-        return pObj->pData;
+        return (Aig_Obj_t *)pObj->pData;
     Aig_ManDup_rec( pNew, p, Aig_ObjFanin0(pObj) );
     if ( Aig_ObjIsBuf(pObj) )
-        return pObj->pData = Aig_ObjChild0Copy(pObj);
+        return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
     Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
     pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
     Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
-    return pObj->pData = pObjNew;
+    return (Aig_Obj_t *)(pObj->pData = pObjNew);
 }
 
 /**Function*************************************************************
@@ -157,7 +160,7 @@ Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t *
     Aig_ManDup_rec( pNew, p, pNode1 );   
     Aig_ManDup_rec( pNew, p, pNode2 );   
     // construct the EXOR
-    pObj = Aig_Exor( pNew, pNode1->pData, pNode2->pData ); 
+    pObj = Aig_Exor( pNew, (Aig_Obj_t *)pNode1->pData, (Aig_Obj_t *)pNode2->pData ); 
     pObj = Aig_NotCond( pObj, Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) );
     // add the PO
     Aig_ObjCreatePo( pNew, pObj );
@@ -183,35 +186,33 @@ void Aig_ManStop( Aig_Man_t * p )
 {
     Aig_Obj_t * pObj;
     int i;
-    if ( p->vMapped )
-        Vec_PtrFree( p->vMapped );
-    // print time
     if ( p->time1 ) { ABC_PRT( "time1", p->time1 ); }
     if ( p->time2 ) { ABC_PRT( "time2", p->time2 ); }
-    // delete timing
-    if ( p->pManTime )
-        Tim_ManStop( p->pManTime );
-    // delete fanout
-    if ( p->pFanData ) 
-        Aig_ManFanoutStop( p );
     // make sure the nodes have clean marks
     Aig_ManForEachObj( p, pObj, i )
         assert( !pObj->fMarkA && !pObj->fMarkB );
+    Tim_ManStopP( (Tim_Man_t **)&p->pManTime );
+    if ( p->pFanData ) 
+        Aig_ManFanoutStop( p );
+    if ( p->pManExdc )  
+        Aig_ManStop( p->pManExdc );
 //    Aig_TableProfile( p );
     Aig_MmFixedStop( p->pMemObjs, 0 );
-    if ( p->vPis )      Vec_PtrFree( p->vPis );
-    if ( p->vPos )      Vec_PtrFree( p->vPos );
-    if ( p->vObjs )     Vec_PtrFree( p->vObjs );
-    if ( p->vBufs )     Vec_PtrFree( p->vBufs );
-    if ( p->vLevelR )   Vec_IntFree( p->vLevelR );
-    if ( p->vLevels )   Vec_VecFree( p->vLevels );
-    if ( p->vFlopNums)  Vec_IntFree( p->vFlopNums );
-    if ( p->vFlopReprs) Vec_IntFree( p->vFlopReprs );
-    if ( p->pManExdc )  Aig_ManStop( p->pManExdc );
-    if ( p->vOnehots )  Vec_VecFree( (Vec_Vec_t *)p->vOnehots );
-    if ( p->vClockDoms) Vec_VecFree( p->vClockDoms );
-    if ( p->vProbs )    Vec_IntFree( p->vProbs );
-    if ( p->vCiNumsOrig)Vec_IntFree( p->vCiNumsOrig );
+    Vec_PtrFreeP( &p->vPis );
+    Vec_PtrFreeP( &p->vPos );
+    Vec_PtrFreeP( &p->vObjs );
+    Vec_PtrFreeP( &p->vBufs );
+    Vec_IntFreeP( &p->vLevelR );
+    Vec_VecFreeP( &p->vLevels );
+    Vec_IntFreeP( &p->vFlopNums );
+    Vec_IntFreeP( &p->vFlopReprs );
+    Vec_VecFreeP( (Vec_Vec_t **)&p->vOnehots );
+    Vec_VecFreeP( &p->vClockDoms );
+    Vec_IntFreeP( &p->vProbs );
+    Vec_IntFreeP( &p->vCiNumsOrig );
+    Vec_PtrFreeP( &p->vMapped );
+    if ( p->pSeqModelVec )
+        Vec_PtrFreeFree( p->pSeqModelVec );
     ABC_FREE( p->pFastSim );
     ABC_FREE( p->pData );
     ABC_FREE( p->pSeqModel );
@@ -226,6 +227,25 @@ void Aig_ManStop( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Stops the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManStopP( Aig_Man_t ** p )
+{
+    if ( *p == NULL )
+        return;
+    Aig_ManStop( *p );
+    *p = NULL;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Removes combinational logic that does not feed into POs.]
 
   Description [Returns the number of dangling nodes removed.]
@@ -246,7 +266,7 @@ int Aig_ManCleanup( Aig_Man_t * p )
         if ( Aig_ObjIsNode(pNode) && Aig_ObjRefs(pNode) == 0 )
             Vec_PtrPush( vObjs, pNode );
     // recursively remove dangling nodes
-    Vec_PtrForEachEntry( vObjs, pNode, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vObjs, pNode, i )
         Aig_ObjDelete_rec( p, pNode, 1 );
     Vec_PtrFree( vObjs );
     return nNodesOld - Aig_ManNodeNum(p);
@@ -288,7 +308,7 @@ int Aig_ManPiCleanup( Aig_Man_t * p )
 {
     Aig_Obj_t * pObj;
     int i, k = 0, nPisOld = Aig_ManPiNum(p);
-    Vec_PtrForEachEntry( p->vPis, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vPis, pObj, i )
     {
         if ( i >= Aig_ManPiNum(p) - Aig_ManRegNum(p) )
             Vec_PtrWriteEntry( p->vPis, k++, pObj );
@@ -319,7 +339,7 @@ int Aig_ManPoCleanup( Aig_Man_t * p )
 {
     Aig_Obj_t * pObj;
     int i, k = 0, nPosOld = Aig_ManPoNum(p);
-    Vec_PtrForEachEntry( p->vPos, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vPos, pObj, i )
     {
         if ( i >= Aig_ManPoNum(p) - Aig_ManRegNum(p) )
             Vec_PtrWriteEntry( p->vPos, k++, pObj );
@@ -453,9 +473,28 @@ void Aig_ManFlipFirstPo( Aig_Man_t * p )
     Aig_ObjChild0Flip( Aig_ManPo(p, 0) ); 
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Aig_ManReleaseData( Aig_Man_t * p )
+{ 
+    void * pD = p->pData; 
+    p->pData = NULL; 
+    return pD;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigMem.c b/src/aig/aig/aigMem.c
index c0b76ff8..a21b812d 100644
--- a/src/aig/aig/aigMem.c
+++ b/src/aig/aig/aigMem.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -31,7 +34,7 @@ struct Aig_MmFixed_t_
     int           nEntriesAlloc; // the total number of entries allocated
     int           nEntriesUsed;  // the number of entries in use
     int           nEntriesMax;   // the max number of entries in use
-    char *        pEntriesFree;  // the linked list of ABC_FREE entries
+    char *        pEntriesFree;  // the linked list of free entries
 
     // this is where the memory is stored
     int           nChunkSize;    // the size of one chunk
@@ -48,8 +51,8 @@ struct Aig_MmFlex_t_
 {
     // information about individual entries
     int           nEntriesUsed;  // the number of entries allocated
-    char *        pCurrent;      // the current pointer to ABC_FREE memory
-    char *        pEnd;          // the first entry outside the ABC_FREE memory
+    char *        pCurrent;      // the current pointer to free memory
+    char *        pEnd;          // the first entry outside the free memory
 
     // this is where the memory is stored
     int           nChunkSize;    // the size of one chunk
@@ -160,7 +163,7 @@ char * Aig_MmFixedEntryFetch( Aig_MmFixed_t * p )
     char * pTemp;
     int i;
 
-    // check if there are still ABC_FREE entries
+    // check if there are still free entries
     if ( p->nEntriesUsed == p->nEntriesAlloc )
     { // need to allocate more entries
         assert( p->pEntriesFree == NULL );
@@ -189,7 +192,7 @@ char * Aig_MmFixedEntryFetch( Aig_MmFixed_t * p )
     p->nEntriesUsed++;
     if ( p->nEntriesMax < p->nEntriesUsed )
         p->nEntriesMax = p->nEntriesUsed;
-    // return the first entry in the ABC_FREE entry list
+    // return the first entry in the free entry list
     pTemp = p->pEntriesFree;
     p->pEntriesFree = *((char **)pTemp);
     return pTemp;
@@ -210,7 +213,7 @@ void Aig_MmFixedEntryRecycle( Aig_MmFixed_t * p, char * pEntry )
 {
     // decrement the counter of used entries
     p->nEntriesUsed--;
-    // add the entry to the linked list of ABC_FREE entries
+    // add the entry to the linked list of free entries
     *((char **)pEntry) = p->pEntriesFree;
     p->pEntriesFree = pEntry;
 }
@@ -245,7 +248,7 @@ void Aig_MmFixedRestart( Aig_MmFixed_t * p )
     }
     // set the last link
     *((char **)pTemp) = NULL;
-    // set the ABC_FREE entry list
+    // set the free entry list
     p->pEntriesFree  = p->pChunks[0];
     // set the correct statistics
     p->nMemoryAlloc  = p->nEntrySize * p->nChunkSize;
@@ -363,7 +366,7 @@ void Aig_MmFlexStop( Aig_MmFlex_t * p, int fVerbose )
 char * Aig_MmFlexEntryFetch( Aig_MmFlex_t * p, int nBytes )
 {
     char * pTemp;
-    // check if there are still ABC_FREE entries
+    // check if there are still free entries
     if ( p->pCurrent == NULL || p->pCurrent + nBytes > p->pEnd )
     { // need to allocate more entries
         if ( p->nChunks == p->nChunksAlloc )
@@ -591,3 +594,5 @@ int Aig_MmStepReadMemUsage( Aig_MmStep_t * p )
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigMffc.c b/src/aig/aig/aigMffc.c
index b902e609..2f51e442 100644
--- a/src/aig/aig/aigMffc.c
+++ b/src/aig/aig/aigMffc.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -237,11 +240,11 @@ int Aig_NodeMffcLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves
     assert( !Aig_IsComplement(pNode) );
     assert( Aig_ObjIsNode(pNode) );
     Aig_ManIncrementTravId( p );
-    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
         pObj->nRefs++;
     ConeSize1 = Aig_NodeDeref_rec( pNode, 0, NULL, NULL );
     ConeSize2 = Aig_NodeRefLabel_rec( p, pNode, 0 );
-    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
         pObj->nRefs--;
     assert( ConeSize1 == ConeSize2 );
     assert( ConeSize1 > 0 );
@@ -265,7 +268,7 @@ int Aig_NodeMffcExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves
     int i, LevelMax, ConeSize1, ConeSize2, ConeCur1, ConeCur2, ConeBest;
     // dereference the current cut
     LevelMax = 0;
-    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
         LevelMax = ABC_MAX( LevelMax, (int)pObj->Level );
     if ( LevelMax == 0 )
         return 0;
@@ -274,7 +277,7 @@ int Aig_NodeMffcExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves
     // try expanding each node in the boundary
     ConeBest = ABC_INFINITY;
     pLeafBest = NULL;
-    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
     {
         if ( (int)pObj->Level != LevelMax )
             continue;
@@ -309,3 +312,5 @@ int Aig_NodeMffcExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 9034f272..141afaaa 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -441,7 +444,7 @@ int Aig_ManPropagateBuffers( Aig_Man_t * p, int fUpdateLevel )
     for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )
     {
         // get the node with a buffer fanin
-        for ( pObj = Vec_PtrEntryLast(p->vBufs); Aig_ObjIsBuf(pObj); pObj = Aig_ObjFanout0(p, pObj) );
+        for ( pObj = (Aig_Obj_t *)Vec_PtrEntryLast(p->vBufs); Aig_ObjIsBuf(pObj); pObj = Aig_ObjFanout0(p, pObj) );
         // replace this node by a node without buffer
         Aig_NodeFixBufferFanins( p, pObj, fUpdateLevel );
         // stop if a cycle occured
@@ -549,3 +552,5 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigOper.c b/src/aig/aig/aigOper.c
index 208e2d44..127d6ef8 100644
--- a/src/aig/aig/aigOper.c
+++ b/src/aig/aig/aigOper.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -262,6 +265,48 @@ Aig_Obj_t * Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
 
   Synopsis    [Implements ITE operation.]
 
+  Description [] 
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_TableLookupInt( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
+{
+    if ( p0 == p1 )
+        return p0;
+    if ( p0 == Aig_ManConst0(p) || p1 == Aig_ManConst0(p) || p0 == Aig_Not(p1) )
+        return Aig_ManConst0(p);
+    if ( p0 == Aig_ManConst1(p) )
+        return p1;
+    if ( p1 == Aig_ManConst1(p) )
+        return p0;
+    if ( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id )
+        return Aig_TableLookup( p, Aig_ObjCreateGhost(p, p0, p1, AIG_OBJ_AND) );
+    return Aig_TableLookup( p, Aig_ObjCreateGhost(p, p1, p0, AIG_OBJ_AND) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements ITE operation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_Mux2( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 )
+{
+    return Aig_Or( p, Aig_And(p, pC, p1), Aig_And(p, Aig_Not(pC), p0) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Implements ITE operation.]
+
   Description []
                
   SideEffects []
@@ -271,46 +316,50 @@ Aig_Obj_t * Aig_Or( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1 )
 ***********************************************************************/
 Aig_Obj_t * Aig_Mux( Aig_Man_t * p, Aig_Obj_t * pC, Aig_Obj_t * p1, Aig_Obj_t * p0 )
 {
-/*
+    int fUseMuxCanon = 0;
     Aig_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp;
     int Count0, Count1;
-    // consider trivial cases
-    if ( p0 == Aig_Not(p1) )
+    if ( !fUseMuxCanon )
+        return Aig_Mux2( p, pC, p1, p0 );
+    if ( p0 == p1 )
+        return p0;
+    if ( p1 == Aig_Not(p0) )
         return Aig_Exor( p, pC, p0 );
-    // other cases can be added
+    if ( pC == Aig_ManConst0(p) )
+        return p0;
+    if ( pC == Aig_ManConst1(p) )
+        return p1;
+    if ( p0 == Aig_ManConst0(p) )
+        return Aig_And( p, pC, p1 );
+    if ( p0 == Aig_ManConst1(p) )
+        return Aig_Or( p, Aig_Not(pC), p1 );
+    if ( p1 == Aig_ManConst0(p) )
+        return Aig_And( p, Aig_Not(pC), p0 );
+    if ( p1 == Aig_ManConst1(p) )
+        return Aig_Or( p, pC, p0 );
     // implement the first MUX (F = C * x1 + C' * x0)
-
-    // check for constants here!!!
-
-    pTempA1 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, pC,          p1, AIG_OBJ_AND) );
-    pTempA2 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, Aig_Not(pC), p0, AIG_OBJ_AND) );
+    pTempA1 = Aig_TableLookupInt( p, pC,          p1 );
+    pTempA2 = Aig_TableLookupInt( p, Aig_Not(pC), p0 );
     if ( pTempA1 && pTempA2 )
     {
-        pTemp = Aig_TableLookup( p, Aig_ObjCreateGhost(p, Aig_Not(pTempA1), Aig_Not(pTempA2), AIG_OBJ_AND) );
+        pTemp = Aig_TableLookupInt( p, Aig_Not(pTempA1), Aig_Not(pTempA2) );
         if ( pTemp ) return Aig_Not(pTemp);
     }
     Count0 = (pTempA1 != NULL) + (pTempA2 != NULL);
     // implement the second MUX (F' = C * x1' + C' * x0')
-    pTempB1 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, pC,          Aig_Not(p1), AIG_OBJ_AND) );
-    pTempB2 = Aig_TableLookup( p, Aig_ObjCreateGhost(p, Aig_Not(pC), Aig_Not(p0), AIG_OBJ_AND) );
+    pTempB1 = Aig_TableLookupInt( p, pC,          Aig_Not(p1) );
+    pTempB2 = Aig_TableLookupInt( p, Aig_Not(pC), Aig_Not(p0) );
     if ( pTempB1 && pTempB2 )
     {
-        pTemp = Aig_TableLookup( p, Aig_ObjCreateGhost(p, Aig_Not(pTempB1), Aig_Not(pTempB2), AIG_OBJ_AND) );
+        pTemp = Aig_TableLookupInt( p, Aig_Not(pTempB1), Aig_Not(pTempB2) );
         if ( pTemp ) return pTemp;
     }
     Count1 = (pTempB1 != NULL) + (pTempB2 != NULL);
     // compare and decide which one to implement
     if ( Count0 >= Count1 )
-    {
-        pTempA1 = pTempA1? pTempA1 : Aig_And(p, pC,          p1);
-        pTempA2 = pTempA2? pTempA2 : Aig_And(p, Aig_Not(pC), p0);
-        return Aig_Or( p, pTempA1, pTempA2 );
-    }
-    pTempB1 = pTempB1? pTempB1 : Aig_And(p, pC,          Aig_Not(p1));
-    pTempB2 = pTempB2? pTempB2 : Aig_And(p, Aig_Not(pC), Aig_Not(p0));
-    return Aig_Not( Aig_Or( p, pTempB1, pTempB2 ) );
-*/
-    return Aig_Or( p, Aig_And(p, pC, p1), Aig_And(p, Aig_Not(pC), p0) );
+        return Aig_Or( p, Aig_And(p, pC, p1), Aig_And(p, Aig_Not(pC), p0) );
+    return Aig_Not( Aig_Or( p, Aig_And(p, pC, Aig_Not(p1)), Aig_And(p, Aig_Not(pC), Aig_Not(p0)) ) );
+//    return Aig_Or( p, Aig_And(p, pC, p1), Aig_And(p, Aig_Not(pC), p0) );
 }
 
 /**Function*************************************************************
@@ -385,7 +434,7 @@ Aig_Obj_t * Aig_Miter( Aig_Man_t * p, Vec_Ptr_t * vPairs )
     assert( vPairs->nSize > 0 );
     assert( vPairs->nSize % 2 == 0 );
     for ( i = 0; i < vPairs->nSize; i += 2 )
-        vPairs->pArray[i/2] = Aig_Not( Aig_Exor( p, vPairs->pArray[i], vPairs->pArray[i+1] ) );
+        vPairs->pArray[i/2] = Aig_Not( Aig_Exor( p, (Aig_Obj_t *)vPairs->pArray[i], (Aig_Obj_t *)vPairs->pArray[i+1] ) );
     vPairs->nSize = vPairs->nSize/2;
     return Aig_Not( Aig_Multi_rec( p, (Aig_Obj_t **)vPairs->pArray, vPairs->nSize, AIG_OBJ_AND ) );
 }
@@ -407,7 +456,7 @@ Aig_Obj_t * Aig_MiterTwo( Aig_Man_t * p, Vec_Ptr_t * vNodes1, Vec_Ptr_t * vNodes
     assert( vNodes1->nSize > 0 && vNodes1->nSize > 0 );
     assert( vNodes1->nSize == vNodes2->nSize );
     for ( i = 0; i < vNodes1->nSize; i++ )
-        vNodes1->pArray[i] = Aig_Not( Aig_Exor( p, vNodes1->pArray[i], vNodes2->pArray[i] ) );
+        vNodes1->pArray[i] = Aig_Not( Aig_Exor( p, (Aig_Obj_t *)vNodes1->pArray[i], (Aig_Obj_t *)vNodes2->pArray[i] ) );
     return Aig_Not( Aig_Multi_rec( p, (Aig_Obj_t **)vNodes1->pArray, vNodes1->nSize, AIG_OBJ_AND ) );
 }
 
@@ -474,8 +523,84 @@ Aig_Obj_t * Aig_CreateExor( Aig_Man_t * p, int nVars )
     return pFunc;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Implements ITE operation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_MuxTest()
+{
+    Vec_Ptr_t * vNodes;
+    Aig_Man_t * p;
+    Aig_Obj_t * pObj, * pFanin0, * pFanin1, * pCtrl;    
+    int nNodes  = 2000;
+    int i,nPIs  =   20;
+//    srand( time(NULL) );
+    srand( 321 );
+    vNodes = Vec_PtrAlloc( 100 );
+    // create a bunch of random MUXes
+    p = Aig_ManStart( 10000 );
+    for ( i = 0; i < nPIs; i++ )
+        Aig_IthVar(p,i);
+    for ( i = 0; i < nNodes; i++ )
+    {
+        if ( rand() % 10 == 0 )
+            pCtrl = Aig_ManConst0(p);
+        else if ( rand() % 10 == 0 )
+            pCtrl = Aig_ManConst1(p);
+        else if ( rand() % 3 == 0 || i < nPIs )
+            pCtrl = Aig_IthVar( p, rand() % nPIs );
+        else
+            pCtrl = (Aig_Obj_t *)Vec_PtrEntry(vNodes, rand() % i);
+        if ( rand() % 2 == 0 )
+            pCtrl = Aig_Not( pCtrl );
+
+        if ( rand() % 10 == 0 )
+            pFanin1 = Aig_ManConst0(p);
+        else if ( rand() % 10 == 0 )
+            pFanin1 = Aig_ManConst1(p);
+        else if ( rand() % 3 == 0 || i < nPIs )
+            pFanin1 = Aig_IthVar( p, rand() % nPIs );
+        else
+            pFanin1 = (Aig_Obj_t *)Vec_PtrEntry(vNodes, rand() % i);
+        if ( rand() % 2 == 0 )
+            pFanin1 = Aig_Not( pFanin1 );
+
+        if ( rand() % 10 == 0 )
+            pFanin0 = Aig_ManConst0(p);
+        else if ( rand() % 10 == 0 )
+            pFanin0 = Aig_ManConst1(p);
+        else if ( rand() % 3 == 0 || i < nPIs )
+            pFanin0 = Aig_IthVar( p, rand() % nPIs );
+        else
+            pFanin0 = (Aig_Obj_t *)Vec_PtrEntry(vNodes, rand() % i);
+        if ( rand() % 2 == 0 )
+            pFanin0 = Aig_Not( pFanin0 );
+
+        pObj = Aig_Mux( p, pCtrl, pFanin1, pFanin0 );
+        Vec_PtrPush( vNodes, pObj );
+    }
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+        Aig_ObjCreatePo( p, pObj );
+    Vec_PtrFree( vNodes );
+
+    printf( "Number of nodes = %6d.\n", Aig_ManObjNum(p) );
+    Aig_ManCleanup( p );
+    printf( "Number of nodes = %6d.\n", Aig_ManObjNum(p) );
+    Aig_ManDumpBlif( p, "test1.blif", NULL, NULL );
+    Aig_ManStop( p );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigOrder.c b/src/aig/aig/aigOrder.c
index 746f0f18..21bf8b8e 100644
--- a/src/aig/aig/aigOrder.c
+++ b/src/aig/aig/aigOrder.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -169,3 +172,5 @@ void Aig_ObjOrderAdvance( Aig_Man_t * p )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 6849ba70..52960cd3 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -20,6 +20,10 @@
 
 #include "aig.h"
 #include "tim.h"
+#include "fra.h"
+
+ABC_NAMESPACE_IMPL_START
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -30,10 +34,10 @@ struct Part_Man_t_
 {
     int              nChunkSize;    // the size of one chunk of memory (~1 Mb)
     int              nStepSize;     // the step size in saving memory (~64 bytes)
-    char *           pFreeBuf;      // the pointer to ABC_FREE memory
-    int              nFreeSize;     // the size of remaining ABC_FREE memory
+    char *           pFreeBuf;      // the pointer to free memory
+    int              nFreeSize;     // the size of remaining free memory
     Vec_Ptr_t *      vMemory;       // the memory allocated
-    Vec_Ptr_t *      vFree;         // the vector of ABC_FREE pieces of memory
+    Vec_Ptr_t *      vFree;         // the vector of free pieces of memory
 };
 
 typedef struct Part_One_t_     Part_One_t;
@@ -91,7 +95,7 @@ void Part_ManStop( Part_Man_t * p )
 {
     void * pMemory;
     int i;
-    Vec_PtrForEachEntry( p->vMemory, pMemory, i )
+    Vec_PtrForEachEntry( void *, p->vMemory, pMemory, i )
         ABC_FREE( pMemory );
     Vec_PtrFree( p->vMemory );
     Vec_PtrFree( p->vFree );
@@ -116,7 +120,7 @@ char * Part_ManFetch( Part_Man_t * p, int nSize )
     assert( nSize > 0 );
     Type = Part_SizeType( nSize, p->nStepSize );
     Vec_PtrFillExtra( p->vFree, Type + 1, NULL );
-    if ( (pMemory = Vec_PtrEntry( p->vFree, Type )) )
+    if ( (pMemory = (char *)Vec_PtrEntry( p->vFree, Type )) )
     {
         Vec_PtrWriteEntry( p->vFree, Type, Part_OneNext(pMemory) );
         return pMemory;
@@ -151,7 +155,7 @@ void Part_ManRecycle( Part_Man_t * p, char * pMemory, int nSize )
     int Type;
     Type = Part_SizeType( nSize, p->nStepSize );
     Vec_PtrFillExtra( p->vFree, Type + 1, NULL );
-    Part_OneSetNext( pMemory, Vec_PtrEntry(p->vFree, Type) );
+    Part_OneSetNext( pMemory, (char *)Vec_PtrEntry(p->vFree, Type) );
     Vec_PtrWriteEntry( p->vFree, Type, pMemory );
 }
 
@@ -288,8 +292,8 @@ Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * pMan )
     {
         if ( Aig_ObjIsNode(pObj) )
         {
-            pPart0 = Aig_ObjFanin0(pObj)->pData;
-            pPart1 = Aig_ObjFanin1(pObj)->pData;
+            pPart0 = (Part_One_t *)Aig_ObjFanin0(pObj)->pData;
+            pPart1 = (Part_One_t *)Aig_ObjFanin1(pObj)->pData;
             pObj->pData = Part_ManMergeEntry( p, pPart0, pPart1, pObj->nRefs );
             assert( pPart0->nRefs > 0 );
             if ( --pPart0->nRefs == 0 )
@@ -301,7 +305,7 @@ Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * pMan )
         }
         if ( Aig_ObjIsPo(pObj) )
         {
-            pPart0 = Aig_ObjFanin0(pObj)->pData;
+            pPart0 = (Part_One_t *)Aig_ObjFanin0(pObj)->pData;
             vSupp = Part_ManTransferEntry(pPart0);
             Vec_IntPush( vSupp, (int)(long)pObj->pNext );
             Vec_PtrPush( vSupports, vSupp );
@@ -369,11 +373,11 @@ Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p )
     for ( i = 0; i < Aig_ManPiNum(p); i++ )
         Vec_PtrPush( vSuppsInv, Vec_IntAlloc(8) );
     // transforms the supports into the inverse supports
-    Vec_PtrForEachEntry( vSupps, vSupp, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vSupps, vSupp, i )
     {
         iOut = Vec_IntPop( vSupp );
         Vec_IntForEachEntry( vSupp, iIn, k )
-            Vec_IntPush( Vec_PtrEntry(vSuppsInv, iIn), iOut );
+            Vec_IntPush( (Vec_Int_t *)Vec_PtrEntry(vSuppsInv, iIn), iOut );
     }
     Vec_VecFree( (Vec_Vec_t *)vSupps );
     return vSuppsInv;
@@ -399,7 +403,7 @@ Vec_Ptr_t * Aig_ManSupportsRegisters( Aig_Man_t * p )
     vSupports = Aig_ManSupports( p );
     // transforms the supports into the latch dependency matrix
     vMatrix = Vec_PtrStart( Aig_ManRegNum(p) );
-    Vec_PtrForEachEntry( vSupports, vSupp, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vSupports, vSupp, i )
     {
         // skip true POs
         iOut = Vec_IntPop( vSupp );
@@ -426,7 +430,7 @@ Vec_Ptr_t * Aig_ManSupportsRegisters( Aig_Man_t * p )
     }
     Vec_PtrFree( vSupports );
     // check that all supports are used
-    Vec_PtrForEachEntry( vMatrix, vSupp, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vMatrix, vSupp, i )
         assert( vSupp != NULL );
     return vMatrix;
 }
@@ -515,13 +519,13 @@ int Aig_ManPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vParts
     int i, nCommon, iBest;
     iBest = -1;
     ValueBest = 0;
-    Vec_PtrForEachEntry( vPartSuppsAll, vPartSupp, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vPartSuppsAll, vPartSupp, i )
     {
 //        vPart = Vec_PtrEntry( vPartsAll, i );
 //        if ( nSuppSizeLimit > 0 && Vec_IntSize(vPart) >= nSuppSizeLimit )
 //            continue;
 //        nCommon = Vec_IntTwoCountCommon( vPartSupp, vOne );
-        nCommon = Aig_ManSuppCharCommon( Vec_PtrEntry(vPartSuppsBit, i), vOne );
+        nCommon = Aig_ManSuppCharCommon( (unsigned *)Vec_PtrEntry(vPartSuppsBit, i), vOne );
         if ( nCommon == 0 )
             continue;
         if ( nCommon == Vec_IntSize(vOne) )
@@ -563,9 +567,9 @@ void Aig_ManPartitionPrint( Aig_Man_t * p, Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vP
     int i, nOutputs, Counter;
 
     Counter = 0;
-    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vPartSuppsAll, vOne, i )
     {
-        nOutputs = Vec_IntSize(Vec_PtrEntry(vPartsAll, i));
+        nOutputs = Vec_IntSize((Vec_Int_t *)Vec_PtrEntry(vPartsAll, i));
         printf( "%d=(%d,%d) ", i, Vec_IntSize(vOne), nOutputs );
         Counter += nOutputs;
         if ( i == Vec_PtrSize(vPartsAll) - 1 )
@@ -597,7 +601,7 @@ void Aig_ManPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll,
     // pack smaller partitions into larger blocks
     iPart = 0;
     vPart = vPartSupp = NULL;
-    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vPartSuppsAll, vOne, i )
     {
         if ( Vec_IntSize(vOne) < nSuppSizeLimit )
         {
@@ -605,27 +609,27 @@ void Aig_ManPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll,
             {
                 assert( vPart == NULL );
                 vPartSupp = Vec_IntDup(vOne);
-                vPart = Vec_PtrEntry(vPartsAll, i);
+                vPart = (Vec_Int_t *)Vec_PtrEntry(vPartsAll, i);
             }
             else
             {
                 vPartSupp = Vec_IntTwoMerge( vTemp = vPartSupp, vOne );
                 Vec_IntFree( vTemp );
-                vPart = Vec_IntTwoMerge( vTemp = vPart, Vec_PtrEntry(vPartsAll, i) );
+                vPart = Vec_IntTwoMerge( vTemp = vPart, (Vec_Int_t *)Vec_PtrEntry(vPartsAll, i) );
                 Vec_IntFree( vTemp );
-                Vec_IntFree( Vec_PtrEntry(vPartsAll, i) );
+                Vec_IntFree( (Vec_Int_t *)Vec_PtrEntry(vPartsAll, i) );
             }
             if ( Vec_IntSize(vPartSupp) < nSuppSizeLimit )
                 continue;
         }
         else
-            vPart = Vec_PtrEntry(vPartsAll, i);
+            vPart = (Vec_Int_t *)Vec_PtrEntry(vPartsAll, i);
         // add the partition 
         Vec_PtrWriteEntry( vPartsAll, iPart, vPart );  
         vPart = NULL;
         if ( vPartSupp ) 
         {
-            Vec_IntFree( Vec_PtrEntry(vPartSuppsAll, iPart) );
+            Vec_IntFree( (Vec_Int_t *)Vec_PtrEntry(vPartSuppsAll, iPart) );
             Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );  
             vPartSupp = NULL;
         }
@@ -638,7 +642,7 @@ void Aig_ManPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll,
         vPart = NULL;
 
         assert( vPartSupp != NULL );
-        Vec_IntFree( Vec_PtrEntry(vPartSuppsAll, iPart) );
+        Vec_IntFree( (Vec_Int_t *)Vec_PtrEntry(vPartSuppsAll, iPart) );
         Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );  
         vPartSupp = NULL;
         iPart++;
@@ -679,7 +683,7 @@ ABC_PRT( "Supps", clock() - clk );
 clk = clock();
     vPartsAll = Vec_PtrAlloc( 256 );
     vPartSuppsAll = Vec_PtrAlloc( 256 );
-    Vec_PtrForEachEntry( vSupports, vOne, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vSupports, vOne, i )
     {
         // get the output number
         iOut = Vec_IntPop(vOne);
@@ -701,21 +705,21 @@ clk = clock();
         else
         {
             // add output to this partition
-            vPart = Vec_PtrEntry( vPartsAll, iPart );
+            vPart = (Vec_Int_t *)Vec_PtrEntry( vPartsAll, iPart );
             Vec_IntPush( vPart, iOut );
             // merge supports
-            vPartSupp = Vec_PtrEntry( vPartSuppsAll, iPart );
+            vPartSupp = (Vec_Int_t *)Vec_PtrEntry( vPartSuppsAll, iPart );
             vPartSupp = Vec_IntTwoMerge( vTemp = vPartSupp, vOne );
             Vec_IntFree( vTemp );
             // reinsert new support
             Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );
 
-            Aig_ManSuppCharAdd( Vec_PtrEntry(vPartSuppsBit, iPart), vOne, Aig_ManPiNum(p) );
+            Aig_ManSuppCharAdd( (unsigned *)Vec_PtrEntry(vPartSuppsBit, iPart), vOne, Aig_ManPiNum(p) );
         }
     }
 
     // stop char-based support representation
-    Vec_PtrForEachEntry( vPartSuppsBit, vTemp, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vPartSuppsBit, vTemp, i )
         ABC_FREE( vTemp );
     Vec_PtrFree( vPartSuppsBit );
 
@@ -728,13 +732,13 @@ ABC_PRT( "Parts", clock() - clk );
 clk = clock();
     // reorder partitions in the decreasing order of support sizes
     // remember partition number in each partition support
-    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vPartSuppsAll, vOne, i )
         Vec_IntPush( vOne, i );
     // sort the supports in the decreasing order
     Vec_VecSort( (Vec_Vec_t *)vPartSuppsAll, 1 );
     // reproduce partitions
     vPartsAll2 = Vec_PtrAlloc( 256 );
-    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vPartSuppsAll, vOne, i )
         Vec_PtrPush( vPartsAll2, Vec_PtrEntry(vPartsAll, Vec_IntPop(vOne)) );
     Vec_PtrFree( vPartsAll );
     vPartsAll = vPartsAll2;
@@ -759,7 +763,7 @@ if ( fVerbose )
         *pvPartSupps = vPartSuppsAll;
 /*
     // converts from intergers to nodes
-    Vec_PtrForEachEntry( vPartsAll, vPart, iPart )
+    Vec_PtrForEachEntry( Vec_Int_t *, vPartsAll, vPart, iPart )
     {
         vPartPtr = Vec_PtrAlloc( Vec_IntSize(vPart) );
         Vec_IntForEachEntry( vPart, iOut, i )
@@ -793,7 +797,7 @@ Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSuppSizeLimit
 clk = clock();
     vSupports = Aig_ManSupportsRegisters( pAig );
     assert( Vec_PtrSize(vSupports) == Aig_ManRegNum(pAig) );
-    Vec_PtrForEachEntry( vSupports, vOne, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vSupports, vOne, i )
         Vec_IntPush( vOne, i );
 if ( fVerbose )
 {
@@ -807,7 +811,7 @@ ABC_PRT( "Supps", clock() - clk );
 clk = clock();
     vPartsAll = Vec_PtrAlloc( 256 );
     vPartSuppsAll = Vec_PtrAlloc( 256 );
-    Vec_PtrForEachEntry( vSupports, vOne, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vSupports, vOne, i )
     {
         // get the output number
         iOut = Vec_IntPop(vOne);
@@ -829,21 +833,21 @@ clk = clock();
         else
         {
             // add output to this partition
-            vPart = Vec_PtrEntry( vPartsAll, iPart );
+            vPart = (Vec_Int_t *)Vec_PtrEntry( vPartsAll, iPart );
             Vec_IntPush( vPart, iOut );
             // merge supports
-            vPartSupp = Vec_PtrEntry( vPartSuppsAll, iPart );
+            vPartSupp = (Vec_Int_t *)Vec_PtrEntry( vPartSuppsAll, iPart );
             vPartSupp = Vec_IntTwoMerge( vTemp = vPartSupp, vOne );
             Vec_IntFree( vTemp );
             // reinsert new support
             Vec_PtrWriteEntry( vPartSuppsAll, iPart, vPartSupp );
 
-            Aig_ManSuppCharAdd( Vec_PtrEntry(vPartSuppsBit, iPart), vOne, Vec_PtrSize(vSupports) );
+            Aig_ManSuppCharAdd( (unsigned *)Vec_PtrEntry(vPartSuppsBit, iPart), vOne, Vec_PtrSize(vSupports) );
         }
     }
 
     // stop char-based support representation
-    Vec_PtrForEachEntry( vPartSuppsBit, vTemp, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vPartSuppsBit, vTemp, i )
         ABC_FREE( vTemp );
     Vec_PtrFree( vPartSuppsBit );
 
@@ -856,13 +860,13 @@ ABC_PRT( "Parts", clock() - clk );
 clk = clock();
     // reorder partitions in the decreasing order of support sizes
     // remember partition number in each partition support
-    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vPartSuppsAll, vOne, i )
         Vec_IntPush( vOne, i );
     // sort the supports in the decreasing order
     Vec_VecSort( (Vec_Vec_t *)vPartSuppsAll, 1 );
     // reproduce partitions
     vPartsAll2 = Vec_PtrAlloc( 256 );
-    Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vPartSuppsAll, vOne, i )
         Vec_PtrPush( vPartsAll2, Vec_PtrEntry(vPartsAll, Vec_IntPop(vOne)) );
     Vec_PtrFree( vPartsAll );
     vPartsAll = vPartsAll2;
@@ -888,7 +892,7 @@ if ( fVerbose )
 
 /*
     // converts from intergers to nodes
-    Vec_PtrForEachEntry( vPartsAll, vPart, iPart )
+    Vec_PtrForEachEntry( Vec_Int_t *, vPartsAll, vPart, iPart )
     {
         vPartPtr = Vec_PtrAlloc( Vec_IntSize(vPart) );
         Vec_IntForEachEntry( vPart, iOut, i )
@@ -919,7 +923,7 @@ Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize )
     nParts = (Aig_ManPoNum(p) / nPartSize) + ((Aig_ManPoNum(p) % nPartSize) > 0);
     vParts = (Vec_Ptr_t *)Vec_VecStart( nParts );
     Aig_ManForEachPo( p, pObj, i )
-        Vec_IntPush( Vec_PtrEntry(vParts, i / nPartSize), i );
+        Vec_IntPush( (Vec_Int_t *)Vec_PtrEntry(vParts, i / nPartSize), i );
     return vParts;
 }
 
@@ -940,18 +944,18 @@ Aig_Obj_t * Aig_ManDupPart_rec( Aig_Man_t * pNew, Aig_Man_t * pOld, Aig_Obj_t *
 {
     assert( !Aig_IsComplement(pObj) );
     if ( Aig_ObjIsTravIdCurrent(pOld, pObj) )
-        return pObj->pData;
+        return (Aig_Obj_t *)pObj->pData;
     Aig_ObjSetTravIdCurrent(pOld, pObj);
     if ( Aig_ObjIsPi(pObj) )
     {
         assert( Vec_IntSize(vSuppMap) == Aig_ManPiNum(pNew) );
         Vec_IntPush( vSuppMap, (int)(long)pObj->pNext );
-        return pObj->pData = Aig_ObjCreatePi(pNew);
+        return (Aig_Obj_t *)(pObj->pData = Aig_ObjCreatePi(pNew));
     }
     assert( Aig_ObjIsNode(pObj) );
     Aig_ManDupPart_rec( pNew, pOld, Aig_ObjFanin0(pObj), vSuppMap );
     Aig_ManDupPart_rec( pNew, pOld, Aig_ObjFanin1(pObj), vSuppMap );
-    return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
 }
 
 /**Function*************************************************************
@@ -1133,7 +1137,7 @@ Vec_Ptr_t * Aig_ManSupportNodes( Aig_Man_t * p, Vec_Ptr_t * vParts )
     int i, k, iOut;
     Aig_ManSetPioNumbers( p );
     vPartSupps = Vec_PtrAlloc( Vec_PtrSize(vParts) );
-    Vec_PtrForEachEntry( vParts, vPart, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
     {
         vSupport = Vec_IntAlloc( 100 );
         Aig_ManIncrementTravId( p );
@@ -1180,8 +1184,8 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi
     for ( i = 0; i < Vec_PtrSize(vParts); i++ )
     {
         // get partition and its support
-        vPart     = Vec_PtrEntry( vParts, i );
-        vPartSupp = Vec_PtrEntry( vPartSupps, i );
+        vPart     = (Vec_Int_t *)Vec_PtrEntry( vParts, i );
+        vPartSupp = (Vec_Int_t *)Vec_PtrEntry( vPartSupps, i );
         // create the new miter
         pNew = Aig_ManStart( 1000 );
         // create the PIs
@@ -1221,7 +1225,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
 {
 //    extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
 //    extern void * Abc_FrameGetGlobalFrame();
-    extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
+//    extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
 
     Vec_Ptr_t * vPios;
     Vec_Ptr_t * vOutsTotal, * vOuts;
@@ -1235,11 +1239,11 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
 
     // compute the total number of IDs
     nIdMax = 0;
-    Vec_PtrForEachEntry( vAigs, pAig, i )
+    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig, i )
         nIdMax += Aig_ManObjNumMax(pAig);
 
     // partition the first AIG in the array
-    pAig = Vec_PtrEntry( vAigs, 0 );
+    pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 );
     vParts = Aig_ManPartitionSmart( pAig, nPartSize, 0, NULL );
 
     // start the total fraiged AIG
@@ -1248,7 +1252,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
     vOutsTotal = Vec_PtrStart( Aig_ManPoNum(pAig) );
 
     // set the PI numbers
-    Vec_PtrForEachEntry( vAigs, pAig, i )
+    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig, i )
         Aig_ManForEachPi( pAig, pObj, k )
             pObj->pNext = (Aig_Obj_t *)(long)k;
 
@@ -1256,18 +1260,18 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
 
     // create the total fraiged AIG
     vPartSupp = Vec_IntAlloc( 100 ); // maps part PI num into total PI num
-    Vec_PtrForEachEntry( vParts, vPart, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
     {
         // derive the partition AIG
         pAigPart = Aig_ManStart( 5000 );
 //        pAigPart->pName = Extra_UtilStrsav( pAigPart->pName );
         Vec_IntClear( vPartSupp );
-        Vec_PtrForEachEntry( vAigs, pAig, k )
+        Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig, k )
         {
             vOuts = Aig_ManDupPart( pAigPart, pAig, vPart, vPartSupp, 0 );
             if ( k == 0 )
             {
-                Vec_PtrForEachEntry( vOuts, pObj, m )
+                Vec_PtrForEachEntry( Aig_Obj_t *, vOuts, pObj, m )
                     Aig_ObjCreatePo( pAigPart, pObj );
             }
             Vec_PtrFree( vOuts );
@@ -1275,7 +1279,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
         // derive the total AIG from the partitioned AIG
         vOuts = Aig_ManDupPart( pAigTotal, pAigPart, vPart, vPartSupp, 1 );
         // add to the outputs
-        Vec_PtrForEachEntry( vOuts, pObj, k )
+        Vec_PtrForEachEntry( Aig_Obj_t *, vOuts, pObj, k )
         {
             assert( Vec_PtrEntry( vOutsTotal, Vec_IntEntry(vPart,k) ) == NULL );
             Vec_PtrWriteEntry( vOutsTotal, Vec_IntEntry(vPart,k), pObj );
@@ -1310,12 +1314,12 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
 //    Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
 
     // clear the PI numbers
-    Vec_PtrForEachEntry( vAigs, pAig, i )
+    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig, i )
         Aig_ManForEachPi( pAig, pObj, k )
             pObj->pNext = NULL;
 
     // add the outputs in the same order
-    Vec_PtrForEachEntry( vOutsTotal, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vOutsTotal, pObj, i )
         Aig_ObjCreatePo( pAigTotal, pObj );
     Vec_PtrFree( vOutsTotal );
 
@@ -1324,14 +1328,14 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
     // create the equivalent nodes lists
     Aig_ManMarkValidChoices( pAig );
     // reconstruct the network
-    vPios = Aig_ManOrderPios( pAig, Vec_PtrEntry(vAigs,0) );
+    vPios = Aig_ManOrderPios( pAig, (Aig_Man_t *)Vec_PtrEntry(vAigs,0) );
     pAig = Aig_ManDupDfsGuided( pTemp = pAig, vPios );
     Aig_ManStop( pTemp );
     Vec_PtrFree( vPios );
     // duplicate the timing manager
-    pTemp = Vec_PtrEntry( vAigs, 0 );
+    pTemp = (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 );
     if ( pTemp->pManTime )
-        pAig->pManTime = Tim_ManDup( pTemp->pManTime, 0 );
+        pAig->pManTime = Tim_ManDup( (Tim_Man_t *)pTemp->pManTime, 0 );
     // reset levels
     Aig_ManChoiceLevel( pAig );
     return pAig;
@@ -1351,7 +1355,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
 ***********************************************************************/
 Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose )
 {
-    extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
+//    extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
 
     Aig_Man_t * pAigPart, * pAigTemp;
     Vec_Int_t * vPart;
@@ -1370,7 +1374,7 @@ Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfM
     Aig_ManSetPioNumbers( pAig );
 
     // create the total fraiged AIG
-    Vec_PtrForEachEntry( vParts, vPart, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i )
     {
         // derive the partition AIG
         pAigPart = Aig_ManDupPartAll( pAig, vPart );
@@ -1460,7 +1464,7 @@ void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_
     Aig_ManForEachObj( pNew, pObj, i )
         pObj->fMarkB = 1;
     Aig_ManForEachObj( pPrev, pObj, i )
-        assert( Aig_Regular(pObj->pData)->fMarkB );
+        assert( Aig_Regular((Aig_Obj_t *)pObj->pData)->fMarkB );
     Aig_ManForEachObj( pNew, pObj, i )
         pObj->fMarkB = 0;
     // make sure the nodes of pThis point to pPrev
@@ -1484,14 +1488,14 @@ void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_
         if ( pObj->pHaig == NULL )
             continue;
         // pObj->pData and pObj->pHaig->pData are equivalent
-        Aig_ObjSetRepr_( pNew, Aig_Regular(pObj->pData), Aig_Regular(pObj->pHaig->pData) );
+        Aig_ObjSetRepr_( pNew, Aig_Regular((Aig_Obj_t *)pObj->pData), Aig_Regular((Aig_Obj_t *)pObj->pHaig->pData) );
     }
     // set the inputs of POs as equivalent
     Aig_ManForEachPo( pThis, pObj, i )
     {
         pObjNew = Aig_ObjFanin0( Aig_ManPo(pNew,i) );
         // pObjNew and Aig_ObjFanin0(pObj)->pData are equivalent
-        Aig_ObjSetRepr_( pNew, pObjNew, Aig_Regular(Aig_ObjFanin0(pObj)->pData) );
+        Aig_ObjSetRepr_( pNew, pObjNew, Aig_Regular((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData) );
     }
 }
 
@@ -1548,7 +1552,7 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
     Aig_Man_t * pNew, * pThis, * pPrev, * pTemp;
     int i;
     // start AIG with choices
-    pPrev = Vec_PtrEntry( vAigs, 0 );
+    pPrev = (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 );
     pNew = Aig_ManDupOrdered( pPrev );
     // create room for equivalent nodes and representatives
     assert( pNew->pReprs == NULL );
@@ -1556,7 +1560,7 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
     pNew->pReprs = ABC_ALLOC( Aig_Obj_t *, pNew->nReprsAlloc );
     memset( pNew->pReprs, 0, sizeof(Aig_Obj_t *) * pNew->nReprsAlloc );
     // add other AIGs one by one
-    Vec_PtrForEachEntryStart( vAigs, pThis, i, 1 )
+    Vec_PtrForEachEntryStart( Aig_Man_t *, vAigs, pThis, i, 1 )
     {
         Aig_ManChoiceConstructiveOne( pNew, pPrev, pThis );
         pPrev = pThis;
@@ -1566,14 +1570,14 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
     // create the equivalent nodes lists
     Aig_ManMarkValidChoices( pNew );
     // reconstruct the network
-    vPios = Aig_ManOrderPios( pNew, Vec_PtrEntry( vAigs, 0 ) );
+    vPios = Aig_ManOrderPios( pNew, (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 ) );
     pNew = Aig_ManDupDfsGuided( pTemp = pNew, vPios );
     Aig_ManStop( pTemp );
     Vec_PtrFree( vPios );
     // duplicate the timing manager
-    pTemp = Vec_PtrEntry( vAigs, 0 );
+    pTemp = (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 );
     if ( pTemp->pManTime )
-        pNew->pManTime = Tim_ManDup( pTemp->pManTime, 0 );
+        pNew->pManTime = Tim_ManDup( (Tim_Man_t *)pTemp->pManTime, 0 );
     // reset levels
     Aig_ManChoiceLevel( pNew );
     return pNew;
@@ -1590,3 +1594,5 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigPartReg.c b/src/aig/aig/aigPartReg.c
index dd10e91e..56fa80e4 100644
--- a/src/aig/aig/aigPartReg.c
+++ b/src/aig/aig/aigPartReg.c
@@ -21,6 +21,9 @@
 #include "aig.h"
 //#include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -127,7 +130,7 @@ int Aig_ManRegFindSeed( Aig_ManPre_t * p )
         if ( p->pfUsedRegs[i] )
             continue;
         nRegsCur = 0;
-        vRegs = Vec_PtrEntry( p->vMatrix, i );
+        vRegs = (Vec_Int_t *)Vec_PtrEntry( p->vMatrix, i );
         Vec_IntForEachEntry( vRegs, iReg, k )
             nRegsCur += !p->pfUsedRegs[iReg];
         if ( nRegsMax < nRegsCur )
@@ -155,13 +158,13 @@ int Aig_ManRegFindBestVar( Aig_ManPre_t * p )
     Vec_Int_t * vSupp;
     int nNewVars, nNewVarsBest = ABC_INFINITY;
     int iVarFree, iVarSupp, iVarBest = -1, i, k;
-    // go through the ABC_FREE variables
+    // go through the free variables
     Vec_IntForEachEntry( p->vFreeVars, iVarFree, i )
     {
 //        if ( p->pfUsedRegs[iVarFree] )
 //            continue;
         // get support of this variable
-        vSupp = Vec_PtrEntry( p->vMatrix, iVarFree );
+        vSupp = (Vec_Int_t *)Vec_PtrEntry( p->vMatrix, iVarFree );
         // count the number of new vars
         nNewVars = 0;
         Vec_IntForEachEntry( vSupp, iVarSupp, k )
@@ -205,7 +208,7 @@ void Aig_ManRegPartitionAdd( Aig_ManPre_t * p, int iReg )
         p->pfUsedRegs[iReg] = 1;
         Vec_IntPush( p->vUniques, iReg );
     }
-    // remove it from the ABC_FREE variables
+    // remove it from the free variables
     if ( Vec_IntSize(p->vFreeVars) > 0 )
     {
         assert( p->pfPartVars[iReg] );
@@ -218,7 +221,7 @@ void Aig_ManRegPartitionAdd( Aig_ManPre_t * p, int iReg )
     p->pfPartVars[iReg] = 1;
     Vec_IntPush( p->vRegs, iReg );
     // add new variables
-    vSupp = Vec_PtrEntry( p->vMatrix, iReg );
+    vSupp = (Vec_Int_t *)Vec_PtrEntry( p->vMatrix, iReg );
     Vec_IntForEachEntry( vSupp, iVar, i )
     {
         if ( p->pfPartVars[iVar] )
@@ -253,7 +256,7 @@ Vec_Ptr_t * Aig_ManRegProjectOnehots( Aig_Man_t * pAig, Aig_Man_t * pPart, Vec_P
         pObj->iData = i;
     // go through each group and check if registers are involved in this one
     nOffset = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
-    Vec_PtrForEachEntry( vOnehots, vGroup, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vOnehots, vGroup, i )
     {
         vGroupNew = NULL;
         Vec_IntForEachEntry( vGroup, iReg, k )
@@ -263,7 +266,7 @@ Vec_Ptr_t * Aig_ManRegProjectOnehots( Aig_Man_t * pAig, Aig_Man_t * pPart, Vec_P
                 continue;
             if ( vGroupNew == NULL )
                 vGroupNew = Vec_IntAlloc( Vec_IntSize(vGroup) );
-            pObjNew = pObj->pData;
+            pObjNew = (Aig_Obj_t *)pObj->pData;
             Vec_IntPush( vGroupNew, pObjNew->iData );
         }
         if ( vGroupNew == NULL )
@@ -284,7 +287,7 @@ Vec_Ptr_t * Aig_ManRegProjectOnehots( Aig_Man_t * pAig, Aig_Man_t * pPart, Vec_P
     if ( vOnehotsPart && fVerbose )
     {
         printf( "Partition contains %d groups of 1-hot registers: { ", Vec_PtrSize(vOnehotsPart) );
-        Vec_PtrForEachEntry( vOnehotsPart, vGroup, k )
+        Vec_PtrForEachEntry( Vec_Int_t *, vOnehotsPart, vGroup, k )
             printf( "%d ", Vec_IntSize(vGroup) );
         printf( "}\n" );
     }
@@ -335,7 +338,7 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC
         nCountPis += Aig_ObjIsTravIdCurrent(pAig, pObj);
     // count outputs of other registers
     Aig_ManForEachLoSeq( pAig, pObj, i )
-        nCountRegs += Aig_ObjIsTravIdCurrent(pAig, pObj);
+        nCountRegs += Aig_ObjIsTravIdCurrent(pAig, pObj); 
     if ( pnCountPis )
         *pnCountPis = nCountPis;
     if ( pnCountRegs )
@@ -354,11 +357,11 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC
     {
         pObj = Aig_ManPi(pAig, nOffset+iOut);
         pObj->pData = Aig_ObjCreatePi(pNew);
-        Aig_ObjCreatePo( pNew, pObj->pData );
+        Aig_ObjCreatePo( pNew, (Aig_Obj_t *)pObj->pData );
         Aig_ObjSetTravIdCurrent( pAig, pObj ); // added
     }
     // create the nodes
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         if ( Aig_ObjIsNode(pObj) )
             pObj->pData = Aig_And(pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
     // add real POs for the registers
@@ -377,9 +380,9 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC
         // map constant nodes
         pMapBack[0] = 0;
         // logic cones of register outputs
-        Vec_PtrForEachEntry( vNodes, pObj, i )
+        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         {
-            pObjNew = Aig_Regular(pObj->pData);
+            pObjNew = Aig_Regular((Aig_Obj_t *)pObj->pData);
             pMapBack[pObjNew->Id] = pObj->Id;
         }
         // map register outputs
@@ -387,7 +390,7 @@ Aig_Man_t * Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnC
         Vec_IntForEachEntry( vPart, iOut, i )
         {
             pObj = Aig_ManPi(pAig, nOffset+iOut);
-            pObjNew = pObj->pData;
+            pObjNew = (Aig_Obj_t *)pObj->pData;
             pMapBack[pObjNew->Id] = pObj->Id;
         }
         *ppMapBack = pMapBack;
@@ -441,7 +444,7 @@ Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize )
 //printf( "Part %3d  Reg %3d : Free = %4d. Total = %4d. Ratio = %6.2f. Unique = %4d.\n", i, k, 
 //                Vec_IntSize(p->vFreeVars), Vec_IntSize(p->vRegs), 
 //                1.0*Vec_IntSize(p->vFreeVars)/Vec_IntSize(p->vRegs), Vec_IntSize(p->vUniques) );
-            // quit if there are not ABC_FREE variables
+            // quit if there are not free variables
             if ( Vec_IntSize(p->vFreeVars) == 0 )
                 break;
         }
@@ -622,3 +625,5 @@ Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigPartSat.c b/src/aig/aig/aigPartSat.c
index a8c9008f..3d9152ae 100644
--- a/src/aig/aig/aigPartSat.c
+++ b/src/aig/aig/aigPartSat.c
@@ -22,6 +22,9 @@
 #include "satSolver.h"
 #include "cnf.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /* 
 
 The node partitioners defined in this file return array of intergers 
@@ -80,7 +83,7 @@ Vec_Int_t * Aig_ManPartitionLevelized( Aig_Man_t * p, int nPartSize )
     int i, k, Counter = 0;
     vNodes = Aig_ManLevelize( p );
     vId2Part = Vec_IntStart( Aig_ManObjNumMax(p) );
-    Vec_VecForEachEntryReverseReverse( vNodes, pObj, i, k )
+    Vec_VecForEachEntryReverseReverse( Aig_Obj_t *, vNodes, pObj, i, k )
         Vec_IntWriteEntry( vId2Part, Aig_ObjId(pObj), Counter++/nPartSize );
     Vec_VecFree( vNodes );
     return vId2Part;
@@ -107,13 +110,13 @@ Vec_Int_t * Aig_ManPartitionDfs( Aig_Man_t * p, int nPartSize, int fPreorder )
     if ( fPreorder )
     {
         vNodes = Aig_ManDfsPreorder( p, 1 );
-        Vec_PtrForEachEntry( vNodes, pObj, i )
+        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
             Vec_IntWriteEntry( vId2Part, Aig_ObjId(pObj), Counter++/nPartSize );
     }
     else
     {
         vNodes = Aig_ManDfs( p, 1 );
-        Vec_PtrForEachEntryReverse( vNodes, pObj, i )
+        Vec_PtrForEachEntryReverse( Aig_Obj_t *, vNodes, pObj, i )
             Vec_IntWriteEntry( vId2Part, Aig_ObjId(pObj), Counter++/nPartSize );
     }
     Vec_PtrFree( vNodes );
@@ -179,7 +182,7 @@ Aig_Man_t * Aig_ManPartSplitOne( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Int_t **
     int i;
     // mark these nodes
     Aig_ManIncrementTravId( p );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
     {
         Aig_ObjSetTravIdCurrent( p, pObj );
         pObj->pData = NULL;
@@ -187,14 +190,14 @@ Aig_Man_t * Aig_ManPartSplitOne( Aig_Man_t * p, Vec_Ptr_t * vNodes, Vec_Int_t **
     // add these nodes in a DFS order
     pNew = Aig_ManStart( Vec_PtrSize(vNodes) );
     vPio2Id = Vec_IntAlloc( 100 );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         Aig_ManPartSplitOne_rec( pNew, p, pObj, vPio2Id );
     // add the POs
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        if ( Aig_ObjRefs(pObj->pData) != Aig_ObjRefs(pObj) )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+        if ( Aig_ObjRefs((Aig_Obj_t *)pObj->pData) != Aig_ObjRefs(pObj) )
         {
-            assert( Aig_ObjRefs(pObj->pData) < Aig_ObjRefs(pObj) );
-            Aig_ObjCreatePo( pNew, pObj->pData );
+            assert( Aig_ObjRefs((Aig_Obj_t *)pObj->pData) < Aig_ObjRefs(pObj) );
+            Aig_ObjCreatePo( pNew, (Aig_Obj_t *)pObj->pData );
             Vec_IntPush( vPio2Id, Aig_ObjId(pObj) );
         }
     assert( Aig_ManNodeNum(pNew) == Vec_PtrSize(vNodes) );
@@ -440,7 +443,7 @@ int Aig_ManAddNewCnfToSolver( sat_solver * pSat, Aig_Man_t * pAig, Vec_Int_t * v
     // remove the CNF
     Cnf_DataFree( pCnf );
     // constrain the solver with the literals corresponding to the original POs
-    Vec_PtrForEachEntry( vPartPos, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vPartPos, pObj, i )
     {
         iNodeIdOld = Aig_ObjFaninId0( pObj );
         iSatVarOld = Vec_IntEntry( vNode2Var, iNodeIdOld );
@@ -537,7 +540,7 @@ int Aig_ManPartitionedSat( Aig_Man_t * p, int nAlgo, int nPartSize,
 
     // synthesize partitions
     if ( fSynthesize )
-    Vec_PtrForEachEntry( vAigs, pAig, i )
+    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig, i )
     {
         pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 );
         Vec_PtrWriteEntry( vAigs, i, pAig );
@@ -551,17 +554,17 @@ int Aig_ManPartitionedSat( Aig_Man_t * p, int nAlgo, int nPartSize,
     vNode2Var = Vec_IntStart( Aig_ManObjNumMax(p) );
 
     // add partitions, one at a time, and run the SAT solver 
-    Vec_PtrForEachEntry( vAigs, pAig, i )
+    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig, i )
     {
 clk = clock();
         // transform polarity of the AIG
         if ( fAlignPol )
-            Aig_ManPartSetNodePolarity( p, pAig, Vec_VecEntry(vPio2Id,i) );
+            Aig_ManPartSetNodePolarity( p, pAig, (Vec_Int_t *)Vec_VecEntry(vPio2Id,i) );
         else
             Aig_ManPartResetNodePolarity( pAig );
         // add CNF of this partition to the SAT solver
         if ( Aig_ManAddNewCnfToSolver( pSat, pAig, vNode2Var, 
-            Vec_VecEntry(vPio2Id,i), Vec_VecEntry(vPart2Pos,i), fAlignPol ) )
+            (Vec_Int_t *)Vec_VecEntry(vPio2Id,i), (Vec_Ptr_t *)Vec_VecEntry(vPart2Pos,i), fAlignPol ) )
         {
             RetValue = 1;
             break;
@@ -596,7 +599,7 @@ ABC_PRT( "Time", clock() - clk );
         Aig_ManDeriveCounterExample( p, vNode2Var, pSat );
     // cleanup
     sat_solver_delete( pSat );
-    Vec_PtrForEachEntry( vAigs, pTemp, i )
+    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
         Aig_ManStop( pTemp );
     Vec_PtrFree( vAigs );
     Vec_VecFree( vPio2Id );
@@ -610,3 +613,5 @@ ABC_PRT( "Time", clock() - clk );
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 2d2f2f3d..9966174f 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -188,8 +191,8 @@ static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t * pRepr;
     if ( (pRepr = Aig_ObjFindRepr(p, pObj)) )
-        return Aig_NotCond( pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
-    return pObj->pData;
+        return Aig_NotCond( (Aig_Obj_t *)pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
+    return (Aig_Obj_t *)pObj->pData;
 }
 static inline Aig_Obj_t * Aig_ObjChild0Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjGetRepr(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) ); }
 static inline Aig_Obj_t * Aig_ObjChild1Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_NotCond( Aig_ObjGetRepr(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) ); }
@@ -221,7 +224,7 @@ void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * pOld )
     // go through the nodes which have representatives
     Aig_ManForEachObj( pOld, pObj, k )
         if ( (pRepr = Aig_ObjFindRepr(pOld, pObj)) )
-            Aig_ObjSetRepr_( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) ); 
+            Aig_ObjSetRepr_( pNew, Aig_Regular((Aig_Obj_t *)pRepr->pData), Aig_Regular((Aig_Obj_t *)pObj->pData) ); 
 }
 
 /**Function*************************************************************
@@ -239,15 +242,15 @@ Aig_Obj_t * Aig_ManDupRepr_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pOb
 {
     Aig_Obj_t * pRepr;
     if ( pObj->pData )
-        return pObj->pData;
+        return (Aig_Obj_t *)pObj->pData;
     if ( (pRepr = Aig_ObjFindRepr(p, pObj)) )
     {
         Aig_ManDupRepr_rec( pNew, p, pRepr );
-        return pObj->pData = Aig_NotCond( pRepr->pData, pRepr->fPhase ^ pObj->fPhase );
+        return (Aig_Obj_t *)(pObj->pData = Aig_NotCond( (Aig_Obj_t *)pRepr->pData, pRepr->fPhase ^ pObj->fPhase ));
     }
     Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin0(pObj) );
     Aig_ManDupRepr_rec( pNew, p, Aig_ObjFanin1(pObj) );
-    return pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) );
+    return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Repr(p, pObj), Aig_ObjChild1Repr(p, pObj) ));
 }
 
 /**Function*************************************************************
@@ -270,6 +273,7 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // map the const and primary inputs
@@ -327,7 +331,7 @@ Aig_Man_t * Aig_ManDupReprBasic( Aig_Man_t * p )
     Aig_ManSeqCleanupBasic( pNew );
     // remove pointers to the dead nodes
     Aig_ManForEachObj( p, pObj, i )
-        if ( pObj->pData && Aig_ObjIsNone(pObj->pData) )
+        if ( pObj->pData && Aig_ObjIsNone((Aig_Obj_t *)pObj->pData) )
             pObj->pData = NULL;
     return pNew;
 }
@@ -550,3 +554,5 @@ int Aig_TransferMappedClasses( Aig_Man_t * pAig, Aig_Man_t * pPart, int * pMapBa
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c
index 6dea6503..f7774d22 100644
--- a/src/aig/aig/aigRet.c
+++ b/src/aig/aig/aigRet.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -76,28 +79,28 @@ static inline Rtm_Obj_t * Rtm_ObjFanout( Rtm_Obj_t * pObj, int i )       { retur
 static inline Rtm_Edg_t * Rtm_ObjEdge( Rtm_Obj_t * pObj, int i )         { return (Rtm_Edg_t *)(pObj->pFanio + 2*i + 1);              }
 static inline Rtm_Edg_t * Rtm_ObjFanoutEdge( Rtm_Obj_t * pObj, int i )   { return (Rtm_Edg_t *)pObj->pFanio[2*(pObj->nFanins+i) + 1]; }
 
-static inline Rtm_Init_t  Rtm_InitNot( Rtm_Init_t Val )                  { if ( Val == RTM_VAL_ZERO ) return RTM_VAL_ONE; if ( Val == RTM_VAL_ONE ) return RTM_VAL_ZERO; assert( 0 ); return -1; }
+static inline Rtm_Init_t  Rtm_InitNot( Rtm_Init_t Val )                  { if ( Val == RTM_VAL_ZERO ) return (Rtm_Init_t)RTM_VAL_ONE; if ( Val == RTM_VAL_ONE ) return (Rtm_Init_t)RTM_VAL_ZERO; assert( 0 ); return (Rtm_Init_t)-1; }
 static inline Rtm_Init_t  Rtm_InitNotCond( Rtm_Init_t Val, int c )       { return c ? Rtm_InitNot(Val) : Val;                         }
-static inline Rtm_Init_t  Rtm_InitAnd(Rtm_Init_t ValA, Rtm_Init_t ValB ) { if ( ValA == RTM_VAL_ONE && ValB == RTM_VAL_ONE ) return RTM_VAL_ONE;  if ( ValA == RTM_VAL_ZERO || ValB == RTM_VAL_ZERO ) return RTM_VAL_ZERO; assert( 0 ); return -1;   }
+static inline Rtm_Init_t  Rtm_InitAnd(Rtm_Init_t ValA, Rtm_Init_t ValB ) { if ( ValA == RTM_VAL_ONE && ValB == RTM_VAL_ONE ) return (Rtm_Init_t)RTM_VAL_ONE;  if ( ValA == RTM_VAL_ZERO || ValB == RTM_VAL_ZERO ) return (Rtm_Init_t)RTM_VAL_ZERO; assert( 0 ); return (Rtm_Init_t)-1;   }
 
 static inline int         Rtm_InitWordsNum( int nLats )                  { return (nLats >> 4) + ((nLats & 15) > 0); }
 static inline int         Rtm_InitGetTwo( unsigned * p, int i )          { return (p[i>>4] >> ((i & 15)<<1)) & 3;    }
 static inline void        Rtm_InitSetTwo( unsigned * p, int i, int val ) { p[i>>4] |= (val << ((i & 15)<<1));        }
 static inline void        Rtm_InitXorTwo( unsigned * p, int i, int val ) { p[i>>4] ^= (val << ((i & 15)<<1));        }
 
-static inline Rtm_Init_t  Rtm_ObjGetFirst1( Rtm_Edg_t * pEdge )          { return pEdge->LData & 3;                                    }
-static inline Rtm_Init_t  Rtm_ObjGetLast1( Rtm_Edg_t * pEdge )           { return (pEdge->LData >> ((pEdge->nLats-1)<<1)) & 3;         }
-static inline Rtm_Init_t  Rtm_ObjGetOne1( Rtm_Edg_t * pEdge, int i )     { assert( i < (int)pEdge->nLats ); return (pEdge->LData >> (i << 1)) & 3;  }
-static inline Rtm_Init_t  Rtm_ObjRemFirst1( Rtm_Edg_t * pEdge )          { int Val = pEdge->LData & 3; pEdge->LData >>= 2; assert(pEdge->nLats > 0); pEdge->nLats--; return Val;  }
-static inline Rtm_Init_t  Rtm_ObjRemLast1( Rtm_Edg_t * pEdge )           { int Val = (pEdge->LData >> ((pEdge->nLats-1)<<1)) & 3; pEdge->LData ^= Val << ((pEdge->nLats-1)<<1); assert(pEdge->nLats > 0); pEdge->nLats--; return Val;  }
+static inline Rtm_Init_t  Rtm_ObjGetFirst1( Rtm_Edg_t * pEdge )          { return (Rtm_Init_t)(pEdge->LData & 3);                                    }
+static inline Rtm_Init_t  Rtm_ObjGetLast1( Rtm_Edg_t * pEdge )           { return (Rtm_Init_t)((pEdge->LData >> ((pEdge->nLats-1)<<1)) & 3);         }
+static inline Rtm_Init_t  Rtm_ObjGetOne1( Rtm_Edg_t * pEdge, int i )     { assert( i < (int)pEdge->nLats ); return (Rtm_Init_t)((pEdge->LData >> (i << 1)) & 3);  }
+static inline Rtm_Init_t  Rtm_ObjRemFirst1( Rtm_Edg_t * pEdge )          { int Val = pEdge->LData & 3; pEdge->LData >>= 2; assert(pEdge->nLats > 0); pEdge->nLats--; return (Rtm_Init_t)Val;  }
+static inline Rtm_Init_t  Rtm_ObjRemLast1( Rtm_Edg_t * pEdge )           { int Val = (pEdge->LData >> ((pEdge->nLats-1)<<1)) & 3; pEdge->LData ^= Val << ((pEdge->nLats-1)<<1); assert(pEdge->nLats > 0); pEdge->nLats--; return (Rtm_Init_t)Val;  }
 static inline void        Rtm_ObjAddFirst1( Rtm_Edg_t * pEdge, Rtm_Init_t Val ) { assert( Val > 0 && Val < 4 ); pEdge->LData = (pEdge->LData << 2) | Val;  pEdge->nLats++;   }
 static inline void        Rtm_ObjAddLast1( Rtm_Edg_t * pEdge, Rtm_Init_t Val )  { assert( Val > 0 && Val < 4 ); pEdge->LData |= Val << (pEdge->nLats<<1);  pEdge->nLats++;   }
 
-static inline Rtm_Init_t  Rtm_ObjGetFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                 { return Rtm_InitGetTwo( p->pExtra + pEdge->LData, 0 );                }
-static inline Rtm_Init_t  Rtm_ObjGetLast2( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                  { return Rtm_InitGetTwo( p->pExtra + pEdge->LData, pEdge->nLats - 1 ); }
-static inline Rtm_Init_t  Rtm_ObjGetOne2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, int i )            { return Rtm_InitGetTwo( p->pExtra + pEdge->LData, i );                }
+static inline Rtm_Init_t  Rtm_ObjGetFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                 { return (Rtm_Init_t)Rtm_InitGetTwo( p->pExtra + pEdge->LData, 0 );                }
+static inline Rtm_Init_t  Rtm_ObjGetLast2( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                  { return (Rtm_Init_t)Rtm_InitGetTwo( p->pExtra + pEdge->LData, pEdge->nLats - 1 ); }
+static inline Rtm_Init_t  Rtm_ObjGetOne2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, int i )            { return (Rtm_Init_t)Rtm_InitGetTwo( p->pExtra + pEdge->LData, i );                }
 static        Rtm_Init_t  Rtm_ObjRemFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge );
-static inline Rtm_Init_t  Rtm_ObjRemLast2( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                  { Rtm_Init_t Val = Rtm_ObjGetLast2( p, pEdge );    Rtm_InitXorTwo( p->pExtra + pEdge->LData, pEdge->nLats - 1, Val ); pEdge->nLats--; return Val; }
+static inline Rtm_Init_t  Rtm_ObjRemLast2( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                  { Rtm_Init_t Val = Rtm_ObjGetLast2( p, pEdge );    Rtm_InitXorTwo( p->pExtra + pEdge->LData, pEdge->nLats - 1, Val ); pEdge->nLats--; return (Rtm_Init_t)Val; }
 static        void        Rtm_ObjAddFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val );
 static inline void        Rtm_ObjAddLast2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val )  { Rtm_InitSetTwo( p->pExtra + pEdge->LData, pEdge->nLats, Val );  pEdge->nLats++;  }
 
@@ -116,13 +119,13 @@ static        void        Rtm_ObjAddLast( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_
 
 // iterator over the primary inputs
 #define Rtm_ManForEachPi( p, pObj, i )                                          \
-    Vec_PtrForEachEntry( p->vPis, pObj, i )
+    Vec_PtrForEachEntry( Rtm_Obj_t *, p->vPis, pObj, i )
 // iterator over the primary outputs
 #define Rtm_ManForEachPo( p, pObj, i )                                          \
-    Vec_PtrForEachEntry( p->vPos, pObj, i )
+    Vec_PtrForEachEntry( Rtm_Obj_t *, p->vPos, pObj, i )
 // iterator over all objects, including those currently not used
 #define Rtm_ManForEachObj( p, pObj, i )                                         \
-    Vec_PtrForEachEntry( p->vObjs, pObj, i ) 
+    Vec_PtrForEachEntry( Rtm_Obj_t *, p->vObjs, pObj, i ) 
 // iterate through the fanins
 #define Rtm_ObjForEachFanin( pObj, pFanin, i )                                  \
     for ( i = 0; i < (int)(pObj)->nFanins && ((pFanin = Rtm_ObjFanin(pObj, i)), 1); i++ )
@@ -222,11 +225,11 @@ void Rtm_ObjTransferToBigger( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
 ***********************************************************************/
 Rtm_Init_t  Rtm_ObjRemFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge )                 
 { 
-    Rtm_Init_t Val = 0, Temp;   
+    Rtm_Init_t Val = (Rtm_Init_t)0, Temp;   
     unsigned * pB = p->pExtra + pEdge->LData, * pE = pB + Rtm_InitWordsNum( pEdge->nLats-- ) - 1;  
     while ( pE >= pB ) 
     {
-        Temp = *pE & 3;
+        Temp = (Rtm_Init_t)(*pE & 3);
         *pE = (*pE >> 2) | (Val << 30);
         Val = Temp;
         pE--;
@@ -253,7 +256,7 @@ void Rtm_ObjAddFirst2( Rtm_Man_t * p, Rtm_Edg_t * pEdge, Rtm_Init_t Val )
     assert( Val != 0 );
     while ( pB < pE ) 
     {
-        Temp = *pB >> 30;
+        Temp = (Rtm_Init_t)(*pB >> 30);
         *pB = (*pB << 2) | Val;
         Val = Temp;
         pB++;
@@ -590,7 +593,7 @@ int Rtm_ManMarkAutoFwd( Rtm_Man_t * pRtm )
     Rtm_Obj_t * pObjRtm;
     int i, Counter = 0;
     // mark nodes reachable from the PIs
-    pObjRtm = Vec_PtrEntry( pRtm->vObjs, 0 );
+    pObjRtm = (Rtm_Obj_t *)Vec_PtrEntry( pRtm->vObjs, 0 );
     Rtm_ObjMarkAutoFwd_rec( pObjRtm );
     Rtm_ManForEachPi( pRtm, pObjRtm, i )
         Rtm_ObjMarkAutoFwd_rec( pObjRtm );
@@ -642,7 +645,7 @@ int Rtm_ManMarkAutoBwd( Rtm_Man_t * pRtm )
     Rtm_Obj_t * pObjRtm;
     int i, Counter = 0;
     // mark nodes reachable from the PIs
-    pObjRtm = Vec_PtrEntry( pRtm->vObjs, 0 );
+    pObjRtm = (Rtm_Obj_t *)Vec_PtrEntry( pRtm->vObjs, 0 );
     pObjRtm->fAuto = 1;
     Rtm_ManForEachPi( pRtm, pObjRtm, i )
         pObjRtm->fAuto = 1;
@@ -699,15 +702,15 @@ Rtm_Man_t * Rtm_ManFromAig( Aig_Man_t * p )
         pObj->pData = Rtm_ObjAlloc( pRtm, 2, pObj->nRefs );
     // connect objects
     Aig_ManForEachPoSeq( p, pObj, i )
-        Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        Rtm_ObjAddFanin( (Rtm_Obj_t *)pObj->pData, (Rtm_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
     Aig_ManForEachLiSeq( p, pObj, i )
-        Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        Rtm_ObjAddFanin( (Rtm_Obj_t *)pObj->pData, (Rtm_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
     Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
-        Rtm_ObjAddFanin( pObjLo->pData, pObjLi->pData, 0 );
+        Rtm_ObjAddFanin( (Rtm_Obj_t *)pObjLo->pData, (Rtm_Obj_t *)pObjLi->pData, 0 );
     Aig_ManForEachNode( p, pObj, i )
     {
-        Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
-        Rtm_ObjAddFanin( pObj->pData, Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
+        Rtm_ObjAddFanin( (Rtm_Obj_t *)pObj->pData, (Rtm_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        Rtm_ObjAddFanin( (Rtm_Obj_t *)pObj->pData, (Rtm_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
     }
     return pRtm;
 }
@@ -729,7 +732,7 @@ Aig_Obj_t * Rtm_ManToAig_rec( Aig_Man_t * pNew, Rtm_Man_t * pRtm, Rtm_Obj_t * pO
     Aig_Obj_t * pRes, * pFanin;
     int k, Val;
     if ( pObjRtm->pCopy )
-        return pObjRtm->pCopy;
+        return (Aig_Obj_t *)pObjRtm->pCopy;
     // get the inputs
     pRes = Aig_ManConst1( pNew );
     Rtm_ObjForEachFaninEdge( pObjRtm, pEdge, k )
@@ -745,7 +748,7 @@ Aig_Obj_t * Rtm_ManToAig_rec( Aig_Man_t * pNew, Rtm_Man_t * pRtm, Rtm_Obj_t * pO
         pFanin = Aig_NotCond( pFanin, k ? pObjRtm->fCompl1 : pObjRtm->fCompl0 );
         pRes = Aig_And( pNew, pRes, pFanin );
     }
-    return pObjRtm->pCopy = pRes;
+    return (Aig_Obj_t *)(pObjRtm->pCopy = pRes);
 }
 
 /**Function*************************************************************
@@ -778,7 +781,7 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm )
     // create the new manager
     pNew = Aig_ManStart( Vec_PtrSize(pRtm->vObjs) + nLatches );
     // create PIs/POs and latches
-    pObjRtm = Vec_PtrEntry( pRtm->vObjs, 0 );
+    pObjRtm = (Rtm_Obj_t *)Vec_PtrEntry( pRtm->vObjs, 0 );
     pObjRtm->pCopy = Aig_ManConst1(pNew);
     Rtm_ManForEachPi( pRtm, pObjRtm, i )
         pObjRtm->pCopy = Aig_ObjCreatePi(pNew);
@@ -789,14 +792,14 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm )
         Rtm_ManToAig_rec( pNew, pRtm, pObjRtm, pLatches );
     // create POs
     Rtm_ManForEachPo( pRtm, pObjRtm, i )
-        Aig_ObjCreatePo( pNew, pObjRtm->pCopy );
+        Aig_ObjCreatePo( pNew, (Aig_Obj_t *)pObjRtm->pCopy );
     // connect latches 
     Rtm_ManForEachObj( pRtm, pObjRtm, i )
     Rtm_ObjForEachFaninEdge( pObjRtm, pEdge, k )
     {
         if ( pEdge->nLats == 0 )
             continue;
-        pObjNew = Rtm_ObjFanin( pObjRtm, k )->pCopy;
+        pObjNew = (Aig_Obj_t *)Rtm_ObjFanin( pObjRtm, k )->pCopy;
         for ( m = 0; m < (int)pEdge->nLats; m++ )
         {
             Val = Rtm_ObjGetOne( pRtm, pEdge, pEdge->nLats - 1 - m );
@@ -843,7 +846,7 @@ clk = clock();
     pRtm = Rtm_ManFromAig( p );
     // set registers
     Aig_ManForEachLoSeq( p, pObjAig, i )
-        Rtm_ObjAddFirst( pRtm, Rtm_ObjEdge(pObjAig->pData, 0), fForward? RTM_VAL_ZERO : RTM_VAL_VOID );
+        Rtm_ObjAddFirst( pRtm, Rtm_ObjEdge((Rtm_Obj_t *)pObjAig->pData, 0), fForward? RTM_VAL_ZERO : RTM_VAL_VOID );
     // detect and mark the autonomous components
     if ( fForward )
         nAutos = Rtm_ManMarkAutoFwd( pRtm );
@@ -870,7 +873,7 @@ clk = clock();
     {
         Aig_ManForEachLoSeq( p, pObjAig, i )
         {
-            pObj = pObjAig->pData;
+            pObj = (Rtm_Obj_t *)pObjAig->pData;
             if ( pObj->fAuto )
                 continue;
             pObj->fMark = 1;
@@ -881,7 +884,7 @@ clk = clock();
     {
         Aig_ManForEachLiSeq( p, pObjAig, i )
         {
-            pObj = pObjAig->pData;
+            pObj = (Rtm_Obj_t *)pObjAig->pData;
             if ( pObj->fAuto )
                 continue;
             pObj->fMark = 1;
@@ -890,7 +893,7 @@ clk = clock();
     }
     // perform retiming 
     DegreeMax = 0;
-    Vec_PtrForEachEntry( vQueue, pObj, i )
+    Vec_PtrForEachEntry( Rtm_Obj_t *, vQueue, pObj, i )
     {
         pObj->fMark = 0;
         // retime the node 
@@ -968,3 +971,5 @@ clk = clock();
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigRetF.c b/src/aig/aig/aigRetF.c
index f045cac8..0a866c30 100644
--- a/src/aig/aig/aigRetF.c
+++ b/src/aig/aig/aigRetF.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -207,3 +210,5 @@ Aig_Man_t * Aig_ManRetimeFrontier( Aig_Man_t * p, int nStepsMax )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index b6331b0e..e31ab74b 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -50,6 +53,7 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
+    pNew->nConstrs = p->nConstrs;
     assert( p->vFlopNums == NULL || Vec_IntSize(p->vFlopNums) == p->nRegs );
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -69,8 +73,8 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
     }
     Aig_ManForEachPi( p, pObj, i )
     {
-        pObjMapped = Vec_PtrEntry( vMap, i );
-        pObj->pData = Aig_NotCond( Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) );
+        pObjMapped = (Aig_Obj_t *)Vec_PtrEntry( vMap, i );
+        pObj->pData = Aig_NotCond( (Aig_Obj_t *)Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) );
         if ( pNew->vFlopReprs && i >= nTruePis && pObj != pObjMapped )
         {
             Vec_IntPush( pNew->vFlopReprs, Aig_ObjPioNum(pObj) );
@@ -172,7 +176,7 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
     Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
         pObjLo->pNext = pObjLi;
     // mark the nodes reachable from these nodes
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         Aig_ManSeqCleanup_rec( p, pObj, vNodes );
     assert( Vec_PtrSize(vNodes) <= Aig_ManPoNum(p) );
     // clean latch output pointers
@@ -271,7 +275,7 @@ int Aig_ManSeqCleanupBasic( Aig_Man_t * p )
     Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
         pObjLo->pNext = pObjLi;
     // mark the nodes reachable from these nodes
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         Aig_ManSeqCleanup_rec( p, pObj, vNodes );
     assert( Vec_PtrSize(vNodes) <= Aig_ManPoNum(p) );
     // clean latch output pointers
@@ -496,7 +500,7 @@ void Aig_ManComputeSccs( Aig_Man_t * p )
     vSupports = Aig_ManSupports( p );
     // transforms the supports into the latch dependency matrix
     vMatrix = Vec_PtrStart( Aig_ManRegNum(p) );
-    Vec_PtrForEachEntry( vSupports, vSupp, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vSupports, vSupp, i )
     {
         // skip true POs
         iOut = Vec_IntPop( vSupp );
@@ -522,11 +526,11 @@ void Aig_ManComputeSccs( Aig_Man_t * p )
     vMatrix2 = Vec_PtrAlloc( Aig_ManRegNum(p) );
     for ( i = 0; i < Aig_ManRegNum(p); i++ )
         Vec_PtrPush( vMatrix2, Vec_IntAlloc(8) );
-    Vec_PtrForEachEntry( vMatrix, vSupp, i )
+    Vec_PtrForEachEntry( Vec_Int_t *, vMatrix, vSupp, i )
     {
         Vec_IntForEachEntry( vSupp, iIn, k )
         {
-            vSupp2 = Vec_PtrEntry( vMatrix2, iIn );
+            vSupp2 = (Vec_Int_t *)Vec_PtrEntry( vMatrix2, iIn );
             Vec_IntPush( vSupp2, i );
         }
     } 
@@ -548,7 +552,7 @@ void Aig_ManComputeSccs( Aig_Man_t * p )
         Vec_IntPush( vComp, iOut );
         Vec_IntForEachEntry( vComp, iOut, i )
         {
-            vSupp = Vec_PtrEntry( vMatrix, iOut );
+            vSupp = (Vec_Int_t *)Vec_PtrEntry( vMatrix, iOut );
             Vec_IntForEachEntry( vSupp, iIn, k )
             {
                 if ( pVarsTot[iIn] )
@@ -556,7 +560,7 @@ void Aig_ManComputeSccs( Aig_Man_t * p )
                 pVarsTot[iIn] = 1;
                 Vec_IntPush( vComp, iIn );
             }
-            vSupp2 = Vec_PtrEntry( vMatrix2, iOut );
+            vSupp2 = (Vec_Int_t *)Vec_PtrEntry( vMatrix2, iOut );
             Vec_IntForEachEntry( vSupp2, iIn, k )
             {
                 if ( pVarsTot[iIn] )
@@ -602,14 +606,14 @@ Aig_Man_t * Aig_ManSclPart( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual,
     if ( pAig->vClockDoms ) 
     {
         vResult = Vec_PtrAlloc( 100 );
-        Vec_PtrForEachEntry( (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
+        Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
             Vec_PtrPush( vResult, Vec_IntDup(vPart) );
     } 
     else
         vResult = Aig_ManRegPartitionSimple( pAig, 0, 0 );
 
     Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
-    Vec_PtrForEachEntry( vResult, vPart, i ) 
+    Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i ) 
     {
         pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
         Aig_ManSetRegNum( pTemp, pTemp->nRegs );
@@ -699,3 +703,5 @@ Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigShow.c b/src/aig/aig/aigShow.c
index 1e9e10ac..24b122c3 100644
--- a/src/aig/aig/aigShow.c
+++ b/src/aig/aig/aigShow.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -59,7 +62,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
 
     // mark the nodes
     if ( vBold )
-        Vec_PtrForEachEntry( vBold, pNode, i )
+        Vec_PtrForEachEntry( Aig_Obj_t *, vBold, pNode, i )
             pNode->fMarkB = 1;
 
     // compute levels
@@ -308,7 +311,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t *
 
     // unmark nodes
     if ( vBold )
-        Vec_PtrForEachEntry( vBold, pNode, i )
+        Vec_PtrForEachEntry( Aig_Obj_t *, vBold, pNode, i )
             pNode->fMarkB = 0;
 
     Aig_ManForEachPo( pMan, pNode, i )
@@ -354,3 +357,5 @@ void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigSplit.c b/src/aig/aig/aigSplit.c
new file mode 100644
index 00000000..51b4f982
--- /dev/null
+++ b/src/aig/aig/aigSplit.c
@@ -0,0 +1,316 @@
+/**CFile****************************************************************
+
+  FileName    [aigSplit.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Splits the property output cone into a set of cofactor properties.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigSplit.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+#include "saig.h"
+#include "cuddInt.h"
+#include "extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the node to MUXes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Aig_Man_t * pNew, st_table * tBdd2Node )
+{
+    Aig_Obj_t * pNode, * pNode0, * pNode1, * pNodeC;
+    assert( !Cudd_IsComplement(bFunc) );
+    if ( st_lookup( tBdd2Node, (char *)bFunc, (char **)&pNode ) )
+        return pNode;
+    // solve for the children nodes
+    pNode0 = Aig_NodeBddToMuxes_rec( dd, Cudd_Regular(cuddE(bFunc)), pNew, tBdd2Node );
+    pNode0 = Aig_NotCond( pNode0, Cudd_IsComplement(cuddE(bFunc)) );
+    pNode1 = Aig_NodeBddToMuxes_rec( dd, cuddT(bFunc), pNew, tBdd2Node );
+    if ( !st_lookup( tBdd2Node, (char *)Cudd_bddIthVar(dd, bFunc->index), (char **)&pNodeC ) )
+        assert( 0 );
+    // create the MUX node
+    pNode = Aig_Mux( pNew, pNodeC, pNode1, pNode0 );
+    st_insert( tBdd2Node, (char *)bFunc, (char *)pNode );
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives AIG for the BDDs of the cofactors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManConvertBddsToAigs( Aig_Man_t * p, DdManager * dd, Vec_Ptr_t * vCofs )
+{
+    DdNode * bFunc;
+    st_table * tBdd2Node;
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManCleanData( p );
+    // generate AIG for BDD
+    pNew = Aig_ManStart( Aig_ManObjNum(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    // create the table mapping BDD nodes into the ABC nodes
+    tBdd2Node = st_init_table( st_ptrcmp, st_ptrhash );
+    // add the constant and the elementary vars
+    st_insert( tBdd2Node, (char *)Cudd_ReadOne(dd), (char *)Aig_ManConst1(pNew) );
+    Aig_ManForEachPi( p, pObj, i )
+        st_insert( tBdd2Node, (char *)Cudd_bddIthVar(dd, i), (char *)pObj->pData );
+    // build primary outputs for the cofactors
+    Vec_PtrForEachEntry( DdNode *, vCofs, bFunc, i )
+    {
+        if ( bFunc == Cudd_ReadLogicZero(dd) )
+            continue;
+        pObj = Aig_NodeBddToMuxes_rec( dd, Cudd_Regular(bFunc), pNew, tBdd2Node );
+        pObj = Aig_NotCond( pObj, Cudd_IsComplement(bFunc) );
+        Aig_ObjCreatePo( pNew, pObj );
+    }
+    st_free_table( tBdd2Node );
+
+    // duplicate the rest of the AIG
+    // add the POs
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        if ( i == 0 )
+            continue;
+        Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );
+        pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    }
+    Aig_ManCleanup( pNew );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManConvertBddsToAigs(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of constraint candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Aig_ManBuildPoBdd_rec( Aig_Man_t * p, Aig_Obj_t * pObj, DdManager * dd )
+{
+    DdNode * bBdd0, * bBdd1;
+    if ( pObj->pData != NULL )
+        return (DdNode *)pObj->pData;
+    assert( Aig_ObjIsNode(pObj) );
+    bBdd0 = Aig_ManBuildPoBdd_rec( p, Aig_ObjFanin0(pObj), dd ); 
+    bBdd1 = Aig_ManBuildPoBdd_rec( p, Aig_ObjFanin1(pObj), dd ); 
+    bBdd0 = Cudd_NotCond( bBdd0, Aig_ObjFaninC0(pObj) );
+    bBdd1 = Cudd_NotCond( bBdd1, Aig_ObjFaninC1(pObj) );
+    pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );  Cudd_Ref( (DdNode *)pObj->pData );
+    return (DdNode *)pObj->pData;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive BDDs for the cofactors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManCofactorBdds( Aig_Man_t * p, Vec_Ptr_t * vSubset, DdManager * dd, DdNode * bFunc )
+{
+    Vec_Ptr_t * vCofs;
+    DdNode * bCube, * bTemp, * bCof, ** pbVars;
+    int i;
+    vCofs = Vec_PtrAlloc( 100 );
+    pbVars = (DdNode **)Vec_PtrArray(vSubset);
+    for ( i = 0; i < (1 << Vec_PtrSize(vSubset)); i++ )
+    {
+        bCube = Extra_bddBitsToCube( dd, i, Vec_PtrSize(vSubset), pbVars, 1 );  Cudd_Ref( bCube );
+        bCof  = Cudd_Cofactor( dd, bFunc, bCube );        Cudd_Ref( bCof );
+        bCof  = Cudd_bddAnd( dd, bTemp = bCof, bCube );   Cudd_Ref( bCof );
+        Cudd_RecursiveDeref( dd, bTemp );
+        Cudd_RecursiveDeref( dd, bCube );
+        Vec_PtrPush( vCofs, bCof );
+    }
+    return vCofs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Construct BDDs for the primary output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdManager * Aig_ManBuildPoBdd( Aig_Man_t * p, DdNode ** pbFunc )
+{
+    DdManager * dd;
+    Aig_Obj_t * pObj;
+    int i;
+    assert( Saig_ManPoNum(p) == 1 );
+    Aig_ManCleanData( p );
+    dd = Cudd_Init( Aig_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
+    pObj = Aig_ManConst1(p);
+    pObj->pData = Cudd_ReadOne(dd);  Cudd_Ref( (DdNode *)pObj->pData );
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        pObj->pData = Cudd_bddIthVar(dd, i);  Cudd_Ref( (DdNode *)pObj->pData );
+    }
+    pObj = Aig_ManPo( p, 0 );
+    *pbFunc = Aig_ManBuildPoBdd_rec( p, Aig_ObjFanin0(pObj), dd );  Cudd_Ref( *pbFunc );
+    *pbFunc = Cudd_NotCond( *pbFunc, Aig_ObjFaninC0(pObj) );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( pObj->pData )
+            Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+    }
+    Cudd_ReduceHeap( dd,  CUDD_REORDER_SYMM_SIFT, 1 );
+    return dd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Randomly selects a random subset of inputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManVecRandSubset( Vec_Ptr_t * vVec, int nVars )
+{
+    Vec_Ptr_t * vRes;
+    void * pEntry;
+    unsigned Rand; 
+    vRes = Vec_PtrDup(vVec);
+    while ( Vec_PtrSize(vRes) > nVars )
+    {
+        Rand   = Aig_ManRandom( 0 );
+        pEntry = Vec_PtrEntry( vRes, Rand % Vec_PtrSize(vRes) );
+        Vec_PtrRemove( vRes, pEntry );
+    }
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManSplit( Aig_Man_t * p, int nVars, int fVerbose )
+{
+    Aig_Man_t * pRes;
+    Aig_Obj_t * pNode;
+    DdNode * bFunc;
+    DdManager * dd;
+    Vec_Ptr_t * vSupp, * vSubs, * vCofs;
+    int i, clk = clock();
+    if ( Saig_ManPoNum(p) != 1 )
+    {
+        printf( "Currently works only for one primary output.\n" );
+        return NULL;
+    }
+    if ( nVars < 1 )
+    {
+        printf( "The number of cofactoring variables should be a positive number.\n" );
+        return NULL;
+    }
+    if ( nVars > 16 )
+    {
+        printf( "The number of cofactoring variables should be less than 17.\n" );
+        return NULL;
+    }
+    vSupp = Aig_Support( p, Aig_ObjFanin0(Aig_ManPo(p,0)) );
+    if ( Vec_PtrSize(vSupp) == 0 )
+    {
+        printf( "Property output function is a constant.\n" );
+        Vec_PtrFree( vSupp );
+        return NULL;
+    }
+    dd    = Aig_ManBuildPoBdd( p, &bFunc ); // bFunc is referenced
+    if ( fVerbose )
+        printf( "Support =%5d.  BDD size =%6d.  ", Vec_PtrSize(vSupp), Cudd_DagSize(bFunc) );
+    vSubs = Aig_ManVecRandSubset( vSupp, nVars );
+    // replace nodes by their BDD variables
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSubs, pNode, i )
+        Vec_PtrWriteEntry( vSubs, i, pNode->pData );
+    // derive cofactors and functions
+    vCofs = Aig_ManCofactorBdds( p, vSubs, dd, bFunc );
+    pRes  = Aig_ManConvertBddsToAigs( p, dd, vCofs );
+    Vec_PtrFree( vSupp );
+    Vec_PtrFree( vSubs );
+    if ( fVerbose )
+        printf( "Created %d cofactors (out of %d).  ", Saig_ManPoNum(pRes), Vec_PtrSize(vCofs) );
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Time", clock() - clk );
+    // dereference
+    Cudd_RecursiveDeref( dd, bFunc );
+    Vec_PtrForEachEntry( DdNode *, vCofs, bFunc, i )
+        Cudd_RecursiveDeref( dd, bFunc );
+    Vec_PtrFree( vCofs );
+    Extra_StopManager( dd );
+    return pRes;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c
index 81635357..13826065 100644
--- a/src/aig/aig/aigTable.c
+++ b/src/aig/aig/aigTable.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -269,3 +272,5 @@ void Aig_TableClear( Aig_Man_t * p )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigTest.c b/src/aig/aig/aigTest.c
index b97ffb03..42c81c3f 100644
--- a/src/aig/aig/aigTest.c
+++ b/src/aig/aig/aigTest.c
@@ -2,6 +2,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 void Aig_ProcedureTest()
 {
     Aig_Man_t * p;
@@ -32,4 +35,5 @@ void Aig_ProcedureTest()
 
     Aig_ManDumpBlif( p, "aig_test_file.blif", NULL, NULL );
     Aig_ManStop( p );
-}
\ No newline at end of file
+}ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigTiming.c b/src/aig/aig/aigTiming.c
index d0cc99e3..4ea93e29 100644
--- a/src/aig/aig/aigTiming.c
+++ b/src/aig/aig/aigTiming.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -150,7 +153,7 @@ void Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIncrease )
     Vec_IntFill( p->vLevelR, Aig_ManObjNumMax(p), 0 );
     // compute levels in reverse topological order
     vNodes = Aig_ManDfsReverse( p );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
     {
         assert( pObj->fMarkA == 0 );
         Aig_ObjSetReverseLevel( p, pObj, Aig_ObjReverseLevelNew(p, pObj) );
@@ -209,7 +212,7 @@ void Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew )
     Vec_VecPush( p->vLevels, LevelOld, pObjNew );
     pObjNew->fMarkA = 1;
     // recursively update level
-    Vec_VecForEachEntryStart( p->vLevels, pTemp, Lev, k, LevelOld )
+    Vec_VecForEachEntryStart( Aig_Obj_t *, p->vLevels, pTemp, Lev, k, LevelOld )
     {
         pTemp->fMarkA = 0;
         assert( Aig_ObjLevel(pTemp) == Lev );
@@ -261,7 +264,7 @@ void Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew )
     Vec_VecPush( p->vLevels, LevelOld, pObjNew );
     pObjNew->fMarkA = 1;
     // recursively update level
-    Vec_VecForEachEntryStart( p->vLevels, pTemp, Lev, k, LevelOld )
+    Vec_VecForEachEntryStart( Aig_Obj_t *, p->vLevels, pTemp, Lev, k, LevelOld )
     {
         pTemp->fMarkA = 0;
         LevelOld = Aig_ObjReverseLevel(p, pTemp); 
@@ -349,3 +352,5 @@ void Aig_ManVerifyReverseLevel( Aig_Man_t * p )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigTruth.c b/src/aig/aig/aigTruth.c
index a92f9e1d..ddcb8736 100644
--- a/src/aig/aig/aigTruth.c
+++ b/src/aig/aig/aigTruth.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -43,8 +46,8 @@ unsigned * Aig_ManCutTruthOne( Aig_Obj_t * pNode, unsigned * pTruth, int nWords
 {
     unsigned * pTruth0, * pTruth1;
     int i;
-    pTruth0 = Aig_ObjFanin0(pNode)->pData;
-    pTruth1 = Aig_ObjFanin1(pNode)->pData;
+    pTruth0 = (unsigned *)Aig_ObjFanin0(pNode)->pData;
+    pTruth1 = (unsigned *)Aig_ObjFanin1(pNode)->pData;
     if ( Aig_ObjIsExor(pNode) )
         for ( i = 0; i < nWords; i++ )
             pTruth[i] = pTruth0[i] ^ pTruth1[i];
@@ -82,13 +85,13 @@ unsigned * Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t *
     assert( Vec_PtrSize(vNodes) <= Vec_PtrSize(vTruthStore) );
     assert( Vec_PtrSize(vNodes) == 0 || pRoot == Vec_PtrEntryLast(vNodes) );  
     // assign elementary truth tables
-    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
         pObj->pData = Vec_PtrEntry( vTruthElem, i );
     // compute truths for other nodes
     nWords = Aig_TruthWordNum( Vec_PtrSize(vLeaves) );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pData = Aig_ManCutTruthOne( pObj, Vec_PtrEntry(vTruthStore, i), nWords );
-    return pRoot->pData;
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+        pObj->pData = Aig_ManCutTruthOne( pObj, (unsigned *)Vec_PtrEntry(vTruthStore, i), nWords );
+    return (unsigned *)pRoot->pData;
 }
 
 ////////////////////////////////////////////////////////////////////////
@@ -96,3 +99,5 @@ unsigned * Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t *
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c
index 94797210..e3387ad1 100644
--- a/src/aig/aig/aigTsim.c
+++ b/src/aig/aig/aigTsim.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -321,7 +324,7 @@ void Aig_TsiStateOrAll( Aig_Tsi_t * pTsi, unsigned * pState )
 {
     unsigned * pPrev;
     int i, k;
-    Vec_PtrForEachEntry( pTsi->vStates, pPrev, i )
+    Vec_PtrForEachEntry( unsigned *, pTsi->vStates, pPrev, i )
     {
         for ( k = 0; k < pTsi->nWords; k++ )
             pState[k] |= pPrev[k];
@@ -423,7 +426,7 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose )
         return NULL;
     }
     // OR all the states
-    pState = Vec_PtrEntry( pTsi->vStates, 0 );
+    pState = (unsigned *)Vec_PtrEntry( pTsi->vStates, 0 );
     Aig_TsiStateOrAll( pTsi, pState );
     // check if there are constants
     fConstants = 0;
@@ -506,3 +509,5 @@ Aig_Man_t * Aig_ManConstReduce( Aig_Man_t * p, int fVerbose )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index f51b8871..1b97fb2c 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -20,6 +20,8 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -84,6 +86,30 @@ void Aig_ManIncrementTravId( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the time stamp.]
+
+  Description [The file should be closed.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Aig_TimeStamp()
+{
+    static char Buffer[100];
+    char * TimeStamp;
+    time_t ltime;
+    // get the current time
+    time( &ltime );
+    TimeStamp = asctime( localtime( &ltime ) );
+    TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
+    strcpy( Buffer, TimeStamp );
+    return Buffer;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Make sure AIG has not gaps in the numeric order.]
 
   Description []
@@ -548,10 +574,10 @@ void Aig_ObjPrintEqn( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int L
     }
     // AND case
     Vec_VecExpand( vLevels, Level );
-    vSuper = Vec_VecEntry(vLevels, Level);
+    vSuper = (Vec_Ptr_t *)Vec_VecEntry(vLevels, Level);
     Aig_ObjCollectMulti( pObj, vSuper );
     fprintf( pFile, "%s", (Level==0? "" : "(") );
-    Vec_PtrForEachEntry( vSuper, pFanin, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
     {
         Aig_ObjPrintEqn( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 );
         if ( i < Vec_PtrSize(vSuper) - 1 )
@@ -597,10 +623,10 @@ void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, i
     if ( Aig_ObjIsExor(pObj) )
     {
         Vec_VecExpand( vLevels, Level );
-        vSuper = Vec_VecEntry( vLevels, Level );
+        vSuper = (Vec_Ptr_t *)Vec_VecEntry( vLevels, Level );
         Aig_ObjCollectMulti( pObj, vSuper );
         fprintf( pFile, "%s", (Level==0? "" : "(") );
-        Vec_PtrForEachEntry( vSuper, pFanin, i )
+        Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
         {
             Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, (fCompl && i==0)), vLevels, Level+1 );
             if ( i < Vec_PtrSize(vSuper) - 1 )
@@ -635,10 +661,10 @@ void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, i
     }
     // AND case
     Vec_VecExpand( vLevels, Level );
-    vSuper = Vec_VecEntry(vLevels, Level);
+    vSuper = (Vec_Ptr_t *)Vec_VecEntry(vLevels, Level);
     Aig_ObjCollectMulti( pObj, vSuper );
     fprintf( pFile, "%s", (Level==0? "" : "(") );
-    Vec_PtrForEachEntry( vSuper, pFanin, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pFanin, i )
     {
         Aig_ObjPrintVerilog( pFile, Aig_NotCond(pFanin, fCompl), vLevels, Level+1 );
         if ( i < Vec_PtrSize(vSuper) - 1 )
@@ -702,7 +728,7 @@ void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig )
         printf( " %p", pObj );
     printf( "\n" );
     vNodes = Aig_ManDfs( p, 0 );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         Aig_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
     printf( "\n" );
 }
@@ -762,7 +788,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec
         pObj->iData = Counter++;
     Aig_ManForEachPo( p, pObj, i )
         pObj->iData = Counter++;
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         pObj->iData = Counter++;
     nDigits = Aig_Base10Log( Counter );
     // write the file 
@@ -809,7 +835,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec
     if ( pConst1 )
         fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData );
     Aig_ManSetPioNumbers( p );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
     {
         fprintf( pFile, ".names" );
         if ( vPiNames && Aig_ObjIsPi(Aig_ObjFanin0(pObj)) )
@@ -877,7 +903,7 @@ void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName )
         pObj->iData = Counter++;
     Aig_ManForEachPo( p, pObj, i )
         pObj->iData = Counter++;
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         pObj->iData = Counter++;
     nDigits = Aig_Base10Log( Counter );
     // write the file
@@ -911,14 +937,14 @@ void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName )
         fprintf( pFile, "wire n%0*d;\n", nDigits, pObjLi->iData );
     }
     // write nodes
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         fprintf( pFile, "wire n%0*d;\n", nDigits, pObj->iData );
     if ( pConst1 )
         fprintf( pFile, "wire n%0*d;\n", nDigits, pConst1->iData );
     // write nodes
     if ( pConst1 )
         fprintf( pFile, "assign n%0*d = 1\'b1;\n", nDigits, pConst1->iData );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
     {
         fprintf( pFile, "assign n%0*d = %sn%0*d & %sn%0*d;\n", 
             nDigits, pObj->iData,
@@ -1193,7 +1219,7 @@ void Aig_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int
 {
     unsigned * pInfo;
     int i, w;
-    Vec_PtrForEachEntryStart( vInfo, pInfo, i, iInputStart )
+    Vec_PtrForEachEntryStart( unsigned *, vInfo, pInfo, i, iInputStart )
         for ( w = iWordStart; w < iWordStop; w++ )
             pInfo[w] = Aig_ManRandom(0);
 }
@@ -1278,10 +1304,15 @@ void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * v
     assert( vArr->nSize <= vArr2->nSize );
 }
 
+ABC_NAMESPACE_IMPL_END
+
 #include "fra.h"
 #include "saig.h"
 
-extern void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Fra_Cex_t * pCex );
+ABC_NAMESPACE_IMPL_START
+
+
+extern void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Abc_Cex_t * pCex );
 extern void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig );
 extern int Aig_ManCounterExampleValueLookup(  Aig_Man_t * pAig, int Id, int iFrame );
 
@@ -1297,7 +1328,7 @@ extern int Aig_ManCounterExampleValueLookup(  Aig_Man_t * pAig, int Id, int iFra
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Fra_Cex_t * pCex )
+void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Abc_Cex_t * pCex )
 {
     Aig_Obj_t * pObj, * pObjRi, * pObjRo;
     int Val0, Val1, nObjs, i, k, iBit = 0;
@@ -1313,36 +1344,36 @@ void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Fra_Cex_t * pCex )
     for ( i = 0; i <= pCex->iFrame; i++ )
     {
         // set constant 1 node
-        Aig_InfoSetBit( pAig->pData2, nObjs * i + 0 );
+        Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + 0 );
         // set primary inputs according to the counter-example
         Saig_ManForEachPi( pAig, pObj, k )
             if ( Aig_InfoHasBit(pCex->pData, iBit++) )
-                Aig_InfoSetBit( pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
+                Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
         // compute values for each node
         Aig_ManForEachNode( pAig, pObj, k )
         {
-            Val0 = Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
-            Val1 = Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjFaninId1(pObj) );
+            Val0 = Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
+            Val1 = Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId1(pObj) );
             if ( (Val0 ^ Aig_ObjFaninC0(pObj)) & (Val1 ^ Aig_ObjFaninC1(pObj)) )
-                Aig_InfoSetBit( pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
+                Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
         }
         // derive values for combinational outputs
         Aig_ManForEachPo( pAig, pObj, k )
         {
-            Val0 = Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
+            Val0 = Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
             if ( Val0 ^ Aig_ObjFaninC0(pObj) )
-                Aig_InfoSetBit( pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
+                Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
         }
         if ( i == pCex->iFrame )
             continue;
         // transfer values to the register output of the next frame
         Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
-            if ( Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjId(pObjRi) ) )
-                Aig_InfoSetBit( pAig->pData2, nObjs * (i+1) + Aig_ObjId(pObjRo) );
+            if ( Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObjRi) ) )
+                Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * (i+1) + Aig_ObjId(pObjRo) );
     }
     assert( iBit == pCex->nBits );
     // check that the counter-example is correct, that is, the corresponding output is asserted
-    assert( Aig_InfoHasBit( pAig->pData2, nObjs * pCex->iFrame + Aig_ObjId(Aig_ManPo(pAig, pCex->iPo)) ) );
+    assert( Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * pCex->iFrame + Aig_ObjId(Aig_ManPo(pAig, pCex->iPo)) ) );
 }
 
 /**Function*************************************************************
@@ -1379,7 +1410,7 @@ void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig )
 int Aig_ManCounterExampleValueLookup(  Aig_Man_t * pAig, int Id, int iFrame )
 {
     assert( Id >= 0 && Id < Aig_ManObjNum(pAig) );
-    return Aig_InfoHasBit( pAig->pData2, Aig_ManObjNum(pAig) * iFrame + Id );
+    return Aig_InfoHasBit( (unsigned *)pAig->pData2, Aig_ManObjNum(pAig) * iFrame + Id );
 }
 
 /**Function*************************************************************
@@ -1393,7 +1424,7 @@ int Aig_ManCounterExampleValueLookup(  Aig_Man_t * pAig, int Id, int iFrame )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Fra_Cex_t * pCex )
+void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Abc_Cex_t * pCex )
 {
     Aig_Obj_t * pObj = Aig_ManObj( pAig, Aig_ManObjNum(pAig)/2 );
     int iFrame = ABC_MAX( 0, pCex->iFrame - 1 );
@@ -1404,9 +1435,123 @@ void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Fra_Cex_t * pCex )
     Aig_ManCounterExampleValueStop( pAig );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Handle the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManSetPhase( Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    // set the PI simulation information
+    Aig_ManConst1( pAig )->fPhase = 1;
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->fPhase = 0;
+    // simulate internal nodes
+    Aig_ManForEachNode( pAig, pObj, i )
+        pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) )
+                     & ( Aig_ObjFanin1(pObj)->fPhase ^ Aig_ObjFaninC1(pObj) );
+    // simulate PO nodes
+    Aig_ManForEachPo( pAig, pObj, i )
+        pObj->fPhase = Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj);
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects muxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_ManMuxesCollect( Aig_Man_t * pAig )
+{
+    Vec_Ptr_t * vMuxes;
+    Aig_Obj_t * pObj;
+    int i;
+    vMuxes = Vec_PtrAlloc( 100 );
+    Aig_ManForEachNode( pAig, pObj, i )
+        if ( Aig_ObjIsMuxType(pObj) )
+            Vec_PtrPush( vMuxes, pObj );
+    return vMuxes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Dereferences muxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManMuxesDeref( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes )
+{
+    Aig_Obj_t * pObj, * pNodeT, * pNodeE, * pNodeC;
+    int i;
+    Vec_PtrForEachEntry( Aig_Obj_t *, vMuxes, pObj, i )
+    {
+        if ( Aig_ObjRecognizeExor( pObj, &pNodeT, &pNodeE ) )
+        {
+            pNodeT->nRefs--;
+            pNodeE->nRefs--;
+        }
+        else
+        {
+            pNodeC = Aig_ObjRecognizeMux( pObj, &pNodeT, &pNodeE );
+            pNodeC->nRefs--;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [References muxes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManMuxesRef( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes )
+{
+    Aig_Obj_t * pObj, * pNodeT, * pNodeE, * pNodeC;
+    int i;
+    Vec_PtrForEachEntry( Aig_Obj_t *, vMuxes, pObj, i )
+    {
+        if ( Aig_ObjRecognizeExor( pObj, &pNodeT, &pNodeE ) )
+        {
+            pNodeT->nRefs++;
+            pNodeE->nRefs++;
+        }
+        else
+        {
+            pNodeC = Aig_ObjRecognizeMux( pObj, &pNodeT, &pNodeE );
+            pNodeC->nRefs++;
+        }
+    }
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigWin.c b/src/aig/aig/aigWin.c
index 0485b243..5568c9ec 100644
--- a/src/aig/aig/aigWin.c
+++ b/src/aig/aig/aigWin.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -82,7 +85,7 @@ int Aig_ManFindCut_int( Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit
     CostBest   = 100;
     pFaninBest = NULL;
 //printf( "Evaluating fanins of the cut:\n" );
-    Vec_PtrForEachEntry( vFront, pNode, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vFront, pNode, i )
     {
         CostCur = Aig_NodeGetLeafCostOne( pNode, nFanoutLimit );
 //printf( "    Fanin %s has cost %d.\n", Aig_ObjName(pNode), CostCur );
@@ -173,7 +176,7 @@ void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited
     assert( Vec_PtrSize(vFront) <= nSizeLimit );
 
     // clean the visit markings
-    Vec_PtrForEachEntry( vVisited, pNode, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vVisited, pNode, i )
         pNode->fMarkA = 0;
 }
 
@@ -182,3 +185,5 @@ void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aig_.c b/src/aig/aig/aig_.c
index b2313d35..ae0cb568 100644
--- a/src/aig/aig/aig_.c
+++ b/src/aig/aig/aig_.c
@@ -20,6 +20,9 @@
 
 #include "aig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -46,3 +49,5 @@
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 5fea4341..03504138 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -20,6 +20,7 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigRetF.c \
     src/aig/aig/aigScl.c \
     src/aig/aig/aigShow.c \
+    src/aig/aig/aigSplit.c \
     src/aig/aig/aigTable.c \
     src/aig/aig/aigTiming.c \
     src/aig/aig/aigTruth.c \