Version abc90215

9 files changed, 45 insertions, 45 deletions

diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h
index d0092a5f..a5a56da6 100644
--- a/src/aig/dch/dch.h
+++ b/src/aig/dch/dch.h
@@ -21,10 +21,6 @@
 #ifndef __DCH_H__
 #define __DCH_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/aig/dch/dchChoice.c b/src/aig/dch/dchChoice.c
index 19689051..019f4ec4 100644
--- a/src/aig/dch/dchChoice.c
+++ b/src/aig/dch/dchChoice.c
@@ -247,8 +247,8 @@ Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig )
     int i;
     // start recording equivalences
     pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
-    pChoices->pEquivs = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
-    pChoices->pReprs  = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+    pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+    pChoices->pReprs  = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
     // map constants and PIs
     Aig_ManCleanData( pAig );
     Aig_ManConst1(pAig)->pData = Aig_ManConst1(pChoices);
@@ -262,7 +262,7 @@ Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig )
         Aig_ObjCreatePo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
     Dch_DeriveChoiceCountEquivs( pChoices );
     // there is no need for cleanup
-    FREE( pChoices->pReprs );
+    ABC_FREE( pChoices->pReprs );
     pChoices = Aig_ManDupDfs( pTemp = pChoices );
     Aig_ManStop( pTemp );
     return pChoices;
diff --git a/src/aig/dch/dchClass.c b/src/aig/dch/dchClass.c
index 5d042847..d8fbe8ed 100644
--- a/src/aig/dch/dchClass.c
+++ b/src/aig/dch/dchClass.c
@@ -134,11 +134,11 @@ static inline Aig_Obj_t ** Dch_ObjRemoveClass( Dch_Cla_t * p, Aig_Obj_t * pRepr
 Dch_Cla_t * Dch_ClassesStart( Aig_Man_t * pAig )
 {
     Dch_Cla_t * p;
-    p = ALLOC( Dch_Cla_t, 1 );
+    p = ABC_ALLOC( Dch_Cla_t, 1 );
     memset( p, 0, sizeof(Dch_Cla_t) );
     p->pAig         = pAig;
-    p->pId2Class    = CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
-    p->pClassSizes  = CALLOC( int, Aig_ManObjNumMax(pAig) );
+    p->pId2Class    = ABC_CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
+    p->pClassSizes  = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
     p->vClassOld    = Vec_PtrAlloc( 100 );
     p->vClassNew    = Vec_PtrAlloc( 100 );
     assert( pAig->pReprs == NULL );
@@ -183,10 +183,10 @@ void Dch_ClassesStop( Dch_Cla_t * p )
 {
     if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
     if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
-    FREE( p->pId2Class );
-    FREE( p->pClassSizes );
-    FREE( p->pMemClasses );
-    free( p );
+    ABC_FREE( p->pId2Class );
+    ABC_FREE( p->pClassSizes );
+    ABC_FREE( p->pMemClasses );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
@@ -338,8 +338,8 @@ void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs )
 
     // allocate the hash table hashing simulation info into nodes
     nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 );
-    ppTable = CALLOC( Aig_Obj_t *, nTableSize ); 
-    ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); 
+    ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize ); 
+    ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); 
 
     // add all the nodes to the hash table
     nEntries = 0;
@@ -390,7 +390,7 @@ void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs )
     }
 
     // allocate room for classes
-    p->pMemClasses = ALLOC( Aig_Obj_t *, nEntries + p->nCands1 );
+    p->pMemClasses = ABC_ALLOC( Aig_Obj_t *, nEntries + p->nCands1 );
     p->pMemClassesFree = p->pMemClasses + nEntries;
  
     // copy the entries into storage in the topological order
@@ -419,8 +419,8 @@ void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs )
         nEntries2 += nNodes;
     }
     assert( nEntries == nEntries2 );
-    free( ppTable );
-    free( ppNexts );
+    ABC_FREE( ppTable );
+    ABC_FREE( ppNexts );
     // now it is time to refine the classes
     Dch_ClassesRefine( p );
     Dch_ClassesCheck( p );
