initial commit of public abc

13 files changed, 508 insertions, 155 deletions

diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 86f43a9e..0a3b5eb7 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -21,6 +21,7 @@
 #ifndef __DAR_H__
 #define __DAR_H__
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -29,9 +30,10 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef __cplusplus
-extern "C" {
-#endif 
+
+
+ABC_NAMESPACE_HEADER_START
+ 
 
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
@@ -80,6 +82,8 @@ struct Dar_RefPar_t_
 /*=== darLib.c ========================================================*/
 extern void            Dar_LibStart();
 extern void            Dar_LibStop();
+extern void            Dar_LibPrepare( int nSubgraphs );
+extern int             Dar_LibReturnClass( unsigned uTruth );
 /*=== darBalance.c ========================================================*/
 extern Aig_Man_t *     Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
 extern Aig_Man_t *     Dar_ManBalanceXor( Aig_Man_t * pAig, int fExor, int fUpdateLevel, int fVerbose );
@@ -98,9 +102,11 @@ extern Aig_Man_t *     Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpd
 extern Aig_Man_t *     Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose );
 extern Aig_Man_t *     Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose );
 
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
 
 #endif
 
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 35da7fe2..3bfcbdaa 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -21,6 +21,9 @@
 #include "darInt.h"
 #include "tim.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -107,13 +110,13 @@ Vec_Ptr_t * Dar_BalanceCone( Aig_Obj_t * pObj, Vec_Vec_t * vStore, int Level )
     if ( Vec_VecSize( vStore ) <= Level )
         Vec_VecPush( vStore, Level, 0 );
     // get the temporary array of nodes
-    vNodes = Vec_VecEntry( vStore, Level );
+    vNodes = (Vec_Ptr_t *)Vec_VecEntry( vStore, Level );
     Vec_PtrClear( vNodes );
     // collect the nodes in the implication supergate
     RetValue = Dar_BalanceCone_rec( pObj, pObj, vNodes );
     assert( vNodes->nSize > 1 );
     // unmark the visited nodes
-    Vec_PtrForEachEntry( vNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
         Aig_Regular(pObj)->fMarkB = 0;
     // if we found the node and its complement in the same implication supergate, 
     // return empty set of nodes (meaning that we should use constant-0 node)
@@ -146,19 +149,19 @@ int Dar_BalanceFindLeft( Vec_Ptr_t * vSuper )
         return 0;
     // set the pointer to the one before the last
     Current = Vec_PtrSize(vSuper) - 2;
-    pObjRight = Vec_PtrEntry( vSuper, Current );
+    pObjRight = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current );
     // go through the nodes to the left of this one
     for ( Current--; Current >= 0; Current-- )
     {
         // get the next node on the left
-        pObjLeft = Vec_PtrEntry( vSuper, Current );
+        pObjLeft = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current );
         // if the level of this node is different, quit the loop
         if ( Aig_ObjLevel(Aig_Regular(pObjLeft)) != Aig_ObjLevel(Aig_Regular(pObjRight)) )
             break;
     }
     Current++;    
     // get the node, for which the equality holds
-    pObjLeft = Vec_PtrEntry( vSuper, Current );
+    pObjLeft = (Aig_Obj_t *)Vec_PtrEntry( vSuper, Current );
     assert( Aig_ObjLevel(Aig_Regular(pObjLeft)) == Aig_ObjLevel(Aig_Regular(pObjRight)) );
     return Current;
 }
@@ -185,14 +188,14 @@ void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int f
     if ( LeftBound == RightBound )
         return;
     // get the two last nodes
-    pObj1 = Vec_PtrEntry( vSuper, RightBound + 1 );
-    pObj2 = Vec_PtrEntry( vSuper, RightBound     );
+    pObj1 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, RightBound + 1 );
+    pObj2 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, RightBound     );
     if ( Aig_Regular(pObj1) == p->pConst1 || Aig_Regular(pObj2) == p->pConst1 || Aig_Regular(pObj1) == Aig_Regular(pObj2) )
         return;
     // find the first node that can be shared
     for ( i = RightBound; i >= LeftBound; i-- )
     {
-        pObj3 = Vec_PtrEntry( vSuper, i );
+        pObj3 = (Aig_Obj_t *)Vec_PtrEntry( vSuper, i );
         if ( Aig_Regular(pObj3) == p->pConst1 )
         {
             Vec_PtrWriteEntry( vSuper, i,          pObj2 );
@@ -271,8 +274,8 @@ void Dar_BalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Aig_Obj_t * pObj )
     // find the p of the node
     for ( i = vStore->nSize-1; i > 0; i-- )
     {
-        pObj1 = vStore->pArray[i  ];
-        pObj2 = vStore->pArray[i-1];
+        pObj1 = (Aig_Obj_t *)vStore->pArray[i  ];
+        pObj2 = (Aig_Obj_t *)vStore->pArray[i-1];
         if ( Aig_ObjLevel(Aig_Regular(pObj1)) <= Aig_ObjLevel(Aig_Regular(pObj2)) )
             break;
         vStore->pArray[i  ] = pObj2;
@@ -297,7 +300,7 @@ Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t
     int LeftBound;
     assert( vSuper->nSize > 1 );
     // sort the new nodes by level in the decreasing order
-    Vec_PtrSort( vSuper, Aig_NodeCompareLevelsDecrease );
+    Vec_PtrSort( vSuper, (int (*)(void))Aig_NodeCompareLevelsDecrease );
     // balance the nodes
     while ( vSuper->nSize > 1 )
     {
@@ -306,11 +309,11 @@ Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t
         // find the node that can be shared (if no such node, randomize choice)
         Dar_BalancePermute( p, vSuper, LeftBound, Type == AIG_OBJ_EXOR );
         // pull out the last two nodes
-        pObj1 = Vec_PtrPop(vSuper);
-        pObj2 = Vec_PtrPop(vSuper);
+        pObj1 = (Aig_Obj_t *)Vec_PtrPop(vSuper);
+        pObj2 = (Aig_Obj_t *)Vec_PtrPop(vSuper);
         Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type) );
     }
