Major restructuring of the code.

42 files changed, 453 insertions, 508 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 14fd4d6e..a784ab92 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __GIA_H__
-#define __GIA_H__
+#ifndef ABC__aig__gia__gia_h
+#define ABC__aig__gia__gia_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"
 #include "giaAbs.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -210,19 +210,6 @@ struct Gia_ParVta_t_
     int            iFrame;        // the number of frames covered 
 };
 
-static inline int          Gia_IntAbs( int n )                    { return (n < 0)? -n : n;                                     }
-static inline int          Gia_Float2Int( float Val )             { union { int x; float y; } v; v.y = Val; return v.x;         }
-static inline float        Gia_Int2Float( int Num )               { union { int x; float y; } v; v.x = Num; return v.y;         }
-static inline int          Gia_Base2Log( unsigned n )             { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
-static inline int          Gia_Base10Log( unsigned n )            { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; }
-static inline int          Gia_Base16Log( unsigned n )            { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 16, r++ ); return r; }
-static inline char *       Gia_UtilStrsav( char * s )             { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL;  }
-static inline int          Gia_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);                       }
-static inline int          Gia_TruthWordNum( int nVars )          { return nVars <= 5 ? 1 : (1 << (nVars - 5));                 }
-static inline int          Gia_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0;                   }
-static inline void         Gia_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));                               }
-static inline void         Gia_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));                               }
-static inline unsigned     Gia_InfoMask( int nVar )               { return (~(unsigned)0) >> (32-nVar);                         }
 static inline unsigned     Gia_ObjCutSign( unsigned ObjId )       { return (1 << (ObjId & 31));                                 }
 static inline int          Gia_WordHasOneBit( unsigned uWord )    { return (uWord & (uWord-1)) == 0;                            }
 static inline int          Gia_WordHasOnePair( unsigned uWord )   { return Gia_WordHasOneBit(uWord & (uWord>>1) & 0x55555555);  }
@@ -246,7 +233,7 @@ static inline int Gia_WordFindFirstBit( unsigned uWord )
 static inline int Gia_ManTruthIsConst0( unsigned * pIn, int nVars )
 {
     int w;
-    for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- )
+    for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
         if ( pIn[w] )
             return 0;
     return 1;
@@ -254,7 +241,7 @@ static inline int Gia_ManTruthIsConst0( unsigned * pIn, int nVars )
 static inline int Gia_ManTruthIsConst1( unsigned * pIn, int nVars )
 {
     int w;
-    for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- )
+    for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
         if ( pIn[w] != ~(unsigned)0 )
             return 0;
     return 1;
@@ -262,35 +249,28 @@ static inline int Gia_ManTruthIsConst1( unsigned * pIn, int nVars )
 static inline void Gia_ManTruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
 {
     int w;
-    for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- )
+    for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
         pOut[w] = pIn[w];
 }
 static inline void Gia_ManTruthClear( unsigned * pOut, int nVars )
 {
     int w;
-    for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- )
+    for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
         pOut[w] = 0;
 }
 static inline void Gia_ManTruthFill( unsigned * pOut, int nVars )
 {
     int w;
-    for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- )
+    for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
         pOut[w] = ~(unsigned)0;
 }
 static inline void Gia_ManTruthNot( unsigned * pOut, unsigned * pIn, int nVars )
 {
     int w;
-    for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- )
+    for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- )
         pOut[w] = ~pIn[w];
 }
 
-static inline int          Gia_Var2Lit( int Var, int fCompl )  { return Var + Var + fCompl; }
-static inline int          Gia_Lit2Var( int Lit )              { return Lit >> 1;           }
-static inline int          Gia_LitIsCompl( int Lit )           { return Lit & 1;            }
-static inline int          Gia_LitNot( int Lit )               { return Lit ^ 1;            }
-static inline int          Gia_LitNotCond( int Lit, int c )    { return Lit ^ (int)(c > 0); }
-static inline int          Gia_LitRegular( int Lit )           { return Lit & ~01;          }
-
 static inline Gia_Obj_t *  Gia_Regular( Gia_Obj_t * p )        { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
 static inline Gia_Obj_t *  Gia_Not( Gia_Obj_t * p )            { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^  01); }
 static inline Gia_Obj_t *  Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
@@ -358,33 +338,33 @@ static inline int          Gia_ObjFaninId0( Gia_Obj_t * pObj, int ObjId )      {
 static inline int          Gia_ObjFaninId1( Gia_Obj_t * pObj, int ObjId )      { return ObjId - pObj->iDiff1;    }
 static inline int          Gia_ObjFaninId0p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId0( pObj, Gia_ObjId(p, pObj) );              }
 static inline int          Gia_ObjFaninId1p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId1( pObj, Gia_ObjId(p, pObj) );              }
-static inline int          Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId )     { return Gia_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); }
-static inline int          Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId )     { return Gia_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); }
-static inline int          Gia_ObjFaninLit0p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Gia_Var2Lit( Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) );    }
-static inline int          Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Gia_Var2Lit( Gia_ObjFaninId1p(p, pObj), Gia_ObjFaninC1(pObj) );    }
+static inline int          Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId )     { return Abc_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); }
+static inline int          Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId )     { return Abc_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); }
+static inline int          Gia_ObjFaninLit0p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Abc_Var2Lit( Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) );    }
+static inline int          Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Abc_Var2Lit( Gia_ObjFaninId1p(p, pObj), Gia_ObjFaninC1(pObj) );    }
 static inline void         Gia_ObjFlipFaninC0( Gia_Obj_t * pObj )              { assert( Gia_ObjIsCo(pObj) ); pObj->fCompl0 ^= 1;          }
 static inline int          Gia_ObjWhatFanin( Gia_Obj_t * pObj, Gia_Obj_t * pFanin )  { return Gia_ObjFanin0(pObj) == pFanin ? 0 : (Gia_ObjFanin1(pObj) == pFanin ? 1 : -1); }
 
-static inline Gia_Obj_t *  Gia_ObjCopy( Gia_Man_t * p, Gia_Obj_t * pObj )      { return Gia_ManObj( p, Gia_Lit2Var(pObj->Value) );                              }
+static inline Gia_Obj_t *  Gia_ObjCopy( Gia_Man_t * p, Gia_Obj_t * pObj )      { return Gia_ManObj( p, Abc_Lit2Var(pObj->Value) );                              }
 
-static inline int          Gia_ObjFanin0Copy( Gia_Obj_t * pObj )               { return Gia_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );     }
-static inline int          Gia_ObjFanin1Copy( Gia_Obj_t * pObj )               { return Gia_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) );     }
+static inline int          Gia_ObjFanin0Copy( Gia_Obj_t * pObj )               { return Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );     }
+static inline int          Gia_ObjFanin1Copy( Gia_Obj_t * pObj )               { return Abc_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) );     }
 
 static inline int          Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )               { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)];  }
 static inline void         Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit )  { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit;  }
 
-static inline int          Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj));  }
-static inline int          Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj));  }
+static inline int          Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj));  }
+static inline int          Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj )         { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj));  }
 
-static inline Gia_Obj_t *  Gia_ObjFromLit( Gia_Man_t * p, int iLit )           { return Gia_NotCond( Gia_ManObj(p, Gia_Lit2Var(iLit)), Gia_LitIsCompl(iLit) );  }
-static inline int          Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Gia_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); }
+static inline Gia_Obj_t *  Gia_ObjFromLit( Gia_Man_t * p, int iLit )           { return Gia_NotCond( Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) );  }
+static inline int          Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); }
 static inline int          Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit )      { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) );        }
 
 static inline int          Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj )     { return Vec_IntGetEntry(p->vLevels, Gia_ObjId(p,pObj));     }
 static inline int          Gia_ObjLevelId( Gia_Man_t * p, int Id )             { return Vec_IntGetEntry(p->vLevels, Id);                    }
 static inline void         Gia_ObjSetLevel( Gia_Man_t * p, Gia_Obj_t * pObj, int l )  { Vec_IntSetEntry(p->vLevels, Gia_ObjId(p,pObj), l);  }
 static inline void         Gia_ObjSetCoLevel( Gia_Man_t * p, Gia_Obj_t * pObj )  { assert( Gia_ObjIsCo(pObj)  ); Gia_ObjSetLevel( p, pObj, Gia_ObjLevel(p,Gia_ObjFanin0(pObj)) );                                                }
-static inline void         Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, 1+ABC_MAX(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); }
+static inline void         Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, 1+Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); }
 
 static inline int          Gia_ObjRefs( Gia_Man_t * p, Gia_Obj_t * pObj )      { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)];    }
 static inline int          Gia_ObjRefsId( Gia_Man_t * p, int Id )              { assert( p->pRefs); return p->pRefs[Id];                    }
@@ -457,17 +437,17 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )
     assert( iLit0 != iLit1 );
     if ( iLit0 < iLit1 )
     {
-        pObj->iDiff0  = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit0);
-        pObj->fCompl0 = Gia_LitIsCompl(iLit0);
-        pObj->iDiff1  = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit1);
-        pObj->fCompl1 = Gia_LitIsCompl(iLit1);
+        pObj->iDiff0  = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0);
+        pObj->fCompl0 = Abc_LitIsCompl(iLit0);
+        pObj->iDiff1  = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit1);
+        pObj->fCompl1 = Abc_LitIsCompl(iLit1);
     }
     else
     {
-        pObj->iDiff1  = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit0);
-        pObj->fCompl1 = Gia_LitIsCompl(iLit0);
-        pObj->iDiff0  = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit1);
-        pObj->fCompl0 = Gia_LitIsCompl(iLit1);
+        pObj->iDiff1  = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0);
+        pObj->fCompl1 = Abc_LitIsCompl(iLit0);
+        pObj->iDiff0  = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit1);
+        pObj->fCompl0 = Abc_LitIsCompl(iLit1);
     }
     if ( p->pFanData )
     {
@@ -480,8 +460,8 @@ static inline int Gia_ManAppendCo( Gia_Man_t * p, int iLit0 )
 { 
     Gia_Obj_t * pObj = Gia_ManAppendObj( p );
     pObj->fTerm = 1;
-    pObj->iDiff0  = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit0);
-    pObj->fCompl0 = Gia_LitIsCompl(iLit0);
+    pObj->iDiff0  = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0);
+    pObj->fCompl0 = Abc_LitIsCompl(iLit0);
     pObj->iDiff1  = Vec_IntSize( p->vCos );
     Vec_IntPush( p->vCos, Gia_ObjId(p, pObj) );
     if ( p->pFanData )
@@ -490,9 +470,9 @@ static inline int Gia_ManAppendCo( Gia_Man_t * p, int iLit0 )
 }
 static inline int Gia_ManAppendMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )  
 { 
-    int iTemp0 = Gia_ManAppendAnd( p, Gia_LitNot(iCtrl), iData0 );
+    int iTemp0 = Gia_ManAppendAnd( p, Abc_LitNot(iCtrl), iData0 );
     int iTemp1 = Gia_ManAppendAnd( p, iCtrl, iData1 );
-    return Gia_LitNotCond( Gia_ManAppendAnd( p, Gia_LitNot(iTemp0), Gia_LitNot(iTemp1) ), 1 );
+    return Abc_LitNotCond( Gia_ManAppendAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), 1 );
 }
 
 #define GIA_ZER 1
@@ -587,7 +567,7 @@ static inline int         Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i )   { re
 #define Gia_ManForEachObjVec( vVec, p, pObj, i )                        \
     for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Vec_IntEntry(vVec,i))); i++ )
 #define Gia_ManForEachObjVecLit( vVec, p, pObj, fCompl, i )             \
-    for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Gia_Lit2Var(Vec_IntEntry(vVec,i)))) && (((fCompl) = Gia_LitIsCompl(Vec_IntEntry(vVec,i))),1); i++ )
+    for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Abc_Lit2Var(Vec_IntEntry(vVec,i)))) && (((fCompl) = Abc_LitIsCompl(Vec_IntEntry(vVec,i))),1); i++ )
 #define Gia_ManForEachObjReverse( p, pObj, i )                          \
     for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- )
 #define Gia_ManForEachAnd( p, pObj, i )                                 \
@@ -817,7 +797,6 @@ extern Gia_Man_t *         Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose );
 /*=== giaUtil.c ===========================================================*/
 extern unsigned            Gia_ManRandom( int fReset );
 extern void                Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop );
-extern unsigned int        Gia_PrimeCudd( unsigned int p );
 extern char *              Gia_TimeStamp();
 extern char *              Gia_FileNameGenericAppend( char * pBase, char * pSuffix );
 extern void                Gia_ManIncrementTravId( Gia_Man_t * p );
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index e9861977..e25ff7fb 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -20,7 +20,7 @@
  
 #include "gia.h"
 #include "giaAig.h"
-#include "saig.h"
+#include "src/aig/saig/saig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -472,7 +472,7 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver )
             // this obj was abstracted before
             assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(pGia, pObj) );
             // if corresponding AIG object is not abstracted, remove abstraction
-            if ( !Vec_IntEntry(vGateClasses, Gia_Lit2Var(pObj->Value)) )
+            if ( !Vec_IntEntry(vGateClasses, Abc_Lit2Var(pObj->Value)) )
             {
                 Vec_IntWriteEntry( pGia->vGateClasses, i, 0 );
                 Counter++;
diff --git a/src/aig/gia/giaAbs.h b/src/aig/gia/giaAbs.h
index 090d5dca..366a4d8a 100644
--- a/src/aig/gia/giaAbs.h
+++ b/src/aig/gia/giaAbs.h
@@ -18,8 +18,8 @@
 
 ***********************************************************************/
  
-#ifndef __GIA_ABS_H__
-#define __GIA_ABS_H__
+#ifndef ABC__aig__gia__giaAbs_h
+#define ABC__aig__gia__giaAbs_h
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index fe30d0f0..3e7f2a01 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "gia.h"
-#include "satSolver2.h"
+#include "src/sat/bsat/satSolver2.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -210,7 +210,7 @@ Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs )
     int i, Entry, nFrames = Vec_IntEntry( vAbs, 0 );
     assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) );
     // get the bitmask
-    nObjMask = (1 << Gia_Base2Log(nObjs)) - 1;
+    nObjMask = (1 << Abc_Base2Log(nObjs)) - 1;
     assert( nObjs <= nObjMask );
     // go through objects
     vPresent = Vec_IntStart( nObjs );
@@ -248,7 +248,7 @@ static inline int Vta_ManReadFrameStart( Vec_Int_t * p, int nWords )
             pTotal[w] |= pThis[i];
     }
     for ( i = nWords * 32 - 1; i >= 0; i-- )
-        if ( Gia_InfoHasBit(pTotal, i) )
+        if ( Abc_InfoHasBit(pTotal, i) )
         {
             ABC_FREE( pTotal );
             return i+1;
@@ -716,7 +716,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p )
             if ( Gia_ObjIsRo(p->pGia, pObj) )
                 assert( pThis->iFrame == 0 && pThis->Value == VTA_VAR0 );
             else if ( Gia_ObjIsPi(p->pGia, pObj) && pThis->Value == VTA_VAR1 )
-                Gia_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
+                Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
         }
     }
     // perform refinement
@@ -776,7 +776,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p->pBins       = ABC_CALLOC( int, p->nBins );
     p->vOrder      = Vec_IntAlloc( 1013 );
     // abstraction
-    p->nObjBits    = Gia_Base2Log( Gia_ManObjNum(pGia) );
+    p->nObjBits    = Abc_Base2Log( Gia_ManObjNum(pGia) );
     p->nObjMask    = (1 << p->nObjBits) - 1;
     assert( Gia_ManObjNum(pGia) <= (int)p->nObjMask );
     p->nWords      = 1;
@@ -922,7 +922,8 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
 ***********************************************************************/
 void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames )
 {
-    unsigned * pInfo, * pCountAll, * pCountUni;
+    unsigned * pInfo;
+    int * pCountAll, * pCountUni;
     int i, k, iFrame, iObj, Entry;
     // print info about frames
     pCountAll = ABC_CALLOC( int, nFrames + 1 );
@@ -933,9 +934,9 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames )
         iFrame = (Entry >> p->nObjBits);
         assert( iFrame < nFrames );
         pInfo  = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj );
-        if ( Gia_InfoHasBit(pInfo, iFrame) == 0 )
+        if ( Abc_InfoHasBit(pInfo, iFrame) == 0 )
         {
-            Gia_InfoSetBit( pInfo, iFrame );
+            Abc_InfoSetBit( pInfo, iFrame );
             pCountUni[iFrame+1]++;
             pCountUni[0]++;
         }
@@ -1062,7 +1063,7 @@ static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f )
     Gia_Obj_t * pObj = Gia_ManPo(p->pGia, 0);
     Vta_Obj_t * pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f );
     assert( pThis != NULL && pThis->fAdded );
-    return Gia_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
+    return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) );
 }
 
 /**Function*************************************************************
@@ -1105,7 +1106,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
         if ( f < p->pPars->nFramesStart )
         {
             // load this timeframe
-            Vga_ManLoadSlice( p, Vec_PtrEntry(p->vFrames, f), 0 );
+            Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 );
             // run SAT solver
             vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status );
             assert( (vCore != NULL) == (Status == 1) );
@@ -1123,7 +1124,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                 {
                     pObj = Gia_ManObj( p->pGia, pThis->iObj );
                     if ( Gia_ObjIsPi(p->pGia, pObj) && sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) )
-                        Gia_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
+                        Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) );
                 }
             }
         }
@@ -1133,7 +1134,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             // load the time frame
             int Limit = Abc_MinInt(5, p->pPars->nFramesStart);
             for ( i = 1; i <= Limit; i++ )
-                Vga_ManLoadSlice( p, Vec_PtrEntry(p->vCores, f-i), i );
+                Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i );
             // iterate as long as there are counter-examples
             do {
                 vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status );
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 00148451..6da633e0 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -19,9 +19,9 @@
 ***********************************************************************/
 
 #include "giaAig.h"
-#include "fra.h"
-#include "dch.h"
-#include "dar.h"
+#include "src/proof/fra/fra.h"
+#include "src/proof/dch/dch.h"
+#include "src/opt/dar/dar.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -30,8 +30,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int Gia_ObjChild0Copy( Aig_Obj_t * pObj )  { return Gia_LitNotCond( Aig_ObjFanin0(pObj)->iData, Aig_ObjFaninC0(pObj) ); }
-static inline int Gia_ObjChild1Copy( Aig_Obj_t * pObj )  { return Gia_LitNotCond( Aig_ObjFanin1(pObj)->iData, Aig_ObjFaninC1(pObj) ); }
+static inline int Gia_ObjChild0Copy( Aig_Obj_t * pObj )  { return Abc_LitNotCond( Aig_ObjFanin0(pObj)->iData, Aig_ObjFaninC0(pObj) ); }
+static inline int Gia_ObjChild1Copy( Aig_Obj_t * pObj )  { return Abc_LitNotCond( Aig_ObjFanin1(pObj)->iData, Aig_ObjFaninC1(pObj) ); }
 
 static inline Aig_Obj_t * Gia_ObjChild0Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id )  { return Aig_NotCond( ppNodes[Gia_ObjFaninId0(pObj, Id)], Gia_ObjFaninC0(pObj) ); }
 static inline Aig_Obj_t * Gia_ObjChild1Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id )  { return Aig_NotCond( ppNodes[Gia_ObjFaninId1(pObj, Id)], Gia_ObjFaninC1(pObj) ); }
