14 files changed, 428 insertions, 62 deletions

diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index 8b49345e..02fcc21b 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -21,6 +21,7 @@
 #ifndef __MFS_H__
 #define __MFS_H__
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -29,9 +30,10 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
@@ -73,9 +75,11 @@ extern void        Abc_NtkMfsParsDefault( Mfs_Par_t * pPars );
 extern int         Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars );
 
  
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
 
 #endif
 
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index c598a19b..bda95d55 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -20,6 +20,9 @@
 
 #include "mfsInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -148,7 +151,7 @@ int Abc_NtkMfsPowerResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
 }
 */
 
-Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars)
+void Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars)
 {
     int i, k;
     Abc_Obj_t *pFanin, *pNode;
@@ -326,7 +329,7 @@ clk = clock();
 p->timeCnf += clock() - clk;
     // create the SAT problem
 clk = clock();
-    p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
+    p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
     if ( p->pSat && p->pPars->fOneHotness )
         Abc_NtkAddOneHotness( p );
     if ( p->pSat == NULL )
@@ -344,8 +347,8 @@ p->timeSat += clock() - clk;
     // minimize the local function of the node using bi-decomposition
     assert( p->nFanins == Abc_ObjFaninNum(pNode) );
     dProb = p->pPars->fPower? ((float *)p->vProbs->pArray)[pNode->Id] : -1.0;
-    pObj = Abc_NodeIfNodeResyn( p->pManDec, pNode->pNtk->pManFunc, pNode->pData, p->nFanins, p->vTruth, p->uCare, dProb );
-    nGain = Hop_DagSize(pNode->pData) - Hop_DagSize(pObj);
+    pObj = Abc_NodeIfNodeResyn( p->pManDec, (Hop_Man_t *)pNode->pNtk->pManFunc, (Hop_Obj_t *)pNode->pData, p->nFanins, p->vTruth, p->uCare, dProb );
+    nGain = Hop_DagSize((Hop_Obj_t *)pNode->pData) - Hop_DagSize(pObj);
     if ( nGain >= 0 )
     {
         p->nNodesDec++;
@@ -432,12 +435,12 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
     if ( pNtk->pExcare )
     {
         Abc_Ntk_t * pTemp;
-        if ( Abc_NtkPiNum(pNtk->pExcare) != Abc_NtkCiNum(pNtk) )
+        if ( Abc_NtkPiNum((Abc_Ntk_t *)pNtk->pExcare) != Abc_NtkCiNum(pNtk) )
             printf( "The PI count of careset (%d) and logic network (%d) differ. Careset is not used.\n",
-                Abc_NtkPiNum(pNtk->pExcare), Abc_NtkCiNum(pNtk) );
+                Abc_NtkPiNum((Abc_Ntk_t *)pNtk->pExcare), Abc_NtkCiNum(pNtk) );
         else
         {
-            pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
+            pTemp = Abc_NtkStrash( (Abc_Ntk_t *)pNtk->pExcare, 0, 0, 0 );
             p->pCare = Abc_NtkToDar( pTemp, 0, 0 );
             Abc_NtkDelete( pTemp );
             p->vSuppsInv = Aig_ManSupportsInverse( p->pCare );
@@ -513,7 +516,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
             p->nTotConfLevel = 0;
             p->nTimeOutsLevel = 0;
             clk2 = clock();
-            Vec_PtrForEachEntry( vNodes, pObj, i )
+            Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
             {
                 if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
                     break;
@@ -584,3 +587,5 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/mfs/mfsCore_.c b/src/opt/mfs/mfsCore_.c
index 66b497f6..69f64ae5 100644
--- a/src/opt/mfs/mfsCore_.c
+++ b/src/opt/mfs/mfsCore_.c
@@ -20,6 +20,9 @@
 
 #include "mfsInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -386,3 +389,5 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/mfs/mfsDiv.c b/src/opt/mfs/mfsDiv.c
index f5a07d31..1473580e 100644
--- a/src/opt/mfs/mfsDiv.c
+++ b/src/opt/mfs/mfsDiv.c
@@ -20,6 +20,9 @@
 
 #include "mfsInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -201,7 +204,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
 
     // count the number of PIs
     nTrueSupp = 0;
-    Vec_PtrForEachEntry( vCone, pObj, k )
+    Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pObj, k )
         nTrueSupp += Abc_ObjIsCi(pObj);
 //    printf( "%d(%d) ", Vec_PtrSize(p->vSupp), m );
 
@@ -221,7 +224,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
 
     // start collecting the divisors
     vDivs = Vec_PtrAlloc( p->pPars->nDivMax );
-    Vec_PtrForEachEntry( vCone, pObj, k )
+    Vec_PtrForEachEntry( Abc_Obj_t *, vCone, pObj, k )
     {
         if ( !Abc_NodeIsTravIdPrevious(pObj) )
             continue;
@@ -235,7 +238,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
 
     // explore the fanouts of already collected divisors
     if ( Vec_PtrSize(vDivs) < p->pPars->nDivMax )
-    Vec_PtrForEachEntry( vDivs, pObj, k )
+    Vec_PtrForEachEntry( Abc_Obj_t *, vDivs, pObj, k )
     {
         // consider fanouts of this node
         Abc_ObjForEachFanout( pObj, pFanout, f )
@@ -262,7 +265,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
             if ( m < Abc_ObjFaninNum(pFanout) )
                 continue;
             // make sure this divisor in not among the nodes
-//            Vec_PtrForEachEntry( p->vNodes, pFanin, m )
+//            Vec_PtrForEachEntry( Abc_Obj_t *, p->vNodes, pFanin, m )
 //                assert( pFanout != pFanin );
             // add the node to the divisors
             Vec_PtrPush( vDivs, pFanout );
@@ -278,7 +281,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
     }
 
     // sort the divisors by level in the increasing order
-    Vec_PtrSort( vDivs, Abc_NodeCompareLevelsIncrease );
+    Vec_PtrSort( vDivs, (int (*)(void))Abc_NodeCompareLevelsIncrease );
 
     // add the fanins of the node
     Abc_ObjForEachFanin( pNode, pFanin, k )
@@ -286,7 +289,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
 
 /*
     printf( "Node level = %d.  ", Abc_ObjLevel(p->pNode) );
-    Vec_PtrForEachEntryStart( vDivs, pObj, k, Vec_PtrSize(vDivs)-p->nDivsPlus )
+    Vec_PtrForEachEntryStart( Abc_Obj_t *, vDivs, pObj, k, Vec_PtrSize(vDivs)-p->nDivsPlus )
         printf( "%d ", Abc_ObjLevel(pObj) );
     printf( "\n" );
 */
@@ -301,3 +304,5 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/mfs/mfsGia.c b/src/opt/mfs/mfsGia.c
new file mode 100644
index 00000000..016b4ae2
--- /dev/null
+++ b/src/opt/mfs/mfsGia.c
@@ -0,0 +1,299 @@
+/**CFile****************************************************************
+
+  FileName    [mfsGia.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Experimental code based on the new AIG package.]
+
+  Author      [Alan Mishchenko]
+
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 29, 2009.]
+
+  Revision    [$Id: mfsGia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#include "mfsInt.h"
+#include "giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Gia_ObjChild0Copy( Aig_Obj_t * pObj )  { return Gia_LitNotCond( Aig_ObjFanin0(pObj)->iData, Aig_ObjFaninC0(pObj) ); }
+static inline int Gia_ObjChild1Copy( Aig_Obj_t * pObj )  { return Gia_LitNotCond( Aig_ObjFanin1(pObj)->iData, Aig_ObjFaninC1(pObj) ); }
+
+// r i10_if6.blif;  ps; mfs -v
+// r pj1_if6.blif;  ps; mfs -v
+// r x/01_if6.blif; ps; mfs -v
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the resubstitution miter as an GIA.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+Gia_Man_t * Gia_ManCreateResubMiter( Aig_Man_t * p )
+{
+    Gia_Man_t * pNew;//, * pTemp;
+    Aig_Obj_t * pObj;
+    int i, * pOuts0, * pOuts1;
+    Aig_ManSetPioNumbers( p );
+    // create the new manager
+    pNew = Gia_ManStart( Aig_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    // create the objects
+    pOuts0 = ABC_ALLOC( int, Aig_ManPoNum(p) );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsAnd(pObj) )
+            pObj->iData = Gia_ManHashAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
+        else if ( Aig_ObjIsPi(pObj) )
+            pObj->iData = Gia_ManAppendCi( pNew );
+        else if ( Aig_ObjIsPo(pObj) )
+            pOuts0[ Aig_ObjPioNum(pObj) ] = Gia_ObjChild0Copy(pObj);
+        else if ( Aig_ObjIsConst1(pObj) )
+            pObj->iData = 1;
+        else
+            assert( 0 );
+    }
+    // create the objects
+    pOuts1 = ABC_ALLOC( int, Aig_ManPoNum(p) );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsAnd(pObj) )
+            pObj->iData = Gia_ManHashAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
+        else if ( Aig_ObjIsPi(pObj) )
+            pObj->iData = Gia_ManAppendCi( pNew );
+        else if ( Aig_ObjIsPo(pObj) )
+            pOuts1[ Aig_ObjPioNum(pObj) ] = Gia_ObjChild0Copy(pObj);
+        else if ( Aig_ObjIsConst1(pObj) )
+            pObj->iData = 1;
+        else
+            assert( 0 );
+    }
+    // add the outputs
+    Gia_ManAppendCo( pNew, pOuts0[0] );
+    Gia_ManAppendCo( pNew, pOuts1[0] );
+    Gia_ManAppendCo( pNew, pOuts0[1] );
+    Gia_ManAppendCo( pNew, Gia_LitNot(pOuts1[1]) );
+    for ( i = 2; i < Aig_ManPoNum(p); i++ )
+        Gia_ManAppendCo( pNew, Gia_LitNot( Gia_ManHashXor(pNew, pOuts0[i], pOuts1[i]) ) );
+    Gia_ManHashStop( pNew );
+    ABC_FREE( pOuts0 );
+    ABC_FREE( pOuts1 );
+//    pNew = Gia_ManCleanup( pTemp = pNew );
+//    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMfsConstructGia( Mfs_Man_t * p )
+{
+    int nBTLimit = 500;
+    // prepare AIG
+    assert( p->pGia == NULL );
+    p->pGia = Gia_ManCreateResubMiter( p->pAigWin );
+    // prepare AIG
+    Gia_ManCreateRefs( p->pGia );
+    Gia_ManCleanMark0( p->pGia );
+    Gia_ManCleanMark1( p->pGia );
+    Gia_ManFillValue ( p->pGia ); // maps nodes into trail ids
+    Gia_ManCleanPhase( p->pGia ); 
+    // prepare solver
+    p->pTas = Tas_ManAlloc( p->pGia, nBTLimit );
+    p->vCex = Tas_ReadModel( p->pTas );
+    p->vGiaLits = Vec_PtrAlloc( 100 );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMfsDeconstructGia( Mfs_Man_t * p )
+{
+    assert( p->pGia != NULL );
+    Gia_ManStop( p->pGia ); p->pGia = NULL;
+    Tas_ManStop( p->pTas ); p->pTas = NULL;
+    Vec_PtrFree( p->vGiaLits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMfsResimulate( Gia_Man_t * p, Vec_Int_t * vCex )
+{
+    Gia_Obj_t * pObj;
+    int i, Entry;
+//    Gia_ManCleanMark1( p );
+    Gia_ManConst0(p)->fMark1 = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->fMark1 = 0;
+//        pObj->fMark1 = Gia_ManRandom(0);
+    Vec_IntForEachEntry( vCex, Entry, i )
+    {
+        pObj = Gia_ManCi( p, Gia_Lit2Var(Entry) );
+        pObj->fMark1 = !Gia_LitIsCompl(Entry);
+    }
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) & 
+                       (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->fMark1 =  Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj);
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsTryResubOnceGia( Mfs_Man_t * p, int * pCands, int nCands )
+{
+    int fVeryVerbose = 0;
+    int fUseGia = 1;
+    unsigned * pData;
+    int i, iVar, status, iOut, clk = clock();
+    p->nSatCalls++;
+//    return -1;
+    assert( p->pGia != NULL );
+    assert( p->pTas != NULL );
+    // convert to literals
+    Vec_PtrClear( p->vGiaLits );
+    // create the first four literals
+    Vec_PtrPush( p->vGiaLits, Gia_ObjChild0(Gia_ManPo(p->pGia, 0)) );
+    Vec_PtrPush( p->vGiaLits, Gia_ObjChild0(Gia_ManPo(p->pGia, 1)) );
+    Vec_PtrPush( p->vGiaLits, Gia_ObjChild0(Gia_ManPo(p->pGia, 2)) );
+    Vec_PtrPush( p->vGiaLits, Gia_ObjChild0(Gia_ManPo(p->pGia, 3)) );
+    for ( i = 0; i < nCands; i++ )
+    {
+        // get the output number
+        iOut = Gia_Lit2Var(pCands[i]) - 2 * p->pCnf->nVars;
+        // write the literal
+        Vec_PtrPush( p->vGiaLits, Gia_ObjChild0(Gia_ManPo(p->pGia, 4 + iOut)) );
+    }
+    // perform SAT solving
+    status = Tas_ManSolveArray( p->pTas, p->vGiaLits );
+    if ( status == -1 )
+    {
+        p->nTimeOuts++;
+        if ( fVeryVerbose )
+        printf( "t" );
+//        p->nSatUndec++;
+//        p->nConfUndec += p->Pars.nBTThis;
+//        Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
+//        p->timeSatUndec += clock() - clk;
+    }
+    else if ( status == 1 )
+    {
+        if ( fVeryVerbose )
+        printf( "u" );
+//        p->nSatUnsat++;
+//        p->nConfUnsat += p->Pars.nBTThis;
+//        p->timeSatUnsat += clock() - clk;
+    }
+    else
+    {
+        p->nSatCexes++;
+        if ( fVeryVerbose )
+        printf( "s" );
+//        p->nSatSat++;
+//        p->nConfSat += p->Pars.nBTThis;
+//        Gia_SatVerifyPattern( pAig, pRoot, vCex, vVisit );
+//        Cec_ManSatAddToStore( vCexStore, vCex, i );
+//        p->timeSatSat += clock() - clk;
+
+        // resimulate the counter-example
+        Abc_NtkMfsResimulate( p->pGia, Tas_ReadModel(p->pTas) );
+   
+        if ( fUseGia )
+        {
+/*
+            int Val0 = Gia_ManPo(p->pGia, 0)->fMark1;
+            int Val1 = Gia_ManPo(p->pGia, 1)->fMark1;
+            int Val2 = Gia_ManPo(p->pGia, 2)->fMark1;
+            int Val3 = Gia_ManPo(p->pGia, 3)->fMark1;
+            assert( Val0 == 1 );
+            assert( Val1 == 1 );
+            assert( Val2 == 1 );
+            assert( Val3 == 1 );
+*/
+            // store the counter-example
+            Vec_IntForEachEntry( p->vProjVars, iVar, i )
+            {
+                pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
+                iOut = iVar - 2 * p->pCnf->nVars;
+//                if ( !Gia_ManPo( p->pGia, 4 + iOut )->fMark1 ) // remove 0s!!!
+                if ( Gia_ManPo( p->pGia, 4 + iOut )->fMark1 ) // remove 0s!!!  - rememeber complemented attribute
+                {
+                    assert( Aig_InfoHasBit(pData, p->nCexes) );
+                    Aig_InfoXorBit( pData, p->nCexes );
+                }
+            }
+            p->nCexes++;
+        }
+
+    }
+    return status;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 8adffd44..5611afa0 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -21,6 +21,7 @@
 #ifndef __MFS_INT_H__
 #define __MFS_INT_H__
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -38,9 +39,10 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
 
 #define MFS_FANIN_MAX   12
 
@@ -168,9 +170,11 @@ extern void             Abc_NtkMfsConstructGia( Mfs_Man_t * p );
 extern void             Abc_NtkMfsDeconstructGia( Mfs_Man_t * p );
 extern int              Abc_NtkMfsTryResubOnceGia( Mfs_Man_t * p, int * pCands, int nCands );
 
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
 
 #endif
 
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index 9cacd021..1b3f2415 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -21,6 +21,9 @@
 #include "mfsInt.h"
 #include "kit.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -94,7 +97,7 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
 
     // collect the outputs of the divisors
     Vec_IntClear( p->vProjVars );
-    Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) )
+    Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) )
     {
         assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
         Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] );
