Version abc70712

8 files changed, 205 insertions, 204 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 29195d19..7f2df105 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -36,6 +36,7 @@ extern "C" {
 #include <time.h>
 
 #include "vec.h"
+#include "aig.h"
 #include "dar.h"
 #include "satSolver.h"
 
@@ -73,8 +74,8 @@ struct Fra_Man_t_
     // high-level data    
     Fra_Par_t *      pPars;             // parameters governing fraiging
     // AIG managers
-    Dar_Man_t *      pManAig;           // the starting AIG manager
-    Dar_Man_t *      pManFraig;         // the final AIG manager
+    Aig_Man_t *      pManAig;           // the starting AIG manager
+    Aig_Man_t *      pManFraig;         // the final AIG manager
     // simulation info
     unsigned *       pSimWords;         // memory for simulation information
     int              nSimWords;         // the number of simulation words
@@ -86,8 +87,8 @@ struct Fra_Man_t_
     Vec_Ptr_t *      vClasses;          // equivalence classes
     Vec_Ptr_t *      vClasses1;         // equivalence class of Const1 node
     Vec_Ptr_t *      vClassesTemp;      // temporary storage for new classes
-    Dar_Obj_t **     pMemClasses;       // memory allocated for equivalence classes
-    Dar_Obj_t **     pMemClassesFree;   // memory allocated for equivalence classes to be used
+    Aig_Obj_t **     pMemClasses;       // memory allocated for equivalence classes
+    Aig_Obj_t **     pMemClassesFree;   // memory allocated for equivalence classes to be used
     Vec_Ptr_t *      vClassOld;         // old equivalence class after splitting
     Vec_Ptr_t *      vClassNew;         // new equivalence class(es) after splitting
     int              nPairs;            // the number of pairs of nodes
@@ -98,8 +99,8 @@ struct Fra_Man_t_
     sint64           nBTLimitGlobal;    // resource limit
     sint64           nInsLimitGlobal;   // resource limit
     // various data members
-    Dar_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
-    Dar_Obj_t **     pMemRepr;          // memory allocated for points to the node representatives
+    Aig_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
+    Aig_Obj_t **     pMemRepr;          // memory allocated for points to the node representatives
     Vec_Ptr_t **     pMemFanins;        // the arrays of fanins
     int *            pMemSatNums;       // the array of SAT numbers
     int              nSizeAlloc;        // allocated size of the arrays
@@ -135,21 +136,21 @@ struct Fra_Man_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline unsigned *   Fra_ObjSim( Dar_Obj_t * pObj )   { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id;  }
+static inline unsigned *   Fra_ObjSim( Aig_Obj_t * pObj )   { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id;  }
 static inline unsigned     Fra_ObjRandomSim()               { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
 
-static inline Dar_Obj_t *  Fra_ObjFraig( Dar_Obj_t * pObj )                              { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id];       }
-static inline Dar_Obj_t *  Fra_ObjRepr( Dar_Obj_t * pObj )                               { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id];        }
-static inline Vec_Ptr_t *  Fra_ObjFaninVec( Dar_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];      }
-static inline int          Fra_ObjSatNum( Dar_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];     }
+static inline Aig_Obj_t *  Fra_ObjFraig( Aig_Obj_t * pObj )                              { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id];       }
+static inline Aig_Obj_t *  Fra_ObjRepr( Aig_Obj_t * pObj )                               { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id];        }
+static inline Vec_Ptr_t *  Fra_ObjFaninVec( Aig_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];      }
+static inline int          Fra_ObjSatNum( Aig_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];     }
 
-static inline void         Fra_ObjSetFraig( Dar_Obj_t * pObj, Dar_Obj_t * pNode )        { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]   = pNode;    }
-static inline void         Fra_ObjSetRepr( Dar_Obj_t * pObj, Dar_Obj_t * pNode )         { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]    = pNode;    }
-static inline void         Fra_ObjSetFaninVec( Dar_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]  = vFanins;  }
-static inline void         Fra_ObjSetSatNum( Dar_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;      }
+static inline void         Fra_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode )        { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]   = pNode;    }
+static inline void         Fra_ObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode )         { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]    = pNode;    }
+static inline void         Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]  = vFanins;  }
+static inline void         Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;      }
 
-static inline Dar_Obj_t *  Fra_ObjChild0Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin0(pObj)), Dar_ObjFaninC0(pObj)) : NULL;  }
-static inline Dar_Obj_t *  Fra_ObjChild1Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin1(pObj)), Dar_ObjFaninC1(pObj)) : NULL;  }
+static inline Aig_Obj_t *  Fra_ObjChild0Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL;  }
+static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL;  }
 
 ////////////////////////////////////////////////////////////////////////
 ///                         ITERATORS                                ///
@@ -167,21 +168,21 @@ extern void                Fra_CreateClasses( Fra_Man_t * p );
 extern int                 Fra_RefineClasses( Fra_Man_t * p );
 extern int                 Fra_RefineClasses1( Fra_Man_t * p );
 /*=== fraCnf.c ========================================================*/
-extern void                Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
+extern void                Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== fraCore.c ========================================================*/
-extern Dar_Man_t *         Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pParams );
+extern Aig_Man_t *         Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pParams );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
-extern Fra_Man_t *         Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pParams );
+extern Fra_Man_t *         Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
 extern void                Fra_ManPrepare( Fra_Man_t * p );
 extern void                Fra_ManStop( Fra_Man_t * p );
 extern void                Fra_ManPrint( Fra_Man_t * p );
 /*=== fraSat.c ========================================================*/