@@ -64,8 +64,8 @@ void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
     {
         int iObjNew, iNextNew;
         Gia_ManFromAig_rec( pNew, p, pNext );
-        iObjNew  = Gia_Lit2Var(pObj->iData);
-        iNextNew = Gia_Lit2Var(pNext->iData);
+        iObjNew  = Abc_Lit2Var(pObj->iData);
+        iNextNew = Abc_Lit2Var(pNext->iData);
         if ( pNew->pNexts )
             pNew->pNexts[iObjNew] = iNextNew;        
     }
@@ -89,7 +89,7 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
     int i;
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->nConstrs = p->nConstrs;
     // create room to store equivalences
     if ( p->pEquivs )
@@ -128,7 +128,7 @@ Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p )
     int i;
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->nConstrs = p->nConstrs;
     // create the PIs
     Aig_ManCleanData( p );
@@ -167,7 +167,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
     int i;
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->nConstrs = p->nConstrs;
     // create the PIs
     Aig_ManCleanData( p );
@@ -246,9 +246,9 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
     assert( !fChoices || (p->pNexts && p->pReprs) );
     // create the new manager
     pNew = Aig_ManStart( Gia_ManAndNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->nConstrs = p->nConstrs;
-//    pNew->pSpec = Gia_UtilStrsav( p->pName );
+//    pNew->pSpec = Abc_UtilStrsav( p->pName );
     // duplicate representation of choice nodes
     if ( fChoices )
         pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
@@ -293,9 +293,9 @@ Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta )
     assert( nOutDelta > 0 && Gia_ManCoNum(p) % nOutDelta == 0 );
     // create the new manager
     pNew = Aig_ManStart( Gia_ManAndNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->nConstrs = p->nConstrs;
-//    pNew->pSpec = Gia_UtilStrsav( p->pName );
+//    pNew->pSpec = Abc_UtilStrsav( p->pName );
     // create the PIs
     ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
     ppNodes[0] = Aig_ManConst0(pNew);
@@ -334,7 +334,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p )
     ppNodes = ABC_FALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
     // create the new manager
     pNew = Aig_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->nConstrs = p->nConstrs;
     // create the PIs
     Gia_ManForEachObj( p, pObj, i )
@@ -349,7 +349,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p )
             ppNodes[i] = Aig_ManConst0(pNew);
         else
             assert( 0 );
-        pObj->Value = Gia_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) );
+        pObj->Value = Abc_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) );
         assert( i == 0 || Aig_ObjId(ppNodes[i]) == i );
     }
     Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
@@ -402,8 +402,8 @@ void Gia_ManReprToAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
     // move pointers from AIG to GIA
     Aig_ManForEachObj( pAig, pObj, i )
     {
-        assert( i == 0 || !Gia_LitIsCompl(pObj->iData) );
-        pGiaObj = Gia_ManObj( pGia, Gia_Lit2Var(pObj->iData) );
+        assert( i == 0 || !Abc_LitIsCompl(pObj->iData) );
+        pGiaObj = Gia_ManObj( pGia, Abc_Lit2Var(pObj->iData) );
         pGiaObj->Value = i;
     }
     // set the pointers to the nodes in AIG
@@ -441,7 +441,7 @@ void Gia_ManReprToAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia )
         pGiaRepr = Gia_ObjReprObj( pGia, i );
         if ( pGiaRepr == NULL )
             continue;
-        Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, Gia_Lit2Var(pGiaRepr->Value)), Aig_ManObj(pAig, Gia_Lit2Var(pGiaObj->Value)) );
+        Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, Abc_Lit2Var(pGiaRepr->Value)), Aig_ManObj(pAig, Abc_Lit2Var(pGiaObj->Value)) );
     }
 }
 
@@ -472,8 +472,8 @@ void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia )
 //        Abc_Print( 1, "%d -> %d %d\n", i, Gia_ObjValue(pObjGia), Gia_ObjValue(pObjGia)/2 );
         if ( Gia_ObjIsCo(pObjGia) )
             continue;
-        assert( i == 0 || !Gia_LitIsCompl(Gia_ObjValue(pObjGia)) );
-        pObjAig  = Aig_ManObj( pAig, Gia_Lit2Var(Gia_ObjValue(pObjGia)) );
+        assert( i == 0 || !Abc_LitIsCompl(Gia_ObjValue(pObjGia)) );
+        pObjAig  = Aig_ManObj( pAig, Abc_Lit2Var(Gia_ObjValue(pObjGia)) );
         pObjAig->iData = i;
     }
     Aig_ManForEachObj( pAig, pObjAig, i )
diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h
index 1c0a24d5..6522a5bc 100644
--- a/src/aig/gia/giaAig.h
+++ b/src/aig/gia/giaAig.h
@@ -18,15 +18,15 @@
 
 ***********************************************************************/
  
-#ifndef __GIA_AIG_H__
-#define __GIA_AIG_H__
+#ifndef ABC__aig__gia__giaAig_h
+#define ABC__aig__gia__giaAig_h
 
 
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#include "aig.h"
+#include "src/aig/aig/aig.h"
 #include "gia.h"
 
 ABC_NAMESPACE_HEADER_START
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index db194c69..2ae070d3 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -146,7 +146,7 @@ int Gia_FileSize( char * pFileName )
 char * Gia_FileNameGeneric( char * FileName )
 {
     char * pDot, * pRes;
-    pRes = Gia_UtilStrsav( FileName );
+    pRes = Abc_UtilStrsav( FileName );
     if ( (pDot = strrchr( pRes, '.' )) )
         *pDot = 0;
     return pRes;
@@ -445,8 +445,8 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
     // allocate the empty AIG
     pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
     pName = Gia_FileNameGeneric( pFileName );
-    pNew->pName = Gia_UtilStrsav( pName );
-//    pNew->pSpec = Gia_UtilStrsav( pFileName );
+    pNew->pName = Abc_UtilStrsav( pName );
+//    pNew->pSpec = Abc_UtilStrsav( pFileName );
     ABC_FREE( pName );
     pNew->nConstrs = nConstr;
 
@@ -482,8 +482,8 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
         uLit1 = uLit  - Gia_ReadAigerDecode( &pCur );
         uLit0 = uLit1 - Gia_ReadAigerDecode( &pCur );
 //        assert( uLit1 > uLit0 );
-        iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
-        iNode1 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
+        iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
+        iNode1 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
         assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches );
 //        Vec_IntPush( vNodes, Gia_And(pNew, iNode0, iNode1) );
         Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) );
@@ -500,14 +500,14 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
         for ( i = 0; i < nLatches; i++ )
         {
             uLit0 = atoi( (char *)pCur );  while ( *pCur++ != '\n' );
-            iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+            iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
             Vec_IntPush( vDrivers, iNode0 );
         }
         // read the PO driver literals
         for ( i = 0; i < nOutputs; i++ )
         {
             uLit0 = atoi( (char *)pCur );  while ( *pCur++ != '\n' );
-            iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+            iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
             Vec_IntPush( vDrivers, iNode0 );
         }
 
@@ -518,14 +518,14 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
         for ( i = 0; i < nLatches; i++ )
         {
             uLit0 = Vec_IntEntry( vLits, i );
-            iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+            iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
             Vec_IntPush( vDrivers, iNode0 );
         }
         // read the PO driver literals
         for ( i = 0; i < nOutputs; i++ )
         {
             uLit0 = Vec_IntEntry( vLits, i+nLatches );
-            iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+            iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
             Vec_IntPush( vDrivers, iNode0 );
         }
         Vec_IntFree( vLits );
@@ -604,7 +604,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
             pCur++;
             // read model name
             ABC_FREE( pNew->pName );
-            pNew->pName = Gia_UtilStrsav( (char *)pCur );
+            pNew->pName = Abc_UtilStrsav( (char *)pCur );
         }
     }
     Vec_IntFree( vNodes );
@@ -753,8 +753,8 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
         uLit1 = uLit  - Gia_ReadAigerDecode( &pCur );
         uLit0 = uLit1 - Gia_ReadAigerDecode( &pCur );
 //        assert( uLit1 > uLit0 );
-        iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
-        iNode1 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
+        iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
+        iNode1 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
         assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches );
 //        Vec_IntPush( vNodes, Gia_And(pNew, iNode0, iNode1) );
         Vec_IntPush( vNodes, Gia_ManHashAnd(pNew, iNode0, iNode1) );
@@ -772,14 +772,14 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
         for ( i = 0; i < nLatches; i++ )
         {
             uLit0 = atoi( (char *)pCur );  while ( *pCur++ != '\n' );
-            iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+            iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
             Vec_IntPush( vDrivers, iNode0 );
         }
         // read the PO driver literals
         for ( i = 0; i < nOutputs; i++ )
         {
             uLit0 = atoi( (char *)pCur );  while ( *pCur++ != '\n' );
-            iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+            iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
             Vec_IntPush( vDrivers, iNode0 );
         }
 
@@ -790,14 +790,14 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
         for ( i = 0; i < nLatches; i++ )
         {
             uLit0 = Vec_IntEntry( vLits, i );
-            iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+            iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
             Vec_IntPush( vDrivers, iNode0 );
         }
         // read the PO driver literals
         for ( i = 0; i < nOutputs; i++ )
         {
             uLit0 = Vec_IntEntry( vLits, i+nLatches );
-            iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+            iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
             Vec_IntPush( vDrivers, iNode0 );
         }
         Vec_IntFree( vLits );
@@ -877,7 +877,7 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
             pCur++;
             // read model name
             ABC_FREE( pNew->pName );
-            pNew->pName = Gia_UtilStrsav( (char *)pCur );
+            pNew->pName = Abc_UtilStrsav( (char *)pCur );
         }
     }
 
@@ -1094,7 +1094,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
     {
         ABC_FREE( pNew->pName );
         pName = Gia_FileNameGeneric( pFileName );
-        pNew->pName = Gia_UtilStrsav( pName );
+        pNew->pName = Abc_UtilStrsav( pName );
 //        pNew->pSpec = Ioa_UtilStrsav( pFileName );
         ABC_FREE( pName );
     }
@@ -1246,30 +1246,30 @@ unsigned char * Gia_WriteEquivClasses( Gia_Man_t * p, int * pEquivSize )
     }
     pBuffer = ABC_ALLOC( unsigned char, sizeof(int) * (nItems + 1) );
     // write constant class
-    iPos = Gia_WriteAigerEncode( pBuffer, 4, Gia_Var2Lit(0, 1) );
+    iPos = Gia_WriteAigerEncode( pBuffer, 4, Abc_Var2Lit(0, 1) );
 //printf( "\nRepr = %d ", 0 );
     iPrevNode = 0;
     for ( iNode = 1; iNode < Gia_ManObjNum(p); iNode++ )
         if ( Gia_ObjIsConst(p, iNode) )
         {
 //printf( "Node = %d ", iNode );
-            iLit = Gia_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
+            iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
             iPrevNode = iNode;
-            iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iLit, 0) );
+            iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iLit, 0) );
         }
     // write non-constant classes
     iPrevRepr = 0;
     Gia_ManForEachClass( p, iRepr )
     {
 //printf( "\nRepr = %d ", iRepr );
-        iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iRepr - iPrevRepr, 1) );
+        iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iRepr - iPrevRepr, 1) );
         iPrevRepr = iPrevNode = iRepr;
         Gia_ClassForEachObj1( p, iRepr, iNode )
         {
 //printf( "Node = %d ", iNode );
-            iLit = Gia_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
+            iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
             iPrevNode = iNode;
-            iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iLit, 0) );
+            iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iLit, 0) );
         }
     }
     Gia_WriteInt( pBuffer, iPos );