-    return Vec_PtrEntry(vSuper, 0);
+    return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0);
 }
 
 /**Function*************************************************************
@@ -333,20 +336,20 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
     assert( !Aig_ObjIsBuf(pObjOld) );
     // return if the result is known
     if ( pObjOld->pData )
-        return pObjOld->pData;
+        return (Aig_Obj_t *)pObjOld->pData;
     assert( Aig_ObjIsNode(pObjOld) );
     // get the implication supergate
     vSuper = Dar_BalanceCone( pObjOld, vStore, Level );
     // check if supergate contains two nodes in the opposite polarity
     if ( vSuper->nSize == 0 )
-        return pObjOld->pData = Aig_ManConst0(pNew);
+        return (Aig_Obj_t *)(pObjOld->pData = Aig_ManConst0(pNew));
     if ( Vec_PtrSize(vSuper) < 2 )
         printf( "Dar_Balance_rec: Internal error!\n" );
     // for each old node, derive the new well-balanced node
     for ( i = 0; i < Vec_PtrSize(vSuper); i++ )
     {
-        pObjNew = Dar_Balance_rec( pNew, Aig_Regular(vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
-        vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement(vSuper->pArray[i]) );
+        pObjNew = Dar_Balance_rec( pNew, Aig_Regular((Aig_Obj_t *)vSuper->pArray[i]), vStore, Level + 1, fUpdateLevel );
+        vSuper->pArray[i] = Aig_NotCond( pObjNew, Aig_IsComplement((Aig_Obj_t *)vSuper->pArray[i]) );
     }
     // build the supergate
     pObjNew = Dar_BalanceBuildSuper( pNew, vSuper, Aig_ObjType(pObjOld), fUpdateLevel );
@@ -366,7 +369,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
     }
     else
         Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
-    return pObjOld->pData = pObjNew;
+    return (Aig_Obj_t *)(pObjOld->pData = pObjNew);
 }
 
 /**Function*************************************************************
@@ -392,6 +395,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     pNew->pName = Aig_UtilStrsav( p->pName );
     pNew->pSpec = Aig_UtilStrsav( p->pSpec );
     pNew->nAsserts = p->nAsserts;
+    pNew->nConstrs = p->nConstrs;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // pass the HAIG manager
@@ -407,7 +411,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     if ( p->pManTime != NULL )
     {
         float arrTime;
-        Tim_ManIncrementTravId( p->pManTime );
+        Tim_ManIncrementTravId( (Tim_Man_t *)p->pManTime );
         Aig_ManSetPioNumbers( p );
         Aig_ManForEachObj( p, pObj, i )
         {
@@ -420,7 +424,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
                 pObj->pData = pObjNew;
                 pObjNew->pHaig = pObj->pHaig;
                 // set the arrival time of the new PI
-                arrTime = Tim_ManGetCiArrival( p->pManTime, Aig_ObjPioNum(pObj) );
+                arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pObj) );
                 pObjNew->Level = (int)arrTime;
             }
             else if ( Aig_ObjIsPo(pObj) )
@@ -431,7 +435,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
                 pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
                 // save arrival time of the output
                 arrTime = (float)Aig_Regular(pObjNew)->Level;
-                Tim_ManSetCoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime );
+                Tim_ManSetCoArrival( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pObj), arrTime );
                 // create PO
                 pObjNew = Aig_ObjCreatePo( pNew, pObjNew );
                 pObjNew->pHaig = pObj->pHaig;
@@ -440,7 +444,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
                 assert( 0 );
         }
         Aig_ManCleanPioNumbers( p );
-        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+        pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 );
     }
     else
     {
@@ -534,12 +538,12 @@ void Dar_BalancePrintStats( Aig_Man_t * p )
             continue;
         Vec_PtrClear( vSuper );
         Dar_BalanceCone_rec( pObj, pObj, vSuper );
-        Vec_PtrForEachEntry( vSuper, pTemp, k )
+        Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k )
             pTemp->fMarkB = 0;
         if ( Vec_PtrSize(vSuper) < 3 )
             continue;
         printf( "  %d(", Vec_PtrSize(vSuper) );
-        Vec_PtrForEachEntry( vSuper, pTemp, k )
+        Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pTemp, k )
             printf( " %d", pTemp->Level );
         printf( " )" );
     }
@@ -554,3 +558,5 @@ void Dar_BalancePrintStats( Aig_Man_t * p )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index 83b6e08e..9811757c 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -20,6 +20,9 @@
 
 #include "darInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -153,7 +156,13 @@ p->timeCuts += clock() - clk;
         p->GainBest = -1;
         Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : ABC_INFINITY;
         Dar_ObjForEachCut( pObj, pCut, k )
+        {
+            int nLeavesOld = pCut->nLeaves;
+            if ( pCut->nLeaves == 3 )
+                pCut->pLeaves[pCut->nLeaves++] = 0;
             Dar_LibEval( p, pObj, pCut, Required );
+            pCut->nLeaves = nLeavesOld; 
+        }
         // check the best gain
         if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
         {
@@ -308,3 +317,5 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/dar/darCut.c b/src/aig/dar/darCut.c
index 7f7b1b4c..b272b388 100644
--- a/src/aig/dar/darCut.c
+++ b/src/aig/dar/darCut.c
@@ -20,6 +20,9 @@
 
 #include "darInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -127,7 +130,7 @@ static inline int Dar_CutFindValue( Dar_Man_t * p, Dar_Cut_t * pCut )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the next ABC_FREE cut to use.]
+  Synopsis    [Returns the next free cut to use.]
 
   Description [Uses the cut with the smallest value.]
                
@@ -628,7 +631,7 @@ void Dar_ManCutsRestart( Dar_Man_t * p, Aig_Obj_t * pRoot )
     Aig_Obj_t * pObj;
     int i;
     Dar_ObjSetCuts( Aig_ManConst1(p->pAig), NULL );
-    Vec_PtrForEachEntry( p->vCutNodes, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, p->vCutNodes, pObj, i )
         if ( !Aig_ObjIsNone(pObj) )
             Dar_ObjSetCuts( pObj, NULL );
     Vec_PtrClear( p->vCutNodes );
@@ -745,3 +748,5 @@ Dar_Cut_t * Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/dar/darData.c b/src/aig/dar/darData.c
index e644c92b..17963c4a 100644
--- a/src/aig/dar/darData.c
+++ b/src/aig/dar/darData.c
@@ -20,6 +20,8 @@
 
 #include "darInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -11145,6 +11147,9 @@ Vec_Int_t * Dar_LibReadPrios()
 
 #include "abc.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /**Function*************************************************************
 
   Synopsis    [Generate arrays.]
@@ -11285,3 +11290,5 @@ void Aig_NtkGenerateArrays( Abc_Ntk_t * pNtk )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h
index 0f2e8894..70831534 100644
--- a/src/aig/dar/darInt.h
+++ b/src/aig/dar/darInt.h
@@ -21,6 +21,7 @@
 #ifndef __DAR_INT_H__
 #define __DAR_INT_H__
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -40,9 +41,10 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef __cplusplus
-extern "C" {
-#endif 
+
+
+ABC_NAMESPACE_HEADER_START
+ 
 
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
@@ -104,7 +106,7 @@ struct Dar_Man_t_
     int              time2;
 };
 
-static inline Dar_Cut_t *  Dar_ObjCuts( Aig_Obj_t * pObj )                         { return pObj->pData;    }
+static inline Dar_Cut_t *  Dar_ObjCuts( Aig_Obj_t * pObj )                         { return (Dar_Cut_t *)pObj->pData;    }
 static inline void         Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts )   { assert( !Aig_ObjIsNone(pObj) ); pObj->pData = pCuts;   }
 
 ////////////////////////////////////////////////////////////////////////
@@ -144,7 +146,6 @@ extern Vec_Int_t *     Dar_LibReadPrios();
 /*=== darLib.c ============================================================*/
 extern void            Dar_LibStart();
 extern void            Dar_LibStop();
