Major restructuring of the code.

27 files changed, 149 insertions, 208 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 2ed3c130..ad8ce927 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#ifndef __AIG_H__
-#define __AIG_H__
+#ifndef ABC__aig__aig__aig_h
+#define ABC__aig__aig__aig_h
 
 
 ////////////////////////////////////////////////////////////////////////
@@ -32,8 +32,8 @@
 #include <assert.h>
 #include <time.h>
 
-#include "vec.h"
-#include "utilCex.h"
+#include "src/misc/vec/vec.h"
+#include "src/misc/util/utilCex.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -222,20 +222,6 @@ static inline Aig_Cut_t *  Aig_CutNext( Aig_Cut_t * pCut )              { return
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int          Aig_IntAbs( int n )                    { return (n < 0)? -n : n;                                }
-//static inline int          Aig_Float2Int( float Val )             { return *((int *)&Val);                                 }
-//static inline float        Aig_Int2Float( int Num )               { return *((float *)&Num);                               }
-static inline int          Aig_Float2Int( float Val )             { union { int x; float y; } v; v.y = Val; return v.x;    }
-static inline float        Aig_Int2Float( int Num )               { union { int x; float y; } v; v.x = Num; return v.y;    }
-static inline int          Aig_Base2Log( unsigned n )             { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
-static inline int          Aig_Base10Log( unsigned n )            { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
-static inline char *       Aig_UtilStrsav( char * s )             { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL; }
-static inline int          Aig_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);                  }
-static inline int          Aig_TruthWordNum( int nVars )          { return nVars <= 5 ? 1 : (1 << (nVars - 5));            }
-static inline int          Aig_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0;              }
-static inline void         Aig_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));                          }
-static inline void         Aig_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));                          }
-static inline unsigned     Aig_InfoMask( int nVar )               { return (~(unsigned)0) >> (32-nVar);                    }
 static inline unsigned     Aig_ObjCutSign( unsigned ObjId )       { return (1 << (ObjId & 31));                            }
 static inline int          Aig_WordCountOnes( unsigned uWord )
 {
@@ -254,13 +240,6 @@ static inline int          Aig_WordFindFirstBit( unsigned uWord )
     return -1;
 }
 
-static inline int          Aig_Var2Lit( int Var, int fCompl )     { return Var + Var + fCompl;                       }
-static inline int          Aig_Lit2Var( int Lit )                 { return Lit >> 1;                                 }
-static inline int          Aig_LitIsCompl( int Lit )              { return Lit & 1;                                  }
-static inline int          Aig_LitNot( int Lit )                  { return Lit ^ 1;                                  }
-static inline int          Aig_LitNotCond( int Lit, int c )       { return Lit ^ (int)(c > 0);                       }
-static inline int          Aig_LitRegular( int Lit )              { return Lit & ~01;                                }
-
 static inline Aig_Obj_t *  Aig_Regular( Aig_Obj_t * p )           { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) & ~01);  }
 static inline Aig_Obj_t *  Aig_Not( Aig_Obj_t * p )               { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^  01);  }
 static inline Aig_Obj_t *  Aig_NotCond( Aig_Obj_t * p, int c )    { return (Aig_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c));  }
