diff options
Diffstat (limited to 'src/sat/fraig')
-rw-r--r-- | src/sat/fraig/fraigFeed.c | 1 | ||||
-rw-r--r-- | src/sat/fraig/fraigInt.h | 2 | ||||
-rw-r--r-- | src/sat/fraig/fraigMan.c | 9 |
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", |