Silencing some of the gcc warnings.

20 files changed, 22 insertions, 31 deletions

diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c
index a5ec7dac..b2e61e61 100644
--- a/src/aig/saig/saigAbsStart.c
+++ b/src/aig/saig/saigAbsStart.c
@@ -246,7 +246,7 @@ Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars )
     int nUseStart = 0;
     Aig_Man_t * pAbs, * pTemp;
     Vec_Int_t * vFlops;
-    int Iter, clk = clock(), clk2 = clock();//, iFlop;
+    int Iter;//, clk = clock(), clk2 = clock();//, iFlop;
     assert( Aig_ManRegNum(p) > 0 );
     if ( pPars->fVerbose )
         printf( "Performing counter-example-based refinement.\n" );
diff --git a/src/aig/saig/saigCexMin.c b/src/aig/saig/saigCexMin.c
index 2e8e9cdc..4b219cac 100644
--- a/src/aig/saig/saigCexMin.c
+++ b/src/aig/saig/saigCexMin.c
@@ -322,7 +322,6 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC
     nPrioOffset = pCex->nRegs;
     Aig_ManConst1(pAig)->iData = Abc_Var2Lit( nPrioOffset + (pCex->iFrame + 1) * pCex->nPis, 1 );
     vRoots = Vec_IntAlloc( 1000 );
-//printf( "Const1 = %d  Offset = %d\n", Aig_ManConst1(pAig)->iData, nPrioOffset ); 
     for ( f = 0; f <= pCex->iFrame; f++ )
     {
         int nPiCount = 0;
@@ -338,14 +337,8 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC
             else if ( f == 0 )
                 Vec_IntPush( vFramePPsOne, Abc_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) );
             else
-            {
-                Aig_Obj_t * pObj0 = Saig_ObjLoToLi(pAig, pObj);
-                int Value = Saig_ObjLoToLi(pAig, pObj)->iData;
                 Vec_IntPush( vFramePPsOne, Saig_ObjLoToLi(pAig, pObj)->iData );
-            }
-//printf( "%d ", Vec_IntEntryLast(vFramePPsOne) );
         }
-//printf( "\n" );
         // compute the PP info
         Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
     }