@@ -335,10 +314,10 @@ static inline void         Aig_ObjChild1Flip( Aig_Obj_t * pObj )  { assert( !Aig
 static inline Aig_Obj_t *  Aig_ObjCopy( Aig_Obj_t * pObj )        { assert( !Aig_IsComplement(pObj) ); return (Aig_Obj_t *)pObj->pData;               } 
 static inline void         Aig_ObjSetCopy( Aig_Obj_t * pObj, Aig_Obj_t * pCopy )     {  assert( !Aig_IsComplement(pObj) ); pObj->pData = pCopy;       } 
 static inline Aig_Obj_t *  Aig_ObjRealCopy( Aig_Obj_t * pObj )    { return Aig_NotCond((Aig_Obj_t *)Aig_Regular(pObj)->pData, Aig_IsComplement(pObj));}
-static inline int          Aig_ObjToLit( Aig_Obj_t * pObj )       { return Aig_Var2Lit( Aig_ObjId(Aig_Regular(pObj)), Aig_IsComplement(pObj) );       }
-static inline Aig_Obj_t *  Aig_ObjFromLit( Aig_Man_t * p,int iLit){ return Aig_NotCond( Aig_ManObj(p, Aig_Lit2Var(iLit)), Aig_LitIsCompl(iLit) );     }
+static inline int          Aig_ObjToLit( Aig_Obj_t * pObj )       { return Abc_Var2Lit( Aig_ObjId(Aig_Regular(pObj)), Aig_IsComplement(pObj) );       }
+static inline Aig_Obj_t *  Aig_ObjFromLit( Aig_Man_t * p,int iLit){ return Aig_NotCond( Aig_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) );     }
 static inline int          Aig_ObjLevel( Aig_Obj_t * pObj )       { assert( !Aig_IsComplement(pObj) ); return pObj->Level;                            }
-static inline int          Aig_ObjLevelNew( Aig_Obj_t * pObj )    { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + ABC_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
+static inline int          Aig_ObjLevelNew( Aig_Obj_t * pObj )    { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + Abc_MaxInt(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
 static inline int          Aig_ObjSetLevel( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return pObj->Level = i;                    }
 static inline void         Aig_ObjClean( Aig_Obj_t * pObj )       { memset( pObj, 0, sizeof(Aig_Obj_t) );                                                             }
 static inline Aig_Obj_t *  Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj )  { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } 
@@ -653,7 +632,6 @@ extern unsigned *      Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves,
 /*=== aigTsim.c ========================================================*/
 extern Aig_Man_t *     Aig_ManConstReduce( Aig_Man_t * p, int fUseMvSweep, int nFramesSymb, int nFramesSatur, int fVerbose, int fVeryVerbose );
 /*=== aigUtil.c =========================================================*/
-extern unsigned        Aig_PrimeCudd( unsigned p );
 extern void            Aig_ManIncrementTravId( Aig_Man_t * p );
 extern char *          Aig_TimeStamp();
 extern int             Aig_ManHasNoGaps( Aig_Man_t * p );
diff --git a/src/aig/aig/aigCanon.c b/src/aig/aig/aigCanon.c
index 706a9c61..2c5e4d17 100644
--- a/src/aig/aig/aigCanon.c
+++ b/src/aig/aig/aigCanon.c
@@ -19,9 +19,9 @@
 ***********************************************************************/
 
 #include "aig.h"
-#include "kit.h"
-#include "bdc.h"
-#include "ioa.h"
+#include "src/bool/kit/kit.h"
+#include "src/bool/bdc/bdc.h"
+#include "src/aig/ioa/ioa.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -106,7 +106,7 @@ Aig_RMan_t * Aig_RManStart()
     p->pAig  = Aig_ManStart( 1000000 );
     Aig_IthVar( p->pAig, p->nVars-1 );
     // create hash table
-    p->nBins = Aig_PrimeCudd(5000);
+    p->nBins = Abc_PrimeCudd(5000);
     p->pBins = ABC_CALLOC( Aig_Tru_t *, p->nBins );
     p->pMemTrus = Aig_MmFlexStart();
     // bi-decomposition manager
@@ -182,7 +182,7 @@ clk = clock();
     pBinsOld = p->pBins;
     nBinsOld = p->nBins;
     // get the new Bins
-    p->nBins = Aig_PrimeCudd( 3 * nBinsOld ); 
+    p->nBins = Abc_PrimeCudd( 3 * nBinsOld ); 
     p->pBins = ABC_CALLOC( Aig_Tru_t *, p->nBins );
     // rehash the entries from the old table
     Counter = 0;
@@ -628,7 +628,7 @@ void Aig_RManRecord( unsigned * pTruth, int nVarsInit )
     else
         s_pRMan->nTtDsdNot++;
     // compute the number of words
-    nWords = Aig_TruthWordNum( nVars );
+    nWords = Abc_TruthWordNum( nVars );
     // copy the function
     memcpy( s_pRMan->pTruthInit, Kit_DsdObjTruth(pObj), 4*nWords );
     Kit_DsdNtkFree( pNtk );
diff --git a/src/aig/aig/aigCuts.c b/src/aig/aig/aigCuts.c
index 1bcf69ce..acff77d2 100644
--- a/src/aig/aig/aigCuts.c
+++ b/src/aig/aig/aigCuts.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "aig.h"
-#include "kit.h"
+#include "src/bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -58,7 +58,7 @@ Aig_ManCut_t * Aig_ManCutStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, in
     p->pAig     = pMan;
     p->pCuts    = ABC_CALLOC( Aig_Cut_t *, Aig_ManObjNumMax(pMan) );
     // allocate memory manager
-    p->nTruthWords = Aig_TruthWordNum(nLeafMax);
+    p->nTruthWords = Abc_TruthWordNum(nLeafMax);
     p->nCutSize = sizeof(Aig_Cut_t) + sizeof(int) * nLeafMax + fTruth * sizeof(unsigned) * p->nTruthWords;
     p->pMemCuts = Aig_MmFixedStart( p->nCutSize * p->nCutsMax, 512 );
     // room for temporary truth tables
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 0c2989d8..2da609f3 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "aig.h"
-#include "tim.h"
+#include "src/misc/tim/tim.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -477,7 +477,7 @@ int Aig_ManLevelNum( Aig_Man_t * p )
     int i, LevelsMax;
     LevelsMax = 0;
     Aig_ManForEachPo( p, pObj, i )
-        LevelsMax = ABC_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level );
+        LevelsMax = Abc_MaxInt( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level );
     return LevelsMax;
 }
 
diff --git a/src/aig/aig/aigDoms.c b/src/aig/aig/aigDoms.c
index 0ac2b358..b81279b2 100644
--- a/src/aig/aig/aigDoms.c
+++ b/src/aig/aig/aigDoms.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "aig.h"
-#include "saig.h"
+#include "src/aig/saig/saig.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index 94eaf497..c2127262 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
 
-#include "saig.h"
-#include "tim.h"
+#include "src/aig/saig/saig.h"
+#include "src/misc/tim/tim.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -52,8 +52,8 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
     assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
@@ -124,7 +124,7 @@ Aig_Man_t * Aig_ManDupSimpleWithHints( Aig_Man_t * p, Vec_Int_t * vHints )
     assert( p->nAsserts == 0 || p->nConstrs == 0 );
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -203,8 +203,8 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
     assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
@@ -303,8 +303,8 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
     int i, nNodes;
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
@@ -379,8 +379,8 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
     assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
@@ -456,8 +456,8 @@ Aig_Man_t * Aig_ManDupTrim( Aig_Man_t * p )
     int i, nNodes;
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
     // create the PIs
     Aig_ManCleanData( p );
@@ -505,8 +505,8 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->fCatchExor = 1;
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
@@ -608,8 +608,8 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
     int i, nNodes;
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
@@ -749,8 +749,8 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
     int i, nNodes;
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
@@ -821,8 +821,8 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
     int i, k;
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
@@ -895,8 +895,8 @@ Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
     int i;
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -980,8 +980,8 @@ Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p )
     int i;
     // start the HOP package
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -1054,8 +1054,8 @@ Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p )
     int i;
     // start the HOP package
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
@@ -1163,8 +1163,8 @@ Aig_Man_t * Aig_ManDupOrpos( Aig_Man_t * p, int fAddRegs )
     }
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -1212,8 +1212,8 @@ Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs )
     assert( iPoNum < Aig_ManPoNum(p)-Aig_ManRegNum(p) );
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -1263,8 +1263,8 @@ Aig_Man_t * Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs )
     }
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -1321,7 +1321,7 @@ Aig_Man_t * Aig_ManDupArray( Vec_Ptr_t * vArray )
     }
     // create the new manager
     pNew = Aig_ManStart( 10000 );
