summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/bdd/cudd/cuddReorder.c2
-rw-r--r--src/map/if/ifDec10.c2
-rw-r--r--src/map/if/ifDec16.c8
-rw-r--r--src/map/mapper/mapperTree.c2
-rw-r--r--src/map/mio/exp.h2
-rw-r--r--src/map/mio/mio.c4
-rw-r--r--src/proof/cec/cecIso.c2
-rw-r--r--src/proof/cec/cecSeq.c2
-rw-r--r--src/proof/fraig/fraigMan.c4
-rw-r--r--src/sat/bsat/satSolver2.c4
-rw-r--r--src/sat/msat/msatOrderH.c5
11 files changed, 19 insertions, 18 deletions
diff --git a/src/bdd/cudd/cuddReorder.c b/src/bdd/cudd/cuddReorder.c
index fef0768a..b7d91dd9 100644
--- a/src/bdd/cudd/cuddReorder.c
+++ b/src/bdd/cudd/cuddReorder.c
@@ -615,7 +615,7 @@ cuddSwapping(
int iterate;
int previousSize;
Move *moves, *move;
- int pivot;
+ int pivot = -1;
int modulo;
int result;
diff --git a/src/map/if/ifDec10.c b/src/map/if/ifDec10.c
index 85c8625d..917f9f53 100644
--- a/src/map/if/ifDec10.c
+++ b/src/map/if/ifDec10.c
@@ -480,7 +480,7 @@ printf( "\n" );
int If_CutPerformCheck10( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
{
int nSupp, fDerive = 0;
- word z[2] = {0}, pF[16];
+ word pF[16];
if ( nLeaves <= 6 )
return 1;
If_Dec10Copy( pF, (word *)pTruth, nVars );
diff --git a/src/map/if/ifDec16.c b/src/map/if/ifDec16.c
index e624f889..442e1fa1 100644
--- a/src/map/if/ifDec16.c
+++ b/src/map/if/ifDec16.c
@@ -2012,10 +2012,10 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
assert( G3.nVars == 0 );
for ( i = 0; i < nLeaves; i++ )
if ( !fUsed[i] )
- G3.pVars[G3.nVars++] = i;
- G3.pVars[G3.nVars++] = nLeaves;
+ G3.pVars[(int)G3.nVars++] = i;
+ G3.pVars[(int)G3.nVars++] = nLeaves;
if ( G2.nVars )
- G3.pVars[G3.nVars++] = nLeaves+1;
+ G3.pVars[(int)G3.nVars++] = nLeaves+1;
assert( G1.nVars + G2.nVars + G3.nVars == nLeaves +
(G1.nVars > 0) + (G2.nVars > 0) + (G1.nMyu > 2) + (G2.nMyu > 2) );
// what if both non-disjoint vars are the same???
@@ -2038,7 +2038,7 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
***********************************************************************/
int If_CutPerformCheck16( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
{
- If_Grp_t G1 = {0}, G2 = {0}, G3 = {0};
+ If_Grp_t G1 = {0}, G3 = {0};
int i, nLutLeaf, nLutLeaf2, nLutRoot, Length;
// quit if parameters are wrong
Length = strlen(pStr);
diff --git a/src/map/mapper/mapperTree.c b/src/map/mapper/mapperTree.c
index 542ff258..2244fa26 100644
--- a/src/map/mapper/mapperTree.c
+++ b/src/map/mapper/mapperTree.c
@@ -37,7 +37,7 @@ static int Map_LibraryGetMaxSuperPi_rec( Map_Super_t * pGate );
static unsigned Map_LibraryGetGateSupp_rec( Map_Super_t * pGate );
// fanout limits
-extern const int s_MapFanoutLimits[10] = { 1/*0*/, 10/*1*/, 5/*2*/, 2/*3*/, 1/*4*/, 1/*5*/, 1/*6*/ };
+static const int s_MapFanoutLimits[10] = { 1/*0*/, 10/*1*/, 5/*2*/, 2/*3*/, 1/*4*/, 1/*5*/, 1/*6*/ };
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
diff --git a/src/map/mio/exp.h b/src/map/mio/exp.h
index 40dff2e8..a76f33cb 100644
--- a/src/map/mio/exp.h
+++ b/src/map/mio/exp.h
@@ -153,7 +153,7 @@ static inline Vec_Int_t * Exp_Or( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int
}
static inline Vec_Int_t * Exp_Xor( int * pMan, int nVars, Vec_Int_t * p0, Vec_Int_t * p1 )
{
- int i, v = 0, Len0 = Vec_IntSize(p0), Len1 = Vec_IntSize(p1);
+ int i, Len0 = Vec_IntSize(p0), Len1 = Vec_IntSize(p1);
Vec_Int_t * r = Vec_IntAlloc( Len0 + Len1 + 5 );
assert( (Len0 & 1) && (Len1 & 1) );
Vec_IntPush( r, 2 * (nVars + Len0/2 + Len1/2 + 2) );
diff --git a/src/map/mio/mio.c b/src/map/mio/mio.c
index f7eddab2..a4596c9f 100644
--- a/src/map/mio/mio.c
+++ b/src/map/mio/mio.c
@@ -41,7 +41,7 @@ static int Mio_CommandPrintLibrary( Abc_Frame_t * pAbc, int argc, char **argv );
static int Mio_CommandReadLibrary2( Abc_Frame_t * pAbc, int argc, char **argv );
static int Mio_CommandPrintLibrary2( Abc_Frame_t * pAbc, int argc, char **argv );
-
+/*
// internal version of GENLIB library
static char * pMcncGenlib[25] = {
"GATE inv1 1 O=!a; PIN * INV 1 999 0.9 0.0 0.9 0.0\n",
@@ -66,7 +66,7 @@ static char * pMcncGenlib[25] = {
"GATE zero 0 O=CONST0;\n",
"GATE one 0 O=CONST1;\n"
};
-
+*/
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/cec/cecIso.c b/src/proof/cec/cecIso.c
index f1ca2ff7..990be5d1 100644
--- a/src/proof/cec/cecIso.c
+++ b/src/proof/cec/cecIso.c
@@ -170,7 +170,7 @@ static inline int Gia_ManIsoHashKey( int Id, unsigned * pStore, int nWords, int
static inline void Gia_ManIsoTableAdd( Gia_Man_t * p, int Id, unsigned * pStore, int nWords, int * pTable, int nTableSize )
{
Gia_Obj_t * pTemp;
- int Key, Ent, Counter = 0, Color = Gia_ObjColors( p, Id );
+ int Key, Ent, Color = Gia_ObjColors( p, Id );
assert( Color == 1 || Color == 2 );
Key = Gia_ManIsoHashKey( Id, pStore, nWords, nTableSize );
for ( Ent = pTable[Key], pTemp = (Ent ? Gia_ManObj(p, Ent) : NULL); pTemp;
diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c
index 21ed8656..2ccbe524 100644
--- a/src/proof/cec/cecSeq.c
+++ b/src/proof/cec/cecSeq.c
@@ -185,7 +185,7 @@ int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t
{
Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
Cec_ManSim_t * pSim;
- int RetValue, clkTotal = clock();
+ int RetValue;//, clkTotal = clock();
assert( (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) % Gia_ManPiNum(pAig) == 0 );
Cec_ManSimSetDefaultParams( pParsSim );
pParsSim->nFrames = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
diff --git a/src/proof/fraig/fraigMan.c b/src/proof/fraig/fraigMan.c
index 0e1dcc66..125a4da1 100644
--- a/src/proof/fraig/fraigMan.c
+++ b/src/proof/fraig/fraigMan.c
@@ -103,8 +103,8 @@ void Prove_ParamsPrint( Prove_Params_t * pParams )
printf( "BDD size limit for bailing out: %d\n", pParams->nBddSizeLimit );
printf( "BDD reordering enabled: %s\n", pParams->fBddReorder? "yes":"no" );
printf( "Last-gasp mitering limit: %d\n", pParams->nMiteringLimitLast );
- printf( "Total conflict limit: %ld\n", (int)pParams->nTotalBacktrackLimit );
- printf( "Total inspection limit: %ld\n", (int)pParams->nTotalInspectLimit );
+ printf( "Total conflict limit: %d\n", (int)pParams->nTotalBacktrackLimit );
+ printf( "Total inspection limit: %d\n", (int)pParams->nTotalInspectLimit );
printf( "Parameter dump complete.\n" );
}
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c
index a02ecc3f..80268a73 100644
--- a/src/sat/bsat/satSolver2.c
+++ b/src/sat/bsat/satSolver2.c
@@ -331,8 +331,8 @@ static inline void act_var_rescale(sat_solver2* s) {
s->var_inc = Abc_MaxInt( s->var_inc, (1<<4) );
}
static inline void act_clause_rescale(sat_solver2* s) {
- static int Total = 0;
- int i, clk = clock();
+// static int Total = 0;
+ int i;//, clk = clock();
unsigned * claActs = (unsigned *)veci_begin(&s->claActs);
for (i = 1; i < veci_size(&s->claActs); i++)
claActs[i] >>= 14;
diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c
index 61c4d4d3..4bdefc6d 100644
--- a/src/sat/msat/msatOrderH.c
+++ b/src/sat/msat/msatOrderH.c
@@ -282,10 +282,11 @@ timeSelect += clock() - clk;
int Msat_HeapCheck_rec( Msat_Order_t * p, int i )
{
return i >= HSIZE(p) ||
- ( HPARENT(i) == 0 ||
(
- !HCOMPARE(p, HHEAP(p, i), HHEAP(p, HPARENT(i))) ) &&
+ ( HPARENT(i) == 0 || !HCOMPARE(p, HHEAP(p, i), HHEAP(p, HPARENT(i))) ) &&
+
Msat_HeapCheck_rec( p, HLEFT(i) ) &&
+
Msat_HeapCheck_rec( p, HRIGHT(i) )
);
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 21:24:10 +0000