@@ -1291,8 +1291,8 @@ unsigned char * Gia_WriteEquivClasses( Gia_Man_t * p, int * pEquivSize )
 int Gia_WriteDiffValue( unsigned char * pPos, int iPos, int iPrev, int iThis )
 {
     if ( iPrev < iThis )
-        return Gia_WriteAigerEncode( pPos, iPos, Gia_Var2Lit(iThis - iPrev, 1) );
-    return Gia_WriteAigerEncode( pPos, iPos, Gia_Var2Lit(iPrev - iThis, 0) );
+        return Gia_WriteAigerEncode( pPos, iPos, Abc_Var2Lit(iThis - iPrev, 1) );
+    return Gia_WriteAigerEncode( pPos, iPos, Abc_Var2Lit(iPrev - iThis, 0) );
 }
 
 /**Function*************************************************************
@@ -1420,7 +1420,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
     pBuffer = ABC_ALLOC( unsigned char, nBufferSize );
     Gia_ManForEachAnd( p, pObj, i )
     {
-        uLit  = Gia_Var2Lit( i, 0 );
+        uLit  = Abc_Var2Lit( i, 0 );
         uLit0 = Gia_ObjFaninLit0( pObj, i );
         uLit1 = Gia_ObjFaninLit1( pObj, i );
         assert( uLit0 < uLit1 );
diff --git a/src/aig/gia/giaBidec.c b/src/aig/gia/giaBidec.c
index fc17b582..54f98afd 100644
--- a/src/aig/gia/giaBidec.c
+++ b/src/aig/gia/giaBidec.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "gia.h"
-#include "bdc.h"
+#include "src/bool/bdc/bdc.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -28,7 +28,7 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int Bdc_FunObjCopy( Bdc_Fun_t * pObj )     { return Gia_LitNotCond( Bdc_FuncCopyInt(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) );  }
+static inline int Bdc_FunObjCopy( Bdc_Fun_t * pObj )     { return Abc_LitNotCond( Bdc_FuncCopyInt(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) );  }
 static inline int Bdc_FunFanin0Copy( Bdc_Fun_t * pObj )  { return Bdc_FunObjCopy( Bdc_FuncFanin0(pObj) );                                        }
 static inline int Bdc_FunFanin1Copy( Bdc_Fun_t * pObj )  { return Bdc_FunObjCopy( Bdc_FuncFanin1(pObj) );                                        }
 
@@ -109,7 +109,7 @@ unsigned * Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t
     int i, nWords, nVars;
     // get the number of variables and words
     nVars  = Vec_IntSize( vLeaves );
-    nWords = Gia_TruthWordNum( nVars );
+    nWords = Abc_TruthWordNum( nVars );
     // check the case of a constant
     if ( Gia_ObjIsConst0( Gia_Regular(pRoot) ) )
     {
@@ -263,7 +263,7 @@ Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose )
     Gia_ManConst0(p)->Value = 0;
     // start the new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
 //    Gia_ManCleanLevels( pNew, Gia_ManObjNum(p) );
     pManDec = Bdc_ManAlloc( pPars );
diff --git a/src/aig/gia/giaCCof.c b/src/aig/gia/giaCCof.c
index 38e5ccdf..b04d5953 100644
--- a/src/aig/gia/giaCCof.c
+++ b/src/aig/gia/giaCCof.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "gia.h"
-#include "satSolver.h"
+#include "src/sat/bsat/satSolver.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -134,10 +134,10 @@ void Gia_ManCofExtendSolver( Ccf_Man_t * p )
 }
 
 static inline int Gia_Obj0Copy( Vec_Int_t * vCopies, int Fan0, int fCompl0 )  
-{ return Gia_LitNotCond( Vec_IntEntry(vCopies, Fan0), fCompl0 ); }
+{ return Abc_LitNotCond( Vec_IntEntry(vCopies, Fan0), fCompl0 ); }
 
 static inline int Gia_Obj1Copy( Vec_Int_t * vCopies, int Fan1, int fCompl1 )  
-{ return Gia_LitNotCond( Vec_IntEntry(vCopies, Fan1), fCompl1 ); }
+{ return Abc_LitNotCond( Vec_IntEntry(vCopies, Fan1), fCompl1 ); }
  
 /**Function*************************************************************
 
@@ -173,7 +173,7 @@ void Gia_ManCofOneDerive_rec( Ccf_Man_t * p, int Id )
     else if ( Gia_ObjCioId(pObj) >= Gia_ManRegNum(p->pGia) ) // PI
         Res = sat_solver_var_value( p->pSat, Id );
     else
-        Res = Gia_Var2Lit( Id, 0 );
+        Res = Abc_Var2Lit( Id, 0 );
     Vec_IntWriteEntry( p->vCopies, Id, Res );
 }
 
@@ -193,15 +193,15 @@ int Gia_ManCofOneDerive( Ccf_Man_t * p, int LitProp )
     int LitOut;
     // derive the cofactor of the property node
     Vec_IntFill( p->vCopies, Gia_ManObjNum(p->pFrames), -1 );
-    Gia_ManCofOneDerive_rec( p, Gia_Lit2Var(LitProp) );
-    LitOut = Vec_IntEntry( p->vCopies, Gia_Lit2Var(LitProp) );
-    LitOut = Gia_LitNotCond( LitOut, Gia_LitIsCompl(LitProp) );
+    Gia_ManCofOneDerive_rec( p, Abc_Lit2Var(LitProp) );
+    LitOut = Vec_IntEntry( p->vCopies, Abc_Lit2Var(LitProp) );
+    LitOut = Abc_LitNotCond( LitOut, Abc_LitIsCompl(LitProp) );
     // add new PO for the cofactor
     Gia_ManAppendCo( p->pFrames, LitOut );
     // add SAT clauses
     Gia_ManCofExtendSolver( p );
     // return negative literal of the cofactor
-    return Gia_LitNot(LitOut);
+    return Abc_LitNot(LitOut);
 } 
 
 /**Function*************************************************************
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 745b19ba..d83f79e9 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -238,8 +238,8 @@ static inline void Cbs_ManSaveModel( Cbs_Man_t * p, Vec_Int_t * vCex )
     p->pProp.iHead = 0;
     Cbs_QueForEachEntry( p->pProp, pVar, i )
         if ( Gia_ObjIsCi(pVar) )
-//            Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) );
-            Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Cbs_VarValue(pVar)) );
+//            Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) );
+            Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Cbs_VarValue(pVar)) );
 } 
 
 /**Function*************************************************************
@@ -377,7 +377,7 @@ static inline int Cbs_VarFaninFanoutMax( Cbs_Man_t * p, Gia_Obj_t * pObj )
     assert( Gia_ObjIsAnd(pObj) );
     Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) );
     Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) );
-    return ABC_MAX( Count0, Count1 );
+    return Abc_MaxInt( Count0, Count1 );
 }
 
 /**Function*************************************************************
@@ -504,7 +504,7 @@ static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj, int Level, Gi
     Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 );
     assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail );
 //    s_Counter++;
-//    s_Counter = Abc_MaxInt( s_Counter, Vec_IntSize(p->vLevReas)/3 );
+//    s_Counter = Abc_MaxIntInt( s_Counter, Vec_IntSize(p->vLevReas)/3 );
 }
 
 
@@ -872,7 +872,7 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level )
     if ( Cbs_QueIsEmpty(&p->pJust) )
         return 0;
     // quit using resource limits
-    p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
+    p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
     if ( Cbs_ManCheckLimits( p ) )
         return 0;
     // remember the state before branching
@@ -946,7 +946,7 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj )
     p->pJust.iHead = p->pJust.iTail = 0;
     p->pClauses.iHead = p->pClauses.iTail = 1;
     p->Pars.nBTTotal += p->Pars.nBTThis;
-    p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
+    p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
     if ( Cbs_ManCheckLimits( p ) )
         RetValue = -1;
 
diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c
index 983081f0..8198c17f 100644
--- a/src/aig/gia/giaCSatOld.c
+++ b/src/aig/gia/giaCSatOld.c
@@ -213,8 +213,8 @@ static inline void Cbs0_ManSaveModel( Cbs0_Man_t * p, Vec_Int_t * vCex )
     p->pProp.iHead = 0;
     Cbs0_QueForEachEntry( p->pProp, pVar, i )
         if ( Gia_ObjIsCi(pVar) )
-//            Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs0_VarValue(pVar)) );
-            Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Cbs0_VarValue(pVar)) );
+//            Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs0_VarValue(pVar)) );
+            Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Cbs0_VarValue(pVar)) );
 } 
 
 /**Function*************************************************************
@@ -332,7 +332,7 @@ static inline int Cbs0_VarFaninFanoutMax( Cbs0_Man_t * p, Gia_Obj_t * pObj )
     assert( Gia_ObjIsAnd(pObj) );
     Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) );
     Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) );
-    return ABC_MAX( Count0, Count1 );
+    return Abc_MaxInt( Count0, Count1 );
 }
 
 /**Function*************************************************************
@@ -596,7 +596,7 @@ int Cbs0_ManSolve_rec( Cbs0_Man_t * p )
     if ( Cbs0_QueIsEmpty(&p->pJust) )
         return 0;
     // quit using resource limits
-    p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
+    p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
     if ( Cbs0_ManCheckLimits( p ) )
         return 0;
     // remember the state before branching
@@ -656,7 +656,7 @@ int Cbs0_ManSolve( Cbs0_Man_t * p, Gia_Obj_t * pObj )
     Cbs0_ManCancelUntil( p, 0 );
     p->pJust.iHead = p->pJust.iTail = 0;
     p->Pars.nBTTotal += p->Pars.nBTThis;
-    p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
+    p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
     if ( Cbs0_ManCheckLimits( p ) )
         RetValue = -1;
 //    printf( "Outcome = %2d.  Confs = %6d.  Decision level max = %3d.\n", 
diff --git a/src/aig/gia/giaCTas.c b/src/aig/gia/giaCTas.c
index c6aa3fec..7cfdac74 100644
--- a/src/aig/gia/giaCTas.c
+++ b/src/aig/gia/giaCTas.c
@@ -122,8 +122,8 @@ static inline void  Tas_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fM
 static inline int   Tas_VarIsJust( Gia_Obj_t * pVar )          { return Gia_ObjIsAnd(pVar) && !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)); } 
 static inline int   Tas_VarFanin0Value( Gia_Obj_t * pVar )     { return !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); }
 static inline int   Tas_VarFanin1Value( Gia_Obj_t * pVar )     { return !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); }
-static inline int   Tas_VarToLit( Tas_Man_t * p, Gia_Obj_t * pObj ) { assert( Tas_VarIsAssigned(pObj) ); return Gia_Var2Lit( Gia_ObjId(p->pAig, pObj), !Tas_VarValue(pObj) );     }
-static inline int   Tas_LitIsTrue( Gia_Obj_t * pObj, int Lit ) { assert( Tas_VarIsAssigned(pObj) ); return Tas_VarValue(pObj) != Gia_LitIsCompl(Lit);                             }
+static inline int   Tas_VarToLit( Tas_Man_t * p, Gia_Obj_t * pObj ) { assert( Tas_VarIsAssigned(pObj) ); return Abc_Var2Lit( Gia_ObjId(p->pAig, pObj), !Tas_VarValue(pObj) );     }
+static inline int   Tas_LitIsTrue( Gia_Obj_t * pObj, int Lit ) { assert( Tas_VarIsAssigned(pObj) ); return Tas_VarValue(pObj) != Abc_LitIsCompl(Lit);                             }
 
 static inline int         Tas_ClsHandle( Tas_Man_t * p, Tas_Cls_t * pClause ) { return ((int *)pClause) - p->pStore.pData;   }
 static inline Tas_Cls_t * Tas_ClsFromHandle( Tas_Man_t * p, int h )           { return (Tas_Cls_t *)(p->pStore.pData + h);   }
@@ -292,8 +292,8 @@ static inline void Tas_ManSaveModel( Tas_Man_t * p, Vec_Int_t * vCex )
     Tas_QueForEachEntry( p->pProp, pVar, i )
     {
         if ( Gia_ObjIsCi(pVar) )
-//            Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Tas_VarValue(pVar)) );
-            Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Tas_VarValue(pVar)) );
+//            Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Tas_VarValue(pVar)) );
+            Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Tas_VarValue(pVar)) );
 /*
         printf( "%5d(%d) = ", Gia_ObjId(p->pAig, pVar), Tas_VarValue(pVar) );
         if ( Gia_ObjIsCi(pVar) )
@@ -443,7 +443,7 @@ static inline int Tas_VarFaninFanoutMax( Tas_Man_t * p, Gia_Obj_t * pObj )
     assert( Gia_ObjIsAnd(pObj) );
     Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) );
     Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) );
-    return ABC_MAX( Count0, Count1 );
+    return Abc_MaxInt( Count0, Count1 );
 }
 
 
@@ -793,11 +793,11 @@ static inline void Tas_ManDeriveReason( Tas_Man_t * p, int Level )
         if ( Tas_VarHasReasonCls( p, pObj ) )
         {
             Tas_Cls_t * pCls = Tas_VarReasonCls( p, pObj );
-            pReason = Gia_ManObj( p->pAig, Gia_Lit2Var(pCls->pLits[0]) );
+            pReason = Gia_ManObj( p->pAig, Abc_Lit2Var(pCls->pLits[0]) );
             assert( pReason == pObj );
             for ( j = 1; j < pCls->nLits; j++ )
             {
-                pReason = Gia_ManObj( p->pAig, Gia_Lit2Var(pCls->pLits[j]) );
+                pReason = Gia_ManObj( p->pAig, Abc_Lit2Var(pCls->pLits[j]) );
                 iLitLevel2 = Tas_VarDecLevel( p, pReason );
                 assert( Tas_VarIsAssigned( pReason ) );
                 assert( !Tas_LitIsTrue( pReason, pCls->pLits[j] ) );
@@ -953,16 +953,16 @@ static inline Tas_Cls_t * Tas_ManAllocCls( Tas_Man_t * p, int nSize )
 ***********************************************************************/
 static inline void Tas_ManWatchClause( Tas_Man_t * p, Tas_Cls_t * pClause, int Lit )
 {
-    assert( Gia_Lit2Var(Lit) < Gia_ManObjNum(p->pAig) );
+    assert( Abc_Lit2Var(Lit) < Gia_ManObjNum(p->pAig) );
     assert( pClause->nLits >= 2 );
     assert( pClause->pLits[0] == Lit || pClause->pLits[1] == Lit );
     if ( pClause->pLits[0] == Lit )
-        pClause->iNext[0] = p->pWatches[Gia_LitNot(Lit)];  
+        pClause->iNext[0] = p->pWatches[Abc_LitNot(Lit)];  
     else
-        pClause->iNext[1] = p->pWatches[Gia_LitNot(Lit)];  
-    if ( p->pWatches[Gia_LitNot(Lit)] == 0 )
-        Vec_IntPush( p->vWatchLits, Gia_LitNot(Lit) );
-    p->pWatches[Gia_LitNot(Lit)] = Tas_ClsHandle( p, pClause );
+        pClause->iNext[1] = p->pWatches[Abc_LitNot(Lit)];  
+    if ( p->pWatches[Abc_LitNot(Lit)] == 0 )
+        Vec_IntPush( p->vWatchLits, Abc_LitNot(Lit) );
+    p->pWatches[Abc_LitNot(Lit)] = Tas_ClsHandle( p, pClause );
 }
 
 /**Function*************************************************************
@@ -994,7 +994,7 @@ static inline Tas_Cls_t * Tas_ManCreateCls( Tas_Man_t * p, int hClause )
     for ( i = hClause; (pObj = pQue->pData[i]); i++ )
     {
         assert( Tas_VarIsAssigned( pObj ) );
-        pClause->pLits[i-hClause] = Gia_LitNot( Tas_VarToLit(p, pObj) );
+        pClause->pLits[i-hClause] = Abc_LitNot( Tas_VarToLit(p, pObj) );
     }
     // add the clause as watched one
     if ( nLits >= 2 )
@@ -1027,7 +1027,7 @@ static inline int Tas_ManCreateFromCls( Tas_Man_t * p, Tas_Cls_t * pCls, int Lev
     Tas_QuePush( pQue, NULL );
     for ( i = 0; i < pCls->nLits; i++ )
     {
-        pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCls->pLits[i]) );
+        pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCls->pLits[i]) );
         assert( Tas_VarIsAssigned(pObj) );
         assert( !Tas_LitIsTrue( pObj, pCls->pLits[i] ) );
         Tas_QuePush( pQue, pObj );
@@ -1052,7 +1052,7 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit )
     Gia_Obj_t * pObj;
     Tas_Cls_t * pCur;
     int * piPrev, iCur, iTemp;
-    int i, LitF = Gia_LitNot(Lit);
+    int i, LitF = Abc_LitNot(Lit);
     // iterate through the clauses
     piPrev = p->pWatches + Lit;
     for ( iCur = p->pWatches[Lit]; iCur; iCur = *piPrev )
@@ -1070,8 +1070,8 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit )
         assert( pCur->pLits[1] == LitF );
 
         // if the first literal is true, the clause is satisfied
-//        if ( pCur->pLits[0] == p->pAssigns[Gia_Lit2Var(pCur->pLits[0])] )
-        pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCur->pLits[0]) );
+//        if ( pCur->pLits[0] == p->pAssigns[Abc_Lit2Var(pCur->pLits[0])] )
+        pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[0]) );
         if ( Tas_VarIsAssigned(pObj) && Tas_LitIsTrue( pObj, pCur->pLits[0] ) )
         {
             piPrev = &pCur->iNext[1];
@@ -1082,8 +1082,8 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit )
         for ( i = 2; i < (int)pCur->nLits; i++ )
         {
             // skip the case when the literal is false
-//            if ( Gia_LitNot(pCur->pLits[i]) == p->pAssigns[Gia_Lit2Var(pCur->pLits[i])] )
-            pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCur->pLits[i]) );
+//            if ( Abc_LitNot(pCur->pLits[i]) == p->pAssigns[Abc_Lit2Var(pCur->pLits[i])] )
+            pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[i]) );
             if ( Tas_VarIsAssigned(pObj) && !Tas_LitIsTrue( pObj, pCur->pLits[i] ) )
                 continue;
             // the literal is either true or unassigned - watch it
@@ -1099,7 +1099,7 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit )
             continue;
 
         // clause is unit - enqueue new implication
-        pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCur->pLits[0]) );
+        pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[0]) );
         if ( !Tas_VarIsAssigned(pObj) )
         {
 /*
@@ -1107,7 +1107,7 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit )
                 int iLitLevel, iPlace;
                 for ( i = 1; i < (int)pCur->nLits; i++ )
                 {
-                    pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCur->pLits[i]) );
+                    pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[i]) );
                     iLitLevel = Tas_VarDecLevel( p, pObj );
                     iPlace = pObj->Value;
                     printf( "Lit = %d. Level = %d. Place = %d.\n", pCur->pLits[i], iLitLevel, iPlace );
@@ -1300,7 +1300,7 @@ int Tas_ManSolve_rec( Tas_Man_t * p, int Level )
     if ( Tas_QueIsEmpty(&p->pJust) )
         return 0;
     // quit using resource limits
-    p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
+    p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead );
     if ( Tas_ManCheckLimits( p ) )
         return 0;
     // remember the state before branching
@@ -1401,7 +1401,7 @@ int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
     Vec_IntClear( p->vActiveVars );
     // statistics
     p->Pars.nBTTotal += p->Pars.nBTThis;
-    p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
+    p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
     if ( Tas_ManCheckLimits( p ) )
         RetValue = -1;
     return RetValue;
@@ -1460,7 +1460,7 @@ int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs )
     Vec_IntClear( p->vActiveVars );
     // statistics
     p->Pars.nBTTotal += p->Pars.nBTThis;
-    p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis );
+    p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis );
     if ( Tas_ManCheckLimits( p ) )
         RetValue = -1;
 
@@ -1644,19 +1644,19 @@ int Tas_StorePatternTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * p
     int i;
     for ( i = 0; i < nLits; i++ )
     {
-        pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
-        pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
-        if ( Gia_InfoHasBit( pPres, iBit ) && 
-             Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+        pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
+        pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
+        if ( Abc_InfoHasBit( pPres, iBit ) && 
+             Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
              return 0;
     }
     for ( i = 0; i < nLits; i++ )
     {
-        pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
-        pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
-        Gia_InfoSetBit( pPres, iBit );
-        if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
-            Gia_InfoXorBit( pInfo, iBit );
+        pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
+        pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
+        Abc_InfoSetBit( pPres, iBit );
+        if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
+            Abc_InfoXorBit( pInfo, iBit );
     }
     return 1;
 }
diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c
index 5a04d9d3..60dcf3af 100644
--- a/src/aig/gia/giaCof.c
+++ b/src/aig/gia/giaCof.c
@@ -457,7 +457,7 @@ int Cof_ManCountRemoved( Cof_Man_t * p, Cof_Obj_t * pRoot, int fConst1 )
     pRoot->iNext = 0;
     p->pLevels[LevelStart] = Cof_ObjHandle( p, pRoot );
     // set the new literal
-    pRoot->iLit = Gia_Var2Lit( 0, fConst1 );
+    pRoot->iLit = Abc_Var2Lit( 0, fConst1 );
     // process nodes in the levelized order
     for ( i = LevelStart; i < p->nLevels; i++ )
     {
@@ -465,7 +465,7 @@ int Cof_ManCountRemoved( Cof_Man_t * p, Cof_Obj_t * pRoot, int fConst1 )
               iHandle && (pTemp = Cof_ManObj(p, iHandle)); 
               iHandle = pTemp->iNext )
         {
-            assert( pTemp->Id != Gia_Lit2Var(pTemp->iLit) );
+            assert( pTemp->Id != Abc_Lit2Var(pTemp->iLit) );
             Cof_ObjForEachFanout( pTemp, pNext, k )
             {
                 if ( Cof_ObjIsCo(pNext) )
@@ -477,11 +477,11 @@ int Cof_ManCountRemoved( Cof_Man_t * p, Cof_Obj_t * pRoot, int fConst1 )
                 assert( pFanin0 == pTemp || pFanin1 == pTemp );
                 pNextGia = Gia_ManObj( p->pGia, pNext->Id );
                 if ( Cof_ObjIsTravIdCurrent(p, pFanin0) )
-                    iLit0 = Gia_LitNotCond( pFanin0->iLit, Gia_ObjFaninC0(pNextGia) );
+                    iLit0 = Abc_LitNotCond( pFanin0->iLit, Gia_ObjFaninC0(pNextGia) );
                 else
                     iLit0 = Gia_ObjFaninLit0( pNextGia, pNext->Id );
                 if ( Cof_ObjIsTravIdCurrent(p, pFanin1) )
-                    iLit1 = Gia_LitNotCond( pFanin1->iLit, Gia_ObjFaninC1(pNextGia) );
+                    iLit1 = Abc_LitNotCond( pFanin1->iLit, Gia_ObjFaninC1(pNextGia) );
                 else
                     iLit1 = Gia_ObjFaninLit1( pNextGia, pNext->Id );
                 iNextNew = Gia_ManHashAndTry( p->pGia, iLit0, iLit1 );
@@ -578,12 +578,12 @@ void Cof_ManPrintFanio( Cof_Man_t * p )
         nFanouts = Cof_ObjFanoutNum(pNode);
         nFaninsAll  += nFanins;
         nFanoutsAll += nFanouts;
-        nFaninsMax   = ABC_MAX( nFaninsMax, nFanins );
-        nFanoutsMax  = ABC_MAX( nFanoutsMax, nFanouts );
+        nFaninsMax   = Abc_MaxInt( nFaninsMax, nFanins );
+        nFanoutsMax  = Abc_MaxInt( nFanoutsMax, nFanouts );
     }
 
     // allocate storage for fanin/fanout numbers
-    nSizeMax = ABC_MAX( 10 * (Gia_Base10Log(nFaninsMax) + 1), 10 * (Gia_Base10Log(nFanoutsMax) + 1) );
+    nSizeMax = Abc_MaxInt( 10 * (Abc_Base10Log(nFaninsMax) + 1), 10 * (Abc_Base10Log(nFanoutsMax) + 1) );
     vFanins  = Vec_IntStart( nSizeMax );
     vFanouts = Vec_IntStart( nSizeMax );
 
@@ -717,7 +717,7 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar )
         return NULL;
     }
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
@@ -728,7 +728,7 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar )
         if ( pObj == pPivot )
         {
             iCofVar = pObj->Value;
-            pObj->Value = Gia_Var2Lit( 0, 0 );
+            pObj->Value = Abc_Var2Lit( 0, 0 );
         }
     }
     Gia_ManForEachAnd( p, pObj, i )
@@ -737,7 +737,7 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar )
         if ( pObj == pPivot )
         {
             iCofVar = pObj->Value;
-            pObj->Value = Gia_Var2Lit( 0, 0 );
+            pObj->Value = Abc_Var2Lit( 0, 0 );
         }
     }
     Gia_ManForEachCo( p, pObj, i )
@@ -745,15 +745,15 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar )
     // compute the positive cofactor
     Gia_ManForEachCi( p, pObj, i )
     {
-        pObj->Value = Gia_Var2Lit( Gia_ObjId(pNew, Gia_ManCi(pNew, i)), 0 );
+        pObj->Value = Abc_Var2Lit( Gia_ObjId(pNew, Gia_ManCi(pNew, i)), 0 );
         if ( pObj == pPivot )
-            pObj->Value = Gia_Var2Lit( 0, 1 );
+            pObj->Value = Abc_Var2Lit( 0, 1 );
     }
     Gia_ManForEachAnd( p, pObj, i )
     {
         pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         if ( pObj == pPivot )
-            pObj->Value = Gia_Var2Lit( 0, 1 );
+            pObj->Value = Abc_Var2Lit( 0, 1 );
     }
     // create MUXes
     assert( iCofVar > 0 );
@@ -836,9 +836,9 @@ Vec_Int_t * Gia_ManTransfer( Gia_Man_t * pAig, Gia_Man_t * pCof, Gia_Man_t * pNe
     Gia_ManForEachObjVec( vSigs, pAig, pObj, i )
     {
         assert( Gia_ObjIsCand(pObj) );
-        pObjF = Gia_ManObj( pCof, Gia_Lit2Var(pObj->Value) );
+        pObjF = Gia_ManObj( pCof, Abc_Lit2Var(pObj->Value) );
         if ( pObjF->Value && ~pObjF->Value )
-            Vec_IntPushUnique( vSigsNew, Gia_Lit2Var(pObjF->Value) );
+            Vec_IntPushUnique( vSigsNew, Abc_Lit2Var(pObjF->Value) );
     }
     return vSigsNew;    
 }
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 258687fe..b3c04acb 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -55,14 +55,14 @@ void Gia_ManDupRemapEquiv( Gia_Man_t * pNew, Gia_Man_t * p )
         Gia_ObjSetRepr( pNew, i, GIA_VOID );
     // iterate over constant candidates
     Gia_ManForEachConst( p, i )
-        Gia_ObjSetRepr( pNew, Gia_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
+        Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
     // iterate over class candidates
     vClass = Vec_IntAlloc( 100 );
     Gia_ManForEachClass( p, i )
     {
         Vec_IntClear( vClass );
         Gia_ClassForEachObj( p, i, k )
-            Vec_IntPushUnique( vClass, Gia_Lit2Var(Gia_ManObj(p, k)->Value) );
+            Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) );
         assert( Vec_IntSize( vClass ) > 1 );
         Vec_IntSort( vClass, 0 );
         iRepr = iPrev = Vec_IntEntry( vClass, 0 );
@@ -173,7 +173,7 @@ Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p )
     int i;
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManDupOrderDfs_rec( pNew, p, pObj );
@@ -205,7 +205,7 @@ Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop )
     int i;
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     for ( i = iOutStart; i < iOutStop; i++ )
     {
@@ -240,8 +240,8 @@ void Gia_ManDupOrderDfsChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t *
     pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     if ( pNext )
     {
-        pNew->pNexts[Gia_Lit2Var(pObj->Value)] = Gia_Lit2Var( Gia_Lit2Var(pNext->Value) );
-        assert( Gia_Lit2Var(pObj->Value) > Gia_Lit2Var(pNext->Value) );
+        pNew->pNexts[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var( Abc_Lit2Var(pNext->Value) );
+        assert( Abc_Lit2Var(pObj->Value) > Abc_Lit2Var(pNext->Value) );
     }
 } 
 
@@ -264,7 +264,7 @@ Gia_Man_t * Gia_ManDupOrderDfsChoices( Gia_Man_t * p )
     assert( p->pReprs && p->pNexts );
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
@@ -297,7 +297,7 @@ Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p )
     int i;
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCoReverse( p, pObj, i )
         Gia_ManDupOrderDfs_rec( pNew, p, pObj );
@@ -329,7 +329,7 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p )
     Gia_Obj_t * pObj;
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
@@ -361,7 +361,7 @@ Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState )
     Gia_Obj_t * pObj;
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachObj1( p, pObj, i )
     {
@@ -371,13 +371,13 @@ Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState )
         {
             pObj->Value = Gia_ManAppendCi( pNew );
             if ( Gia_ObjCioId(pObj) >= Gia_ManPiNum(p) )
-                pObj->Value = Gia_LitNotCond( pObj->Value, Gia_InfoHasBit((unsigned *)pInitState, Gia_ObjCioId(pObj) - Gia_ManPiNum(p)) );
+                pObj->Value = Abc_LitNotCond( pObj->Value, Abc_InfoHasBit((unsigned *)pInitState, Gia_ObjCioId(pObj) - Gia_ManPiNum(p)) );
         }
         else if ( Gia_ObjIsCo(pObj) )
         {
             pObj->Value = Gia_ObjFanin0Copy(pObj);
             if ( Gia_ObjCioId(pObj) >= Gia_ManPoNum(p) )
-                pObj->Value = Gia_LitNotCond( pObj->Value, Gia_InfoHasBit((unsigned *)pInitState, Gia_ObjCioId(pObj) - Gia_ManPoNum(p)) );
+                pObj->Value = Abc_LitNotCond( pObj->Value, Abc_InfoHasBit((unsigned *)pInitState, Gia_ObjCioId(pObj) - Gia_ManPoNum(p)) );
             pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
         }
     }
@@ -403,7 +403,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
     Gia_Obj_t * pObj;
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachObj1( p, pObj, i )
     {
@@ -437,7 +437,7 @@ Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p )
     Gia_Obj_t * pObj;
     int i, iCtrl;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
@@ -477,7 +477,7 @@ Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass )
     int i, Counter1 = 0, Counter2 = 0;
     assert( p->vFlopClasses != NULL );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachPi( p, pObj, i )
@@ -522,7 +522,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->nConstrs = p->nConstrs;
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachObj1( p, pObj, i )
     {
@@ -561,8 +561,8 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
 //            assert( ~pRepr->Value );
             if ( !~pRepr->Value )
                 continue;
-            if ( Gia_Lit2Var(pObj->Value) != Gia_Lit2Var(pRepr->Value) )
-                Gia_ObjSetRepr( pNew, Gia_Lit2Var(pObj->Value), Gia_Lit2Var(pRepr->Value) ); 
+            if ( Abc_Lit2Var(pObj->Value) != Abc_Lit2Var(pRepr->Value) )
+                Gia_ObjSetRepr( pNew, Abc_Lit2Var(pObj->Value), Abc_Lit2Var(pRepr->Value) ); 
         }
         pNew->pNexts = Gia_ManDeriveNexts( pNew );
     }
@@ -588,7 +588,7 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes )
     int i, t, Entry;
     assert( nTimes > 0 );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     vPis = Vec_IntAlloc( Gia_ManPiNum(p) * nTimes );
     vPos = Vec_IntAlloc( Gia_ManPoNum(p) * nTimes );
@@ -604,17 +604,17 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes )
             {
                 pObj->Value = Gia_ManAppendCi( pNew );
                 if ( Gia_ObjIsPi(p, pObj) )
-                    Vec_IntPush( vPis, Gia_Lit2Var(pObj->Value) );
+                    Vec_IntPush( vPis, Abc_Lit2Var(pObj->Value) );
                 else
-                    Vec_IntPush( vRos, Gia_Lit2Var(pObj->Value) );
+                    Vec_IntPush( vRos, Abc_Lit2Var(pObj->Value) );
             }
             else if ( Gia_ObjIsCo(pObj) )
             {
                 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
                 if ( Gia_ObjIsPo(p, pObj) )
-                    Vec_IntPush( vPos, Gia_Lit2Var(pObj->Value) );
+                    Vec_IntPush( vPos, Abc_Lit2Var(pObj->Value) );
                 else
-                    Vec_IntPush( vRis, Gia_Lit2Var(pObj->Value) );
+                    Vec_IntPush( vRis, Abc_Lit2Var(pObj->Value) );
             }
         }
     }
@@ -667,7 +667,7 @@ int Gia_ManDupDfs2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
     {
         Gia_Obj_t * pRepr = Gia_ManObj( p, p->pReprsOld[Gia_ObjId(p, pObj)] );
         pRepr->Value = Gia_ManDupDfs2_rec( pNew, p, pRepr );
-        return pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+        return pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
     }
     if ( Gia_ObjIsCi(pObj) )
         return pObj->Value = Gia_ManAppendCi(pNew);
@@ -698,7 +698,7 @@ Gia_Man_t * Gia_ManDupDfs2( Gia_Man_t * p )
     int i;
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManDupDfs2_rec( pNew, p, pObj );
@@ -756,7 +756,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
     Gia_Obj_t * pObj;
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
@@ -789,7 +789,7 @@ Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p )
     int i;
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
@@ -819,7 +819,7 @@ Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pRoot )
     assert( Gia_ObjIsCo(pRoot) );
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
@@ -847,14 +847,14 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits )
     int i, iLit, iLitRes;
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
     Vec_IntForEachEntry( vLits, iLit, i )
     {
-        iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Gia_Lit2Var(iLit)) );
-        Gia_ManAppendCo( pNew, Gia_LitNotCond( iLitRes, Gia_LitIsCompl(iLit)) );
+        iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Abc_Lit2Var(iLit)) );
+        Gia_ManAppendCo( pNew, Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iLit)) );
     }
     Gia_ManSetRegNum( pNew, 0 );
     return pNew;
@@ -877,7 +877,7 @@ Gia_Man_t * Gia_ManDupNormalized( Gia_Man_t * p )
     Gia_Obj_t * pObj;
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
@@ -908,7 +908,7 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos )
     int i;
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManSetRefs( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
@@ -943,7 +943,7 @@ Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 )
     assert( Gia_ManRegNum(p) == 0 );
     assert( Gia_ManRegNum(p2) == 0 );
     pNew = Gia_ManStart( Gia_ManObjNum(p)+Gia_ManObjNum(p2) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     // dup first AIG
     Gia_ManConst0(p)->Value = 0;
@@ -1005,13 +1005,13 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits
     int i;
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
     {
         pObj->Value = Gia_ManAppendCi(pNew);
         if ( ~pCi2Lit[i] )
-            pObj->Value = Gia_LitNotCond( Gia_ManObj(p, Gia_Lit2Var(pCi2Lit[i]))->Value, Gia_LitIsCompl(pCi2Lit[i]) );
+            pObj->Value = Abc_LitNotCond( Gia_ManObj(p, Abc_Lit2Var(pCi2Lit[i]))->Value, Abc_LitIsCompl(pCi2Lit[i]) );
     }
     Gia_ManHashAlloc( pNew );
     if ( vLits )
@@ -1019,8 +1019,8 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits
         int iLit, iLitRes;
         Vec_IntForEachEntry( vLits, iLit, i )
         {
-            iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Gia_Lit2Var(iLit)) );
-            Gia_ManAppendCo( pNew, Gia_LitNotCond( iLitRes, Gia_LitIsCompl(iLit)) );
+            iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Abc_Lit2Var(iLit)) );
+            Gia_ManAppendCo( pNew, Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iLit)) );
         }
     }
     else
@@ -1055,7 +1055,7 @@ Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p )
     assert( p->pReprsOld != NULL );
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
@@ -1112,7 +1112,7 @@ Gia_Man_t * Gia_ManDupTopAnd_iter( Gia_Man_t * p, int fVerbose )
     {
         if ( Gia_ObjIsCi(pObj) )
         {
-            Vec_IntPush( vLeaves, Gia_Var2Lit( Gia_ObjId(p, pObj), 0 ) );
+            Vec_IntPush( vLeaves, Abc_Var2Lit( Gia_ObjId(p, pObj), 0 ) );
             continue;
         }
         assert( Gia_ObjIsAnd(pObj) );
@@ -1132,16 +1132,16 @@ Gia_Man_t * Gia_ManDupTopAnd_iter( Gia_Man_t * p, int fVerbose )
     pVar2Val = ABC_FALLOC( char, Gia_ManObjNum(p) );
     Vec_IntForEachEntry( vLeaves, iLit, i )
     {
-        iObjId = Gia_Lit2Var(iLit);
+        iObjId = Abc_Lit2Var(iLit);
         pObj = Gia_ManObj(p, iObjId);
         if ( Gia_ObjIsCi(pObj) )
         {
-            pCi2Lit[Gia_ObjCioId(pObj)] = !Gia_LitIsCompl(iLit);
+            pCi2Lit[Gia_ObjCioId(pObj)] = !Abc_LitIsCompl(iLit);
             nCiLits++;
         }
         if ( pVar2Val[iObjId] != 0 && pVar2Val[iObjId] != 1 )
-            pVar2Val[iObjId] = Gia_LitIsCompl(iLit);
-        else if ( pVar2Val[iObjId] != Gia_LitIsCompl(iLit) )
+            pVar2Val[iObjId] = Abc_LitIsCompl(iLit);
+        else if ( pVar2Val[iObjId] != Abc_LitIsCompl(iLit) )
             break;
     }
     if ( i < Vec_IntSize(vLeaves) )
@@ -1156,7 +1156,7 @@ Gia_Man_t * Gia_ManDupTopAnd_iter( Gia_Man_t * p, int fVerbose )
     Vec_IntClear( vLeaves );
     Gia_ManForEachObj( p, pObj, i )
         if ( !Gia_ObjIsCi(pObj) && (pVar2Val[i] == 0 || pVar2Val[i] == 1) )
-            Vec_IntPush( vLeaves, Gia_Var2Lit(i, pVar2Val[i]) );
+            Vec_IntPush( vLeaves, Abc_Var2Lit(i, pVar2Val[i]) );
     if ( fVerbose )
         printf( "Detected %6d AND leaves and %6d CI leaves.\n", Vec_IntSize(vLeaves), nCiLits );
     // create the input map
@@ -1272,7 +1272,7 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq
     }
     // start the manager
     pNew = Gia_ManStart( Gia_ManObjNum(p0) + Gia_ManObjNum(p1) );
-    pNew->pName = Gia_UtilStrsav( "miter" );
+    pNew->pName = Abc_UtilStrsav( "miter" );
     // map combinational inputs
     Gia_ManFillValue( p0 );
     Gia_ManFillValue( p1 );
@@ -1372,7 +1372,7 @@ Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p )
     int i, iLit;
     assert( (Gia_ManPoNum(p) & 1) == 0 );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachCi( p, pObj, i )
@@ -1444,7 +1444,7 @@ Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias )
     }
     // start the new manager
     pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
-    pNew->pName = Gia_UtilStrsav( pGia0->pName );
+    pNew->pName = Abc_UtilStrsav( pGia0->pName );
     // create new CIs and assign them to the old manager CIs
     for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
     {
@@ -1485,7 +1485,7 @@ Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes )
     Gia_Obj_t * pObj;
     int i, nConstr = 0;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
@@ -1546,7 +1546,7 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
     Gia_ManFillValue( p );
     // start the new manager
     pNew = Gia_ManStart( 5000 );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     // create PIs
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachPi( p, pObj, i )
@@ -1647,7 +1647,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
 
     // start the new manager
     pNew = Gia_ManStart( 5000 );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     // create constant
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
@@ -1681,7 +1681,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
         {
             if ( !~pObj->Value )
                 continue;
-            assert( !Gia_LitIsCompl(pObj->Value) );
+            assert( !Abc_LitIsCompl(pObj->Value) );
             pCopy = Gia_ObjCopy( pTemp, pObj );
             if ( !~pCopy->Value )
             {
@@ -1689,7 +1689,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
                 pObj->Value = ~0;
                 continue;
             }
-            assert( !Gia_LitIsCompl(pCopy->Value) );
+            assert( !Abc_LitIsCompl(pCopy->Value) );
             pObj->Value = pCopy->Value;
         }
     }
diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c
index 5c7092a3..1daf52a1 100644
--- a/src/aig/gia/giaEmbed.c
+++ b/src/aig/gia/giaEmbed.c
@@ -20,7 +20,7 @@
 
 #include <math.h>
 #include "gia.h"
-#include "ioa.h"
+#include "src/aig/ioa/ioa.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -690,12 +690,12 @@ void Emb_ManPrintFanio( Emb_Man_t * p )
         nFanouts = Emb_ObjFanoutNum(pNode);
         nFaninsAll  += nFanins;
         nFanoutsAll += nFanouts;
-        nFaninsMax   = ABC_MAX( nFaninsMax, nFanins );
-        nFanoutsMax  = ABC_MAX( nFanoutsMax, nFanouts );
+        nFaninsMax   = Abc_MaxInt( nFaninsMax, nFanins );
+        nFanoutsMax  = Abc_MaxInt( nFanoutsMax, nFanouts );
     }
 
     // allocate storage for fanin/fanout numbers
-    nSizeMax = ABC_MAX( 10 * (Gia_Base10Log(nFaninsMax) + 1), 10 * (Gia_Base10Log(nFanoutsMax) + 1) );
+    nSizeMax = Abc_MaxInt( 10 * (Abc_Base10Log(nFaninsMax) + 1), 10 * (Abc_Base10Log(nFanoutsMax) + 1) );
     vFanins  = Vec_IntStart( nSizeMax );
     vFanouts = Vec_IntStart( nSizeMax );
 
@@ -1436,8 +1436,8 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols )
     pY0 = Emb_ManSol( p, 0 );
     for ( k = 0; k < p->nObjs; k++ )
     {
-        Min0 = ABC_MIN( Min0, pY0[k] );
-        Max0 = ABC_MAX( Max0, pY0[k] );
+        Min0 = Abc_MinInt( Min0, pY0[k] );
+        Max0 = Abc_MaxInt( Max0, pY0[k] );
     }
     Str0 = 1.0*GIA_PLACE_SIZE/(Max0 - Min0);
     // update the coordinates
@@ -1450,8 +1450,8 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols )
     pY1 = Emb_ManSol( p, 1 );
     for ( k = 0; k < p->nObjs; k++ )
     {
-        Min1 = ABC_MIN( Min1, pY1[k] );
-        Max1 = ABC_MAX( Max1, pY1[k] );
+        Min1 = Abc_MinInt( Min1, pY1[k] );
+        Max1 = Abc_MaxInt( Max1, pY1[k] );
     }
     Str1 = 1.0*GIA_PLACE_SIZE/(Max1 - Min1);
     // update the coordinates
@@ -1498,10 +1498,10 @@ double Emb_ManComputeHPWL( Emb_Man_t * p )
         iMinY = iMaxY = p->pPlacement[2*pThis->Value+1];
         Emb_ObjForEachFanout( pThis, pNext, k )
         {
-            iMinX = ABC_MIN( iMinX, p->pPlacement[2*pNext->Value+0] );
-            iMaxX = ABC_MAX( iMaxX, p->pPlacement[2*pNext->Value+0] );
-            iMinY = ABC_MIN( iMinY, p->pPlacement[2*pNext->Value+1] );
-            iMaxY = ABC_MAX( iMaxY, p->pPlacement[2*pNext->Value+1] );
+            iMinX = Abc_MinInt( iMinX, p->pPlacement[2*pNext->Value+0] );
+            iMaxX = Abc_MaxInt( iMaxX, p->pPlacement[2*pNext->Value+0] );
+            iMinY = Abc_MinInt( iMinY, p->pPlacement[2*pNext->Value+1] );
+            iMaxY = Abc_MaxInt( iMaxY, p->pPlacement[2*pNext->Value+1] );
         }
         Result += (iMaxX - iMinX) + (iMaxY - iMinY);
     }
@@ -1548,10 +1548,10 @@ void Emb_ManPlacementRefine( Emb_Man_t * p, int nIters, int fVerbose )
             iMinY = iMaxY = p->pPlacement[2*pThis->Value+1];
             Emb_ObjForEachFanout( pThis, pNext, k )
             {
-                iMinX = ABC_MIN( iMinX, p->pPlacement[2*pNext->Value+0] );
-                iMaxX = ABC_MAX( iMaxX, p->pPlacement[2*pNext->Value+0] );
-                iMinY = ABC_MIN( iMinY, p->pPlacement[2*pNext->Value+1] );
-                iMaxY = ABC_MAX( iMaxY, p->pPlacement[2*pNext->Value+1] );
+                iMinX = Abc_MinInt( iMinX, p->pPlacement[2*pNext->Value+0] );
+                iMaxX = Abc_MaxInt( iMaxX, p->pPlacement[2*pNext->Value+0] );
+                iMinY = Abc_MinInt( iMinY, p->pPlacement[2*pNext->Value+1] );
+                iMaxY = Abc_MaxInt( iMaxY, p->pPlacement[2*pNext->Value+1] );
             }
             pEdgeX[pThis->Value] = 0.5 * (iMaxX + iMinX);
             pEdgeY[pThis->Value] = 0.5 * (iMaxY + iMinY);
diff --git a/src/aig/gia/giaEnable.c b/src/aig/gia/giaEnable.c
index 37f0c94f..d23c0c3d 100644
--- a/src/aig/gia/giaEnable.c
+++ b/src/aig/gia/giaEnable.c
@@ -338,9 +338,9 @@ Vec_Int_t * Gia_ManTransferFrames( Gia_Man_t * pAig, Gia_Man_t * pFrames, int nF
         assert( Gia_ObjIsCand(pObj) );
         for ( f = 0; f < nFrames; f++ )
         {
-            pObjF = Gia_ManObj( pFrames, Gia_Lit2Var(Gia_ObjCopyF( pAig, f, pObj )) );
+            pObjF = Gia_ManObj( pFrames, Abc_Lit2Var(Gia_ObjCopyF( pAig, f, pObj )) );
             if ( pObjF->Value && ~pObjF->Value )
-                Vec_IntPushUnique( vSigsNew, Gia_Lit2Var(pObjF->Value) );
+                Vec_IntPushUnique( vSigsNew, Abc_Lit2Var(pObjF->Value) );
         }
     }
     return vSigsNew;    
@@ -365,7 +365,7 @@ Gia_Man_t * Gia_ManUnrollInit( Gia_Man_t * p, int nFrames )
     ABC_FREE( p->pCopies );
     p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) );
     pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachRo( p, pObj, i )
         Gia_ObjSetCopyF( p, 0, pObj, 0 );
@@ -440,7 +440,7 @@ Gia_Man_t * Gia_ManRemoveEnables2( Gia_Man_t * p )
     Gia_Obj_t * pThis, * pNode;
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
@@ -481,13 +481,13 @@ Gia_Man_t * Gia_ManRemoveEnables2( Gia_Man_t * p )
         {
 //            printf( "FlopIn compl = %d. FlopOut is d0. Complement = %d.\n", 
 //                Gia_ObjFaninC0(pFlopIn), Gia_IsComplement(pObj0) );
-            pFlopIn->Value = Gia_LitNotCond(Gia_Regular(pObj1)->Value, !Gia_IsComplement(pObj1));
+            pFlopIn->Value = Abc_LitNotCond(Gia_Regular(pObj1)->Value, !Gia_IsComplement(pObj1));
         }
         else if ( Gia_Regular(pObj1) == pFlopOut )
         {
 //            printf( "FlopIn compl = %d. FlopOut is d1. Complement = %d.\n", 
 //                Gia_ObjFaninC0(pFlopIn), Gia_IsComplement(pObj1) );
-            pFlopIn->Value = Gia_LitNotCond(Gia_Regular(pObj0)->Value, !Gia_IsComplement(pObj0));
+            pFlopIn->Value = Abc_LitNotCond(Gia_Regular(pObj0)->Value, !Gia_IsComplement(pObj0));
         }
     }
     Gia_ManForEachCo( p, pThis, i )
@@ -610,7 +610,7 @@ Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p )
     
 
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachObj1( p, pObj, i )
     {
@@ -627,7 +627,7 @@ Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p )
         if ( pData == NULL )
             pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
         else
-            pObj->Value = Gia_ManAppendCo( pNew, Gia_LitNotCond(Gia_Regular(pData)->Value, Gia_IsComplement(pData)) );
+            pObj->Value = Gia_ManAppendCo( pNew, Abc_LitNotCond(Gia_Regular(pData)->Value, Gia_IsComplement(pData)) );
     }
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     Vec_PtrFree( vDatas );
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index c93da86e..43724871 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "gia.h"
-#include "cec.h"
+#include "src/proof/cec/cec.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -417,7 +417,7 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj,
     if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) )
     {
         Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll, fDualOut );
-        pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+        pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
         return;
     }
     if ( ~pObj->Value )
@@ -474,7 +474,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
     if ( fDualOut )
         Gia_ManEquivSetColors( p, fVerbose );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
@@ -536,7 +536,7 @@ void Gia_ManEquivUpdatePointers( Gia_Man_t * p, Gia_Man_t * pNew )
     {
         if ( !~pObj->Value )
             continue;
-        pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
+        pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
         if ( pObjNew->fMark0 )
             pObj->Value = ~0;
     }
@@ -568,10 +568,10 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina
         pObj = Gia_ManObj( p, i );
         if ( !~pObj->Value )
             continue;
-        pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
-        if ( Gia_Lit2Var(pObjNew->Value) == 0 )
+        pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
+        if ( Abc_Lit2Var(pObjNew->Value) == 0 )
             continue;
-        Gia_ObjSetRepr( pFinal, Gia_Lit2Var(pObjNew->Value), 0 );
+        Gia_ObjSetRepr( pFinal, Abc_Lit2Var(pObjNew->Value), 0 );
     }
     // iterate over class candidates
     vClass = Vec_IntAlloc( 100 );
@@ -583,8 +583,8 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina
             pObj = Gia_ManObj( p, k );
             if ( !~pObj->Value )
                 continue;
-            pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
-            Vec_IntPushUnique( vClass, Gia_Lit2Var(pObjNew->Value) );
+            pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
+            Vec_IntPushUnique( vClass, Abc_Lit2Var(pObjNew->Value) );
         }
         if ( Vec_IntSize( vClass ) < 2 )
             continue;
@@ -624,14 +624,14 @@ Gia_Man_t * Gia_ManEquivRemapDfs( Gia_Man_t * p )
         Gia_ObjSetRepr( pNew, i, GIA_VOID );
     // iterate over constant candidates
     Gia_ManForEachConst( p, i )
-        Gia_ObjSetRepr( pNew, Gia_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
+        Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 );
     // iterate over class candidates
     vClass = Vec_IntAlloc( 100 );
     Gia_ManForEachClass( p, i )
     {
         Vec_IntClear( vClass );
         Gia_ClassForEachObj( p, i, k )
-            Vec_IntPushUnique( vClass, Gia_Lit2Var(Gia_ManObj(p, k)->Value) );
+            Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) );
         assert( Vec_IntSize( vClass ) > 1 );
         Vec_IntSort( vClass, 0 );
         iRepr = iPrev = Vec_IntEntry( vClass, 0 );
@@ -758,7 +758,7 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
 //    if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
     if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
         return;
-    iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+    iLitNew = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
     if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
     {
         if ( vTrace ) 
@@ -847,7 +847,7 @@ Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace )
     Gia_ManSetPhase( p );
     Gia_ManFillValue( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
@@ -917,7 +917,7 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
     if ( fDualOut )
         Gia_ManEquivSetColors( p, fVerbose );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
@@ -983,7 +983,7 @@ void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Ve
 //    if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
     if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) )
         return;
-    iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+    iLitNew = Abc_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
     if ( Gia_ObjCopyF(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
         Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjCopyF(p, f, pObj), iLitNew) );
     Gia_ObjSetCopyF( p, f, pObj, iLitNew );
@@ -1063,10 +1063,10 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames
     if ( fDualOut )
         Gia_ManEquivSetColors( p, 0 );
     pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachRo( p, pObj, i )
-        Gia_ObjSetCopyF( p, 0, pObj, Gia_InfoHasBit(pInit->pData, i) );
+        Gia_ObjSetCopyF( p, 0, pObj, Abc_InfoHasBit(pInit->pData, i) );
     for ( f = 0; f < nFrames; f++ )
     {
         Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
@@ -1463,7 +1463,7 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
     {
         if ( Gia_ObjIsConst0(pRepr) )
         {
-            pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+            pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
             return;
         }
         Gia_ManEquivToChoices_rec( pNew, p, pRepr );
@@ -1471,22 +1471,22 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
         Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
         Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
         pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-        if ( Gia_LitRegular(pObj->Value) == Gia_LitRegular(pRepr->Value) )
+        if ( Abc_LitRegular(pObj->Value) == Abc_LitRegular(pRepr->Value) )
         {
-            assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
+            assert( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
             return;
         }
         if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit
             return;
         assert( pRepr->Value < pObj->Value );
-        pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) );
-        pObjNew  = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
+        pReprNew = Gia_ManObj( pNew, Abc_Lit2Var(pRepr->Value) );
+        pObjNew  = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
         if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) )
         {
 //            assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew );
             if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) != pReprNew )
                 return;
-            pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+            pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
             return;
         }
         if ( !Gia_ObjCheckTfi( pNew, pReprNew, pObjNew ) )
@@ -1495,7 +1495,7 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
             Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
             Gia_ManAddNextEntry_rec( pNew, pReprNew, pObjNew ); 
         }
-        pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+        pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
         return;
     }
     assert( Gia_ObjIsAnd(pObj) );
@@ -1573,7 +1573,7 @@ Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
     assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
     Gia_ManSetPhase( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
     pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
     for ( i = 0; i < Gia_ManObjNum(p); i++ )
@@ -1654,9 +1654,9 @@ int Gia_ManCountChoices( Gia_Man_t * p )
 
 ABC_NAMESPACE_IMPL_END
 
-#include "aig.h"
-#include "saig.h"
-#include "cec.h"
+#include "src/aig/aig/aig.h"
+#include "src/aig/saig/saig.h"
+#include "src/proof/cec/cec.h"
 #include "giaAig.h"
 
 ABC_NAMESPACE_IMPL_START
@@ -1826,7 +1826,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
     {
         if ( pObj1->Value == ~0 )
             continue;
-        pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj1->Value) );
+        pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj1->Value) );
         pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
         pObj->fMark0 = 1;
     }
@@ -1835,7 +1835,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
     {
         if ( pObj2->Value == ~0 )
             continue;
-        pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj2->Value) );
+        pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj2->Value) );
         pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
         pObj->fMark1 = 1;
     }
@@ -1965,7 +1965,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
     {
         if ( pObj1->Value == ~0 )
             continue;
-        pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj1->Value) );
+        pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj1->Value) );
         pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
         pObj->fMark0 = 1;
     }
@@ -1974,7 +1974,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
     {
         if ( pObj2->Value == ~0 )
             continue;
-        pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj2->Value) );
+        pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj2->Value) );
         pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) );
         pObj->fMark1 = 1;
     }
diff --git a/src/aig/gia/giaEra.c b/src/aig/gia/giaEra.c
index ec3e1b1b..672149bc 100644
--- a/src/aig/gia/giaEra.c
+++ b/src/aig/gia/giaEra.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "gia.h"
-#include "mem.h"
+#include "src/misc/mem/mem.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -45,7 +45,7 @@ struct Gia_ManEra_t_
 {
     Gia_Man_t *    pAig;         // user's AIG manager
     int            nWordsSim;       // 2^(PInum)
-    int            nWordsDat;   // Gia_BitWordNum
+    int            nWordsDat;   // Abc_BitWordNum
     unsigned *     pDataSim;     // simulation data
     Mem_Fixed_t *  pMemory;      // memory manager
     Vec_Ptr_t *    vStates;      // reached states
@@ -83,12 +83,12 @@ Gia_ManEra_t * Gia_ManEraCreate( Gia_Man_t * pAig )
     int i;
     p = ABC_CALLOC( Gia_ManEra_t, 1 );
     p->pAig      = pAig;
-    p->nWordsSim = Gia_TruthWordNum( Gia_ManPiNum(pAig) );
-    p->nWordsDat = Gia_BitWordNum( Gia_ManRegNum(pAig) );
+    p->nWordsSim = Abc_TruthWordNum( Gia_ManPiNum(pAig) );
+    p->nWordsDat = Abc_BitWordNum( Gia_ManRegNum(pAig) );
     p->pDataSim  = ABC_ALLOC( unsigned, p->nWordsSim*Gia_ManObjNum(pAig) );
     p->pMemory   = Mem_FixedStart( sizeof(Gia_ObjEra_t) + sizeof(unsigned) * p->nWordsDat );
     p->vStates   = Vec_PtrAlloc( 100000 );
-    p->nBins     = Gia_PrimeCudd( 100000 );
+    p->nBins     = Abc_PrimeCudd( 100000 );
     p->pBins     = ABC_CALLOC( unsigned, p->nBins );
     Vec_PtrPush( p->vStates, NULL );
     // assign primary input values
@@ -226,7 +226,7 @@ void Gia_ManEraHashResize( Gia_ManEra_t * p )
     // replace the table
     pBinsOld = p->pBins;
     nBinsOld = p->nBins;
-    p->nBins = Gia_PrimeCudd( 3 * p->nBins ); 
+    p->nBins = Abc_PrimeCudd( 3 * p->nBins ); 
     p->pBins = ABC_CALLOC( unsigned, p->nBins );
     // rehash the entries from the old table
     Counter = 0;
@@ -266,7 +266,7 @@ void Gia_ManInsertState( Gia_ManEra_t * p, Gia_ObjEra_t * pState )
     Gia_ManForEachRo( p->pAig, pObj, i )
     {
         pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) );
-        if ( Gia_InfoHasBit(pState->pData, i) )
+        if ( Abc_InfoHasBit(pState->pData, i) )
             memset( pSimInfo, 0xff, sizeof(unsigned) * p->nWordsSim );
         else
             memset( pSimInfo, 0, sizeof(unsigned) * p->nWordsSim );
@@ -465,8 +465,8 @@ int Gia_ManAnalyzeResult( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int fMiter )
         Gia_ManForEachRi( p->pAig, pObj, i )
         {
             pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) );
-            if ( Gia_InfoHasBit(p->pStateNew->pData, i) != Gia_InfoHasBit(pSimInfo, k) )
-                Gia_InfoXorBit( p->pStateNew->pData, i );
+            if ( Abc_InfoHasBit(p->pStateNew->pData, i) != Abc_InfoHasBit(pSimInfo, k) )
+                Abc_InfoXorBit( p->pStateNew->pData, i );
         }
         piPlace = Gia_ManEraHashFind( p, p->pStateNew );
         if ( piPlace == NULL )
diff --git a/src/aig/gia/giaEra2.c b/src/aig/gia/giaEra2.c
index b3e516eb..265335e2 100644
--- a/src/aig/gia/giaEra2.c
+++ b/src/aig/gia/giaEra2.c
@@ -136,11 +136,11 @@ static inline Gia_ObjAre_t *  Gia_ObjNextObj0( Gia_ManAre_t * p, Gia_ObjAre_t *
 static inline Gia_ObjAre_t *  Gia_ObjNextObj1( Gia_ManAre_t * p, Gia_ObjAre_t * q )   { return Gia_ManAreObj( p, q->F[1] );                      }
 static inline Gia_ObjAre_t *  Gia_ObjNextObj2( Gia_ManAre_t * p, Gia_ObjAre_t * q )   { return Gia_ManAreObj( p, q->F[2] );                      }
 
-static inline int             Gia_StaHasValue0( Gia_StaAre_t * p, int iReg )          { return Gia_InfoHasBit( p->pData,  iReg << 1 );           }
-static inline int             Gia_StaHasValue1( Gia_StaAre_t * p, int iReg )          { return Gia_InfoHasBit( p->pData, (iReg << 1) + 1 );      }
+static inline int             Gia_StaHasValue0( Gia_StaAre_t * p, int iReg )          { return Abc_InfoHasBit( p->pData,  iReg << 1 );           }
+static inline int             Gia_StaHasValue1( Gia_StaAre_t * p, int iReg )          { return Abc_InfoHasBit( p->pData, (iReg << 1) + 1 );      }
 
-static inline void            Gia_StaSetValue0( Gia_StaAre_t * p, int iReg )          { Gia_InfoSetBit( p->pData,  iReg << 1 );                  }
-static inline void            Gia_StaSetValue1( Gia_StaAre_t * p, int iReg )          { Gia_InfoSetBit( p->pData, (iReg << 1) + 1 );             }
+static inline void            Gia_StaSetValue0( Gia_StaAre_t * p, int iReg )          { Abc_InfoSetBit( p->pData,  iReg << 1 );                  }
+static inline void            Gia_StaSetValue1( Gia_StaAre_t * p, int iReg )          { Abc_InfoSetBit( p->pData, (iReg << 1) + 1 );             }
 
 static inline Gia_StaAre_t *  Gia_StaPrev( Gia_ManAre_t * p, Gia_StaAre_t * pS )      { return Gia_ManAreSta(p, pS->iPrev);                      }
 static inline Gia_StaAre_t *  Gia_StaNext( Gia_ManAre_t * p, Gia_StaAre_t * pS )      { return Gia_ManAreSta(p, pS->iNext);                      }
@@ -198,7 +198,7 @@ void Gia_ManCountMintermsInCube( Gia_StaAre_t * pCube, int nVars, unsigned * pSt
         for ( i = 0; i < nVars; i++ )
             if ( m & (1 << i) )
                 Mint |= (1 << Dashes[i]);
-        Gia_InfoSetBit( pStore, Mint );
+        Abc_InfoSetBit( pStore, Mint );
     }
 }
 
@@ -220,7 +220,7 @@ int Gia_ManCountMinterms( Gia_ManAre_t * p )
     int i, nMemSize, Counter = 0;
     if ( Gia_ManRegNum(p->pAig) > 30 )
         return -1;
-    nMemSize = Gia_BitWordNum( 1 << Gia_ManRegNum(p->pAig) );
+    nMemSize = Abc_BitWordNum( 1 << Gia_ManRegNum(p->pAig) );
     pMemory  = ABC_CALLOC( unsigned, nMemSize );
     Gia_ManAreForEachCubeStore( p, pCube, i )
         if ( Gia_StaIsUsed(pCube) )
@@ -477,7 +477,7 @@ Gia_ManAre_t * Gia_ManAreCreate( Gia_Man_t * pAig )
     assert( sizeof(Gia_ObjAre_t) == 16 );
     p = ABC_CALLOC( Gia_ManAre_t, 1 );
     p->pAig       = pAig;
-    p->nWords     = Gia_BitWordNum( 2 * Gia_ManRegNum(pAig) );
+    p->nWords     = Abc_BitWordNum( 2 * Gia_ManRegNum(pAig) );
     p->nSize      = sizeof(Gia_StaAre_t)/4 + p->nWords;
     p->ppObjs     = ABC_CALLOC( unsigned *, MAX_PAGE_NUM );
     p->ppStas     = ABC_CALLOC( unsigned *, MAX_PAGE_NUM );
@@ -1421,7 +1421,7 @@ static inline Gia_Obj_t * Gia_ManAreMostUsedPi( Gia_ManAre_t * p )
         if ( pObj->Value <= 1 )
             continue;
         Gia_ManIncrementTravId( p->pNew );
-        Gia_ManAreMostUsedPi_rec( p->pNew, Gia_ManObj(p->pNew, Gia_Lit2Var(pObj->Value)) );
+        Gia_ManAreMostUsedPi_rec( p->pNew, Gia_ManObj(p->pNew, Abc_Lit2Var(pObj->Value)) );
     }
     // check the CI counters
     Gia_ManForEachCi( p->pNew, pObj, i )
@@ -1471,7 +1471,7 @@ static inline int Gia_ManCheckPOs( Gia_ManAre_t * p )
     int i, CountCur, CountMax = 0;
     Gia_ManForEachPo( p->pAig, pObj, i )
     {
-        pObjNew = Gia_ManObj( p->pNew, Gia_Lit2Var(pObj->Value) );
+        pObjNew = Gia_ManObj( p->pNew, Abc_Lit2Var(pObj->Value) );
         if ( Gia_ObjIsConst0(pObjNew) )
             CountCur = 0;
         else 
@@ -1479,7 +1479,7 @@ static inline int Gia_ManCheckPOs( Gia_ManAre_t * p )
             Gia_ManIncrementTravId( p->pNew );
             CountCur = Gia_ManCheckPOs_rec( p->pNew, pObjNew );
         }
-        CountMax = ABC_MAX( CountMax, CountCur );
+        CountMax = Abc_MaxInt( CountMax, CountCur );
     }
     return CountMax;
 }
@@ -1501,10 +1501,10 @@ static inline int Gia_ManCheckPOstatus( Gia_ManAre_t * p )
     int i;
     Gia_ManForEachPo( p->pAig, pObj, i )
     {
-        pObjNew = Gia_ManObj( p->pNew, Gia_Lit2Var(pObj->Value) );
+        pObjNew = Gia_ManObj( p->pNew, Abc_Lit2Var(pObj->Value) );
         if ( Gia_ObjIsConst0(pObjNew) )
         {
-            if ( Gia_LitIsCompl(pObj->Value) )
+            if ( Abc_LitIsCompl(pObj->Value) )
             {
                 p->iOutFail = i;
                 return 1;
@@ -1638,7 +1638,7 @@ int Gia_ManAreDeriveNexts( Gia_ManAre_t * p, Gia_PtrAre_t Sta )
         else if ( Gia_StaHasValue1( pSta, i ) )
             pObj->Value = 1;
         else // don't-care literal
-            pObj->Value = Gia_Var2Lit( Gia_ObjId( p->pNew, Gia_ManCi(p->pNew, Gia_ObjCioId(pObj)) ), 0 );
+            pObj->Value = Abc_Var2Lit( Gia_ObjId( p->pNew, Gia_ManCi(p->pNew, Gia_ObjCioId(pObj)) ), 0 );
     }
     Gia_ManForEachAnd( p->pAig, pObj, i )
         pObj->Value = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
@@ -1770,8 +1770,8 @@ int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbos
 ABC_NAMESPACE_IMPL_END
 
 #include "giaAig.h"
-#include "cnf.h"
-#include "satSolver.h"
+#include "src/sat/cnf/cnf.h"
+#include "src/sat/bsat/satSolver.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -1848,22 +1848,22 @@ void Gia_ManAreDeriveCexSat( Gia_ManAre_t * p, Gia_StaAre_t * pCur, Gia_StaAre_t
     for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
     {
         if ( Gia_StaHasValue0(pCur, i) )
-            Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 1 ) );
+            Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 1 ) );
         else if ( Gia_StaHasValue1(pCur, i) )
-            Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 0 ) );
+            Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 0 ) );
     }
     if ( pNext )
     for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
     {
         if ( Gia_StaHasValue0(pNext, i) )
-            Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 1 ) );
+            Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 1 ) );
         else if ( Gia_StaHasValue1(pNext, i) )
-            Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 0 ) );
+            Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 0 ) );
     }
     if ( iOutFailed >= 0 )
     {
         assert( iOutFailed < Gia_ManPoNum(p->pAig) );
-        Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCos, iOutFailed), 0 ) );
+        Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, iOutFailed), 0 ) );
     }
     // solve SAT
     status = sat_solver_solve( (sat_solver *)p->pSat, (int *)Vec_IntArray(p->vAssumps), (int *)Vec_IntArray(p->vAssumps) + Vec_IntSize(p->vAssumps), 
@@ -1935,7 +1935,7 @@ Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast )
         Vec_IntForEachEntry( p->vCofVars, Var, v )
         {
             assert( Var < Gia_ManPiNum(p->pAig) );
-            Gia_InfoSetBit( pCex->pData, Gia_ManRegNum(p->pAig) + (Vec_PtrSize(vStates)-1-i) * Gia_ManPiNum(p->pAig) + Var );
+            Abc_InfoSetBit( pCex->pData, Gia_ManRegNum(p->pAig) + (Vec_PtrSize(vStates)-1-i) * Gia_ManPiNum(p->pAig) + Var );
         }
     }
     // free temporary things
diff --git a/src/aig/gia/giaFanout.c b/src/aig/gia/giaFanout.c
index c3e39405..412594ad 100644
--- a/src/aig/gia/giaFanout.c
+++ b/src/aig/gia/giaFanout.c
@@ -120,7 +120,7 @@ void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout )
     assert( Gia_ObjId(p, pFanout) > 0 );
     if ( Gia_ObjId(p, pObj) >= p->nFansAlloc || Gia_ObjId(p, pFanout) >= p->nFansAlloc )
     {
-        int nFansAlloc = 2 * ABC_MAX( Gia_ObjId(p, pObj), Gia_ObjId(p, pFanout) ); 
+        int nFansAlloc = 2 * Abc_MaxInt( Gia_ObjId(p, pObj), Gia_ObjId(p, pFanout) ); 
         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/gia/giaForce.c b/src/aig/gia/giaForce.c
index b9135404..6927266b 100644
--- a/src/aig/gia/giaForce.c
+++ b/src/aig/gia/giaForce.c
@@ -609,7 +609,7 @@ int Frc_ManCrossCut_rec( Frc_Man_t * p, Frc_Obj_t * pObj )
         Frc_Obj_t * pFanin;
         int i;
         p->nCutCur++;
-        p->nCutMax = ABC_MAX( p->nCutMax, p->nCutCur );
+        p->nCutMax = Abc_MaxInt( p->nCutMax, p->nCutCur );
         if ( !Frc_ObjIsCi(pObj) )
             Frc_ObjForEachFanin( pObj, pFanin, i )
                 p->nCutCur -= Frc_ManCrossCut_rec( p, pFanin );
@@ -636,7 +636,7 @@ int Frc_ManCrossCut2_rec( Frc_Man_t * p, Frc_Obj_t * pObj )
         Frc_Obj_t * pFanin;
         int i;
         p->nCutCur++;
-        p->nCutMax = ABC_MAX( p->nCutMax, p->nCutCur );
+        p->nCutMax = Abc_MaxInt( p->nCutMax, p->nCutCur );
         if ( !Frc_ObjIsCi(pObj) )
             Frc_ObjForEachFaninReverse( pObj, pFanin, i )
                 p->nCutCur -= Frc_ManCrossCut2_rec( p, pFanin );
@@ -912,8 +912,8 @@ void Frc_ManPlacementRefine( Frc_Man_t * p, int nIters, int fVerbose )
             iMinX = iMaxX = pThis->pPlace;
             Frc_ObjForEachFanout( pThis, pNext, k )
             {
-                iMinX = ABC_MIN( iMinX, pNext->pPlace );
-                iMaxX = ABC_MAX( iMaxX, pNext->pPlace );
+                iMinX = Abc_MinInt( iMinX, pNext->pPlace );
+                iMaxX = Abc_MaxInt( iMaxX, pNext->pPlace );
             }
             pThis->fEdgeCenter = 0.5 * (iMaxX + iMinX);
             CostThis += (iMaxX - iMinX);
diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c
index 480326bd..237e6c5c 100644
--- a/src/aig/gia/giaFrames.c
+++ b/src/aig/gia/giaFrames.c
@@ -90,7 +90,7 @@ void Gia_ManUnrollDup_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj, int Id )
         pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     }
     else assert( 0 );
-    Gia_ManObj(pNew, Gia_Lit2Var(pObj->Value))->Value = Id;
+    Gia_ManObj(pNew, Abc_Lit2Var(pObj->Value))->Value = Id;
 }
 
 /**Function*************************************************************
@@ -111,7 +111,7 @@ Gia_Man_t * Gia_ManUnrollDup( Gia_Man_t * p, Vec_Int_t * vLimit )
     int i;
     assert( Vec_IntSize(vLimit) == 0 );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
 
     // save constant class
     Gia_ManFillValue( p );
@@ -161,7 +161,7 @@ Vec_Ptr_t * Gia_ManUnrollAbs( Gia_Man_t * p, int nFrames )
     int nObjBits, nObjMask;
     int f, fMax, k, Entry, Prev, iStart, iStop, Size;
     // get the bitmasks
-    nObjBits = Gia_Base2Log( Gia_ManObjNum(p) );
+    nObjBits = Abc_Base2Log( Gia_ManObjNum(p) );
     nObjMask = (1 << nObjBits) - 1;
     assert( Gia_ManObjNum(p) <= nObjMask );
     // derive the tents
@@ -349,12 +349,12 @@ static inline int Gia_ObjUnrRead( Gia_ManUnr_t * p, int Id, int Degree )
 static inline int Gia_ObjUnrReadCopy0( Gia_ManUnr_t * p, Gia_Obj_t * pObj, int Id )  
 {
     int Lit = Gia_ObjUnrRead(p, Gia_ObjFaninId0(pObj, Id), Vec_IntEntry(p->vDegDiff, 2*Id));
-    return Gia_LitNotCond( Lit, Gia_ObjFaninC0(pObj) );
+    return Abc_LitNotCond( Lit, Gia_ObjFaninC0(pObj) );
 }
 static inline int Gia_ObjUnrReadCopy1( Gia_ManUnr_t * p, Gia_Obj_t * pObj, int Id )  
 {
     int Lit = Gia_ObjUnrRead(p, Gia_ObjFaninId1(pObj, Id), Vec_IntEntry(p->vDegDiff, 2*Id+1));
-    return Gia_LitNotCond( Lit, Gia_ObjFaninC1(pObj) );
+    return Abc_LitNotCond( Lit, Gia_ObjFaninC1(pObj) );
 }
 static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t * pNew )  
 {
@@ -367,7 +367,7 @@ static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t *
             pObj = Gia_ManPi( pNew, Gia_ManPiNum(p->pAig) * f + Gia_ObjCioId(pObjReal) );
         else
             pObj = Gia_ManPi( pNew, Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * f + Gia_ObjCioId(pObjReal) );
-        return Gia_Var2Lit( Gia_ObjId(pNew, pObj), 0 );
+        return Abc_Var2Lit( Gia_ObjId(pNew, pObj), 0 );
     }
     if ( f == 0 ) // initialize!
     {
@@ -378,9 +378,9 @@ static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t *
             pObj = Gia_ManPi( pNew, Gia_ManPiNum(p->pAig) * p->pPars->nFrames + Gia_ObjCioId(pObjReal)-Gia_ManPiNum(p->pAig) );
         else
             pObj = Gia_ManPi( pNew, Gia_ObjCioId(pObjReal)-Gia_ManPiNum(p->pAig) );
-        return Gia_Var2Lit( Gia_ObjId(pNew, pObj), 0 );
+        return Abc_Var2Lit( Gia_ObjId(pNew, pObj), 0 );
     }
-    pObj = Gia_ManObj( p->pOrder, Gia_Lit2Var(Gia_ObjRoToRi(p->pAig, pObjReal)->Value) );
+    pObj = Gia_ManObj( p->pOrder, Abc_Lit2Var(Gia_ObjRoToRi(p->pAig, pObjReal)->Value) );
     assert( Gia_ObjIsCo(pObj) );
     return Gia_ObjUnrRead( p, Gia_ObjId(p->pOrder, pObj), 0 );
 }
@@ -405,7 +405,7 @@ void * Gia_ManUnrollStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
     // start timeframes
     assert( p->pNew == NULL );
     p->pNew = Gia_ManStart( 10000 );
-    p->pNew->pName = Gia_UtilStrsav( p->pAig->pName );
+    p->pNew->pName = Abc_UtilStrsav( p->pAig->pName );
     Gia_ManHashAlloc( p->pNew );
     // create combinational inputs
     if ( !p->pPars->fSaveLastLit ) // only in the case when unrolling depth is known
@@ -541,7 +541,7 @@ Gia_Man_t * Gia_ManUnroll( Gia_ManUnr_t * p )
     int fMax, f, i, Lit, Beg, End;
     // start timeframes
     pNew = Gia_ManStart( 10000 );
-    pNew->pName = Gia_UtilStrsav( p->pAig->pName );
+    pNew->pName = Abc_UtilStrsav( p->pAig->pName );
     Gia_ManHashAlloc( pNew );
     // create combinational inputs
     for ( f = 0; f < p->pPars->nFrames; f++ )
@@ -754,7 +754,7 @@ Gia_Man_t * Gia_ManFramesInit( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
     Gia_ManFraSupports( p );
     pFrames = Gia_ManStart( Vec_VecSizeSize((Vec_Vec_t*)p->vIns)+
         Vec_VecSizeSize((Vec_Vec_t*)p->vAnds)+Vec_VecSizeSize((Vec_Vec_t*)p->vOuts) );
-    pFrames->pName = Gia_UtilStrsav( pAig->pName );
+    pFrames->pName = Abc_UtilStrsav( pAig->pName );
     Gia_ManHashAlloc( pFrames );
     Gia_ManConst0(pAig)->Value = 0;
     for ( f = 0; f < pPars->nFrames; f++ )
@@ -864,7 +864,7 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
     if ( pPars->fInit )
         return Gia_ManFramesInit( pAig, pPars );
     pFrames = Gia_ManStart( pPars->nFrames * Gia_ManObjNum(pAig) );
-    pFrames->pName = Gia_UtilStrsav( pAig->pName );
+    pFrames->pName = Abc_UtilStrsav( pAig->pName );
     Gia_ManHashAlloc( pFrames );
     Gia_ManConst0(pAig)->Value = 0;
     for ( f = 0; f < pPars->nFrames; f++ )
diff --git a/src/aig/gia/giaFront.c b/src/aig/gia/giaFront.c
index 6eb20635..903a66e7 100644
--- a/src/aig/gia/giaFront.c
+++ b/src/aig/gia/giaFront.c
@@ -115,7 +115,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
     Gia_ManSetRefs( p );
     // start the new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->nFront = 1 + (int)((float)1.1 * nCrossCutMaxInit); 
     // start the frontier
     pFront = ABC_CALLOC( char, pNew->nFront );
@@ -134,7 +134,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
                 nCrossCutMax = nCrossCut;
             // create new node
             iLit = Gia_ManAppendCi( pNew );
-            pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(iLit) );
+            pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(iLit) );
             assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
             pObjNew->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront );
             // handle CIs without fanout
@@ -147,7 +147,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p )
             assert( Gia_ObjValue(pObj) == 0 );
             // create new node
             iLit = Gia_ManAppendCo( pNew, 0 );
-            pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(iLit) );
+            pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(iLit) );
             assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) );
             // get the fanin
             pFanin0New = Gia_ManObj( pNew, Gia_ObjFaninId0(pObj, i) );
diff --git a/src/aig/gia/giaGiarf.c b/src/aig/gia/giaGiarf.c
index 501f9bb3..2f18c16d 100644
--- a/src/aig/gia/giaGiarf.c
+++ b/src/aig/gia/giaGiarf.c
@@ -301,7 +301,7 @@ int Hcd_ManHashKey( unsigned * pSim, int nWords, int nTableSize )
 void Hcd_ManClassesRehash( Hcd_Man_t * p, Vec_Int_t * vRefined )
 {
     int * pTable, nTableSize, Key, i, k;
-    nTableSize = Gia_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 );
+    nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 );
     pTable = ABC_CALLOC( int, nTableSize );
     Vec_IntForEachEntry( vRefined, i, k )
     {
@@ -538,7 +538,7 @@ Gia_Man_t * Gia_GenerateReducedLevel( Gia_Man_t * p, int Level, Vec_Ptr_t ** pvR
     vRoots = Vec_PtrAlloc( 100 );
     // copy unmarked nodes
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi(pNew);
@@ -553,7 +553,7 @@ Gia_Man_t * Gia_GenerateReducedLevel( Gia_Man_t * p, int Level, Vec_Ptr_t ** pvR
         {
 //            printf( "Substituting %d <--- %d\n", Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj) ); 
             assert( pRepr < pObj );
-            pObj->Value  = Gia_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
+            pObj->Value  = Abc_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
             continue;
         }
         pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
@@ -644,19 +644,19 @@ int Gia_GiarfStorePatternTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, in
     int i;
     for ( i = 0; i < nLits; i++ )
     {
-        pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
-        pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
-        if ( Gia_InfoHasBit( pPres, iBit ) && 
-             Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
+        pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
+        pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
+        if ( Abc_InfoHasBit( pPres, iBit ) && 
+             Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
              return 0;
     }
     for ( i = 0; i < nLits; i++ )
     {
-        pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
-        pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
-        Gia_InfoSetBit( pPres, iBit );
-        if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
-            Gia_InfoXorBit( pInfo, iBit );
+        pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
+        pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
+        Abc_InfoSetBit( pPres, iBit );
+        if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
+            Abc_InfoXorBit( pInfo, iBit );
     }
     return 1;
 }
@@ -699,10 +699,10 @@ void Gia_GiarfInsertPattern( Hcd_Man_t * p, Vec_Int_t * vCex, int k )
     int Lit, i;
     Vec_IntForEachEntry( vCex, Lit, i )
     {
-        pObj = Gia_ManCi( p->pGia, Gia_Lit2Var(Lit) );
+        pObj = Gia_ManCi( p->pGia, Abc_Lit2Var(Lit) );
         pInfo = Hcd_ObjSimP( p, Gia_ObjId( p->pGia, pObj ) );
-        if ( Gia_InfoHasBit( pInfo, k ) == Gia_LitIsCompl(Lit) )
-            Gia_InfoXorBit( pInfo, k );
+        if ( Abc_InfoHasBit( pInfo, k ) == Abc_LitIsCompl(Lit) )
+            Abc_InfoXorBit( pInfo, k );
     }
 }
 
@@ -737,7 +737,7 @@ void Gia_GiarfPrintClasses( Gia_Man_t * pGia )
 
 ABC_NAMESPACE_IMPL_END
 
-#include "cecInt.h"
+#include "src/proof/cec/cecInt.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -785,7 +785,7 @@ int Gia_ComputeEquivalencesLevel( Hcd_Man_t * p, Gia_Man_t * pGiaLev, Vec_Ptr_t
         iRoot = Gia_ObjId( p->pGia, pRoot );
         if ( !Gia_ObjIsConst( p->pGia, iRoot ) )
             continue;
-        iRootNew = Gia_LitNotCond( pRoot->Value, pRoot->fPhase );
+        iRootNew = Abc_LitNotCond( pRoot->Value, pRoot->fPhase );
         assert( iRootNew != 1 );
         if ( fUse2Solver )
         {
@@ -880,8 +880,8 @@ int Gia_ComputeEquivalencesLevel( Hcd_Man_t * p, Gia_Man_t * pGiaLev, Vec_Ptr_t
             pMemberPrev = (Gia_Obj_t *)Vec_PtrEntryLast( vMembers );
             Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k )
             {
-                iMemberPrev = Gia_LitNotCond( pMemberPrev->Value,  pMemberPrev->fPhase ); 
-                iMember     = Gia_LitNotCond( pMember->Value,     !pMember->fPhase ); 
+                iMemberPrev = Abc_LitNotCond( pMemberPrev->Value,  pMemberPrev->fPhase ); 
+                iMember     = Abc_LitNotCond( pMember->Value,     !pMember->fPhase ); 
                 assert( iMemberPrev != iMember );
                 if ( fUse2Solver )
                 {
diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c
index a6e5315a..35d076e5 100644
--- a/src/aig/gia/giaGlitch.c
+++ b/src/aig/gia/giaGlitch.c
@@ -333,7 +333,7 @@ static inline int Gli_NodeComputeValue( Gli_Obj_t * pNode )
     int i, Phase = 0;
     for ( i = 0; i < (int)pNode->nFanins; i++ )
         Phase |= (Gli_ObjFanin(pNode, i)->fPhase << i);
-    return Gia_InfoHasBit( pNode->uTruth, Phase );
+    return Abc_InfoHasBit( pNode->uTruth, Phase );
 }
 
 /**Function*************************************************************
@@ -352,7 +352,7 @@ static inline int Gli_NodeComputeValue2( Gli_Obj_t * pNode )
     int i, Phase = 0;
     for ( i = 0; i < (int)pNode->nFanins; i++ )
         Phase |= (Gli_ObjFanin(pNode, i)->fPhase2 << i);
-    return Gia_InfoHasBit( pNode->uTruth, Phase );
+    return Abc_InfoHasBit( pNode->uTruth, Phase );
 }
 
 /**Function*************************************************************
@@ -593,7 +593,7 @@ unsigned Gli_ManSimulateSeqNode( Gli_Man_t * p, Gli_Obj_t * pNode )
         for ( k = 0; k < nFanins; k++ )
             if ( (pSimInfos[k] >> i) & 1 )
                 Phase |= (1 << k);
-        if ( Gia_InfoHasBit( pNode->uTruth, Phase ) )
+        if ( Abc_InfoHasBit( pNode->uTruth, Phase ) )
             Result |= (1 << i);
     }
     return Result;
@@ -755,7 +755,7 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb
     }
     else 
     {
-        int nIters = Gia_BitWordNum(nPatterns);
+        int nIters = Abc_BitWordNum(nPatterns);
         Gli_ManSimulateSeqPref( p, 16 );
         for ( i = 0; i < 32; i++ )
         {
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index f346a310..41092cc7 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -46,10 +46,10 @@ static inline int Gia_ManHashOne( int iLit0, int iLit1, int TableSize )
 {
     unsigned Key = 0;
     assert( iLit0 < iLit1 );
-    Key ^= Gia_Lit2Var(iLit0) * 7937;
-    Key ^= Gia_Lit2Var(iLit1) * 2971;
-    Key ^= Gia_LitIsCompl(iLit0) * 911;
-    Key ^= Gia_LitIsCompl(iLit1) * 353;
+    Key ^= Abc_Lit2Var(iLit0) * 7937;
+    Key ^= Abc_Lit2Var(iLit1) * 2971;
+    Key ^= Abc_LitIsCompl(iLit0) * 911;
+    Key ^= Abc_LitIsCompl(iLit1) * 353;
     return (int)(Key % TableSize);
 }
 
@@ -68,8 +68,8 @@ static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1 )
 {
     Gia_Obj_t * pThis;
     int * pPlace = p->pHTable + Gia_ManHashOne( iLit0, iLit1, p->nHTable );
-    for ( pThis = (*pPlace)? Gia_ManObj(p, Gia_Lit2Var(*pPlace)) : NULL; pThis; 
-          pPlace = (int *)&pThis->Value, pThis = (*pPlace)? Gia_ManObj(p, Gia_Lit2Var(*pPlace)) : NULL )
+    for ( pThis = (*pPlace)? Gia_ManObj(p, Abc_Lit2Var(*pPlace)) : NULL; pThis; 
+          pPlace = (int *)&pThis->Value, pThis = (*pPlace)? Gia_ManObj(p, Abc_Lit2Var(*pPlace)) : NULL )
               if ( Gia_ObjFaninLit0p(p, pThis) == iLit0 && Gia_ObjFaninLit1p(p, pThis) == iLit1 )
                   break;
     return pPlace;
@@ -109,7 +109,7 @@ int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 )
 void Gia_ManHashAlloc( Gia_Man_t * p )  
 {
     assert( p->pHTable == NULL );
-    p->nHTable = Gia_PrimeCudd( p->nObjsAlloc );
+    p->nHTable = Abc_PrimeCudd( p->nObjsAlloc );
     p->pHTable = ABC_CALLOC( int, p->nHTable );
 }
 
@@ -134,7 +134,7 @@ void Gia_ManHashStart( Gia_Man_t * p )
     {
         pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i) );
         assert( *pPlace == 0 );
-        *pPlace = Gia_Var2Lit( i, 0 );
+        *pPlace = Abc_Var2Lit( i, 0 );
     }
 }
 
@@ -175,20 +175,20 @@ void Gia_ManHashResize( Gia_Man_t * p )
     // replace the table
     pHTableOld = p->pHTable;
     nHTableOld = p->nHTable;
-    p->nHTable = Gia_PrimeCudd( 2 * Gia_ManAndNum(p) ); 
+    p->nHTable = Abc_PrimeCudd( 2 * Gia_ManAndNum(p) ); 
     p->pHTable = ABC_CALLOC( int, p->nHTable );
     // rehash the entries from the old table
     Counter = 0;
     for ( i = 0; i < nHTableOld; i++ )
-    for ( pThis = (pHTableOld[i]? Gia_ManObj(p, Gia_Lit2Var(pHTableOld[i])) : NULL),
+    for ( pThis = (pHTableOld[i]? Gia_ManObj(p, Abc_Lit2Var(pHTableOld[i])) : NULL),
           iNext = (pThis? pThis->Value : 0);  
-          pThis;  pThis = (iNext? Gia_ManObj(p, Gia_Lit2Var(iNext)) : NULL),   
+          pThis;  pThis = (iNext? Gia_ManObj(p, Abc_Lit2Var(iNext)) : NULL),   
           iNext = (pThis? pThis->Value : 0)  )
     {
         pThis->Value = 0;
         pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0p(p, pThis), Gia_ObjFaninLit1p(p, pThis) );
         assert( *pPlace == 0 ); // should not be there
-        *pPlace = Gia_Var2Lit( Gia_ObjId(p, pThis), 0 );
+        *pPlace = Abc_Var2Lit( Gia_ObjId(p, pThis), 0 );
         assert( *pPlace != 0 );
         Counter++;
     }
@@ -220,9 +220,9 @@ void Gia_ManHashProfile( Gia_Man_t * p )
     for ( i = 0; i < Limit; i++ )
     {
         Counter = 0;
-        for ( pEntry = (p->pHTable[i]? Gia_ManObj(p, Gia_Lit2Var(p->pHTable[i])) : NULL); 
+        for ( pEntry = (p->pHTable[i]? Gia_ManObj(p, Abc_Lit2Var(p->pHTable[i])) : NULL); 
               pEntry; 
-              pEntry = (pEntry->Value? Gia_ManObj(p, Gia_Lit2Var(pEntry->Value)) : NULL) )
+              pEntry = (pEntry->Value? Gia_ManObj(p, Abc_Lit2Var(pEntry->Value)) : NULL) )
             Counter++;
         if ( Counter ) 
             printf( "%d ", Counter );
@@ -480,7 +480,7 @@ int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )
         return iLit1 ? iLit0 : 0;
     if ( iLit0 == iLit1 )
         return iLit1;
-    if ( iLit0 == Gia_LitNot(iLit1) )
+    if ( iLit0 == Abc_LitNot(iLit1) )
         return 0;
     if ( (p->nObjs & 0xFF) == 0 && 2 * p->nHTable < Gia_ManAndNum(p) )
         Gia_ManHashResize( p );
@@ -531,7 +531,7 @@ int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 )
         return iLit1 ? iLit0 : 0;
     if ( iLit0 == iLit1 )
         return iLit1;
-    if ( iLit0 == Gia_LitNot(iLit1) )
+    if ( iLit0 == Abc_LitNot(iLit1) )
         return 0;
     if ( iLit0 > iLit1 )
         iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
@@ -556,10 +556,10 @@ int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 )
 ***********************************************************************/
 int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )  
 { 
-    int fCompl = Gia_LitIsCompl(iLit0) ^ Gia_LitIsCompl(iLit1);
-    int iTemp0 = Gia_ManHashAnd( p, Gia_LitRegular(iLit0), Gia_LitNot(Gia_LitRegular(iLit1)) );
-    int iTemp1 = Gia_ManHashAnd( p, Gia_LitRegular(iLit1), Gia_LitNot(Gia_LitRegular(iLit0)) );
-    return Gia_LitNotCond( Gia_ManHashAnd( p, Gia_LitNot(iTemp0), Gia_LitNot(iTemp1) ), !fCompl );
+    int fCompl = Abc_LitIsCompl(iLit0) ^ Abc_LitIsCompl(iLit1);
+    int iTemp0 = Gia_ManHashAnd( p, Abc_LitRegular(iLit0), Abc_LitNot(Abc_LitRegular(iLit1)) );
+    int iTemp1 = Gia_ManHashAnd( p, Abc_LitRegular(iLit1), Abc_LitNot(Abc_LitRegular(iLit0)) );
+    return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
 }
 
 /**Function*************************************************************
@@ -575,9 +575,9 @@ int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )
 ***********************************************************************/
 int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )  
 { 
-    int iTemp0 = Gia_ManHashAnd( p, Gia_LitNot(iCtrl), iData0 );
+    int iTemp0 = Gia_ManHashAnd( p, Abc_LitNot(iCtrl), iData0 );
     int iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 );