diff --git a/src/aig/saig/saigConstr.c b/src/aig/saig/saigConstr.c
index 91bdf46f..fe7363b0 100644
--- a/src/aig/saig/saigConstr.c
+++ b/src/aig/saig/saigConstr.c
@@ -273,7 +273,7 @@ Vec_Ptr_t * Saig_ManDetectConstrCheckCont( Vec_Ptr_t * vSuper, Vec_Ptr_t * vSupe
 ***********************************************************************/
 int Saig_ManDetectConstr( Aig_Man_t * p, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvCons )
 {
-    Vec_Ptr_t * vSuper, * vSuper2, * vUnique;
+    Vec_Ptr_t * vSuper, * vSuper2 = NULL, * vUnique;
     Aig_Obj_t * pObj, * pObj2, * pFlop;
     int i, nFlops, RetValue;
     *pvOuts = NULL;
diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c
index e60d1b82..cb43c5a2 100644
--- a/src/aig/saig/saigConstr2.c
+++ b/src/aig/saig/saigConstr2.c
@@ -202,7 +202,7 @@ int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerb
         Saig_ManForEachPo( p, pObj, i )
         {
             if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) )
-                printf( "Primary output :  ", i );
+                printf( "Primary output :  " );
             else
                 printf( "Constraint %3d :  ", i-(Saig_ManPoNum(p) - Saig_ManConstrNum(p))  );
             printf( "ProbOne = %f  ",  (float)Vec_IntEntry(vProbs,  i)/(32*nWords*nFrames) );
diff --git a/src/aig/saig/saigGlaCba.c b/src/aig/saig/saigGlaCba.c
index d6af6e47..d1efca0b 100644
--- a/src/aig/saig/saigGlaCba.c
+++ b/src/aig/saig/saigGlaCba.c
@@ -246,7 +246,7 @@ Aig_Man_t * Aig_Gla1DeriveAbs( Aig_Gla1Man_t * p )
 { 
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj;
-    int i, nFlops = 0, RetValue;
+    int i, RetValue;
     assert( Saig_ManPoNum(p->pAig) == 1 );
     // start the new manager
     pNew = Aig_ManStart( 5000 );
diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c
index c22cf415..cdc91759 100644
--- a/src/aig/saig/saigGlaPba.c
+++ b/src/aig/saig/saigGlaPba.c
@@ -451,7 +451,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
     }
     if ( fVerbose )
     {
-        printf( "SAT solver returned UNSAT after %7d conflicts.      ", pSat->stats.conflicts );
+        printf( "SAT solver returned UNSAT after %7d conflicts.      ", (int)pSat->stats.conflicts );
         Abc_PrintTime( 1, "Time", clock() - clk );
     }
     assert( RetValue == l_False );
diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c
index 4fa0012d..8417cbf5 100644
--- a/src/aig/saig/saigGlaPba2.c
+++ b/src/aig/saig/saigGlaPba2.c
@@ -412,7 +412,7 @@ Vec_Int_t * Aig_Gla3ManUnsatCore( sat_solver2 * pSat, int nConfMax, int fVerbose
     }
     if ( fVerbose )
     {
-        printf( "SAT solver returned UNSAT after %7d conflicts.      ", pSat->stats.conflicts );
+        printf( "SAT solver returned UNSAT after %7d conflicts.      ", (int)pSat->stats.conflicts );
         Abc_PrintTime( 1, "Time", clock() - clk );
     }
     assert( RetValue == l_False );
diff --git a/src/aig/saig/saigInd.c b/src/aig/saig/saigInd.c
index c9043ba2..33146077 100644
--- a/src/aig/saig/saigInd.c
+++ b/src/aig/saig/saigInd.c
@@ -150,7 +150,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique,
     Vec_Int_t * vTopVarNums, * vState, * vTopVarIds = NULL;
     Vec_Ptr_t * vTop, * vBot;
     Aig_Obj_t * pObjPi, * pObjPiCopy, * pObjPo;
-    int i, k, f, clk, Lits[2], status, RetValue, nSatVarNum, nConfPrev;
+    int i, k, f, clk, Lits[2], status = -1, RetValue, nSatVarNum, nConfPrev;
     int nOldSize, iReg, iLast, fAdded, nConstrs = 0, nClauses = 0;
     assert( fUnique == 0 || fUniqueAll == 0 );
     assert( Saig_ManPoNum(p) == 1 );
@@ -287,7 +287,7 @@ nextrun:
         {
             printf( "%4d : PI =%5d. PO =%5d. AIG =%5d. Var =%7d. Clau =%7d. Conf =%7d. ",
                 f, Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart), Aig_ManNodeNum(pAigPart), 
-                nSatVarNum, nClauses, pSat->stats.conflicts-nConfPrev );
+                nSatVarNum, nClauses, (int)pSat->stats.conflicts-nConfPrev );
             ABC_PRT( "Time", clock() - clk );
         }
         if ( status == l_Undef )
diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c
index ad6a9496..0e7c9de1 100644
--- a/src/aig/saig/saigIso.c
+++ b/src/aig/saig/saigIso.c
@@ -421,7 +421,7 @@ int Iso_StoCompareVecStr( Vec_Str_t ** p1, Vec_Str_t ** p2 )
 ***********************************************************************/
 Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose )
 {
-    int fVeryVerbose = 0;
+//    int fVeryVerbose = 0;
     Aig_Man_t * pPart, * pTemp;
     Vec_Ptr_t * vBuffers, * vClasses;
     Vec_Int_t * vLevel, * vRemain;
diff --git a/src/aig/saig/saigIsoFast.c b/src/aig/saig/saigIsoFast.c
index 6556b90f..a415dcc8 100644
--- a/src/aig/saig/saigIsoFast.c
+++ b/src/aig/saig/saigIsoFast.c
@@ -181,7 +181,7 @@ Vec_Int_t * Iso_StoCollectInfo( Iso_Sto_t * p, Aig_Obj_t * pPo )
     Aig_Man_t * pAig = p->pAig;
     Aig_Obj_t * pObj;
     int i, Value, Entry, * pPerm;
-    int clk = clock();
+//    int clk = clock();
 
     assert( Aig_ObjIsPo(pPo) );
 
diff --git a/src/aig/saig/saigIsoSlow.c b/src/aig/saig/saigIsoSlow.c
index 9279931f..6ec74112 100644
--- a/src/aig/saig/saigIsoSlow.c
+++ b/src/aig/saig/saigIsoSlow.c
@@ -318,7 +318,7 @@ Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig )
     Iso_Man_t * p;
     Iso_Obj_t * pIso;
     Aig_Obj_t * pObj;
