From 686d38d66754027cd29c64f1dc2975248eab7796 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 13 Feb 2011 15:16:10 -0800 Subject: Changes to enable C++ compilation after recent modifications. --- src/aig/aig/aigDoms.c | 8 ++++---- src/aig/llb/llb2Bad.c | 2 +- src/aig/llb/llb2Core.c | 3 +-- src/aig/llb/llb2Dump.c | 2 +- src/aig/llb/llb2Flow.c | 14 +++++++------- src/aig/llb/llb3Nonlin.c | 3 +-- src/aig/llb/llbInt.h | 2 ++ src/aig/saig/saigDup.c | 2 +- src/aig/saig/saigTempor.c | 4 ++-- src/aig/ssw/sswInt.h | 1 + src/aig/ssw/sswSweep.c | 1 - src/base/cmd/cmd.h | 2 ++ src/base/cmd/cmdLoad.c | 2 -- src/misc/extra/extra.h | 2 +- src/misc/hash/hashGen.h | 4 ++-- src/misc/util/utilSignal.c | 11 ++++++----- src/misc/util/utilSignal.h | 38 ++++++++++++++++--------------------- src/misc/util/util_hack.h | 47 +++++++--------------------------------------- src/sat/pdr/pdrInv.c | 2 +- src/sat/pdr/pdrMan.c | 4 ++-- 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 #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 #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 #include #include @@ -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++ ) -- cgit v1.2.3