@@ -246,7 +249,7 @@ unsigned * Abc_NtkMfsInterplateTruth( Mfs_Man_t * p, int * pCands, int nCands, i
         return NULL;
     }
     // get the learned clauses
-    pCnf = sat_solver_store_release( pSat );
+    pCnf = (Sto_Man_t *)sat_solver_store_release( pSat );
     sat_solver_delete( pSat );
 
     // set the global variables
@@ -349,7 +352,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
 //printf( "%d\n", pSat->stats.conflicts );
 //    ABC_PRT( "S", clock() - clk );
     // get the learned clauses
-    pCnf = sat_solver_store_release( pSat );
+    pCnf = (Sto_Man_t *)sat_solver_store_release( pSat );
     sat_solver_delete( pSat );
 
     // set the global variables
@@ -369,7 +372,7 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
 
     // transform interpolant into AIG
     pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
-    pFunc = Kit_GraphToHop( p->pNtk->pManFunc, pGraph );
+    pFunc = Kit_GraphToHop( (Hop_Man_t *)p->pNtk->pManFunc, pGraph );
     Kit_GraphFree( pGraph );
     return pFunc;
 }
@@ -379,3 +382,5 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 96a43368..74889c45 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -20,6 +20,9 @@
 
 #include "mfsInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -210,3 +213,5 @@ void Mfs_ManStop( Mfs_Man_t * p )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index 49ce6901..38004089 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -20,6 +20,9 @@
 
 #include "mfsInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -46,7 +49,7 @@ void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFani
     // create the new node
     pObjNew = Abc_NtkCreateNode( pObj->pNtk );
     pObjNew->pData = pFunc;