-    return Gia_LitNotCond( Gia_ManHashAnd( p, Gia_LitNot(iTemp0), Gia_LitNot(iTemp1) ), 1 );
+    return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), 1 );
 }
 
 /**Function*************************************************************
@@ -597,7 +597,7 @@ Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash )
     Gia_Obj_t * pObj;
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->fAddStrash = fAddStrash;
     Gia_ManHashAlloc( pNew );
     Gia_ManConst0(p)->Value = 0;
diff --git a/src/aig/gia/giaHcd.c b/src/aig/gia/giaHcd.c
index 454785b9..3f37e724 100644
--- a/src/aig/gia/giaHcd.c
+++ b/src/aig/gia/giaHcd.c
@@ -20,8 +20,8 @@
 
 #include "gia.h"
 #include "giaAig.h"
-#include "aig.h"
-#include "dar.h"
+#include "src/aig/aig/aig.h"
+#include "src/opt/dar/dar.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -332,7 +332,7 @@ Gia_Man_t * Hcd_ManChoiceMiter( Vec_Ptr_t * vGias )
     }
     // start the new manager
     pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
-    pNew->pName = Gia_UtilStrsav( pGia0->pName );
+    pNew->pName = Abc_UtilStrsav( pGia0->pName );
     // create new CIs and assign them to the old manager CIs
     for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
     {
@@ -457,7 +457,7 @@ void Hcd_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
     {
         if ( Gia_ObjIsConst0(pRepr) )
         {
-            pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+            pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
             return;
         }
         Hcd_ManEquivToChoices_rec( pNew, p, pRepr );
@@ -465,20 +465,20 @@ void Hcd_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
         Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
         Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
         pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-        if ( Gia_LitRegular(pObj->Value) == Gia_LitRegular(pRepr->Value) )
+        if ( Abc_LitRegular(pObj->Value) == Abc_LitRegular(pRepr->Value) )
         {
-            assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
+            assert( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
             return;
         }
         if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit
             return;
         assert( pRepr->Value < pObj->Value );
-        pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) );
-        pObjNew  = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
+        pReprNew = Gia_ManObj( pNew, Abc_Lit2Var(pRepr->Value) );
+        pObjNew  = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) );
         if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) )
         {
             assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew );
-            pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+            pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
             return;
         }
         if ( !Hcd_ObjCheckTfi( pNew, pReprNew, pObjNew ) )
@@ -487,7 +487,7 @@ void Hcd_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
             Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
             Hcd_ManAddNextEntry_rec( pNew, pReprNew, pObjNew ); 
         }
-        pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+        pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
         return;
     }
     assert( Gia_ObjIsAnd(pObj) );
@@ -563,7 +563,7 @@ Gia_Man_t * Hcd_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
     assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
     Gia_ManSetPhase( p );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
     pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
     for ( i = 0; i < Gia_ManObjNum(p); i++ )
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 787aa090..e03439d0 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -19,9 +19,9 @@
 ***********************************************************************/
 
 #include "gia.h"