-    int i, nNodes = 0, nEdges = 0;
+    int i;//, nNodes = 0, nEdges = 0;
     p = Iso_ManStart( pAig );
     Aig_ManForEachObj( pAig, pObj, i )
     {
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c
index 20dbeec7..7fde61b1 100644
--- a/src/aig/saig/saigMiter.c
+++ b/src/aig/saig/saigMiter.c
@@ -608,8 +608,8 @@ int Saig_ManDemiterCheckPo( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t ** ppPo0,
     // make sure they can reach only one
     pObjR0 = Aig_Regular(pObj0);
     pObjR1 = Aig_Regular(pObj1);
-    if ( pObjR0->fMarkA && pObjR0->fMarkB || pObjR1->fMarkA && pObjR1->fMarkB || 
-         pObjR0->fMarkA && pObjR1->fMarkA || pObjR0->fMarkB && pObjR1->fMarkB )
+    if ( (pObjR0->fMarkA && pObjR0->fMarkB) || (pObjR1->fMarkA && pObjR1->fMarkB) || 
+         (pObjR0->fMarkA && pObjR1->fMarkA) || (pObjR0->fMarkB && pObjR1->fMarkB) )
          return 0;
 
     if ( pObjR1->fMarkA && !pObjR0->fMarkA )
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index 4107c5a2..637da63e 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -259,7 +259,7 @@ Vec_Int_t * Saig_TsiComputeTransient( Saig_Tsim_t * p, int nPref )
 {
     Vec_Int_t * vCounters;
     unsigned * pState;
-    int ValueThis, ValuePrev = -1, StepPrev = -1;
+    int ValueThis = -1, ValuePrev = -1, StepPrev = -1;
     int i, k, nRegs = p->pAig->nRegs;
     vCounters = Vec_IntStart( nPref );
     for ( i = 0; i < nRegs; i++ )
diff --git a/src/aig/saig/saigRefSat.c b/src/aig/saig/saigRefSat.c
index 632ad354..dcd95d36 100644
--- a/src/aig/saig/saigRefSat.c
+++ b/src/aig/saig/saigRefSat.c
@@ -508,7 +508,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder )
     Aig_Obj_t * pObj;
     Vec_Vec_t * vLits = NULL;
     Vec_Int_t * vAssumps, * vVar2PiId;
-    int i, k, f = 0, Entry, RetValue, Counter = 0;
+    int i, k, Entry, RetValue;//, f = 0, Counter = 0;
     int nCoreLits, * pCoreLits;
     int clk = clock();
     // create CNF
@@ -551,8 +551,6 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder )
     vAssumps = Vec_IntAlloc( Aig_ManPiNum(p->pFrames) );
     Aig_ManForEachPi( p->pFrames, pObj, i )
     {
-        int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
-        int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
 //        RetValue = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
 //        Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) );
         Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) );
diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c
index 021481b9..1b48d58b 100644
--- a/src/aig/saig/saigSimExt.c
+++ b/src/aig/saig/saigSimExt.c
@@ -149,7 +149,7 @@ int Saig_ManExtendOne( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo,
     int iPi, int iFrame, Vec_Int_t * vUndo, Vec_Int_t * vVis, Vec_Int_t * vVis2 )
 {
     Aig_Obj_t * pFanout, * pObj = Aig_ManPi(p, iPi);
-    int i, k, f, iFanout, Value, Value2, Entry;
+    int i, k, f, iFanout = -1, Value, Value2, Entry;
     // save original value
     Value = Saig_ManSimInfoGet( vSimInfo, pObj, iFrame );
     assert( Value == SAIG_ZER || Value == SAIG_ONE );
diff --git a/src/aig/saig/saigSimExt2.c b/src/aig/saig/saigSimExt2.c
index 858c2b3b..fbd06ac7 100644
--- a/src/aig/saig/saigSimExt2.c
+++ b/src/aig/saig/saigSimExt2.c
@@ -173,7 +173,7 @@ int Saig_ManSimDataInit2( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo
 void Saig_ManSetAndDriveImplications_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f, int fMax, Vec_Ptr_t * vSimInfo )
 {
     Aig_Obj_t * pFanout;
-    int k, iFanout, Value0, Value1;
+    int k, iFanout = -1, Value0, Value1;
     int Value = Saig_ManSimInfo2Get( vSimInfo, pObj, f );
     assert( !Saig_ManSimInfo2IsOld( Value ) );
     Saig_ManSimInfo2Set( vSimInfo, pObj, f, Saig_ManSimInfo2SetOld(Value) );
diff --git a/src/aig/saig/saigSimFast.c b/src/aig/saig/saigSimFast.c
index b8eed19e..e8e47a66 100644
--- a/src/aig/saig/saigSimFast.c
+++ b/src/aig/saig/saigSimFast.c
@@ -348,7 +348,7 @@ Vec_Int_t * Faig_ManComputeSwitchProbs4( Aig_Man_t * p, int nFrames, int nPref,
     Vec_Int_t * vSwitching;
     int * pProbs;
     float * pSwitching;
-    int nFramesReal, clk, clkTotal = clock();
+    int nFramesReal, clk;//, clkTotal = clock();
     if ( fProbOne )
         fTrans = 0;
     vSwitching = Vec_IntStart( Aig_ManObjNumMax(p) );
diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c
index 6579c37b..f22dfdc8 100644
--- a/src/aig/saig/saigSimMv.c
+++ b/src/aig/saig/saigSimMv.c
@@ -572,7 +572,7 @@ void Saig_MvManPostProcess( Saig_MvMan_t * p, int iState )
 {
     Saig_MvObj_t * pEntry;
     unsigned * pState;
-    int i, k, j, nTotal = 0, Counter = 0, iFlop;
+    int i, k, j, nTotal = 0, iFlop;
     Vec_Int_t * vUniques = Vec_IntAlloc( 100 );
     Vec_Int_t * vCounter = Vec_IntAlloc( 100 );
     // count registers that never became undef
diff --git a/src/aig/saig/saigStrSim.c b/src/aig/saig/saigStrSim.c
index cdf177d0..06890c7a 100644
--- a/src/aig/saig/saigStrSim.c
+++ b/src/aig/saig/saigStrSim.c
@@ -719,7 +719,7 @@ void Saig_StrSimSetContiguousMatching( Aig_Man_t * p0, Aig_Man_t * p1 )
 void Ssw_StrSimMatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes )
 {
     Aig_Obj_t * pNext, * pObj;
-    int i, k, iFan;
+    int i, k, iFan = -1;
     Vec_PtrClear( vNodes );
     Aig_ManIncrementTravId( p );
     Aig_ManForEachObj( p, pObj, i )
diff --git a/src/aig/saig/saigSwitch.c b/src/aig/saig/saigSwitch.c
index 01411c05..832d674b 100644
--- a/src/aig/saig/saigSwitch.c
+++ b/src/aig/saig/saigSwitch.c
@@ -268,7 +268,7 @@ Vec_Int_t * Saig_ManComputeSwitchProb4s( Aig_Man_t * p, int nFrames, int nPref,
     Saig_SimObj_t * pAig, * pEntry;
     Vec_Int_t * vSwitching;
     float * pSwitching;
-    int nFramesReal, clk, clkTotal = clock();
+    int nFramesReal, clk;//, clkTotal = clock();
     vSwitching = Vec_IntStart( Aig_ManObjNumMax(p) );
     pSwitching = (float *)vSwitching->pArray;
 clk = clock();
@@ -557,7 +557,7 @@ Aig_CMan_t * Aig_CManCreate( Aig_Man_t * p )
         Aig_CManAddPo( pCMan, 
             (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj) ); 
     printf( "\nBytes alloc = %5d.  Bytes used = %7d.  Ave per node = %4.2f. \n", 
-        pCMan->nBytes, pCMan->pCur - pCMan->Data, 
+        pCMan->nBytes, (int)(pCMan->pCur - pCMan->Data), 
         1.0 * (pCMan->pCur - pCMan->Data) / (pCMan->nNodes + pCMan->nOuts ) );
 //    Aig_CManStop( pCMan );
     return pCMan;