Made abc.h independent of CUDD and Extra.

96 files changed, 494 insertions, 430 deletions

diff --git a/src/aig/mem/mem.c b/src/aig/mem/mem.c
index 28d7e86e..23d8d7ec 100644
--- a/src/aig/mem/mem.c
+++ b/src/aig/mem/mem.c
@@ -72,10 +72,13 @@ struct Mem_Flex_t_
 
 struct Mem_Step_t_
 {
-    int             nMems;    // the number of fixed memory managers employed
-    Mem_Fixed_t **  pMems;    // memory managers: 2^1 words, 2^2 words, etc
-    int             nMapSize; // the size of the memory array
-    Mem_Fixed_t **  pMap;     // maps the number of bytes into its memory manager
+    int             nMems;              // the number of fixed memory managers employed
+    Mem_Fixed_t **  pMems;              // memory managers: 2^1 words, 2^2 words, etc
+    int             nMapSize;           // the size of the memory array
+    Mem_Fixed_t **  pMap;               // maps the number of bytes into its memory manager
+    int             nLargeChunksAlloc;  // the maximum number of large memory chunks
+    int             nLargeChunks;       // the current number of large memory chunks
+    void **         pLargeChunks;       // the allocated large memory chunks
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -316,7 +319,7 @@ Mem_Flex_t * Mem_FlexStart()
     p->pCurrent      = NULL;
     p->pEnd          = NULL;
 
-    p->nChunkSize    = (1 << 14);
+    p->nChunkSize    = (1 << 12);
     p->nChunksAlloc  = 64;
     p->nChunks       = 0;
     p->pChunks       = ABC_ALLOC( char *, p->nChunksAlloc );
@@ -509,12 +512,12 @@ void Mem_StepStop( Mem_Step_t * p, int fVerbose )
     int i;
     for ( i = 0; i < p->nMems; i++ )
         Mem_FixedStop( p->pMems[i], fVerbose );
-//    if ( p->pLargeChunks ) 
-//    {
-//      for ( i = 0; i < p->nLargeChunks; i++ )
-//          ABC_FREE( p->pLargeChunks[i] );
-//      ABC_FREE( p->pLargeChunks );
-//    }
+    if ( p->pLargeChunks ) 
+    {
+        for ( i = 0; i < p->nLargeChunks; i++ )
+            ABC_FREE( p->pLargeChunks[i] );
+        ABC_FREE( p->pLargeChunks );
+    }
     ABC_FREE( p->pMems );
     ABC_FREE( p->pMap );
     ABC_FREE( p );
@@ -538,18 +541,16 @@ char * Mem_StepEntryFetch( Mem_Step_t * p, int nBytes )
     if ( nBytes > p->nMapSize )
     {
 //        printf( "Allocating %d bytes.\n", nBytes );
-/*
+//        return ABC_ALLOC( char, nBytes );
         if ( p->nLargeChunks == p->nLargeChunksAlloc )
         {
             if ( p->nLargeChunksAlloc == 0 )
-                p->nLargeChunksAlloc = 5;
+                p->nLargeChunksAlloc = 32;
             p->nLargeChunksAlloc *= 2;
-            p->pLargeChunks = ABC_REALLOC( char *, p->pLargeChunks, p->nLargeChunksAlloc ); 
+            p->pLargeChunks = (void **)ABC_REALLOC( char *, p->pLargeChunks, p->nLargeChunksAlloc ); 
         }
         p->pLargeChunks[ p->nLargeChunks++ ] = ABC_ALLOC( char, nBytes );
-        return p->pLargeChunks[ p->nLargeChunks - 1 ];
-*/
-        return ABC_ALLOC( char, nBytes );
+        return (char *)p->pLargeChunks[ p->nLargeChunks - 1 ];
     }
     return Mem_FixedEntryFetch( p->pMap[nBytes] );
 }
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index c1c6a91c..68a50525 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -33,11 +33,11 @@
 #include <time.h>
 
 #include "vec.h"
-#include "cuddInt.h"
 #include "hop.h"
-#include "extra.h"
+#include "st.h"
 #include "stmm.h"
 #include "nm.h"
+#include "mem.h"
 #include "utilCex.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -193,8 +193,8 @@ struct Abc_Ntk_t_
     short             fHiePath;      // flag to mark the network on the path
     // miscellaneous data members
     int               nTravIds;      // the unique traversal IDs of nodes
-    Extra_MmFixed_t * pMmObj;        // memory manager for objects
-    Extra_MmStep_t *  pMmStep;       // memory manager for arrays
+    Mem_Fixed_t *     pMmObj;        // memory manager for objects
+    Mem_Step_t *      pMmStep;       // memory manager for arrays
     void *            pManFunc;      // functionality manager (AIG manager, BDD manager, or memory manager for SOPs)
 //    Abc_Lib_t *       pVerLib;       // for structural verilog designs
     Abc_ManTime_t *   pManTime;      // the timing manager (for mapped networks) stores arrival/required times for all nodes
@@ -209,7 +209,7 @@ struct Abc_Ntk_t_
     void *            pExcare;       // the EXDC network (if given)
     void *            pData;         // misc
     Abc_Ntk_t *       pCopy;         // copy of this network
-    Hop_Man_t *       pHaig;         // history AIG
+    void *            pHaig;         // history AIG
     float *           pLutTimes;     // arrivals/requireds/slacks using LUT-delay model
     Vec_Ptr_t *       vOnehots;      // names of one-hot-encoded registers
     // node attributes
@@ -420,29 +420,29 @@ static inline int         Abc_NodeIsTravIdCurrent( Abc_Obj_t * pNode )       { r
 static inline int         Abc_NodeIsTravIdPrevious( Abc_Obj_t * pNode )      { return (int )(pNode->TravId == pNode->pNtk->nTravIds - 1); }
 
 // checking initial state of the latches
-static inline void        Abc_LatchSetInitNone( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_NONE;         }
-static inline void        Abc_LatchSetInit0( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_ZERO;         }
-static inline void        Abc_LatchSetInit1( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_ONE;          }
-static inline void        Abc_LatchSetInitDc( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_DC;           }
-static inline int         Abc_LatchIsInitNone( Abc_Obj_t * pLatch )  { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_NONE; }
-static inline int         Abc_LatchIsInit0( Abc_Obj_t * pLatch )     { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ZERO; }
-static inline int         Abc_LatchIsInit1( Abc_Obj_t * pLatch )     { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ONE;  }
-static inline int         Abc_LatchIsInitDc( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_DC;   }
-static inline int         Abc_LatchInit( Abc_Obj_t * pLatch )        { assert(Abc_ObjIsLatch(pLatch)); return (int)(ABC_PTRINT_T)pLatch->pData;      }
+static inline void        Abc_LatchSetInitNone( Abc_Obj_t * pLatch ) { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_NONE;                       }
+static inline void        Abc_LatchSetInit0( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_ZERO;                       }
+static inline void        Abc_LatchSetInit1( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_ONE;                        }
+static inline void        Abc_LatchSetInitDc( Abc_Obj_t * pLatch )   { assert(Abc_ObjIsLatch(pLatch)); pLatch->pData = (void *)ABC_INIT_DC;                         }
+static inline int         Abc_LatchIsInitNone( Abc_Obj_t * pLatch )  { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_NONE;               }
+static inline int         Abc_LatchIsInit0( Abc_Obj_t * pLatch )     { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ZERO;               }
+static inline int         Abc_LatchIsInit1( Abc_Obj_t * pLatch )     { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_ONE;                }
+static inline int         Abc_LatchIsInitDc( Abc_Obj_t * pLatch )    { assert(Abc_ObjIsLatch(pLatch)); return pLatch->pData == (void *)ABC_INIT_DC;                 }
+static inline int         Abc_LatchInit( Abc_Obj_t * pLatch )        { assert(Abc_ObjIsLatch(pLatch)); return (int)(ABC_PTRINT_T)pLatch->pData;                     }
 
 // global BDDs of the nodes
-static inline void *      Abc_NtkGlobalBdd( Abc_Ntk_t * pNtk )          { return (void *)Vec_PtrEntry(pNtk->vAttrs, VEC_ATTR_GLOBAL_BDD);                          }
-static inline DdManager * Abc_NtkGlobalBddMan( Abc_Ntk_t * pNtk )       { return (DdManager *)Vec_AttMan( (Vec_Att_t *)Abc_NtkGlobalBdd(pNtk) );                   }
-static inline DdNode **   Abc_NtkGlobalBddArray( Abc_Ntk_t * pNtk )     { return (DdNode **)Vec_AttArray( (Vec_Att_t *)Abc_NtkGlobalBdd(pNtk) );                   }
-static inline DdNode *    Abc_ObjGlobalBdd( Abc_Obj_t * pObj )          { return (DdNode *)Vec_AttEntry( (Vec_Att_t *)Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id );    }
-static inline void        Abc_ObjSetGlobalBdd( Abc_Obj_t * pObj, DdNode * bF )   { Vec_AttWriteEntry( (Vec_Att_t *)Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id, bF );   }
+static inline void *      Abc_NtkGlobalBdd( Abc_Ntk_t * pNtk )          { return Vec_PtrEntry(pNtk->vAttrs, VEC_ATTR_GLOBAL_BDD);                                   }
+static inline void *      Abc_NtkGlobalBddMan( Abc_Ntk_t * pNtk )       { return Vec_AttMan( (Vec_Att_t *)Abc_NtkGlobalBdd(pNtk) );                                 }
+static inline void **     Abc_NtkGlobalBddArray( Abc_Ntk_t * pNtk )     { return Vec_AttArray( (Vec_Att_t *)Abc_NtkGlobalBdd(pNtk) );                               }
+static inline void *      Abc_ObjGlobalBdd( Abc_Obj_t * pObj )          { return Vec_AttEntry( (Vec_Att_t *)Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id );               }
+static inline void        Abc_ObjSetGlobalBdd( Abc_Obj_t * pObj, void * bF )   { Vec_AttWriteEntry( (Vec_Att_t *)Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id, bF );      }
 
 // MV variables of the nodes
-static inline void *      Abc_NtkMvVar( Abc_Ntk_t * pNtk )              { return Vec_PtrEntry(pNtk->vAttrs, VEC_ATTR_MVVAR);                          }
-static inline void *      Abc_NtkMvVarMan( Abc_Ntk_t * pNtk )           { return Abc_NtkMvVar(pNtk)? Vec_AttMan( (Vec_Att_t *)Abc_NtkMvVar(pNtk) ) : NULL;         }
+static inline void *      Abc_NtkMvVar( Abc_Ntk_t * pNtk )              { return Vec_PtrEntry(pNtk->vAttrs, VEC_ATTR_MVVAR);                                        }
+static inline void *      Abc_NtkMvVarMan( Abc_Ntk_t * pNtk )           { return Abc_NtkMvVar(pNtk)? Vec_AttMan( (Vec_Att_t *)Abc_NtkMvVar(pNtk) ) : NULL;          }
 static inline void *      Abc_ObjMvVar( Abc_Obj_t * pObj )              { return Abc_NtkMvVar(pObj->pNtk)? Vec_AttEntry( (Vec_Att_t *)Abc_NtkMvVar(pObj->pNtk), pObj->Id ) : NULL; }
-static inline int         Abc_ObjMvVarNum( Abc_Obj_t * pObj )           { return (Abc_NtkMvVar(pObj->pNtk) && Abc_ObjMvVar(pObj))? *((int*)Abc_ObjMvVar(pObj)) : 2;   }
-static inline void        Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_AttWriteEntry( (Vec_Att_t *)Abc_NtkMvVar(pObj->pNtk), pObj->Id, pV );                }
+static inline int         Abc_ObjMvVarNum( Abc_Obj_t * pObj )           { return (Abc_NtkMvVar(pObj->pNtk) && Abc_ObjMvVar(pObj))? *((int*)Abc_ObjMvVar(pObj)) : 2; }
+static inline void        Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_AttWriteEntry( (Vec_Att_t *)Abc_NtkMvVar(pObj->pNtk), pObj->Id, pV );                 }
 
 ////////////////////////////////////////////////////////////////////////
 ///                        ITERATORS                                 ///
@@ -609,11 +609,8 @@ extern ABC_DLL Abc_Ntk_t *        Abc_NtkFraigRestore();
 extern ABC_DLL void               Abc_NtkFraigStoreClean();
 /*=== abcFunc.c ==========================================================*/
 extern ABC_DLL int                Abc_NtkSopToBdd( Abc_Ntk_t * pNtk );
-extern ABC_DLL DdNode *           Abc_ConvertSopToBdd( DdManager * dd, char * pSop );
-extern ABC_DLL char *             Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode );
 extern ABC_DLL int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect );
-extern ABC_DLL void               Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 );
-extern ABC_DLL int                Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
+extern ABC_DLL void               Abc_NodeBddToCnf( Abc_Obj_t * pNode, Mem_Flex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 );
 extern ABC_DLL void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkSopToAig( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkAigToBdd( Abc_Ntk_t * pNtk );
@@ -688,10 +685,10 @@ extern ABC_DLL Abc_Ntk_t *        Abc_NtkToLogic( Abc_Ntk_t * pNtk );
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkToNetlist( Abc_Ntk_t * pNtk );
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkToNetlistBench( Abc_Ntk_t * pNtk );
 /*=== abcNtbdd.c ==========================================================*/
-extern ABC_DLL Abc_Ntk_t *        Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkDeriveFromBdd( void * dd, void * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
-extern ABC_DLL DdManager *        Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
-extern ABC_DLL DdManager *        Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan );
+extern ABC_DLL void *             Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
+extern ABC_DLL void *             Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan );
 extern ABC_DLL int                Abc_NtkSizeOfGlobalBdds( Abc_Ntk_t * pNtk );
 /*=== abcNtk.c ==========================================================*/
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan );
@@ -782,8 +779,6 @@ extern ABC_DLL Vec_Ptr_t *        Abc_NtkManCutReadCutSmall( Abc_ManCut_t * p );
 extern ABC_DLL Vec_Ptr_t *        Abc_NtkManCutReadVisited( Abc_ManCut_t * p );
 extern ABC_DLL Vec_Ptr_t *        Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, int  fContain );
 extern ABC_DLL void               Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited, int fIncludeFanins );
-extern ABC_DLL DdNode *           Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
-extern ABC_DLL DdNode *           Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, Vec_Ptr_t * vVisited );
 extern ABC_DLL Vec_Ptr_t *        Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vFanins, int LevelMax );
 /*=== abcRefs.c ==========================================================*/
 extern ABC_DLL int                Abc_NodeMffcSize( Abc_Obj_t * pNode );
@@ -802,24 +797,24 @@ extern ABC_DLL int                Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateL
 extern ABC_DLL int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fVerbose, ABC_INT64_T * pNumConfs, ABC_INT64_T * pNumInspects );
 extern ABC_DLL void *             Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes );
 /*=== abcSop.c ==========================================================*/
-extern ABC_DLL char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
-extern ABC_DLL char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
-extern ABC_DLL char *             Abc_SopCreateConst0( Extra_MmFlex_t * pMan );
-extern ABC_DLL char *             Abc_SopCreateConst1( Extra_MmFlex_t * pMan );
-extern ABC_DLL char *             Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 );
-extern ABC_DLL char *             Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
-extern ABC_DLL char *             Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars );
-extern ABC_DLL char *             Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
-extern ABC_DLL char *             Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl );
-extern ABC_DLL char *             Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars );
-extern ABC_DLL char *             Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars );
-extern ABC_DLL char *             Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars );
-extern ABC_DLL char *             Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
-extern ABC_DLL char *             Abc_SopCreateMux( Extra_MmFlex_t * pMan );
-extern ABC_DLL char *             Abc_SopCreateInv( Extra_MmFlex_t * pMan );
-extern ABC_DLL char *             Abc_SopCreateBuf( Extra_MmFlex_t * pMan );
-extern ABC_DLL char *             Abc_SopCreateFromTruth( Extra_MmFlex_t * pMan, int nVars, unsigned * pTruth );
-extern ABC_DLL char *             Abc_SopCreateFromIsop( Extra_MmFlex_t * pMan, int nVars, Vec_Int_t * vCover );
+extern ABC_DLL char *             Abc_SopRegister( Mem_Flex_t * pMan, char * pName );
+extern ABC_DLL char *             Abc_SopStart( Mem_Flex_t * pMan, int nCubes, int nVars );
+extern ABC_DLL char *             Abc_SopCreateConst0( Mem_Flex_t * pMan );
+extern ABC_DLL char *             Abc_SopCreateConst1( Mem_Flex_t * pMan );
+extern ABC_DLL char *             Abc_SopCreateAnd2( Mem_Flex_t * pMan, int fCompl0, int fCompl1 );
+extern ABC_DLL char *             Abc_SopCreateAnd( Mem_Flex_t * pMan, int nVars, int * pfCompl );
+extern ABC_DLL char *             Abc_SopCreateNand( Mem_Flex_t * pMan, int nVars );
+extern ABC_DLL char *             Abc_SopCreateOr( Mem_Flex_t * pMan, int nVars, int * pfCompl );
+extern ABC_DLL char *             Abc_SopCreateOrMultiCube( Mem_Flex_t * pMan, int nVars, int * pfCompl );
+extern ABC_DLL char *             Abc_SopCreateNor( Mem_Flex_t * pMan, int nVars );
+extern ABC_DLL char *             Abc_SopCreateXor( Mem_Flex_t * pMan, int nVars );
+extern ABC_DLL char *             Abc_SopCreateXorSpecial( Mem_Flex_t * pMan, int nVars );
+extern ABC_DLL char *             Abc_SopCreateNxor( Mem_Flex_t * pMan, int nVars );
+extern ABC_DLL char *             Abc_SopCreateMux( Mem_Flex_t * pMan );
+extern ABC_DLL char *             Abc_SopCreateInv( Mem_Flex_t * pMan );
+extern ABC_DLL char *             Abc_SopCreateBuf( Mem_Flex_t * pMan );
+extern ABC_DLL char *             Abc_SopCreateFromTruth( Mem_Flex_t * pMan, int nVars, unsigned * pTruth );
+extern ABC_DLL char *             Abc_SopCreateFromIsop( Mem_Flex_t * pMan, int nVars, Vec_Int_t * vCover );
 extern ABC_DLL int                Abc_SopGetCubeNum( char * pSop );
 extern ABC_DLL int                Abc_SopGetLitNum( char * pSop );
 extern ABC_DLL int                Abc_SopGetVarNum( char * pSop );
