summaryrefslogtreecommitdiffstats
path: root/src/sat/fraig
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/fraig')
-rw-r--r--src/sat/fraig/fraigFeed.c1
-rw-r--r--src/sat/fraig/fraigInt.h2
-rw-r--r--src/sat/fraig/fraigMan.c9
3 files changed, 5 insertions, 7 deletions
diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c
index 8a3cc6c7..e1e8d12c 100644
--- a/src/sat/fraig/fraigFeed.c
+++ b/src/sat/fraig/fraigFeed.c
@@ -634,7 +634,6 @@ void Fraig_FeedBackCheckTable( Fraig_Man_t * p )
Fraig_HashTable_t * pT = p->pTableF;
Fraig_Node_t * pEntF, * pEntD;
int i, k, m, nPairs;
- int clk = clock();
nPairs = 0;
for ( i = 0; i < pT->nBins; i++ )
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index dc7bc815..c13d7083 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -107,7 +107,7 @@
// copied from "extra.h" for stand-aloneness
#define Fraig_PrintTime(a,t) printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
-#define Fraig_HashKey2(a,b,TSIZE) (((unsigned)(a) + (unsigned)(b) * 12582917) % TSIZE)
+#define Fraig_HashKey2(a,b,TSIZE) (((PORT_PTRUINT_T)(a) + (PORT_PTRUINT_T)(b) * 12582917) % TSIZE)
//#define Fraig_HashKey2(a,b,TSIZE) (( ((unsigned)(a)->Num * 19) ^ ((unsigned)(b)->Num * 1999) ) % TSIZE)
//#define Fraig_HashKey2(a,b,TSIZE) ( ((unsigned)((a)->Num + (b)->Num) * ((a)->Num + (b)->Num + 1) / 2) % TSIZE)
// the other two hash functions give bad distribution of hash chain lengths (not clear why)
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index 12cb5c45..cbeef4c6 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -95,13 +95,13 @@ void Prove_ParamsPrint( Prove_Params_t * pParams )
printf( "Multiplicative coeficient for mitering: %.2f\n", pParams->nMiteringLimitMulti );
printf( "Starting number of rewriting iterations: %d\n", pParams->nRewritingLimitStart );
printf( "Multiplicative coeficient for rewriting: %.2f\n", pParams->nRewritingLimitMulti );
- printf( "Starting number of conflicts in fraiging: %d\n", pParams->nFraigingLimitMulti );
+ printf( "Starting number of conflicts in fraiging: %.2f\n", pParams->nFraigingLimitMulti );
printf( "Multiplicative coeficient for fraiging: %.2f\n", pParams->nRewritingLimitMulti );
- printf( "BDD size limit for bailing out: %.2f\n", pParams->nBddSizeLimit );
+ 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: %d\n", pParams->nTotalBacktrackLimit );
- printf( "Total inspection limit: %d\n", pParams->nTotalInspectLimit );
+ printf( "Total conflict limit: %lld\n", pParams->nTotalBacktrackLimit );
+ printf( "Total inspection limit: %lld\n", pParams->nTotalInspectLimit );
printf( "Parameter dump complete.\n" );
}
@@ -347,7 +347,6 @@ void Fraig_ManCreateSolver( Fraig_Man_t * p )
void Fraig_ManPrintStats( Fraig_Man_t * p )
{
double nMemory;
- int clk = clock();
nMemory = ((double)(p->vInputs->nSize + p->vNodes->nSize) *
(sizeof(Fraig_Node_t) + sizeof(unsigned)*(p->nWordsRand + p->nWordsDyna) /*+ p->nSuppWords*sizeof(unsigned)*/))/(1<<20);
printf( "Words: Random = %d. Dynamic = %d. Used = %d. Memory = %0.2f Mb.\n",