-    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Aig_ManForEachPi( p, pObj, i )
         Aig_ObjCreatePi(pNew);
     // create the PIs
diff --git a/src/aig/aig/aigFact.c b/src/aig/aig/aigFact.c
index 9c4e5689..40885365 100644
--- a/src/aig/aig/aigFact.c
+++ b/src/aig/aig/aigFact.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "aig.h"
-#include "kit.h"
+#include "src/bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -289,7 +289,7 @@ Vec_Ptr_t * Aig_SuppMinPerform( Aig_Man_t * p, Vec_Ptr_t * vOrGate, Vec_Ptr_t *
     Aig_Obj_t * pObj;
     Vec_Ptr_t * vTrSupp, * vTrNode, * vCofs;
     unsigned * uFunc, * uCare, * uFunc0, * uFunc1, * uCof;
-    int i, nWords = Aig_TruthWordNum( Vec_PtrSize(vSupp) );
+    int i, nWords = Abc_TruthWordNum( Vec_PtrSize(vSupp) );
     // assign support nodes
     vTrSupp = Vec_PtrAllocTruthTables( Vec_PtrSize(vSupp) );
     Vec_PtrForEachEntry( Aig_Obj_t *, vSupp, pObj, i )
diff --git a/src/aig/aig/aigFanout.c b/src/aig/aig/aigFanout.c
index d6317f43..d2fc1fe3 100644
--- a/src/aig/aig/aigFanout.c
+++ b/src/aig/aig/aigFanout.c
@@ -112,7 +112,7 @@ void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout )
     assert( pFanout->Id > 0 );
     if ( pObj->Id >= p->nFansAlloc || pFanout->Id >= p->nFansAlloc )
     {
-        int nFansAlloc = 2 * ABC_MAX( pObj->Id, pFanout->Id ); 
+        int nFansAlloc = 2 * Abc_MaxInt( pObj->Id, pFanout->Id ); 
         p->pFanData = ABC_REALLOC( int, p->pFanData, 5 * nFansAlloc );
         memset( p->pFanData + 5 * p->nFansAlloc, 0, sizeof(int) * 5 * (nFansAlloc - p->nFansAlloc) );
         p->nFansAlloc = nFansAlloc;
diff --git a/src/aig/aig/aigFrames.c b/src/aig/aig/aigFrames.c
index fdcd14aa..6840aadf 100644
--- a/src/aig/aig/aigFrames.c
+++ b/src/aig/aig/aigFrames.c
@@ -61,8 +61,8 @@ Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int
 
     // start the fraig package
     pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFs );
-    pFrames->pName = Aig_UtilStrsav( pAig->pName );
-    pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
+    pFrames->pName = Abc_UtilStrsav( pAig->pName );
+    pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
     // map constant nodes
     for ( f = 0; f < nFs; f++ )
         Aig_ObjSetFrames( pObjMap, nFs, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c
index aa019191..bb6cf987 100644
--- a/src/aig/aig/aigInter.c
+++ b/src/aig/aig/aigInter.c
@@ -19,8 +19,8 @@
 ***********************************************************************/
 
 #include "aig.h"
-#include "cnf.h"
-#include "satStore.h"
+#include "src/sat/cnf/cnf.h"
+#include "src/sat/bsat/satStore.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/aig/aig/aigJust.c b/src/aig/aig/aigJust.c
index eca17d40..bff2baed 100644
--- a/src/aig/aig/aigJust.c
+++ b/src/aig/aig/aigJust.c
@@ -114,7 +114,7 @@ int Aig_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Ve
 //        if ( Aig_ObjId(pNode) % 1000 == 0 )
 //            Value ^= 1;
         if ( vSuppLits )
-            Vec_IntPush( vSuppLits, Aig_Var2Lit( Aig_ObjPioNum(pNode), !Value ) );
+            Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjPioNum(pNode), !Value ) );
         return 1;
     }
     assert( Aig_ObjIsNode(pNode) );