@@ -837,10 +832,10 @@ extern ABC_DLL int                Abc_SopIsExorType( char * pSop );
 extern ABC_DLL int                Abc_SopCheck( char * pSop, int nFanins );
 extern ABC_DLL char *             Abc_SopFromTruthBin( char * pTruth );
 extern ABC_DLL char *             Abc_SopFromTruthHex( char * pTruth );
-extern ABC_DLL char *             Abc_SopEncoderPos( Extra_MmFlex_t * pMan, int iValue, int nValues );
-extern ABC_DLL char *             Abc_SopEncoderLog( Extra_MmFlex_t * pMan, int iBit, int nValues );
-extern ABC_DLL char *             Abc_SopDecoderPos( Extra_MmFlex_t * pMan, int nValues );
-extern ABC_DLL char *             Abc_SopDecoderLog( Extra_MmFlex_t * pMan, int nValues );
+extern ABC_DLL char *             Abc_SopEncoderPos( Mem_Flex_t * pMan, int iValue, int nValues );
+extern ABC_DLL char *             Abc_SopEncoderLog( Mem_Flex_t * pMan, int iBit, int nValues );
+extern ABC_DLL char *             Abc_SopDecoderPos( Mem_Flex_t * pMan, int nValues );
+extern ABC_DLL char *             Abc_SopDecoderLog( Mem_Flex_t * pMan, int nValues );
 /*=== abcStrash.c ==========================================================*/
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, int fAllNodes, int fCleanup, int fRecord );
 extern ABC_DLL Abc_Obj_t *        Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int fRecord );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 956a26b9..b624fb10 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -109,6 +110,7 @@ static void        Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan );
 static void        Abc_AigRemoveFromLevelStructure( Vec_Vec_t * vStruct, Abc_Obj_t * pNode );
 static void        Abc_AigRemoveFromLevelStructureR( Vec_Vec_t * vStruct, Abc_Obj_t * pNode );
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -131,7 +133,7 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig )
     pMan = ABC_ALLOC( Abc_Aig_t, 1 );
     memset( pMan, 0, sizeof(Abc_Aig_t) );
     // allocate the table
-    pMan->nBins    = Cudd_PrimeCopy( 10000 );
+    pMan->nBins    = Cudd_Prime( 10000 );
     pMan->pBins    = ABC_ALLOC( Abc_Obj_t *, pMan->nBins );
     memset( pMan->pBins, 0, sizeof(Abc_Obj_t *) * pMan->nBins );
     pMan->vNodes   = Vec_PtrAlloc( 100 );
@@ -593,7 +595,7 @@ void Abc_AigResize( Abc_Aig_t * pMan )
 
 clk = clock();
     // get the new table size
-    nBinsNew = Cudd_PrimeCopy( 3 * pMan->nBins ); 
+    nBinsNew = Cudd_Prime( 3 * pMan->nBins ); 
     // allocate a new array
     pBinsNew = ABC_ALLOC( Abc_Obj_t *, nBinsNew );
     memset( pBinsNew, 0, sizeof(Abc_Obj_t *) * nBinsNew );
diff --git a/src/base/abc/abcBlifMv.c b/src/base/abc/abcBlifMv.c
index 946e3f75..21535cb5 100644
--- a/src/base/abc/abcBlifMv.c
+++ b/src/base/abc/abcBlifMv.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -46,7 +47,7 @@ void Abc_NtkStartMvVars( Abc_Ntk_t * pNtk )
 {
     Vec_Att_t * pAttMan;
     assert( Abc_NtkMvVar(pNtk) == NULL );
-    pAttMan = Vec_AttAlloc( Abc_NtkObjNumMax(pNtk) + 1, Extra_MmFlexStart(), (void(*)(void*))Extra_MmFlexStop, NULL, NULL );
+    pAttMan = Vec_AttAlloc( Abc_NtkObjNumMax(pNtk) + 1, Mem_FlexStart(), (void(*)(void*))Mem_FlexStop, NULL, NULL );
     Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_MVVAR, pAttMan );
 //printf( "allocing attr\n" );
 }
@@ -64,9 +65,9 @@ void Abc_NtkStartMvVars( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 void Abc_NtkFreeMvVars( Abc_Ntk_t * pNtk ) 
 { 
-    Extra_MmFlex_t * pUserMan;
-    pUserMan = (Extra_MmFlex_t *)Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, 0 ); 
-    Extra_MmFlexStop( pUserMan );
+    Mem_Flex_t * pUserMan;
+    pUserMan = (Mem_Flex_t *)Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, 0 ); 
+    Mem_FlexStop( pUserMan, 0 );
 }
 
 /**Function*************************************************************
@@ -82,7 +83,7 @@ void Abc_NtkFreeMvVars( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 void Abc_NtkSetMvVarValues( Abc_Obj_t * pObj, int nValues )
 {
-    Extra_MmFlex_t * pFlex;
+    Mem_Flex_t * pFlex;
     struct temp 
     { 
         int nValues; 
@@ -96,8 +97,8 @@ void Abc_NtkSetMvVarValues( Abc_Obj_t * pObj, int nValues )
     if ( Abc_ObjMvVar(pObj) != NULL )
         return;
     // create the structure
-    pFlex = (Extra_MmFlex_t *)Abc_NtkMvVarMan( pObj->pNtk );
-    pVarStruct = (struct temp *)Extra_MmFlexEntryFetch( pFlex, sizeof(struct temp) );
+    pFlex = (Mem_Flex_t *)Abc_NtkMvVarMan( pObj->pNtk );
+    pVarStruct = (struct temp *)Mem_FlexEntryFetch( pFlex, sizeof(struct temp) );
     pVarStruct->nValues = nValues;
     pVarStruct->pNames = NULL;
     Abc_ObjSetMvVar( pObj, pVarStruct );
@@ -784,7 +785,7 @@ Abc_Ntk_t * Abc_NtkSkeletonBlifMv( Abc_Ntk_t * pNtk )
             for ( v = 0; v < nValues; v++ )
             {
                 pNodeNew = Abc_NtkCreateNode( pNtkNew );
-                pNodeNew->pData = Abc_SopEncoderPos( (Extra_MmFlex_t *)pNtkNew->pManFunc, v, nValues );
+                pNodeNew->pData = Abc_SopEncoderPos( (Mem_Flex_t *)pNtkNew->pManFunc, v, nValues );
                 pNetNew = Abc_NtkCreateNet( pNtkNew );
                 pTermNew = Abc_NtkCreateBi( pNtkNew );
                 Abc_ObjAddFanin( pNodeNew, pNet->pCopy );
@@ -806,7 +807,7 @@ Abc_Ntk_t * Abc_NtkSkeletonBlifMv( Abc_Ntk_t * pNtk )
             for ( k = 0; k < nBits; k++ )
             {
                 pNodeNew = Abc_NtkCreateNode( pNtkNew );
-                pNodeNew->pData = Abc_SopEncoderLog( (Extra_MmFlex_t *)pNtkNew->pManFunc, k, nValues );
+                pNodeNew->pData = Abc_SopEncoderLog( (Mem_Flex_t *)pNtkNew->pManFunc, k, nValues );
                 pNetNew = Abc_NtkCreateNet( pNtkNew );
                 pTermNew = Abc_NtkCreateBi( pNtkNew );
                 Abc_ObjAddFanin( pNodeNew, pNet->pCopy );
@@ -831,7 +832,7 @@ Abc_Ntk_t * Abc_NtkSkeletonBlifMv( Abc_Ntk_t * pNtk )
             Abc_NodeSetTravIdCurrent( pNet );
             nValues = Abc_ObjMvVarNum(pNet);
             pNodeNew = Abc_NtkCreateNode( pNtkNew );
-            pNodeNew->pData = Abc_SopDecoderPos( (Extra_MmFlex_t *)pNtkNew->pManFunc, nValues );
+            pNodeNew->pData = Abc_SopDecoderPos( (Mem_Flex_t *)pNtkNew->pManFunc, nValues );
             for ( v = 0; v < nValues; v++ )
             {
                 pTermNew = Abc_NtkCreateBo( pNtkNew );
@@ -855,7 +856,7 @@ Abc_Ntk_t * Abc_NtkSkeletonBlifMv( Abc_Ntk_t * pNtk )
             nValues = Abc_ObjMvVarNum(pNet);
             nBits = Extra_Base2Log( nValues );
             pNodeNew = Abc_NtkCreateNode( pNtkNew );
-            pNodeNew->pData = Abc_SopDecoderLog( (Extra_MmFlex_t *)pNtkNew->pManFunc, nValues );
+            pNodeNew->pData = Abc_SopDecoderLog( (Mem_Flex_t *)pNtkNew->pManFunc, nValues );
             for ( k = 0; k < nBits; k++ )
             {
                 pTermNew = Abc_NtkCreateBo( pNtkNew );
@@ -950,7 +951,7 @@ Abc_Ntk_t * Abc_NtkInsertBlifMv( Abc_Ntk_t * pNtkBase, Abc_Ntk_t * pNtkLogic )
 ***********************************************************************/
 int Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk )
 {
-    Extra_MmFlex_t * pMmFlex;
+    Mem_Flex_t * pMmFlex;
     Abc_Obj_t * pNode;
     Vec_Str_t * vCube;
     char * pSop0, * pSop1, * pBlifMv, * pCube, * pCur;
@@ -963,7 +964,7 @@ int Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk )
         return 0;
     }
 
-    pMmFlex = Extra_MmFlexStart();
+    pMmFlex = Mem_FlexStart();
     vCube   = Vec_StrAlloc( 100 );
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
@@ -972,7 +973,7 @@ int Abc_NtkConvertToBlifMv( Abc_Ntk_t * pNtk )
         // allocate room for the MV-SOP
         nCubes = Abc_SopGetCubeNum(pSop0) + Abc_SopGetCubeNum(pSop1);
         nSize = nCubes*(2*Abc_ObjFaninNum(pNode) + 2)+1;
-        pBlifMv = Extra_MmFlexEntryFetch( pMmFlex, nSize );
+        pBlifMv = Mem_FlexEntryFetch( pMmFlex, nSize );
         // add the cubes
         pCur = pBlifMv;
         Abc_SopForEachCube( pSop0, Abc_ObjFaninNum(pNode), pCube )
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index ee6f4173..5fb22d79 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int Entry )
+static inline void Vec_IntPushMem( Mem_Step_t * pMemMan, Vec_Int_t * p, int Entry )
 {
     if ( p->nSize == p->nCap )
     {
@@ -52,7 +52,7 @@ static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int
         if ( p->nSize == 0 )
             p->nCap = 1;
         if ( pMemMan )
-            pArray = (int *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 );
+            pArray = (int *)Mem_StepEntryFetch( pMemMan, p->nCap * 8 );
         else
             pArray = ABC_ALLOC( int, p->nCap * 2 );
         if ( p->pArray )
@@ -60,7 +60,7 @@ static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int
             for ( i = 0; i < p->nSize; i++ )
                 pArray[i] = p->pArray[i];
             if ( pMemMan )
-                Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 );
+                Mem_StepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 );
             else
                 ABC_FREE( p->pArray );
         }
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 35ea8332..1c88635a 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -35,59 +35,14 @@ static int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, in
 static DdNode * Abc_ConvertAigToBdd( DdManager * dd, Hop_Obj_t * pRoot);
 static Hop_Obj_t * Abc_ConvertSopToAig( Hop_Man_t * pMan, char * pSop );
 
+extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Converts the network from SOP to BDD representation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pNode;
-    DdManager * dd;
-    int nFaninsMax, i;
- 
-    assert( Abc_NtkHasSop(pNtk) ); 
-
-    // start the functionality manager
-    nFaninsMax = Abc_NtkGetFaninMax( pNtk );
-    if ( nFaninsMax == 0 )
-        printf( "Warning: The network has only constant nodes.\n" );
-
-    dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-
-    // convert each node from SOP to BDD
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        assert( pNode->pData );
-        pNode->pData = Abc_ConvertSopToBdd( dd, (char *)pNode->pData );
-        if ( pNode->pData == NULL )
-        {
-            printf( "Abc_NtkSopToBdd: Error while converting SOP into BDD.\n" );
-            return 0;
-        }
-        Cudd_Ref( (DdNode *)pNode->pData );
-    }
-
-    Extra_MmFlexStop( (Extra_MmFlex_t *)pNtk->pManFunc );
-    pNtk->pManFunc = dd;
-
-    // update the network type
-    pNtk->ntkFunc = ABC_FUNC_BDD;
-    return 1;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Converts the node from SOP to BDD representation.]
 
   Description []
@@ -145,7 +100,7 @@ DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop )
 
 /**Function*************************************************************
 
-  Synopsis    [Removes complemented SOP covers.]
+  Synopsis    [Converts the network from SOP to BDD representation.]
 
   Description []
                
@@ -154,117 +109,45 @@ DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
+int Abc_NtkSopToBdd( Abc_Ntk_t * pNtk )
 {
-    DdManager * dd;
-    DdNode * bFunc;
-    Vec_Str_t * vCube;
     Abc_Obj_t * pNode;
-    int nFaninsMax, fFound, i;
-
-    assert( Abc_NtkHasSop(pNtk) );
-
-    // check if there are nodes with complemented SOPs
-    fFound = 0;
-    Abc_NtkForEachNode( pNtk, pNode, i )
-        if ( Abc_SopIsComplement((char *)pNode->pData) )
-        {
-            fFound = 1;
-            break;
-        }
-    if ( !fFound )
-        return;
+    DdManager * dd;
+    int nFaninsMax, i;
+ 
+    assert( Abc_NtkHasSop(pNtk) ); 
 
-    // start the BDD package
+    // start the functionality manager
     nFaninsMax = Abc_NtkGetFaninMax( pNtk );
     if ( nFaninsMax == 0 )
         printf( "Warning: The network has only constant nodes.\n" );
-    dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-
-    // change the cover of negated nodes
-    vCube = Vec_StrAlloc( 100 );
-    Abc_NtkForEachNode( pNtk, pNode, i )
-        if ( Abc_SopIsComplement((char *)pNode->pData) )
-        {
-            bFunc = Abc_ConvertSopToBdd( dd, (char *)pNode->pData );  Cudd_Ref( bFunc );
-            pNode->pData = Abc_ConvertBddToSop( (Extra_MmFlex_t *)pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, 1 );
-            Cudd_RecursiveDeref( dd, bFunc );
-            assert( !Abc_SopIsComplement((char *)pNode->pData) );
-        }
-    Vec_StrFree( vCube );
-    Extra_StopManager( dd );
-}
-
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Converts the network from BDD to SOP representation.]
-
-  Description [If the flag is set to 1, forces the direct phase of all covers.]
-               
-  SideEffects []
-
-  SeeAlso     []
 
-***********************************************************************/
-int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
-{
-    Abc_Obj_t * pNode;
-    Extra_MmFlex_t * pManNew;
-    DdManager * dd = (DdManager *)pNtk->pManFunc;
-    DdNode * bFunc;
-    Vec_Str_t * vCube;
-    int i, fMode;
-
-    if ( fDirect )
-        fMode = 1;
-    else
-        fMode = -1;
-
-    assert( Abc_NtkHasBdd(pNtk) );
-    if ( dd->size > 0 )
-    Cudd_zddVarsFromBddVars( dd, 2 );
-    // create the new manager
-    pManNew = Extra_MmFlexStart();
+    dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
 
-    // go through the objects
-    vCube = Vec_StrAlloc( 100 );
+    // convert each node from SOP to BDD
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         assert( pNode->pData );
-        bFunc = (DdNode *)pNode->pData;
-        pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, fMode );
-        if ( pNode->pNext == NULL )
+        pNode->pData = Abc_ConvertSopToBdd( dd, (char *)pNode->pData );
+        if ( pNode->pData == NULL )
         {
-            Extra_MmFlexStop( pManNew );
-            Abc_NtkCleanNext( pNtk );
-//            printf( "Converting from BDDs to SOPs has failed.\n" );
-            Vec_StrFree( vCube );
+            printf( "Abc_NtkSopToBdd: Error while converting SOP into BDD.\n" );
             return 0;
         }
+        Cudd_Ref( (DdNode *)pNode->pData );
     }
-    Vec_StrFree( vCube );
 
-    // update the network type
-    pNtk->ntkFunc = ABC_FUNC_SOP;
-    // set the new manager
-    pNtk->pManFunc = pManNew;
-    // transfer from next to data
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pData );
-        pNode->pData = pNode->pNext;
-        pNode->pNext = NULL;
-    }
+    Mem_FlexStop( (Mem_Flex_t *)pNtk->pManFunc, 0 );
+    pNtk->pManFunc = dd;
 
-    // check for remaining references in the package
-    Extra_StopManager( dd );
+    // update the network type
+    pNtk->ntkFunc = ABC_FUNC_BDD;
     return 1;
 }
 