-    Vec_PtrForEachEntry( vFanins, pFanin, k )
+    Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pFanin, k )
         Abc_ObjAddFanin( pObjNew, pFanin );
     // replace the old node by the new node
 //printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
@@ -136,7 +139,7 @@ p->timeGia += clock() - clk;
     // store the counter-example
     Vec_IntForEachEntry( p->vProjVars, iVar, i )
     {
-        pData = Vec_PtrEntry( p->vDivCexes, i );
+        pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
         if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!!
         {
             assert( Aig_InfoHasBit(pData, p->nCexes) );
@@ -238,7 +241,7 @@ p->timeInt += clock() - clk;
             printf( "%3d: %2d ", p->nCexes, iVar );
             for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
             {
-                pData = Vec_PtrEntry( p->vDivCexes, i );
+                pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
                 printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) );
             }
             printf( "\n" );
@@ -251,12 +254,12 @@ p->timeInt += clock() - clk;
         {
             if ( p->pPars->fPower )
             {
-                Abc_Obj_t * pDiv = Vec_PtrEntry(p->vDivs, iVar);
+                Abc_Obj_t * pDiv = (Abc_Obj_t *)Vec_PtrEntry(p->vDivs, iVar);
                 // only accept the divisor if it is "cool"
                 if ( Abc_MfsObjProb(p, pDiv) >= 0.15 )
                     continue;
             }
-            pData  = Vec_PtrEntry( p->vDivCexes, iVar );
+            pData  = (unsigned *)Vec_PtrEntry( p->vDivCexes, iVar );
             for ( w = 0; w < nWords; w++ )
                 if ( pData[w] != ~0 )
                     break;
@@ -383,7 +386,7 @@ p->timeInt += clock() - clk;
             printf( "%3d: %2d %2d ", p->nCexes, iVar, iVar2 );
             for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
             {
-                pData = Vec_PtrEntry( p->vDivCexes, i );
+                pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
                 printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) );
             }
             printf( "\n" );
