summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaAiger.c4
-rw-r--r--src/aig/gia/giaDup.c2
-rw-r--r--src/aig/saig/saigConstr.c4
-rw-r--r--src/base/abci/abcMap.c6
-rw-r--r--src/base/abci/abcRec2.c4
-rw-r--r--src/base/abci/abcTim.c4
-rw-r--r--src/base/io/ioReadBlif.c2
-rw-r--r--src/bool/lucky/luckyInt.h28
-rw-r--r--src/bool/lucky/luckySwapIJ.c2
-rw-r--r--src/map/mapper/mapperTree.c4
-rw-r--r--src/map/scl/scl.c14
-rw-r--r--src/map/scl/sclBuff.c2
-rw-r--r--src/map/scl/sclInt.h4
-rw-r--r--src/map/scl/sclUtil.c4
-rw-r--r--src/misc/util/abc_global.h11
-rw-r--r--src/proof/abs/absGla.c8
-rw-r--r--src/sat/bsat/satSolver2.c4
-rw-r--r--src/sat/bsat/satSolver2.h1
18 files changed, 57 insertions, 51 deletions
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 086ab0a8..538b23e9 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -1063,7 +1063,7 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipS
vFlopMap = pNew->vFlopClasses; pNew->vFlopClasses = NULL;
vGateMap = pNew->vGateClasses; pNew->vGateClasses = NULL;
vObjMap = pNew->vObjClasses; pNew->vObjClasses = NULL;
- pManTime = pNew->pManTime; pNew->pManTime = NULL;
+ pManTime = (Tim_Man_t *)pNew->pManTime; pNew->pManTime = NULL;
pNew = Gia_ManCleanup( pTemp = pNew );
if ( (vGateMap || vObjMap) && (Gia_ManObjNum(pNew) < Gia_ManObjNum(pTemp)) )
printf( "Cleanup removed objects after reading. Old gate/object abstraction maps are invalid!\n" );
@@ -1555,7 +1555,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
// write timing information
if ( p->pManTime )
{
- Vec_Str_t * vStr = Tim_ManSave( p->pManTime );
+ Vec_Str_t * vStr = Tim_ManSave( (Tim_Man_t *)p->pManTime );
unsigned char Buffer[10];
int nSize = Vec_StrSize(vStr);
Gia_WriteInt( Buffer, nSize );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index e49ce616..da0551fc 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -923,7 +923,7 @@ Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p )
***********************************************************************/
Gia_Man_t * Gia_ManDupUnnomalize( Gia_Man_t * p )
{
- Tim_Man_t * pTime = p->pManTime;
+ Tim_Man_t * pTime = (Tim_Man_t *)p->pManTime;
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
int i, k, curCi, curCo, curNo, nodeLim;
diff --git a/src/aig/saig/saigConstr.c b/src/aig/saig/saigConstr.c
index 682c46cf..5f54ef83 100644
--- a/src/aig/saig/saigConstr.c
+++ b/src/aig/saig/saigConstr.c
@@ -292,8 +292,8 @@ Aig_Man_t * Saig_ManDupUnfoldConstrs( Aig_Man_t * pAig )
Vec_VecFree( (Vec_Vec_t *)vConsAll );
return Aig_ManDupDfs( pAig );
}
- Vec_PtrSort( vOuts, Saig_ManDupCompare );
- Vec_PtrSort( vCons, Saig_ManDupCompare );
+ Vec_PtrSort( vOuts, (int (*)(void))Saig_ManDupCompare );
+ Vec_PtrSort( vCons, (int (*)(void))Saig_ManDupCompare );
Vec_PtrPush( vOutsAll, vOuts );
Vec_PtrPush( vConsAll, vCons );
}
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 7c1c05be..0476ec92 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -66,7 +66,7 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, double AreaMulti,
Vec_Int_t * vSwitching = NULL;
float * pSwitching = NULL;
clock_t clk, clkTotal = clock();
- Mio_Library_t * pLib = Abc_FrameReadLibGen();
+ Mio_Library_t * pLib = (Mio_Library_t *)Abc_FrameReadLibGen();
assert( Abc_NtkIsStrash(pNtk) );
@@ -102,9 +102,9 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, double AreaMulti,
// return the library to normal
if ( AreaMulti != 0.0 )
- Mio_LibraryMultiArea( Abc_FrameReadLibGen(), -AreaMulti );
+ Mio_LibraryMultiArea( (Mio_Library_t *)Abc_FrameReadLibGen(), -AreaMulti );
if ( DelayMulti != 0.0 )
- Mio_LibraryMultiDelay( Abc_FrameReadLibGen(), -DelayMulti );
+ Mio_LibraryMultiDelay( (Mio_Library_t *)Abc_FrameReadLibGen(), -DelayMulti );
// print a warning about choice nodes
if ( Abc_NtkGetChoiceNum( pNtk ) )
diff --git a/src/base/abci/abcRec2.c b/src/base/abci/abcRec2.c
index c84ea3ea..460fe71d 100644
--- a/src/base/abci/abcRec2.c
+++ b/src/base/abci/abcRec2.c
@@ -163,7 +163,7 @@ static inline int Rec_AppendObj( Abc_ManRec_t2 * p, Rec_Obj_t2 ** pObj )
if ( p->nRecObjs == p->nRecObjsAlloc )
{
assert( p->nRecObjs > 0 );
- p->pRecObjs = realloc(p->pRecObjs, 2 * p->nRecObjsAlloc * p->recObjSize );
+ p->pRecObjs = ABC_REALLOC( char, p->pRecObjs, 2 * p->nRecObjsAlloc * p->recObjSize );
memset( p->pRecObjs + p->nRecObjsAlloc * p->recObjSize, 0, p->recObjSize * p->nRecObjsAlloc );
p->nRecObjsAlloc *= 2;
hasRealloced = 1;
@@ -2177,7 +2177,7 @@ void Abc_NtkRecCutTruthFromLib2( Gia_Man_t * pGia2, Vec_Ptr_t * vNodes, int nLea
Vec_PtrForEachEntry( Gia_Obj_t *, vNodes, pObj, i )
{
Gia_ObjSetCopyF(pGia2, 0, pObj, i);
- pSims = Vec_PtrEntry(vTtTemps, i);
+ pSims = (unsigned *)Vec_PtrEntry(vTtTemps, i);
if ( i < nLeaves )
{
Kit_TruthCopy( pSims, (unsigned *)Vec_PtrEntry(vTtElems, i), nInputs );
diff --git a/src/base/abci/abcTim.c b/src/base/abci/abcTim.c
index a9cc4b96..35f1186d 100644
--- a/src/base/abci/abcTim.c
+++ b/src/base/abci/abcTim.c
@@ -385,11 +385,11 @@ void Abc_NtkTestTim( Abc_Ntk_t * pNtk, int fVerbose )
// create GIA manager (pGia) with hierarhy/timing manager attached (pGia->pManTime)
// while assuming that some nodes are white boxes (see Abc_NodeIsWhiteBox)
pGia = Abc_NtkTestTimDeriveGia( pNtk, fVerbose );
- printf( "Created GIA manager for network with %d white boxes.\n", Tim_ManBoxNum(pGia->pManTime) );
+ printf( "Created GIA manager for network with %d white boxes.\n", Tim_ManBoxNum((Tim_Man_t *)pGia->pManTime) );
// print the timing manager
if ( fVerbose )
- Tim_ManPrint( pGia->pManTime );
+ Tim_ManPrint( (Tim_Man_t *)pGia->pManTime );
// test writing both managers into a file and reading them back
Abc_NtkTestTimByWritingFile( pGia, "test1.aig" );
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index bb031200..72f5c9dc 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -607,7 +607,7 @@ int Io_ReadBlifReorderFormalNames( Vec_Ptr_t * vTokens, Mio_Gate_t * pGate, Mio_
pName = (char *)Vec_PtrEntry(vTokens, nSize - 1);
if ( !strncmp( pNamePin, pName, Length ) && pName[Length] == '=' ) // the last entry is pTwin
{
- pName = Vec_PtrPop( vTokens );
+ pName = (char *)Vec_PtrPop( vTokens );
Vec_PtrPush( vTokens, NULL );
Vec_PtrPush( vTokens, pName );
return 1;
diff --git a/src/bool/lucky/luckyInt.h b/src/bool/lucky/luckyInt.h
index 4801b961..f236693c 100644
--- a/src/bool/lucky/luckyInt.h
+++ b/src/bool/lucky/luckyInt.h
@@ -24,13 +24,16 @@
#include <math.h>
#include <time.h>
-
// comment out this line to run Lucky Code outside of ABC
#define _RUNNING_ABC_
#ifdef _RUNNING_ABC_
+
#include "misc/util/abc_global.h"
+#include "lucky.h"
+
#else
+
#define ABC_NAMESPACE_HEADER_START
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_IMPL_START
@@ -42,6 +45,18 @@ typedef unsigned __int64 word;
#define inline __inline // compatible with MS VS 6.0
#define ABC_ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
// #define LUCKY_VERIFY
+
+typedef struct
+{
+ int varN;
+ int* swapArray;
+ int swapCtr;
+ int totalSwaps;
+ int* flipArray;
+ int flipCtr;
+ int totalFlips;
+}permInfo;
+
#endif
@@ -71,17 +86,6 @@ typedef struct
int positionToSwap2;
} swapInfo;
-typedef struct
-{
- int varN;
- int* swapArray;
- int swapCtr;
- int totalSwaps;
- int* flipArray;
- int flipCtr;
- int totalFlips;
-}permInfo;
-
static inline void TimePrint( char* Message )
{
diff --git a/src/bool/lucky/luckySwapIJ.c b/src/bool/lucky/luckySwapIJ.c
index 9901f9cb..d1170f45 100644
--- a/src/bool/lucky/luckySwapIJ.c
+++ b/src/bool/lucky/luckySwapIJ.c
@@ -76,7 +76,7 @@ void swap_ij_case3( word* f,int totalVars, int i, int j)
shift = (wwj - wwi)/2;
WORDS_IN_TT = Kit_TruthWordNum_64bit(totalVars);
SizeOfBlock = sizeof(word)*wwi/2;
- temp = malloc(SizeOfBlock);
+ temp = (word *)malloc(SizeOfBlock);
for(y=wwj/2; y<WORDS_IN_TT; y+=wwj)
for(x=y-shift; x<y; x+=wwi)
{
diff --git a/src/map/mapper/mapperTree.c b/src/map/mapper/mapperTree.c
index 9bf74ff2..8c23417c 100644
--- a/src/map/mapper/mapperTree.c
+++ b/src/map/mapper/mapperTree.c
@@ -162,7 +162,7 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam
}
pLibName = strtok( pTemp, " \t\r\n" );
- pLib->pGenlib = Abc_FrameReadLibGen();
+ pLib->pGenlib = (Mio_Library_t *)Abc_FrameReadLibGen();
if ( pLib->pGenlib == NULL || strcmp( Mio_LibraryReadName(pLib->pGenlib), pLibName ) )
{
printf( "Supergate library \"%s\" requires the use of genlib library \"%s\".\n", pFileName, pLibName );
@@ -410,7 +410,7 @@ int Map_LibraryReadFileTreeStr( Map_SuperLib_t * pLib, Vec_Str_t * vStr, char *
}
pLibName = strtok( pTemp, " \t\r\n" );
- pLib->pGenlib = Abc_FrameReadLibGen();
+ pLib->pGenlib = (Mio_Library_t *)Abc_FrameReadLibGen();
// if ( pLib->pGenlib == NULL || strcmp( , pLibName ) )
if ( pLib->pGenlib == NULL || Map_LibraryCompareLibNames(Mio_LibraryReadName(pLib->pGenlib), pLibName) )
{
diff --git a/src/map/scl/scl.c b/src/map/scl/scl.c
index ee474c7d..f5c9d914 100644
--- a/src/map/scl/scl.c
+++ b/src/map/scl/scl.c
@@ -120,7 +120,7 @@ int Scl_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
// read new library
Abc_SclLoad( pFileName, (SC_Lib **)&pAbc->pLibScl );
if ( fVerbose )
- Abc_SclWriteText( "scl_out.txt", pAbc->pLibScl );
+ Abc_SclWriteText( "scl_out.txt", (SC_Lib *)pAbc->pLibScl );
return 0;
usage:
@@ -221,7 +221,7 @@ int Scl_CommandPrint( Abc_Frame_t * pAbc, int argc, char **argv )
}
// save current library
- Abc_SclPrintCells( pAbc->pLibScl );
+ Abc_SclPrintCells( (SC_Lib *)pAbc->pLibScl );
return 0;
usage:
@@ -274,7 +274,7 @@ int Scl_CommandPrintGS( Abc_Frame_t * pAbc, int argc, char **argv )
}
// save current library
- Abc_SclPrintGateSizes( pAbc->pLibScl, Abc_FrameReadNtk(pAbc) );
+ Abc_SclPrintGateSizes( (SC_Lib *)pAbc->pLibScl, Abc_FrameReadNtk(pAbc) );
return 0;
usage:
@@ -344,7 +344,7 @@ int Scl_CommandStime( Abc_Frame_t * pAbc, int argc, char **argv )
return 1;
}
- Abc_SclTimePerform( pAbc->pLibScl, Abc_FrameReadNtk(pAbc), fUseWireLoads, fShowAll, fShort );
+ Abc_SclTimePerform( (SC_Lib *)pAbc->pLibScl, Abc_FrameReadNtk(pAbc), fUseWireLoads, fShowAll, fShort );
return 0;
usage:
@@ -611,7 +611,7 @@ int Scl_CommandGsize( Abc_Frame_t * pAbc, int argc, char **argv )
return 1;
}
- Abc_SclSizingPerform( pAbc->pLibScl, Abc_FrameReadNtk(pAbc), pPars );
+ Abc_SclSizingPerform( (SC_Lib *)pAbc->pLibScl, Abc_FrameReadNtk(pAbc), pPars );
return 0;
usage:
@@ -717,7 +717,7 @@ int Scl_CommandUpsize( Abc_Frame_t * pAbc, int argc, char **argv )
return 1;
}
- Abc_SclUpsizePerform( pAbc->pLibScl, pNtk, Window, Ratio, nIters, fVerbose );
+ Abc_SclUpsizePerform( (SC_Lib *)pAbc->pLibScl, pNtk, Window, Ratio, nIters, fVerbose );
return 0;
usage:
@@ -782,7 +782,7 @@ int Scl_CommandMinsize( Abc_Frame_t * pAbc, int argc, char **argv )
return 1;
}
- Abc_SclMinsizePerform( pAbc->pLibScl, pNtk, fVerbose );
+ Abc_SclMinsizePerform( (SC_Lib *)pAbc->pLibScl, pNtk, fVerbose );
return 0;
usage:
diff --git a/src/map/scl/sclBuff.c b/src/map/scl/sclBuff.c
index 5a438cd4..808cd1ec 100644
--- a/src/map/scl/sclBuff.c
+++ b/src/map/scl/sclBuff.c
@@ -136,7 +136,7 @@ Abc_Obj_t * Abc_SclPerformBufferingOne( Abc_Obj_t * pObj, int Degree, int fVerbo
// collect fanouts and sort by reverse level
vFanouts = Vec_PtrAlloc( Abc_ObjFanoutNum(pObj) );
Abc_NodeCollectFanouts( pObj, vFanouts );
- Vec_PtrSort( vFanouts, Abc_NodeCompareLevels );
+ Vec_PtrSort( vFanouts, (int (*)(void))Abc_NodeCompareLevels );
// select the first Degree fanouts
pBuffer = Abc_NtkCreateNodeBuf( pObj->pNtk, NULL );
// check if it is possible to not increase level
diff --git a/src/map/scl/sclInt.h b/src/map/scl/sclInt.h
index bf2ee0f5..9474e24d 100644
--- a/src/map/scl/sclInt.h
+++ b/src/map/scl/sclInt.h
@@ -198,8 +198,8 @@ static inline SC_Cell * SC_LibCell( SC_Lib * p, int i ) { return (SC_
static inline SC_Pin * SC_CellPin( SC_Cell * p, int i ) { return (SC_Pin *)Vec_PtrEntry(p->vPins, i); }
static inline Vec_Wrd_t * SC_CellFunc( SC_Cell * p ) { return SC_CellPin(p, p->n_inputs)->vFunc; }
-static inline double SC_LibCapFf( SC_Lib * p, double cap ) { return cap * p->unit_cap_fst * pow(10, 15 - p->unit_cap_snd); }
-static inline double SC_LibTimePs( SC_Lib * p, double time ) { return time * pow(10, 12 - p->unit_time); }
+static inline double SC_LibCapFf( SC_Lib * p, double cap ) { return cap * p->unit_cap_fst * pow(10.0, 15 - p->unit_cap_snd); }
+static inline double SC_LibTimePs( SC_Lib * p, double time ) { return time * pow(10.0, 12 - p->unit_time); }
#define SC_LibForEachCell( p, pCell, i ) Vec_PtrForEachEntry( SC_Cell *, p->vCells, pCell, i )
#define SC_LibForEachCellClass( p, pCell, i ) Vec_PtrForEachEntry( SC_Cell *, p->vCellClasses, pCell, i )
diff --git a/src/map/scl/sclUtil.c b/src/map/scl/sclUtil.c
index f3a88e72..6a1f6a36 100644
--- a/src/map/scl/sclUtil.c
+++ b/src/map/scl/sclUtil.c
@@ -20,6 +20,7 @@
#include "sclInt.h"
#include "map/mio/mio.h"
+#include "bool/kit/kit.h"
ABC_NAMESPACE_IMPL_START
@@ -135,7 +136,7 @@ void Abc_SclLinkCells( SC_Lib * p )
Vec_PtrPush( vList, pCell );
qsort( (void *)Vec_PtrArray(vList), Vec_PtrSize(vList), sizeof(void *), (int(*)(const void *,const void *))Abc_SclCompareCells );
// create new representative
- pRepr = Vec_PtrEntry( vList, 0 );
+ pRepr = (SC_Cell *)Vec_PtrEntry( vList, 0 );
pRepr->pNext = pRepr->pPrev = pRepr;
pRepr->Order = 0;
// relink cells
@@ -152,7 +153,6 @@ void Abc_SclLinkCells( SC_Lib * p )
}
void Abc_SclPrintCells( SC_Lib * p )
{
- extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
SC_Cell * pCell, * pRepr;
int i, k, j, nLength = 0;
assert( Vec_PtrSize(p->vCellClasses) > 0 );
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index 997c026e..03474a04 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -264,6 +264,12 @@ enum Abc_VerbLevel
ABC_VERBOSE = 2
};
+// string printing
+extern char * vnsprintf(const char* format, va_list args);
+extern char * nsprintf(const char* format, ...);
+extern int Gia_ManToBridgeText( FILE * pFile, int Size, unsigned char * pBuffer );
+
+// misc printing procedures
static inline void Abc_Print( int level, const char * format, ... )
{
extern ABC_DLL int Abc_FrameIsBridgeMode();
@@ -275,8 +281,6 @@ static inline void Abc_Print( int level, const char * format, ... )
va_start( args, format );
if ( Abc_FrameIsBridgeMode() )
{
- extern int Gia_ManToBridgeText( FILE * pFile, int Size, unsigned char * pBuffer );
- extern char * vnsprintf(const char* format, va_list args);
char * tmp = vnsprintf( format, args );
Gia_ManToBridgeText( stdout, strlen(tmp), (unsigned char*)tmp );
free( tmp );
@@ -362,9 +366,6 @@ extern void Abc_QuickSort3( word * pData, int nSize, int fDecrease );
extern void Abc_QuickSortCostData( int * pCosts, int nSize, int fDecrease, word * pData, int * pResult );
extern int * Abc_QuickSortCost( int * pCosts, int nSize, int fDecrease );
-// string printing
-extern char * vnsprintf(const char* format, va_list args);
-extern char * nsprintf(const char* format, ...);
ABC_NAMESPACE_HEADER_END
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 2b2cb8ea..698ab377 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -18,9 +18,10 @@
***********************************************************************/
+#include "base/main/main.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver2.h"
-#include "base/main/main.h"
+#include "bool/kit/kit.h"
#include "abs.h"
#include "absRef.h"
//#include "absRef2.h"
@@ -83,8 +84,8 @@ struct Ga2_Man_t_
static inline int Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj)); }
static inline void Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i); }
-static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj) ); }
-static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)+1 ); }
+static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return (Vec_Int_t *)Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj) ); }
+static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return (Vec_Int_t *)Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)+1 ); }
static inline int Ga2_ObjIsAbs0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return Ga2_ObjId(p,pObj) >= 0 && Ga2_ObjId(p,pObj) < p->LimAbs; }
static inline int Ga2_ObjIsLeaf0( Ga2_Man_t * p, Gia_Obj_t * pObj ) { assert(Ga2_ObjId(p,pObj) >= 0); return Ga2_ObjId(p,pObj) >= p->LimAbs && Ga2_ObjId(p,pObj) < p->LimPpi; }
@@ -628,7 +629,6 @@ if ( fVerbose )
***********************************************************************/
Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover )
{
- extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
int RetValue;
assert( nVars <= 5 );
// transform truth table into the SOP
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index 74393a5b..951940b3 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -1552,8 +1552,10 @@ void sat_solver2_reducedb(sat_solver2* s)
// compact proof (compacts 'proofs' and update 'claProofs')
if ( s->pPrf1 )
+ {
+ extern int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot );
s->hProofPivot = Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
-
+ }
// report the results
TimeTotal += clock() - clk;
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h
index a1539637..8c32cbde 100644
--- a/src/sat/bsat/satSolver2.h
+++ b/src/sat/bsat/satSolver2.h
@@ -70,7 +70,6 @@ extern void var_set_partA (sat_solver2* s, int v, int partA);
extern void * Sat_ProofCore( sat_solver2 * s );
extern void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars );
extern word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars );
-extern int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot );
extern void Sat_ProofCheck( sat_solver2 * s );
//=================================================================================================
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 02:42:35 +0000