@@ -221,8 +221,8 @@ int Aig_ObjTerSimulate( Aig_Man_t * pAig, Aig_Obj_t * pNode, Vec_Int_t * vSuppLi
     Aig_ManIncrementTravId( pAig );
     Vec_IntForEachEntry( vSuppLits, Entry, i )
     {
-        pObj = Aig_ManPi( pAig, Aig_Lit2Var(Entry) );
-        Aig_ObjSetTerValue( pObj, Aig_LitIsCompl(Entry) ? AIG_VAL0 : AIG_VAL1 );
+        pObj = Aig_ManPi( pAig, Abc_Lit2Var(Entry) );
+        Aig_ObjSetTerValue( pObj, Abc_LitIsCompl(Entry) ? AIG_VAL0 : AIG_VAL1 );
         Aig_ObjSetTravIdCurrent( pAig, pObj );
 //printf( "%d ", Entry );
     }
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index b0544c90..814e5248 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "aig.h"
-#include "tim.h"
+#include "src/misc/tim/tim.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -68,7 +68,7 @@ Aig_Man_t * Aig_ManStart( int nNodesMax )
     p->pConst1->fPhase = 1;
     p->nObjs[AIG_OBJ_CONST1]++;
     // start the table
-    p->nTableSize = Aig_PrimeCudd( nNodesMax );
+    p->nTableSize = Abc_PrimeCudd( nNodesMax );
     p->pTable = ABC_ALLOC( Aig_Obj_t *, p->nTableSize );
     memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
     return p;
@@ -92,8 +92,8 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
     int i;
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     // create the PIs
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
     Aig_ManForEachPi( p, pObj, i )
@@ -149,8 +149,8 @@ Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t *
     int i;
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
diff --git a/src/aig/aig/aigMffc.c b/src/aig/aig/aigMffc.c
index 2f51e442..ed0015ac 100644
--- a/src/aig/aig/aigMffc.c
+++ b/src/aig/aig/aigMffc.c
@@ -269,7 +269,7 @@ int Aig_NodeMffcExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves
     // dereference the current cut
     LevelMax = 0;
     Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
-        LevelMax = ABC_MAX( LevelMax, (int)pObj->Level );
+        LevelMax = Abc_MaxInt( LevelMax, (int)pObj->Level );
     if ( LevelMax == 0 )
         return 0;
     // dereference the cut
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 36578d35..71796993 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -122,11 +122,11 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
     // create the power counter
     if ( p->vProbs )
     {
-        float Prob0 = Aig_Int2Float( Vec_IntEntry( p->vProbs, Aig_ObjFaninId0(pObj) ) );
-        float Prob1 = Aig_Int2Float( Vec_IntEntry( p->vProbs, Aig_ObjFaninId1(pObj) ) );
+        float Prob0 = Abc_Int2Float( Vec_IntEntry( p->vProbs, Aig_ObjFaninId0(pObj) ) );
+        float Prob1 = Abc_Int2Float( Vec_IntEntry( p->vProbs, Aig_ObjFaninId1(pObj) ) );
         Prob0 = Aig_ObjFaninC0(pObj)? 1.0 - Prob0 : Prob0;
         Prob1 = Aig_ObjFaninC1(pObj)? 1.0 - Prob1 : Prob1;
-        Vec_IntSetEntry( p->vProbs, pObj->Id, Aig_Float2Int(Prob0 * Prob1) );
+        Vec_IntSetEntry( p->vProbs, pObj->Id, Abc_Float2Int(Prob0 * Prob1) );
     }
     return pObj;
 }
@@ -563,7 +563,7 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
     if ( p->pFanData && Aig_ObjIsBuf(pObjOld) )
     {
         Vec_PtrPush( p->vBufs, pObjOld );
-        p->nBufMax = ABC_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) );
+        p->nBufMax = Abc_MaxInt( p->nBufMax, Vec_PtrSize(p->vBufs) );
         Aig_ManPropagateBuffers( p, fUpdateLevel );
     }
 }
diff --git a/src/aig/aig/aigPack.c b/src/aig/aig/aigPack.c
index 0ecbf533..b89d6077 100644
--- a/src/aig/aig/aigPack.c
+++ b/src/aig/aig/aigPack.c
@@ -295,19 +295,19 @@ int Aig_ManPackAddPatternTry( Aig_ManPack_t * p, int iBit, Vec_Int_t * vLits )
     int i, Lit;
     Vec_IntForEachEntry( vLits, Lit, i )
     {
-        pInfo = Vec_WrdEntryP( p->vPiPats, Aig_Lit2Var(Lit) );
-        pPres = Vec_WrdEntryP( p->vPiCare, Aig_Lit2Var(Lit) );
-        if ( Aig_InfoHasBit( (unsigned *)pPres, iBit ) && 
-             Aig_InfoHasBit( (unsigned *)pInfo, iBit ) == Aig_LitIsCompl(Lit) )
+        pInfo = Vec_WrdEntryP( p->vPiPats, Abc_Lit2Var(Lit) );
+        pPres = Vec_WrdEntryP( p->vPiCare, Abc_Lit2Var(Lit) );
+        if ( Abc_InfoHasBit( (unsigned *)pPres, iBit ) && 
+             Abc_InfoHasBit( (unsigned *)pInfo, iBit ) == Abc_LitIsCompl(Lit) )
              return 0;
     }
     Vec_IntForEachEntry( vLits, Lit, i )
     {
-        pInfo = Vec_WrdEntryP( p->vPiPats, Aig_Lit2Var(Lit) );
-        pPres = Vec_WrdEntryP( p->vPiCare, Aig_Lit2Var(Lit) );
-        Aig_InfoSetBit( (unsigned *)pPres, iBit );
-        if ( Aig_InfoHasBit( (unsigned *)pInfo, iBit ) == Aig_LitIsCompl(Lit) )
-             Aig_InfoXorBit( (unsigned *)pInfo, iBit );
+        pInfo = Vec_WrdEntryP( p->vPiPats, Abc_Lit2Var(Lit) );
+        pPres = Vec_WrdEntryP( p->vPiCare, Abc_Lit2Var(Lit) );
+        Abc_InfoSetBit( (unsigned *)pPres, iBit );
+        if ( Abc_InfoHasBit( (unsigned *)pInfo, iBit ) == Abc_LitIsCompl(Lit) )
+             Abc_InfoXorBit( (unsigned *)pInfo, iBit );
     }
     return 1;
 }
@@ -335,16 +335,16 @@ void Aig_ManPackAddPattern( Aig_ManPack_t * p, Vec_Int_t * vLits )
         word * pInfo, * pPres;
         int i, Lit;
         Vec_IntForEachEntry( vLits, Lit, i )