-extern void            Dar_LibPrepare( int nSubgraphs );
 extern void            Dar_LibReturnCanonicals( unsigned * pCanons );
 extern void            Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
 extern Aig_Obj_t *     Dar_LibBuildBest( Dar_Man_t * p );
@@ -156,9 +157,11 @@ extern void            Dar_ManPrintStats( Dar_Man_t * p );
 extern char **         Dar_Permutations( int n );
 extern void            Dar_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap );
 
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
 
 #endif
 
diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c
index 7f9188e0..52fd36b3 100644
--- a/src/aig/dar/darLib.c
+++ b/src/aig/dar/darLib.c
@@ -19,6 +19,11 @@
 ***********************************************************************/
 
 #include "darInt.h"
+#include "gia.h"
+#include "dar.h"
+
+ABC_NAMESPACE_IMPL_START
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -41,7 +46,9 @@ struct Dar_LibObj_t_ // library object (2 words)
 
 struct Dar_LibDat_t_ // library object data
 {
+    union { 
     Aig_Obj_t *      pFunc;         // the corresponding AIG node if it exists
+    int              iGunc; };      // the corresponding AIG node if it exists
     int              Level;         // level of this node after it is constructured
     int              TravId;        // traversal ID of the library object data
     float            dProb;         // probability of the node being 1
@@ -184,6 +191,23 @@ void Dar_LibFree( Dar_Lib_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Dar_LibReturnClass( unsigned uTruth )
+{
+    return s_DarLib->pMap[uTruth & 0xffff];
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns canonical truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Dar_LibReturnCanonicals( unsigned * pCanons )
 {
     int Visits[222] = {0};
@@ -1005,14 +1029,310 @@ Aig_Obj_t * Dar_LibBuildBest( Dar_Man_t * p )
 {
     int i, Counter = 4;
     for ( i = 0; i < Vec_PtrSize(p->vLeavesBest); i++ )
-        s_DarLib->pDatas[i].pFunc = Vec_PtrEntry( p->vLeavesBest, i );
+        s_DarLib->pDatas[i].pFunc = (Aig_Obj_t *)Vec_PtrEntry( p->vLeavesBest, i );
     Dar_LibBuildClear_rec( Dar_LibObj(s_DarLib, p->OutBest), &Counter );
     return Dar_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, p->OutBest) );
 }
 
 
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Matches the cut with its canonical form.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar2_LibCutMatch( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth )
+{
+    unsigned uPhase;
+    char * pPerm;
+    int i;
+    assert( Vec_IntSize(vCutLits) == 4 );
+    // get the fanin permutation
+    uPhase = s_DarLib->pPhases[uTruth];
+    pPerm  = s_DarLib->pPerms4[ (int)s_DarLib->pPerms[uTruth] ];
+    // collect fanins with the corresponding permutation/phase
+    for ( i = 0; i < Vec_IntSize(vCutLits); i++ )
+    {
+//        pFanin = Gia_ManObj( p, pCut->pLeaves[ (int)pPerm[i] ] );
+//        pFanin = Gia_ManObj( p, Vec_IntEntry( vCutLits, (int)pPerm[i] ) );
+//        pFanin = Gia_ObjFromLit( p, Vec_IntEntry( vCutLits, (int)pPerm[i] ) );
+        s_DarLib->pDatas[i].iGunc = Gia_LitNotCond( Vec_IntEntry(vCutLits, (int)pPerm[i]), ((uPhase >> i) & 1) );
+        s_DarLib->pDatas[i].Level = Gia_ObjLevel( p, Gia_Regular(Gia_ObjFromLit(p, s_DarLib->pDatas[i].iGunc)) );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns numbers to the nodes of one class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar2_LibEvalAssignNums( Gia_Man_t * p, int Class )
+{
+    Dar_LibObj_t * pObj;
+    Dar_LibDat_t * pData, * pData0, * pData1;
+    int iFanin0, iFanin1, i, iLit;
+    for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ )
+    {
+        // get one class node, assign its temporary number and set its data
+        pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes0[Class][i]);
+        pObj->Num = 4 + i;
+        assert( (int)pObj->Num < s_DarLib->nNodes0Max + 4 );
+        pData = s_DarLib->pDatas + pObj->Num;
+        pData->fMffc = 0;
+        pData->iGunc = -1;
+        pData->TravId = 0xFFFF;
+
+        // explore the fanins
+        assert( (int)Dar_LibObj(s_DarLib, pObj->Fan0)->Num < s_DarLib->nNodes0Max + 4 );
+        assert( (int)Dar_LibObj(s_DarLib, pObj->Fan1)->Num < s_DarLib->nNodes0Max + 4 );
+        pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num;
+        pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num;
+        pData->Level = 1 + ABC_MAX(pData0->Level, pData1->Level);
+        if ( pData0->iGunc == -1 || pData1->iGunc == -1 )
+            continue;
+        iFanin0 = Gia_LitNotCond( pData0->iGunc, pObj->fCompl0 );
+        iFanin1 = Gia_LitNotCond( pData1->iGunc, pObj->fCompl1 );
+        // compute the resulting literal
+        if ( iFanin0 == 0 || iFanin1 == 0 || iFanin0 == Gia_LitNot(iFanin1) )
+            iLit = 0;
+        else if ( iFanin0 == 1 || iFanin0 == iFanin1 )
+            iLit = iFanin1;
+        else if ( iFanin1 == 1 )
+            iLit = iFanin0;
+        else
+        {
+            iLit = Gia_ManHashLookup( p, Gia_ObjFromLit(p, iFanin0), Gia_ObjFromLit(p, iFanin1) );
+            if ( iLit == 0 )
+                iLit = -1;
+        }
+        pData->iGunc = iLit;
+        if ( pData->iGunc >= 0 )
+        {
+            // update the level to be more accurate
+            pData->Level = Gia_ObjLevel( p, Gia_Regular(Gia_ObjFromLit(p, pData->iGunc)) );
+            // mark the node if it is part of MFFC
+//            pData->fMffc = Gia_ObjIsTravIdCurrentArray(p, Gia_Regular(pData->pGunc));
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluates one cut.]
+
+  Description [Returns the best gain.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar2_LibEval_rec( Dar_LibObj_t * pObj, int Out )
+{
+    Dar_LibDat_t * pData;
+    int Area;
+    pData = s_DarLib->pDatas + pObj->Num;
+    if ( pData->TravId == Out )
+        return 0;
+    pData->TravId = Out;
+    if ( pObj->fTerm )
+        return 0;
+    assert( pObj->Num > 3 );
+    if ( pData->iGunc >= 0 )//&& !pData->fMffc )
+        return 0;
+    // this is a new node - get a bound on the area of its branches
+//    nNodesSaved--;
+    Area = Dar2_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out );
+//    if ( Area > nNodesSaved )
+//        return 0xff;
+    Area += Dar2_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out );
+//    if ( Area > nNodesSaved )
+//        return 0xff;
+    return Area + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluates one cut.]
+
+  Description [Returns the best gain.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar2_LibEval( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth, int fKeepLevel, Vec_Int_t * vLeavesBest2 )
+{
+    int p_OutBest    = -1;
+    int p_OutNumBest = -1;
+    int p_LevelBest  =  1000000;
+    int p_GainBest   = -1000000;
+    int p_ClassBest  = -1;
+    int fTraining    =  0;
+    Dar_LibObj_t * pObj;
+    int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained, clk;
+    clk = clock();
+    assert( Vec_IntSize(vCutLits) == 4 );
+    assert( (uTruth >> 16) == 0 );
+    // check if the cut exits and assigns leaves and their levels
+    if ( !Dar2_LibCutMatch(p, vCutLits, uTruth) )
+        return -1;
+    // mark MFFC of the node
+//    nNodesSaved = Dar2_LibCutMarkMffc( p->pAig, pRoot, pCut->nLeaves, p->pPars->fPower? &PowerSaved : NULL );
+    nNodesSaved = 0;
+    // evaluate the cut
+    Class = s_DarLib->pMap[uTruth];
+    Dar2_LibEvalAssignNums( p, Class );
+    // profile outputs by their savings
+//    p->nTotalSubgs += s_DarLib->nSubgr0[Class];
+//    p->ClassSubgs[Class] += s_DarLib->nSubgr0[Class];
+    for ( Out = 0; Out < s_DarLib->nSubgr0[Class]; Out++ )
+    {
+        pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr0[Class][Out]);
+//        nNodesAdded = Dar2_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required, p->pPars->fPower? &PowerAdded : NULL );
+        nNodesAdded = Dar2_LibEval_rec( pObj, Out );
+        nNodesGained = nNodesSaved - nNodesAdded;
+        if ( fKeepLevel )
+        {
+            if ( s_DarLib->pDatas[pObj->Num].Level >  p_LevelBest || 
+                (s_DarLib->pDatas[pObj->Num].Level == p_LevelBest && nNodesGained <= p_GainBest) )
+                continue;
+        }
+        else
+        {
+            if ( nNodesGained <  p_GainBest || 
+                (nNodesGained == p_GainBest && s_DarLib->pDatas[pObj->Num].Level >= p_LevelBest) )
+                continue;
+        }
+        // remember this possibility
+        Vec_IntClear( vLeavesBest2 );
+        for ( k = 0; k < Vec_IntSize(vCutLits); k++ )
+            Vec_IntPush( vLeavesBest2, s_DarLib->pDatas[k].iGunc );
+        p_OutBest    = s_DarLib->pSubgr0[Class][Out];
+        p_OutNumBest = Out;
+        p_LevelBest  = s_DarLib->pDatas[pObj->Num].Level;
+        p_GainBest   = nNodesGained;
+        p_ClassBest  = Class;
+//        assert( p_LevelBest <= Required );
+    }
+//clk = clock() - clk;
+//p->ClassTimes[Class] += clk;
+//p->timeEval += clk;
+    assert( p_OutBest != -1 );
+    return p_OutBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Clears the fields of the nodes used i this cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar2_LibBuildClear_rec( Dar_LibObj_t * pObj, int * pCounter )
+{
+    if ( pObj->fTerm )
+        return;
+    pObj->Num = (*pCounter)++;
+    s_DarLib->pDatas[ pObj->Num ].iGunc = -1;
+    Dar2_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan0), pCounter );
+    Dar2_LibBuildClear_rec( Dar_LibObj(s_DarLib, pObj->Fan1), pCounter );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reconstructs the best cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar2_LibBuildBest_rec( Gia_Man_t * p, Dar_LibObj_t * pObj )
+{
+    Gia_Obj_t * pNode;
+    Dar_LibDat_t * pData;
+    int iFanin0, iFanin1;
+    pData = s_DarLib->pDatas + pObj->Num;
+    if ( pData->iGunc >= 0 )
+        return pData->iGunc;
+    iFanin0 = Dar2_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan0) );
+    iFanin1 = Dar2_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, pObj->Fan1) );
+    iFanin0 = Gia_LitNotCond( iFanin0, pObj->fCompl0 );
+    iFanin1 = Gia_LitNotCond( iFanin1, pObj->fCompl1 );
+    pData->iGunc = Gia_ManHashAnd( p, iFanin0, iFanin1 );
+    pNode = Gia_ManObj( p, Gia_Lit2Var(pData->iGunc) );
+    if ( Gia_ObjIsAnd( pNode ) )
+        Gia_ObjSetAndLevel( p, pNode );
+    Gia_ObjSetPhase( pNode );
+    return pData->iGunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reconstructs the best cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar2_LibBuildBest( Gia_Man_t * p, Vec_Int_t * vLeavesBest2, int OutBest )
+{
+    int i, iLeaf, Counter = 4;
+    assert( Vec_IntSize(vLeavesBest2) == 4 );
+    Vec_IntForEachEntry( vLeavesBest2, iLeaf, i )
+        s_DarLib->pDatas[i].iGunc = iLeaf;
+    Dar2_LibBuildClear_rec( Dar_LibObj(s_DarLib, OutBest), &Counter );
+    return Dar2_LibBuildBest_rec( p, Dar_LibObj(s_DarLib, OutBest) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluate and build the new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_LibEvalBuild( Gia_Man_t * p, Vec_Int_t * vCutLits, unsigned uTruth, int fKeepLevel, Vec_Int_t * vLeavesBest2 )
+{
+    int OutBest = Dar2_LibEval( p, vCutLits, uTruth, fKeepLevel, vLeavesBest2 );
+    return Dar2_LibBuildBest( p, vLeavesBest2, OutBest );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c
index b11d3175..59150103 100644
--- a/src/aig/dar/darMan.c
+++ b/src/aig/dar/darMan.c
@@ -20,6 +20,8 @@
 
 #include "darInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -127,9 +129,46 @@ void Dar_ManPrintStats( Dar_Man_t * p )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+#if 0
+
+ABC_NAMESPACE_IMPL_END
+
+#include "kit.h"
+
+ABC_NAMESPACE_IMPL_START
+
+void Dar_ManPrintScript()
+{
+    unsigned pCanons[222];
+    int i;
+    Dar_LibReturnCanonicals( pCanons );
+    for ( i = 1; i < 222; i++ )
+    {
+        Kit_DsdNtk_t * pNtk;
+        pNtk = Kit_DsdDecompose( pCanons + i, 4 );
+        printf( "    \"" );
+        Kit_DsdPrint( stdout, pNtk );
+        printf( "\",              /* %3d  */\n", i );
+        Kit_DsdNtkFree( pNtk );
+    }
+}
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/dar/darPrec.c b/src/aig/dar/darPrec.c
index 85a31dfc..4d164123 100644
--- a/src/aig/dar/darPrec.c
+++ b/src/aig/dar/darPrec.c
@@ -20,6 +20,9 @@
 
 #include "darInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -130,7 +133,7 @@ void Dar_Permutations_rec( char ** pRes, int nFact, int n, char Array[] )
 
   Description [The number of permutations in the array is n!. The number of
   entries in each permutation is n. Therefore, the resulting array is a 
-  two-dimentional array of the size: n! x n. To ABC_FREE the resulting array,
+  two-dimentional array of the size: n! x n. To free the resulting array,
   call ABC_FREE() on the pointer returned by this procedure.]
 
   SideEffects []
@@ -297,14 +300,10 @@ void Dar_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puP
     int i, k;
 
     nFuncs  = (1 << 16);
-    uCanons = ABC_ALLOC( unsigned short, nFuncs );
-    uPhases = ABC_ALLOC( char, nFuncs );
-    uPerms  = ABC_ALLOC( char, nFuncs );
-    uMap    = ABC_ALLOC( unsigned char, nFuncs );
-    memset( uCanons, 0, sizeof(unsigned short) * nFuncs );
-    memset( uPhases, 0, sizeof(char) * nFuncs );
-    memset( uPerms,  0, sizeof(char) * nFuncs );
-    memset( uMap,    0, sizeof(unsigned char) * nFuncs );
+    uCanons = ABC_CALLOC( unsigned short, nFuncs );
+    uPhases = ABC_CALLOC( char, nFuncs );
+    uPerms  = ABC_CALLOC( char, nFuncs );
+    uMap    = ABC_CALLOC( unsigned char, nFuncs );
     pPerms4 = Dar_Permutations( 4 );
 
     nClasses = 1;
@@ -330,11 +329,13 @@ void Dar_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puP
                     uCanons[uPerm] = uTruth;
                     uPhases[uPerm] = i;
                     uPerms[uPerm]  = k;
+                    uMap[uPerm]    = uMap[uTruth];
 
                     uPerm = ~uPerm & 0xFFFF;
                     uCanons[uPerm] = uTruth;
                     uPhases[uPerm] = i | 16;
                     uPerms[uPerm]  = k;
+                    uMap[uPerm]    = uMap[uTruth];
                 }
                 else
                     assert( uCanons[uPerm] == uTruth );
@@ -348,17 +349,21 @@ void Dar_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puP
                     uCanons[uPerm] = uTruth;
                     uPhases[uPerm] = i;
                     uPerms[uPerm]  = k;
+                    uMap[uPerm]    = uMap[uTruth];
 
                     uPerm = ~uPerm & 0xFFFF;
                     uCanons[uPerm] = uTruth;
                     uPhases[uPerm] = i | 16;
                     uPerms[uPerm]  = k;
+                    uMap[uPerm]    = uMap[uTruth];
                 }
                 else
                     assert( uCanons[uPerm] == uTruth );
             }
         }
     }