+
+
+
 /**Function*************************************************************
 
   Synopsis    [Converts the node from BDD to SOP representation.]
@@ -276,7 +159,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode )
+char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode )
 {
     int fVerify = 0;
     char * pSop;
@@ -291,7 +174,7 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
         Vec_StrFill( vCube, nFanins, '-' );
         Vec_StrPush( vCube, '\0' );
         if ( pMan )
-            pSop = Extra_MmFlexEntryFetch( pMan, nFanins + 4 );
+            pSop = Mem_FlexEntryFetch( pMan, nFanins + 4 );
         else
             pSop = ABC_ALLOC( char, nFanins + 4 );
         if ( bFuncOn == Cudd_ReadOne(dd) )
@@ -386,7 +269,7 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
 
     // allocate memory for the cover
     if ( pMan )
-        pSop = Extra_MmFlexEntryFetch( pMan, (nFanins + 3) * nCubes + 1 );
+        pSop = Mem_FlexEntryFetch( pMan, (nFanins + 3) * nCubes + 1 );
     else 
         pSop = ABC_ALLOC( char, (nFanins + 3) * nCubes + 1 );
     pSop[(nFanins + 3) * nCubes] = 0;
@@ -417,6 +300,73 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
 
 /**Function*************************************************************
 
+  Synopsis    [Converts the network from BDD to SOP representation.]
+
+  Description [If the flag is set to 1, forces the direct phase of all covers.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
+{
+    Abc_Obj_t * pNode;
+    Mem_Flex_t * pManNew;
+    DdManager * dd = (DdManager *)pNtk->pManFunc;
+    DdNode * bFunc;
+    Vec_Str_t * vCube;
+    int i, fMode;
+
+    if ( fDirect )
+        fMode = 1;
+    else
+        fMode = -1;
+
+    assert( Abc_NtkHasBdd(pNtk) );
+    if ( dd->size > 0 )
+    Cudd_zddVarsFromBddVars( dd, 2 );
+    // create the new manager
+    pManNew = Mem_FlexStart();
+
+    // go through the objects
+    vCube = Vec_StrAlloc( 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        assert( pNode->pData );
+        bFunc = (DdNode *)pNode->pData;
+        pNode->pNext = (Abc_Obj_t *)Abc_ConvertBddToSop( pManNew, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, fMode );
+        if ( pNode->pNext == NULL )
+        {
+            Mem_FlexStop( pManNew, 0 );
+            Abc_NtkCleanNext( pNtk );
+//            printf( "Converting from BDDs to SOPs has failed.\n" );
+            Vec_StrFree( vCube );
+            return 0;
+        }
+    }
+    Vec_StrFree( vCube );
+
+    // update the network type
+    pNtk->ntkFunc = ABC_FUNC_SOP;
+    // set the new manager
+    pNtk->pManFunc = pManNew;
+    // transfer from next to data
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pData );
+        pNode->pData = pNode->pNext;
+        pNode->pNext = NULL;
+    }
+
+    // check for remaining references in the package
+    Extra_StopManager( dd );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Derive the SOP from the ZDD representation of the cubes.]
 
   Description []
@@ -482,7 +432,7 @@ int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFani
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 )
+void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Mem_Flex_t * pMmMan, Vec_Str_t * vCube, int fAllPrimes, char ** ppSop0, char ** ppSop1 )
 {
     assert( Abc_NtkHasBdd(pNode->pNtk) ); 
     *ppSop0 = Abc_ConvertBddToSop( pMmMan, (DdManager *)pNode->pNtk->pManFunc, (DdNode *)pNode->pData, (DdNode *)pNode->pData, Abc_ObjFaninNum(pNode), fAllPrimes, vCube, 0 );
@@ -490,6 +440,59 @@ void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * v
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Removes complemented SOP covers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
+{
+    DdManager * dd;
+    DdNode * bFunc;
+    Vec_Str_t * vCube;
+    Abc_Obj_t * pNode;
+    int nFaninsMax, fFound, i;
+
+    assert( Abc_NtkHasSop(pNtk) );
+
+    // check if there are nodes with complemented SOPs
+    fFound = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( Abc_SopIsComplement((char *)pNode->pData) )
+        {
+            fFound = 1;
+            break;
+        }
+    if ( !fFound )
+        return;
+
+    // start the BDD package
+    nFaninsMax = Abc_NtkGetFaninMax( pNtk );
+    if ( nFaninsMax == 0 )
+        printf( "Warning: The network has only constant nodes.\n" );
+    dd = Cudd_Init( nFaninsMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+
+    // change the cover of negated nodes
+    vCube = Vec_StrAlloc( 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( Abc_SopIsComplement((char *)pNode->pData) )
+        {
+            bFunc = Abc_ConvertSopToBdd( dd, (char *)pNode->pData );  Cudd_Ref( bFunc );
+            pNode->pData = Abc_ConvertBddToSop( (Mem_Flex_t *)pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), 0, vCube, 1 );
+            Cudd_RecursiveDeref( dd, bFunc );
+            assert( !Abc_SopIsComplement((char *)pNode->pData) );
+        }
+    Vec_StrFree( vCube );
+    Extra_StopManager( dd );
+}
+
+
 
 
 /**Function*************************************************************
@@ -573,7 +576,7 @@ int Abc_NtkSopToAig( Abc_Ntk_t * pNtk )
             return 0;
         }
     }
-    Extra_MmFlexStop( (Extra_MmFlex_t *)pNtk->pManFunc );
+    Mem_FlexStop( (Mem_Flex_t *)pNtk->pManFunc, 0 );
     pNtk->pManFunc = pMan;
 
     // update the network type
@@ -876,14 +879,14 @@ int Abc_NtkMapToSop( Abc_Ntk_t * pNtk )
     assert( Abc_NtkHasMapping(pNtk) );
     // update the functionality manager
     assert( pNtk->pManFunc == Abc_FrameReadLibGen() );
-    pNtk->pManFunc = Extra_MmFlexStart();
+    pNtk->pManFunc = Mem_FlexStart();
     pNtk->ntkFunc  = ABC_FUNC_SOP;
     // update the nodes
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
         pSop = Mio_GateReadSop((Mio_Gate_t *)pNode->pData);
         assert( Abc_SopGetVarNum(pSop) == Abc_ObjFaninNum(pNode) );
-        pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, pSop );
+        pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, pSop );
     }
     return 1;
 }
diff --git a/src/base/abc/abcHie.c b/src/base/abc/abcHie.c
index 1155731e..37359522 100644
--- a/src/base/abc/abcHie.c
+++ b/src/base/abc/abcHie.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index 7528f470..b5fa1f64 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -257,7 +258,7 @@ void Abc_NtkNodeConvertToMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t *
     Abc_ObjAddFanin( pMux, pNode1 );
     Abc_ObjAddFanin( pMux, pNode0 );
     if ( Abc_NtkHasSop(pNtk) )
-        pMux->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, "11- 1\n0-1 1\n" );
+        pMux->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, "11- 1\n0-1 1\n" );
     else if ( Abc_NtkHasBdd(pNtk) )
         pMux->pData = Cudd_bddIte((DdManager *)pNtk->pManFunc,Cudd_bddIthVar((DdManager *)pNtk->pManFunc,0),Cudd_bddIthVar((DdManager *)pNtk->pManFunc,1),Cudd_bddIthVar((DdManager *)pNtk->pManFunc,2)), Cudd_Ref( (DdNode *)pMux->pData );
     else if ( Abc_NtkHasAig(pNtk) )
@@ -444,7 +445,7 @@ Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk )
             if ( (k >> i) & 1 )
                 Abc_ObjAddFanin( pObjNew, Abc_NtkCi(pNtkNew, Abc_NtkPiNum(pNtkNew)+k) );
         assert( Abc_ObjFaninNum(pObjNew) == nStates/2 );
-        pObjNew->pData = Abc_SopCreateOr( (Extra_MmFlex_t *)pNtkNew->pManFunc, nStates/2, NULL );
+        pObjNew->pData = Abc_SopCreateOr( (Mem_Flex_t *)pNtkNew->pManFunc, nStates/2, NULL );
         // save the new flop
         pObj = Abc_NtkCi( pNtk, Abc_NtkPiNum(pNtk) + i );
         pObj->pCopy = pObjNew;
@@ -474,7 +475,7 @@ Abc_Ntk_t * Abc_NtkConvertOnehot( Abc_Ntk_t * pNtk )
             Abc_ObjAddFanin( pObjNew, Abc_ObjRegular(pObj->pCopy) );
             pfCompl[i] = Abc_ObjIsComplement(pObj->pCopy) ^ !((k >> i) & 1);
         }
-        pObjNew->pData = Abc_SopCreateAnd( (Extra_MmFlex_t *)pNtkNew->pManFunc, nFlops, pfCompl );
+        pObjNew->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtkNew->pManFunc, nFlops, pfCompl );
         // connect it to the flop input
         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, Abc_NtkPoNum(pNtkNew)+k), pObjNew );
     }
@@ -585,7 +586,7 @@ void Abc_NtkTransformBack( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew, Vec_Ptr_t *
         Abc_ObjAddFanin( pNodeNew, pCtrl );
         Abc_ObjAddFanin( pNodeNew, pDriver );
         Abc_ObjAddFanin( pNodeNew, Abc_ObjFanout0(pObj) );
-        Abc_ObjSetData( pNodeNew, Abc_SopRegister((Extra_MmFlex_t *)pNtkNew->pManFunc, "0-1 1\n11- 1\n") );
+        Abc_ObjSetData( pNodeNew, Abc_SopRegister((Mem_Flex_t *)pNtkNew->pManFunc, "0-1 1\n11- 1\n") );
         Abc_ObjPatchFanin( Abc_ObjFanin0(pObj), pDriver, pNodeNew );
     }
     // remove the useless POs
diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c
index d3e4d735..f376f039 100644
--- a/src/base/abc/abcLib.c
+++ b/src/base/abc/abcLib.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -435,7 +436,7 @@ Abc_Ntk_t * Abc_LibDeriveAig( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib )
     // deallocate memory manager, which remembers the phase
     if ( pNtk->pData )
     {
-        Extra_MmFlexStop( (Extra_MmFlex_t *)pNtk->pData );
+        Mem_FlexStop( (Mem_Flex_t *)pNtk->pData, 0 );
         pNtk->pData = NULL;
     }
     // set the COs
diff --git a/src/base/abc/abcMinBase.c b/src/base/abc/abcMinBase.c
index ee0085a2..a8dc9249 100644
--- a/src/base/abc/abcMinBase.c
+++ b/src/base/abc/abcMinBase.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index f8041ec7..0845f3d2 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 9077e621..e6911485 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -255,7 +255,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         Abc_NtkDupObj(pNtkNew, pObj, 0);
-        pObj->pCopy->pData = Abc_SopCreateAnd2( (Extra_MmFlex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+        pObj->pCopy->pData = Abc_SopCreateAnd2( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
     }
     // create the choice nodes
     Abc_NtkForEachNode( pNtk, pObj, i )
@@ -272,7 +272,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
             Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
         }
         // create the logic function
-        pNodeNew->pData = Abc_SopCreateOrMultiCube( (Extra_MmFlex_t *)pNtkNew->pManFunc, Vec_IntSize(vInts), Vec_IntArray(vInts) );
+        pNodeNew->pData = Abc_SopCreateOrMultiCube( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_IntSize(vInts), Vec_IntArray(vInts) );
         // set the new node
         pObj->pCopy->pCopy = pNodeNew;
         Vec_IntFree( vInts );
@@ -349,7 +349,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
     Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
     {
         Abc_NtkDupObj( pNtkNew, pObj, 0 );
-        pObj->pCopy->pData = Abc_SopCreateAnd( (Extra_MmFlex_t *)pNtkNew->pManFunc, 2, NULL );
+        pObj->pCopy->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtkNew->pManFunc, 2, NULL );
         if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) )
             pObj->pCopy->pCopy = Abc_NtkCreateNodeInv( pNtkNew, pObj->pCopy );
     }
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index e6a8a5ba..3ec261a8 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -63,15 +63,15 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan
     pNtk->vBoxes      = Vec_PtrAlloc( 100 );
     pNtk->vLtlProperties = Vec_PtrAlloc( 100 );
     // start the memory managers
-    pNtk->pMmObj      = fUseMemMan? Extra_MmFixedStart( sizeof(Abc_Obj_t) ) : NULL;
-    pNtk->pMmStep     = fUseMemMan? Extra_MmStepStart( ABC_NUM_STEPS ) : NULL;
+    pNtk->pMmObj      = fUseMemMan? Mem_FixedStart( sizeof(Abc_Obj_t) ) : NULL;
+    pNtk->pMmStep     = fUseMemMan? Mem_StepStart( ABC_NUM_STEPS ) : NULL;
     // get ready to assign the first Obj ID
     pNtk->nTravIds    = 1;
     // start the functionality manager
     if ( Abc_NtkIsStrash(pNtk) )
         pNtk->pManFunc = Abc_AigAlloc( pNtk );
     else if ( Abc_NtkHasSop(pNtk) || Abc_NtkHasBlifMv(pNtk) )
-        pNtk->pManFunc = Extra_MmFlexStart();
+        pNtk->pManFunc = Mem_FlexStart();
     else if ( Abc_NtkHasBdd(pNtk) )
         pNtk->pManFunc = Cudd_Init( 20, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
     else if ( Abc_NtkHasAig(pNtk) )
@@ -906,7 +906,7 @@ Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop )
     pNode = Abc_NtkCreateNode( pNtkNew );
     Abc_NtkForEachPi( pNtkNew, pFanin, i )
         Abc_ObjAddFanin( pNode, pFanin );
-    pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtkNew->pManFunc, pSop );
+    pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, pSop );
     // create the only PO
     pNodePo = Abc_NtkCreatePo(pNtkNew);
     Abc_ObjAddFanin( pNodePo, pNode );
@@ -990,14 +990,14 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     if ( pNtk->pSeqModelVec )
         Vec_PtrFreeFree( pNtk->pSeqModelVec );
     TotalMemory  = 0;
-    TotalMemory += pNtk->pMmObj? Extra_MmFixedReadMemUsage(pNtk->pMmObj)  : 0;
-    TotalMemory += pNtk->pMmStep? Extra_MmStepReadMemUsage(pNtk->pMmStep) : 0;
+    TotalMemory += pNtk->pMmObj? Mem_FixedReadMemUsage(pNtk->pMmObj)  : 0;
+    TotalMemory += pNtk->pMmStep? Mem_StepReadMemUsage(pNtk->pMmStep) : 0;
 //    fprintf( stdout, "The total memory allocated internally by the network = %0.2f Mb.\n", ((double)TotalMemory)/(1<<20) );
     // free the storage 
     if ( pNtk->pMmObj )
-        Extra_MmFixedStop( pNtk->pMmObj );
+        Mem_FixedStop( pNtk->pMmObj, 0 );
     if ( pNtk->pMmStep )
-        Extra_MmStepStop ( pNtk->pMmStep );
+        Mem_StepStop ( pNtk->pMmStep, 0 );
     // name manager
     Nm_ManFree( pNtk->pManName );
     // free the timing manager
@@ -1007,7 +1007,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     if ( Abc_NtkIsStrash(pNtk) )
         Abc_AigFree( (Abc_Aig_t *)pNtk->pManFunc );
     else if ( Abc_NtkHasSop(pNtk) || Abc_NtkHasBlifMv(pNtk) )
-        Extra_MmFlexStop( (Extra_MmFlex_t *)pNtk->pManFunc );
+        Mem_FlexStop( (Mem_Flex_t *)pNtk->pManFunc, 0 );
     else if ( Abc_NtkHasBdd(pNtk) )
         Extra_StopManager( (DdManager *)pNtk->pManFunc );
     else if ( Abc_NtkHasAig(pNtk) )
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 40bbc18b..4c17962b 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -49,7 +49,7 @@ Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
 {
     Abc_Obj_t * pObj;
     if ( pNtk->pMmObj )
-        pObj = (Abc_Obj_t *)Extra_MmFixedEntryFetch( pNtk->pMmObj );
+        pObj = (Abc_Obj_t *)Mem_FixedEntryFetch( pNtk->pMmObj );
     else
         pObj = (Abc_Obj_t *)ABC_ALLOC( Abc_Obj_t, 1 );
     memset( pObj, 0, sizeof(Abc_Obj_t) );
@@ -86,7 +86,7 @@ void Abc_ObjRecycle( Abc_Obj_t * pObj )
     memset( pObj, 0, sizeof(Abc_Obj_t) );
     // recycle the object
     if ( pNtk->pMmObj )
-        Extra_MmFixedEntryRecycle( pNtk->pMmObj, (char *)pObj );
+        Mem_FixedEntryRecycle( pNtk->pMmObj, (char *)pObj );
     else
         ABC_FREE( pObj );
 }
@@ -345,7 +345,7 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName
             if ( Abc_NtkIsStrash(pNtkNew) ) 
             {}
             else if ( Abc_NtkHasSop(pNtkNew) || Abc_NtkHasBlifMv(pNtkNew) )
-                pObjNew->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtkNew->pManFunc, (char *)pObj->pData );
+                pObjNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, (char *)pObj->pData );
             else if ( Abc_NtkHasBdd(pNtkNew) )
                 pObjNew->pData = Cudd_bddTransfer((DdManager *)pObj->pNtk->pManFunc, (DdManager *)pNtkNew->pManFunc, (DdNode *)pObj->pData), Cudd_Ref((DdNode *)pObjNew->pData);
             else if ( Abc_NtkHasAig(pNtkNew) )
@@ -581,7 +581,7 @@ Abc_Obj_t * Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
     pNode = Abc_NtkCreateNode( pNtk );   
     if ( Abc_NtkHasSop(pNtk) || Abc_NtkHasBlifMv(pNtk) )
-        pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, " 0\n" );
+        pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 0\n" );
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_ReadLogicZero((DdManager *)pNtk->pManFunc), Cudd_Ref( (DdNode *)pNode->pData );
     else if ( Abc_NtkHasAig(pNtk) )
@@ -610,7 +610,7 @@ Abc_Obj_t * Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
     pNode = Abc_NtkCreateNode( pNtk );   
     if ( Abc_NtkHasSop(pNtk) || Abc_NtkHasBlifMv(pNtk) )
-        pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, " 1\n" );
+        pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 1\n" );
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_ReadOne((DdManager *)pNtk->pManFunc), Cudd_Ref( (DdNode *)pNode->pData );
     else if ( Abc_NtkHasAig(pNtk) )
@@ -640,7 +640,7 @@ Abc_Obj_t * Abc_NtkCreateNodeInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
     pNode = Abc_NtkCreateNode( pNtk );   
     if ( pFanin ) Abc_ObjAddFanin( pNode, pFanin );
     if ( Abc_NtkHasSop(pNtk) )
-        pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, "0 1\n" );
+        pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, "0 1\n" );
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_Not(Cudd_bddIthVar((DdManager *)pNtk->pManFunc,0)), Cudd_Ref( (DdNode *)pNode->pData );
     else if ( Abc_NtkHasAig(pNtk) )
@@ -670,7 +670,7 @@ Abc_Obj_t * Abc_NtkCreateNodeBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
     pNode = Abc_NtkCreateNode( pNtk ); 
     if ( pFanin ) Abc_ObjAddFanin( pNode, pFanin );
     if ( Abc_NtkHasSop(pNtk) )
-        pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, "1 1\n" );
+        pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, "1 1\n" );
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_bddIthVar((DdManager *)pNtk->pManFunc,0), Cudd_Ref( (DdNode *)pNode->pData );
     else if ( Abc_NtkHasAig(pNtk) )
@@ -702,7 +702,7 @@ Abc_Obj_t * Abc_NtkCreateNodeAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
     for ( i = 0; i < vFanins->nSize; i++ )
         Abc_ObjAddFanin( pNode, (Abc_Obj_t *)vFanins->pArray[i] );
     if ( Abc_NtkHasSop(pNtk) )
-        pNode->pData = Abc_SopCreateAnd( (Extra_MmFlex_t *)pNtk->pManFunc, Vec_PtrSize(vFanins), NULL );
+        pNode->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtk->pManFunc, Vec_PtrSize(vFanins), NULL );
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Extra_bddCreateAnd( (DdManager *)pNtk->pManFunc, Vec_PtrSize(vFanins) ), Cudd_Ref((DdNode *)pNode->pData); 
     else if ( Abc_NtkHasAig(pNtk) )
@@ -732,7 +732,7 @@ Abc_Obj_t * Abc_NtkCreateNodeOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
     for ( i = 0; i < vFanins->nSize; i++ )
         Abc_ObjAddFanin( pNode, (Abc_Obj_t *)vFanins->pArray[i] );
     if ( Abc_NtkHasSop(pNtk) )
-        pNode->pData = Abc_SopCreateOr( (Extra_MmFlex_t *)pNtk->pManFunc, Vec_PtrSize(vFanins), NULL );
+        pNode->pData = Abc_SopCreateOr( (Mem_Flex_t *)pNtk->pManFunc, Vec_PtrSize(vFanins), NULL );
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Extra_bddCreateOr( (DdManager *)pNtk->pManFunc, Vec_PtrSize(vFanins) ), Cudd_Ref((DdNode *)pNode->pData); 
     else if ( Abc_NtkHasAig(pNtk) )
@@ -762,7 +762,7 @@ Abc_Obj_t * Abc_NtkCreateNodeExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
     for ( i = 0; i < vFanins->nSize; i++ )
         Abc_ObjAddFanin( pNode, (Abc_Obj_t *)vFanins->pArray[i] );
     if ( Abc_NtkHasSop(pNtk) )
-        pNode->pData = Abc_SopCreateXorSpecial( (Extra_MmFlex_t *)pNtk->pManFunc, Vec_PtrSize(vFanins) );
+        pNode->pData = Abc_SopCreateXorSpecial( (Mem_Flex_t *)pNtk->pManFunc, Vec_PtrSize(vFanins) );
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Extra_bddCreateExor( (DdManager *)pNtk->pManFunc, Vec_PtrSize(vFanins) ), Cudd_Ref((DdNode *)pNode->pData); 
     else if ( Abc_NtkHasAig(pNtk) )
@@ -792,7 +792,7 @@ Abc_Obj_t * Abc_NtkCreateNodeMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_
     Abc_ObjAddFanin( pNode, pNode1 );
     Abc_ObjAddFanin( pNode, pNode0 );
     if ( Abc_NtkHasSop(pNtk) )
-        pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, "11- 1\n0-1 1\n" );
+        pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, "11- 1\n0-1 1\n" );
     else if ( Abc_NtkHasBdd(pNtk) )
         pNode->pData = Cudd_bddIte((DdManager *)pNtk->pManFunc,Cudd_bddIthVar((DdManager *)pNtk->pManFunc,0),Cudd_bddIthVar((DdManager *)pNtk->pManFunc,1),Cudd_bddIthVar((DdManager *)pNtk->pManFunc,2)), Cudd_Ref( (DdNode *)pNode->pData );
     else if ( Abc_NtkHasAig(pNtk) )
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index 5be2f8ef..9e751f0a 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -53,11 +54,11 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName )
+char * Abc_SopRegister( Mem_Flex_t * pMan, char * pName )
 {
     char * pRegName;
     if ( pName == NULL ) return NULL;
-    pRegName = Extra_MmFlexEntryFetch( pMan, strlen(pName) + 1 );
+    pRegName = Mem_FlexEntryFetch( pMan, strlen(pName) + 1 );
     strcpy( pRegName, pName );
     return pRegName;
 }
@@ -73,13 +74,13 @@ char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars )
+char * Abc_SopStart( Mem_Flex_t * pMan, int nCubes, int nVars )
 {
     char * pSopCover, * pCube;
     int i, Length;
 
     Length = nCubes * (nVars + 3);
-    pSopCover = Extra_MmFlexEntryFetch( pMan, Length + 1 );
+    pSopCover = Mem_FlexEntryFetch( pMan, Length + 1 );
     memset( pSopCover, '-', Length );
     pSopCover[Length] = 0;
 
@@ -104,7 +105,7 @@ char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateConst1( Extra_MmFlex_t * pMan )
+char * Abc_SopCreateConst1( Mem_Flex_t * pMan )
 {
     return Abc_SopRegister( pMan, " 1\n" );
 }
@@ -120,7 +121,7 @@ char * Abc_SopCreateConst1( Extra_MmFlex_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateConst0( Extra_MmFlex_t * pMan )
+char * Abc_SopCreateConst0( Mem_Flex_t * pMan )
 {
     return Abc_SopRegister( pMan, " 0\n" );
 }
@@ -136,7 +137,7 @@ char * Abc_SopCreateConst0( Extra_MmFlex_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 )
+char * Abc_SopCreateAnd2( Mem_Flex_t * pMan, int fCompl0, int fCompl1 )
 {
     char Buffer[6];
     Buffer[0] = '1' - fCompl0;
@@ -159,7 +160,7 @@ char * Abc_SopCreateAnd2( Extra_MmFlex_t * pMan, int fCompl0, int fCompl1 )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
+char * Abc_SopCreateAnd( Mem_Flex_t * pMan, int nVars, int * pfCompl )
 {
     char * pSop;
     int i;
@@ -181,7 +182,7 @@ char * Abc_SopCreateAnd( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars )
+char * Abc_SopCreateNand( Mem_Flex_t * pMan, int nVars )
 {
     char * pSop;
     int i;
@@ -203,7 +204,7 @@ char * Abc_SopCreateNand( Extra_MmFlex_t * pMan, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
+char * Abc_SopCreateOr( Mem_Flex_t * pMan, int nVars, int * pfCompl )
 {
     char * pSop;
     int i;
@@ -225,7 +226,7 @@ char * Abc_SopCreateOr( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl )
+char * Abc_SopCreateOrMultiCube( Mem_Flex_t * pMan, int nVars, int * pfCompl )
 {
     char * pSop, * pCube;
     int i;
@@ -250,7 +251,7 @@ char * Abc_SopCreateOrMultiCube( Extra_MmFlex_t * pMan, int nVars, int * pfCompl
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars )
+char * Abc_SopCreateNor( Mem_Flex_t * pMan, int nVars )
 {
     char * pSop;
     int i;
@@ -271,7 +272,7 @@ char * Abc_SopCreateNor( Extra_MmFlex_t * pMan, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars )
+char * Abc_SopCreateXor( Mem_Flex_t * pMan, int nVars )
 {
     assert( nVars == 2 );
     return Abc_SopRegister(pMan, "01 1\n10 1\n");
@@ -288,7 +289,7 @@ char * Abc_SopCreateXor( Extra_MmFlex_t * pMan, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars )
+char * Abc_SopCreateXorSpecial( Mem_Flex_t * pMan, int nVars )
 {
     char * pSop;
     pSop = Abc_SopCreateAnd( pMan, nVars, NULL );
@@ -308,7 +309,7 @@ char * Abc_SopCreateXorSpecial( Extra_MmFlex_t * pMan, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars )
+char * Abc_SopCreateNxor( Mem_Flex_t * pMan, int nVars )
 {
     assert( nVars == 2 );
     return Abc_SopRegister(pMan, "11 1\n00 1\n");
@@ -326,7 +327,7 @@ char * Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateMux( Extra_MmFlex_t * pMan )
+char * Abc_SopCreateMux( Mem_Flex_t * pMan )
 {
     return Abc_SopRegister(pMan, "11- 1\n0-1 1\n");
 }
@@ -342,7 +343,7 @@ char * Abc_SopCreateMux( Extra_MmFlex_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateInv( Extra_MmFlex_t * pMan )
+char * Abc_SopCreateInv( Mem_Flex_t * pMan )
 {
     return Abc_SopRegister(pMan, "0 1\n");
 }
@@ -358,7 +359,7 @@ char * Abc_SopCreateInv( Extra_MmFlex_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateBuf( Extra_MmFlex_t * pMan )
+char * Abc_SopCreateBuf( Mem_Flex_t * pMan )
 {
     return Abc_SopRegister(pMan, "1 1\n");
 }
@@ -374,7 +375,7 @@ char * Abc_SopCreateBuf( Extra_MmFlex_t * pMan )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateFromTruth( Extra_MmFlex_t * pMan, int nVars, unsigned * pTruth )
+char * Abc_SopCreateFromTruth( Mem_Flex_t * pMan, int nVars, unsigned * pTruth )
 {
     char * pSop, * pCube;
     int nMints, Counter, i, k;
@@ -413,7 +414,7 @@ char * Abc_SopCreateFromTruth( Extra_MmFlex_t * pMan, int nVars, unsigned * pTru
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopCreateFromIsop( Extra_MmFlex_t * pMan, int nVars, Vec_Int_t * vCover )
+char * Abc_SopCreateFromIsop( Mem_Flex_t * pMan, int nVars, Vec_Int_t * vCover )
 {
     char * pSop, * pCube;
     int i, k, Entry, Literal;
@@ -1001,7 +1002,7 @@ char * Abc_SopFromTruthHex( char * pTruth )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopEncoderPos( Extra_MmFlex_t * pMan, int iValue, int nValues )
+char * Abc_SopEncoderPos( Mem_Flex_t * pMan, int iValue, int nValues )
 {
     char Buffer[32];
     assert( iValue < nValues );
@@ -1020,7 +1021,7 @@ char * Abc_SopEncoderPos( Extra_MmFlex_t * pMan, int iValue, int nValues )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopEncoderLog( Extra_MmFlex_t * pMan, int iBit, int nValues )
+char * Abc_SopEncoderLog( Mem_Flex_t * pMan, int iBit, int nValues )
 {
     char * pResult;
     Vec_Str_t * vSop;
@@ -1064,7 +1065,7 @@ char * Abc_SopEncoderLog( Extra_MmFlex_t * pMan, int iBit, int nValues )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopDecoderPos( Extra_MmFlex_t * pMan, int nValues )
+char * Abc_SopDecoderPos( Mem_Flex_t * pMan, int nValues )
 {
     char * pResult;
     Vec_Str_t * vSop;
@@ -1100,7 +1101,7 @@ char * Abc_SopDecoderPos( Extra_MmFlex_t * pMan, int nValues )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_SopDecoderLog( Extra_MmFlex_t * pMan, int nValues )
+char * Abc_SopDecoderLog( Mem_Flex_t * pMan, int nValues )
 {
     char * pResult;
     Vec_Str_t * vSop;
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 43c53004..38d800d0 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -315,6 +315,7 @@ int Abc_NtkGetAigNodeNum( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 int Abc_NtkGetClauseNum( Abc_Ntk_t * pNtk )
 {
+    extern int Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
     Abc_Obj_t * pNode;
     DdNode * bCover, * zCover, * bFunc;
     DdManager * dd = (DdManager *)pNtk->pManFunc;
diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c
index b595a536..02d5fd17 100644
--- a/src/base/abci/abcAuto.c
+++ b/src/base/abci/abcAuto.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -63,7 +64,7 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
     nInputs  = Abc_NtkCiNum(pNtk);
     nOutputs = Abc_NtkCoNum(pNtk);
 //    dd       = pNtk->pManGlob;
-    dd = Abc_NtkGlobalBddMan( pNtk );
+    dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
 
     // complement the global functions
     vFuncsGlob = Vec_PtrAlloc( Abc_NtkCoNum(pNtk) );
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index 840fd6f5..f69c80bd 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcBm.c b/src/base/abci/abcBm.c
index 8855fd9e..25fba5fd 100644
--- a/src/base/abci/abcBm.c
+++ b/src/base/abci/abcBm.c
@@ -28,6 +28,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "sim.h"
 #include "satSolver.h"
 
diff --git a/src/base/abci/abcCas.c b/src/base/abci/abcCas.c
index 76fe5e9f..68c91343 100644
--- a/src/base/abci/abcCas.c
+++ b/src/base/abci/abcCas.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -69,16 +70,16 @@ Abc_Ntk_t * Abc_NtkCascade( Abc_Ntk_t * pNtk, int nLutSize, int fCheck, int fVer
 
     if ( fVerbose )
     {
-        DdManager * dd = Abc_NtkGlobalBddMan( pNtk );
+        DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
         printf( "Shared BDD size = %6d nodes.  ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
         ABC_PRT( "BDD construction time", clock() - clk );
     }
 
     // collect global BDDs
-    dd = Abc_NtkGlobalBddMan( pNtk );
+    dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
     ppOutputs = ABC_ALLOC( DdNode *, Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pNode, i )
-        ppOutputs[i] = Abc_ObjGlobalBdd(pNode);
+        ppOutputs[i] = (DdNode *)Abc_ObjGlobalBdd(pNode);
 
     // call the decomposition
     pFileGeneric = Extra_FileNameGeneric( pNtk->pSpec );
diff --git a/src/base/abci/abcCascade.c b/src/base/abci/abcCascade.c
index a2e6d234..02858d97 100644
--- a/src/base/abci/abcCascade.c
+++ b/src/base/abci/abcCascade.c
@@ -248,7 +248,7 @@ void Abc_NtkBddDec( Abc_Ntk_t * pNtk, int fVerbose )
     int i;
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkCoNum(pNtk) <= BDD_FUNC_MAX );
-    dd = Abc_NtkBuildGlobalBdds( pNtk, nBddSizeMax, fDropInternal, fReorder, fVerbose );
+    dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddSizeMax, fDropInternal, fReorder, fVerbose );
     if ( dd == NULL )
     {
         Abc_Print( -1, "Construction of global BDDs has failed.\n" );
@@ -264,7 +264,7 @@ void Abc_NtkBddDec( Abc_Ntk_t * pNtk, int fVerbose )
 //        Cudd_addConst( dd, i );
     // collect global BDDs
     Abc_NtkForEachCo( pNtk, pNode, i )
-        pFuncs[i] = Abc_ObjGlobalBdd(pNode);
+        pFuncs[i] = (DdNode *)Abc_ObjGlobalBdd(pNode);
 
     pReo = Extra_ReorderInit( Abc_NtkCiNum(pNtk), 1000 );
     Extra_ReorderSetMinimizationType( pReo, REO_MINIMIZE_WIDTH );
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index 1b7709c5..07996b9a 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
-//#include "reo.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -57,7 +57,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
         return NULL;
     if ( fVerbose )
     {
-        DdManager * dd = Abc_NtkGlobalBddMan( pNtk );
+        DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
         printf( "Shared BDD size = %6d nodes.  ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
         ABC_PRT( "BDD construction time", clock() - clk );
     }
@@ -114,7 +114,7 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode, * pDriver, * pNodeNew;
 //    DdManager * dd = pNtk->pManGlob;
-    DdManager * dd = Abc_NtkGlobalBddMan( pNtk );
+    DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
     int i;
 
 //    pReo = Extra_ReorderInit( Abc_NtkCiNum(pNtk), 1000 );
@@ -136,7 +136,7 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
             continue;
         }
 //        pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) );
-        pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Abc_ObjGlobalBdd(pNode) );
+        pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)Abc_ObjGlobalBdd(pNode) );
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
 
 //        Extra_ShuffleTest( pReo, dd, Abc_ObjGlobalBdd(pNode) );
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 10cacff1..a08ce490 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "cut.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 225bf1be..62f9b325 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1146,10 +1146,10 @@ Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t
         {
             uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
             Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover );
-            pNodeNew->pData = Abc_SopCreateFromIsop( (Extra_MmFlex_t *)pNtkNew->pManFunc, pCut->nFanins, vCover );
+            pNodeNew->pData = Abc_SopCreateFromIsop( (Mem_Flex_t *)pNtkNew->pManFunc, pCut->nFanins, vCover );
         }
         else
-            pNodeNew->pData = Abc_SopCreateFromIsop( (Extra_MmFlex_t *)pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
+            pNodeNew->pData = Abc_SopCreateFromIsop( (Mem_Flex_t *)pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] );
         // save the node
         pObj->pData = pNodeNew;
     }
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 0bfb4ec0..558d9349 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "dsd.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -61,7 +62,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, int fVerbose, int fPrint, int fS
     DdManager * dd;
     Abc_Ntk_t * pNtkNew;
     assert( Abc_NtkIsStrash(pNtk) );
-    dd = Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
+    dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );
     if ( dd == NULL )
         return NULL;
     if ( fVerbose )
@@ -110,7 +111,7 @@ Abc_Ntk_t * Abc_NtkDsdInternal( Abc_Ntk_t * pNtk, int fVerbose, int fPrint, int
         Vec_PtrPush( vFuncsGlob, Cudd_NotCond(Abc_ObjGlobalBdd(pObj), Abc_ObjFaninC0(pObj)) );
 
     // perform the decomposition
-    dd = Abc_NtkGlobalBddMan(pNtk);
+    dd = (DdManager *)Abc_NtkGlobalBddMan(pNtk);
     pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose );
     Dsd_Decompose( pManDsd, (DdNode **)vFuncsGlob->pArray, Abc_NtkCoNum(pNtk) );
     Vec_PtrFree( vFuncsGlob );
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index bd030609..dbbcb1b1 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -144,7 +144,7 @@ void Abc_NtkFxuCollectInfo( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
     Abc_Obj_t * pNode;
     int i;
     // add information to the manager
-    p->pManSop    = (Extra_MmFlex_t *)pNtk->pManFunc;
+    p->pManSop    = (Mem_Flex_t *)pNtk->pManFunc;
     p->vSops      = Vec_PtrAlloc(0);
     p->vFanins    = Vec_PtrAlloc(0);
     p->vSopsNew   = Vec_PtrAlloc(0);
diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
index dc376826..a886949f 100644
--- a/src/base/abci/abcGen.c
+++ b/src/base/abci/abcGen.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 82e968bd..ce1366de 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -417,13 +417,13 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
             if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0) )
             {
                 assert( RetValue == 0 );
-                pNodeNew->pData = Abc_SopCreateAnd( (Extra_MmFlex_t *)pNtkNew->pManFunc, If_CutLeaveNum(pCutBest), NULL );
+                pNodeNew->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtkNew->pManFunc, If_CutLeaveNum(pCutBest), NULL );
                 pNodeNew = (Vec_IntSize(vCover) == 0) ? Abc_NtkCreateNodeConst0(pNtkNew) : Abc_NtkCreateNodeConst1(pNtkNew);
             }
             else
             {
                 // derive the AIG for that tree
-                pNodeNew->pData = Abc_SopCreateFromIsop( (Extra_MmFlex_t *)pNtkNew->pManFunc, If_CutLeaveNum(pCutBest), vCover );
+                pNodeNew->pData = Abc_SopCreateFromIsop( (Mem_Flex_t *)pNtkNew->pManFunc, If_CutLeaveNum(pCutBest), vCover );
                 if ( RetValue )
                     Abc_SopComplement( (char *)pNodeNew->pData );
             }
diff --git a/src/base/abci/abcLut.c b/src/base/abci/abcLut.c
index a33cc7db..98991e25 100644
--- a/src/base/abci/abcLut.c
+++ b/src/base/abci/abcLut.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "cut.h" 
 
 ABC_NAMESPACE_IMPL_START
@@ -582,7 +583,7 @@ Abc_Obj_t * Abc_NodeSuperChoiceLut( Abc_ManScl_t * p, Abc_Obj_t * pObj )
     Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pFanin, i )
         Abc_ObjAddFanin( pObjNew, pFanin );
     // create the function
-    pObjNew->pData = Abc_SopCreateFromTruth( (Extra_MmFlex_t *)pObj->pNtk->pManFunc, Vec_PtrSize(p->vLeaves), p->uTruth ); // need ISOP
+    pObjNew->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pObj->pNtk->pManFunc, Vec_PtrSize(p->vLeaves), p->uTruth ); // need ISOP
     pObjNew->Level = Abc_NodeGetLevel( pObjNew );
     return pObjNew;
 }
@@ -763,7 +764,7 @@ int Abc_NodeDecomposeStep( Abc_ManScl_t * p )
             Abc_ObjAddFanin( pObjNew, pFanin );
         }
         // create the function
-        pObjNew->pData = Abc_SopCreateFromTruth( (Extra_MmFlex_t *)pNtk->pManFunc, p->nLutSize, pTruth ); // need ISOP
+        pObjNew->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, p->nLutSize, pTruth ); // need ISOP
         pObjNew->Level = Abc_NodeGetLevel( pObjNew );
         pNodesNew[v] = pObjNew;
     }
diff --git a/src/base/abci/abcLutmin.c b/src/base/abci/abcLutmin.c
index 71dea2e1..c539b53e 100644
--- a/src/base/abci/abcLutmin.c
+++ b/src/base/abci/abcLutmin.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 543df7b0..33707b15 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -657,7 +657,7 @@ Abc_Obj_t * Abc_NodeFromMapSuperChoice_rec( Abc_Ntk_t * pNtkNew, Map_Super_t * p
         pNodeFanin = Abc_NodeFromMapSuperChoice_rec( pNtkNew, ppFanins[i], pNodePis, nNodePis );
         Abc_ObjAddFanin( pNodeNew, pNodeFanin );
     }
-    pNodeNew->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtkNew->pManFunc, Mio_GateReadSop(pRoot) );
+    pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Mio_GateReadSop(pRoot) );
     return pNodeNew;
 }
 
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 0c75919c..5397f167 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcMulti.c b/src/base/abci/abcMulti.c
index 4e962cff..299e22d5 100644
--- a/src/base/abci/abcMulti.c
+++ b/src/base/abci/abcMulti.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcMv.c b/src/base/abci/abcMv.c
index 4bfb1a02..98d27a19 100644
--- a/src/base/abci/abcMv.c
+++ b/src/base/abci/abcMv.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcNpnSave.c b/src/base/abci/abcNpnSave.c
index 381409de..568a3e28 100644
--- a/src/base/abci/abcNpnSave.c
+++ b/src/base/abci/abcNpnSave.c
@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "aig.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index d27eab82..33226a19 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -52,7 +53,7 @@ static DdNode *    Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, in
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi )
+Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, void * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi )
 {
     Abc_Ntk_t * pNtk; 
     Vec_Ptr_t * vNamesPiFake = NULL;
@@ -72,7 +73,7 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo
 
     // make sure BDD depends on the variables whose index 
     // does not exceed the size of the array with PI names
-    bSupp = Cudd_Support( dd, bFunc );   Cudd_Ref( bSupp );
+    bSupp = Cudd_Support( dd, (DdNode *)bFunc );   Cudd_Ref( bSupp );
     for ( bTemp = bSupp; bTemp != Cudd_ReadOne(dd); bTemp = cuddT(bTemp) )
         if ( (int)Cudd_NodeReadIndex(bTemp) >= Vec_PtrSize(vNamesPi) )
             break;
@@ -90,7 +91,7 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo
         Abc_ObjAssignName( Abc_NtkCreatePi(pNtk), pName, NULL );
     // create the node
     pNode = Abc_NtkCreateNode( pNtk );
-    pNode->pData = (DdNode *)Cudd_bddTransfer( dd, (DdManager *)pNtk->pManFunc, bFunc ); Cudd_Ref((DdNode *)pNode->pData);
+    pNode->pData = (DdNode *)Cudd_bddTransfer( dd, (DdManager *)pNtk->pManFunc, (DdNode *)bFunc ); Cudd_Ref((DdNode *)pNode->pData);
     Abc_NtkForEachPi( pNtk, pNodePi, i )
         Abc_ObjAddFanin( pNode, pNodePi );
     // create the only PO
@@ -246,7 +247,7 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose )
+void * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose )
 {
     ProgressBar * pProgress;
     Abc_Obj_t * pObj, * pFanin;
@@ -450,7 +451,7 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
             Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
     }
     // prepare the return value
-    bFunc = Abc_ObjGlobalBdd(pNode);
+    bFunc = (DdNode *)Abc_ObjGlobalBdd(pNode);
     // dereference BDD at the node
     if ( --pNode->vFanouts.nSize == 0 && fDropInternal )
     {
@@ -471,9 +472,9 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan ) 
+void * Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk, int fFreeMan ) 
 { 
-    return (DdManager *)Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, fFreeMan ); 
+    return Abc_NtkAttrFree( pNtk, VEC_ATTR_GLOBAL_BDD, fFreeMan ); 
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcOdc.c b/src/base/abci/abcOdc.c
index 5db556b8..50694832 100644
--- a/src/base/abci/abcOdc.c
+++ b/src/base/abci/abcOdc.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index 35c1ee29..154c5e1c 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -21,6 +21,7 @@
 #include "abc.h"
 #include "fraig.h"
 #include "math.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c
index 957d99b5..262797d2 100644
--- a/src/base/abci/abcQuant.c
+++ b/src/base/abci/abcQuant.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c
index 6eb7fb06..f7bc5186 100644
--- a/src/base/abci/abcReach.c
+++ b/src/base/abci/abcReach.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -103,7 +104,7 @@ DdNode ** Abc_NtkCreatePartitions( DdManager * dd, Abc_Ntk_t * pNtk, int fReorde
     Abc_NtkForEachLatch( pNtk, pNode, i )
     {
         bVar  = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
-        pbParts[i] = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) );  Cudd_Ref( pbParts[i] );
+        pbParts[i] = Cudd_bddXnor( dd, bVar, (DdNode *)Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) );  Cudd_Ref( pbParts[i] );
     }
     // free the global BDDs
     Abc_NtkFreeGlobalBdds( pNtk, 0 );
@@ -264,7 +265,7 @@ void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fP
     assert( Abc_ObjFanoutNum(Abc_NtkPo(pNtk,0)) == 0 ); // PO should go first
 
     // compute the global BDDs of the latches
-    dd = Abc_NtkBuildGlobalBdds( pNtk, nBddMax, 1, fReorder, fVerbose );    
+    dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddMax, 1, fReorder, fVerbose );    
     if ( dd == NULL )
     {
         printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax );
@@ -274,7 +275,7 @@ void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fP
         printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
 
     // save the output BDD
-    bOutput = Abc_ObjGlobalBdd(Abc_NtkPo(pNtk,0)); Cudd_Ref( bOutput );
+    bOutput = (DdNode *)Abc_ObjGlobalBdd(Abc_NtkPo(pNtk,0)); Cudd_Ref( bOutput );
 
     // create partitions
     pbParts = Abc_NtkCreatePartitions( dd, pNtk, fReorder, fVerbose );
diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c
index 434577ec..e0cec5cd 100644
--- a/src/base/abci/abcReconv.c
+++ b/src/base/abci/abcReconv.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 4e922ebd..3ba171b7 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "dec.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -187,7 +188,10 @@ pManRef->timeTotal = clock() - clkStart;
 ***********************************************************************/
 Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose )
 {
-    extern int            Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
+    extern DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
+    extern DdNode * Abc_NodeConeDcs( DdManager * dd, DdNode ** pbVarsX, DdNode ** pbVarsY, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, Vec_Ptr_t * vVisited );
+    extern char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode );
+    extern int    Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax );
     int fVeryVerbose = 0;
     Abc_Obj_t * pFanin;
     Dec_Graph_t * pFForm;
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index 4a63db67..719d722e 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "dec.h"
 #include "dsd.h"
 #include "cut.h"