-#include "aig.h"
-#include "if.h"
-#include "dar.h"
+#include "src/aig/aig/aig.h"
+#include "src/map/if/if.h"
+#include "src/opt/dar/dar.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -306,11 +306,11 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p )
     {
         nLuts++;
         nFanins += Gia_ObjLutSize(p, i);
-        nLutSize = ABC_MAX( nLutSize, Gia_ObjLutSize(p, i) );
+        nLutSize = Abc_MaxInt( nLutSize, Gia_ObjLutSize(p, i) );
         Gia_LutForEachFanin( p, i, iFan, k )
-            pLevels[i] = ABC_MAX( pLevels[i], pLevels[iFan] );
+            pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[iFan] );
         pLevels[i]++;
-        LevelMax = ABC_MAX( LevelMax, pLevels[i] );
+        LevelMax = Abc_MaxInt( LevelMax, pLevels[i] );
     }
     ABC_FREE( pLevels );
     Abc_Print( 1, "mapping (K=%d)  :  ", nLutSize );
@@ -355,7 +355,7 @@ int Gia_ManLutSizeMax( Gia_Man_t * p )
 {
     int i, nSizeMax = -1;
     Gia_ManForEachLut( p, i )
-        nSizeMax = ABC_MAX( nSizeMax, Gia_ObjLutSize(p, i) );
+        nSizeMax = Abc_MaxInt( nSizeMax, Gia_ObjLutSize(p, i) );
     return nSizeMax;
 }
 
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 39b0059d..972958bb 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "gia.h"
-#include "tim.h"
+#include "src/misc/tim/tim.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -262,7 +262,8 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p )
     Vec_Int_t * vAbs = p->vObjClasses;
     int i, k, Entry, iStart, iStop, nFrames;
     int nObjBits, nObjMask, iObj, iFrame, nWords;
