Version abc90215

6 files changed, 57 insertions, 57 deletions

diff --git a/src/opt/res/res.h b/src/opt/res/res.h
index 3c3431bf..88d985a3 100644
--- a/src/opt/res/res.h
+++ b/src/opt/res/res.h
@@ -21,10 +21,6 @@
 #ifndef __RES_H__
 #define __RES_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -33,6 +29,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index a19a1573..cce3b48a 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -93,7 +93,7 @@ extern int s_ResynTime;
 Res_Man_t * Res_ManAlloc( Res_Par_t * pPars )
 {
     Res_Man_t * p;
-    p = ALLOC( Res_Man_t, 1 );
+    p = ABC_ALLOC( Res_Man_t, 1 );
     memset( p, 0, sizeof(Res_Man_t) );
     assert( pPars->nWindow > 0 && pPars->nWindow < 100 );
     assert( pPars->nCands > 0 && pPars->nCands < 100 );
@@ -143,18 +143,18 @@ void Res_ManFree( Res_Man_t * p )
         printf( "Proved = %d.", p->nProvedSets );
         printf( "\n" );
 
-        PRTP( "Windowing  ", p->timeWin,      p->timeTotal );
-        PRTP( "Divisors   ", p->timeDiv,      p->timeTotal );
-        PRTP( "Strashing  ", p->timeAig,      p->timeTotal );
-        PRTP( "Simulation ", p->timeSim,      p->timeTotal );
-        PRTP( "Candidates ", p->timeCand,     p->timeTotal );
-        PRTP( "SAT solver ", p->timeSatTotal, p->timeTotal );
-        PRTP( "    sat    ", p->timeSatSat,   p->timeTotal );
-        PRTP( "    unsat  ", p->timeSatUnsat, p->timeTotal );
-        PRTP( "    simul  ", p->timeSatSim,   p->timeTotal );
-        PRTP( "Interpol   ", p->timeInt,      p->timeTotal );
-        PRTP( "Undating   ", p->timeUpd,      p->timeTotal );
-        PRTP( "TOTAL      ", p->timeTotal,    p->timeTotal );
+        ABC_PRTP( "Windowing  ", p->timeWin,      p->timeTotal );
+        ABC_PRTP( "Divisors   ", p->timeDiv,      p->timeTotal );
+        ABC_PRTP( "Strashing  ", p->timeAig,      p->timeTotal );
+        ABC_PRTP( "Simulation ", p->timeSim,      p->timeTotal );
+        ABC_PRTP( "Candidates ", p->timeCand,     p->timeTotal );
+        ABC_PRTP( "SAT solver ", p->timeSatTotal, p->timeTotal );
+        ABC_PRTP( "    sat    ", p->timeSatSat,   p->timeTotal );
+        ABC_PRTP( "    unsat  ", p->timeSatUnsat, p->timeTotal );
+        ABC_PRTP( "    simul  ", p->timeSatSim,   p->timeTotal );
+        ABC_PRTP( "Interpol   ", p->timeInt,      p->timeTotal );
+        ABC_PRTP( "Undating   ", p->timeUpd,      p->timeTotal );
+        ABC_PRTP( "TOTAL      ", p->timeTotal,    p->timeTotal );
     }
     Res_WinFree( p->pWin );
     if ( p->pAig ) Abc_NtkDelete( p->pAig );
@@ -165,7 +165,7 @@ void Res_ManFree( Res_Man_t * p )
     Vec_VecFree( p->vResubs );
     Vec_VecFree( p->vResubsW );
     Vec_VecFree( p->vLevels );
-    free( p );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h
index 5aae46cc..172b5369 100644
--- a/src/opt/res/resInt.h
+++ b/src/opt/res/resInt.h
@@ -21,10 +21,6 @@
 #ifndef __RES_INT_H__
 #define __RES_INT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -35,6 +31,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c
index 798e7abc..d5983942 100644
--- a/src/opt/res/resSat.c
+++ b/src/opt/res/resSat.c
@@ -63,50 +63,50 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
 
     // assign unique numbers to each node
     nNodes = 0;