-            printf( "%d", Aig_LitIsCompl(Lit) );
+            printf( "%d", Abc_LitIsCompl(Lit) );
         printf( "\n\n" );
         for ( k = 1; k < 64; k++ )
         {
             Vec_IntForEachEntry( vLits, Lit, i )
             {
-                pInfo = Vec_WrdEntryP( p->vPiPats, Aig_Lit2Var(Lit) );
-                pPres = Vec_WrdEntryP( p->vPiCare, Aig_Lit2Var(Lit) );
-                if ( Aig_InfoHasBit( (unsigned *)pPres, k ) )
-                    printf( "%d", Aig_InfoHasBit( (unsigned *)pInfo, k ) );
+                pInfo = Vec_WrdEntryP( p->vPiPats, Abc_Lit2Var(Lit) );
+                pPres = Vec_WrdEntryP( p->vPiCare, Abc_Lit2Var(Lit) );
+                if ( Abc_InfoHasBit( (unsigned *)pPres, k ) )
+                    printf( "%d", Abc_InfoHasBit( (unsigned *)pInfo, k ) );
                 else
                     printf( "-" );
             }
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 6ee3930b..1510ddc7 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -19,8 +19,8 @@
 ***********************************************************************/
 
 #include "aig.h"
-#include "tim.h"
-#include "fra.h"
+#include "src/misc/tim/tim.h"
+#include "src/proof/fra/fra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -471,13 +471,13 @@ unsigned * Aig_ManSuppCharStart( Vec_Int_t * vOne, int nPis )
 {
     unsigned * pBuffer;
     int i, Entry;
-    int nWords = Aig_BitWordNum(nPis);
+    int nWords = Abc_BitWordNum(nPis);
     pBuffer = ABC_ALLOC( unsigned, nWords );
     memset( pBuffer, 0, sizeof(unsigned) * nWords );
     Vec_IntForEachEntry( vOne, Entry, i )
     {
         assert( Entry < nPis );
-        Aig_InfoSetBit( pBuffer, Entry );
+        Abc_InfoSetBit( pBuffer, Entry );
     }
     return pBuffer;
 }
@@ -499,7 +499,7 @@ void Aig_ManSuppCharAdd( unsigned * pBuffer, Vec_Int_t * vOne, int nPis )
     Vec_IntForEachEntry( vOne, Entry, i )
     {
         assert( Entry < nPis );
-        Aig_InfoSetBit( pBuffer, Entry );
+        Abc_InfoSetBit( pBuffer, Entry );
     }
 }
 
@@ -518,7 +518,7 @@ int Aig_ManSuppCharCommon( unsigned * pBuffer, Vec_Int_t * vOne )
 {
     int i, Entry, nCommon = 0;
     Vec_IntForEachEntry( vOne, Entry, i )
-        nCommon += Aig_InfoHasBit(pBuffer, Entry);
+        nCommon += Abc_InfoHasBit(pBuffer, Entry);
     return nCommon;
 }
 
@@ -558,7 +558,7 @@ int Aig_ManPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vParts
         if ( Vec_IntSize(vPartSupp) < 100 )
             Repulse = 1;
         else
-            Repulse = 1+Aig_Base2Log(Vec_IntSize(vPartSupp)-100);
+            Repulse = 1+Abc_Base2Log(Vec_IntSize(vPartSupp)-100);
         Value = Attract/Repulse;
         if ( ValueBest < Value )
         {
diff --git a/src/aig/aig/aigPartSat.c b/src/aig/aig/aigPartSat.c
index 48e5cf80..52fbe2e2 100644
--- a/src/aig/aig/aigPartSat.c
+++ b/src/aig/aig/aigPartSat.c
@@ -19,8 +19,8 @@
 ***********************************************************************/
 
 #include "aig.h"
-#include "satSolver.h"
-#include "cnf.h"
+#include "src/sat/bsat/satSolver.h"
+#include "src/sat/cnf/cnf.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/aig/aig/aigRepar.c b/src/aig/aig/aigRepar.c
index 03155e91..e0fe4cb1 100644
--- a/src/aig/aig/aigRepar.c
+++ b/src/aig/aig/aigRepar.c
@@ -19,8 +19,8 @@
 ***********************************************************************/
 
 #include "aig.h"
-#include "cnf.h"
-#include "satSolver2.h"
+#include "src/sat/cnf/cnf.h"
+#include "src/sat/bsat/satSolver2.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -313,7 +313,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
 
     // start the interpolant
     pBase = Aig_ManStart( 1000 );
-    pBase->pName = Aig_UtilStrsav( "repar" );
+    pBase->pName = Abc_UtilStrsav( "repar" );
     for ( k = 0; k < 2*nOuts; k++ )
         Aig_IthVar(pBase, i);
 
@@ -338,7 +338,7 @@ Aig_Man_t * Aig_ManInterRepar( Aig_Man_t * pMan, int fVerbose )
         Sat_Solver2PrintStats( stdout, pSat );
 
         // derive interpolant
-        pInter = Sat_ProofInterpolant( pSat, vVars );
+        pInter = (Aig_Man_t *)Sat_ProofInterpolant( pSat, vVars );
         Aig_ManPrintStats( pInter );
         // make sure interpolant does not depend on useless vars
         Aig_ManForEachPi( pInter, pObj, i )
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 9966174f..d08b6553 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -271,8 +271,8 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered )
     int i;
     // start the HOP package
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c
index f7774d22..acc5b6ec 100644
--- a/src/aig/aig/aigRet.c
+++ b/src/aig/aig/aigRet.c
@@ -176,7 +176,7 @@ void Rtm_ObjTransferToBig( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
     assert( pEdge->nLats == 10 );
     if ( p->nExtraCur + 1 > p->nExtraAlloc )
     {
-        int nExtraAllocNew = ABC_MAX( 2 * p->nExtraAlloc, 1024 );
+        int nExtraAllocNew = Abc_MaxInt( 2 * p->nExtraAlloc, 1024 );
         p->pExtra = ABC_REALLOC( unsigned, p->pExtra, nExtraAllocNew );
         p->nExtraAlloc = nExtraAllocNew;
     }
@@ -202,7 +202,7 @@ void Rtm_ObjTransferToBigger( Rtm_Man_t * p, Rtm_Edg_t * pEdge )
     nWords = (pEdge->nLats + 1) >> 4;
     if ( p->nExtraCur + nWords + 1 > p->nExtraAlloc )
     {
-        int nExtraAllocNew = ABC_MAX( 2 * p->nExtraAlloc, 1024 );
+        int nExtraAllocNew = Abc_MaxInt( 2 * p->nExtraAlloc, 1024 );
         p->pExtra = ABC_REALLOC( unsigned, p->pExtra, nExtraAllocNew );
         p->nExtraAlloc = nExtraAllocNew;
     }
@@ -360,7 +360,7 @@ int Rtm_ManLatchMax( Rtm_Man_t * p )
             assert( Val == 1 || Val == 2 );
         }
 */