-    unsigned * pInfo, * pCountAll, * pCountUni;
+    unsigned * pInfo;
+    int * pCountAll, * pCountUni;
     if ( vAbs == NULL )
         return;
     nFrames = Vec_IntEntry( vAbs, 0 );
@@ -270,10 +271,10 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p )
     pCountAll = ABC_ALLOC( int, nFrames + 1 );
     pCountUni = ABC_ALLOC( int, nFrames + 1 );
     // start storage for seen objects
-    nWords = Gia_BitWordNum( nFrames );
+    nWords = Abc_BitWordNum( nFrames );
     vSeens = Vec_IntStart( Gia_ManObjNum(p) * nWords );
     // get the bitmasks
-    nObjBits = Gia_Base2Log( Gia_ManObjNum(p) );
+    nObjBits = Abc_Base2Log( Gia_ManObjNum(p) );
     nObjMask = (1 << nObjBits) - 1;
     assert( Gia_ManObjNum(p) <= nObjMask );
     // print info about frames
@@ -289,16 +290,16 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p )
             iObj   = (Entry &  nObjMask);
             iFrame = (Entry >> nObjBits);
             pInfo  = (unsigned *)Vec_IntEntryP( vSeens, nWords * iObj );
-            if ( Gia_InfoHasBit(pInfo, iFrame) == 0 )
+            if ( Abc_InfoHasBit(pInfo, iFrame) == 0 )
             {
-                Gia_InfoSetBit( pInfo, iFrame );
+                Abc_InfoSetBit( pInfo, iFrame );
                 pCountUni[iFrame+1]++;
                 pCountUni[0]++;
             }
             pCountAll[iFrame+1]++;
             pCountAll[0]++;
         }
