summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2021-09-26 11:30:54 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2021-09-26 11:30:54 -0700
commitba64e78608064612db61d6515f19dd2cabe69cee (patch)
treed4df3672f9d056a010244711f73c848e020168e8 /src/proof
parent2ce1ce8bed69623de58d9394e22a3a8812096561 (diff)
downloadabc-ba64e78608064612db61d6515f19dd2cabe69cee.tar.gz
abc-ba64e78608064612db61d6515f19dd2cabe69cee.tar.bz2
abc-ba64e78608064612db61d6515f19dd2cabe69cee.zip
Changing declaration of Vec_Ptr_t sorting function to satisfy some compilers.
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/abs/absVta.c4
-rw-r--r--src/proof/dch/dchSimSat.c4
-rw-r--r--src/proof/pdr/pdrCore.c4
-rw-r--r--src/proof/pdr/pdrIncr.c4
-rw-r--r--src/proof/pdr/pdrInv.c6
5 files changed, 11 insertions, 11 deletions
diff --git a/src/proof/abs/absVta.c b/src/proof/abs/absVta.c
index 597e4b72..b6001d3f 100644
--- a/src/proof/abs/absVta.c
+++ b/src/proof/abs/absVta.c
@@ -705,8 +705,8 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
// objects with equal distance should receive priority based on number
// those objects whose prototypes have been added in other timeframes
// should have higher priority than the current object
- Vec_PtrSort( vTermsUsed, (int (*)(void))Vta_ManComputeDepthIncrease );
- Vec_PtrSort( vTermsUnused, (int (*)(void))Vta_ManComputeDepthIncrease );
+ Vec_PtrSort( vTermsUsed, (int (*)(const void *, const void *))Vta_ManComputeDepthIncrease );
+ Vec_PtrSort( vTermsUnused, (int (*)(const void *, const void *))Vta_ManComputeDepthIncrease );
if ( Vec_PtrSize(vTermsUsed) > 1 )
{
pThis0 = (Vta_Obj_t *)Vec_PtrEntry(vTermsUsed, 0);
diff --git a/src/proof/dch/dchSimSat.c b/src/proof/dch/dchSimSat.c
index d3dbbe16..bbab0529 100644
--- a/src/proof/dch/dchSimSat.c
+++ b/src/proof/dch/dchSimSat.c
@@ -91,8 +91,8 @@ void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2
Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );
Dch_ManCollectTfoCands_rec( p, pObj1 );
Dch_ManCollectTfoCands_rec( p, pObj2 );
- Vec_PtrSort( p->vSimRoots, (int (*)(void))Aig_ObjCompareIdIncrease );
- Vec_PtrSort( p->vSimClasses, (int (*)(void))Aig_ObjCompareIdIncrease );
+ Vec_PtrSort( p->vSimRoots, (int (*)(const void *, const void *))Aig_ObjCompareIdIncrease );
+ Vec_PtrSort( p->vSimClasses, (int (*)(const void *, const void *))Aig_ObjCompareIdIncrease );
Vec_PtrForEachEntry( Aig_Obj_t *, p->vSimClasses, pObj, i )
pObj->fMarkA = 0;
}
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index f71569a3..d77fd4e1 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -157,7 +157,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
assert( p->iUseFrame > 0 );
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
{
- Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
vArrayK1 = Vec_VecEntry( p->vClauses, k+1 );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
{
@@ -216,7 +216,7 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
// clean up the last one
vArrayK = Vec_VecEntry( p->vClauses, kMax );
- Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
{
// remove cubes in the same frame that are contained by pCubeK
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c
index f4f2c8c8..9ca72ba6 100644
--- a/src/proof/pdr/pdrIncr.c
+++ b/src/proof/pdr/pdrIncr.c
@@ -47,7 +47,7 @@ Vec_Ptr_t * IPdr_ManPushClausesK( Pdr_Man_t * p, int k )
assert( Vec_VecSize(p->vClauses) == k + 1 );
vArrayK = Vec_VecEntry( p->vClauses, k );
- Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
vArrayK1 = Vec_PtrAlloc( 100 );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
{
@@ -117,7 +117,7 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs )
int i, k, Counter = 0;
Vec_VecForEachLevelStart( vClauses, vArrayK, k, kStart )
{
- Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
{
Abc_Print( 1, "Frame[%4d]Cube[%4d] = ", k, Counter++ );
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index ba4f0448..ae61ce2c 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -248,7 +248,7 @@ void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart )
int i, k, Counter = 0;
Vec_VecForEachLevelStart( p->vClauses, vArrayK, k, kStart )
{
- Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
{
Abc_Print( 1, "C=%4d. F=%4d ", Counter++, k );
@@ -370,7 +370,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
vCubes = Pdr_ManCollectCubes( p, kStart );
else
vCubes = Vec_PtrDup( p->vInfCubes );
- Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrSort( vCubes, (int (*)(const void *, const void *))Pdr_SetCompare );
// Pdr_ManDumpAig( p->pAig, vCubes );
// count cubes
Count = 0;
@@ -446,7 +446,7 @@ Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p )
vCubes = Pdr_ManCollectCubes( p, kStart );
else
vCubes = Vec_PtrDup( p->vInfCubes );
- Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
+ Vec_PtrSort( vCubes, (int (*)(const void *, const void *))Pdr_SetCompare );
// collect variable appearances
vFlopCounts = p->pPars->fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL;
// output cubes