@@ -395,11 +398,11 @@ p->timeInt += clock() - clk;
         fBreak = 0;
         for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
         {
-            pData  = Vec_PtrEntry( p->vDivCexes, iVar );
+            pData  = (unsigned *)Vec_PtrEntry( p->vDivCexes, iVar );
 #if 1  // sjang
             if ( p->pPars->fPower )
             {
-                Abc_Obj_t * pDiv = Vec_PtrEntry(p->vDivs, iVar);
+                Abc_Obj_t * pDiv = (Abc_Obj_t *)Vec_PtrEntry(p->vDivs, iVar);
                 // only accept the divisor if it is "cool"
                 if ( Abc_MfsObjProb(p, pDiv) >= 0.12 )
                     continue;
@@ -407,11 +410,11 @@ p->timeInt += clock() - clk;
 #endif
             for ( iVar2 = 0; iVar2 < iVar; iVar2++ )
             {
-                pData2 = Vec_PtrEntry( p->vDivCexes, iVar2 );
+                pData2 = (unsigned *)Vec_PtrEntry( p->vDivCexes, iVar2 );
 #if 1 // sjang
                 if ( p->pPars->fPower )
                 {
-                    Abc_Obj_t * pDiv = Vec_PtrEntry(p->vDivs, iVar2);
+                    Abc_Obj_t * pDiv = (Abc_Obj_t *)Vec_PtrEntry(p->vDivs, iVar2);
                     // only accept the divisor if it is "cool"
                     if ( Abc_MfsObjProb(p, pDiv) >= 0.12 )
                         continue;
@@ -607,3 +610,5 @@ int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/mfs/mfsResub_.c b/src/opt/mfs/mfsResub_.c
index 47600b30..bca1285d 100644
--- a/src/opt/mfs/mfsResub_.c
+++ b/src/opt/mfs/mfsResub_.c
@@ -20,6 +20,9 @@
 
 #include "mfsInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -558,3 +561,5 @@ int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c
index eab80c53..c5806f2a 100644
--- a/src/opt/mfs/mfsSat.c
+++ b/src/opt/mfs/mfsSat.c
@@ -20,6 +20,9 @@
 
 #include "mfsInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -95,7 +98,7 @@ int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
     int RetValue, i;
     // collect projection variables
     Vec_IntClear( p->vProjVars );
-    Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) )
+    Vec_PtrForEachEntryStart( Aig_Obj_t *, p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) )
     {
         assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
         Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] );