-        assert( pCountAll[0] == (unsigned)(iStop - iStart) );
+        assert( pCountAll[0] == (iStop - iStart) );
 //        printf( "%5d%5d  ", pCountAll[0], pCountUni[0] ); 
         printf( "%3d :", i );
         printf( "%6d", pCountAll[0] ); 
diff --git a/src/aig/gia/giaPat.c b/src/aig/gia/giaPat.c
index 643ae6b7..124f5e0b 100644
--- a/src/aig/gia/giaPat.c
+++ b/src/aig/gia/giaPat.c
@@ -100,8 +100,8 @@ void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, V
     Gia_SatCollectCone( p, Gia_ObjFanin0(pRoot), vVisit );
     // set binary values to nodes in the counter-example
     Vec_IntForEachEntry( vCex, Entry, i )
-//        Sat_ObjSetXValue( Gia_ManObj(p, Gia_Lit2Var(Entry)), Gia_LitIsCompl(Entry)? GIA_ZER : GIA_ONE );
-        Sat_ObjSetXValue( Gia_ManCi(p, Gia_Lit2Var(Entry)), Gia_LitIsCompl(Entry)? GIA_ZER : GIA_ONE );
+//        Sat_ObjSetXValue( Gia_ManObj(p, Abc_Lit2Var(Entry)), Abc_LitIsCompl(Entry)? GIA_ZER : GIA_ONE );
+        Sat_ObjSetXValue( Gia_ManCi(p, Abc_Lit2Var(Entry)), Abc_LitIsCompl(Entry)? GIA_ZER : GIA_ONE );
     // simulate
     Gia_ManForEachObjVec( vVisit, p, pObj, i )
     {
diff --git a/src/aig/gia/giaReparam.c b/src/aig/gia/giaReparam.c
index 5210f998..10294671 100644
--- a/src/aig/gia/giaReparam.c
+++ b/src/aig/gia/giaReparam.c
@@ -20,7 +20,7 @@
 
 #include "gia.h"
 #include "giaAig.h"
-#include "saig.h"
+#include "src/aig/saig/saig.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -52,7 +52,7 @@ Gia_Man_t * Gia_ManDupIn2Ff( Gia_Man_t * p )
     int i;
     vPiOuts = Vec_IntAlloc( Gia_ManPiNum(p) );
     pNew = Gia_ManStart( Gia_ManObjNum(p) + 2 * Gia_ManPiNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachPi( p, pObj, i )
@@ -112,7 +112,7 @@ Gia_Man_t * Gia_ManDupFf2In( Gia_Man_t * p, int nFlopsOld )
     Gia_Obj_t * pObj;
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachRo( p, pObj, i )
diff --git a/src/aig/gia/giaRetime.c b/src/aig/gia/giaRetime.c
index 58029b66..0b9a6bfb 100644
--- a/src/aig/gia/giaRetime.c
+++ b/src/aig/gia/giaRetime.c
@@ -125,7 +125,7 @@ Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut )
     int i;
     // create the new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     // create the true PIs
     Gia_ManFillValue( p );
@@ -135,7 +135,7 @@ Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut )
         pObj->Value = Gia_ManAppendCi( pNew );
     // create the registers
     Vec_PtrForEachEntry( Gia_Obj_t *, vCut, pObj, i )