@@ -317,6 +318,7 @@ Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_
 ***********************************************************************/
 Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut )
 {
+    extern DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
     Dec_Graph_t * pGraph;
     Dsd_Node_t * pNodeDsd;
     Abc_Obj_t * pLeaf;
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index a0a1af91..aab4d1ce 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "dec.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index f36600fa..54e19f50 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "rwr.h"
 #include "dec.h"
 
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index 12e94478..3e60ebf9 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "fraig.h"
+#include "extra.h"
 #include "sim.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 30c77e59..b0c5024a 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -834,7 +834,7 @@ int Abc_NodeAddClausesTop( sat_solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVa
 sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes )
 {
     sat_solver * pSat;
-    Extra_MmFlex_t * pMmFlex;
+    Mem_Flex_t * pMmFlex;
     Abc_Obj_t * pNode;
     Vec_Str_t * vCube;
     Vec_Int_t * vVars;
@@ -850,7 +850,7 @@ sat_solver * Abc_NtkMiterSatCreateLogic( Abc_Ntk_t * pNtk, int fAllPrimes )
     // start the data structures
     pSat    = sat_solver_new();
 sat_solver_store_alloc( pSat );
-    pMmFlex = Extra_MmFlexStart();
+    pMmFlex = Mem_FlexStart();
     vCube   = Vec_StrAlloc( 100 );
     vVars   = Vec_IntAlloc( 100 );
 
@@ -883,7 +883,7 @@ finish:
     // delete
     Vec_StrFree( vCube );
     Vec_IntFree( vVars );
-    Extra_MmFlexStop( pMmFlex );
+    Mem_FlexStop( pMmFlex, 0 );
     return pSat;
 }
 
