Changes to enable C++ compilation after recent modifications.

20 files changed, 58 insertions, 96 deletions

diff --git a/src/aig/aig/aigDoms.c b/src/aig/aig/aigDoms.c
index c12c0caa..7097a34a 100644
--- a/src/aig/aig/aigDoms.c
+++ b/src/aig/aig/aigDoms.c
@@ -547,11 +547,11 @@ void Aig_ObjDomCompute( Aig_Sto_t * pSto, Aig_Obj_t * pObj )
             Vec_IntPush( pSto->vFans, iFanout>>1 );
     if ( Vec_IntSize(pSto->vFans) == 0 )
         return;
-    vDoms0 = Vec_PtrEntry( pSto->vDoms, Vec_IntEntry(pSto->vFans, 0) );
+    vDoms0 = (Vec_Ptr_t *)Vec_PtrEntry( pSto->vDoms, Vec_IntEntry(pSto->vFans, 0) );
     vDoms2 = Aig_ObjDomVecDup( pSto, vDoms0, 0 );
     Vec_IntForEachEntryStart( pSto->vFans, iFanout, i, 1 )
     {
-        vDoms1 = Vec_PtrEntry( pSto->vDoms, iFanout );
+        vDoms1 = (Vec_Ptr_t *)Vec_PtrEntry( pSto->vDoms, iFanout );
         vDoms2 = Aig_ObjDomMerge( pSto, vDomsT = vDoms2, vDoms1 );
         Aig_ObjDomVecRecycle( pSto, vDomsT );
     }
@@ -662,11 +662,11 @@ Vec_Ptr_t * Aig_ObjDomCollect( Aig_Sto_t * pSto, Vec_Int_t * vCut )
 {
     Vec_Ptr_t * vDoms0, * vDoms1, * vDoms2;
     int i, ObjId;
-    vDoms0 = Vec_PtrEntry( pSto->vDoms, Vec_IntEntry(vCut, 0) );
+    vDoms0 = (Vec_Ptr_t *)Vec_PtrEntry( pSto->vDoms, Vec_IntEntry(vCut, 0) );
     vDoms2 = Aig_ObjDomVecDup( pSto, vDoms0, 1 );
     Vec_IntForEachEntryStart( vCut, ObjId, i, 1 )
     {
-        vDoms1 = Vec_PtrEntry( pSto->vDoms, ObjId );
+        vDoms1 = (Vec_Ptr_t *)Vec_PtrEntry( pSto->vDoms, ObjId );
         if ( vDoms1 == NULL )
             continue;
         Aig_ObjDomUnion( pSto, vDoms2, vDoms1 );
diff --git a/src/aig/llb/llb2Bad.c b/src/aig/llb/llb2Bad.c
index 88ff4c75..8e2a37ff 100644
--- a/src/aig/llb/llb2Bad.c
+++ b/src/aig/llb/llb2Bad.c
@@ -87,7 +87,7 @@ DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut )
     {
         if ( !Aig_ObjIsNode(pObj) )
             continue;
-        Cudd_RecursiveDeref( dd, pObj->pData );
+        Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
     }
     Vec_PtrFree( vNodes );
     Cudd_Deref( bResult );
diff --git a/src/aig/llb/llb2Core.c b/src/aig/llb/llb2Core.c
index 7fa361b9..596a34af 100644
--- a/src/aig/llb/llb2Core.c
+++ b/src/aig/llb/llb2Core.c
@@ -95,7 +95,6 @@ DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarInde
 Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p )
 {
     extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
-    extern int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
     Abc_Cex_t * pCex;
     Aig_Obj_t * pObj;
     Vec_Ptr_t * vSupps, * vQuant0, * vQuant1;
@@ -118,7 +117,7 @@ Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p )
     pCex->iPo = -1;
 
     // get the last cube
-    bOneCube = Cudd_bddIntersect( p->ddR, Vec_PtrEntryLast(p->vRings), p->ddR->bFunc );  Cudd_Ref( bOneCube );
+    bOneCube = Cudd_bddIntersect( p->ddR, (DdNode *)Vec_PtrEntryLast(p->vRings), p->ddR->bFunc );  Cudd_Ref( bOneCube );
     RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
     Cudd_RecursiveDeref( p->ddR, bOneCube );
     assert( RetValue );