+    for ( uTruth = 1; uTruth < 0xffff; uTruth++ )
+        assert( uMap[uTruth] != 0 );
     uPhases[(1<<16)-1] = 16;
     assert( nClasses == 222 );
     ABC_FREE( pPerms4 );
@@ -385,3 +390,5 @@ void Dar_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puP
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index 5f6c5520..87e2d0da 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -24,6 +24,9 @@
 #include "bdc.h"
 #include "bdcInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -234,8 +237,8 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Ptr_t * vCut, K
     Kit_GraphForEachLeaf( pGraph, pNode, i )
     {
         pNode->pFunc = Vec_PtrEntry(vCut, i);
-        pNode->Level = Aig_Regular(pNode->pFunc)->Level;
-        assert( Aig_Regular(pNode->pFunc)->Level < (1<<24)-1 );
+        pNode->Level = Aig_Regular((Aig_Obj_t *)pNode->pFunc)->Level;
+        assert( Aig_Regular((Aig_Obj_t *)pNode->pFunc)->Level < (1<<24)-1 );
     }
 //printf( "Trying:\n" );
     // compute the AIG size after adding the internal nodes
@@ -246,8 +249,8 @@ int Dar_RefactTryGraph( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Ptr_t * vCut, K
         pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.Node );
         pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.Node );
         // get the AIG nodes corresponding to the children 
-        pAnd0 = pNode0->pFunc; 
-        pAnd1 = pNode1->pFunc; 
+        pAnd0 = (Aig_Obj_t *)pNode0->pFunc; 
+        pAnd1 = (Aig_Obj_t *)pNode1->pFunc; 
         if ( pAnd0 && pAnd1 )
         {
             // if they are both present, find the resulting node
@@ -320,13 +323,13 @@ Aig_Obj_t * Dar_RefactBuildGraph( Aig_Man_t * pAig, Vec_Ptr_t * vCut, Kit_Graph_
         pNode->pFunc = Vec_PtrEntry(vCut, i);
     // check for a literal
     if ( Kit_GraphIsVar(pGraph) )
-        return Aig_NotCond( Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
+        return Aig_NotCond( (Aig_Obj_t *)Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
     // build the AIG nodes corresponding to the AND gates of the graph
 //printf( "Building (current number %d):\n", Aig_ManObjNumMax(pAig) );
     Kit_GraphForEachNode( pGraph, pNode, i )
     {
-        pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
-        pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
+        pAnd0 = Aig_NotCond( (Aig_Obj_t *)Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
+        pAnd1 = Aig_NotCond( (Aig_Obj_t *)Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
         pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 );
 /*
 printf( "Checking " );
@@ -339,7 +342,7 @@ printf( "\n" );
 */
     }
     // complement the result if necessary
-    return Aig_NotCond( pNode->pFunc, Kit_GraphIsComplement(pGraph) );
+    return Aig_NotCond( (Aig_Obj_t *)pNode->pFunc, Kit_GraphIsComplement(pGraph) );
 }
 
 /**Function*************************************************************
@@ -473,7 +476,7 @@ int Dar_ObjCutLevelAchieved( Vec_Ptr_t * vCut, int nLevelMin )
 {
     Aig_Obj_t * pObj;
     int i;
-    Vec_PtrForEachEntry( vCut, pObj, i )
+    Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
         if ( !Aig_ObjIsPi(pObj) && (int)pObj->Level <= nLevelMin )
             return 1;
     return 0;
@@ -510,8 +513,8 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
 
     // resynthesize each node once
     clkStart = clock();
-    vCut = Vec_VecEntry( p->vCuts, 0 );
-    vCut2 = Vec_VecEntry( p->vCuts, 1 );
+    vCut = (Vec_Ptr_t *)Vec_VecEntry( p->vCuts, 0 );
+    vCut2 = (Vec_Ptr_t *)Vec_VecEntry( p->vCuts, 1 );
     p->nNodesInit = Aig_ManNodeNum(pAig);
     nNodesOld = Vec_PtrSize( pAig->vObjs );
 //    pProgress = Bar_ProgressStart( stdout, nNodesOld );
@@ -629,3 +632,5 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/dar/darResub.c b/src/aig/dar/darResub.c
index f819934e..44367207 100644
--- a/src/aig/dar/darResub.c
+++ b/src/aig/dar/darResub.c
@@ -20,6 +20,9 @@
 
 #include "darInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -46,3 +49,5 @@
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 20f3e14a..0332f961 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -23,12 +23,13 @@
 #include "gia.h"
 #include "giaAig.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-        extern void * Tim_ManDup( void * p, int fDiscrete );     
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -83,10 +84,11 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
 
     pParsRwr->fVerbose = fVerbose;
     pParsRef->fVerbose = fVerbose;
-
+//printf( "1" );
     pAig = Aig_ManDupDfs( pAig ); 
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
+//printf( "2" );
     // balance
     if ( fBalance )
     {
@@ -96,18 +98,21 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
     }
    
 //Aig_ManDumpBlif( pAig, "inter.blif", NULL, NULL );
+//printf( "3" );
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
     pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
+//printf( "4" );
     // refactor
     Dar_ManRefactor( pAig, pParsRef );
     pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
+//printf( "5" );
     // balance
     if ( fBalance )
     {
@@ -116,12 +121,14 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
     if ( fVerbose ) Aig_ManPrintStats( pAig );
     }
     
+//printf( "6" );
     // rewrite
     Dar_ManRewrite( pAig, pParsRwr );
     pAig = Aig_ManDupDfs( pTemp = pAig ); 
     Aig_ManStop( pTemp );
     if ( fVerbose ) Aig_ManPrintStats( pAig );
 
+//printf( "7" );
     return pAig;
 }
 
@@ -369,7 +376,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
     Vec_PtrPush( vAigs, pAig );
 //Aig_ManPrintStats( pAig );
 
-    pAig = Vec_PtrEntry( vAigs, 1 );
+    pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 1 );
     Aig_ManForEachObj( pAig, pObj, i )
         pObj->pHaig = pObj->pNext;
 
@@ -402,7 +409,7 @@ clk = clock();
     // (it is also important when constructing choices)
     if ( !fConstruct )
     {
-        pMan = Vec_PtrPop( vAigs );
+        pMan = (Aig_Man_t *)Vec_PtrPop( vAigs );
         Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
         Vec_PtrWriteEntry( vAigs, 0, pMan );
     }
@@ -416,7 +423,7 @@ clk = clock();
         pMan = Aig_ManChoiceConstructive( vAigs, fVerbose );
     else
         pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
-    Vec_PtrForEachEntry( vAigs, pTemp, i )
+    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
         Aig_ManStop( pTemp );
     Vec_PtrFree( vAigs );
 if ( fVerbose )
@@ -430,81 +437,6 @@ ABC_PRT( "Choicing time ", clock() - clk );
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates the AIG in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Dar_ManChoiceMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
-{
-    if ( ~pObj->Value )
-        return pObj->Value;
-    Dar_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin0(pObj) );
-    if ( Gia_ObjIsCo(pObj) )
-        return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-    Dar_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin1(pObj) );
-    return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-} 
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the miter of several AIGs for choice computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Man_t * Dar_ManChoiceMiter( Vec_Ptr_t * vGias )
-{
-    Gia_Man_t * pNew, * pGia, * pGia0;
-    int i, k, iNode, nNodes;
-    // make sure they have equal parameters
-    assert( Vec_PtrSize(vGias) > 0 );
-    pGia0 = Vec_PtrEntry( vGias, 0 );
-    Vec_PtrForEachEntry( vGias, pGia, i )
-    {
-        assert( Gia_ManCiNum(pGia)  == Gia_ManCiNum(pGia0) );
-        assert( Gia_ManCoNum(pGia)  == Gia_ManCoNum(pGia0) );
-        assert( Gia_ManRegNum(pGia) == Gia_ManRegNum(pGia0) );
-        Gia_ManFillValue( pGia );
-        Gia_ManConst0(pGia)->Value = 0;
-    }
-    // start the new manager
-    pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
-    pNew->pName = Gia_UtilStrsav( pGia0->pName );
-    // create new CIs and assign them to the old manager CIs
-    for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
-    {
-        iNode = Gia_ManAppendCi(pNew);
-        Vec_PtrForEachEntry( vGias, pGia, i )
-            Gia_ManCi( pGia, k )->Value = iNode; 
-    }
-    // create internal nodes
-    Gia_ManHashAlloc( pNew );
-    for ( k = 0; k < Gia_ManCoNum(pGia0); k++ )
-    {
-        Vec_PtrForEachEntry( vGias, pGia, i )
-            Dar_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) );
-    }
-    Gia_ManHashStop( pNew );
-    // check the presence of dangling nodes
-    nNodes = Gia_ManHasDandling( pNew );
-    assert( nNodes == 0 );
-    // finalize
-    Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia0) );
-    return pNew;
-}
-
-
-/**Function*************************************************************
-
   Synopsis    [Reproduces script "compress".]
 
   Description []
@@ -606,9 +538,9 @@ Aig_Man_t * Dar_NewCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel,
     {
         // rewrite
         //Dar_ManRewrite( pAig, pParsRwr );
-        pParsRwr->fUpdateLevel = 0;  // disable level update
+//        pParsRwr->fUpdateLevel = 0;  // disable level update  // this change was requested in July and later disabled
         Dar_ManRewrite( pAig, pParsRwr );
-        pParsRwr->fUpdateLevel = fUpdateLevel;  // reenable level update if needed
+//        pParsRwr->fUpdateLevel = fUpdateLevel;  // reenable level update if needed
 
         pAig = Aig_ManDupDfs( pTemp = pAig ); 
         Aig_ManStop( pTemp );
@@ -719,21 +651,21 @@ Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
     Aig_ManStop( pAig );
 
     // swap around the first and the last
-    pTemp = Vec_PtrPop( vGias );
+    pTemp = (Gia_Man_t *)Vec_PtrPop( vGias );
     Vec_PtrPush( vGias, Vec_PtrEntry(vGias,0) );
     Vec_PtrWriteEntry( vGias, 0, pTemp );
 
 //    Aig_Man_t * pAig;
 //    int i;
 //    printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) );
-//    Vec_PtrForEachEntry( p->vAigs, pAig, i )
+//    Vec_PtrForEachEntry( Aig_Man_t *, p->vAigs, pAig, i )
 //        Aig_ManPrintStats( pAig );
 
     // derive the miter
-    pGia = Dar_ManChoiceMiter( vGias );
+    pGia = Gia_ManChoiceMiter( vGias );
 
     // cleanup
-    Vec_PtrForEachEntry( vGias, pTemp, i )
+    Vec_PtrForEachEntry( Gia_Man_t *, vGias, pTemp, i )
         Gia_ManStop( pTemp );
     Vec_PtrFree( vGias );
     return pGia;
@@ -808,7 +740,7 @@ clk = clock();
     pMan->pSpec = Aig_UtilStrsav( pTemp->pSpec );
 
     // cleanup
-    Vec_PtrForEachEntry( vAigs, pTemp, i )
+    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
         Aig_ManStop( pTemp );
     Vec_PtrFree( vAigs );
 
@@ -834,7 +766,7 @@ if ( fVerbose )
 ***********************************************************************/
 Aig_Man_t * Dar_ManChoiceNewAig( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
-    extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
+//    extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
     extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
     int fVerbose = pPars->fVerbose;
     Aig_Man_t * pMan, * pTemp;
@@ -850,14 +782,14 @@ pPars->timeSynth = clock() - clk;
     // swap the first and last network
     // this should lead to the primary choice being "better" because of synthesis
     // (it is also important when constructing choices)
-    pMan = Vec_PtrPop( vAigs );
+    pMan = (Aig_Man_t *)Vec_PtrPop( vAigs );
     Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
     Vec_PtrWriteEntry( vAigs, 0, pMan );
 
     // derive the total AIG
     pMan = Dch_DeriveTotalAig( vAigs );
     // cleanup
-    Vec_PtrForEachEntry( vAigs, pTemp, i )
+    Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
         Aig_ManStop( pTemp );
     Vec_PtrFree( vAigs );
 
@@ -905,7 +837,7 @@ pPars->timeSynth = clock() - clk;
 Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
-    extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
+//    extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
     extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
     int fVerbose = pPars->fVerbose;
     Aig_Man_t * pMan, * pTemp;
@@ -922,7 +854,7 @@ Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 
     // perform synthesis
 clk = clock();
-    pGia = Dar_NewChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, pPars->fPower, pPars->fLightSynth, 0 );
+    pGia = Dar_NewChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
 pPars->timeSynth = clock() - clk;
 
     // perform choice computation
@@ -963,3 +895,5 @@ pPars->timeSynth = clock() - clk;
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/dar/dar_.c b/src/aig/dar/dar_.c
index 12fd7d17..323abed2 100644
--- a/src/aig/dar/dar_.c
+++ b/src/aig/dar/dar_.c
@@ -20,6 +20,9 @@
 
 #include "darInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -46,3 +49,5 @@
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+