-        nLatchMax = ABC_MAX( nLatchMax, (int)pEdge->nLats );
+        nLatchMax = Abc_MaxInt( nLatchMax, (int)pEdge->nLats );
     }
     return nLatchMax;
 }
@@ -477,7 +477,7 @@ int Rtm_ObjGetDegreeFwd( Rtm_Obj_t * pObj )
     Rtm_Obj_t * pFanin;
     int i, Degree = 0;
     Rtm_ObjForEachFanin( pObj, pFanin, i )
-        Degree = ABC_MAX( Degree, (int)pFanin->Num );
+        Degree = Abc_MaxInt( Degree, (int)pFanin->Num );
     return Degree + 1;
 }
 
@@ -497,7 +497,7 @@ int Rtm_ObjGetDegreeBwd( Rtm_Obj_t * pObj )
     Rtm_Obj_t * pFanout;
     int i, Degree = 0;
     Rtm_ObjForEachFanout( pObj, pFanout, i )
-        Degree = ABC_MAX( Degree, (int)pFanout->Num );
+        Degree = Abc_MaxInt( Degree, (int)pFanout->Num );
     return Degree + 1;
 }
 
@@ -910,7 +910,7 @@ clk = clock();
                 if ( !Rtm_ObjCheckRetimeFwd( pNext ) ) // skip non-retimable
                     continue;
                 Degree = Rtm_ObjGetDegreeFwd( pNext );
-                DegreeMax = ABC_MAX( DegreeMax, Degree );
+                DegreeMax = Abc_MaxInt( DegreeMax, Degree );
                 if ( Degree > nStepsMax ) // skip nodes with high degree
                     continue;
                 pNext->fMark = 1;
@@ -931,7 +931,7 @@ clk = clock();
                 if ( !Rtm_ObjCheckRetimeBwd( pNext ) ) // skip non-retimable
                     continue;
                 Degree = Rtm_ObjGetDegreeBwd( pNext );
-                DegreeMax = ABC_MAX( DegreeMax, Degree );
+                DegreeMax = Abc_MaxInt( DegreeMax, Degree );
                 if ( Degree > nStepsMax ) // skip nodes with high degree
                     continue;
                 pNext->fMark = 1;
@@ -952,8 +952,8 @@ clk = clock();
 
     // get the new manager
     pNew = Rtm_ManToAig( pRtm );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Rtm_ManFree( pRtm );
     // group the registers
 clk = clock();
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 2bc7f8ea..74b56bcf 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -50,8 +50,8 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
     int i, nTruePis;
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
     pNew->nConstrs = p->nConstrs;
     assert( p->vFlopNums == NULL || Vec_IntSize(p->vFlopNums) == p->nRegs );
diff --git a/src/aig/aig/aigSplit.c b/src/aig/aig/aigSplit.c
index 51b4f982..82f60e2d 100644
--- a/src/aig/aig/aigSplit.c
+++ b/src/aig/aig/aigSplit.c
@@ -19,9 +19,8 @@
 ***********************************************************************/
 
 #include "aig.h"
-#include "saig.h"
-#include "cuddInt.h"
-#include "extra.h"
+#include "src/aig/saig/saig.h"
+#include "src/misc/extra/extraBdd.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -84,7 +83,7 @@ Aig_Man_t * Aig_ManConvertBddsToAigs( Aig_Man_t * p, DdManager * dd, Vec_Ptr_t *
     Aig_ManCleanData( p );
     // generate AIG for BDD
     pNew = Aig_ManStart( Aig_ManObjNum(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
     Aig_ManForEachPi( p, pObj, i )
         pObj->pData = Aig_ObjCreatePi( pNew );
diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c
index 13826065..ec2531c7 100644
--- a/src/aig/aig/aigTable.c
+++ b/src/aig/aig/aigTable.c
@@ -77,7 +77,7 @@ clk = clock();
     pTableOld = p->pTable;
     nTableSizeOld = p->nTableSize;
     // get the new table
-    p->nTableSize = Aig_PrimeCudd( 2 * Aig_ManNodeNum(p) ); 
+    p->nTableSize = Abc_PrimeCudd( 2 * Aig_ManNodeNum(p) ); 
     p->pTable = ABC_ALLOC( Aig_Obj_t *, p->nTableSize );
     memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
     // rehash the entries from the old table
diff --git a/src/aig/aig/aigTiming.c b/src/aig/aig/aigTiming.c
index 4ea93e29..e855e012 100644
--- a/src/aig/aig/aigTiming.c
+++ b/src/aig/aig/aigTiming.c
@@ -121,7 +121,7 @@ int Aig_ObjReverseLevelNew( Aig_Man_t * p, Aig_Obj_t * pObj )
     Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i )
     {
         LevelCur = Aig_ObjReverseLevel( p, pFanout );
-        Level = ABC_MAX( Level, LevelCur );
+        Level = Abc_MaxInt( Level, LevelCur );
     }
     return Level + 1;
 }