diff --git a/src/base/abci/abcSense.c b/src/base/abci/abcSense.c
index cfecfaf3..8a477c4e 100644
--- a/src/base/abci/abcSense.c
+++ b/src/base/abci/abcSense.c
@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "fraig.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c
index 4e0a7373..41abc4db 100644
--- a/src/base/abci/abcSymm.c
+++ b/src/base/abci/abcSymm.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "sim.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -93,7 +94,7 @@ void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fReorder, int
 
     // compute the global functions
 clk = clock();
-    dd = Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, fReorder, fVerbose );
+    dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, fReorder, fVerbose );
     printf( "Shared BDD size = %d nodes.\n", Abc_NtkSizeOfGlobalBdds(pNtk) ); 
     Cudd_AutodynDisable( dd );
     if ( !fGarbCollect )
@@ -138,7 +139,7 @@ void Ntk_NetworkSymmsBdd( DdManager * dd, Abc_Ntk_t * pNtk, int fNaive, int fVer
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
 //      bFunc = pNtk->vFuncsGlob->pArray[i];
-        bFunc = Abc_ObjGlobalBdd( pNode );
+        bFunc = (DdNode *)Abc_ObjGlobalBdd( pNode );
         nSupps += Cudd_SupportSize( dd, bFunc );
         if ( Cudd_IsConstant(bFunc) )
             continue;
diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c
index b77eec63..829a83bd 100644
--- a/src/base/abci/abcUnate.c
+++ b/src/base/abci/abcUnate.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -76,14 +77,14 @@ void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose )
     int clkBdd, clkUnate;
 
     // compute the global BDDs
-    dd = Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, fVerbose);
+    dd = (DdManager *)Abc_NtkBuildGlobalBdds(pNtk, 10000000, 1, 1, fVerbose);
     if ( dd == NULL )
         return;
 clkBdd = clock() - clk;
 
     // get information about the network
 //    dd       = pNtk->pManGlob;
-//    dd       = Abc_NtkGlobalBddMan( pNtk );
+//    dd       = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
 //    pbGlobal = (DdNode **)Vec_PtrArray( pNtk->vFuncsGlob );
 
     // print the size of the BDDs
@@ -95,7 +96,7 @@ clkBdd = clock() - clk;
         Abc_NtkForEachCo( pNtk, pNode, i )
         {
 //            p = Extra_UnateComputeSlow( dd, pbGlobal[i] );
-            p = Extra_UnateComputeSlow( dd, Abc_ObjGlobalBdd(pNode) );
+            p = Extra_UnateComputeSlow( dd, (DdNode *)Abc_ObjGlobalBdd(pNode) );
             if ( fVerbose )
                 Extra_UnateInfoPrint( p );
             TotalSupps += p->nVars;
@@ -111,7 +112,7 @@ clkBdd = clock() - clk;
         Abc_NtkForEachCo( pNtk, pNode, i )
         {
 //            p = Extra_UnateComputeFast( dd, pbGlobal[i] );
-            p = Extra_UnateComputeFast( dd, Abc_ObjGlobalBdd(pNode) );
+            p = Extra_UnateComputeFast( dd, (DdNode *)Abc_ObjGlobalBdd(pNode) );
             if ( fVerbose )
                 Extra_UnateInfoPrint( p );
             TotalSupps += p->nVars;
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index ae7fbd02..f62ec7fc 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -61,7 +62,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, int fVerbose )
     }
 
     // compute the global BDDs of the latches
-    dd = Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );    
+    dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, 10000000, 1, 1, fVerbose );    
     if ( dd == NULL )
         return 0;
     if ( fVerbose )
@@ -141,7 +142,7 @@ DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbo
     {
         bVar  = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
 //        bProd = Cudd_bddXnor( dd, bVar, pNtk->vFuncsGlob->pArray[i] );  Cudd_Ref( bProd );
-        bProd = Cudd_bddXnor( dd, bVar, Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) );  Cudd_Ref( bProd );
+        bProd = Cudd_bddXnor( dd, bVar, (DdNode *)Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) );  Cudd_Ref( bProd );
         bRel  = Cudd_bddAnd( dd, bTemp = bRel, bProd );                 Cudd_Ref( bRel );
         Cudd_RecursiveDeref( dd, bTemp ); 
         Cudd_RecursiveDeref( dd, bProd ); 
diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h
index b1835dbf..1c75db54 100644
--- a/src/base/io/ioAbc.h
+++ b/src/base/io/ioAbc.h
@@ -27,6 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include "abc.h"
+#include "extra.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
diff --git a/src/base/io/ioReadBblif.c b/src/base/io/ioReadBblif.c
index e2fcca43..5b15c9d4 100644
--- a/src/base/io/ioReadBblif.c
+++ b/src/base/io/ioReadBblif.c
@@ -73,7 +73,7 @@ Abc_Ntk_t * Bbl_ManToAbc( Bbl_Man_t * p )
             pObjNew = Abc_NtkCreateNode( pNtk );
         else assert( 0 );
         if ( Bbl_ObjIsLut(pObj) )
-            pObjNew->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, Bbl_ObjSop(p, pObj) );
+            pObjNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, Bbl_ObjSop(p, pObj) );
         Vec_PtrSetEntry( vCopy, Bbl_ObjId(pObj), pObjNew );
     }
     // connect objects
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 681a4e36..0f60bb7f 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -176,12 +176,12 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
                 if ( Extra_TruthIsConst0(uTruth, nNames) )
                 {
                     pNode = Io_ReadCreateNode( pNtk, (char *)vTokens->pArray[0], ppNames, 0 );
-                    Abc_ObjSetData( pNode, Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, " 0\n" ) );
+                    Abc_ObjSetData( pNode, Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 0\n" ) );
                 }
                 else if ( Extra_TruthIsConst1(uTruth, nNames) )
                 {
                     pNode = Io_ReadCreateNode( pNtk, (char *)vTokens->pArray[0], ppNames, 0 );
-                    Abc_ObjSetData( pNode, Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, " 1\n" ) );
+                    Abc_ObjSetData( pNode, Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 1\n" ) );
                 }
                 else
                 {
@@ -189,11 +189,11 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
                     pNode = Io_ReadCreateNode( pNtk, (char *)vTokens->pArray[0], ppNames, nNames );
                     assert( nNames > 0 );
                     if ( nNames > 1 )
-                        Abc_ObjSetData( pNode, Abc_SopCreateFromTruth((Extra_MmFlex_t *)pNtk->pManFunc, nNames, uTruth) );
+                        Abc_ObjSetData( pNode, Abc_SopCreateFromTruth((Mem_Flex_t *)pNtk->pManFunc, nNames, uTruth) );
                     else if ( pString[0] == '2' )
-                        Abc_ObjSetData( pNode, Abc_SopCreateBuf((Extra_MmFlex_t *)pNtk->pManFunc) );
+                        Abc_ObjSetData( pNode, Abc_SopCreateBuf((Mem_Flex_t *)pNtk->pManFunc) );
                     else if ( pString[0] == '1' )
-                        Abc_ObjSetData( pNode, Abc_SopCreateInv((Extra_MmFlex_t *)pNtk->pManFunc) );
+                        Abc_ObjSetData( pNode, Abc_SopCreateInv((Mem_Flex_t *)pNtk->pManFunc) );
                     else
                     {
                         printf( "%s: Reading truth table (%s) of single-input node has failed.\n", Extra_FileReaderGetFileName(p), pString );
@@ -211,28 +211,28 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p )
                 pNode = Io_ReadCreateNode( pNtk, (char *)vTokens->pArray[0], ppNames, nNames );
                 // assign the cover
                 if ( strcmp(pType, "AND") == 0 )
-                    Abc_ObjSetData( pNode, Abc_SopCreateAnd((Extra_MmFlex_t *)pNtk->pManFunc, nNames, NULL) );
+                    Abc_ObjSetData( pNode, Abc_SopCreateAnd((Mem_Flex_t *)pNtk->pManFunc, nNames, NULL) );
                 else if ( strcmp(pType, "OR") == 0 )
-                    Abc_ObjSetData( pNode, Abc_SopCreateOr((Extra_MmFlex_t *)pNtk->pManFunc, nNames, NULL) );
+                    Abc_ObjSetData( pNode, Abc_SopCreateOr((Mem_Flex_t *)pNtk->pManFunc, nNames, NULL) );
                 else if ( strcmp(pType, "NAND") == 0 )
-                    Abc_ObjSetData( pNode, Abc_SopCreateNand((Extra_MmFlex_t *)pNtk->pManFunc, nNames) );
+                    Abc_ObjSetData( pNode, Abc_SopCreateNand((Mem_Flex_t *)pNtk->pManFunc, nNames) );
                 else if ( strcmp(pType, "NOR") == 0 )
-                    Abc_ObjSetData( pNode, Abc_SopCreateNor((Extra_MmFlex_t *)pNtk->pManFunc, nNames) );
+                    Abc_ObjSetData( pNode, Abc_SopCreateNor((Mem_Flex_t *)pNtk->pManFunc, nNames) );
                 else if ( strcmp(pType, "XOR") == 0 )
-                    Abc_ObjSetData( pNode, Abc_SopCreateXor((Extra_MmFlex_t *)pNtk->pManFunc, nNames) );
+                    Abc_ObjSetData( pNode, Abc_SopCreateXor((Mem_Flex_t *)pNtk->pManFunc, nNames) );
                 else if ( strcmp(pType, "NXOR") == 0 || strcmp(pType, "XNOR") == 0 )
-                    Abc_ObjSetData( pNode, Abc_SopCreateNxor((Extra_MmFlex_t *)pNtk->pManFunc, nNames) );
+                    Abc_ObjSetData( pNode, Abc_SopCreateNxor((Mem_Flex_t *)pNtk->pManFunc, nNames) );
                 else if ( strncmp(pType, "BUF", 3) == 0 )
-                    Abc_ObjSetData( pNode, Abc_SopCreateBuf((Extra_MmFlex_t *)pNtk->pManFunc) );
+                    Abc_ObjSetData( pNode, Abc_SopCreateBuf((Mem_Flex_t *)pNtk->pManFunc) );
                 else if ( strcmp(pType, "NOT") == 0 )
-                    Abc_ObjSetData( pNode, Abc_SopCreateInv((Extra_MmFlex_t *)pNtk->pManFunc) );
+                    Abc_ObjSetData( pNode, Abc_SopCreateInv((Mem_Flex_t *)pNtk->pManFunc) );
                 else if ( strncmp(pType, "MUX", 3) == 0 )
 //                    Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "1-0 1\n-11 1\n") );
-                    Abc_ObjSetData( pNode, Abc_SopRegister((Extra_MmFlex_t *)pNtk->pManFunc, "0-1 1\n11- 1\n") );
+                    Abc_ObjSetData( pNode, Abc_SopRegister((Mem_Flex_t *)pNtk->pManFunc, "0-1 1\n11- 1\n") );
                 else if ( strncmp(pType, "gnd", 3) == 0 )
-                    Abc_ObjSetData( pNode, Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, " 0\n" ) );
+                    Abc_ObjSetData( pNode, Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 0\n" ) );
                 else if ( strncmp(pType, "vdd", 3) == 0 )
-                    Abc_ObjSetData( pNode, Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, " 1\n" ) );
+                    Abc_ObjSetData( pNode, Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 1\n" ) );
                 else
                 {
                     printf( "Io_ReadBenchNetwork(): Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) );
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 06920afe..2093df3c 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -285,7 +285,7 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
         {
             pNtk->ntkType = ABC_NTK_NETLIST;
             pNtk->ntkFunc = ABC_FUNC_BLACKBOX;
-            Extra_MmFlexStop( (Extra_MmFlex_t *)pNtk->pManFunc );
+            Mem_FlexStop( (Mem_Flex_t *)pNtk->pManFunc, 0 );
             pNtk->pManFunc = NULL;
         }
         else
@@ -510,7 +510,7 @@ int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens )
     Vec_StrPush( p->vCubes, 0 );
 
     // set the pointer to the functionality of the node
-    Abc_ObjSetData( pNode, Abc_SopRegister((Extra_MmFlex_t *)pNtk->pManFunc, p->vCubes->pArray) );
+    Abc_ObjSetData( pNode, Abc_SopRegister((Mem_Flex_t *)pNtk->pManFunc, p->vCubes->pArray) );
 
     // check the size
     if ( Abc_ObjFaninNum(pNode) != Abc_SopGetVarNum((char *)Abc_ObjData(pNode)) )
@@ -645,7 +645,7 @@ int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
     {
         assert( p->pNtkCur->ntkFunc == ABC_FUNC_SOP );
         p->pNtkCur->ntkFunc = ABC_FUNC_MAP;
-        Extra_MmFlexStop( (Extra_MmFlex_t *)p->pNtkCur->pManFunc );
+        Mem_FlexStop( (Mem_Flex_t *)p->pNtkCur->pManFunc, 0 );
         p->pNtkCur->pManFunc = pGenlib;
     }
 
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index cc8bff17..0e121b47 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -813,7 +813,7 @@ static Abc_Lib_t * Io_MvParse( Io_MvMan_t * p )
         {
             if ( pMod->pNtk->ntkFunc == ABC_FUNC_SOP )
             {
-                Extra_MmFlexStop( (Extra_MmFlex_t *)pMod->pNtk->pManFunc );
+                Mem_FlexStop( (Mem_Flex_t *)pMod->pNtk->pManFunc, 0 );
                 pMod->pNtk->pManFunc = NULL;
                 pMod->pNtk->ntkFunc = ABC_FUNC_BLACKBOX;
             }
@@ -1248,7 +1248,7 @@ static int Io_MvParseLineSubckt( Io_MvMod_t * p, char * pLine )
         if ( k == nEquals )
         {
             Abc_Obj_t * pNode = Abc_NtkCreateNode( p->pNtk );
-            pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)p->pNtk->pManFunc, " 0\n" );
+            pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, " 0\n" );
             pNet = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pNode, "abc") );
             Abc_ObjAddFanin( pNet, pNode );
             pTerm = Abc_NtkCreateBi( p->pNtk );
@@ -1362,7 +1362,7 @@ static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine )
     Vec_Ptr_t * vTokens = p->pMan->vTokens;
     Abc_Obj_t * pObj;
     Io_MvVar_t * pVar = NULL;
-    Extra_MmFlex_t * pFlex;
+    Mem_Flex_t * pFlex;
     char * pName;
     int nCommas, nValues, i, k;
     // count commas and get the tokens
@@ -1393,22 +1393,22 @@ static int Io_MvParseLineMv( Io_MvMod_t * p, char * pLine )
         return 0;
     }
     // go through variables
-    pFlex = (Extra_MmFlex_t *)Abc_NtkMvVarMan( p->pNtk );
+    pFlex = (Mem_Flex_t *)Abc_NtkMvVarMan( p->pNtk );
     for ( i = 0; i <= nCommas; i++ )
     {
         pName = (char *)Vec_PtrEntry( vTokens, i+1 );
         pObj = Abc_NtkFindOrCreateNet( p->pNtk, pName );
         // allocate variable
-        pVar = (Io_MvVar_t *)Extra_MmFlexEntryFetch( pFlex, sizeof(Io_MvVar_t) );
+        pVar = (Io_MvVar_t *)Mem_FlexEntryFetch( pFlex, sizeof(Io_MvVar_t) );
         pVar->nValues = nValues;
         pVar->pNames = NULL;
         // create names
         if ( Vec_PtrSize(vTokens) > nCommas + 3 )
         {
-            pVar->pNames = (char **)Extra_MmFlexEntryFetch( pFlex, sizeof(char *) * nValues );
+            pVar->pNames = (char **)Mem_FlexEntryFetch( pFlex, sizeof(char *) * nValues );
             Vec_PtrForEachEntryStart( char *, vTokens, pName, k, nCommas + 3 )
             {
-                pVar->pNames[k-(nCommas + 3)] = (char *)Extra_MmFlexEntryFetch( pFlex, strlen(pName) + 1 );
+                pVar->pNames[k-(nCommas + 3)] = (char *)Mem_FlexEntryFetch( pFlex, strlen(pName) + 1 );
                 strcpy( pVar->pNames[k-(nCommas + 3)], pName );
             }
         }
@@ -1640,10 +1640,10 @@ static Abc_Obj_t * Io_MvParseAddResetCircuit( Io_MvMod_t * p, char * pName )
 //        int nValues = Abc_ObjMvVarNum(pOutNet);
 //        sprintf( Buffer, "2 %d %d %d\n1 - - =1\n0 - - =2\n", nValues, nValues, nValues );
         sprintf( Buffer, "1 - - =1\n0 - - =2\n" );
-        pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)p->pNtk->pManFunc, Buffer );
+        pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, Buffer );
     }
     else
-        pNode->pData = Abc_SopCreateMux( (Extra_MmFlex_t *)p->pNtk->pManFunc );
+        pNode->pData = Abc_SopCreateMux( (Mem_Flex_t *)p->pNtk->pManFunc );
     // add nets
     Abc_ObjAddFanin( pNode, pResetLONet );
     Abc_ObjAddFanin( pNode, pData1Net );
@@ -1704,7 +1704,7 @@ static int Io_MvParseLineNamesMvOne( Io_MvMod_t * p, Vec_Ptr_t * vTokens, Vec_Pt
     pNode->pData = Io_MvParseTableMv( p, pNode, vTokens2, nInputs, nOutputs, iOut );
     if ( pNode->pData == NULL )
         return 0;
-    pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)p->pNtk->pManFunc, (char *)pNode->pData );
+    pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, (char *)pNode->pData );
 //printf( "Finished parsing node \"%s\" with table:\n%s\n", pName, pNode->pData );
     return 1;
 }
@@ -1826,7 +1826,7 @@ static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins )
     // get the tokens
     Io_MvSplitIntoTokens( vTokens, pTable, '.' );
     if ( Vec_PtrSize(vTokens) == 0 )
-        return Abc_SopCreateConst0( (Extra_MmFlex_t *)p->pNtk->pManFunc );
+        return Abc_SopCreateConst0( (Mem_Flex_t *)p->pNtk->pManFunc );
     if ( Vec_PtrSize(vTokens) == 1 )
     {
         pOutput = (char *)Vec_PtrEntry( vTokens, 0 );
@@ -1836,7 +1836,7 @@ static char * Io_MvParseTableBlif( Io_MvMod_t * p, char * pTable, int nFanins )
             sprintf( p->pMan->sError, "Line %d: Constant table has wrong output value \"%s\".", Io_MvGetLine(p->pMan, pOutput), pOutput );
             return NULL;
         }
-        return pOutput[0] == '0' ? Abc_SopCreateConst0((Extra_MmFlex_t *)p->pNtk->pManFunc) : Abc_SopCreateConst1((Extra_MmFlex_t *)p->pNtk->pManFunc);
+        return pOutput[0] == '0' ? Abc_SopCreateConst0((Mem_Flex_t *)p->pNtk->pManFunc) : Abc_SopCreateConst1((Mem_Flex_t *)p->pNtk->pManFunc);
     }
     pProduct = (char *)Vec_PtrEntry( vTokens, 0 );
     if ( Vec_PtrSize(vTokens) % 2 == 1 )
@@ -1914,7 +1914,7 @@ static int Io_MvParseLineNamesBlif( Io_MvMod_t * p, char * pLine )
     pNode->pData = Io_MvParseTableBlif( p, pName + strlen(pName), Abc_ObjFaninNum(pNode) );
     if ( pNode->pData == NULL )
         return 0;
-    pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)p->pNtk->pManFunc, (char *)pNode->pData );
+    pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, (char *)pNode->pData );
     return 1;
 }
 
@@ -1953,7 +1953,7 @@ static int Io_MvParseLineShortBlif( Io_MvMod_t * p, char * pLine )
     // create fanins
     pNode = Io_ReadCreateNode( p->pNtk, pName, (char **)(vTokens->pArray + 1), 1 );
     // parse the table of this node
-    pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)p->pNtk->pManFunc, "1 1\n" );
+    pNode->pData = Abc_SopRegister( (Mem_Flex_t *)p->pNtk->pManFunc, "1 1\n" );
     return 1;
 }
 