-extern int                 Fra_NodesAreEquiv( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
-extern int                 Fra_NodeIsConst( Fra_Man_t * p, Dar_Obj_t * pNew );
+extern int                 Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
+extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
 /*=== fraSim.c ========================================================*/
-extern int                 Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj );
-extern int                 Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 );
+extern int                 Fra_NodeHasZeroSim( Fra_Man_t * p, Aig_Obj_t * pObj );
+extern int                 Fra_NodeCompareSims( Fra_Man_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
 extern void                Fra_SavePattern( Fra_Man_t * p );
 extern void                Fra_Simulate( Fra_Man_t * p );
 extern void                Fra_Resimulate( Fra_Man_t * p );
diff --git a/src/aig/fra/fraAnd.c b/src/aig/fra/fraAnd.c
index a360ce9b..36b4ccc3 100644
--- a/src/aig/fra/fraAnd.c
+++ b/src/aig/fra/fraAnd.c
@@ -40,48 +40,48 @@
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
+Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld )
 { 
-    Dar_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig;
+    Aig_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig;
     int RetValue;
-    assert( !Dar_IsComplement(pObjOld) );
-    assert( Dar_ObjIsNode(pObjOld) );
+    assert( !Aig_IsComplement(pObjOld) );
+    assert( Aig_ObjIsNode(pObjOld) );
     // get the fraiged fanins
     pFanin0Fraig = Fra_ObjChild0Fra(pObjOld);
     pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
     // get the fraiged node
-    pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
-    if ( Dar_ObjIsConst1(Dar_Regular(pObjFraig)) )
+    pObjFraig = Aig_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
+    if ( Aig_ObjIsConst1(Aig_Regular(pObjFraig)) )
         return pObjFraig;
-    Dar_Regular(pObjFraig)->pData = p;
+    Aig_Regular(pObjFraig)->pData = p;
     // get representative of this class
     pObjOldRepr = Fra_ObjRepr(pObjOld);
     if ( pObjOldRepr == NULL || // this is a unique node
-       (!p->pPars->fDoSparse && pObjOldRepr == Dar_ManConst1(p->pManAig)) ) // this is a sparse node
+       (!p->pPars->fDoSparse && pObjOldRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node
     {
-        assert( Dar_Regular(pFanin0Fraig) != Dar_Regular(pFanin1Fraig) );
-        assert( Dar_Regular(pObjFraig) != Dar_Regular(pFanin0Fraig) );
-        assert( Dar_Regular(pObjFraig) != Dar_Regular(pFanin1Fraig) );
+        assert( Aig_Regular(pFanin0Fraig) != Aig_Regular(pFanin1Fraig) );
+        assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin0Fraig) );
+        assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin1Fraig) );
         return pObjFraig;
     }
     // get the fraiged representative
     pObjOldReprFraig = Fra_ObjFraig(pObjOldRepr);
     // if the fraiged nodes are the same, return
-    if ( Dar_Regular(pObjFraig) == Dar_Regular(pObjOldReprFraig) )
+    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjOldReprFraig) )
         return pObjFraig;
-    assert( Dar_Regular(pObjFraig) != Dar_ManConst1(p->pManFraig) );
+    assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
 //    printf( "Node = %d. Repr = %d.\n", pObjOld->Id, pObjOldRepr->Id );
 
     // if they are proved different, the c-ex will be in p->pPatWords
-    RetValue = Fra_NodesAreEquiv( p, Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) );
+    RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) );
     if ( RetValue == 1 )  // proved equivalent
     {
 //        pObjOld->fMarkA = 1;
-        return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
+        return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
     }
     if ( RetValue == -1 ) // failed
     {
-        Dar_Obj_t * ppNodes[2] = { Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) };
+        Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) };
         Vec_Ptr_t * vNodes;
 
         if ( !p->pPars->fSpeculate )
@@ -90,11 +90,11 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
 //        pObjOld->fMarkB = 1;
         p->nSpeculs++;
 
-        vNodes = Dar_ManDfsNodes( p->pManFraig, ppNodes, 2 );
+        vNodes = Aig_ManDfsNodes( p->pManFraig, ppNodes, 2 );
         printf( "%d ", Vec_PtrSize(vNodes) );
         Vec_PtrFree( vNodes );
 
-        return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
+        return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
     }
 //    printf( "Disproved %d and %d.\n", pObjOldRepr->Id, pObjOld->Id );
     // simulate the counter-example and return the Fraig node
@@ -118,18 +118,18 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
 ***********************************************************************/
 void Fra_Sweep( Fra_Man_t * p )
 {
-    Dar_Obj_t * pObj, * pObjNew;
+    Aig_Obj_t * pObj, * pObjNew;
     int i, k = 0;
 p->nClassesZero = Vec_PtrSize(p->vClasses1);
 p->nClassesBeg  = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
     // duplicate internal nodes
-//    p->pProgress = Extra_ProgressBarStart( stdout, Dar_ManNodeNum(p->pManAig) );
-    Dar_ManForEachNode( p->pManAig, pObj, i )
+//    p->pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p->pManAig) );
+    Aig_ManForEachNode( p->pManAig, pObj, i )
     {
 //        Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
         // default to simple strashing if simulation detected a counter-example for a PO
         if ( p->pManFraig->pData )
-            pObjNew = Dar_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
+            pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
         else
             pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented
         Fra_ObjSetFraig( pObj, pObjNew );
@@ -138,15 +138,15 @@ p->nClassesBeg  = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0
 //    Extra_ProgressBarStop( p->pProgress );
 p->nClassesEnd = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
     // try to prove the outputs of the miter
-    p->nNodesMiter = Dar_ManNodeNum(p->pManFraig);
+    p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
 //    Fra_MiterStatus( p->pManFraig );
 //    if ( p->pPars->fProve && p->pManFraig->pData == NULL )
 //        Fra_MiterProve( p );
     // add the POs
-    Dar_ManForEachPo( p->pManAig, pObj, i )
-        Dar_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) );
+    Aig_ManForEachPo( p->pManAig, pObj, i )
+        Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) );
     // remove dangling nodes 