diff --git a/src/aig/aig/aigTruth.c b/src/aig/aig/aigTruth.c
index ddcb8736..5115c4f4 100644
--- a/src/aig/aig/aigTruth.c
+++ b/src/aig/aig/aigTruth.c
@@ -88,7 +88,7 @@ unsigned * Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t *
     Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
         pObj->pData = Vec_PtrEntry( vTruthElem, i );
     // compute truths for other nodes
-    nWords = Aig_TruthWordNum( Vec_PtrSize(vLeaves) );
+    nWords = Abc_TruthWordNum( Vec_PtrSize(vLeaves) );
     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         pObj->pData = Aig_ManCutTruthOne( pObj, (unsigned *)Vec_PtrEntry(vTruthStore, i), nWords );
     return (unsigned *)pRoot->pData;
diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c
index 5e711ff6..99aa5c64 100644
--- a/src/aig/aig/aigTsim.c
+++ b/src/aig/aig/aigTsim.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "aig.h"
-#include "saig.h"
+#include "src/aig/saig/saig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -133,10 +133,10 @@ Aig_Tsi_t * Aig_TsiStart( Aig_Man_t * pAig )
     p = ABC_ALLOC( Aig_Tsi_t, 1 );
     memset( p, 0, sizeof(Aig_Tsi_t) );
     p->pAig    = pAig;
-    p->nWords  = Aig_BitWordNum( 2*Aig_ManRegNum(pAig) );
+    p->nWords  = Abc_BitWordNum( 2*Aig_ManRegNum(pAig) );
     p->vStates = Vec_PtrAlloc( 1000 );
     p->pMem    = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 );
-    p->nBins   = Aig_PrimeCudd(TSI_MAX_ROUNDS/2);
+    p->nBins   = Abc_PrimeCudd(TSI_MAX_ROUNDS/2);
     p->pBins   = ABC_ALLOC( unsigned *, p->nBins );
     memset( p->pBins, 0, sizeof(unsigned *) * p->nBins );
     return p;