@@ -1970,22 +1970,22 @@ static int Io_MvParseLineShortBlif( Io_MvMod_t * p, char * pLine )
 ***********************************************************************/
 Io_MvVar_t * Abc_NtkMvVarDup( Abc_Ntk_t * pNtk, Io_MvVar_t * pVar )
 {
-    Extra_MmFlex_t * pFlex;
+    Mem_Flex_t * pFlex;
     Io_MvVar_t * pVarDup;
     int i;
     if ( pVar == NULL )
         return NULL;
-    pFlex = (Extra_MmFlex_t *)Abc_NtkMvVarMan( pNtk );
+    pFlex = (Mem_Flex_t *)Abc_NtkMvVarMan( pNtk );
     assert( pFlex != NULL );
-    pVarDup = (Io_MvVar_t *)Extra_MmFlexEntryFetch( pFlex, sizeof(Io_MvVar_t) );
+    pVarDup = (Io_MvVar_t *)Mem_FlexEntryFetch( pFlex, sizeof(Io_MvVar_t) );
     pVarDup->nValues = pVar->nValues;
     pVarDup->pNames = NULL;
     if ( pVar->pNames == NULL )
         return pVarDup;
-    pVarDup->pNames = (char **)Extra_MmFlexEntryFetch( pFlex, sizeof(char *) * pVar->nValues );
+    pVarDup->pNames = (char **)Mem_FlexEntryFetch( pFlex, sizeof(char *) * pVar->nValues );
     for ( i = 0; i < pVar->nValues; i++ )
     {
-        pVarDup->pNames[i] = (char *)Extra_MmFlexEntryFetch( pFlex, strlen(pVar->pNames[i]) + 1 );
+        pVarDup->pNames[i] = (char *)Mem_FlexEntryFetch( pFlex, strlen(pVar->pNames[i]) + 1 );
         strcpy( pVarDup->pNames[i], pVar->pNames[i] );
     }
     return pVarDup;
@@ -2070,7 +2070,7 @@ static int Io_MvParseLineGateBlif( Io_MvMod_t * p, Vec_Ptr_t * vTokens )
     {
         assert( p->pNtk->ntkFunc == ABC_FUNC_SOP );
         p->pNtk->ntkFunc = ABC_FUNC_MAP;
-        Extra_MmFlexStop( (Extra_MmFlex_t *)p->pNtk->pManFunc );
+        Mem_FlexStop( (Mem_Flex_t *)p->pNtk->pManFunc, 0 );
         p->pNtk->pManFunc = pGenlib;
     }
 
diff --git a/src/base/io/ioReadDsd.c b/src/base/io/ioReadDsd.c
index 35bc6aaa..3608507b 100644
--- a/src/base/io/ioReadDsd.c
+++ b/src/base/io/ioReadDsd.c
@@ -186,11 +186,11 @@ Abc_Obj_t * Io_ReadDsd_rec( Abc_Ntk_t * pNtk, char * pCur, char * pSop )
             }
         }
         if ( pSop )
-            pObj->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, pSop );
+            pObj->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, pSop );
         else if ( TypeExor )
-            pObj->pData = Abc_SopCreateXorSpecial( (Extra_MmFlex_t *)pNtk->pManFunc, nParts );
+            pObj->pData = Abc_SopCreateXorSpecial( (Mem_Flex_t *)pNtk->pManFunc, nParts );
         else
-            pObj->pData = Abc_SopCreateAnd( (Extra_MmFlex_t *)pNtk->pManFunc, nParts, NULL );
+            pObj->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtk->pManFunc, nParts, NULL );
         return pObj;
     }
     if ( *pCur >= 'a' && *pCur <= 'z' )
diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c
index 8c739e61..5590ec80 100644
--- a/src/base/io/ioReadEdif.c
+++ b/src/base/io/ioReadEdif.c
@@ -198,21 +198,21 @@ Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p )
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
         if ( strncmp( (char *)pObj->pData, "And", 3 ) == 0 )