diff --git a/src/aig/llb/llb2Dump.c b/src/aig/llb/llb2Dump.c
index 55f94907..3e1dd8c5 100644
--- a/src/aig/llb/llb2Dump.c
+++ b/src/aig/llb/llb2Dump.c
@@ -83,7 +83,7 @@ void Llb_ManDumpReached( DdManager * ddG, DdNode * bReached, char * pModel, char
 
     // write the file
     pFile = fopen( pFileName, "wb" );
-    Cudd_DumpBlif( ddG, 1, &bReached, (char **)Vec_PtrArray(vNamesIn), (char **)Vec_PtrArray(vNamesOut), pModel, pFile );
+    Cudd_DumpBlif( ddG, 1, &bReached, (char **)Vec_PtrArray(vNamesIn), (char **)Vec_PtrArray(vNamesOut), pModel, pFile, 0 );
     fclose( pFile );
 
     // cleanup
diff --git a/src/aig/llb/llb2Flow.c b/src/aig/llb/llb2Flow.c
index 36b3ff1b..1b177807 100644
--- a/src/aig/llb/llb2Flow.c
+++ b/src/aig/llb/llb2Flow.c
@@ -144,7 +144,7 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp
             continue;
         if ( piFirst[i] == piLast[i] )
         {
-            vMap = Vec_PtrEntry( vMaps, piFirst[i] );
+            vMap = (Vec_Int_t *)Vec_PtrEntry( vMaps, piFirst[i] );
             Vec_IntWriteEntry( vMap, pObj->Id, 2 );
             continue;
         }
@@ -152,7 +152,7 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp
         // set support for all in between        
         for ( k = piFirst[i]; k <= piLast[i]; k++ )
         {
-            vMap = Vec_PtrEntry( vMaps, k );
+            vMap = (Vec_Int_t *)Vec_PtrEntry( vMaps, k );
             Vec_IntWriteEntry( vMap, pObj->Id, 1 );
         }
     }
@@ -165,8 +165,8 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp
     printf( "%d ", Counter );
     Vec_PtrForEachEntryStart( Vec_Int_t *, vMaps, vMap, i, 1 )
     {
-        vPrev = Vec_PtrEntry( vMaps, i-1 );
-        vNext = (i == Vec_PtrSize(vMaps)-1)? NULL: Vec_PtrEntry( vMaps, i+1 );
+        vPrev = (Vec_Int_t *)Vec_PtrEntry( vMaps, i-1 );
+        vNext = (i == Vec_PtrSize(vMaps)-1)? NULL: (Vec_Int_t *)Vec_PtrEntry( vMaps, i+1 );
 
         CounterPlus = CounterMinus = 0;
         Aig_ManForEachObj( p, pObj, k )
@@ -1134,7 +1134,7 @@ void Llb_ManFlowGetObjSet( Aig_Man_t * p, Vec_Ptr_t * vLower, int iStart, int nS
     Vec_PtrClear( vSet );
     for ( i = 0; i < nSize; i++ )
     {
-        pObj = Vec_PtrEntry( vLower, (iStart + i) % Vec_PtrSize(vLower) );
+        pObj = (Aig_Obj_t *)Vec_PtrEntry( vLower, (iStart + i) % Vec_PtrSize(vLower) );
         Vec_PtrPush( vSet, pObj );
     }
 }
@@ -1334,7 +1334,7 @@ void Llb_ManMinCutTest( Aig_Man_t * pAig, int Num )
 {
     extern void Llb_BddConstructTest( Aig_Man_t * p, Vec_Ptr_t * vResult );
     extern void Llb_BddExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, Vec_Ptr_t * vMaps );
-    extern void Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult );
+ 
 
     int fVerbose = 1;
     Gia_ParLlb_t Pars, * pPars = &Pars;
@@ -1354,7 +1354,7 @@ void Llb_ManMinCutTest( Aig_Man_t * pAig, int Num )
 //    vMaps   = Llb_ManCutMap( p, vResult, vSupps );
 
 //    Llb_BddExperiment( pAig, p, pPars, vResult, vMaps );
-    Llb_CoreExperiment( pAig, p, pPars, vResult );
+    Llb_CoreExperiment( pAig, p, pPars, vResult, 0 );
 
 //    Vec_VecFree( (Vec_Vec_t *)vMaps );
 //    Vec_VecFree( (Vec_Vec_t *)vSupps );
diff --git a/src/aig/llb/llb3Nonlin.c b/src/aig/llb/llb3Nonlin.c
index adab5b0b..e52e28ca 100644
--- a/src/aig/llb/llb3Nonlin.c
+++ b/src/aig/llb/llb3Nonlin.c
@@ -238,7 +238,6 @@ DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd )
 Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
 {
     extern Abc_Cex_t * Ssw_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames );
-    extern int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
     Abc_Cex_t * pCex;
     Aig_Obj_t * pObj;
     Vec_Int_t * vVarsNs;
@@ -269,7 +268,7 @@ Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
     pCex->iPo = -1;
 
     // get the last cube
-    bOneCube = Cudd_bddIntersect( p->ddR, Vec_PtrEntryLast(p->vRings), p->ddR->bFunc );  Cudd_Ref( bOneCube );
+    bOneCube = Cudd_bddIntersect( p->ddR, (DdNode *)Vec_PtrEntryLast(p->vRings), p->ddR->bFunc );  Cudd_Ref( bOneCube );
     RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
     Cudd_RecursiveDeref( p->ddR, bOneCube );
     assert( RetValue );
diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h
index 3ee1f5c2..70578c47 100644
--- a/src/aig/llb/llbInt.h
+++ b/src/aig/llb/llbInt.h
@@ -29,6 +29,7 @@
 #include <stdio.h>
 #include "aig.h"
 #include "saig.h"
+#include "ssw.h"
 #include "cuddInt.h"
 #include "extra.h"
 #include "llb.h"
@@ -150,6 +151,7 @@ extern DdNode *        Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int
 extern DdNode *        Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc );
 /*=== llb2Core.c ======================================================*/
 extern DdNode *        Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues );
+extern int             Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, int TimeTarget ); 
 /*=== llb2Driver.c ======================================================*/
 extern Vec_Int_t *     Llb_DriverCountRefs( Aig_Man_t * p );
 extern Vec_Int_t *     Llb_DriverCollectNs( Aig_Man_t * pAig, Vec_Int_t * vDriRefs );
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index 4d34224e..f4e557f8 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -115,7 +115,7 @@ Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs )
     Aig_ManForEachNodeVec( pAig, vPairs, pObj, i )
     {
         pObj2  = Aig_ManObj( pAig, Vec_IntEntry(vPairs, ++i) );
-        pMiter = Aig_Exor( pAigNew, pObj->pData, pObj2->pData );
+        pMiter = Aig_Exor( pAigNew, (Aig_Obj_t *)pObj->pData, (Aig_Obj_t *)pObj2->pData );
         pMiter = Aig_NotCond( pMiter, pObj->fPhase ^ pObj2->fPhase );
         Aig_ObjCreatePo( pAigNew, pMiter );
     }
diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c
index 74f4a9d3..962a81de 100644
--- a/src/aig/saig/saigTempor.c
+++ b/src/aig/saig/saigTempor.c
@@ -69,7 +69,7 @@ Aig_Man_t * Saig_ManTemporFrames( Aig_Man_t * pAig, int nFrames )
     }
     // create POs for the flop inputs
     Saig_ManForEachLi( pAig, pObj, i )
-        Aig_ObjCreatePo( pFrames, pObj->pData );
+        Aig_ObjCreatePo( pFrames, (Aig_Obj_t *)pObj->pData );
     Aig_ManCleanup( pFrames );
     return pFrames;
 }
@@ -123,7 +123,7 @@ Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames )
 
     // create flop output values
     Saig_ManForEachLo( pAig, pObj, i )
-        pObj->pData = Aig_Mux( pAigNew, pReset, Aig_ObjCreatePi(pAigNew), Aig_ManPo(pFrames, i)->pData );
+        pObj->pData = Aig_Mux( pAigNew, pReset, Aig_ObjCreatePi(pAigNew), (Aig_Obj_t *)Aig_ManPo(pFrames, i)->pData );
     Aig_ManStop( pFrames );
 
     // add internal nodes of this frame
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index ad868c6e..189494bc 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -29,6 +29,7 @@
 #include "saig.h"
 #include "satSolver.h"
 #include "ssw.h"