-    Abc_AigConst1(pAig)->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+    Abc_AigConst1(pAig)->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
     Abc_NtkForEachPi( pAig, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
     Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
 
     // start the solver
     pSat = sat_solver_new();
     sat_solver_store_alloc( pSat );
 
     // add clause for the constant node
-    Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
+    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
     // add clauses for AND gates
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        Res_SatAddAnd( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 
-            (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(PORT_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+        Res_SatAddAnd( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
+            (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
     Vec_PtrFree( vNodes );
     // add clauses for POs
     Vec_PtrForEachEntry( vFanins, pObj, i )
-        Res_SatAddEqual( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 
-            (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+        Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
+            (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
     // add trivial clauses
     pObj = Vec_PtrEntry(vFanins, 0);
-    Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 0 ); // care-set
+    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // care-set
     pObj = Vec_PtrEntry(vFanins, 1);
-    Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 0 ); // on-set
+    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // on-set
 
     // bookmark the clauses of A
     sat_solver_store_mark_clauses_a( pSat );
 
     // duplicate the clauses
     pObj = Vec_PtrEntry(vFanins, 1);
-    Sat_SolverDoubleClauses( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy );
+    Sat_SolverDoubleClauses( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy );
     // add the equality constraints
     Vec_PtrForEachEntryStart( vFanins, pObj, i, 2 )
-        Res_SatAddEqual( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, ((int)(PORT_PTRUINT_T)pObj->pCopy) + nNodes, 0 );
+        Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, ((int)(ABC_PTRUINT_T)pObj->pCopy) + nNodes, 0 );
 
     // bookmark the roots
     sat_solver_store_mark_roots( pSat );
 
     // solve the problem
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
+    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( status == l_False )
     {
         pCnf = sat_solver_store_release( pSat );
@@ -155,39 +155,39 @@ void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, int fOnSet )
 
     // assign unique numbers to each node
     nNodes = 0;
-    Abc_AigConst1(pAig)->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+    Abc_AigConst1(pAig)->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
     Abc_NtkForEachPi( pAig, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
     Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
-        pObj->pCopy = (void *)(PORT_PTRUINT_T)nNodes++;
+        pObj->pCopy = (void *)(ABC_PTRUINT_T)nNodes++;
 
     // start the solver
     pSat = sat_solver_new();
 
     // add clause for the constant node
-    Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
+    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)Abc_AigConst1(pAig)->pCopy, 0 );
     // add clauses for AND gates
     Vec_PtrForEachEntry( vNodes, pObj, i )
-        Res_SatAddAnd( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 
-            (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(PORT_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+        Res_SatAddAnd( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
+            (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, (int)(ABC_PTRUINT_T)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
     Vec_PtrFree( vNodes );
     // add clauses for the first PO
     pObj = Abc_NtkPo( pAig, 0 );
-    Res_SatAddEqual( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 
-        (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+    Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
+        (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
     // add clauses for the second PO
     pObj = Abc_NtkPo( pAig, 1 );
-    Res_SatAddEqual( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 
-        (int)(PORT_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+    Res_SatAddEqual( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 
+        (int)(ABC_PTRUINT_T)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
 
     // add trivial clauses
     pObj = Abc_NtkPo( pAig, 0 );
-    Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, 0 ); // care-set
+    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, 0 ); // care-set
 
     pObj = Abc_NtkPo( pAig, 1 );
-    Res_SatAddConst1( pSat, (int)(PORT_PTRUINT_T)pObj->pCopy, !fOnSet ); // on-set
+    Res_SatAddConst1( pSat, (int)(ABC_PTRUINT_T)pObj->pCopy, !fOnSet ); // on-set
 
     Vec_PtrFree( vFanins );
     return pSat;
@@ -218,7 +218,7 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
 //printf( "Looking for %s:  ", fOnSet? "onset " : "offset" );
 
     // decide what problem should be solved
-    Lit = toLitCond( (int)(PORT_PTRUINT_T)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
+    Lit = toLitCond( (int)(ABC_PTRUINT_T)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
     if ( fOnSet )
     {
         iPat = p->nPats1;
@@ -254,8 +254,8 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
     for ( k = iPat; k < nPatsLimit; k++ )
     {
         // solve with the assumption
-//        status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
-        status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
+//        status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+        status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)10000, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
         if ( status == l_False )
         {
 //printf( "Const %d\n", !fOnSet );
@@ -275,7 +275,7 @@ int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
             Vec_IntClear( vLits );
             for ( i = 0; i < p->nTruePis; i++ )
             {
-                Var = (int)(PORT_PTRUINT_T)Abc_NtkPi(p->pAig,i)->pCopy;
+                Var = (int)(ABC_PTRUINT_T)Abc_NtkPi(p->pAig,i)->pCopy;
                 value = (int)(pSat->model.ptr[Var] == l_True);
                 if ( value )
                     Abc_InfoSetBit( Vec_PtrEntry(vPats, i), k );
diff --git a/src/opt/res/resSim.c b/src/opt/res/resSim.c
index 5c1dd2b6..59b2b6ea 100644
--- a/src/opt/res/resSim.c
+++ b/src/opt/res/resSim.c
@@ -43,7 +43,7 @@
 Res_Sim_t * Res_SimAlloc( int nWords )
 {
     Res_Sim_t * p;
-    p = ALLOC( Res_Sim_t, 1 );
+    p = ABC_ALLOC( Res_Sim_t, 1 );
     memset( p, 0, sizeof(Res_Sim_t) );
     // simulation parameters
     p->nWords    = nWords;
@@ -128,7 +128,7 @@ void Res_SimFree( Res_Sim_t * p )
     Vec_PtrFree( p->vPats1 );
     Vec_PtrFree( p->vOuts );
     Vec_VecFree( p->vCands );
-    free( p );
+    ABC_FREE( p );
 }
 
 
diff --git a/src/opt/res/resWin.c b/src/opt/res/resWin.c
index a3648925..e46fdc70 100644
--- a/src/opt/res/resWin.c
+++ b/src/opt/res/resWin.c
@@ -44,7 +44,7 @@ Res_Win_t * Res_WinAlloc()
 {
     Res_Win_t * p;
     // start the manager
-    p = ALLOC( Res_Win_t, 1 );
+    p = ABC_ALLOC( Res_Win_t, 1 );
     memset( p, 0, sizeof(Res_Win_t) );
     // set internal parameters
     p->nFanoutLimit = 10;
@@ -78,7 +78,7 @@ void Res_WinFree( Res_Win_t * p )
     Vec_PtrFree( p->vNodes  );
     Vec_PtrFree( p->vDivs   );
     Vec_VecFree( p->vMatrix );
-    free( p );
+    ABC_FREE( p );
 }