-            Abc_ObjSetData( pObj, Abc_SopCreateAnd((Extra_MmFlex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
+            Abc_ObjSetData( pObj, Abc_SopCreateAnd((Mem_Flex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
         else if ( strncmp( (char *)pObj->pData, "Or", 2 ) == 0 )
-            Abc_ObjSetData( pObj, Abc_SopCreateOr((Extra_MmFlex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
+            Abc_ObjSetData( pObj, Abc_SopCreateOr((Mem_Flex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj), NULL) );
         else if ( strncmp( (char *)pObj->pData, "Nand", 4 ) == 0 )
-            Abc_ObjSetData( pObj, Abc_SopCreateNand((Extra_MmFlex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+            Abc_ObjSetData( pObj, Abc_SopCreateNand((Mem_Flex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
         else if ( strncmp( (char *)pObj->pData, "Nor", 3 ) == 0 )
-            Abc_ObjSetData( pObj, Abc_SopCreateNor((Extra_MmFlex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+            Abc_ObjSetData( pObj, Abc_SopCreateNor((Mem_Flex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
         else if ( strncmp( (char *)pObj->pData, "Exor", 4 ) == 0 )
-            Abc_ObjSetData( pObj, Abc_SopCreateXor((Extra_MmFlex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+            Abc_ObjSetData( pObj, Abc_SopCreateXor((Mem_Flex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
         else if ( strncmp( (char *)pObj->pData, "Exnor", 5 ) == 0 )
-            Abc_ObjSetData( pObj, Abc_SopCreateNxor((Extra_MmFlex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
+            Abc_ObjSetData( pObj, Abc_SopCreateNxor((Mem_Flex_t *)pNtk->pManFunc, Abc_ObjFaninNum(pObj)) );
         else if ( strncmp( (char *)pObj->pData, "Inv", 3 ) == 0 )
-            Abc_ObjSetData( pObj, Abc_SopCreateInv((Extra_MmFlex_t *)pNtk->pManFunc) );
+            Abc_ObjSetData( pObj, Abc_SopCreateInv((Mem_Flex_t *)pNtk->pManFunc) );
         else if ( strncmp( (char *)pObj->pData, "Buf", 3 ) == 0 )
-            Abc_ObjSetData( pObj, Abc_SopCreateBuf((Extra_MmFlex_t *)pNtk->pManFunc) );
+            Abc_ObjSetData( pObj, Abc_SopCreateBuf((Mem_Flex_t *)pNtk->pManFunc) );
         else
         {
             printf( "%s: Unknown gate type \"%s\".\n", Extra_FileReaderGetFileName(p), (char*)pObj->pData );
diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c
index 63ffa296..36d44c68 100644
--- a/src/base/io/ioReadPla.c
+++ b/src/base/io/ioReadPla.c
@@ -254,12 +254,12 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros )
         if ( ppSops[i]->nSize == 0 )
         {
             Abc_ObjRemoveFanins(pNode);
-            pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, " 0\n" );
+            pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 0\n" );
             Vec_StrFree( ppSops[i] );
             continue;
         }
         Vec_StrPush( ppSops[i], 0 );
-        pNode->pData = Abc_SopRegister( (Extra_MmFlex_t *)pNtk->pManFunc, ppSops[i]->pArray );
+        pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, ppSops[i]->pArray );
         Vec_StrFree( ppSops[i] );
     }
     ABC_FREE( ppSops );
diff --git a/src/base/ver/ver.h b/src/base/ver/ver.h
index ab679664..e421ff95 100644
--- a/src/base/ver/ver.h
+++ b/src/base/ver/ver.h
@@ -28,6 +28,7 @@
 
 #include <stdio.h>
 #include "abc.h"
+#include "extra.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
diff --git a/src/map/cov/cov.h b/src/map/cov/cov.h
index f8136a7f..80ef1925 100644
--- a/src/map/cov/cov.h
+++ b/src/map/cov/cov.h
@@ -22,6 +22,7 @@
 #define __COV_H__
 
 #include "abc.h"
+#include "extra.h"
 #include "covInt.h"
 
 
diff --git a/src/map/cov/covBuild.c b/src/map/cov/covBuild.c
index 3975c91d..6ca17583 100644
--- a/src/map/cov/covBuild.c
+++ b/src/map/cov/covBuild.c
@@ -82,7 +82,7 @@ Abc_Obj_t * Abc_NtkCovDeriveCube( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_Cub
         Vec_IntWriteEntry( vLits, i, Lit==1 );
         Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
     }
-    pNodeNew->pData = Abc_SopCreateAnd( (Extra_MmFlex_t *)pNtkNew->pManFunc, vLits->nSize, vLits->pArray );
+    pNodeNew->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtkNew->pManFunc, vLits->nSize, vLits->pArray );
     if ( fCompl )
         Abc_SopComplement( (char *)pNodeNew->pData );
     Vec_IntFree( vLits );
@@ -153,7 +153,7 @@ Abc_Obj_t * Abc_NtkCovDeriveNode_rec( Cov_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Ob
             pFaninNew = Abc_NtkCovDeriveCube( pNtkNew, pObj, pCube, vSupp, 0 );
             Abc_ObjAddFanin( pNodeNew, pFaninNew );
         }
-        pNodeNew->pData = Abc_SopCreateXorSpecial( (Extra_MmFlex_t *)pNtkNew->pManFunc, nCubes );
+        pNodeNew->pData = Abc_SopCreateXorSpecial( (Mem_Flex_t *)pNtkNew->pManFunc, nCubes );
     }
 /*
     printf( "Created node %d(%d) at level %d: ", pNodeNew->Id, pObj->Id, Level );
@@ -280,8 +280,8 @@ Abc_Obj_t * Abc_NtkCovDeriveCubeInv( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, Min_
 //        Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
         Abc_ObjAddFanin( pNodeNew, Abc_NtkCovDeriveInv( pNtkNew, pFanin, Lit==1 ) );
     }
-//    pNodeNew->pData = Abc_SopCreateAnd( (Extra_MmFlex_t *)pNtkNew->pManFunc, vLits->nSize, vLits->pArray );
-    pNodeNew->pData = Abc_SopCreateAnd( (Extra_MmFlex_t *)pNtkNew->pManFunc, vLits->nSize, NULL );
+//    pNodeNew->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtkNew->pManFunc, vLits->nSize, vLits->pArray );
+    pNodeNew->pData = Abc_SopCreateAnd( (Mem_Flex_t *)pNtkNew->pManFunc, vLits->nSize, NULL );
     Vec_IntFree( vLits );
     return pNodeNew;
 }
@@ -335,7 +335,7 @@ Abc_Obj_t * Abc_NtkCovDeriveNodeInv_rec( Cov_Man_t * p, Abc_Ntk_t * pNtkNew, Abc
             pFaninNew = Abc_NtkCovDeriveCubeInv( pNtkNew, pObj, pCube, vSupp );
             Abc_ObjAddFanin( pNodeNew, pFaninNew );
         }
-        pNodeNew->pData = Abc_SopCreateXorSpecial( (Extra_MmFlex_t *)pNtkNew->pManFunc, nCubes );
+        pNodeNew->pData = Abc_SopCreateXorSpecial( (Mem_Flex_t *)pNtkNew->pManFunc, nCubes );
     }
 
     pObj->pCopy = pNodeNew;
@@ -472,7 +472,7 @@ Abc_Obj_t * Abc_NtkCovDerive_rec( Cov_Man_t * p, Abc_Ntk_t * pNtkNew, Abc_Obj_t
         // derive the function
         vCover = Vec_StrAlloc( 100 );
         Min_CoverCreate( vCover, pCover, (char)Type );
-        pNodeNew->pData = Abc_SopRegister((Extra_MmFlex_t *)pNtkNew->pManFunc, Vec_StrArray(vCover) );
+        pNodeNew->pData = Abc_SopRegister((Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vCover) );
         Vec_StrFree( vCover );
     }
 
diff --git a/src/map/cov/covInt.h b/src/map/cov/covInt.h
index b2d293d4..73c6bc20 100644
--- a/src/map/cov/covInt.h
+++ b/src/map/cov/covInt.h
@@ -22,6 +22,7 @@
 #define __COV_INT_H__
 
 #include "abc.h"
+#include "extra.h"
 
 
 ABC_NAMESPACE_HEADER_START
diff --git a/src/map/mio/mioFunc.c b/src/map/mio/mioFunc.c
index e58d3958..c14944c4 100644
--- a/src/map/mio/mioFunc.c
+++ b/src/map/mio/mioFunc.c
@@ -90,6 +90,7 @@ int Mio_LibraryParseFormulas( Mio_Library_t * pLib )
 ***********************************************************************/
 int Mio_GateParseFormula( Mio_Gate_t * pGate )
 {
+    extern char * Abc_ConvertBddToSop( Mem_Flex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, int fAllPrimes, Vec_Str_t * vCube, int fMode );
     DdManager * dd = pGate->pLib->dd;
     char * pPinNames[100];
     char * pPinNamesCopy[100];
@@ -114,13 +115,13 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate )
         if ( strcmp( pGate->pForm, MIO_STRING_CONST0 ) == 0 )
         {
             pGate->bFunc = b0;
-            pGate->pSop = Abc_SopRegister( (Extra_MmFlex_t *)pGate->pLib->pMmFlex, " 0\n" );
+            pGate->pSop = Abc_SopRegister( (Mem_Flex_t *)pGate->pLib->pMmFlex, " 0\n" );
             pGate->pLib->pGate0 = pGate;
         }
         else if ( strcmp( pGate->pForm, MIO_STRING_CONST1 ) == 0 )
         {
             pGate->bFunc = b1;
-            pGate->pSop = Abc_SopRegister( (Extra_MmFlex_t *)pGate->pLib->pMmFlex, " 1\n" );
+            pGate->pSop = Abc_SopRegister( (Mem_Flex_t *)pGate->pLib->pMmFlex, " 1\n" );
             pGate->pLib->pGate1 = pGate;
         }
         else
diff --git a/src/map/mio/mioInt.h b/src/map/mio/mioInt.h
index 35a583b6..87bd7d4e 100644
--- a/src/map/mio/mioInt.h
+++ b/src/map/mio/mioInt.h
@@ -25,6 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include "abc.h"
+#include "mem.h"
 #include "mvc.h"
 #include "main.h"
 #include "mio.h"
@@ -69,7 +70,7 @@ struct  Mio_LibraryStruct_t_
     Mio_Gate_t *       pGateAnd2;   // the AND2 gate
     st_table *         tName2Gate;  // the mapping of gate names into their pointer
     DdManager *        dd;          // the nanager storing functions of gates
-    Extra_MmFlex_t *   pMmFlex;     // the memory manaqer for SOPs
+    Mem_Flex_t *       pMmFlex;     // the memory manaqer for SOPs
     Vec_Str_t *        vCube;       // temporary cube
 }; 
 
diff --git a/src/map/mio/mioRead.c b/src/map/mio/mioRead.c
index 42c6d8bf..eb5d47ea 100644
--- a/src/map/mio/mioRead.c
+++ b/src/map/mio/mioRead.c
@@ -101,7 +101,7 @@ Mio_Library_t * Mio_LibraryReadOne( Abc_Frame_t * pAbc, char * FileName, int fEx
     memset( pLib, 0, sizeof(Mio_Library_t) );
     pLib->pName = Extra_UtilStrsav( FileName );
     pLib->tName2Gate = st_init_table(strcmp, st_strhash);
-    pLib->pMmFlex = Extra_MmFlexStart();
+    pLib->pMmFlex = Mem_FlexStart();
     pLib->vCube = Vec_StrAlloc( 100 );
 
     // read the file and clean comments
diff --git a/src/map/mio/mioUtils.c b/src/map/mio/mioUtils.c
index 0e8cbb03..d0d47060 100644
--- a/src/map/mio/mioUtils.c
+++ b/src/map/mio/mioUtils.c
@@ -56,7 +56,7 @@ void Mio_LibraryDelete( Mio_Library_t * pLib )
     ABC_FREE( pLib->pName );
     Mio_LibraryForEachGateSafe( pLib, pGate, pGate2 )
         Mio_GateDelete( pGate );
-    Extra_MmFlexStop( pLib->pMmFlex );
+    Mem_FlexStop( pLib->pMmFlex, 0 );
     Vec_StrFree( pLib->vCube );
     if ( pLib->tName2Gate )
         st_free_table( pLib->tName2Gate );
diff --git a/src/misc/st/stmm.c b/src/misc/st/stmm.c
index 1d4f65b4..1305d5b0 100644
--- a/src/misc/st/stmm.c
+++ b/src/misc/st/stmm.c
@@ -95,7 +95,7 @@ stmm_free_table (stmm_table *table)
     // no need to deallocate entries because they are in the memory manager now
     // added by alanmi
     if ( table->pMemMan )
-        Extra_MmFixedStop (table->pMemMan);
+        Extra_MmFixedStop ((Extra_MmFixed_t *)table->pMemMan);
     ABC_FREE(table->bins);
     ABC_FREE(table);
 }
@@ -111,7 +111,7 @@ stmm_clean (stmm_table *table)
     // reset the parameters
     table->num_entries = 0;
     // restart the memory manager
-    Extra_MmFixedRestart (table->pMemMan);
+    Extra_MmFixedRestart ((Extra_MmFixed_t *)table->pMemMan);
 }
 
 
@@ -187,7 +187,7 @@ stmm_lookup_int (stmm_table *table, char *key, int *value)
     hash_val = do_hash(key,table);\
     }\
     \
-    new = (stmm_table_entry *)Extra_MmFixedEntryFetch( table->pMemMan );\
+    new = (stmm_table_entry *)Extra_MmFixedEntryFetch( (Extra_MmFixed_t *)table->pMemMan );\
     \
     new->key = key;\
     new->record = value;\
@@ -216,7 +216,7 @@ stmm_insert (stmm_table *table, char *key, char *value)
     }
 
 //              newEntry = ABC_ALLOC( stmm_table_entry, 1 );
-    newEntry = (stmm_table_entry *) Extra_MmFixedEntryFetch (table->pMemMan);
+    newEntry = (stmm_table_entry *) Extra_MmFixedEntryFetch ((Extra_MmFixed_t *)table->pMemMan);
     if (newEntry == NULL) {
         return STMM_OUT_OF_MEM;
     }
@@ -249,7 +249,7 @@ stmm_add_direct (stmm_table *table, char *key, char *value)
     hash_val = do_hash (key, table);
 
 //      newEntry = ABC_ALLOC( stmm_table_entry, 1 );
-    newEntry = (stmm_table_entry *) Extra_MmFixedEntryFetch (table->pMemMan);
+    newEntry = (stmm_table_entry *) Extra_MmFixedEntryFetch ((Extra_MmFixed_t *)table->pMemMan);
     if (newEntry == NULL) {
     return STMM_OUT_OF_MEM;
     }
@@ -281,7 +281,7 @@ stmm_find_or_add (stmm_table *table, char *key, char ***slot)
     }
 
     // newEntry = ABC_ALLOC( stmm_table_entry, 1 );
-    newEntry = (stmm_table_entry *) Extra_MmFixedEntryFetch (table->pMemMan);
+    newEntry = (stmm_table_entry *) Extra_MmFixedEntryFetch ((Extra_MmFixed_t *)table->pMemMan);
     if (newEntry == NULL) {
         return STMM_OUT_OF_MEM;
     }
@@ -390,18 +390,14 @@ stmm_copy (stmm_table *old_table)
     }
 
     // allocate the memory manager for the newEntry table
-    newEntry_table->pMemMan =
-    Extra_MmFixedStart (sizeof (stmm_table_entry));
+    newEntry_table->pMemMan = Extra_MmFixedStart (sizeof (stmm_table_entry));
 
     for (i = 0; i < num_bins; i++) {
     newEntry_table->bins[i] = NULL;
     ptr = old_table->bins[i];
     while (ptr != NULL) {
 //                      newEntry = ABC_ALLOC( stmm_table_entry, 1 );
-        newEntry =
-        (stmm_table_entry *) Extra_MmFixedEntryFetch (newEntry_table->
-                                pMemMan);
-
+        newEntry = (stmm_table_entry *)Extra_MmFixedEntryFetch ((Extra_MmFixed_t *)newEntry_table->pMemMan);
         if (newEntry == NULL) {
 /*
                 for ( j = 0; j <= i; j++ )
@@ -415,7 +411,7 @@ stmm_copy (stmm_table *old_table)
                     }
                 }
 */
-        Extra_MmFixedStop (newEntry_table->pMemMan);
+        Extra_MmFixedStop ((Extra_MmFixed_t *)newEntry_table->pMemMan);
 
         ABC_FREE(newEntry_table->bins);
         ABC_FREE(newEntry_table);
@@ -450,7 +446,7 @@ stmm_delete (stmm_table *table, char **keyp, char **value)
      *value = ptr->record;
     *keyp = ptr->key;
 //      ABC_FREE( ptr );
-    Extra_MmFixedEntryRecycle (table->pMemMan, (char *) ptr);
+    Extra_MmFixedEntryRecycle ((Extra_MmFixed_t *)table->pMemMan, (char *) ptr);
 
     table->num_entries--;
     return 1;
@@ -476,7 +472,7 @@ stmm_delete_int (stmm_table *table, long *keyp, char **value)
      *value = ptr->record;
     *keyp = (long) ptr->key;
 //      ABC_FREE( ptr );
-    Extra_MmFixedEntryRecycle (table->pMemMan, (char *) ptr);
+    Extra_MmFixedEntryRecycle ((Extra_MmFixed_t *)table->pMemMan, (char *) ptr);
 
     table->num_entries--;
     return 1;
@@ -505,7 +501,7 @@ stmm_foreach (stmm_table *table, enum stmm_retval (*func) (char *, char *, char
         *last = ptr->next;
         table->num_entries--;    /* cstevens@ic */
 //                              ABC_FREE( ptr );
-        Extra_MmFixedEntryRecycle (table->pMemMan, (char *) ptr);
+        Extra_MmFixedEntryRecycle ((Extra_MmFixed_t *)table->pMemMan, (char *) ptr);
 
         ptr = *last;
         }
diff --git a/src/misc/st/stmm.h b/src/misc/st/stmm.h
index 7d2e3f3a..eee90073 100644
--- a/src/misc/st/stmm.h
+++ b/src/misc/st/stmm.h
@@ -14,8 +14,7 @@
 #ifndef STMM_INCLUDED
 #define STMM_INCLUDED
 
-
-#include "extra.h"
+#include "abc_global.h"
 
 ABC_NAMESPACE_HEADER_START
 
@@ -63,7 +62,7 @@ struct stmm_table
     stmm_table_entry **bins;
     // memory manager to improve runtime and prevent memory fragmentation
     // added by alanmi - January 16, 2003
-    Extra_MmFixed_t *pMemMan;
+    void * pMemMan;
 };
 
 struct stmm_generator
diff --git a/src/opt/dec/decFactor.c b/src/opt/dec/decFactor.c
index aa9d9c8a..06ccf9ca 100644
--- a/src/opt/dec/decFactor.c
+++ b/src/opt/dec/decFactor.c
@@ -366,7 +366,8 @@ Mvc_Cover_t * Dec_ConvertSopToMvc( char * pSop )
 ***********************************************************************/
 int Dec_FactorVerify( char * pSop, Dec_Graph_t * pFForm )
 {
-    extern DdNode *       Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph );
+    extern DdNode * Abc_ConvertSopToBdd( DdManager * dd, char * pSop );
+    extern DdNode * Dec_GraphDeriveBdd( DdManager * dd, Dec_Graph_t * pGraph );
     DdManager * dd = (DdManager *)Abc_FrameReadManDd();
     DdNode * bFunc1, * bFunc2;
     int RetValue;
diff --git a/src/opt/dec/decUtil.c b/src/opt/dec/decUtil.c
index adf216f6..d2b5631e 100644
--- a/src/opt/dec/decUtil.c
+++ b/src/opt/dec/decUtil.c
@@ -17,6 +17,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "dec.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h
index db855f3b..282b1d2b 100644
--- a/src/opt/fxu/fxu.h
+++ b/src/opt/fxu/fxu.h
@@ -60,7 +60,7 @@ struct FxuDataStruct
     Vec_Ptr_t *       vSopsNew;         // the SOPs for each node in the network after extraction
     Vec_Ptr_t *       vFaninsNew;       // the fanins of each node in the network after extraction
     // the SOP manager
-    Extra_MmFlex_t *  pManSop;
+    Mem_Flex_t *      pManSop;
     // statistics   
     int               nNodesOld;        // the old number of nodes
     int               nNodesNew;        // the number of divisors actually extracted
diff --git a/src/opt/fxu/fxuCreate.c b/src/opt/fxu/fxuCreate.c
index 3466b520..76c534e3 100644
--- a/src/opt/fxu/fxuCreate.c
+++ b/src/opt/fxu/fxuCreate.c
@@ -16,7 +16,6 @@
 
 ***********************************************************************/
 
-#include "abc.h"
 #include "fxuInt.h"
 #include "fxu.h"
 
diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h
index 96bec083..bbceac47 100644
--- a/src/opt/fxu/fxuInt.h
+++ b/src/opt/fxu/fxuInt.h
@@ -24,8 +24,8 @@
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
+#include "abc.h"
 #include "extra.h"
-#include "vec.h"
 
 ABC_NAMESPACE_HEADER_START
 
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 28a68bd8..650a154a 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -27,6 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include "abc.h"
+#include "extra.h"
 #include "mfs.h"
 #include "aig.h"
 #include "cnf.h"
diff --git a/src/opt/res/resSim.c b/src/opt/res/resSim.c
index 560acc43..740b7d0a 100644
--- a/src/opt/res/resSim.c
+++ b/src/opt/res/resSim.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "resInt.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/res/resStrash.c b/src/opt/res/resStrash.c
index 9740af4c..1ee84957 100644
--- a/src/opt/res/resStrash.c
+++ b/src/opt/res/resStrash.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "resInt.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/rwr/rwrDec.c b/src/opt/rwr/rwrDec.c
index 76d8ac51..a280f5f1 100644
--- a/src/opt/rwr/rwrDec.c
+++ b/src/opt/rwr/rwrDec.c
@@ -18,6 +18,7 @@
 
 ***********************************************************************/
 
+#include "extra.h"
 #include "rwr.h"
 #include "dec.h"
 
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index 8f0c1821..4dc6c082 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -18,6 +18,7 @@
 
 ***********************************************************************/
 
+#include "extra.h"
 #include "rwr.h"
 #include "dec.h"
 #include "ivy.h"
diff --git a/src/opt/rwr/rwrExp.c b/src/opt/rwr/rwrExp.c
index c4664fbf..fa75f066 100644
--- a/src/opt/rwr/rwrExp.c
+++ b/src/opt/rwr/rwrExp.c
@@ -18,6 +18,7 @@
 
 ***********************************************************************/
 
+#include "extra.h"
 #include "rwr.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/rwr/rwrLib.c b/src/opt/rwr/rwrLib.c
index 731871d0..a7c01047 100644
--- a/src/opt/rwr/rwrLib.c
+++ b/src/opt/rwr/rwrLib.c
@@ -18,6 +18,7 @@
 
 ***********************************************************************/
 
+#include "extra.h"
 #include "rwr.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index ffc5fcae..0f32c0da 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -18,6 +18,7 @@
 
 ***********************************************************************/
 
+#include "extra.h"
 #include "rwr.h"
 #include "main.h"
 #include "dec.h"
diff --git a/src/opt/rwr/rwrPrint.c b/src/opt/rwr/rwrPrint.c
index 11a084d3..5574df88 100644
--- a/src/opt/rwr/rwrPrint.c
+++ b/src/opt/rwr/rwrPrint.c
@@ -18,6 +18,7 @@
 
 ***********************************************************************/
 
+#include "extra.h"
 #include "rwr.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/rwr/rwrTemp.c b/src/opt/rwr/rwrTemp.c
index 6a670c3a..654e37c1 100644
--- a/src/opt/rwr/rwrTemp.c
+++ b/src/opt/rwr/rwrTemp.c
@@ -18,6 +18,7 @@
 
 ***********************************************************************/
 
+#include "extra.h"
 #include "rwr.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/rwr/rwrUtil.c b/src/opt/rwr/rwrUtil.c
index 7a836d63..7613691a 100644
--- a/src/opt/rwr/rwrUtil.c
+++ b/src/opt/rwr/rwrUtil.c
@@ -18,6 +18,7 @@
 
 ***********************************************************************/
 
+#include "extra.h"
 #include "rwr.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/sim/simMan.c b/src/opt/sim/simMan.c
index 234aa412..f3a9650b 100644
--- a/src/opt/sim/simMan.c
+++ b/src/opt/sim/simMan.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "sim.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/sim/simSat.c b/src/opt/sim/simSat.c
index 29fc6975..5654c493 100644
--- a/src/opt/sim/simSat.c
+++ b/src/opt/sim/simSat.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "sim.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/sim/simSeq.c b/src/opt/sim/simSeq.c
index db05226f..fd75ba8d 100644
--- a/src/opt/sim/simSeq.c
+++ b/src/opt/sim/simSeq.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "sim.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c
index 563f98ac..67ac5efe 100644
--- a/src/opt/sim/simSupp.c
+++ b/src/opt/sim/simSupp.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "fraig.h"
 #include "sim.h"
 
diff --git a/src/opt/sim/simSwitch.c b/src/opt/sim/simSwitch.c
index 4f675082..a9045ca1 100644
--- a/src/opt/sim/simSwitch.c
+++ b/src/opt/sim/simSwitch.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "sim.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/sim/simSym.c b/src/opt/sim/simSym.c
index d8a1eb4f..c6b588ac 100644
--- a/src/opt/sim/simSym.c
+++ b/src/opt/sim/simSym.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "sim.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c
index 4f6690e5..bdc8fbee 100644
--- a/src/opt/sim/simSymSat.c
+++ b/src/opt/sim/simSymSat.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "sim.h"
 #include "fraig.h"
 
diff --git a/src/opt/sim/simSymSim.c b/src/opt/sim/simSymSim.c
index 85ba56fb..af942a19 100644
--- a/src/opt/sim/simSymSim.c
+++ b/src/opt/sim/simSymSim.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "sim.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/sim/simSymStr.c b/src/opt/sim/simSymStr.c
index e9a25905..4d83dc61 100644
--- a/src/opt/sim/simSymStr.c
+++ b/src/opt/sim/simSymStr.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "sim.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/opt/sim/simUtils.c b/src/opt/sim/simUtils.c
index 25d4cd44..aa3fc8af 100644
--- a/src/opt/sim/simUtils.c
+++ b/src/opt/sim/simUtils.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "extra.h"
 #include "sim.h"
 
 ABC_NAMESPACE_IMPL_START
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index d49f75c0..78ed2601 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -41,7 +41,7 @@ struct ABC_ManagerStruct_t
     Abc_Ntk_t *           pNtk;          // the starting ABC network
     Abc_Ntk_t *           pTarget;       // the AIG representing the target
     char *                pDumpFileName; // the name of the file to dump the target network
-    Extra_MmFlex_t *      pMmNames;      // memory manager for signal names
+    Mem_Flex_t *      pMmNames;      // memory manager for signal names
     // solving parameters
     int                   mode;          // 0 = resource-aware integration; 1 = brute-force SAT
     Prove_Params_t        Params;        // integrated CEC parameters
@@ -88,7 +88,7 @@ ABC_Manager ABC_InitManager()
     mng->pNtk->pName = Extra_UtilStrsav("csat_network");
     mng->tName2Node = stmm_init_table(strcmp, stmm_strhash);
     mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
-    mng->pMmNames   = Extra_MmFlexStart();
+    mng->pMmNames   = Mem_FlexStart();
     mng->vNodes     = Vec_PtrAlloc( 100 );
     mng->vValues    = Vec_IntAlloc( 100 );
     mng->mode       = 0; // set "resource-aware integration" as the default mode
@@ -116,7 +116,7 @@ void ABC_ReleaseManager( ABC_Manager mng )
     ABC_TargetResFree(p_res);
     if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name );
     if ( mng->tName2Node ) stmm_free_table( mng->tName2Node );
-    if ( mng->pMmNames )   Extra_MmFlexStop( mng->pMmNames );
+    if ( mng->pMmNames )   Mem_FlexStop( mng->pMmNames, 0 );
     if ( mng->pNtk )       Abc_NtkDelete( mng->pNtk );
     if ( mng->pTarget )    Abc_NtkDelete( mng->pTarget );
     if ( mng->vNodes )     Vec_PtrFree( mng->vNodes );
@@ -181,7 +181,7 @@ int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, cha
     int i;
 
     // save the name in the local memory manager
-    pNewName = Extra_MmFlexEntryFetch( mng->pMmNames, strlen(name) + 1 );
+    pNewName = Mem_FlexEntryFetch( mng->pMmNames, strlen(name) + 1 );
     strcpy( pNewName, name );
     name = pNewName;
 
@@ -220,51 +220,51 @@ int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, cha
             case CSAT_CONST:
                 if ( nofi != 0 )
                     { printf( "ABC_AddGate: The constant gate \"%s\" has fanins.\n", name ); return 0; }
-                pSop = Abc_SopCreateConst1( (Extra_MmFlex_t *)mng->pNtk->pManFunc );
+                pSop = Abc_SopCreateConst1( (Mem_Flex_t *)mng->pNtk->pManFunc );
                 break;
             case CSAT_BAND:
                 if ( nofi < 1 )
                     { printf( "ABC_AddGate: The AND gate \"%s\" no fanins.\n", name ); return 0; }
-                pSop = Abc_SopCreateAnd( (Extra_MmFlex_t *)mng->pNtk->pManFunc, nofi, NULL );
+                pSop = Abc_SopCreateAnd( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi, NULL );
                 break;
             case CSAT_BNAND:
                 if ( nofi < 1 )
                     { printf( "ABC_AddGate: The NAND gate \"%s\" no fanins.\n", name ); return 0; }
-                pSop = Abc_SopCreateNand( (Extra_MmFlex_t *)mng->pNtk->pManFunc, nofi );
+                pSop = Abc_SopCreateNand( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi );
                 break;
             case CSAT_BOR:
                 if ( nofi < 1 )
                     { printf( "ABC_AddGate: The OR gate \"%s\" no fanins.\n", name ); return 0; }
-                pSop = Abc_SopCreateOr( (Extra_MmFlex_t *)mng->pNtk->pManFunc, nofi, NULL );
+                pSop = Abc_SopCreateOr( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi, NULL );
                 break;
             case CSAT_BNOR:
                 if ( nofi < 1 )
                     { printf( "ABC_AddGate: The NOR gate \"%s\" no fanins.\n", name ); return 0; }
-                pSop = Abc_SopCreateNor( (Extra_MmFlex_t *)mng->pNtk->pManFunc, nofi );
+                pSop = Abc_SopCreateNor( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi );
                 break;
             case CSAT_BXOR:
                 if ( nofi < 1 )
                     { printf( "ABC_AddGate: The XOR gate \"%s\" no fanins.\n", name ); return 0; }
                 if ( nofi > 2 )
                     { printf( "ABC_AddGate: The XOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
-                pSop = Abc_SopCreateXor( (Extra_MmFlex_t *)mng->pNtk->pManFunc, nofi );
+                pSop = Abc_SopCreateXor( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi );
                 break;
             case CSAT_BXNOR:
                 if ( nofi < 1 )
                     { printf( "ABC_AddGate: The XNOR gate \"%s\" no fanins.\n", name ); return 0; }
                 if ( nofi > 2 )
                     { printf( "ABC_AddGate: The XNOR gate \"%s\" has more than two fanins.\n", name ); return 0; }
-                pSop = Abc_SopCreateNxor( (Extra_MmFlex_t *)mng->pNtk->pManFunc, nofi );
+                pSop = Abc_SopCreateNxor( (Mem_Flex_t *)mng->pNtk->pManFunc, nofi );
                 break;
             case CSAT_BINV:
                 if ( nofi != 1 )
                     { printf( "ABC_AddGate: The inverter gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
-                pSop = Abc_SopCreateInv( (Extra_MmFlex_t *)mng->pNtk->pManFunc );
+                pSop = Abc_SopCreateInv( (Mem_Flex_t *)mng->pNtk->pManFunc );
                 break;
             case CSAT_BBUF:
                 if ( nofi != 1 )
                     { printf( "ABC_AddGate: The buffer gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
-                pSop = Abc_SopCreateBuf( (Extra_MmFlex_t *)mng->pNtk->pManFunc );
+                pSop = Abc_SopCreateBuf( (Mem_Flex_t *)mng->pNtk->pManFunc );
                 break;
             default :
                 break;