@@ -175,3 +178,5 @@ int Abc_NtkAddOneHotness( Mfs_Man_t * p )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c
index 7e6c25da..a5c7b987 100644
--- a/src/opt/mfs/mfsStrash.c
+++ b/src/opt/mfs/mfsStrash.c
@@ -20,6 +20,8 @@
 
 #include "mfsInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -47,7 +49,7 @@ void Abc_MfsConvertAigToHop_rec( Aig_Obj_t * pObj, Hop_Man_t * pHop )
     Abc_MfsConvertAigToHop_rec( Aig_ObjFanin0(pObj), pHop ); 
     Abc_MfsConvertAigToHop_rec( Aig_ObjFanin1(pObj), pHop );
     pObj->pData = Hop_And( pHop, (Hop_Obj_t *)Aig_ObjChild0Copy(pObj), (Hop_Obj_t *)Aig_ObjChild1Copy(pObj) ); 
-    assert( !Hop_IsComplement(pObj->pData) );
+    assert( !Hop_IsComplement((Hop_Obj_t *)pObj->pData) );
 }
 
 /**Function*************************************************************
@@ -77,7 +79,7 @@ Hop_Obj_t * Abc_MfsConvertAigToHop( Aig_Man_t * pMan, Hop_Man_t * pHop )
         pObj->pData = Hop_IthVar( pHop, i );
     // construct the AIG
     Abc_MfsConvertAigToHop_rec( Aig_ObjFanin0(pRoot), pHop );
-    return Hop_NotCond( Aig_ObjFanin0(pRoot)->pData, Aig_ObjFaninC0(pRoot) );
+    return Hop_NotCond( (Hop_Obj_t *)Aig_ObjFanin0(pRoot)->pData, Aig_ObjFaninC0(pRoot) );
 }
 
 // should be called as follows:   pNodeNew->pData = Abc_MfsConvertAigToHop( pAigManInterpol, pNodeNew->pNtk->pManFunc );
@@ -123,8 +125,8 @@ void Abc_MfsConvertHopToAig( Abc_Obj_t * pObjOld, Aig_Man_t * pMan )
     Abc_Obj_t * pFanin;
     int i;
     // get the local AIG
-    pHopMan = pObjOld->pNtk->pManFunc;
-    pRoot = pObjOld->pData;
+    pHopMan = (Hop_Man_t *)pObjOld->pNtk->pManFunc;
+    pRoot = (Hop_Obj_t *)pObjOld->pData;
     // check the case of a constant
     if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
     {
@@ -138,7 +140,7 @@ void Abc_MfsConvertHopToAig( Abc_Obj_t * pObjOld, Aig_Man_t * pMan )
         Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy;
     // construct the AIG
     Abc_MfsConvertHopToAig_rec( Hop_Regular(pRoot), pMan );
-    pObjOld->pCopy = (Abc_Obj_t *)Aig_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  
+    pObjOld->pCopy = (Abc_Obj_t *)Aig_NotCond( (Aig_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  
     Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
 
     // assign the fanin nodes
@@ -146,7 +148,7 @@ void Abc_MfsConvertHopToAig( Abc_Obj_t * pObjOld, Aig_Man_t * pMan )
         Hop_ManPi(pHopMan, i)->pData = pFanin->pNext;
     // construct the AIG
     Abc_MfsConvertHopToAig_rec( Hop_Regular(pRoot), pMan );
-    pObjOld->pNext = (Abc_Obj_t *)Aig_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  
+    pObjOld->pNext = (Abc_Obj_t *)Aig_NotCond( (Aig_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  
     Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
 }
 
@@ -167,11 +169,11 @@ Aig_Obj_t * Abc_NtkConstructAig_rec( Mfs_Man_t * p, Abc_Obj_t * pNode, Aig_Man_t
     Abc_Obj_t * pObj;
     int i;
     // assign AIG nodes to the leaves
-    Vec_PtrForEachEntry( p->vSupp, pObj, i )
+    Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pObj, i )
         pObj->pCopy = pObj->pNext = (Abc_Obj_t *)Aig_ObjCreatePi( pMan );
     // strash intermediate nodes
     Abc_NtkIncrementTravId( pNode->pNtk );
-    Vec_PtrForEachEntry( p->vNodes, pObj, i )
+    Vec_PtrForEachEntry( Abc_Obj_t *, p->vNodes, pObj, i )
     {
         Abc_MfsConvertHopToAig( pObj, pMan );
         if ( pObj == pNode )
@@ -179,7 +181,7 @@ Aig_Obj_t * Abc_NtkConstructAig_rec( Mfs_Man_t * p, Abc_Obj_t * pNode, Aig_Man_t
     }
     // create the observability condition
     pRoot = Aig_ManConst0(pMan);
-    Vec_PtrForEachEntry( p->vRoots, pObj, i )
+    Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
     {
         pExor = Aig_Exor( pMan, (Aig_Obj_t *)pObj->pCopy, (Aig_Obj_t *)pObj->pNext );
         pRoot = Aig_Or( pMan, pRoot, pExor );
@@ -202,19 +204,19 @@ Aig_Obj_t * Abc_NtkConstructCare_rec( Aig_Man_t * pCare, Aig_Obj_t * pObj, Aig_M
 {
     Aig_Obj_t * pObj0, * pObj1;
     if ( Aig_ObjIsTravIdCurrent( pCare, pObj ) )
-        return pObj->pData;
+        return (Aig_Obj_t *)pObj->pData;
     Aig_ObjSetTravIdCurrent( pCare, pObj );
     if ( Aig_ObjIsPi(pObj) )
-        return pObj->pData = NULL;
+        return (Aig_Obj_t *)(pObj->pData = NULL);
     pObj0 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin0(pObj), pMan );
     if ( pObj0 == NULL )
-        return pObj->pData = NULL;
+        return (Aig_Obj_t *)(pObj->pData = NULL);
     pObj1 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin1(pObj), pMan );
     if ( pObj1 == NULL )
-        return pObj->pData = NULL;
+        return (Aig_Obj_t *)(pObj->pData = NULL);
     pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) );
     pObj1 = Aig_NotCond( pObj1, Aig_ObjFaninC1(pObj) );
-    return pObj->pData = Aig_And( pMan, pObj0, pObj1 );
+    return (Aig_Obj_t *)(pObj->pData = Aig_And( pMan, pObj0, pObj1 ));
 }
 
 /**Function*************************************************************
@@ -245,16 +247,16 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
     {
         // mark the care set
         Aig_ManIncrementTravId( p->pCare );
-        Vec_PtrForEachEntry( p->vSupp, pFanin, i )
+        Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pFanin, i )
         {
             pPi = Aig_ManPi( p->pCare, (int)(ABC_PTRUINT_T)pFanin->pData );
             Aig_ObjSetTravIdCurrent( p->pCare, pPi );
             pPi->pData = pFanin->pCopy;
         }
         // construct the constraints
-        Vec_PtrForEachEntry( p->vSupp, pFanin, i )
+        Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pFanin, i )
         {
-            vOuts = Vec_PtrEntry( p->vSuppsInv, (int)(ABC_PTRUINT_T)pFanin->pData );
+            vOuts = (Vec_Int_t *)Vec_PtrEntry( p->vSuppsInv, (int)(ABC_PTRUINT_T)pFanin->pData );
             Vec_IntForEachEntry( vOuts, iOut, k )
             {
                 pPo = Aig_ManPo( p->pCare, iOut );
@@ -290,7 +292,7 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
         pObjAig = (Aig_Obj_t *)pNode->pCopy;
         Aig_ObjCreatePo( pMan, pObjAig );
         // construct the divisors
-        Vec_PtrForEachEntry( p->vDivs, pFanin, i )
+        Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pFanin, i )
         {
             pObjAig = (Aig_Obj_t *)pFanin->pCopy;
             Aig_ObjCreatePo( pMan, pObjAig );
@@ -332,7 +334,7 @@ Aig_Man_t * Abc_NtkAigForConstraints( Mfs_Man_t * p, Abc_Obj_t * pNode )
     pMan = Aig_ManStart( 1000 );
     // mark the care set
     Aig_ManIncrementTravId( p->pCare );
-    Vec_PtrForEachEntry( p->vSupp, pFanin, i )
+    Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pFanin, i )
     {
         pPi = Aig_ManPi( p->pCare, (int)(ABC_PTRUINT_T)pFanin->pData );
         Aig_ObjSetTravIdCurrent( p->pCare, pPi );
@@ -340,9 +342,9 @@ Aig_Man_t * Abc_NtkAigForConstraints( Mfs_Man_t * p, Abc_Obj_t * pNode )
     }
     // construct the constraints
     pObjRoot = Aig_ManConst1(pMan);
-    Vec_PtrForEachEntry( p->vSupp, pFanin, i )
+    Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pFanin, i )
     {
-        vOuts = Vec_PtrEntry( p->vSuppsInv, (int)(ABC_PTRUINT_T)pFanin->pData );
+        vOuts = (Vec_Int_t *)Vec_PtrEntry( p->vSuppsInv, (int)(ABC_PTRUINT_T)pFanin->pData );
         Vec_IntForEachEntry( vOuts, iOut, k )
         {
             pPo = Aig_ManPo( p->pCare, iOut );
@@ -363,8 +365,13 @@ Aig_Man_t * Abc_NtkAigForConstraints( Mfs_Man_t * p, Abc_Obj_t * pNode )
     return pMan;
 }
 
+ABC_NAMESPACE_IMPL_END
+
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /**Function*************************************************************
 
   Synopsis    [Compute the ratio of don't-cares.]
@@ -395,3 +402,5 @@ double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/mfs/mfsWin.c b/src/opt/mfs/mfsWin.c
index e3e5e24e..2ed996be 100644
--- a/src/opt/mfs/mfsWin.c
+++ b/src/opt/mfs/mfsWin.c
@@ -20,6 +20,9 @@
 
 #include "mfsInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -110,3 +113,5 @@ Vec_Ptr_t * Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutL
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/mfs/mfs_.c b/src/opt/mfs/mfs_.c
index 32caf7ff..2682fa42 100644
--- a/src/opt/mfs/mfs_.c
+++ b/src/opt/mfs/mfs_.c
@@ -20,6 +20,9 @@
 
 #include "mfsInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -45,3 +48,5 @@
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+