diff --git a/src/aig/dch/dchCnf.c b/src/aig/dch/dchCnf.c
index dc822d77..81fc2f2c 100644
--- a/src/aig/dch/dchCnf.c
+++ b/src/aig/dch/dchCnf.c
@@ -166,7 +166,7 @@ void Dch_AddClausesSuper( Dch_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
     assert( Aig_ObjIsNode( pNode ) );
     // create storage for literals
     nLits = Vec_PtrSize(vSuper) + 1;
-    pLits = ALLOC( int, nLits );
+    pLits = ABC_ALLOC( int, nLits );
     // suppose AND-gate is A & B = C
     // add !A => !C   or   A + !C
     Vec_PtrForEachEntry( vSuper, pFanin, i )
@@ -197,7 +197,7 @@ void Dch_AddClausesSuper( Dch_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
     }
     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
     assert( RetValue );
-    free( pLits );
+    ABC_FREE( pLits );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c
index 27c039cf..8e854355 100644
--- a/src/aig/dch/dchCore.c
+++ b/src/aig/dch/dchCore.c
@@ -93,7 +93,7 @@ p->timeChoice = clock() - clk;
 //    pResult = Aig_ManDupSimpleDfs( p->pAigTotal );
     // count the number of equivalences and choices
     p->nEquivs = Dch_DeriveChoiceCountEquivs( pResult );
-    p->nChoices = Aig_ManCountChoices( pResult );
+    p->nChoices = Aig_ManChoiceNum( pResult );
 p->timeTotal = clock() - clkTotal;
     Dch_ManStop( p );
     return pResult;
diff --git a/src/aig/dch/dchInt.h b/src/aig/dch/dchInt.h
index e9a6f2e4..4e6315a4 100644
--- a/src/aig/dch/dchInt.h
+++ b/src/aig/dch/dchInt.h
@@ -21,10 +21,6 @@
 #ifndef __DCH_INT_H__
 #define __DCH_INT_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -37,6 +33,10 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c
index a5faa2a6..caed0ed5 100644
--- a/src/aig/dch/dchMan.c
+++ b/src/aig/dch/dchMan.c
@@ -43,7 +43,7 @@ Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
 {
     Dch_Man_t * p;
     // create interpolation manager
-    p = ALLOC( Dch_Man_t, 1 );
+    p = ABC_ALLOC( Dch_Man_t, 1 );
     memset( p, 0, sizeof(Dch_Man_t) );
     p->pPars        = pPars;
     p->vAigs        = vAigs;
@@ -51,13 +51,13 @@ Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
     Aig_ManFanoutStart( p->pAigTotal );
     // SAT solving
     p->nSatVars     = 1;
-    p->pSatVars     = CALLOC( int, Aig_ManObjNumMax(p->pAigTotal) );
+    p->pSatVars     = ABC_CALLOC( int, Aig_ManObjNumMax(p->pAigTotal) );
     p->vUsedNodes   = Vec_PtrAlloc( 1000 );
     p->vFanins      = Vec_PtrAlloc( 100 );
     p->vSimRoots    = Vec_PtrAlloc( 1000 );
     p->vSimClasses  = Vec_PtrAlloc( 1000 );
     // equivalences proved
-    p->pReprsProved = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAigTotal) );
+    p->pReprsProved = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAigTotal) );
     return p;
 }
 
@@ -95,18 +95,18 @@ void Dch_ManPrintStats( Dch_Man_t * p )
         p->nLits, p->nReprs, p->nEquivs, p->nChoices );
     printf( "Choicing runtime statistics:\n" );
     p->timeOther = p->timeTotal-p->timeSimInit-p->timeSimSat-p->timeSat-p->timeChoice;
-    PRTP( "Sim init   ", p->timeSimInit,  p->timeTotal );
-    PRTP( "Sim SAT    ", p->timeSimSat,   p->timeTotal );
-    PRTP( "SAT solving", p->timeSat,      p->timeTotal );
-    PRTP( "  sat      ", p->timeSatSat,   p->timeTotal );
-    PRTP( "  unsat    ", p->timeSatUnsat, p->timeTotal );
-    PRTP( "  undecided", p->timeSatUndec, p->timeTotal );
-    PRTP( "Choice     ", p->timeChoice,   p->timeTotal );
-    PRTP( "Other      ", p->timeOther,    p->timeTotal );
-    PRTP( "TOTAL      ", p->timeTotal,    p->timeTotal );
+    ABC_PRTP( "Sim init   ", p->timeSimInit,  p->timeTotal );
+    ABC_PRTP( "Sim SAT    ", p->timeSimSat,   p->timeTotal );
+    ABC_PRTP( "SAT solving", p->timeSat,      p->timeTotal );
+    ABC_PRTP( "  sat      ", p->timeSatSat,   p->timeTotal );
+    ABC_PRTP( "  unsat    ", p->timeSatUnsat, p->timeTotal );
+    ABC_PRTP( "  undecided", p->timeSatUndec, p->timeTotal );
+    ABC_PRTP( "Choice     ", p->timeChoice,   p->timeTotal );
+    ABC_PRTP( "Other      ", p->timeOther,    p->timeTotal );
+    ABC_PRTP( "TOTAL      ", p->timeTotal,    p->timeTotal );
     if ( p->pPars->timeSynth )
     {
-    PRT( "Synthesis  ", p->pPars->timeSynth );
+    ABC_PRT( "Synthesis  ", p->pPars->timeSynth );
     }
 }
 
@@ -137,9 +137,9 @@ void Dch_ManStop( Dch_Man_t * p )
     Vec_PtrFree( p->vFanins );
     Vec_PtrFree( p->vSimRoots );
     Vec_PtrFree( p->vSimClasses );
-    FREE( p->pReprsProved );
-    FREE( p->pSatVars );
-    free( p );
+    ABC_FREE( p->pReprsProved );
+    ABC_FREE( p->pSatVars );
+    ABC_FREE( p );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/dch/dchSat.c b/src/aig/dch/dchSat.c
index 07196259..6966e635 100644
--- a/src/aig/dch/dchSat.c
+++ b/src/aig/dch/dchSat.c
@@ -83,7 +83,7 @@ int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
 clk = clock();
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
-        (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
     {
@@ -125,7 +125,7 @@ p->timeSatUndec += clock() - clk;
     }
 clk = clock();
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
-        (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
 p->timeSat += clock() - clk;
     if ( RetValue1 == l_False )
     {
diff --git a/src/aig/dch/dchSweep.c b/src/aig/dch/dchSweep.c
index 36c5fc33..afaf7426 100644
--- a/src/aig/dch/dchSweep.c
+++ b/src/aig/dch/dchSweep.c
@@ -127,7 +127,7 @@ void Dch_ManSweep( Dch_Man_t * p )
     }
     Bar_ProgressStop( pProgress );
     // update the representatives of the nodes (makes classes invalid)
-    FREE( p->pAigTotal->pReprs );
+    ABC_FREE( p->pAigTotal->pReprs );
     p->pAigTotal->pReprs = p->pReprsProved;
     p->pReprsProved = NULL;
     // clean the mark