@@ -274,7 +274,7 @@ void Aig_TsiStatePrint( Aig_Tsi_t * p, unsigned * pState )
     int i, Value, nZeros = 0, nOnes = 0, nDcs = 0;
     for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
     {
-        Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+        Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
         if ( Value == 1 )
             printf( "0" ), nZeros++;
         else if ( Value == 2 )
@@ -304,7 +304,7 @@ int Aig_TsiStateCount( Aig_Tsi_t * p, unsigned * pState )
     int i, Value, nCounter = 0;
     Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
     {
-        Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+        Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
         nCounter += (Value == 1 || Value == 2);
     }
     return nCounter;
@@ -369,9 +369,9 @@ Vec_Ptr_t * Aig_ManTernarySimulate( Aig_Man_t * p, int fVerbose, int fVeryVerbos
         {
             Value = Aig_ObjGetXsim(pObjLo);
             if ( Value & 1 )
-                Aig_InfoSetBit( pState, 2 * i );
+                Abc_InfoSetBit( pState, 2 * i );
             if ( Value & 2 )
-                Aig_InfoSetBit( pState, 2 * i + 1 );
+                Abc_InfoSetBit( pState, 2 * i + 1 );
         }
 
 //        printf( "%d ", Aig_TsiStateCount(pTsi, pState) );
@@ -446,7 +446,7 @@ Aig_TsiStatePrint( pTsi, pState );
         for ( i = 0; i < pTsi->nWords - 1; i++ )
             if ( pState[i] != ~0 )
                 fConstants = 1;
-        if ( pState[i] != Aig_InfoMask( 2*Aig_ManRegNum(p) - 32*(pTsi->nWords-1) ) )
+        if ( pState[i] != Abc_InfoMask( 2*Aig_ManRegNum(p) - 32*(pTsi->nWords-1) ) )
             fConstants = 1;
     }
     if ( fConstants == 0 )
@@ -465,7 +465,7 @@ Aig_TsiStatePrint( pTsi, pState );
     nCounter = 0;
     Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
     {
-        Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+        Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i );
         nCounter += (Value == 1 || Value == 2);
         if ( Value == 1 )
             Vec_PtrPush( vMap, Aig_ManConst0(p) );
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 8cbaa63b..5546c776 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -30,42 +30,6 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/**Function********************************************************************
-
-  Synopsis    [Returns the next prime >= p.]
-
-  Description [Copied from CUDD, for stand-aloneness.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-unsigned int Aig_PrimeCudd( unsigned int p )
-{
-    int i,pn;
-
-    p--;
-    do {
-        p++;
-        if (p&1) {
-        pn = 1;
-        i = 3;
-        while ((unsigned) (i * i) <= p) {
-        if (p % i == 0) {
-            pn = 0;
-            break;
-        }
-        i += 2;
-        }
-    } else {
-        pn = 0;
-    }
-    } while (!pn);
-    return(p);
-
-} /* end of Cudd_Prime */
-
 /**Function*************************************************************
 
   Synopsis    [Increments the current traversal ID of the network.]
@@ -140,7 +104,7 @@ int Aig_ManLevels( Aig_Man_t * p )
     Aig_Obj_t * pObj;
     int i, LevelMax = 0;
     Aig_ManForEachPo( p, pObj, i )
-        LevelMax = ABC_MAX( LevelMax, (int)Aig_ObjFanin0(pObj)->Level );
+        LevelMax = Abc_MaxInt( LevelMax, (int)Aig_ObjFanin0(pObj)->Level );
     return LevelMax;
 }
 
@@ -791,7 +755,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec
         pObj->iData = Counter++;
     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         pObj->iData = Counter++;
-    nDigits = Aig_Base10Log( Counter );
+    nDigits = Abc_Base10Log( Counter );
     // write the file 
     pFile = fopen( pFileName, "w" );
     fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif()\n" );
@@ -906,7 +870,7 @@ void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName )
         pObj->iData = Counter++;
     Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         pObj->iData = Counter++;
-    nDigits = Aig_Base10Log( Counter );
+    nDigits = Abc_Base10Log( Counter );
     // write the file
     pFile = fopen( pFileName, "w" );
     fprintf( pFile, "// Verilog file written by procedure Aig_ManDumpVerilog()\n" );
@@ -1299,7 +1263,7 @@ void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * v
     Aig_Obj_t ** pBeg2 = (Aig_Obj_t **)vArr2->pArray;
     Aig_Obj_t ** pEnd1 = (Aig_Obj_t **)vArr1->pArray + vArr1->nSize;
     Aig_Obj_t ** pEnd2 = (Aig_Obj_t **)vArr2->pArray + vArr2->nSize;
-    Vec_PtrGrow( vArr, ABC_MAX( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
+    Vec_PtrGrow( vArr, Abc_MaxInt( Vec_PtrSize(vArr1), Vec_PtrSize(vArr2) ) );
     pBeg  = (Aig_Obj_t **)vArr->pArray;
     while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
     {
@@ -1324,8 +1288,8 @@ void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * v
 
 ABC_NAMESPACE_IMPL_END
 
-#include "fra.h"
-#include "saig.h"
+#include "src/proof/fra/fra.h"
+#include "src/aig/saig/saig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -1353,45 +1317,45 @@ void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Abc_Cex_t * pCex )
     assert( Aig_ManRegNum(pAig) > 0 ); // makes sense only for sequential AIGs
     assert( pAig->pData2 == NULL );    // if this fail, there may be a memory leak
     // allocate memory to store simulation bits for internal nodes
-    pAig->pData2 = ABC_CALLOC( unsigned, Aig_BitWordNum( (pCex->iFrame + 1) * Aig_ManObjNum(pAig) ) );
+    pAig->pData2 = ABC_CALLOC( unsigned, Abc_BitWordNum( (pCex->iFrame + 1) * Aig_ManObjNum(pAig) ) );
     // the register values in the counter-example should be zero
     Saig_ManForEachLo( pAig, pObj, k )
-        assert( Aig_InfoHasBit(pCex->pData, iBit++) == 0 );
+        assert( Abc_InfoHasBit(pCex->pData, iBit++) == 0 );
     // iterate through the timeframes
     nObjs = Aig_ManObjNum(pAig);
     for ( i = 0; i <= pCex->iFrame; i++ )
     {
         // set constant 1 node
-        Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + 0 );
+        Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + 0 );
         // set primary inputs according to the counter-example
         Saig_ManForEachPi( pAig, pObj, k )
-            if ( Aig_InfoHasBit(pCex->pData, iBit++) )
-                Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
+            if ( Abc_InfoHasBit(pCex->pData, iBit++) )
+                Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
         // compute values for each node
         Aig_ManForEachNode( pAig, pObj, k )
         {
-            Val0 = Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
-            Val1 = Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId1(pObj) );
+            Val0 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
+            Val1 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId1(pObj) );
             if ( (Val0 ^ Aig_ObjFaninC0(pObj)) & (Val1 ^ Aig_ObjFaninC1(pObj)) )
-                Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
+                Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
         }
         // derive values for combinational outputs
         Aig_ManForEachPo( pAig, pObj, k )
         {
-            Val0 = Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
+            Val0 = Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
             if ( Val0 ^ Aig_ObjFaninC0(pObj) )
-                Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
+                Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
         }
         if ( i == pCex->iFrame )
             continue;
         // transfer values to the register output of the next frame
         Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
-            if ( Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObjRi) ) )
-                Aig_InfoSetBit( (unsigned *)pAig->pData2, nObjs * (i+1) + Aig_ObjId(pObjRo) );
+            if ( Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * i + Aig_ObjId(pObjRi) ) )
+                Abc_InfoSetBit( (unsigned *)pAig->pData2, nObjs * (i+1) + Aig_ObjId(pObjRo) );
     }
     assert( iBit == pCex->nBits );
     // check that the counter-example is correct, that is, the corresponding output is asserted
-    assert( Aig_InfoHasBit( (unsigned *)pAig->pData2, nObjs * pCex->iFrame + Aig_ObjId(Aig_ManPo(pAig, pCex->iPo)) ) );
+    assert( Abc_InfoHasBit( (unsigned *)pAig->pData2, nObjs * pCex->iFrame + Aig_ObjId(Aig_ManPo(pAig, pCex->iPo)) ) );
 }
 
 /**Function*************************************************************
@@ -1428,7 +1392,7 @@ void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig )
 int Aig_ManCounterExampleValueLookup(  Aig_Man_t * pAig, int Id, int iFrame )
 {
     assert( Id >= 0 && Id < Aig_ManObjNum(pAig) );
-    return Aig_InfoHasBit( (unsigned *)pAig->pData2, Aig_ManObjNum(pAig) * iFrame + Id );
+    return Abc_InfoHasBit( (unsigned *)pAig->pData2, Aig_ManObjNum(pAig) * iFrame + Id );
 }
 
 /**Function*************************************************************
@@ -1445,7 +1409,7 @@ int Aig_ManCounterExampleValueLookup(  Aig_Man_t * pAig, int Id, int iFrame )
 void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Abc_Cex_t * pCex )
 {
     Aig_Obj_t * pObj = Aig_ManObj( pAig, Aig_ManObjNum(pAig)/2 );
-    int iFrame = ABC_MAX( 0, pCex->iFrame - 1 );
+    int iFrame = Abc_MaxInt( 0, pCex->iFrame - 1 );
     printf( "\nUsing counter-example, which asserts output %d in frame %d.\n", pCex->iPo, pCex->iFrame );
     Aig_ManCounterExampleValueStart( pAig, pCex );
     printf( "Value of object %d in frame %d is %d.\n", Aig_ObjId(pObj), iFrame,