-    Dar_ManCleanup( p->pManFraig );
+    Aig_ManCleanup( p->pManFraig );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 33421423..3de54453 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -36,8 +36,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline Dar_Obj_t *  Fra_ObjNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pObj )                       { return ppNexts[pObj->Id];  }
-static inline void         Fra_ObjSetNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pObj, Dar_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
+static inline Aig_Obj_t *  Fra_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj )                       { return ppNexts[pObj->Id];  }
+static inline void         Fra_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -54,9 +54,9 @@ static inline void         Fra_ObjSetNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pOb
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_PrintClass( Dar_Obj_t ** pClass )
+void Fra_PrintClass( Aig_Obj_t ** pClass )
 {
-    Dar_Obj_t * pTemp;
+    Aig_Obj_t * pTemp;
     int i;
     printf( "{ " );
     for ( i = 0; pTemp = pClass[i]; i++ )
@@ -75,9 +75,9 @@ void Fra_PrintClass( Dar_Obj_t ** pClass )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_CountClass( Dar_Obj_t ** pClass )
+int Fra_CountClass( Aig_Obj_t ** pClass )
 {
-    Dar_Obj_t * pTemp;
+    Aig_Obj_t * pTemp;
     int i;
     for ( i = 0; pTemp = pClass[i]; i++ );
     return i;
@@ -96,7 +96,7 @@ int Fra_CountClass( Dar_Obj_t ** pClass )
 ***********************************************************************/
 int Fra_CountPairsClasses( Fra_Man_t * p )
 {
-    Dar_Obj_t ** pClass;
+    Aig_Obj_t ** pClass;
     int i, nNodes, nPairs = 0;
     Vec_PtrForEachEntry( p->vClasses, pClass, i )
     {
@@ -120,7 +120,7 @@ int Fra_CountPairsClasses( Fra_Man_t * p )
 ***********************************************************************/
 void Fra_PrintClasses( Fra_Man_t * p )
 {
-    Dar_Obj_t ** pClass;
+    Aig_Obj_t ** pClass;
     int i;
     printf( "Total classes = %d. Total pairs = %d.\n", Vec_PtrSize(p->vClasses), Fra_CountPairsClasses(p) );
     Vec_PtrForEachEntry( p->vClasses, pClass, i )
@@ -142,7 +142,7 @@ void Fra_PrintClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned Fra_NodeHash( Fra_Man_t * p, Dar_Obj_t * pObj )
+unsigned Fra_NodeHash( Fra_Man_t * p, Aig_Obj_t * pObj )
 {
     static int s_FPrimes[128] = { 
         1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
@@ -220,21 +220,21 @@ unsigned int Cudd_PrimeFra( unsigned int p )
 ***********************************************************************/
 void Fra_CreateClasses( Fra_Man_t * p )
 {
-    Dar_Obj_t ** ppTable, ** ppNexts;
-    Dar_Obj_t * pObj, * pTemp;
+    Aig_Obj_t ** ppTable, ** ppNexts;
+    Aig_Obj_t * pObj, * pTemp;
     int i, k, nTableSize, nEntries, nNodes, iEntry;
 
     // allocate the hash table hashing simulation info into nodes
-    nTableSize = Cudd_PrimeFra( Dar_ManObjIdMax(p->pManAig) + 1 );
-    ppTable = ALLOC( Dar_Obj_t *, nTableSize ); 
-    ppNexts = ALLOC( Dar_Obj_t *, nTableSize ); 
-    memset( ppTable, 0, sizeof(Dar_Obj_t *) * nTableSize );
+    nTableSize = Cudd_PrimeFra( Aig_ManObjIdMax(p->pManAig) + 1 );
+    ppTable = ALLOC( Aig_Obj_t *, nTableSize ); 
+    ppNexts = ALLOC( Aig_Obj_t *, nTableSize ); 
+    memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
 
     // add all the nodes to the hash table
     Vec_PtrClear( p->vClasses1 );
-    Dar_ManForEachObj( p->pManAig, pObj, i )
+    Aig_ManForEachObj( p->pManAig, pObj, i )
     {
-        if ( !Dar_ObjIsNode(pObj) && !Dar_ObjIsPi(pObj) )
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
             continue;
         // hash the node by its simulation info
         iEntry = Fra_NodeHash( p, pObj ) % nTableSize;
@@ -242,7 +242,7 @@ void Fra_CreateClasses( Fra_Man_t * p )
         if ( iEntry == 0 && Fra_NodeHasZeroSim( p, pObj ) )
         {
             Vec_PtrPush( p->vClasses1, pObj );
-            Fra_ObjSetRepr( pObj, Dar_ManConst1(p->pManAig) );
+            Fra_ObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
             continue;
         }
         // add the node to the class
@@ -275,15 +275,15 @@ void Fra_CreateClasses( Fra_Man_t * p )
         }
 
     // allocate room for classes
-    p->pMemClasses = ALLOC( Dar_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
+    p->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
     p->pMemClassesFree = p->pMemClasses + 2*nEntries;
 
     // copy the entries into storage in the topological order
     Vec_PtrClear( p->vClasses );
     nEntries = 0;
-    Dar_ManForEachObj( p->pManAig, pObj, i )
+    Aig_ManForEachObj( p->pManAig, pObj, i )
     {
-        if ( !Dar_ObjIsNode(pObj) && !Dar_ObjIsPi(pObj) )
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
             continue;
         // skip the nodes that are not representatives of non-trivial classes
         if ( pObj->fMarkA == 0 )
@@ -307,7 +307,7 @@ void Fra_CreateClasses( Fra_Man_t * p )
             Fra_ObjSetRepr( pTemp, pObj );
         }
         // add as many empty entries
-//        memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Dar_Obj_t *) * nNodes );
+//        memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Aig_Obj_t *) * nNodes );
         p->pMemClasses[2*nEntries + nNodes] = NULL;
         // increment the number of entries
         nEntries += k;
@@ -329,9 +329,9 @@ void Fra_CreateClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass )
+Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass )
 {
-    Dar_Obj_t * pObj, ** ppThis;
+    Aig_Obj_t * pObj, ** ppThis;
     int i;
     assert( ppClass[0] != NULL && ppClass[1] != NULL );
 
@@ -390,7 +390,7 @@ Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass )
 ***********************************************************************/
 int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses )
 {
-    Dar_Obj_t ** pClass, ** pClass2;
+    Aig_Obj_t ** pClass, ** pClass2;
     int nRefis;
     pClass = Vec_PtrEntryLast( vClasses );
     for ( nRefis = 0; pClass2 = Fra_RefineClassOne( p, pClass ); nRefis++ )
@@ -426,7 +426,7 @@ int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses )
 int Fra_RefineClasses( Fra_Man_t * p )
 {
     Vec_Ptr_t * vTemp;
-    Dar_Obj_t ** pClass;
+    Aig_Obj_t ** pClass;
     int clk, i, nRefis;
     // check if some outputs already became non-constant
     // this is a special case when computation can be stopped!!!
@@ -466,14 +466,14 @@ p->timeRef += clock() - clk;
 ***********************************************************************/
 int Fra_RefineClasses1( Fra_Man_t * p )
 {
-    Dar_Obj_t * pObj, ** ppClass;
+    Aig_Obj_t * pObj, ** ppClass;
     int i, k, nRefis, clk;
     // check if there is anything to refine
     if ( Vec_PtrSize(p->vClasses1) == 0 )
         return 0;
 clk = clock();
     // make sure constant 1 class contains only non-constant nodes
-    assert( Vec_PtrEntry(p->vClasses1,0) != Dar_ManConst1(p->pManAig) );
+    assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pManAig) );
     // collect all the nodes to be refined
     k = 0;
     Vec_PtrClear( p->vClassNew );
diff --git a/src/aig/fra/fraCnf.c b/src/aig/fra/fraCnf.c
index a662ade2..7df55d93 100644
--- a/src/aig/fra/fraCnf.c
+++ b/src/aig/fra/fraCnf.c
@@ -40,23 +40,23 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_AddClausesMux( Fra_Man_t * p, Dar_Obj_t * pNode )
+void Fra_AddClausesMux( Fra_Man_t * p, Aig_Obj_t * pNode )
 {
-    Dar_Obj_t * pNodeI, * pNodeT, * pNodeE;
+    Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
     int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
 
-    assert( !Dar_IsComplement( pNode ) );
-    assert( Dar_ObjIsMuxType( pNode ) );
+    assert( !Aig_IsComplement( pNode ) );
+    assert( Aig_ObjIsMuxType( pNode ) );
     // get nodes (I = if, T = then, E = else)
-    pNodeI = Dar_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
+    pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
     // get the variable numbers
     VarF = Fra_ObjSatNum(pNode);
     VarI = Fra_ObjSatNum(pNodeI);
-    VarT = Fra_ObjSatNum(Dar_Regular(pNodeT));
-    VarE = Fra_ObjSatNum(Dar_Regular(pNodeE));
+    VarT = Fra_ObjSatNum(Aig_Regular(pNodeT));
+    VarE = Fra_ObjSatNum(Aig_Regular(pNodeE));
     // get the complementation flags
-    fCompT = Dar_IsComplement(pNodeT);
-    fCompE = Dar_IsComplement(pNodeE);
+    fCompT = Aig_IsComplement(pNodeT);
+    fCompE = Aig_IsComplement(pNodeE);
 
     // f = ITE(i, t, e)
 
@@ -123,12 +123,12 @@ void Fra_AddClausesMux( Fra_Man_t * p, Dar_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_AddClausesSuper( Fra_Man_t * p, Dar_Obj_t * pNode, Vec_Ptr_t * vSuper )
+void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
 {
-    Dar_Obj_t * pFanin;
+    Aig_Obj_t * pFanin;
     int * pLits, nLits, RetValue, i;
-    assert( !Dar_IsComplement(pNode) );
-    assert( Dar_ObjIsNode( pNode ) );
+    assert( !Aig_IsComplement(pNode) );
+    assert( Aig_ObjIsNode( pNode ) );
     // create storage for literals
     nLits = Vec_PtrSize(vSuper) + 1;
     pLits = ALLOC( int, nLits );
@@ -136,14 +136,14 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Dar_Obj_t * pNode, Vec_Ptr_t * vSuper )
     // add !A => !C   or   A + !C
     Vec_PtrForEachEntry( vSuper, pFanin, i )
     {
-        pLits[0] = toLitCond(Fra_ObjSatNum(Dar_Regular(pFanin)), Dar_IsComplement(pFanin));
+        pLits[0] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
         pLits[1] = toLitCond(Fra_ObjSatNum(pNode), 1);
         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
         assert( RetValue );
     }
     // add A & B => C   or   !A + !B + C
     Vec_PtrForEachEntry( vSuper, pFanin, i )
-        pLits[i] = toLitCond(Fra_ObjSatNum(Dar_Regular(pFanin)), !Dar_IsComplement(pFanin));
+        pLits[i] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
     pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0);
     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
     assert( RetValue );
@@ -161,18 +161,18 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Dar_Obj_t * pNode, Vec_Ptr_t * vSuper )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_CollectSuper_rec( Dar_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
+void Fra_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
 {
     // if the new node is complemented or a PI, another gate begins
-    if ( Dar_IsComplement(pObj) || Dar_ObjIsPi(pObj) || (!fFirst && Dar_ObjRefs(pObj) > 1) || 
-         (fUseMuxes && Dar_ObjIsMuxType(pObj)) )
+    if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || 
+         (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
     {
         Vec_PtrPushUnique( vSuper, pObj );
         return;
     }
     // go through the branches
-    Fra_CollectSuper_rec( Dar_ObjChild0(pObj), vSuper, 0, fUseMuxes );
-    Fra_CollectSuper_rec( Dar_ObjChild1(pObj), vSuper, 0, fUseMuxes );
+    Fra_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
+    Fra_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
 }
 
 /**Function*************************************************************
@@ -186,11 +186,11 @@ void Fra_CollectSuper_rec( Dar_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Fra_CollectSuper( Dar_Obj_t * pObj, int fUseMuxes )
+Vec_Ptr_t * Fra_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes )
 {
     Vec_Ptr_t * vSuper;
-    assert( !Dar_IsComplement(pObj) );
-    assert( !Dar_ObjIsPi(pObj) );
+    assert( !Aig_IsComplement(pObj) );
+    assert( !Aig_ObjIsPi(pObj) );
     vSuper = Vec_PtrAlloc( 4 );
     Fra_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
     return vSuper;
@@ -207,19 +207,19 @@ Vec_Ptr_t * Fra_CollectSuper( Dar_Obj_t * pObj, int fUseMuxes )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_ObjAddToFrontier( Fra_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+void Fra_ObjAddToFrontier( Fra_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
 {
     Fra_Man_t * pTemp = pObj->pData;
-    assert( !Dar_IsComplement(pObj) );
+    assert( !Aig_IsComplement(pObj) );
     if ( Fra_ObjSatNum(pObj) )
         return;
     assert( Fra_ObjSatNum(pObj) == 0 );
     assert( Fra_ObjFaninVec(pObj) == NULL );
-    if ( Dar_ObjIsConst1(pObj) )
+    if ( Aig_ObjIsConst1(pObj) )
         return;
 //printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars );
     Fra_ObjSetSatNum( pObj, p->nSatVars++ );
-    if ( Dar_ObjIsNode(pObj) )
+    if ( Aig_ObjIsNode(pObj) )
         Vec_PtrPush( vFrontier, pObj );
 }
 
@@ -234,10 +234,10 @@ void Fra_ObjAddToFrontier( Fra_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vFrontie
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
+void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 { 
     Vec_Ptr_t * vFrontier, * vFanins;
-    Dar_Obj_t * pNode, * pFanin;
+    Aig_Obj_t * pNode, * pFanin;
     int i, k, fUseMuxes = 1;
     assert( pOld || pNew );
     // quit if CNF is ready
@@ -253,22 +253,22 @@ void Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
         // create the supergate
         assert( Fra_ObjSatNum(pNode) );
         assert( Fra_ObjFaninVec(pNode) == NULL );
-        if ( fUseMuxes && Dar_ObjIsMuxType(pNode) )
+        if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
         {
             vFanins = Vec_PtrAlloc( 4 );
-            Vec_PtrPushUnique( vFanins, Dar_ObjFanin0( Dar_ObjFanin0(pNode) ) );
-            Vec_PtrPushUnique( vFanins, Dar_ObjFanin0( Dar_ObjFanin1(pNode) ) );
-            Vec_PtrPushUnique( vFanins, Dar_ObjFanin1( Dar_ObjFanin0(pNode) ) );
-            Vec_PtrPushUnique( vFanins, Dar_ObjFanin1( Dar_ObjFanin1(pNode) ) );
+            Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
+            Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
+            Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
+            Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
             Vec_PtrForEachEntry( vFanins, pFanin, k )
-                Fra_ObjAddToFrontier( p, Dar_Regular(pFanin), vFrontier );
+                Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
             Fra_AddClausesMux( p, pNode );
         }
         else
         {
             vFanins = Fra_CollectSuper( pNode, fUseMuxes );
             Vec_PtrForEachEntry( vFanins, pFanin, k )
-                Fra_ObjAddToFrontier( p, Dar_Regular(pFanin), vFrontier );
+                Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
             Fra_AddClausesSuper( p, pNode, vFanins );
         }
         assert( Vec_PtrSize(vFanins) > 1 );
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 7fdd1b83..5338d662 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -39,15 +39,15 @@
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Man_t * Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pPars )
+Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
 {
     Fra_Man_t * p;
-    Dar_Man_t * pManAigNew;
+    Aig_Man_t * pManAigNew;
     int clk;
-    if ( Dar_ManNodeNum(pManAig) == 0 )
-        return Dar_ManDup(pManAig);
+    if ( Aig_ManNodeNum(pManAig) == 0 )
+        return Aig_ManDup(pManAig);
 clk = clock();
-    assert( Dar_ManLatchNum(pManAig) == 0 );
+    assert( Aig_ManLatchNum(pManAig) == 0 );
     p = Fra_ManStart( pManAig, pPars );
     Fra_Simulate( p );
     Fra_Sweep( p );
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 19ed6c03..78246a8c 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -66,7 +66,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
+Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
 {
     Fra_Man_t * p;
     // allocate the fraiging manager
@@ -74,15 +74,15 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
     memset( p, 0, sizeof(Fra_Man_t) );
     p->pPars      = pPars;
     p->pManAig    = pManAig;
-    p->pManFraig  = Dar_ManStartFrom( pManAig );
-    assert( Dar_ManPiNum(p->pManAig) == Dar_ManPiNum(p->pManFraig) );
+    p->pManFraig  = Aig_ManStartFrom( pManAig );
+    assert( Aig_ManPiNum(p->pManAig) == Aig_ManPiNum(p->pManFraig) );
     // allocate simulation info
     p->nSimWords  = pPars->nSimWords;
-    p->pSimWords  = ALLOC( unsigned, (Dar_ManObjIdMax(pManAig) + 1) * p->nSimWords );
+    p->pSimWords  = ALLOC( unsigned, (Aig_ManObjIdMax(pManAig) + 1) * p->nSimWords );
     // clean simulation info of the constant node
-    memset( p->pSimWords, 0, sizeof(unsigned) * ((Dar_ManPiNum(pManAig) + 1) * p->nSimWords) );
+    memset( p->pSimWords, 0, sizeof(unsigned) * ((Aig_ManPiNum(pManAig) + 1) * p->nSimWords) );
     // allocate storage for sim pattern
-    p->nPatWords  = Dar_BitWordNum( Dar_ManPiNum(pManAig) );
+    p->nPatWords  = Aig_BitWordNum( Aig_ManPiNum(pManAig) );
     p->pPatWords  = ALLOC( unsigned, p->nPatWords ); 
     p->pPatScores = ALLOC( int, 32 * p->nSimWords ); 
     p->vPiVars    = Vec_PtrAlloc( 100 );
@@ -92,11 +92,11 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
     p->vClassNew  = Vec_PtrAlloc( 100 );
     p->vClassesTemp = Vec_PtrAlloc( 100 );
     // allocate other members
-    p->nSizeAlloc = Dar_ManObjIdMax(pManAig) + 1;
-    p->pMemFraig  = ALLOC( Dar_Obj_t *, p->nSizeAlloc );
-    memset( p->pMemFraig, 0, p->nSizeAlloc * sizeof(Dar_Obj_t *) );
-    p->pMemRepr  = ALLOC( Dar_Obj_t *, p->nSizeAlloc );
-    memset( p->pMemRepr, 0, p->nSizeAlloc * sizeof(Dar_Obj_t *) );
+    p->nSizeAlloc = Aig_ManObjIdMax(pManAig) + 1;
+    p->pMemFraig  = ALLOC( Aig_Obj_t *, p->nSizeAlloc );
+    memset( p->pMemFraig, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
+    p->pMemRepr  = ALLOC( Aig_Obj_t *, p->nSizeAlloc );
+    memset( p->pMemRepr, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
     p->pMemFanins  = ALLOC( Vec_Ptr_t *, p->nSizeAlloc );
     memset( p->pMemFanins, 0, p->nSizeAlloc * sizeof(Vec_Ptr_t *) );
     p->pMemSatNums  = ALLOC( int, p->nSizeAlloc );
@@ -123,18 +123,18 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
 ***********************************************************************/
 void Fra_ManPrepare( Fra_Man_t * p )
 {
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i;
     // set the pointers to the manager
-    Dar_ManForEachObj( p->pManFraig, pObj, i )
+    Aig_ManForEachObj( p->pManFraig, pObj, i )
         pObj->pData = p;
     // set the pointer to the manager
-    Dar_ManForEachObj( p->pManAig, pObj, i )
+    Aig_ManForEachObj( p->pManAig, pObj, i )
         pObj->pData = p;
     // set the pointers to the available fraig nodes
-    Fra_ObjSetFraig( Dar_ManConst1(p->pManAig), Dar_ManConst1(p->pManFraig) );
-    Dar_ManForEachPi( p->pManAig, pObj, i )
-        Fra_ObjSetFraig( pObj, Dar_ManPi(p->pManFraig, i) );
+    Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), Aig_ManConst1(p->pManFraig) );
+    Aig_ManForEachPi( p->pManAig, pObj, i )
+        Fra_ObjSetFraig( pObj, Aig_ManPi(p->pManFraig, i) );
 }
 
 /**Function*************************************************************
@@ -187,14 +187,14 @@ void Fra_ManStop( Fra_Man_t * p )
 ***********************************************************************/
 void Fra_ManPrint( Fra_Man_t * p )
 {
-    double nMemory = 1.0*Dar_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
+    double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
     printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb.  ", p->nSimWords, p->nSimRounds, nMemory );
     printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
     printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pPars->nBTLimitNode, p->pPars->nBTLimitMiter );
     printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 
         p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
     printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", 
-        Dar_ManNodeNum(p->pManFraig), p->nNodesMiter, Dar_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
+        Aig_ManNodeNum(p->pManFraig), p->nNodesMiter, Aig_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
     if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
     PRT( "AIG simulation  ", p->timeSim  );
     PRT( "AIG traversal   ", p->timeTrav  );
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index 1c72c807..66b1ba5a 100644
--- a/src/aig/fra/fraSat.c
+++ b/src/aig/fra/fraSat.c
@@ -24,7 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
+static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -41,13 +41,13 @@ static int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t *
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_NodesAreEquiv( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
+int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
     int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
 
     // make sure the nodes are not complemented
-    assert( !Dar_IsComplement(pNew) );
-    assert( !Dar_IsComplement(pOld) );
+    assert( !Aig_IsComplement(pNew) );
+    assert( !Aig_IsComplement(pOld) );
     assert( pNew != pOld );
 
     // if at least one of the nodes is a failed node, perform adjustments:
@@ -189,12 +189,12 @@ p->timeSatFail += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_NodeIsConst( Fra_Man_t * p, Dar_Obj_t * pNew )
+int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
 {
     int pLits[2], RetValue1, RetValue, clk;
 
     // make sure the nodes are not complemented
-    assert( !Dar_IsComplement(pNew) );
+    assert( !Aig_IsComplement(pNew) );
     assert( pNew != p->pManFraig->pConst1 );
     p->nSatCalls++;
 
@@ -261,19 +261,19 @@ p->timeSatFail += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_SetActivityFactors_rec( Fra_Man_t * p, Dar_Obj_t * pObj, int LevelMin, int LevelMax )
+int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, int LevelMax )
 {
     Vec_Ptr_t * vFanins;
-    Dar_Obj_t * pFanin;
+    Aig_Obj_t * pFanin;
     int i, Counter = 0;
-    assert( !Dar_IsComplement(pObj) );
+    assert( !Aig_IsComplement(pObj) );
     assert( Fra_ObjSatNum(pObj) );
     // skip visited variables
-    if ( Dar_ObjIsTravIdCurrent(p->pManFraig, pObj) )
+    if ( Aig_ObjIsTravIdCurrent(p->pManFraig, pObj) )
         return 0;
-    Dar_ObjSetTravIdCurrent(p->pManFraig, pObj);
+    Aig_ObjSetTravIdCurrent(p->pManFraig, pObj);
     // add the PI to the list
-    if ( pObj->Level <= (unsigned)LevelMin || Dar_ObjIsPi(pObj) )
+    if ( pObj->Level <= (unsigned)LevelMin || Aig_ObjIsPi(pObj) )
         return 0;
     // set the factor of this variable
     // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump
@@ -282,7 +282,7 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Dar_Obj_t * pObj, int LevelMin, i
     // explore the fanins
     vFanins = Fra_ObjFaninVec( pObj );
     Vec_PtrForEachEntry( vFanins, pFanin, i )
-        Counter += Fra_SetActivityFactors_rec( p, Dar_Regular(pFanin), LevelMin, LevelMax );
+        Counter += Fra_SetActivityFactors_rec( p, Aig_Regular(pFanin), LevelMin, LevelMax );
     return 1 + Counter;
 }
 
@@ -297,7 +297,7 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Dar_Obj_t * pObj, int LevelMin, i
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
+int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
     int clk, LevelMin, LevelMax;
     assert( pOld || pNew );
@@ -305,15 +305,15 @@ clk = clock();
     // reset the active variables
     veci_resize(&p->pSat->act_vars, 0);
     // prepare for traversal
-    Dar_ManIncrementTravId( p->pManFraig );
+    Aig_ManIncrementTravId( p->pManFraig );
     // determine the min and max level to visit
     assert( p->pPars->dActConeRatio > 0 && p->pPars->dActConeRatio < 1 );
-    LevelMax = DAR_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
+    LevelMax = AIG_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
     LevelMin = (int)(LevelMax * (1.0 - p->pPars->dActConeRatio));
     // traverse
-    if ( pOld && !Dar_ObjIsConst1(pOld) )
+    if ( pOld && !Aig_ObjIsConst1(pOld) )
         Fra_SetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
-    if ( pNew && !Dar_ObjIsConst1(pNew) )
+    if ( pNew && !Aig_ObjIsConst1(pNew) )
         Fra_SetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
 //Fra_PrintActivity( p );
 p->timeTrav += clock() - clk;
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 7207cfa2..beaa79fd 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -39,11 +39,11 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeAssignRandom( Fra_Man_t * p, Dar_Obj_t * pObj )
+void Fra_NodeAssignRandom( Fra_Man_t * p, Aig_Obj_t * pObj )
 {
     unsigned * pSims;
     int i;
-    assert( Dar_ObjIsPi(pObj) );
+    assert( Aig_ObjIsPi(pObj) );
     pSims = Fra_ObjSim(pObj);
     for ( i = 0; i < p->nSimWords; i++ )
         pSims[i] = Fra_ObjRandomSim();
@@ -60,11 +60,11 @@ void Fra_NodeAssignRandom( Fra_Man_t * p, Dar_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeAssignConst( Fra_Man_t * p, Dar_Obj_t * pObj, int fConst1 )
+void Fra_NodeAssignConst( Fra_Man_t * p, Aig_Obj_t * pObj, int fConst1 )
 {
     unsigned * pSims;
     int i;
-    assert( Dar_ObjIsPi(pObj) );
+    assert( Aig_ObjIsPi(pObj) );
     pSims = Fra_ObjSim(pObj);
     for ( i = 0; i < p->nSimWords; i++ )
         pSims[i] = fConst1? ~(unsigned)0 : 0;
@@ -83,9 +83,9 @@ void Fra_NodeAssignConst( Fra_Man_t * p, Dar_Obj_t * pObj, int fConst1 )
 ***********************************************************************/
 void Fra_AssignRandom( Fra_Man_t * p )
 {
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i;
-    Dar_ManForEachPi( p->pManAig, pObj, i )
+    Aig_ManForEachPi( p->pManAig, pObj, i )
         Fra_NodeAssignRandom( p, pObj );
 }
 
@@ -102,17 +102,17 @@ void Fra_AssignRandom( Fra_Man_t * p )
 ***********************************************************************/
 void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
 {
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i, Limit;
-    Dar_ManForEachPi( p->pManAig, pObj, i )
+    Aig_ManForEachPi( p->pManAig, pObj, i )
     {
-        Fra_NodeAssignConst( p, pObj, Dar_InfoHasBit(pPat, i) );
-//        printf( "%d", Dar_InfoHasBit(pPat, i) );
+        Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, i) );
+//        printf( "%d", Aig_InfoHasBit(pPat, i) );
     }
 //    printf( "\n" );
-    Limit = DAR_MIN( Dar_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
+    Limit = AIG_MIN( Aig_ManPiNum(p->pManAig), p->nSimWords * 32 - 1 );
     for ( i = 0; i < Limit; i++ )
-        Dar_InfoXorBit( Fra_ObjSim( Dar_ManPi(p->pManAig,i) ), i+1 );
+        Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 );
 }
 
 /**Function*************************************************************
@@ -126,7 +126,7 @@ void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj )
+int Fra_NodeHasZeroSim( Fra_Man_t * p, Aig_Obj_t * pObj )
 {
     unsigned * pSims;
     int i;
@@ -148,7 +148,7 @@ int Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeComplementSim( Fra_Man_t * p, Dar_Obj_t * pObj )
+void Fra_NodeComplementSim( Fra_Man_t * p, Aig_Obj_t * pObj )
 {
     unsigned * pSims;
     int i;
@@ -168,7 +168,7 @@ void Fra_NodeComplementSim( Fra_Man_t * p, Dar_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 )
+int Fra_NodeCompareSims( Fra_Man_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
 {
     unsigned * pSims0, * pSims1;
     int i;
@@ -192,20 +192,20 @@ int Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeSimulate( Fra_Man_t * p, Dar_Obj_t * pObj )
+void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj )
 {
     unsigned * pSims, * pSims0, * pSims1;
     int fCompl, fCompl0, fCompl1, i;
-    assert( !Dar_IsComplement(pObj) );
-    assert( Dar_ObjIsNode(pObj) );
+    assert( !Aig_IsComplement(pObj) );
+    assert( Aig_ObjIsNode(pObj) );
     // get hold of the simulation information
     pSims  = Fra_ObjSim(pObj);
-    pSims0 = Fra_ObjSim(Dar_ObjFanin0(pObj));
-    pSims1 = Fra_ObjSim(Dar_ObjFanin1(pObj));
+    pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj));
+    pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj));
     // get complemented attributes of the children using their random info
     fCompl  = pObj->fPhase;
-    fCompl0 = Dar_ObjFaninPhase(Dar_ObjChild0(pObj));
-    fCompl1 = Dar_ObjFaninPhase(Dar_ObjChild1(pObj));
+    fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj));
+    fCompl1 = Aig_ObjFaninPhase(Aig_ObjChild1(pObj));
     // simulate
     if ( fCompl0 && fCompl1 )
     {
@@ -290,13 +290,13 @@ void Fra_SavePattern1( Fra_Man_t * p )
 ***********************************************************************/
 void Fra_SavePattern( Fra_Man_t * p )
 {
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i;
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
-    Dar_ManForEachPi( p->pManFraig, pObj, i )
+    Aig_ManForEachPi( p->pManFraig, pObj, i )
 //    Vec_PtrForEachEntry( p->vPiVars, pObj, i )
         if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
-            Dar_InfoSetBit( p->pPatWords, i );
+            Aig_InfoSetBit( p->pPatWords, i );
 //            Ivy_InfoSetBit( p->pPatWords, pObj->Id - 1 );
 }
 
@@ -329,7 +329,7 @@ void Fra_CleanPatScores( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_AddToPatScores( Fra_Man_t * p, Dar_Obj_t * pClass, Dar_Obj_t * pClassNew )
+void Fra_AddToPatScores( Fra_Man_t * p, Aig_Obj_t * pClass, Aig_Obj_t * pClassNew )
 {
     unsigned * pSims0, * pSims1;
     unsigned uDiff;
@@ -363,7 +363,7 @@ void Fra_AddToPatScores( Fra_Man_t * p, Dar_Obj_t * pClass, Dar_Obj_t * pClassNe
 int Fra_SelectBestPat( Fra_Man_t * p )
 {
     unsigned * pSims;
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i, nLimit = p->nSimWords * 32, MaxScore = 0, BestPat = -1;
     for ( i = 1; i < nLimit; i++ )
     {
@@ -379,11 +379,11 @@ int Fra_SelectBestPat( Fra_Man_t * p )
 //    printf( "Max score is %3d.  ", MaxScore );
     // copy the best pattern into the selected pattern
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
-    Dar_ManForEachPi( p->pManAig, pObj, i )
+    Aig_ManForEachPi( p->pManAig, pObj, i )
     {
         pSims = Fra_ObjSim(pObj);
-        if ( Dar_InfoHasBit(pSims, BestPat) )
-            Dar_InfoSetBit(p->pPatWords, i);
+        if ( Aig_InfoHasBit(pSims, BestPat) )
+            Aig_InfoSetBit(p->pPatWords, i);
     }
     return MaxScore;
 }
@@ -401,17 +401,17 @@ int Fra_SelectBestPat( Fra_Man_t * p )
 ***********************************************************************/
 void Fra_SimulateOne( Fra_Man_t * p )
 {
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i, clk;
 clk = clock();
-    Dar_ManForEachNode( p->pManAig, pObj, i )
+    Aig_ManForEachNode( p->pManAig, pObj, i )
     {
         Fra_NodeSimulate( p, pObj );
 /*
-        if ( Dar_ObjFraig(pObj) == NULL )
+        if ( Aig_ObjFraig(pObj) == NULL )
             printf( "%3d --- -- %d  :  ", pObj->Id, pObj->fPhase );
         else
-            printf( "%3d %3d %2d %d  :  ", pObj->Id, Dar_Regular(Dar_ObjFraig(pObj))->Id, Dar_ObjSatNum(Dar_Regular(Dar_ObjFraig(pObj))), pObj->fPhase );
+            printf( "%3d %3d %2d %d  :  ", pObj->Id, Aig_Regular(Aig_ObjFraig(pObj))->Id, Aig_ObjSatNum(Aig_Regular(Aig_ObjFraig(pObj))), pObj->fPhase );
         Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 30 );
         printf( "\n" );
 */
@@ -527,7 +527,7 @@ void Fra_Simulate( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Dar_Obj_t * pObj )
+void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
 { 
     unsigned * pSims;
     int i, k, BestPat, * pModel;
@@ -545,10 +545,10 @@ void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Dar_Obj_t * pObj )
     // determine the best pattern
     BestPat = i * 32 + k;
     // fill in the counter-example data
-    pModel = ALLOC( int, Dar_ManPiNum(p->pManFraig) );
-    Dar_ManForEachPi( p->pManAig, pObj, i )
+    pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig) );
+    Aig_ManForEachPi( p->pManAig, pObj, i )
     {
-        pModel[i] = Dar_InfoHasBit(Fra_ObjSim(pObj), BestPat);
+        pModel[i] = Aig_InfoHasBit(Fra_ObjSim(pObj), BestPat);
 //        printf( "%d", pModel[i] );
     }
 //    printf( "\n" );
@@ -571,26 +571,26 @@ void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Dar_Obj_t * pObj )
 ***********************************************************************/
 int Fra_CheckOutputSims( Fra_Man_t * p )
 {
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i;
     // make sure the reference simulation pattern does not detect the bug
-    pObj = Dar_ManPo( p->pManAig, 0 );
-    assert( Dar_ObjFanin0(pObj)->fPhase == (unsigned)Dar_ObjFaninC0(pObj) ); // Dar_ObjFaninPhase(Dar_ObjChild0(pObj)) == 0
-    Dar_ManForEachPo( p->pManAig, pObj, i )
+    pObj = Aig_ManPo( p->pManAig, 0 );
+    assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); // Aig_ObjFaninPhase(Aig_ObjChild0(pObj)) == 0
+    Aig_ManForEachPo( p->pManAig, pObj, i )
     {
         // complement simulation info
-//        if ( Dar_ObjFanin0(pObj)->fPhase ^ Dar_ObjFaninC0(pObj) ) // Dar_ObjFaninPhase(Dar_ObjChild0(pObj))
-//            Fra_NodeComplementSim( p, Dar_ObjFanin0(pObj) );
+//        if ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) ) // Aig_ObjFaninPhase(Aig_ObjChild0(pObj))
+//            Fra_NodeComplementSim( p, Aig_ObjFanin0(pObj) );
         // check 
-        if ( !Fra_NodeHasZeroSim( p, Dar_ObjFanin0(pObj) ) )
+        if ( !Fra_NodeHasZeroSim( p, Aig_ObjFanin0(pObj) ) )
         {
             // create the counter-example from this pattern
-            Fra_CheckOutputSimsSavePattern( p, Dar_ObjFanin0(pObj) );
+            Fra_CheckOutputSimsSavePattern( p, Aig_ObjFanin0(pObj) );
             return 1;
         }
         // complement simulation info
-//        if ( Dar_ObjFanin0(pObj)->fPhase ^ Dar_ObjFaninC0(pObj) )
-//            Fra_NodeComplementSim( p, Dar_ObjFanin0(pObj) );
+//        if ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) )
+//            Fra_NodeComplementSim( p, Aig_ObjFanin0(pObj) );
     }
     return 0;
 }