Version abc90215

9 files changed, 34 insertions, 34 deletions

diff --git a/src/aig/int/int.h b/src/aig/int/int.h
index e0c4e960..c9c5cd1a 100644
--- a/src/aig/int/int.h
+++ b/src/aig/int/int.h
@@ -21,10 +21,6 @@
 #ifndef __INT_H__
 #define __INT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 /* 
     The interpolation algorithm implemented here was introduced in the paper:
     K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13.
@@ -38,6 +34,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/int/intContain.c b/src/aig/int/intContain.c
index dcc80b29..3c16629f 100644
--- a/src/aig/int/intContain.c
+++ b/src/aig/int/intContain.c
@@ -231,7 +231,7 @@ int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter,
     }
 
      // solve the problem
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
 
 //    Inter_ManCheckUniqueness( pTrans, pSat, pCnf, nSteps );
 
@@ -317,7 +317,7 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf
     printf( "Uniquness does not hold in %d frames.\n", Counter );
 
     Fra_SmlStop( pSml );
-    free( pCounterEx );
+    ABC_FREE( pCounterEx );
     return 1;
 }
 
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
index 8fe15cda..cab0302f 100644
--- a/src/aig/int/intCore.c
+++ b/src/aig/int/intCore.c
@@ -146,7 +146,7 @@ p->timeCnf += clock() - clk;
         {
             printf( "Step = %2d. Frames = 1 + %d. And = %5d. Lev = %5d.  ", 
                 s+1, p->nFrames, Aig_ManNodeNum(p->pFrames), Aig_ManLevelNum(p->pFrames) );
-            PRT( "Time", clock() - clk2 );
+            ABC_PRT( "Time", clock() - clk2 );
         }
         // iterate the interpolation procedure
         for ( i = 0; ; i++ )
@@ -176,7 +176,7 @@ p->timeCnf += clock() - clk;
             {
                 printf( "   I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d.  ", 
                     i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur );
-                PRT( "Time", clock() - clk );
+                ABC_PRT( "Time", clock() - clk );
             }
             if ( RetValue == 0 ) // found a (spurious?) counter-example
             {
diff --git a/src/aig/int/intCtrex.c b/src/aig/int/intCtrex.c
index 4cbe2007..98c01de6 100644
--- a/src/aig/int/intCtrex.c
+++ b/src/aig/int/intCtrex.c
@@ -123,7 +123,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
         return NULL;
     }
     // solve the miter
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     // if the problem is SAT, get the counterexample
     if ( status == l_True )
     {
@@ -134,9 +134,9 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
         for ( i = 0; i < Vec_IntSize(vCiIds); i++ )
             if ( pModel[i] )
                 Aig_InfoSetBit( pCtrex->pData, Saig_ManRegNum(pAig) + i );
-        free( pModel );
+        ABC_FREE( pModel );
     }
-    // free the sat_solver
+    // ABC_FREE the sat_solver
     sat_solver_delete( pSat );
     Vec_IntFree( vCiIds );
     // verify counter-example
@@ -146,7 +146,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
     // report the results
     if ( fVerbose )
     {
-        PRT( "Total ctrex generation time", clock() - clk );
+        ABC_PRT( "Total ctrex generation time", clock() - clk );
     }
     return pCtrex;
 
diff --git a/src/aig/int/intDup.c b/src/aig/int/intDup.c
index 3e5aaa7e..4c5b7ab6 100644
--- a/src/aig/int/intDup.c
+++ b/src/aig/int/intDup.c
@@ -46,13 +46,13 @@ Aig_Man_t * Inter_ManStartInitState( int nRegs )
     Aig_Obj_t ** ppInputs;
     int i;
     assert( nRegs > 0 );
-    ppInputs = ALLOC( Aig_Obj_t *, nRegs );
+    ppInputs = ABC_ALLOC( Aig_Obj_t *, nRegs );
     p = Aig_ManStart( nRegs );
     for ( i = 0; i < nRegs; i++ )
         ppInputs[i] = Aig_Not( Aig_ObjCreatePi(p) );
     pRes = Aig_Multi( p, ppInputs, nRegs, AIG_OBJ_AND );
     Aig_ObjCreatePo( p, pRes );
-    free( ppInputs );
+    ABC_FREE( ppInputs );
     return p;
 }
 
diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h
index c84fef2d..2d571f09 100644
--- a/src/aig/int/intInt.h
+++ b/src/aig/int/intInt.h
@@ -21,10 +21,6 @@
 #ifndef __INT_INT_H__
 #define __INT_INT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -39,6 +35,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/int/intM114.c b/src/aig/int/intM114.c
index dbf078e2..359d5458 100644
--- a/src/aig/int/intM114.c
+++ b/src/aig/int/intM114.c
@@ -217,19 +217,19 @@ int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward )
     }
 
     // collect global variables
-    pGlobalVars = CALLOC( int, sat_solver_nvars(pSat) );
+    pGlobalVars = ABC_CALLOC( int, sat_solver_nvars(pSat) );
     Vec_IntForEachEntry( p->vVarsAB, Var, i )
         pGlobalVars[Var] = 1;
     pSat->pGlobalVars = fUseBias? pGlobalVars : NULL;
 
     // solve the problem
 clk = clock();
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     p->nConfCur = pSat->stats.conflicts;
 p->timeSat += clock() - clk;
 
     pSat->pGlobalVars = NULL;
-    FREE( pGlobalVars );
+    ABC_FREE( pGlobalVars );
     if ( status == l_False )
     {
         pSatCnf = sat_solver_store_release( pSat );
diff --git a/src/aig/int/intMan.c b/src/aig/int/intMan.c
index ec5d06d3..14a79f65 100644
--- a/src/aig/int/intMan.c
+++ b/src/aig/int/intMan.c
@@ -43,7 +43,7 @@ Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars )
 {
     Inter_Man_t * p;
     // create interpolation manager
-    p = ALLOC( Inter_Man_t, 1 );
+    p = ABC_ALLOC( Inter_Man_t, 1 );
     memset( p, 0, sizeof(Inter_Man_t) );
     p->vVarsAB = Vec_IntAlloc( Aig_ManRegNum(pAig) );
     p->nConfLimit = pPars->nBTLimit;
@@ -92,13 +92,13 @@ void Inter_ManStop( Inter_Man_t * p )
     {
         p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu;
         printf( "Runtime statistics:\n" );
-        PRTP( "Rewriting  ", p->timeRwr,   p->timeTotal );
-        PRTP( "CNF mapping", p->timeCnf,   p->timeTotal );
-        PRTP( "SAT solving", p->timeSat,   p->timeTotal );
-        PRTP( "Interpol   ", p->timeInt,   p->timeTotal );
-        PRTP( "Containment", p->timeEqu,   p->timeTotal );
-        PRTP( "Other      ", p->timeOther, p->timeTotal );
-        PRTP( "TOTAL      ", p->timeTotal, p->timeTotal );
+        ABC_PRTP( "Rewriting  ", p->timeRwr,   p->timeTotal );
+        ABC_PRTP( "CNF mapping", p->timeCnf,   p->timeTotal );
+        ABC_PRTP( "SAT solving", p->timeSat,   p->timeTotal );
+        ABC_PRTP( "Interpol   ", p->timeInt,   p->timeTotal );
+        ABC_PRTP( "Containment", p->timeEqu,   p->timeTotal );
+        ABC_PRTP( "Other      ", p->timeOther, p->timeTotal );
+        ABC_PRTP( "TOTAL      ", p->timeTotal, p->timeTotal );
     }
 
     if ( p->pCnfAig )
@@ -116,7 +116,7 @@ void Inter_ManStop( Inter_Man_t * p )
         Aig_ManStop( p->pInter );
     if ( p->pInterNew )
         Aig_ManStop( p->pInterNew );
-    free( p );
+    ABC_FREE( p );
 }
 
 
diff --git a/src/aig/int/intUtil.c b/src/aig/int/intUtil.c
index 722a3611..c0dc9ddb 100644
--- a/src/aig/int/intUtil.c
+++ b/src/aig/int/intUtil.c
@@ -51,9 +51,9 @@ int Inter_ManCheckInitialState( Aig_Man_t * p )
     Cnf_DataFree( pCnf );
     if ( pSat == NULL )
         return 0;
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     sat_solver_delete( pSat );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     return status == l_True;
 }
 
@@ -79,9 +79,9 @@ int Inter_ManCheckAllStates( Aig_Man_t * p )
     Cnf_DataFree( pCnf );
     if ( pSat == NULL )
         return 1;
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     sat_solver_delete( pSat );
-    PRT( "Time", clock() - clk );
+    ABC_PRT( "Time", clock() - clk );
     return status == l_False;
 }