-        pObj->Value = Gia_LitNotCond( Gia_ManAppendCi(pNew), pObj->fPhase );
+        pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), pObj->fPhase );
     // duplicate logic above the cut
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManRetimeDup_rec( pNew, Gia_ObjFanin0(pObj) );
@@ -156,7 +156,7 @@ Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut )
     Vec_PtrForEachEntry( Gia_Obj_t *, vCut, pObj, i )
     {
         Gia_ManRetimeDup_rec( pNew, pObj );
-        Gia_ManAppendCo( pNew, Gia_LitNotCond( pObj->Value, pObj->fPhase ) );
+        Gia_ManAppendCo( pNew, Abc_LitNotCond( pObj->Value, pObj->fPhase ) );
     }
     Gia_ManHashStop( pNew );
     Gia_ManSetRegNum( pNew, Vec_PtrSize(vCut) );
diff --git a/src/aig/gia/giaSat.c b/src/aig/gia/giaSat.c
index c2d70795..cb410dd7 100644
--- a/src/aig/gia/giaSat.c
+++ b/src/aig/gia/giaSat.c
@@ -265,7 +265,7 @@ int Gia_ManSatPartCount( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnLeaves, int *
         (*pnLeaves)++;
     else
         Level1 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC1(pObj);
-    return ABC_MAX( Level0, Level1 );
+    return Abc_MaxInt( Level0, Level1 );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/gia/giaScl.c b/src/aig/gia/giaScl.c
index a482d024..0ec67c93 100644
--- a/src/aig/gia/giaScl.c
+++ b/src/aig/gia/giaScl.c
@@ -199,7 +199,7 @@ Gia_Man_t * Gia_ManReduceEquiv( Gia_Man_t * p, int fVerbose )
         else if ( ~pMaps[iLit] ) // in this case, ID(pObj) > ID(pRepr) 
             pCi2Lit[Gia_ManPiNum(p)+i] = pMaps[iLit], Counter++; 
         else
-            pMaps[iLit] = Gia_Var2Lit( Gia_ObjId(p, pObjRo), 0 );
+            pMaps[iLit] = Abc_Var2Lit( Gia_ObjId(p, pObjRo), 0 );
     }
 /*
     Gia_ManForEachCi( p, pObjRo, i )
diff --git a/src/aig/gia/giaShrink.c b/src/aig/gia/giaShrink.c
index fc9e80d6..07119daf 100644
--- a/src/aig/gia/giaShrink.c
+++ b/src/aig/gia/giaShrink.c
@@ -19,8 +19,8 @@
 ***********************************************************************/
 
 #include "gia.h"
-#include "aig.h"
-#include "dar.h"
+#include "src/aig/aig/aig.h"
+#include "src/opt/dar/dar.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -75,7 +75,7 @@ Gia_Man_t * Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose
     Gia_ManConst0(p)->Value = 0;
     // start the new manager
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pName = Abc_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManCleanLevels( pNew, Gia_ManObjNum(p) );
     Gia_ManForEachObj1( p, pObj, i )
@@ -114,7 +114,7 @@ Gia_Man_t * Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose
             else
             {
                 pObj->Value = Dar_LibEvalBuild( pNew, vLeaves, 0xffff & *pTruth, fKeepLevel, vLeavesBest );
-                pObj->Value = Gia_LitNotCond( pObj->Value, Gia_ObjPhaseRealLit(pNew, pObj->Value) ^ pObj->fPhase );
+                pObj->Value = Abc_LitNotCond( pObj->Value, Gia_ObjPhaseRealLit(pNew, pObj->Value) ^ pObj->fPhase );
             }
         }
     }
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 4be740cd..817fc2e2 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -133,18 +133,18 @@ Vec_Int_t * Gia_ManSimDeriveResets( Gia_Man_t * pGia )
     {
         if ( Count < nImpLimit )
             continue;
-        pObj = Gia_ManObj( pGia, Gia_Lit2Var(Lit) );
-        if ( Gia_LitIsCompl(Lit) ) // const 0
+        pObj = Gia_ManObj( pGia, Abc_Lit2Var(Lit) );
+        if ( Abc_LitIsCompl(Lit) ) // const 0
         {
 //            Ssm_ObjSetLogic0( pObj );
-            Vec_IntWriteEntry( vResult, Gia_Lit2Var(Lit), 0 );
+            Vec_IntWriteEntry( vResult, Abc_Lit2Var(Lit), 0 );
             CounterPi0 += Gia_ObjIsPi(pGia, pObj);
             Counter0++;
         }
         else
         {
 //            Ssm_ObjSetLogic1( pObj );
-            Vec_IntWriteEntry( vResult, Gia_Lit2Var(Lit), 1 );
+            Vec_IntWriteEntry( vResult, Abc_Lit2Var(Lit), 1 );
             CounterPi1 += Gia_ObjIsPi(pGia, pObj);
             Counter1++;
         }
@@ -568,8 +568,8 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
             continue;
         for ( w = nWords-1; w >= 0; w-- )
             pData[w] = Gia_ManRandom( 0 );
-        if ( Gia_InfoHasBit( pData, iPat ) )
-            Gia_InfoSetBit( p->pData, Counter + iPioId );
+        if ( Abc_InfoHasBit( pData, iPat ) )
+            Abc_InfoSetBit( p->pData, Counter + iPioId );
     }
     ABC_FREE( pData );
     return p;
diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c
index 27945704..74a34d1b 100644
--- a/src/aig/gia/giaSim2.c
+++ b/src/aig/gia/giaSim2.c
@@ -471,7 +471,7 @@ void Gia_Sim2ProcessRefined( Gia_Sim2_t * p, Vec_Int_t * vRefined )
     int * pTable, nTableSize, i, k, Key;
     if ( Vec_IntSize(vRefined) == 0 )
         return;
-    nTableSize = Gia_PrimeCudd( 1000 + Vec_IntSize(vRefined) / 3 );
+    nTableSize = Abc_PrimeCudd( 1000 + Vec_IntSize(vRefined) / 3 );
     pTable = ABC_CALLOC( int, nTableSize );
     Vec_IntForEachEntry( vRefined, i, k )
     {
@@ -617,8 +617,8 @@ Abc_Cex_t * Gia_Sim2GenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
     {
         for ( w = nWords-1; w >= 0; w-- )
             pData[w] = Gia_ManRandom( 0 );
-        if ( Gia_InfoHasBit( pData, iPat ) )
-            Gia_InfoSetBit( p->pData, Counter + i );
+        if ( Abc_InfoHasBit( pData, iPat ) )
+            Abc_InfoSetBit( p->pData, Counter + i );
     }
     ABC_FREE( pData );
     return p;
diff --git a/src/aig/gia/giaSpeedup.c b/src/aig/gia/giaSpeedup.c
index cce0b68d..d20fe1a4 100644
--- a/src/aig/gia/giaSpeedup.c
+++ b/src/aig/gia/giaSpeedup.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "gia.h"
-#include "if.h"
+#include "src/map/if/if.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -597,7 +597,7 @@ void Gia_ManSpeedupObj( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_I
     for ( i = 0; i < nCofs; i++ )
     {
         Gia_ManForEachObjVec( vLeaves, p, pTemp, k )
-            pTemp->Value = Gia_Var2Lit( Gia_ObjId(p, pTemp), 0 );
+            pTemp->Value = Abc_Var2Lit( Gia_ObjId(p, pTemp), 0 );
         Gia_ManForEachObjVec( vTimes, p, pTemp, k )
             pTemp->Value = ((i & (1<<k)) != 0);
         Gia_ManForEachObjVec( vNodes, p, pTemp, k )
@@ -611,7 +611,7 @@ void Gia_ManSpeedupObj( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_I
             pCofs[i] = Gia_ManHashMux( pNew, Gia_ObjToLit(p,pTemp), pCofs[i+nSkip], pCofs[i] );
     // create choice node  (pObj is repr and ppCofs[0] is new)
     iObj    = Gia_ObjId( p, pObj );
-    iResult = Gia_Lit2Var( pCofs[0] );
+    iResult = Abc_Lit2Var( pCofs[0] );
     if ( iResult <= iObj )
         return;
     Gia_ObjSetRepr( pNew, iResult, iObj );
diff --git a/src/aig/gia/giaSupMin.c b/src/aig/gia/giaSupMin.c
index 4abaab0f..90c30c71 100644
--- a/src/aig/gia/giaSupMin.c
+++ b/src/aig/gia/giaSupMin.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "gia.h"
-#include "kit.h"
+#include "src/bool/kit/kit.h"
 
 ABC_NAMESPACE_IMPL_START
 
diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c
index bc2f0f67..848bd646 100644
--- a/src/aig/gia/giaSwitch.c
+++ b/src/aig/gia/giaSwitch.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "giaAig.h"
-#include "main.h"
+#include "src/base/main/main.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -569,7 +569,7 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars )
     {
         printf( "Obj = %8d (%8d). F = %6d. ", 
             pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront, 
-            4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
+            4.0*Abc_BitWordNum(2 * p->pAig->nFront)/(1<<20) );
         printf( "AIG = %7.2f Mb. F-mem = %7.2f Mb. Other = %7.2f Mb.  ", 
             12.0*Gia_ManObjNum(p->pAig)/(1<<20), 
             4.0*p->nWords*p->pAig->nFront/(1<<20), 
@@ -691,8 +691,8 @@ Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * pAig, int nFrames, int nPref
     Aig_ManForEachObj( pAig, pObj, i )
     {
 //        if ( Aig_ObjIsPo(pObj) )
-//            printf( "%d=%f\n", i, Aig_Int2Float( Vec_IntEntry(vSwitching, Gia_Lit2Var(pObj->iData)) ) );
-        Vec_IntWriteEntry( vResult, i, Vec_IntEntry(vSwitching, Gia_Lit2Var(pObj->iData)) );
+//            printf( "%d=%f\n", i, Abc_Int2Float( Vec_IntEntry(vSwitching, Abc_Lit2Var(pObj->iData)) ) );
+        Vec_IntWriteEntry( vResult, i, Vec_IntEntry(vSwitching, Abc_Lit2Var(pObj->iData)) );
     }
     // delete intermediate results
     Vec_IntFree( vSwitching );
diff --git a/src/aig/gia/giaTsim.c b/src/aig/gia/giaTsim.c
index e829ff5b..c4fb7f26 100644
--- a/src/aig/gia/giaTsim.c
+++ b/src/aig/gia/giaTsim.c
@@ -84,15 +84,15 @@ Gia_ManTer_t * Gia_ManTerCreate( Gia_Man_t * pAig )
     p = ABC_CALLOC( Gia_ManTer_t, 1 );
     p->pAig   = Gia_ManFront( pAig );
     p->nIters = 300;
-    p->pDataSim    = ABC_ALLOC( unsigned, Gia_BitWordNum(2*p->pAig->nFront) );
-    p->pDataSimCis = ABC_ALLOC( unsigned, Gia_BitWordNum(2*Gia_ManCiNum(p->pAig)) );
-    p->pDataSimCos = ABC_ALLOC( unsigned, Gia_BitWordNum(2*Gia_ManCoNum(p->pAig)) );
+    p->pDataSim    = ABC_ALLOC( unsigned, Abc_BitWordNum(2*p->pAig->nFront) );
+    p->pDataSimCis = ABC_ALLOC( unsigned, Abc_BitWordNum(2*Gia_ManCiNum(p->pAig)) );
+    p->pDataSimCos = ABC_ALLOC( unsigned, Abc_BitWordNum(2*Gia_ManCoNum(p->pAig)) );
     // allocate storage for terminary states
-    p->nStateWords = Gia_BitWordNum( 2*Gia_ManRegNum(pAig) );
+    p->nStateWords = Abc_BitWordNum( 2*Gia_ManRegNum(pAig) );
     p->vStates  = Vec_PtrAlloc( 1000 );
     p->pCount0  = ABC_CALLOC( int, Gia_ManRegNum(pAig) );
     p->pCountX  = ABC_CALLOC( int, Gia_ManRegNum(pAig) );
-    p->nBins    = Gia_PrimeCudd( 500 );
+    p->nBins    = Abc_PrimeCudd( 500 );
     p->pBins    = ABC_CALLOC( unsigned *, p->nBins );
     p->vRetired = Vec_IntAlloc( 100 );
     p->pRetired = ABC_CALLOC( char, Gia_ManRegNum(pAig) );
@@ -511,7 +511,7 @@ void Gia_ManTerAnalyze2( Vec_Ptr_t * vStates, int nRegs )
     unsigned * pTemp, * pStates = (unsigned *)Vec_PtrPop( vStates );
     int i, w, nZeros, nConsts, nStateWords;
     // detect constant zero registers
-    nStateWords = Gia_BitWordNum( 2*nRegs );
+    nStateWords = Abc_BitWordNum( 2*nRegs );
     memset( pStates, 0, sizeof(int) * nStateWords );
     Vec_PtrForEachEntry( unsigned *, vStates, pTemp, i )
         for ( w = 0; w < nStateWords; w++ )
@@ -579,7 +579,7 @@ Vec_Ptr_t * Gia_ManTerTranspose( Gia_ManTer_t * p )
     unsigned * pState, * pFlop;
     int i, k, nFlopWords;
     vFlops = Vec_PtrAlloc( 100 );
-    nFlopWords = Gia_BitWordNum( 2*Vec_PtrSize(p->vStates) );
+    nFlopWords = Abc_BitWordNum( 2*Vec_PtrSize(p->vStates) );
     for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
     {
         if ( p->pCount0[i] == Vec_PtrSize(p->vStates) ) 
@@ -634,7 +634,7 @@ int * Gia_ManTerCreateMap( Gia_ManTer_t * p, int fVerbose )
     Gia_Obj_t * pObj;
     Vec_Int_t * vMapKtoI;
     int i, iRepr, nFlopWords, Counter0 = 0, CounterE = 0;
-    nFlopWords = Gia_BitWordNum( 2*Vec_PtrSize(p->vStates) );
+    nFlopWords = Abc_BitWordNum( 2*Vec_PtrSize(p->vStates) );
     p->vFlops = Gia_ManTerTranspose( p );
     pCi2Lit = ABC_FALLOC( int, Gia_ManCiNum(p->pAig) );
     vMapKtoI = Vec_IntAlloc( 100 );
@@ -648,7 +648,7 @@ int * Gia_ManTerCreateMap( Gia_ManTer_t * p, int fVerbose )
             if ( iRepr < 0 )
                 continue;
             pObj = Gia_ManCi( p->pAig, Gia_ManPiNum(p->pAig)+Vec_IntEntry(vMapKtoI, iRepr) );
-            pCi2Lit[Gia_ManPiNum(p->pAig)+i] = Gia_Var2Lit( Gia_ObjId( p->pAig, pObj ), 0 );
+            pCi2Lit[Gia_ManPiNum(p->pAig)+i] = Abc_Var2Lit( Gia_ObjId( p->pAig, pObj ), 0 );
             CounterE++;
         }
     Vec_IntFree( vMapKtoI );
@@ -684,8 +684,8 @@ Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose )
             pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront );
         printf( "AIG = %7.2f Mb. F-mem = %7.2f Mb. Other = %7.2f Mb.  ", 
             12.0*Gia_ManObjNum(p->pAig)/(1<<20), 
-            4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20), 
-            4.0*Gia_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) );
+            4.0*Abc_BitWordNum(2 * p->pAig->nFront)/(1<<20), 
+            4.0*Abc_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) );
         ABC_PRT( "Time", clock() - clk );
     }
     // perform simulation
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index f19f0602..e56f6ea9 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -80,42 +80,6 @@ void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int
             pInfo[w] = Gia_ManRandom(0);
 }
 
-/**Function********************************************************************
-
-  Synopsis    [Returns the next prime >= p.]
-
-  Description [Copied from CUDD, for stand-aloneness.]
-
-  SideEffects [None]
-
-  SeeAlso     []
-
-******************************************************************************/
-unsigned int Gia_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*************************************************************
 
@@ -483,7 +447,7 @@ int Gia_ManLevelNum( Gia_Man_t * p )
         else if ( Gia_ObjIsCo(pObj) )
         {
             Gia_ObjSetCoLevel( p, pObj );
-            p->nLevels = ABC_MAX( p->nLevels, Gia_ObjLevel(p, pObj) );
+            p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) );
         }
         else
             Gia_ObjSetLevel( p, pObj, 0 );
@@ -1150,11 +1114,11 @@ int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
     int RetValue, i, k, iBit = 0;
     Gia_ManCleanMark0(pAig);
     Gia_ManForEachRo( pAig, pObj, i )
-        pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
+        pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
     for ( i = 0; i <= p->iFrame; i++ )
     {
         Gia_ManForEachPi( pAig, pObj, k )
-            pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
+            pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
         Gia_ManForEachAnd( pAig, pObj, k )
             pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
                            (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
@@ -1194,12 +1158,12 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
     assert( Gia_ManPiNum(pAig) == p->nPis );
     Gia_ManCleanMark0(pAig);
 //    Gia_ManForEachRo( pAig, pObj, i )
-//       pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
+//       pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
     iBit = p->nRegs;
     for ( i = 0; i <= p->iFrame; i++ )
     {
         Gia_ManForEachPi( pAig, pObj, k )
-            pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
+            pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
         Gia_ManForEachAnd( pAig, pObj, k )
             pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
                            (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));