+#include "ioa.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 40121e42..edae0846 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -331,7 +331,6 @@ p->timeBmc += clock() - clk;
 ***********************************************************************/
 void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num )
 {
-    extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
     FILE * pFile;
     char pBuffer[16];
     Aig_Man_t * pNew;
diff --git a/src/base/cmd/cmd.h b/src/base/cmd/cmd.h
index 787e52b9..740cf758 100644
--- a/src/base/cmd/cmd.h
+++ b/src/base/cmd/cmd.h
@@ -60,6 +60,8 @@ extern void        Cmd_FlagDeleteByName( Abc_Frame_t * pAbc, const char * key );
 extern void        Cmd_FlagUpdateValue( Abc_Frame_t * pAbc, const char * key, char * value );
 /*=== cmdHist.c ========================================================*/
 extern void          Cmd_HistoryAddCommand( Abc_Frame_t * pAbc, const char * command );
+/*=== cmdLoad.c ========================================================*/
+extern int         CmdCommandLoad( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 
 
diff --git a/src/base/cmd/cmdLoad.c b/src/base/cmd/cmdLoad.c
index 8ff03282..b96737c6 100644
--- a/src/base/cmd/cmdLoad.c
+++ b/src/base/cmd/cmdLoad.c
@@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int CmdCommandLoad          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 240fee03..dd0edb44 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -611,7 +611,7 @@ extern char *        Extra_UtilTildeExpand( char *fname );
 extern char *        Extra_UtilFileSearch( char *file, char *path, char *mode );
 extern void          (*Extra_UtilMMoutOfMemory)( long size );
 
-extern const char *        globalUtilOptarg;
+extern const char *  globalUtilOptarg;
 extern int           globalUtilOptind;
 
 /**AutomaticEnd***************************************************************/
diff --git a/src/misc/hash/hashGen.h b/src/misc/hash/hashGen.h
index 257b9dba..fc1b82c3 100644
--- a/src/misc/hash/hashGen.h
+++ b/src/misc/hash/hashGen.h
@@ -229,7 +229,7 @@ static inline void Hash_GenWriteEntry( Hash_Gen_t *p, void * key, void * data )
   p->nSize++;
   (*pLast) = pEntry = ABC_ALLOC( Hash_Gen_Entry_t, 1 );
   pEntry->pNext = NULL;
-  pEntry->key  = key;
+  pEntry->key  = (char *)key;
   pEntry->data = data;
 
   return;
@@ -271,7 +271,7 @@ static inline Hash_Gen_Entry_t * Hash_GenEntry( Hash_Gen_t *p, void * key, int f
     p->nSize++;
     (*pLast) = pEntry = ABC_ALLOC( Hash_Gen_Entry_t, 1 );
     pEntry->pNext = NULL;
-    pEntry->key  = key;
+    pEntry->key  = (char *)key;
     pEntry->data = NULL;
     return pEntry;
   }
diff --git a/src/misc/util/utilSignal.c b/src/misc/util/utilSignal.c
index 6a793ce0..7304e410 100644
--- a/src/misc/util/utilSignal.c
+++ b/src/misc/util/utilSignal.c
@@ -4,17 +4,17 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName []
+  PackageName [Signal handling utilities.]
 
-  Synopsis    []
+  Synopsis    [Signal handling utilities.]
 
-  Author      []
+  Author      [Baruch Sterin]
   
   Affiliation [UC Berkeley]
 
-  Date        []
+  Date        [Ver. 1.0. Started - February 1, 2011.]
 
-  Revision    []
+  Revision    [$Id: utilSignal.c,v 1.00 2011/02/01 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -23,6 +23,7 @@
 #include <signal.h>
 #include "abc_global.h"
 #include "hashGen.h"
+#include "utilSignal.h"
 
 #ifndef _MSC_VER
 
diff --git a/src/misc/util/utilSignal.h b/src/misc/util/utilSignal.h
index d9802aa0..30c0ba1d 100644
--- a/src/misc/util/utilSignal.h
+++ b/src/misc/util/utilSignal.h
@@ -4,17 +4,17 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName []
+  PackageName [Signal handling utilities.]
 
-  Synopsis    []
+  Synopsis    [Signal handling utilities.]
 
-  Author      []
+  Author      [Baruch Sterin]
   
   Affiliation [UC Berkeley]
 
-  Date        []
+  Date        [Ver. 1.0. Started - February 1, 2011.]
 
-  Revision    []
+  Revision    [$Id: utilSignal.h,v 1.00 2011/02/01 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
  
@@ -44,23 +44,17 @@ ABC_NAMESPACE_HEADER_START
 ////////////////////////////////////////////////////////////////////////
 
 /*=== utilSignal.c ==========================================================*/
-
-void Util_SignalCleanup();
-
-void Util_SignalStartHandler();
-void Util_SignalResetHandler();
-void Util_SignalStopHandler();
-
-void Util_SignalBlockSignals();
-void Util_SignalUnblockSignals();
-
-void Util_SignalAddChildPid(int pid);
-void Util_SignalRemoveChildPid(int pid);
-
-int Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name);
-void Util_SignalTmpFileRemove(const char* fname, int fLeave);
-
-int Util_SignalSystem(const char* cmd);
+extern void      Util_SignalCleanup();
+extern void      Util_SignalStartHandler();
+extern void      Util_SignalResetHandler();
+extern void      Util_SignalStopHandler();
+extern void      Util_SignalBlockSignals();
+extern void      Util_SignalUnblockSignals();
+extern void      Util_SignalAddChildPid(int pid);
+extern void      Util_SignalRemoveChildPid(int pid);
+extern int       Util_SignalTmpFile(const char* prefix, const char* suffix, char** out_name);
+extern void      Util_SignalTmpFileRemove(const char* fname, int fLeave);
+extern int       Util_SignalSystem(const char* cmd);
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/misc/util/util_hack.h b/src/misc/util/util_hack.h
index f7ad89f9..1a734f03 100644
--- a/src/misc/util/util_hack.h
+++ b/src/misc/util/util_hack.h
@@ -21,7 +21,6 @@
 #ifndef __UTIL_HACK_H__
 #define __UTIL_HACK_H__
 
-
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
@@ -31,50 +30,18 @@
 
 #include "abc_global.h"
 
-
 ABC_NAMESPACE_HEADER_START
 
+#define NIL(type)           ((type *) 0)
 
-#ifndef EXTERN
-#define EXTERN extern
-#endif
-#define NIL(type)              ((type *) 0)
-#define random                 rand
-#define srandom                srand
-
-#define util_cpu_time          Extra_CpuTime            
-#define getSoftDataLimit       Extra_GetSoftDataLimit   
-#define util_getopt_reset      Extra_UtilGetoptReset    
-#define util_getopt            Extra_UtilGetopt         
-#define util_print_time        Extra_UtilPrintTime      
-#define util_strsav            Extra_UtilStrsav         
-#define util_tilde_expand      Extra_UtilTildeExpand    
-#define util_file_search       Extra_UtilFileSearch
-#define MMoutOfMemory          Extra_UtilMMoutOfMemory      
-
-#define util_optarg            globalUtilOptarg
-#define util_optind            globalUtilOptind
-
-#ifndef ARGS
-#define ARGS(protos) protos
-#endif
-
-extern long        Extra_CpuTime();
-extern int         Extra_GetSoftDataLimit();
-extern void        Extra_UtilGetoptReset();
-extern int         Extra_UtilGetopt( int argc, char *argv[], const char *optstring );
-extern char *      Extra_UtilPrintTime( long t );
-extern char *      Extra_UtilStrsav( char *s );
-extern char *      Extra_UtilTildeExpand( char *fname );
-extern char *      Extra_UtilFileSearch( char *file, char *path, char *mode );
-
-extern char *      globalUtilOptarg;
-extern int         globalUtilOptind;
-
+#define util_cpu_time       Extra_CpuTime            
+#define getSoftDataLimit    Extra_GetSoftDataLimit   
+#define MMoutOfMemory       Extra_UtilMMoutOfMemory      
 
+extern long                 Extra_CpuTime();
+extern int                  Extra_GetSoftDataLimit();
+extern void               (*Extra_UtilMMoutOfMemory)( long size );
 
 ABC_NAMESPACE_HEADER_END
 
-
-
 #endif
diff --git a/src/sat/pdr/pdrInv.c b/src/sat/pdr/pdrInv.c
index 184b6c4f..5eb32790 100644
--- a/src/sat/pdr/pdrInv.c
+++ b/src/sat/pdr/pdrInv.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "pdrInt.h"
+#include "extra.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -44,7 +45,6 @@ ABC_NAMESPACE_IMPL_START
 ***********************************************************************/
 void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
 {
-    extern int Extra_Base10Log( unsigned int Num );
     static int PastSize;
     Vec_Ptr_t * vVec;
     int i, ThisSize, Length, LengthStart;
diff --git a/src/sat/pdr/pdrMan.c b/src/sat/pdr/pdrMan.c
index f33f6586..789f4ce8 100644
--- a/src/sat/pdr/pdrMan.c
+++ b/src/sat/pdr/pdrMan.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "pdrInt.h"
+#include "ssw.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -157,7 +158,6 @@ void Pdr_ManStop( Pdr_Man_t * p )
 ***********************************************************************/
 Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
 {
-    extern Abc_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames );
     Abc_Cex_t * pCex;
     Pdr_Obl_t * pObl;
     int i, f, Lit, nFrames = 0;
@@ -165,7 +165,7 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
     for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
         nFrames++;
     // create the counter-example
-    pCex = Gia_ManAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
+    pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
     pCex->iPo    = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput;
     pCex->iFrame = nFrames-1;
     for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )